[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