coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Ralf Jung <jung AT mpi-sws.org>
To: coq-club AT inria.fr, ekcburak AT hotmail.com
Subject: Re: [Coq-Club] fun <-> forall
Date: Thu, 26 Oct 2017 13:13:00 +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:GdqK6xIx9S3o8ssajtmcpTZWNBhigK39O0sv0rFitYgXLf3xwZ3uMQTl6Ol3ixeRBMOAtKIC1rKempujcFJDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBWB6kG1uDUVA1D0MRd/DuXzAI/bycqtk6i/+JbZfh9BhxK9Zq93JRSy6w7Ws5o4m4xnf5w4zhWBgGZOdKwCx35uKnqWhxe5/dirupl5/HID6Loa68dcXPCiLOwDRrtCAWF+Pg==

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