coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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.
>>>
>>>
>>>
- Re: [Coq-Club] fun <-> forall, (continued)
- 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, Jason Gross, 10/31/2017
- Re: [Coq-Club] fun <-> forall, Cyril Cohen, 10/31/2017
Archive powered by MHonArc 2.6.18.