The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

How about this:

Goal forall f, let x:=1 in let y:=2 in f x y.

Proof.

  intro.

  match goal with

    | [ |- appcontext G[let x := ?v in @?P x] ]

      => let G' := context G[P v] in

         change G';

           cbv beta

  end.

I don't think it works under binders, though...

On Wed, Feb 11, 2015 at 3:44 AM, Cedric Auger <sedrikov AT gmail.com> wrote:

If I remember well, when you have a definition in your context, for example given by something like "set (a:=term).", when you revert this hypothesis, you end up with a let binding in the goal. ("revert a." produces "let a := term in …"). Maybe that the tactic language (I hardly ever use it) can pattern match let bindings to do the reverse. With an "unset" tactic, you could stack/unstack definitions. Then the "subst" tactic (maybe unfold as well?) would allow you to unfold the let bindings and have a zeta reduction (but from the hypothesis-definitions, not directly from the goal).

2015-02-11 0:05 GMT+01:00 Jonathan Leivent <jonikelee AT gmail.com>:

Given a term, is there a way to do selective zeta reduction, so that only certain local definitions are reduced?  For example, consider a term like:

  let x:=1 in let y:=2 in f x y

is there a way to do zeta reduction only on y, to end up with:

  let x:=1 in f x 2

I'm not even sure how one would pick out which local definition to target - perhaps by its value or type.  Even if there was just a way to reduce only the outermost local definition, that could perhaps be used to build a more general approach.

Is there anything along these lines in Coq?

-- Jonathan