The Coq mailing list

[Samuel Gruetter <gruetter AT mit.edu>]

Hi Clément,

this is a fun exercise :)

Below is my solution, which, depending on taste, might be called simpler ;-)

Instead of constructing an explicit proof term, I construct the hypothesis I want to prove, and then prove it with "rewrite".

Cheers,

Sam

Ltac rev_funct_ext_goal e10 e20 res1 res2 :=
  let e1 := eval cbv beta in e10 in
  let e2 := eval cbv beta in e20 in
  match e1 with
  | fun x1 => @?f1 x1 => match e2 with
    | fun x2 => @?f2 x2 =>
        let z := fresh "x" in
        exact (forall z, ltac:(rev_funct_ext_goal (f1 z) (f2 z) (res1 z) (res2 z)))
    end
  | _ => exact (res1 = res2)
  end.

Ltac rev_funct_ext H :=
  match type of H with
  | ?e1 = ?e2  =>
      (* can't use assert instead of cut because assert implicitly does "cbv beta",
         and then "rewrite H" will not work any more *)
     let P := constr:(ltac:(rev_funct_ext_goal e1 e2 e1 e2)) in cut P;
     [ let H' := fresh H in intro H'; cbv beta in H'
     | intros; rewrite H; reflexivity]
  end.

Axiom catC: Type.
Axiom obj: Type -> Type.
Axiom arrow: forall (catC: Type), obj catC -> obj catC -> Type.
Axiom fmap : forall {C: Type} (a b: obj C), arrow C b a -> Type.
Axiom foo : forall {C a b}, arrow C b a -> arrow C b a.

Goal ((fun (a b : obj catC) (f : arrow catC b a) => fmap a b (foo f)) =
      (fun (a b : obj catC) (f : arrow catC b a) => fmap a b f) -> True).
Proof.
  intros.
  rev_funct_ext H.
Abort.

Goal (fun a b => a + b) = (fun a b => a - b) -> False.
intro H. rev_funct_ext H. specialize (H0 1 1). discriminate.
Qed.

---------- Forwarded message ----------
From: Clément Pit-Claudel <cpitclaudel AT gmail.com>
Date: Thu, Oct 26, 2017 at 12:07 PM
Subject: Re: [Coq-Club] fun <-> forall
To: Burak Ekici <ekcburak AT hotmail.com>, "coq-club AT inria.fr" <coq-club AT inria.fr>


Turning this into a tactic turns out to be surprisingly tricky.  Can someone share a better solution? Here's mine:

    Ltac specialize_eq_ind_argument eql x :=
      constr:(fun f => ltac:(lazymatch (eval cbv beta in (eql f)) with
                          | ?l = ?r => exact (l x = r x)
                          end)).

    Ltac quantify_equality eql arrow_type k :=
      lazymatch (eval cbv beta in arrow_type) with
      | forall (h:?hd), @?tl h =>
        let binder := fresh "x" in
        constr:(fun (binder: hd) =>
                  ltac:(let eql_with_hd := specialize_eq_ind_argument eql binder in
                        let with_tl := quantify_equality eql_with_hd (tl binder) k in
                        exact with_tl))
      | _ => k eql
      end.

    Ltac reverse_functional_extensionality H :=
      lazymatch type of H with
      | _ = ?g =>
        let tg := type of g in
        let pr := quantify_equality (fun f0 => f0 = g) tg ltac:(fun eql => constr:(eq_ind_r eql eq_refl H)) in
        let h' := fresh H in
        pose proof pr as h';
        cbv beta in h'
      end.

And here's an example:

    Axiom catC: Type.
    Axiom obj: Type -> Type.
    Axiom arrow: forall (catC: Type), obj catC -> obj catC -> Type.
    Axiom fmap : forall {C: Type} (a b: obj C), arrow C b a -> Type.
    Axiom foo : forall {C a b}, arrow C b a -> arrow C b a.

    Goal ((fun (a b : obj catC) (f : arrow catC b a) => fmap a b (foo f)) =
          (fun (a b : obj catC) (f : arrow catC b a) => fmap a b f) -> True).
    Proof.
      intros.
      reverse_functional_extensionality H.

Clément.

On 2017-10-26 11:11, Burak Ekici wrote: > Hi Clément, > > Thanks a lot! That's exactly what I was looking for... > > Best, > > ― > > Burak. > > > > On 26-10-2017 18:08, Clément Pit-Claudel wrote: >> On 2017-10-26 10:25, Burak Ekici wrote: >>> However, could not make it work whatever I did... >> Does the following work for you? >> >>    pose proof (fun x y z => eq_ind_r (fun f => f x y z = _ x y z) eq_refl H1c) as H'; >>      cbv beta in H'. >> >> Here's a complete example: >> >> Axiom catC: Type. >> Axiom obj: Type -> Type. >> Axiom arrow: forall (catC: Type), obj catC -> obj catC -> Type. >> Axiom fmap : forall {C: Type} (a b: obj C), arrow C b a -> Type. >> Axiom foo : forall {C a b}, arrow C b a -> arrow C b a. >> >> Goal ((fun (a b : obj catC) (f : arrow catC b a) => fmap a b (foo f)) = >>        (fun (a b : obj catC) (f : arrow catC b a) => fmap a b f) -> True). >> Proof. >>    intros. >>    pose proof (fun x y z => eq_ind_r (fun f => f x y z = _ x y z) eq_refl H) as H'; >>      cbv beta in H'. >> >