The Coq mailing list

[Agnishom Chattopadhyay <agnishom AT cmi.ac.in>]

I realized that hnf was not working because what I had was something like "(eval (FAnd (FOr f g) h) x) = ...." but it does seem to work when I pull out the term and use hnf on it. Is there a way I can use hnf on one branch of the equality?

The issue with most strategies I can think of is that they are becoming rather long-winded, and I am having to copy-paste large chunks of the terms obscuring my proof text, especially for something which is a rather simple algebraic manipulation

On Wed, May 27, 2020 at 7:08 PM jonikelee AT gmail.com <jonikelee AT gmail.com> wrote:

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.