The Coq mailing list

["jonikelee AT gmail.com" <jonikelee AT gmail.com>]

On Wed, 27 May 2020 17:45:55 -0400
"jonikelee AT gmail.com" <jonikelee AT gmail.com> wrote:

> Sorry, did a non-list send by accident.  Resending...
> 
> On Wed, 27 May 2020 16:25:29 -0500
> Agnishom Chattopadhyay <agnishom AT cmi.ac.in> wrote:
> 
> > No, it did not.
> > 
> > Is there a tactic which says "do one step of reduction"?    
> 
> I have developed beta1 and zeta1 tactics that do one step of those
> reductions, but none that would help here.  
> 
> Are you sure hnf doesn't work?  I tried it, and it seemed to work for
> me:

It might not be working for you if the term is "e = (eval (FAnd
(FOr f g) h) x)" - meaning that the head is equals, not eval.  You can
use the set tactic to pull out the rhs of that equation, and use a match
tactic to drive the set:

For instance, if your goal is "e = (eval (FAnd (FOr f g) h) x)", one can
do something like:
match goal with |- e = ?R => let t:=fresh in set (t:=R) in *; hnf in t;
subst t end.

If the equation is intead the type of some hyp H, use "match type of H
with e = ?R ..." instead.