The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Coq Users,

I was following this discussion and I think there is one implied question in 
the original post which hasn't been answered as yet: Petar wrote that he used 
coqc with -dont-load-proofs and it still made a speed difference between 
defining the inversions rules as axioms and deriving them. I thought that the 
difference between ending a proof with Qed and Defined is that in the first 
case the proof term remains opaque and only the information that the proof 
exists may be used in further steps, but not the proof term as such. So I 
don't understand why the speed difference between axioms and opaque proofs 
exists and would very much appreciate if someone could explain why this is.

In Coq 8.5 I got the impression that proof terms are not loaded unless really 
used e.g. in a Print. A Print of an imported proof results in a message that 
an opaque proof term has been loaded from a library. Also the background 
proof mechanism of CoqIDE makes the user believe that Coq 8.5 can handle 
opaque proofs. 

Finally I wonder what effect it would have to put the proofs into a module 
and then remove the proof terms by opaque signature ascription. In my 
experience this makes the proofs more opaque than Qed does, e.g. they are no 
longer accessible to Print. Would it still be required to load the proof 
terms when such an opaque module is loaded from a library?

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, Prof. Dr. Hermann Eul
Chairperson of the Supervisory Board: Tiffany Doon Silva
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928