The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Does this work?  It's shorter, but I don't have a computer at the moment to test it with.

Ltac quantify_equality H :=

  first [ let x := fresh in exact (fun x => ltac:(quantify_equality (f_equal (fun f => f x) H)))

        | exact H ].
Ltac reverse_functional_extensionality H :=
  let H' := fresh in
  rename H into H';
  pose proof (ltac:(quantify_equality H')) as H;

  clear H'.

       

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