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: Anton Trunov <anton.a.trunov AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] fun <-> forall
  • Date: Thu, 26 Oct 2017 15:47:23 +0200
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=anton.a.trunov AT gmail.com; spf=Pass smtp.mailfrom=anton.a.trunov AT gmail.com; spf=None smtp.helo=postmaster AT mail-wm0-f51.google.com
  • Ironport-phdr: 9a23:5vfa2RbcSOuDE0t6fk8MhY3/LSx+4OfEezUN459isYplN5qZpsq6bnLW6fgltlLVR4KTs6sC0LWG9f24EUU7or+/81k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i76vnYuHUD0MhMwLeDoEKbTid623qa84c79eQJN0RO7fbR0ZCmssAPWqIFCiI1+LaB3w13VuGZOfPp+ymZhJFbVlBH5sJTjtKV/+jhd7qpyv/VLVr/3Kvw1

A minor observation: I guess if we simplify the hypothesis, instead of
changing the goal, it makes it easier to solve the original problem:

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.
(* here `repeat` is not necessary, but will handle the case with several
arguments *)
repeat change (fun x => ?f x) with f.
congruence.
Qed.

-Anton

> On 26 Oct 2017, at 13:18, Robbert Krebbers
> <mailinglists AT robbertkrebbers.nl>
> 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