The Coq mailing list

[James Wilcox <wilcoxjay AT gmail.com>]

I am trying to use second-order ltac patterns to implement a reflection tactic that can recurse under binders, roughly following the strategy outlined in the CPDT chapter on reflection. I can't figure out how to write a second-order pattern that matches a function application. 

For example, I would expect to be able to write something like 

Ltac reflect x := 

match eval simpl in x with 

(* other cases here *)

| fun (y : ?T) => (@?F y) (@?A y) => (* ... *)

end.

Coq accepts this definition syntactically, but whenever the case matches, it complains "Only bound indices allowed in second order pattern matching."

The closest I can get to something like this working is to disallow references to bound variables in the left hand side of the application, as follows: 

 fun (y : ?T) => ?F (@?A y) => (* ... *)

This works as long as the tactic never encounters a function application that applies an _expression_ that refers to bound variables, but this is not as general as I'd like.

Does anyone know if there is a way to do this? I've included a complete but simple example showing the issue below.

James

Example:

The goal is to write a tactic that annotates every function application with the function apply, defined as:

Definition apply {A B} (f : A -> B) (x : A) : B := f x.

A version of the desired tactic with the limitations mentioned above is:

Ltac refl' x := 

  lazymatch eval simpl in x with

  | fun x => snd (@?B x) => let r := refl' B in constr:(fun z => snd (r z))

  | fun x => fst (@?B x) => let r := refl' B in constr:(fun z => fst (r z))

  | fun (x : ?T) => x => constr:(fun (z : T) => z)

  | fun (y : ?T) (z : ?U) => @?B y z => 

    let r := refl' (fun (p : T * U) => B (fst p) (snd p)) in

    constr:(fun (y : T) (z : U) => r (y, z))

  | fun (y : ?T) => ?F (@?A y) => let r1 := refl' (fun _ : T => F) in 

                              let r2 := refl' A in 

                              constr:(fun y : T => @apply _ _ (r1 y) (r2 y))

  | fun (_ : ?T) => ?B => constr:(fun (_ : T) => B)

  end.

(* simple driver tactic to print the simplified term constructed by refl' *)

Ltac refl x := 

  let r := refl' (fun _ : unit => x) in 

  let r' := eval simpl in (r tt) in

  idtac r'.

For example, it is able to handle the following simple case:

Goal False.

refl (fun (x : nat) (f : nat -> nat) => S x).

(* prints: (fun (x : nat) (_ : nat -> nat) => apply S x) *)

But of course it doesn't work if the _expression_ being applied refers to bound variables:

Goal False.

refl (fun (x : nat) (f : nat -> nat) => f x).

(* Error: Ltac variable F depends on pattern variable name y 

   which is not bound in current context. *)

Is it possible to implement a version of refl' which handles this case?