The Coq mailing list

[Théo Zimmermann <theo.zimmi AT gmail.com>]

Dear Michael,

Actually, the method described by Nicolas in this paper does not require writing a gallina function mapping axiomatic Z to concrete Z. All you need is to provide a relation between the two types. When you have a function, then this relation can be defined in terms of the function but the technique is much more general than this. You also need to prove a few "transfer lemmas" but they don't need to compute.

Pierre Letouzey and I planned to look at how this technique could apply to the standard library (precisely between axiomatic and concrete representations) as an alternative to the current module based solution to avoid duplication of proofs. But we didn't get started yet...

Cheers,

Théo

Le lun. 21 mai 2018 à 15:20, Soegtrop, Michael <michael.soegtrop AT intel.com> a écrit :

Dear Nicholas,

thanks for the pointer, very interesting!

Just I am not sure if it would be possible to write a gallina function mapping axiomatic Z to concrete Z. In axiomatic Z, the number 2 would be succ(succ(zero)), where succ is a function from ZAxioms.t to ZAxioms.t, not a constructor. What I could do is:

1.) write an Ltac function
2.) define an inductive prop, which relates axiomatic and concrete Z
3.) write such a function assuming a more Church numeral like definition of the axiomatic Z

But as far as I can see none of this would help me to use the techniques you describe with the axiomatic Z from the standard library.

Any suggestions welcome!

Best regards,

Michael
Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928