The Coq mailing list

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

On 03/30/2016 04:48 PM, Thorsten Altenkirch wrote:
> 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.

Fortunately, that's not what I was doing :) I was talking about propositional 
extensionality (see the mail that you quoted).


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

Attachment: signature.asc
Description: OpenPGP digital signature