[om] Little question about Coq theories in OpenMath
Professor James Davenport
jhd at cs.bath.ac.uk
Tue Jul 16 13:37:12 CEST 2002
On Thu, 11 Jul 2002, Olga Caprotti wrote:
> about this issue. It seems to me that both approaches have to be
> allowed: the second (richer CDs) needed when one interfaces Coq with
> systems that have similar formal precision, the first needed when
> Coq talks to systems that basically are not type-aware or formal.
> This first approach is the one I used for the Pocklington example which
> however was dealing with very simple objects to be sent to GAP.
I suspect this is right, though I don't have enough experience of the
different types of equality in Coq to be certain. Note also that not all
symbols are involved: the ordinary arithmetic (modulo divide) and
comparison relations are probably the same.
> Simpler questions have to be answered first when trying to use OpenMath
> instead of Content-MML (with lots of csymbols). For instance,
> Claudio asked me how to convert a function like divide which in Coq
> takes 3 arguments: numerator, denominator and a proof that the
> denominator is not zero. In this case I believe it would be useful
> to have such a divide symbol in OpenMath: it would even be possible to
> keep the extra information in types-unaware systems e.g. using something
> like "assert" in Maple. Maybe James can comment on this further.
A three-argument divide would certainly be possible, though I wonder about
the type of the third argument - it would either have to be "Coq-proof",
which rather militates against the portability of OpenMath, or the
phrasebook would have to know about translating into Coq-proof.
It would also be fundamentally incompatible with other OpenMath
implementations. How about
<OMA>
<OMS name="divide" cd="arith1"/>
x
<OMATTR>
<OMATP>
<OMS name="proofnonzero" cd="proofs1"/>
... <-- some form of proof -->
<OMATP>
y
</OMATTR>
</OMA>
A sufficiently clever phrasebook, possibly calling Coq recursively, might
even be able to construct these proofs.
> I guess the choice of which symbol to put in a CD is an art and not
It does look that way.
> so easy to decide. To this end, it would help to extend HELM to systems
> other that COQ or even to start comparing MBase theories with Coq theories.
Indeed so.
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
More information about the Om
mailing list