The Coq mailing list

[Clément Pit--Claudel <clement.pit AT gmail.com>]

It's a pretty heavy axiom, but it should be fine. Would rephrasing your 
original lemma to use an equivalence instead of equality work, though?

If not, see https://coq.inria.fr/cocorico/CoqAndAxioms and 
https://coq.inria.fr/faq#htoc36 for background on using axioms with Coq.

Best,
Clément.

On 03/30/2016 02:27 PM, Benoît Viguier wrote:
> 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
>  
> <mailto: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.
> 
>

Attachment: signature.asc
Description: OpenPGP digital signature