Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] fun <-> forall

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] fun <-> forall


Chronological Thread 
  • 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.
>>>
>>>
>>>



Archive powered by MHonArc 2.6.18.

Top of Page