The Coq mailing list

[Clément Pit-Claudel <cpitclaudel AT gmail.com>]

On 2017-10-31 01:19, Jason Gross wrote:
> Does this work?  It's shorter, but I don't have a computer at the moment to 
> test it with.

Yes! Much nicer.

> On Thu, Oct 26, 2017, 9:08 AM Clément Pit-Claudel 
> <cpitclaudel AT gmail.com
>  
> <mailto:cpitclaudel AT gmail.com>>
>  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'.
>     >>
>     >
>