The Coq mailing list

[Robbert Krebbers <mailinglists AT robbertkrebbers.nl>]

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.