The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Do your tactics have to return constrs, or is it ok to, e.g., pose a silly goal, solve it, and then use continuation passing style, as in

  Ltac mk_let_in_term term var cont :=

     let T := fresh in

     let t := fresh in

     let H := fresh in

     evar (T : Type); evar (t : T); subst T;

     let t' := (eval unfold t in t) in

     subst t;

     assert (H : term -> term); [ | clear H ];

     [ intro H;

       set (x := var);

       revert x;

       let G := match goal with |- ?G => constr:(G) end in

       unify t' G;

       exact H

     | ];

     instantiate;

     cont t'.

(Note: I haven't actually tested this tactic, as I have to run off now.  But feel free to ask me about it or tell me to rewrite it if it doesn't work.)

-Jason

On Tuesday, September 3, 2013, Gregory Malecha wrote:

Hi, Jason --

That is producing the right term but it requires a lot of goal manipulation and I haven't found a good way use those kinds of tactics to construct the term that I want and then return them to be used by other tactics. 

On Tue, Sep 3, 2013 at 5:57 PM, Jason Gross <jasongross9 AT gmail.com> wrote:

Does [let x := fresh in set (x := bar); try revert x] do what you want?

-Jason

On Tuesday, September 3, 2013, Gregory Malecha wrote:

Hello --

I have a term [foo] with a lot of occurances of a large subterm [bar]. I would like to abstract all of the instances of [bar] and produce a term like:

let x := bar in foo[bar |-> x]

One way to do something like this is with the [pattern] tactic, but this fails when there is dependency on [bar] since it is constructing a lambda abstraction, i.e. it constructs:

(fun x =>  foo[bar |-> x]) bar

I have a plugin/patch that achieves the former but I am wondering if there is an existing way to do it that I don't know about.

Thank you very much.

--

gregory malecha

http://www.people.fas.harvard.edu/~gmalecha/

--

gregory malecha

http://www.people.fas.harvard.edu/~gmalecha/