coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re:[Coq-Club]

From: Clément Pit--Claudel <clement.pit AT gmail.com>
To: coq-club AT inria.fr
Subject: Re:[Coq-Club]
Date: Wed, 30 Mar 2016 13:36:20 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=clement.pit AT gmail.com; spf=SoftFail smtp.mailfrom=clement.pit AT gmail.com; spf=None smtp.helo=postmaster AT mout.kundenserver.de
Ironport-phdr: 9a23:r2ENsBH6SZjZEfGENLkaoJ1GYnF86YWxBRYc798ds5kLTJ75o8mwAkXT6L1XgUPTWs2DsrQf27qQ6fCrBTRIyK3CmU5BWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYsExnyfTB4Ov7yUtaLyZ/nh6boq9aPO01hv3mUX/BbFF2OtwLft80b08NJC50a7V/3mEZOYPlc3mhyJFiezF7W78a0+4N/oWwL46pyv50IbaKvdKMhCLdcET4OMmYv5cStuwOQYxGI4y43VuQTnxxUNDDE8FS/dZP4ryf3sqIp0y2XOMDwUfYsWCiK4KJiSRuugyACYW1quFrLg9B92foI6CmqoAZyltbZ

On 03/30/2016 01:12 PM, Benoît Viguier wrote:
> Can someone explain me why I am not allowed to complete this proof ? Using
> the functionnal extensionality, it should be right. No ?

No. You need Prop Extensionality for that rewrite to be valid.

Axiom prop_ext : forall (P Q : Prop),
(P <-> Q) -> P = Q.
apply prop_ext.
rewrite Nat.leb_le.
reflexivity.

Clément.

Attachment: signature.asc
Description: OpenPGP digital signature

[Coq-Club], Benoît Viguier, 03/30/2016
- Re:[Coq-Club], Pierre Casteran, 03/30/2016
- Re:[Coq-Club], Clément Pit--Claudel, 03/30/2016
  - Re:[Coq-Club], Benoît Viguier, 03/30/2016
    - Re:[Coq-Club], Clément Pit--Claudel, 03/30/2016
      - Re:[Coq-Club], Thorsten Altenkirch, 03/30/2016
        
        Re:[Coq-Club], roux cody, 03/30/2016
        
        Re:[Coq-Club], Thorsten Altenkirch, 03/30/2016
        
        Re:[Coq-Club], Clément Pit--Claudel, 03/30/2016
        
        Re:[Coq-Club], Thorsten Altenkirch, 03/30/2016
- Re:[Coq-Club], Emilio Jesús Gallego Arias, 03/30/2016