The Coq mailing list

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

One wonders, if we all have developed these toolboxes of tricks to get
single-step reductions because Coq doesn't provide them: perhaps Coq
should provide them?

Attached are some single-step beta and zeta reduction term-manipulating
tactics, along with a related pattern-based subst tactic.  I haven't
tested these since Coq 8.6.

Jonathan

On Thu, 28 May 2020 20:40:09 +0200
Christian Doczkal <christian.doczkal AT inria.fr> wrote:

> If one only runs into the need for blocking reduction every once in a
> while, one can also do:
> 
> Definition locked {X} (x:X) := x.
> Lemma lock {X} (x:X) : x = locked x. Proof. reflexivity. Qed.
> Opaque locked.
> 
> Goal forall {A} (f g h: @Formula A) x,
>     exists y, eval (FAnd (FOr f g) h) x = y.
> Proof.
>   eexists.
>   rewrite (lock (FOr _ _)); simpl; rewrite <- lock.
> Abort.
> 
> (Or: "rewrite [FOr _ _]lock /= -lock" when using the ssreflect
> rewrite)
> 
> Best,
> Christian
> 
> On 5/28/20 6:30 PM, Clément Pit-Claudel wrote:
> > 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.
> >   

(***********************************************************************

Single Step beta and zeta reduction, and associated substitution tactics

***********************************************************************)


Ltac subst_binder x c T :=
  (*Do the substitution "T[x := c]" without any other reduction. Requires that
  x be an intropattern and T a constr_with_bindings that needs a binding for x
  - these are the types one gets when matching T under a binder for x*)
  (*How it works: the constr for the lazymatch uses let-ins that are then
  unfolded within the tactic-in-term by delta reduction, making the let-in
  bindings be unused by the resulting proof term (z).  The lazymatch can then
  ignore (via underscores) the unused let-in binders and pick out the result
  (T'), which is then a normal constr instead of a constr_with_bindings.*)
  let r := fresh in
  lazymatch constr:
    (let x := c in let r := T in ltac:(let z := (eval cbv delta [x r] in r) in
                                     exact z)) with
    (let _ := _ in let _ := _ in ?T') => T'
  end.

Ltac zeta1 term :=
  (*Do a single zeta reduction step on a let-in term, such that nothing else
  within the term is reduced*)
  lazymatch term with
  | (let x := ?c in ?T) => subst_binder x c T
  | _ => fail "zeta1: There is no outer let-in in" term
  end.

Ltac beta1 term :=
  (*Do a single beta reduction step on a fun application term, such that
  nothing else within the term is reduced*)
  lazymatch term with
  | ((fun x => ?T) ?c) => subst_binder x c T
  | (?F ?A) => let F' := beta1 F in constr:(F' A)
  | _ => fail "beta1: There is no fun application at the head of" term
  end.

Ltac subarg_beta1 c T :=
  (*T must be a function application, into which c is substituted for the
  outermost arg, and then a single beta reduction is done.  The primary
  purpose is when T is the result of eval pattern, making some common subterm
  into its outermost arg, and then c is substituted for that subterm*)
  lazymatch T with
    (?F _) => let T' := constr:(F c) in beta1 T'
  end.

Ltac subst_in p c T :=
  (*Do the substitution "T[p := c]" without any other reduction, and with p
  and T being normal constrs, with all of p free in T*)
  (*Unfortunately, we can't pass a position selector to eval pattern unless
  this is a Tactic Notation, but a Tactic Notation can't return a constr.  If
  a position is needed, replicate the eval-pattern-subarg_beta1 term with the
  position inserted into the eval-pattern part.*)
  let T' := (eval pattern p in T) in subarg_beta1 c T'.

(*** Unit Tests ***)

Goal True.
Proof.
  let t := constr:(let a := 1 in let b := 2 in a + b) in
  let t' := zeta1 t in
  constr_eq t' (let b := 2 in 1 + b).

  let t := constr:((fun x => x) (let a := 1 in a)) in
  tryif (let t' := zeta1 t in idtac t')
  then fail "zeta1 should have failed on" t else idtac.

  let t := constr:(let a := (let b := 1 in b) in a + 1) in
  let t' := zeta1 t in
  constr_eq t' ((let b := 1 in b) + 1).

  let t := constr:(let a := 1 in (fun x => x + a) 3) in
  let t' := zeta1 t in
  constr_eq t' ((fun x => x + 1) 3).

  let t := constr:(let a := Type in a) in
  let t' := zeta1 t in
  constr_eq t' Type.

  let t := constr:(id (let a := 1 in a)) in
  tryif (let t' := zeta1 t in idtac t')
  then fail "zeta1 should have failed on" t else idtac.

  let t := constr:((fun x y => x + y) 1 2) in
  let t' := beta1 t in
  constr_eq t' ((fun y => 1 + y) 2).
  
  let t := constr:((fun x => x) (fun y => 1 + y) 2) in
  let t' := beta1 t in
  constr_eq t' ((fun y => 1 + y) 2).

  let t := constr:((fun x => let y := 1 in x + y) 2) in
  let t' := beta1 t in
  constr_eq t' (let y := 1 in 2 + y).

  let t := constr:(let a := 1 in ((fun x => a + x) 2)) in
  tryif (let t' := beta1 t in idtac t')
  then fail "beta1 should have failed on" t else idtac.
  
  let t := constr:((id (fun x => x)) 1) in
  tryif (let t' := beta1 t in idtac t')
  then fail "beta1 should have failed on " t else idtac.

  let t := constr:((fun x => x) Type) in
  let t' := beta1 t in
  constr_eq t' Type.

  pose proof 0 as a.
  let t := constr:((fun c => let b := (a + 1) in c + a + b + a) (a + 2)) in
  let t' := subst_in a (a + 3) t in
  constr_eq t' ((fun c => let b := (a + 3 + 1) in c + (a + 3) + b + (a + 3)) ((a + 3) + 2));
  let t'' := subst_in (a + 3) 42 t' in
  constr_eq t'' ((fun c => let b := (42 + 1) in c + 42 + b + 42) (42 + 2)).

  exact I.
Qed.