The Coq mailing list

[Maximilian Wuttke <mwuttke97 AT posteo.de>]

Hi, I have two ideas.

1. You could use `change` with patterns, like `change eval (FAnd ?t1
?t2) with (eval ?t1 && eval ?t2)`. This way you wouldn't have to spell
out t1 and t2. Also `change` supports `at`.

2. You could use rewriting. Have a rewriting lemma for every 'rule'.
`setoid_rewrite lem at num` could be used to specify the position where
to rewrite (I usually try out different values for `num`).

On 28/05/2020 15:41, Agnishom Chattopadhyay wrote:
> 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
> <mailto:jonikelee AT gmail.com> <jonikelee AT gmail.com
> <mailto:jonikelee AT gmail.com>> wrote:
> 
>     On Wed, 27 May 2020 17:45:55 -0400
>     "jonikelee AT gmail.com <mailto:jonikelee AT gmail.com>"
>     <jonikelee AT gmail.com <mailto: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
>     <mailto: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.
>