Skip to Content.
Sympa Menu

coq-club - [Coq-Club]extensionality and eta-conversion

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club]extensionality and eta-conversion


chronological Thread 
  • From: Fabrice Lemercier <nouvid-coq AT yahoo.fr>
  • To: coq-club AT pauillac.inria.fr
  • Subject: [Coq-Club]extensionality and eta-conversion
  • Date: Wed, 2 Aug 2006 03:51:09 +0200 (CEST)
  • Domainkey-signature: a=rsa-sha1; q=dns; c=nofws; s=s1024; d=yahoo.fr; h=Message-ID:Received:Date:From:Reply-To:Subject:To:MIME-Version:Content-Type:Content-Transfer-Encoding; b=YrlE6PPJII62J9eH0zsyB4Ti4XZ7BqAumFLCpBc8D2sJmll8dfZJ/ajA8NCc0UQdU/cMGXyVMbYjDvWzj3C7AtE5X/u9aTFC2f2Va48y9OXYBA2b2VUhlJH5iQavlyD91T0xPHt+Kd1LLz+/UNmyn8nOq4JaeE/xK+BDP4WgACg= ;
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Hello,

I can prove in Coq that extensionality implies
eta-conversion.
How can I prove the  converse?

Lemma ext_eta :
  forall  A B:Set,
  (forall f1 f2:A->B, (forall x, f1 x = f2 x) -> f1 =
f2) ->
  (forall f:A->B, (fun x => f x) = f).
Proof.
intros.
apply H.
intro.
reflexivity.
Qed.

Lemma eta_ext :
  forall A B:Set,
  (forall f:A->B, (fun x => f x) = f) ->
  (forall f1 f2:A->B, (forall x, f1 x = f2 x) -> f1 =
f2).
Proof.
???



        

        
                
___________________________________________________________________________ 
Découvrez un nouveau moyen de poser toutes vos questions quelque soit le 
sujet ! 
Yahoo! Questions/Réponses pour partager vos connaissances, vos opinions et 
vos expériences. 
http://fr.answers.yahoo.com ;



Archive powered by MhonArc 2.6.16.

Top of Page