The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

And now sufficiently many bugs have been fixed that the following works correctly in trunk:

Ltac ret_and_left T :=

  let t := type of T in

  lazymatch eval hnf in t with

    | ?a /\ ?b => constr:(proj1 T)

    | forall x : ?T', @?f x =>

      let tac := ret_and_left in

      let ret := constr:(fun x' : T' => let fx := T x' in

                                        $(let t := tac fx in

                                          exact t)$) in

      let ret' := (eval cbv zeta in ret) in

      ret'

  end.

-Jason

On Wed, Mar 5, 2014 at 3:19 PM, Jason Gross <jasongross9 AT gmail.com> wrote:

I have long been annoyed that I could not recurse under binders in Ltac, and jumped through many hoops to fake it.  I recently discovered, that in Coq 8.5, this will be possible!  (And it already is in trunk, modulo a few bugs.)  I thought others in the Coq community might like to know this.

Here is some code that runs in trunk (and demos this feature and both bugs):

Ltac ret_and_left T :=
  let t := type of T in
  lazymatch eval hnf in t with
    | ?a /\ ?b => constr:(proj1 T)
    | forall x : ?T', @?f x =>
      let tac := ret_and_left in
      constr:(fun x : T' => $(let fx := constr:(T x) in
                              let t := tac fx in
                              exact t)$)
  end.

Goal forall A B : Prop, (A -> A -> A /\ B) -> True. intros. let t' := ret_and_left H in pose t'.

(* we get [a := fun _ x0 : A => proj1 (H x0 x0) : A -> A -> A]

we should get [a := fun x0 x1 : A => proj1 (H x0 x1) : A -> A -> A]. *)

-Jason