The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

(* this doesn't work, I don't really know why...

*)

Ltac sk3 t :=

match eval hnf in t with

| (fun z => ?t') =>

let m := do_sk z t'

in change t with m

end.

sk3 doesn't work because ?t' cannot mention z, and z is unbound in do_sk z t'.  You can get the error message that it complains about by changing [match] to [lazymatch].  I agree with Adam that proof by reflection should work, and "Building a Reification Tactic that Recurses Under Binders" at http://adam.chlipala.net/cpdt/html/Reflection.html explains how, as well as explaining what I said above.  Alternatively, I think mtac gives you the ability to recurse under binders in a nice way.

-Jason

On Sunday, September 15, 2013, Adam Chlipala  wrote:

On 09/15/2013 03:25 PM, robert wrote:

I've copied below a simplified version of a tactic I've been playing with recently to automatically convert terms into applicative form using SKI combinators. (why? I'm evaluating the hypothesis that proof automation for properties about functions works better when things are in applicative form)

 

The hard part here is opening up lambda-terms to work on their bodies. I've found a trick that lets me do pretty much what I want, but it has the side-effect of generating useless and potentially large proof structure. I've found this can have a noticable effect on Qed time for some examples. I wonder if there is a way to accomplish the same thing without cluttering up the generated proof.

Have you read Section 15.5 of CPDT <http://adam.chlipala.net/cpdt/>?  I haven't read all of the code you included, but the prose makes it sound like that section shows how to do what you're looking for.