The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

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