The Coq mailing list

[roux cody <cody.roux AT gmail.com>]

I think he was referring to *propositional extensionality* AKA

pext : forall p q : Prop, (p <-> q) <-> p = q

This is not really comparable with functional extensionality, but it "feels" strong, since it's approximately the excluded middle (I don't think it implies it though). It does imply proof irrelevance.

This was found to lead to non-termination and inconsistency in some version as documented here
https://sympa.inria.fr/sympa/arc/coq-club/2013-12/msg00119.html

But I believe this was fixed shortly afterwards. I think efforts are made for this principle to be consistent with the current Coq implementation, since it holds in the "proof-irrelevant model" which is often taken as the informal mental model of the system.

Best,

Cody

On Wed, Mar 30, 2016 at 10:48 AM, Thorsten Altenkirch <Thorsten.Altenkirch AT nottingham.ac.uk> wrote:

Why would you call ³functional extensionality² a ³strong axiom²? It is
certainly accepted in HoTT (as a consequence of univalence) and it seems
rather an error that it is not provable in Coq (however, one which isn¹t
so easy to fix but see iur work on OTT).

I don¹t know what Maxime said, but it rather seems that functional
extensionality can reveal problems with other principles. However, it is
very wrong then to blame functional extensionality.

Thorsten

On 30/03/2016 13:40, "Clément Pit--Claudel" <clement.pit AT gmail.com> wrote:

>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.
>>
>>
>

This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please send it back to me, and immediately delete it.

Please do not use, copy or disclose the information contained in this
message or in any attachment.  Any views or opinions expressed by the
author of this email do not necessarily reflect the views of the
University of Nottingham.

This message has been checked for viruses but the contents of an
attachment may still contain software viruses which could damage your
computer system, you are advised to perform your own checks. Email
communications with the University of Nottingham may be monitored as
permitted by UK legislation.