The Coq mailing list

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

Does the hnf tactic work?


On Wed, 27 May 2020 10:55:26 -0500
Agnishom Chattopadhyay <agnishom AT cmi.ac.in> wrote:

> I have something like:
> 
> Inductive Formula {A : Type} : Type :=
> | FAtomic : (A -> bool) -> Formula
> | FAnd : Formula -> Formula -> Formula
> | FOr : Formula -> Formula -> Formula
> .
> 
> and something like
> 
> Fixpoint eval {A : Type} (f : @Formula A) (x : A) : bool :=
> match f with
> | FAtomic f => f x
> | FAnd f g => (eval f x) && (eval g x)
> | FOr f g => (eval f x) || (eval g x)
> end.
> 
> Now, let's say I have a proof and I have an expression e = (FAnd (FOr
> f g) h), and I am trying to simplify (eval e x). If I simply suggest
> `simpl.`, Coq simplifies it all the way down. How can I control simpl
> so that only the first FAnd is simplified but the FOr is not?
> 
> Currently, I am using "replace ... with ... " but this requires me to
> type out all the details, which is very painful. The actual formula
> and eval that I have are more complex than this.
> 
> Another option seems to be `remember (FOr f g) as z.` and then doing
> `simpl.`, but this is also not very nice since I have to copy large
> chunks of the expression to my proof.