coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re:[Coq-Club]

From: Benoît Viguier <beviguier AT gmail.com>
To: coq-club AT inria.fr
Subject: Re:[Coq-Club]
Date: Wed, 30 Mar 2016 14:27:41 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=beviguier AT gmail.com; spf=Pass smtp.mailfrom=beviguier AT gmail.com; spf=None smtp.helo=postmaster AT mail-pa0-f51.google.com
Ironport-phdr: 9a23:oN4VtBZH8O6yPwj4u1aVmqr/LSx+4OfEezUN459isYplN5qZpc+9bnLW6fgltlLVR4KTs6sC0LqG9fqwEjBRqb+681k8M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aJBzzOEJPK/jvHcaK1oLsh7D0oc2YP1QArQH+SI0xBS3+lR/WuMgSjNkqAYcK4TyNnEF1ff9Lz3hjP1OZkkW0zM6x+Jl+73YY4Kp5pIYTGZn9Kq8/VPlTCCksG2Ez/szi8xfZHiWV4X5JeGgQlZxUNDbE4wz7U4255iH3qOtyxSiXJ+X5SLk1XXKp6KI9G0ygszsOKzNsqDKfscd3lq8O+B8=

Hi,

thanks for your quick answers. Is there any risk I should know while using this Axiom ? It seemed it was inconsistent with Coq termination in late 2013 cf Maxime Dénès talk.

Regards.

Benoît

2016-03-30 13:36 GMT+02:00 Clément Pit--Claudel <clement.pit AT gmail.com>:

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.

[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