The Coq mailing list

[James Wilcox <wilcoxjay AT gmail.com>]

Thanks, that seems to work! 

My mental model was that the ?F would not even match if it referred to the bound variable, but I guess that's just not how it works. 

Thanks again!

James

On Sat, May 14, 2016 at 9:17 AM, Guillaume Melquiond <guillaume.melquiond AT inria.fr> wrote:

On 14/05/2016 16:23, James Wilcox wrote:
> 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?

I am still not sure whether it is a bug or a feature, but you are
allowed to reuse "y" there. In other words, instead of calling "refl'
(fun _ : T => F)", call "refl' (fun y : T => F)". That way, any
occurrence of "y" still in "F" will get rebound.

Best regards,

Guillaume