The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Hi,

I realized today that it is possible to make tactics that recurse under binders using typeclasses; I had previously thought that this was possible only in Coq trunk using tactics in terms.  If anyone else is interested in making their tactics recurse under binders on a tactic-by-tactic basis, here is some code demo-ing the trick:

Class ret_and_left {T} (arg : T) {R} := make_recur_ret_and_left : R.

Ltac ret_and_left_helper f :=

  let T := type of f in

  lazymatch eval hnf in T with

    | ?a /\ ?b => exact (proj1 f)

    | ?T' -> _

      => exact (fun x' : T' => _ : ret_and_left (f x'))

  end.

Hint Extern 0 (@ret_and_left _ ?f _) => ret_and_left_helper f : typeclass_instances.

Arguments ret_and_left / .

Goal forall A B : Prop, (A -> A -> A /\ B) -> True.

  intros A B H.

  pose (_ : ret_and_left H) as H'; simpl in H'.

(* fun x' x'0 : A => proj1 (H x' x'0) : A -> A -> A *)

The idea is that, wherever you want to call the tactic recursively, you instead ask for a typeclass instance of the related class, and you pass the arguments to the class instead.

-Jason