The Coq mailing list

[Cedric Auger <Cedric.Auger AT lri.fr>]

Elie Soubiran a écrit :
> Hello Cedric,
>
> In my opinion, it is forbidden because you could easily build two 
> different proofs for a given lemma (using automation for example).
>
> (* runs only on a hacked version of Coq *)
> Require Omega.
>
> Module Type S.
>   Lemma foo : 1+1= 2.
>    omega.
>   Qed.
> End S.
>
> Module M : S.
>   Lemma foo : 1+1 = 2.
>     reflexivity.
>   Qed.
> End M.
>  (* Error: Signature components for label foo do not match.*)
>
> Maybe this restriction is not relevant, we should rather let the user 
> takes care of building the same proof in the signature and in the 
> implementation.
The user has already to do that with lambda terms, so having to do this 
for proofs as well is not a matter...
> Elie
>
> On Thu, Jun 18, 2009 at 6:29 PM, Cedric Auger <Cedric.Auger AT lri.fr 
> <mailto:Cedric.Auger AT lri.fr>> wrote:
>
>     Hi all,
>
>     Is there any special reason to forbide the proof-editing mode in
>     Module Types and allow Definitions?
>
>     Since the proof editing mode is just a way to build Definitions, I
>     don't see the reason to allow directly writing lambda terms but
>     not to use the tools to build them.
>
>     -- 
>     Cédric AUGER
>
>     Univ Paris-Sud, Laboratoire LRI, UMR 8623, F-91405, Orsay
>
>     --------------------------------------------------------
>     Bug reports: http://logical.saclay.inria.fr/coq-bugs
>     Archives: http://pauillac.inria.fr/pipermail/coq-club
>             http://pauillac.inria.fr/bin/wilma/coq-club
>     Info: http://pauillac.inria.fr/mailman/listinfo/coq-club


--
Cédric AUGER

Univ Paris-Sud, Laboratoire LRI, UMR 8623, F-91405, Orsay