coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Ralf Jung <jung AT mpi-sws.org>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] fun <-> forall
- Date: Thu, 26 Oct 2017 13:30:13 +0200
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jung AT mpi-sws.org; spf=Pass smtp.mailfrom=jung AT mpi-sws.org; spf=None smtp.helo=postmaster AT jupiter.mpi-klsb.mpg.de
- Ironport-phdr: 9a23:qwuGNReHLGmg1B92UDLaMP7KlGMj4u6mDksu8pMizoh2WeGdxc2+bR7h7PlgxGXEQZ/co6odzbGJ4+a9ASQp2tWojjMrSNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpW1aJhKqPg1sY+/xB4T6jsKt1un09YeATR9PgW+HaLd8ZDerqwqZ4ssLh4RKL74wjwDWuT1PYesAljAgHk6agxupvpT4x5Vk6SkF4/8=
Oh, right -- I read "Goal" instead of Hypothesis. Sorry for that.
; Ralf
On 26.10.2017 13:18, Robbert Krebbers wrote:
> Unless I am mistaken, what Burak wants goes in the opposite way, so
> function extensionality is not needed.
>
> A simplified example of what I think he asks for:
>
> Goal forall (A B : Type) (f g : A -> B),
> (fun x => f x) = (fun x => g x) ->
> forall x, f x = g x.
> Proof.
> intros A B f g Hfg x.
> change ((fun x => f x) x = (fun x => g x) x).
> rewrite Hfg.
> reflexivity.
> Qed.
>
> On 10/26/2017 01:13 PM, Ralf Jung wrote:
>> Hi Burak,
>>
>> what you are looking for is function extensionality:
>>
>> f = g <-> forall x, f x = g x
>>
>> Function extensionality cannot be proven in Coq, but you can assume it
>> as an axiom. (It is compatible with the theory.)
>>
>> So, the answer to "Is there a way" is "Yes, if you are willing to assume
>> an axiom". You can find it in the standard library at
>> <https://coq.inria.fr/stdlib/Coq.Logic.FunctionalExtensionality.html>.
>>
>> Kind regards,
>> Ralf
>>
>> On 26.10.2017 13:09, Burak Ekici wrote:
>>> Hi all,
>>>
>>> I have an hypothesis of the following form "H : (fun a b f => XX a b f)
>>> = (fun a b f => YY a b f)".
>>>
>>> Is there a way to turn it into "H: forall a b f, XX a b f = YY a b f"?
>>>
>>> Thanks!
>>>
>>> Best,
>>>
>>> ―
>>>
>>> Burak.
>>>
>>>
>>>
- [Coq-Club] fun <-> forall, Burak Ekici, 10/26/2017
- Re: [Coq-Club] fun <-> forall, Ralf Jung, 10/26/2017
- Re: [Coq-Club] fun <-> forall, Robbert Krebbers, 10/26/2017
- Re: [Coq-Club] fun <-> forall, Ralf Jung, 10/26/2017
- Re: [Coq-Club] fun <-> forall, Burak Ekici, 10/26/2017
- Re: [Coq-Club] fun <-> forall, Clément Pit-Claudel, 10/26/2017
- Re: [Coq-Club] fun <-> forall, Burak Ekici, 10/26/2017
- Re: [Coq-Club] fun <-> forall, Clément Pit-Claudel, 10/26/2017
- Message not available
- Re: [Coq-Club] fun <-> forall, Samuel Gruetter, 10/28/2017
- [Coq-Club] Macro for Ltac, Dominique Larchey-Wendling, 10/30/2017
- Re: [Coq-Club] Macro for Ltac, Pierre Courtieu, 10/30/2017
- Re: [Coq-Club] Macro for Ltac, Dominique Larchey-Wendling, 10/30/2017
- Re: [Coq-Club] fun <-> forall, Burak Ekici, 10/26/2017
- Re: [Coq-Club] fun <-> forall, Clément Pit-Claudel, 10/30/2017
- Re: [Coq-Club] fun <-> forall, Clément Pit-Claudel, 10/26/2017
- Re: [Coq-Club] fun <-> forall, Burak Ekici, 10/26/2017
- Re: [Coq-Club] fun <-> forall, Jason Gross, 10/31/2017
- Re: [Coq-Club] fun <-> forall, Ralf Jung, 10/26/2017
- Re: [Coq-Club] fun <-> forall, Robbert Krebbers, 10/26/2017
- Re: [Coq-Club] fun <-> forall, Ralf Jung, 10/26/2017
Archive powered by MHonArc 2.6.18.