# [om] Little question about Coq theories in OpenMath

Professor James Davenport jhd at cs.bath.ac.uk
Sun Jun 30 17:49:53 CEST 2002

On Fri, 28 Jun 2002, Paul Libbrecht wrote:
> A while ago, we had a rather long discussion with the team of Andrea
> Asperti in Bologna on how to export Coq content to OpenMath.
I wish I'd been involved in those, but one can't be everywhere.
> Basically, two approaches were proposed and I have to say I could not
> really decide which is better and would like to have more precise ideas
> on their implications for applications of OpenMath (especially
> phrasebooks and rendering engines):
>
> - their original approach was to say that OpenMath is a "content"
> representation as opposed to a "semantic" (they call it so...)
> representation that Coq has.
> That is, in their conversion to "content" they accept to loose some
> semantics. Among others, there are about nineteen equalities in Coq
> which they all map to the official one of OpenMath.
Well, the'official one' need not be the only one in OpenMath. There are
certainly several equalities. Indeed, I have been working on a ternary
equality "x = y in D", or, for example
<OMA>
<OMS name="eq" cd="relation2"/>
<OMI> 2 </OMI>
<OMI> 5 </OMI>
<OMA>
<OMS name="GFp" cd="setname2"/>
<OMI> 3 </OMI>
</OMA>
</OMA>
I have a paper on equalities, but I certainly can't count to 19, and one
might hope that the above suggestion would handle several of them.
> Inputting an OpenMath object into Coq would then involve guessing, using
> Coq type-checking I guess, the exact symbol attached to the generic
> equality. Wether this task is feasible is, to me, an open question.
Possibly augmented with hints.
> - the other approach is, of course, to define new content dictionaries
> (possibly helped by a declaration framework such as OMDoc) which would
> contain the very rich set of symbols found in the Coq classical
> libraries thus avoid loosing the semantics in the conversion but
> destroying interoperability as all the applications would need to be
> extended to support these content dictionaries if they were to be used.
Several new CDs are certainly needed, and I don't think they would destroy
all inter-operability.
> I think some of the members of the list had attempts with Coq.
> Can they comment on the conversion process ? Could they, for example,
> take advantage of an OpenMath conversion to have Coq delegate
> computational tasks to another mathematical system ??
> Did anyone try to present Coq theories aside of the HELM project ?
James
--
om at openmath.org  -  general discussion on OpenMath
Post public announcements to om-announce at openmath.org
Automatic list maintenance software at majordomo at openmath.org
Mail om-owner at openmath.org for assistance with any problems