The Coq mailing list

[Clément Pit-Claudel <cpitclaudel AT gmail.com>]

On 27/05/2020 11.55, Agnishom Chattopadhyay wrote:
> 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.

This is a common problem with recursive functions in Coq.  Two tricks I like: 

1. Define a set of equations for your function, which you can then use to 
rewrite:

       Open Scope bool_scope.
       Lemma eval_FAnd {A : Type} (f g : @Formula A) (x : A) :
         eval (FAnd f g) x = (eval f x) && (eval g x).
       Proof. reflexivity. Qed.
       (* more equations here *)

       Goal forall {A} (f g h: @Formula A) x,
           exists y, eval (FAnd (FOr f g) h) x = y.
       Proof.
         eexists.
         rewrite eval_FAnd.
       Abort.

   You can also look at the Equation plug-ins — I keep hearing good things 
about it.  This solution quickly gets old quickly if you have many cases, 
though, because you need to define the lemmas.  Also, the rewrites can get 
costly.

2. Define an unfolding function, which does one step of unfolding for you:

       Definition eval1 {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.

       Goal forall {A} (f g h: @Formula A) x,
           exists y, eval (FAnd (FOr f g) h) x = y.
       Proof.
         eexists.
         change (eval ?f ?x) with (eval1 f x). (* No need to rewrite, even! *)
         cbv [eval1].
       Abort.

   Of course, it's still annoying to have to duplicate the function, so you 
can automatically define it:

       Ltac unfold_once expr param :=
         pose expr as result;
         destruct param; cbn in result;
         lazymatch goal with
         | [ _ := ?result |- _ ] => exact result
         end.

       Definition eval1_auto' {A : Type} (f : @Formula A) (x : A) : bool.
         unfold_once (eval f x) f.
       Defined.

       Goal forall {A} (f g h: @Formula A) x,
           exists y, eval (FAnd (FOr f g) h) x = y.
       Proof.
         eexists.
         change (eval ?f ?x) with (eval1_auto' f x).
         cbv [eval1_auto'].
       Abort.

   Here's a slightly cleaner definition, too:

       Definition eval1_auto {A : Type} (f : @Formula A) (x : A) : bool.
         let r := constr:(ltac:(unfold_once (eval f x) f)) in
         let r := eval cbv zeta in r in
         exact r.
       Defined.