The Coq mailing list

[Cyril Cohen <cohen AT crans.org>]

Hello,

Using the view mechanism of ssreflect, you can do this:

From Coq Require Import ssreflect ssrfun.

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.

Lemma congf1 {X Y} {f g : forall u : X, Y u} {x} : f = g -> f x = g x.
Proof. by move->. Qed.

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.
move=> /congf1/congf1/congf1 eq_fmap.
Abort.


Best,

--
Cyril

On 26/10/2017 18:07, Clément Pit-Claudel wrote:
> 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'.