The Coq mailing list

[Elie Soubiran <soubiran AT lix.polytechnique.fr>]

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.


Elie

On Thu, Jun 18, 2009 at 6:29 PM, Cedric Auger <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