Week 1: Basic Program Syntax

Author: Adam Chlipala, with modifications by CS-428 staff.
License: No redistribution allowed (usage by permission in CS-428).

Simple syntax

As a first example, let's look at the syntax of simple arithmetic expressions. We use the Coq feature of modules, which let us group related definitions together. A key benefit is that names can be reused across modules, which is helpful to define several variants of a suite of functionality, within a single source file.

Module ArithWithConstants.

The following definition closely mirrors a standard BNF grammar for expressions. It defines abstract syntax trees of arithmetic expressions.

Inductive arith :=
| Const (n : nat)
| Plus (e1 e2 : arith)
| Times (e1 e2 : arith).

Here are a few examples of specific expressions.

Example ex1 :=
  Const 42.
Example ex2 :=
  Plus (Const 1) (Times (Const 2) (Const 3)).

We can make this expression more readable using notations. There are two ways to do this:

The simplest way allows us to freely mix our own syntax with Coq's usual syntax:

Notation "'$' n" := (Const n)
  (at level 1, format "'$' n").
Infix "+" := Plus.
Infix "*" := Times.

Print ex2.ex2 = $1 + $2 * $3
     : arith

More elaborate, but also more powerful, are “custom entries”, which let us define our own mini-language betweeen custom delimiters. Here, we use « … ».

Declare Custom Entry arith.
Notation "« e »" := (e)
  (e custom arith at level 200).
Notation "n" := (Const n)
  (in custom arith at level 0, n constr at level 0).
Notation "( e )" := (e)
  (in custom arith at level 0, e at level 200).
Infix "+" := Plus
  (in custom arith at level 50).
Infix "*" := Times
  (in custom arith at level 40).

Print ex2.ex2 = « 1 + 2 * 3 »
     : arith

What's the value of an expression? Unlike in many programming languages, in Coq, recursive functions must be marked as recursive explicitly. That marking comes with the Fixpoint command, as opposed to Definition. Note also that Coq checks termination of each recursive definition. Intuitively, recursive calls must be on subterms of the original argument.

Fixpoint eval (e: arith) : nat :=
  match e with
  | Const n => n
  | Plus e1 e2 => eval e1 + eval e2
  | Times e1 e2 => eval e1 * eval e2
  end.

We can run this program (evaluate the corresponding term) using Compute:

Compute eval ex1.= 42
: nat
Compute eval ex2.= 7
: nat

How many nodes appear in the tree for an expression?

Fixpoint size (e : arith) : nat :=
  match e with
  | Const _ => 1
  | Plus e1 e2 => 1 + size e1 + size e2
  | Times e1 e2 => 1 + size e1 + size e2
  end.

Compute size ex1.= 1
: nat
Compute size ex2.= 5
: nat

What's the longest path from the root of a syntax tree to a leaf?

Fixpoint depth (e : arith) : nat :=
  match e with
  | Const _ => 1
  | Plus e1 e2 => 1 + max (depth e1) (depth e2)
  | Times e1 e2 => 1 + max (depth e1) (depth e2)
  end.

Compute depth ex1.= 1
: nat
Compute depth ex2.= 3
: nat

Proofs by induction

Our first proof! Size is an upper bound on depth:

Theorem depth_le_size : forall e,
    depth e <= size e.forall e : arith, depth e <= size e
Proof.forall e : arith, depth e <= size e

Within a proof, we apply commands called tactics. Here's our first one. Keep in mind that the best way to understand what's going on is to run the proof script for yourself, inspecting intermediate states!

  induction e.n: nat
depth (Const n) <= size (Const n)
e1, e2: arith
IHe1: depth e1 <= size e1
IHe2: depth e2 <= size e2
depth (Plus e1 e2) <= size (Plus e1 e2)
e1, e2: arith
IHe1: depth e1 <= size e1
IHe2: depth e2 <= size e2
depth (Times e1 e2) <= size (Times e1 e2)

induction x: Structure the proof by induction on the structure of x, where x is a variable in the theorem statement. You will get one generated subgoal per constructor in the inductive definition of x. (Indeed, it is required that x's type was introduced with Inductive.)

Bullets (-) are used to structure the proof: each bullet corresponds to one goal.

  - (* Const case *)n: nat
depth (Const n) <= size (Const n)
    simpl.n: nat
1 <= 1

simpl: Simplify throughout the goal, applying the definitions of recursive functions directly. That is, when a subterm matches one of the match cases in a defining Fixpoint, replace with the body of that case, then repeat.

    lia.

lia: A complete decision procedure for linear arithmetic. Relevant formulas are essentially those built up from variables and constant natural numbers and integers using only addition, with congruence and incongruence comparisons on top. (Multiplication by constants is supported, as a shorthand for repeated addition.)

  - (* Plus case *)e1, e2: arith
IHe1: depth e1 <= size e1
IHe2: depth e2 <= size e2
depth (Plus e1 e2) <= size (Plus e1 e2)
    simpl.e1, e2: arith
IHe1: depth e1 <= size e1
IHe2: depth e2 <= size e2
S (max (depth e1) (depth e2)) <= S (size e1 + size e2)
    lia.

  - (* Times *)e1, e2: arith
IHe1: depth e1 <= size e1
IHe2: depth e2 <= size e2
depth (Times e1 e2) <= size (Times e1 e2)
    simpl.e1, e2: arith
IHe1: depth e1 <= size e1
IHe2: depth e2 <= size e2
S (max (depth e1) (depth e2)) <= S (size e1 + size e2)
    lia.
Qed.

We are applying the same operations to all goals — wouldn't it be better to say just that?

Theorem depth_le_size_snazzy : forall e,
    depth e <= size e.forall e : arith, depth e <= size e
Proof.forall e : arith, depth e <= size e
  induction e.n: nat
depth (Const n) <= size (Const n)
e1, e2: arith
IHe1: depth e1 <= size e1
IHe2: depth e2 <= size e2
depth (Plus e1 e2) <= size (Plus e1 e2)
e1, e2: arith
IHe1: depth e1 <= size e1
IHe2: depth e2 <= size e2
depth (Times e1 e2) <= size (Times e1 e2)
  all: simpl.n: nat
1 <= 1
e1, e2: arith
IHe1: depth e1 <= size e1
IHe2: depth e2 <= size e2
S (max (depth e1) (depth e2)) <= S (size e1 + size e2)
e1, e2: arith
IHe1: depth e1 <= size e1
IHe2: depth e2 <= size e2
S (max (depth e1) (depth e2)) <= S (size e1 + size e2)
  all: lia.
Qed.

Or even better, look at that!

Theorem depth_le_size_super_snazzy : forall e,
    depth e <= size e.forall e : arith, depth e <= size e
Proof.forall e : arith, depth e <= size e
  induction e; simpl; lia.

Chaining tactics with semicolon, as in t1; t2, asks to run t1 on the goal, then run t2 on every generated subgoal. This is an essential ingredient for automation.

Qed.

A silly recursive function: swap the operand orders of all binary operators.

Fixpoint commuter (e : arith) : arith :=
  match e with
  | Const _ => e
  | Plus e1 e2 => Plus (commuter e2) (commuter e1)
  | Times e1 e2 => Times (commuter e2) (commuter e1)
  end.

Print ex1.ex1 = Const 42
     : arith
Compute commuter ex1.= Const 42
: arith
Print ex2.ex2 =
Plus (Const 1) (Times (Const 2) (Const 3))
     : arith
Compute commuter ex2.= Plus (Times (Const 3) (Const 2)) (Const 1)
: arith

commuter has all the appropriate interactions with other functions (and itself).

Theorem commuter_correct : forall e,
    eval (commuter e) = eval e.forall e : arith, eval (commuter e) = eval e
Proof.forall e : arith, eval (commuter e) = eval e
  induction e; simpl; lia.
Qed.

Theorem size_commuter : forall e,
    size (commuter e) = size e.forall e : arith, size (commuter e) = size e
Proof.forall e : arith, size (commuter e) = size e
  induction e; simpl; lia.
Qed.

Theorem depth_commuter : forall e,
    depth (commuter e) = depth e.forall e : arith, depth (commuter e) = depth e
Proof.forall e : arith, depth (commuter e) = depth e
  induction e; simpl; lia.
Qed.

This last theorem is a bit different, since we prove equalities on arith terms, rather than natural numbers.

Theorem commuter_involutive : forall e,
    commuter (commuter e) = e.forall e : arith, commuter (commuter e) = e
Proof.forall e : arith, commuter (commuter e) = e
  induction e; simpl.n: nat
Const n = Const n
e1, e2: arith
IHe1: commuter (commuter e1) = e1
IHe2: commuter (commuter e2) = e2
Plus (commuter (commuter e1)) (commuter (commuter e2)) =
Plus e1 e2
e1, e2: arith
IHe1: commuter (commuter e1) = e1
IHe2: commuter (commuter e2) = e2
Times (commuter (commuter e1))
  (commuter (commuter e2)) = 
Times e1 e2

To conclude the proof, we find ourselves needing a new tactic, congruence:

  all: congruence.

congruence: A complete decision procedure for the theory of equality and uninterpreted functions. That is, the goal must follow from only reflexivity, symmetry, transitivity, and congruence of equality, including that functions really do behave as functions.

Qed.

Exercise: Working without lia

Try to revisit the proof of commuter_correct without using the lia tactic. Use the Search command to identify relevant theorems, and the rewrite tactic (introduced below) to make use of them.

Theorem commuter_correct_by_hand : forall e,
    eval (commuter e) = eval e.forall e : arith, eval (commuter e) = eval e
Proof.forall e : arith, eval (commuter e) = eval e
  induction e; simpl.n: nat
n = n
e1, e2: arith
IHe1: eval (commuter e1) = eval e1
IHe2: eval (commuter e2) = eval e2
eval (commuter e2) + eval (commuter e1) =
eval e1 + eval e2
e1, e2: arith
IHe1: eval (commuter e1) = eval e1
IHe2: eval (commuter e2) = eval e2
eval (commuter e2) * eval (commuter e1) =
eval e1 * eval e2

Solution

We need three new ingredients:

A tactic to solve a goal of the form a == a:
```
  -n: nat
n = n reflexivity.
```

A theorem to rewrite a + b:

  - (* Plus *)e1, e2: arith
IHe1: eval (commuter e1) = eval e1
IHe2: eval (commuter e2) = eval e2
eval (commuter e2) + eval (commuter e1) =
eval e1 + eval e2
    rewrite Nat.add_comm.e1, e2: arith
IHe1: eval (commuter e1) = eval e1
IHe2: eval (commuter e2) = eval e2
eval (commuter e1) + eval (commuter e2) =
eval e1 + eval e2
    rewrite IHe1.e1, e2: arith
IHe1: eval (commuter e1) = eval e1
IHe2: eval (commuter e2) = eval e2
eval e1 + eval (commuter e2) = eval e1 + eval e2
    rewrite IHe2.e1, e2: arith
IHe1: eval (commuter e1) = eval e1
IHe2: eval (commuter e2) = eval e2
eval e1 + eval e2 = eval e1 + eval e2
    reflexivity.

A theorem to rewrite a * b:

  - (* Times *)e1, e2: arith
IHe1: eval (commuter e1) = eval e1
IHe2: eval (commuter e2) = eval e2
eval (commuter e2) * eval (commuter e1) =
eval e1 * eval e2
    rewrite Nat.mul_comm.e1, e2: arith
IHe1: eval (commuter e1) = eval e1
IHe2: eval (commuter e2) = eval e2
eval (commuter e1) * eval (commuter e2) =
eval e1 * eval e2
    rewrite IHe1.e1, e2: arith
IHe1: eval (commuter e1) = eval e1
IHe2: eval (commuter e2) = eval e2
eval e1 * eval (commuter e2) = eval e1 * eval e2
    rewrite IHe2.e1, e2: arith
IHe1: eval (commuter e1) = eval e1
IHe2: eval (commuter e2) = eval e2
eval e1 * eval e2 = eval e1 * eval e2
    reflexivity.
Qed.

Here is a more succinct way to write this:

Theorem commuter_correct_shorter : forall e,
    eval (commuter e) = eval e.forall e : arith, eval (commuter e) = eval e
Proof.forall e : arith, eval (commuter e) = eval e
  induction e; simpl.n: nat
n = n
e1, e2: arith
IHe1: eval (commuter e1) = eval e1
IHe2: eval (commuter e2) = eval e2
eval (commuter e2) + eval (commuter e1) =
eval e1 + eval e2
e1, e2: arith
IHe1: eval (commuter e1) = eval e1
IHe2: eval (commuter e2) = eval e2
eval (commuter e2) * eval (commuter e1) =
eval e1 * eval e2
  2: rewrite Nat.add_comm.n: nat
n = n
e1, e2: arith
IHe1: eval (commuter e1) = eval e1
IHe2: eval (commuter e2) = eval e2
eval (commuter e1) + eval (commuter e2) =
eval e1 + eval e2
e1, e2: arith
IHe1: eval (commuter e1) = eval e1
IHe2: eval (commuter e2) = eval e2
eval (commuter e2) * eval (commuter e1) =
eval e1 * eval e2
  3: rewrite Nat.mul_comm.n: nat
n = n
e1, e2: arith
IHe1: eval (commuter e1) = eval e1
IHe2: eval (commuter e2) = eval e2
eval (commuter e1) + eval (commuter e2) =
eval e1 + eval e2
e1, e2: arith
IHe1: eval (commuter e1) = eval e1
IHe2: eval (commuter e2) = eval e2
eval (commuter e1) * eval (commuter e2) =
eval e1 * eval e2
  all: congruence.
Qed.

… and here is a way to automate this the proof that records why each step was taken:

Theorem commuter_correct_snazzy : forall e,
    eval (commuter e) = eval e.forall e : arith, eval (commuter e) = eval e
Proof.forall e : arith, eval (commuter e) = eval e
  induction e; simpl.n: nat
n = n
e1, e2: arith
IHe1: eval (commuter e1) = eval e1
IHe2: eval (commuter e2) = eval e2
eval (commuter e2) + eval (commuter e1) =
eval e1 + eval e2
e1, e2: arith
IHe1: eval (commuter e1) = eval e1
IHe2: eval (commuter e2) = eval e2
eval (commuter e2) * eval (commuter e1) =
eval e1 * eval e2
  all: try match goal with
         | [  |- context[_ + _] ] => rewrite Nat.add_comm
         | [  |- context[_ * _] ] => rewrite Nat.mul_comm
         end.n: nat
n = n
e1, e2: arith
IHe1: eval (commuter e1) = eval e1
IHe2: eval (commuter e2) = eval e2
eval (commuter e1) + eval (commuter e2) =
eval e1 + eval e2
e1, e2: arith
IHe1: eval (commuter e1) = eval e1
IHe2: eval (commuter e2) = eval e2
eval (commuter e1) * eval (commuter e2) =
eval e1 * eval e2
  all: congruence.
Qed.

End ArithWithConstants.

Working with variables

Let's shake things up a bit by adding variables to expressions. Note that all of the automated proof scripts from before will keep working with no changes! That sort of "free" proof evolution is invaluable for theorems about real-world compilers, say.

Module ArithWithVariables.

For readability, we let var refer to strings, using the Notation command, and use it in the definition of the new Var constructor:

Notation var := string.

Inductive arith : Set :=
| Const (n : nat)
| Var (x : var) (* <-- this is the new constructor! *)
| Plus (e1 e2 : arith)
| Times (e1 e2 : arith).

Example ex1 := Const 42.
Example ex2 := Plus (Const 1) (Times (Var "x") (Var "y")).

Adjusting eval to the Var case requires a new argument, vn: val, which maps variable names to values:

Notation val := (var -> nat).

Fixpoint eval (vn: val) (e: arith) : nat :=
  match e with
  | Const n => n
  | Var v => vn v
  | Plus e1 e2 => eval vn e1 + eval vn e2
  | Times e1 e2 => eval vn e1 * eval vn e2
  end.

The simplest valuation returns 0 for every input:

Example val0: val := fun _ => 0.
Compute val0 "x".= 0
: nat
Compute eval val0 ex2.= 1
: nat

… but we can also pass a more complex function:

Compute eval
  (fun v => match v with
            | "x" => 2
            | "y" => 3
            | _ => 0
            end)
  ex2.= 7
: nat

Coq's Compute and Eval commands are not restricted to closed terms; for example, we can evaluate ex1 without passing a valuation, because the valuation is never used:

Compute eval _ ex1.= 42
: nat

When the valuation is needed to produce an answer, we receive a partially reduced term instead (the notation ?vn in the output indicates):

Compute eval _ (Plus (Const 3) (Var "x")).     = S (S (S (?vn "x")))
     : nat
where
?vn : [ |- val]

The functions size, depth, and commuter are similarly easy to adjust, this time with no additional parameters needed:

Fixpoint size (e : arith) : nat :=
  match e with
  | Const _ => 1
  | Var _ => 1
  | Plus e1 e2 => 1 + size e1 + size e2
  | Times e1 e2 => 1 + size e1 + size e2
  end.

Compute size ex1.= 1
: nat
Compute size ex2.= 5
: nat

Fixpoint depth (e : arith) : nat :=
  match e with
  | Const _ => 1
  | Var _ => 1
  | Plus e1 e2 => 1 + max (depth e1) (depth e2)
  | Times e1 e2 => 1 + max (depth e1) (depth e2)
  end.

Compute depth ex1.= 1
: nat
Compute depth ex2.= 3
: nat

Fixpoint commuter (e : arith) : arith :=
  match e with
  | Const _ => e
  | Var _ => e
  | Plus e1 e2 => Plus (commuter e2) (commuter e1)
  | Times e1 e2 => Times (commuter e2) (commuter e1)
  end.

Compute commuter ex1.= Const 42
: arith
Compute commuter ex2.= Plus (Times (Var "y") (Var "x")) (Const 1)
: arith

Due to the automation, the proofs are unchanged:

Theorem depth_le_size : forall e,
    depth e <= size e.forall e : arith, depth e <= size e
Proof.forall e : arith, depth e <= size e
  induction e; simpl; lia.
Qed.

Theorem commuter_correct : forall vn e,
    eval vn (commuter e) = eval vn e.forall (vn : val) (e : arith),
eval vn (commuter e) = eval vn e
Proof.forall (vn : val) (e : arith),
eval vn (commuter e) = eval vn e
  induction e; simpl; lia.
Qed.

Theorem size_commuter : forall e,
    size (commuter e) = size e.forall e : arith, size (commuter e) = size e
Proof.forall e : arith, size (commuter e) = size e
  induction e; simpl; lia.
Qed.

Theorem depth_commuter : forall e,
    depth (commuter e) = depth e.forall e : arith, depth (commuter e) = depth e
Proof.forall e : arith, depth (commuter e) = depth e
  induction e; simpl; lia.
Qed.

Theorem commuter_involutive : forall e,
    commuter (commuter e) = e.forall e : arith, commuter (commuter e) = e
Proof.forall e : arith, commuter (commuter e) = e
  induction e; simpl; congruence.
Qed.

Complex transformations

Variable substitution

Now that we have variables, we can consider new operations, like substituting an expression for a variable.

To define this operation, we use an infix operator == for equality tests on strings. It has a somewhat funny and very expressive type, whose details we will try to gloss over.

Infix "==" := string_dec (at level 70).

Compute "x" == "x".= yes
: {"x" = "x"} + {"x" <> "x"}
Compute "x" == "y".= no
: {"x" = "y"} + {"x" <> "y"}

Fixpoint substitute
  (inThis : arith) (replaceThis : var) (withThis : arith) : arith
  :=
  match inThis with
  | Const _ => inThis
  | Var x => if x == replaceThis then withThis else inThis
  | Plus e1 e2 =>
      Plus (substitute e1 replaceThis withThis)
           (substitute e2 replaceThis withThis)
  | Times e1 e2 =>
      Times (substitute e1 replaceThis withThis)
            (substitute e2 replaceThis withThis)
  end.

An intuitive property about how much substitute might increase depth:

Theorem substitute_depth : forall replaceThis withThis inThis,
    depth (substitute inThis replaceThis withThis) <=
      depth inThis + depth withThis.forall (replaceThis : var) (withThis inThis : arith),
depth (substitute inThis replaceThis withThis) <=
depth inThis + depth withThis
Proof.forall (replaceThis : var) (withThis inThis : arith),
depth (substitute inThis replaceThis withThis) <=
depth inThis + depth withThis
  induction inThis; simpl.replaceThis: var
withThis: arith
n: nat
1 <= S (depth withThis)
replaceThis: var
withThis: arith
x: var
depth (if x == replaceThis then withThis else Var x) <=
S (depth withThis)
replaceThis: var
withThis, inThis1, inThis2: arith
IHinThis1: depth
  (substitute inThis1 replaceThis withThis) <=
depth inThis1 + depth withThis
IHinThis2: depth
  (substitute inThis2 replaceThis withThis) <=
depth inThis2 + depth withThis
S
  (max
     (depth (substitute inThis1 replaceThis withThis))
     (depth (substitute inThis2 replaceThis withThis))) <=
S
  (max (depth inThis1) (depth inThis2) +
   depth withThis)
replaceThis: var
withThis, inThis1, inThis2: arith
IHinThis1: depth
  (substitute inThis1 replaceThis withThis) <=
depth inThis1 + depth withThis
IHinThis2: depth
  (substitute inThis2 replaceThis withThis) <=
depth inThis2 + depth withThis
S
  (max
     (depth (substitute inThis1 replaceThis withThis))
     (depth (substitute inThis2 replaceThis withThis))) <=
S
  (max (depth inThis1) (depth inThis2) +
   depth withThis)

  -replaceThis: var
withThis: arith
n: nat
1 <= S (depth withThis) lia.
  - (* Var *)replaceThis: var
withThis: arith
x: var
depth (if x == replaceThis then withThis else Var x) <=
S (depth withThis)
    destruct (x == replaceThis); simpl.replaceThis: var
withThis: arith
x: var
e: x = replaceThis
depth withThis <= S (depth withThis)
replaceThis: var
withThis: arith
x: var
n: x <> replaceThis
1 <= S (depth withThis)

destruct e: Break the proof into one case for each constructor that might have been used to build the value of expression e. In the special case where e essentially has a Boolean type, we consider whether e is true or false.

    + (* = case *)replaceThis: var
withThis: arith
x: var
e: x = replaceThis
depth withThis <= S (depth withThis)
      lia.

    + (* ≠ case *)replaceThis: var
withThis: arith
x: var
n: x <> replaceThis
1 <= S (depth withThis)
      lia.

  -replaceThis: var
withThis, inThis1, inThis2: arith
IHinThis1: depth
  (substitute inThis1 replaceThis withThis) <=
depth inThis1 + depth withThis
IHinThis2: depth
  (substitute inThis2 replaceThis withThis) <=
depth inThis2 + depth withThis
S
  (max
     (depth (substitute inThis1 replaceThis withThis))
     (depth (substitute inThis2 replaceThis withThis))) <=
S
  (max (depth inThis1) (depth inThis2) +
   depth withThis) lia.
  -replaceThis: var
withThis, inThis1, inThis2: arith
IHinThis1: depth
  (substitute inThis1 replaceThis withThis) <=
depth inThis1 + depth withThis
IHinThis2: depth
  (substitute inThis2 replaceThis withThis) <=
depth inThis2 + depth withThis
S
  (max
     (depth (substitute inThis1 replaceThis withThis))
     (depth (substitute inThis2 replaceThis withThis))) <=
S
  (max (depth inThis1) (depth inThis2) +
   depth withThis) lia.
Qed.

Let's get fancier about automation, using match goal to pattern-match the goal and decide what to do next! The |- syntax separates hypotheses and conclusion in a goal. The context syntax is for matching against any subterm of a term. The construct try is also useful, for attempting a tactic and rolling back the effect if any error is encountered.

Theorem substitute_depth_snazzy : forall replaceThis withThis inThis,
    depth (substitute inThis replaceThis withThis) <=
      depth inThis + depth withThis.forall (replaceThis : var) (withThis inThis : arith),
depth (substitute inThis replaceThis withThis) <=
depth inThis + depth withThis
Proof.forall (replaceThis : var) (withThis inThis : arith),
depth (substitute inThis replaceThis withThis) <=
depth inThis + depth withThis
  induction inThis; simpl;
    try match goal with
      | [ |- context[if ?a == ?b then _ else _] ] =>
          destruct (a == b); simpl
      end; lia.
Qed.

A silly self-substitution has no effect.

Theorem substitute_self : forall replaceThis inThis,
    substitute inThis replaceThis (Var replaceThis) = inThis.forall (replaceThis : var) (inThis : arith),
substitute inThis replaceThis (Var replaceThis) =
inThis
Proof.forall (replaceThis : var) (inThis : arith),
substitute inThis replaceThis (Var replaceThis) =
inThis
  induction inThis; simpl;
    try match goal with
      | [ |- context[if ?a == ?b then _ else _] ] =>
          destruct (a == b); simpl
      end; congruence.
Qed.

We can do substitution and commuting in either order.

Theorem substitute_commuter : forall replaceThis withThis inThis,
    commuter (substitute inThis replaceThis withThis)
    = substitute (commuter inThis) replaceThis (commuter withThis).forall (replaceThis : var) (withThis inThis : arith),
commuter (substitute inThis replaceThis withThis) =
substitute (commuter inThis) replaceThis
  (commuter withThis)
Proof.forall (replaceThis : var) (withThis inThis : arith),
commuter (substitute inThis replaceThis withThis) =
substitute (commuter inThis) replaceThis
  (commuter withThis)
  induction inThis; simpl;
    try match goal with
      | [ |- context[if ?a == ?b then _ else _] ] =>
          destruct (a == b); simpl
      end; congruence.
Qed.

Constant folding

Constant folding is one of the classic compiler optimizations. We repeatedly find opportunities to replace fancier expressions with known constant values.

Fixpoint constantFold (e : arith) : arith :=
  match e with
  | Const _ => e
  | Var _ => e
  | Plus e1 e2 =>
      let e1' := constantFold e1 in
      let e2' := constantFold e2 in
      match e1', e2' with
      | Const n1, Const n2 => Const (n1 + n2)
      | Const 0, _ => e2'
      | _, Const 0 => e1'
      | _, _ => Plus e1' e2'
      end
  | Times e1 e2 =>
      let e1' := constantFold e1 in
      let e2' := constantFold e2 in
      match e1', e2' with
      | Const n1, Const n2 => Const (n1 * n2)
      | Const 1, _ => e2'
      | _, Const 1 => e1'
      | Const 0, _ => Const 0
      | _, Const 0 => Const 0
      | _, _ => Times e1' e2'
      end
  end.

This is supposed to be an optimization, so it had better not increase the size of an expression!

As before, automation makes short work of the proof. A new scripting construct is match patterns with dummy bodies. Such a pattern matches any match in a goal, over any type!

Theorem size_constantFold : forall e,
    size (constantFold e) <= size e.forall e : arith, size (constantFold e) <= size e
Proof.forall e : arith, size (constantFold e) <= size e
  induction e; simpl;
    repeat match goal with
      | [ |- context[match ?E with _ => _ end] ] =>
          destruct E; simpl in *
      end; lia.
Qed.

Looking carefully at the steps taken by the automation, you may be surprised to find that we destruct constantFold e instead of e. One way to understand why is to complete the proof by hand:

Theorem size_constantFold_manual : forall e,
    size (constantFold e) <= size e.forall e : arith, size (constantFold e) <= size e
Proof.forall e : arith, size (constantFold e) <= size e
  induction e; simpl; try lia.e1, e2: arith
IHe1: size (constantFold e1) <= size e1
IHe2: size (constantFold e2) <= size e2
size
  match constantFold e1 with
  | Const (0 as n1) =>
      match constantFold e2 with
      | Const n2 => Const (n1 + n2)
      | _ => constantFold e2
      end
  | Const (S _ as n1) =>
      match constantFold e2 with
      | Const n2 => Const (n1 + n2)
      | _ => Plus (constantFold e1) (constantFold e2)
      end
  | _ =>
      match constantFold e2 with
      | Const 0 => constantFold e1
      | _ => Plus (constantFold e1) (constantFold e2)
      end
  end <= S (size e1 + size e2)
e1, e2: arith
IHe1: size (constantFold e1) <= size e1
IHe2: size (constantFold e2) <= size e2
size
  match constantFold e1 with
  | Const (0 as n1) =>
      match constantFold e2 with
      | Const n2 => Const (n1 * n2)
      | _ => Const 0
      end
  | Const (1 as n1) =>
      match constantFold e2 with
      | Const n2 => Const (n1 * n2)
      | _ => constantFold e2
      end
  | Const (S (S _) as n1) =>
      match constantFold e2 with
      | Const n2 => Const (n1 * n2)
      | _ => Times (constantFold e1) (constantFold e2)
      end
  | _ =>
      match constantFold e2 with
      | Const 0 => Const 0
      | Const 1 => constantFold e1
      | _ => Times (constantFold e1) (constantFold e2)
      end
  end <= S (size e1 + size e2)

  - (* Plus *)e1, e2: arith
IHe1: size (constantFold e1) <= size e1
IHe2: size (constantFold e2) <= size e2
size
  match constantFold e1 with
  | Const (0 as n1) =>
      match constantFold e2 with
      | Const n2 => Const (n1 + n2)
      | _ => constantFold e2
      end
  | Const (S _ as n1) =>
      match constantFold e2 with
      | Const n2 => Const (n1 + n2)
      | _ => Plus (constantFold e1) (constantFold e2)
      end
  | _ =>
      match constantFold e2 with
      | Const 0 => constantFold e1
      | _ => Plus (constantFold e1) (constantFold e2)
      end
  end <= S (size e1 + size e2)

What happens if we try to destruct e1 and e2? The Const and Var cases are simple, but in Plus and Times we make no progress:

    destruct e1, e2; try destruct n; simpl; try lia.e2_1, e2_2: arith
IHe1: size (constantFold (Const 0)) <= size (Const 0)
IHe2: size (constantFold (Plus e2_1 e2_2)) <=
size (Plus e2_1 e2_2)
size
  match
    match constantFold e2_1 with
    | Const (0 as n1) =>
        match constantFold e2_2 with
        | Const n2 => Const (n1 + n2)
        | _ => constantFold e2_2
        end
    | Const (S _ as n1) =>
        match constantFold e2_2 with
        | Const n2 => Const (n1 + n2)
        | _ =>
            Plus (constantFold e2_1)
              (constantFold e2_2)
        end
    | _ =>
        match constantFold e2_2 with
        | Const 0 => constantFold e2_1
        | _ =>
            Plus (constantFold e2_1)
              (constantFold e2_2)
        end
    end
  with
  | Const n2 => Const n2
  | _ =>
      match constantFold e2_1 with
      | Const (0 as n1) =>
          match constantFold e2_2 with
          | Const n2 => Const (n1 + n2)
          | _ => constantFold e2_2
          end
      | Const (S _ as n1) =>
          match constantFold e2_2 with
          | Const n2 => Const (n1 + n2)
          | _ =>
              Plus (constantFold e2_1)
                (constantFold e2_2)
          end
      | _ =>
          match constantFold e2_2 with
          | Const 0 => constantFold e2_1
          | _ =>
              Plus (constantFold e2_1)
                (constantFold e2_2)
          end
      end
  end <= S (S (S (size e2_1 + size e2_2)))

(… dozens of additional goals omitted.)

Abort.

Abort.: Give up on the current proof.

Let's try again.

Theorem size_constantFold_manual : forall e,
    size (constantFold e) <= size e.forall e : arith, size (constantFold e) <= size e
Proof.forall e : arith, size (constantFold e) <= size e
  induction e; simpl; try lia.e1, e2: arith
IHe1: size (constantFold e1) <= size e1
IHe2: size (constantFold e2) <= size e2
size
  match constantFold e1 with
  | Const (0 as n1) =>
      match constantFold e2 with
      | Const n2 => Const (n1 + n2)
      | _ => constantFold e2
      end
  | Const (S _ as n1) =>
      match constantFold e2 with
      | Const n2 => Const (n1 + n2)
      | _ => Plus (constantFold e1) (constantFold e2)
      end
  | _ =>
      match constantFold e2 with
      | Const 0 => constantFold e1
      | _ => Plus (constantFold e1) (constantFold e2)
      end
  end <= S (size e1 + size e2)
e1, e2: arith
IHe1: size (constantFold e1) <= size e1
IHe2: size (constantFold e2) <= size e2
size
  match constantFold e1 with
  | Const (0 as n1) =>
      match constantFold e2 with
      | Const n2 => Const (n1 * n2)
      | _ => Const 0
      end
  | Const (1 as n1) =>
      match constantFold e2 with
      | Const n2 => Const (n1 * n2)
      | _ => constantFold e2
      end
  | Const (S (S _) as n1) =>
      match constantFold e2 with
      | Const n2 => Const (n1 * n2)
      | _ => Times (constantFold e1) (constantFold e2)
      end
  | _ =>
      match constantFold e2 with
      | Const 0 => Const 0
      | Const 1 => constantFold e1
      | _ => Times (constantFold e1) (constantFold e2)
      end
  end <= S (size e1 + size e2)

  - (* Plus *)e1, e2: arith
IHe1: size (constantFold e1) <= size e1
IHe2: size (constantFold e2) <= size e2
size
  match constantFold e1 with
  | Const (0 as n1) =>
      match constantFold e2 with
      | Const n2 => Const (n1 + n2)
      | _ => constantFold e2
      end
  | Const (S _ as n1) =>
      match constantFold e2 with
      | Const n2 => Const (n1 + n2)
      | _ => Plus (constantFold e1) (constantFold e2)
      end
  | _ =>
      match constantFold e2 with
      | Const 0 => constantFold e1
      | _ => Plus (constantFold e1) (constantFold e2)
      end
  end <= S (size e1 + size e2)

The key intuition to complete this proof is that, given the induction hypotheses, it is possible to reason on a homogeneous formula that only mentions e1 and e2 through constantFold.

    transitivity (S (size (constantFold e1)
                     + size (constantFold e2))).e1, e2: arith
IHe1: size (constantFold e1) <= size e1
IHe2: size (constantFold e2) <= size e2
size
  match constantFold e1 with
  | Const (0 as n1) =>
      match constantFold e2 with
      | Const n2 => Const (n1 + n2)
      | _ => constantFold e2
      end
  | Const (S _ as n1) =>
      match constantFold e2 with
      | Const n2 => Const (n1 + n2)
      | _ => Plus (constantFold e1) (constantFold e2)
      end
  | _ =>
      match constantFold e2 with
      | Const 0 => constantFold e1
      | _ => Plus (constantFold e1) (constantFold e2)
      end
  end <=
S (size (constantFold e1) + size (constantFold e2))
e1, e2: arith
IHe1: size (constantFold e1) <= size e1
IHe2: size (constantFold e2) <= size e2
S (size (constantFold e1) + size (constantFold e2)) <=
S (size e1 + size e2)

transitivity X: When proving Y ℛ Z, switch to proving Y ℛ X and X ℛ Z (here ℛ is <=).

The first goal now has no naked e1 and e2. By treating constantFold e1 and constantFold e2 as two arbitrary expressions, we find ourselves reasoning on the body of the function constantFold, without worrying about recursion.

    +e1, e2: arith
IHe1: size (constantFold e1) <= size e1
IHe2: size (constantFold e2) <= size e2
size
  match constantFold e1 with
  | Const (0 as n1) =>
      match constantFold e2 with
      | Const n2 => Const (n1 + n2)
      | _ => constantFold e2
      end
  | Const (S _ as n1) =>
      match constantFold e2 with
      | Const n2 => Const (n1 + n2)
      | _ => Plus (constantFold e1) (constantFold e2)
      end
  | _ =>
      match constantFold e2 with
      | Const 0 => constantFold e1
      | _ => Plus (constantFold e1) (constantFold e2)
      end
  end <=
S (size (constantFold e1) + size (constantFold e2)) destruct (constantFold e1), (constantFold e2).e1, e2: arith
n: nat
IHe1: size (Const n) <= size e1
n0: nat
IHe2: size (Const n0) <= size e2
size match n with
     | 0 | _ => Const (n + n0)
     end <= S (size (Const n) + size (Const n0))
e1, e2: arith
n: nat
IHe1: size (Const n) <= size e1
x: var
IHe2: size (Var x) <= size e2
size
  match n with
  | 0 => Var x
  | S _ => Plus (Const n) (Var x)
  end <= S (size (Const n) + size (Var x))
e1, e2: arith
n: nat
IHe1: size (Const n) <= size e1
a1, a2: arith
IHe2: size (Plus a1 a2) <= size e2
size
  match n with
  | 0 => Plus a1 a2
  | S _ => Plus (Const n) (Plus a1 a2)
  end <= S (size (Const n) + size (Plus a1 a2))
e1, e2: arith
n: nat
IHe1: size (Const n) <= size e1
a1, a2: arith
IHe2: size (Times a1 a2) <= size e2
size
  match n with
  | 0 => Times a1 a2
  | S _ => Plus (Const n) (Times a1 a2)
  end <= S (size (Const n) + size (Times a1 a2))
e1, e2: arith
x: var
IHe1: size (Var x) <= size e1
n: nat
IHe2: size (Const n) <= size e2
size
  match n with
  | 0 => Var x
  | S _ => Plus (Var x) (Const n)
  end <= S (size (Var x) + size (Const n))
e1, e2: arith
x: var
IHe1: size (Var x) <= size e1
x0: var
IHe2: size (Var x0) <= size e2
size (Plus (Var x) (Var x0)) <=
S (size (Var x) + size (Var x0))
e1, e2: arith
x: var
IHe1: size (Var x) <= size e1
a1, a2: arith
IHe2: size (Plus a1 a2) <= size e2
size (Plus (Var x) (Plus a1 a2)) <=
S (size (Var x) + size (Plus a1 a2))
e1, e2: arith
x: var
IHe1: size (Var x) <= size e1
a1, a2: arith
IHe2: size (Times a1 a2) <= size e2
size (Plus (Var x) (Times a1 a2)) <=
S (size (Var x) + size (Times a1 a2))
e1, e2, a1, a2: arith
IHe1: size (Plus a1 a2) <= size e1
n: nat
IHe2: size (Const n) <= size e2
size
  match n with
  | 0 => Plus a1 a2
  | S _ => Plus (Plus a1 a2) (Const n)
  end <= S (size (Plus a1 a2) + size (Const n))
e1, e2, a1, a2: arith
IHe1: size (Plus a1 a2) <= size e1
x: var
IHe2: size (Var x) <= size e2
size (Plus (Plus a1 a2) (Var x)) <=
S (size (Plus a1 a2) + size (Var x))
e1, e2, a1, a2: arith
IHe1: size (Plus a1 a2) <= size e1
a3, a4: arith
IHe2: size (Plus a3 a4) <= size e2
size (Plus (Plus a1 a2) (Plus a3 a4)) <=
S (size (Plus a1 a2) + size (Plus a3 a4))
e1, e2, a1, a2: arith
IHe1: size (Plus a1 a2) <= size e1
a3, a4: arith
IHe2: size (Times a3 a4) <= size e2
size (Plus (Plus a1 a2) (Times a3 a4)) <=
S (size (Plus a1 a2) + size (Times a3 a4))
e1, e2, a1, a2: arith
IHe1: size (Times a1 a2) <= size e1
n: nat
IHe2: size (Const n) <= size e2
size
  match n with
  | 0 => Times a1 a2
  | S _ => Plus (Times a1 a2) (Const n)
  end <= S (size (Times a1 a2) + size (Const n))
e1, e2, a1, a2: arith
IHe1: size (Times a1 a2) <= size e1
x: var
IHe2: size (Var x) <= size e2
size (Plus (Times a1 a2) (Var x)) <=
S (size (Times a1 a2) + size (Var x))
e1, e2, a1, a2: arith
IHe1: size (Times a1 a2) <= size e1
a3, a4: arith
IHe2: size (Plus a3 a4) <= size e2
size (Plus (Times a1 a2) (Plus a3 a4)) <=
S (size (Times a1 a2) + size (Plus a3 a4))
e1, e2, a1, a2: arith
IHe1: size (Times a1 a2) <= size e1
a3, a4: arith
IHe2: size (Times a3 a4) <= size e2
size (Plus (Times a1 a2) (Times a3 a4)) <=
S (size (Times a1 a2) + size (Times a3 a4))
      all: try destruct n; simpl.e1, e2: arith
IHe1: size (Const 0) <= size e1
n0: nat
IHe2: size (Const n0) <= size e2
1 <= 3
e1, e2: arith
n: nat
IHe1: size (Const (S n)) <= size e1
n0: nat
IHe2: size (Const n0) <= size e2
1 <= 3
e1, e2: arith
IHe1: size (Const 0) <= size e1
x: var
IHe2: size (Var x) <= size e2
1 <= 3
e1, e2: arith
n: nat
IHe1: size (Const (S n)) <= size e1
x: var
IHe2: size (Var x) <= size e2
3 <= 3
e1, e2: arith
IHe1: size (Const 0) <= size e1
a1, a2: arith
IHe2: size (Plus a1 a2) <= size e2
S (size a1 + size a2) <= S (S (S (size a1 + size a2)))
e1, e2: arith
n: nat
IHe1: size (Const (S n)) <= size e1
a1, a2: arith
IHe2: size (Plus a1 a2) <= size e2
S (S (S (size a1 + size a2))) <=
S (S (S (size a1 + size a2)))
e1, e2: arith
IHe1: size (Const 0) <= size e1
a1, a2: arith
IHe2: size (Times a1 a2) <= size e2
S (size a1 + size a2) <= S (S (S (size a1 + size a2)))
e1, e2: arith
n: nat
IHe1: size (Const (S n)) <= size e1
a1, a2: arith
IHe2: size (Times a1 a2) <= size e2
S (S (S (size a1 + size a2))) <=
S (S (S (size a1 + size a2)))
e1, e2: arith
x: var
IHe1: size (Var x) <= size e1
IHe2: size (Const 0) <= size e2
1 <= 3
e1, e2: arith
x: var
IHe1: size (Var x) <= size e1
n: nat
IHe2: size (Const (S n)) <= size e2
3 <= 3
e1, e2: arith
x: var
IHe1: size (Var x) <= size e1
x0: var
IHe2: size (Var x0) <= size e2
3 <= 3
e1, e2: arith
x: var
IHe1: size (Var x) <= size e1
a1, a2: arith
IHe2: size (Plus a1 a2) <= size e2
S (S (S (size a1 + size a2))) <=
S (S (S (size a1 + size a2)))
e1, e2: arith
x: var
IHe1: size (Var x) <= size e1
a1, a2: arith
IHe2: size (Times a1 a2) <= size e2
S (S (S (size a1 + size a2))) <=
S (S (S (size a1 + size a2)))
e1, e2, a1, a2: arith
IHe1: size (Plus a1 a2) <= size e1
IHe2: size (Const 0) <= size e2
S (size a1 + size a2) <= S (S (size a1 + size a2 + 1))
e1, e2, a1, a2: arith
IHe1: size (Plus a1 a2) <= size e1
n: nat
IHe2: size (Const (S n)) <= size e2
S (S (size a1 + size a2 + 1)) <=
S (S (size a1 + size a2 + 1))
e1, e2, a1, a2: arith
IHe1: size (Plus a1 a2) <= size e1
x: var
IHe2: size (Var x) <= size e2
S (S (size a1 + size a2 + 1)) <=
S (S (size a1 + size a2 + 1))
e1, e2, a1, a2: arith
IHe1: size (Plus a1 a2) <= size e1
a3, a4: arith
IHe2: size (Plus a3 a4) <= size e2
S (S (size a1 + size a2 + S (size a3 + size a4))) <=
S (S (size a1 + size a2 + S (size a3 + size a4)))
e1, e2, a1, a2: arith
IHe1: size (Plus a1 a2) <= size e1
a3, a4: arith
IHe2: size (Times a3 a4) <= size e2
S (S (size a1 + size a2 + S (size a3 + size a4))) <=
S (S (size a1 + size a2 + S (size a3 + size a4)))
e1, e2, a1, a2: arith
IHe1: size (Times a1 a2) <= size e1
IHe2: size (Const 0) <= size e2
S (size a1 + size a2) <= S (S (size a1 + size a2 + 1))
e1, e2, a1, a2: arith
IHe1: size (Times a1 a2) <= size e1
n: nat
IHe2: size (Const (S n)) <= size e2
S (S (size a1 + size a2 + 1)) <=
S (S (size a1 + size a2 + 1))
e1, e2, a1, a2: arith
IHe1: size (Times a1 a2) <= size e1
x: var
IHe2: size (Var x) <= size e2
S (S (size a1 + size a2 + 1)) <=
S (S (size a1 + size a2 + 1))
e1, e2, a1, a2: arith
IHe1: size (Times a1 a2) <= size e1
a3, a4: arith
IHe2: size (Plus a3 a4) <= size e2
S (S (size a1 + size a2 + S (size a3 + size a4))) <=
S (S (size a1 + size a2 + S (size a3 + size a4)))
e1, e2, a1, a2: arith
IHe1: size (Times a1 a2) <= size e1
a3, a4: arith
IHe2: size (Times a3 a4) <= size e2
S (S (size a1 + size a2 + S (size a3 + size a4))) <=
S (S (size a1 + size a2 + S (size a3 + size a4)))
      all: lia.
    +e1, e2: arith
IHe1: size (constantFold e1) <= size e1
IHe2: size (constantFold e2) <= size e2
S (size (constantFold e1) + size (constantFold e2)) <=
S (size e1 + size e2) lia.

  -e1, e2: arith
IHe1: size (constantFold e1) <= size e1
IHe2: size (constantFold e2) <= size e2
size
  match constantFold e1 with
  | Const (0 as n1) =>
      match constantFold e2 with
      | Const n2 => Const (n1 * n2)
      | _ => Const 0
      end
  | Const (1 as n1) =>
      match constantFold e2 with
      | Const n2 => Const (n1 * n2)
      | _ => constantFold e2
      end
  | Const (S (S _) as n1) =>
      match constantFold e2 with
      | Const n2 => Const (n1 * n2)
      | _ => Times (constantFold e1) (constantFold e2)
      end
  | _ =>
      match constantFold e2 with
      | Const 0 => Const 0
      | Const 1 => constantFold e1
      | _ => Times (constantFold e1) (constantFold e2)
      end
  end <= S (size e1 + size e2) transitivity (S (size (constantFold e1) + size (constantFold e2))).e1, e2: arith
IHe1: size (constantFold e1) <= size e1
IHe2: size (constantFold e2) <= size e2
size
  match constantFold e1 with
  | Const (0 as n1) =>
      match constantFold e2 with
      | Const n2 => Const (n1 * n2)
      | _ => Const 0
      end
  | Const (1 as n1) =>
      match constantFold e2 with
      | Const n2 => Const (n1 * n2)
      | _ => constantFold e2
      end
  | Const (S (S _) as n1) =>
      match constantFold e2 with
      | Const n2 => Const (n1 * n2)
      | _ => Times (constantFold e1) (constantFold e2)
      end
  | _ =>
      match constantFold e2 with
      | Const 0 => Const 0
      | Const 1 => constantFold e1
      | _ => Times (constantFold e1) (constantFold e2)
      end
  end <=
S (size (constantFold e1) + size (constantFold e2))
e1, e2: arith
IHe1: size (constantFold e1) <= size e1
IHe2: size (constantFold e2) <= size e2
S (size (constantFold e1) + size (constantFold e2)) <=
S (size e1 + size e2)
    +e1, e2: arith
IHe1: size (constantFold e1) <= size e1
IHe2: size (constantFold e2) <= size e2
size
  match constantFold e1 with
  | Const (0 as n1) =>
      match constantFold e2 with
      | Const n2 => Const (n1 * n2)
      | _ => Const 0
      end
  | Const (1 as n1) =>
      match constantFold e2 with
      | Const n2 => Const (n1 * n2)
      | _ => constantFold e2
      end
  | Const (S (S _) as n1) =>
      match constantFold e2 with
      | Const n2 => Const (n1 * n2)
      | _ => Times (constantFold e1) (constantFold e2)
      end
  | _ =>
      match constantFold e2 with
      | Const 0 => Const 0
      | Const 1 => constantFold e1
      | _ => Times (constantFold e1) (constantFold e2)
      end
  end <=
S (size (constantFold e1) + size (constantFold e2)) destruct (constantFold e1), (constantFold e2).e1, e2: arith
n: nat
IHe1: size (Const n) <= size e1
n0: nat
IHe2: size (Const n0) <= size e2
size match n with
     | 0 | _ => Const (n * n0)
     end <= S (size (Const n) + size (Const n0))
e1, e2: arith
n: nat
IHe1: size (Const n) <= size e1
x: var
IHe2: size (Var x) <= size e2
size
  match n with
  | 0 => Const 0
  | 1 => Var x
  | S (S _) => Times (Const n) (Var x)
  end <= S (size (Const n) + size (Var x))
e1, e2: arith
n: nat
IHe1: size (Const n) <= size e1
a1, a2: arith
IHe2: size (Plus a1 a2) <= size e2
size
  match n with
  | 0 => Const 0
  | 1 => Plus a1 a2
  | S (S _) => Times (Const n) (Plus a1 a2)
  end <= S (size (Const n) + size (Plus a1 a2))
e1, e2: arith
n: nat
IHe1: size (Const n) <= size e1
a1, a2: arith
IHe2: size (Times a1 a2) <= size e2
size
  match n with
  | 0 => Const 0
  | 1 => Times a1 a2
  | S (S _) => Times (Const n) (Times a1 a2)
  end <= S (size (Const n) + size (Times a1 a2))
e1, e2: arith
x: var
IHe1: size (Var x) <= size e1
n: nat
IHe2: size (Const n) <= size e2
size
  match n with
  | 0 => Const 0
  | 1 => Var x
  | S (S _) => Times (Var x) (Const n)
  end <= S (size (Var x) + size (Const n))
e1, e2: arith
x: var
IHe1: size (Var x) <= size e1
x0: var
IHe2: size (Var x0) <= size e2
size (Times (Var x) (Var x0)) <=
S (size (Var x) + size (Var x0))
e1, e2: arith
x: var
IHe1: size (Var x) <= size e1
a1, a2: arith
IHe2: size (Plus a1 a2) <= size e2
size (Times (Var x) (Plus a1 a2)) <=
S (size (Var x) + size (Plus a1 a2))
e1, e2: arith
x: var
IHe1: size (Var x) <= size e1
a1, a2: arith
IHe2: size (Times a1 a2) <= size e2
size (Times (Var x) (Times a1 a2)) <=
S (size (Var x) + size (Times a1 a2))
e1, e2, a1, a2: arith
IHe1: size (Plus a1 a2) <= size e1
n: nat
IHe2: size (Const n) <= size e2
size
  match n with
  | 0 => Const 0
  | 1 => Plus a1 a2
  | S (S _) => Times (Plus a1 a2) (Const n)
  end <= S (size (Plus a1 a2) + size (Const n))
e1, e2, a1, a2: arith
IHe1: size (Plus a1 a2) <= size e1
x: var
IHe2: size (Var x) <= size e2
size (Times (Plus a1 a2) (Var x)) <=
S (size (Plus a1 a2) + size (Var x))
e1, e2, a1, a2: arith
IHe1: size (Plus a1 a2) <= size e1
a3, a4: arith
IHe2: size (Plus a3 a4) <= size e2
size (Times (Plus a1 a2) (Plus a3 a4)) <=
S (size (Plus a1 a2) + size (Plus a3 a4))
e1, e2, a1, a2: arith
IHe1: size (Plus a1 a2) <= size e1
a3, a4: arith
IHe2: size (Times a3 a4) <= size e2
size (Times (Plus a1 a2) (Times a3 a4)) <=
S (size (Plus a1 a2) + size (Times a3 a4))
e1, e2, a1, a2: arith
IHe1: size (Times a1 a2) <= size e1
n: nat
IHe2: size (Const n) <= size e2
size
  match n with
  | 0 => Const 0
  | 1 => Times a1 a2
  | S (S _) => Times (Times a1 a2) (Const n)
  end <= S (size (Times a1 a2) + size (Const n))
e1, e2, a1, a2: arith
IHe1: size (Times a1 a2) <= size e1
x: var
IHe2: size (Var x) <= size e2
size (Times (Times a1 a2) (Var x)) <=
S (size (Times a1 a2) + size (Var x))
e1, e2, a1, a2: arith
IHe1: size (Times a1 a2) <= size e1
a3, a4: arith
IHe2: size (Plus a3 a4) <= size e2
size (Times (Times a1 a2) (Plus a3 a4)) <=
S (size (Times a1 a2) + size (Plus a3 a4))
e1, e2, a1, a2: arith
IHe1: size (Times a1 a2) <= size e1
a3, a4: arith
IHe2: size (Times a3 a4) <= size e2
size (Times (Times a1 a2) (Times a3 a4)) <=
S (size (Times a1 a2) + size (Times a3 a4))
      all: try destruct n; simpl.e1, e2: arith
IHe1: size (Const 0) <= size e1
n0: nat
IHe2: size (Const n0) <= size e2
1 <= 3
e1, e2: arith
n: nat
IHe1: size (Const (S n)) <= size e1
n0: nat
IHe2: size (Const n0) <= size e2
size match n with
     | 0 | _ => Const (n0 + n * n0)
     end <= 3
e1, e2: arith
IHe1: size (Const 0) <= size e1
x: var
IHe2: size (Var x) <= size e2
1 <= 3
e1, e2: arith
n: nat
IHe1: size (Const (S n)) <= size e1
x: var
IHe2: size (Var x) <= size e2
size
  match n with
  | 0 => Var x
  | S _ => Times (Const (S n)) (Var x)
  end <= 3
e1, e2: arith
IHe1: size (Const 0) <= size e1
a1, a2: arith
IHe2: size (Plus a1 a2) <= size e2
1 <= S (S (S (size a1 + size a2)))
e1, e2: arith
n: nat
IHe1: size (Const (S n)) <= size e1
a1, a2: arith
IHe2: size (Plus a1 a2) <= size e2
size
  match n with
  | 0 => Plus a1 a2
  | S _ => Times (Const (S n)) (Plus a1 a2)
  end <= S (S (S (size a1 + size a2)))
e1, e2: arith
IHe1: size (Const 0) <= size e1
a1, a2: arith
IHe2: size (Times a1 a2) <= size e2
1 <= S (S (S (size a1 + size a2)))
e1, e2: arith
n: nat
IHe1: size (Const (S n)) <= size e1
a1, a2: arith
IHe2: size (Times a1 a2) <= size e2
size
  match n with
  | 0 => Times a1 a2
  | S _ => Times (Const (S n)) (Times a1 a2)
  end <= S (S (S (size a1 + size a2)))
e1, e2: arith
x: var
IHe1: size (Var x) <= size e1
IHe2: size (Const 0) <= size e2
1 <= 3
e1, e2: arith
x: var
IHe1: size (Var x) <= size e1
n: nat
IHe2: size (Const (S n)) <= size e2
size
  match n with
  | 0 => Var x
  | S _ => Times (Var x) (Const (S n))
  end <= 3
e1, e2: arith
x: var
IHe1: size (Var x) <= size e1
x0: var
IHe2: size (Var x0) <= size e2
3 <= 3
e1, e2: arith
x: var
IHe1: size (Var x) <= size e1
a1, a2: arith
IHe2: size (Plus a1 a2) <= size e2
S (S (S (size a1 + size a2))) <=
S (S (S (size a1 + size a2)))
e1, e2: arith
x: var
IHe1: size (Var x) <= size e1
a1, a2: arith
IHe2: size (Times a1 a2) <= size e2
S (S (S (size a1 + size a2))) <=
S (S (S (size a1 + size a2)))
e1, e2, a1, a2: arith
IHe1: size (Plus a1 a2) <= size e1
IHe2: size (Const 0) <= size e2
1 <= S (S (size a1 + size a2 + 1))
e1, e2, a1, a2: arith
IHe1: size (Plus a1 a2) <= size e1
n: nat
IHe2: size (Const (S n)) <= size e2
size
  match n with
  | 0 => Plus a1 a2
  | S _ => Times (Plus a1 a2) (Const (S n))
  end <= S (S (size a1 + size a2 + 1))
e1, e2, a1, a2: arith
IHe1: size (Plus a1 a2) <= size e1
x: var
IHe2: size (Var x) <= size e2
S (S (size a1 + size a2 + 1)) <=
S (S (size a1 + size a2 + 1))
e1, e2, a1, a2: arith
IHe1: size (Plus a1 a2) <= size e1
a3, a4: arith
IHe2: size (Plus a3 a4) <= size e2
S (S (size a1 + size a2 + S (size a3 + size a4))) <=
S (S (size a1 + size a2 + S (size a3 + size a4)))
e1, e2, a1, a2: arith
IHe1: size (Plus a1 a2) <= size e1
a3, a4: arith
IHe2: size (Times a3 a4) <= size e2
S (S (size a1 + size a2 + S (size a3 + size a4))) <=
S (S (size a1 + size a2 + S (size a3 + size a4)))
e1, e2, a1, a2: arith
IHe1: size (Times a1 a2) <= size e1
IHe2: size (Const 0) <= size e2
1 <= S (S (size a1 + size a2 + 1))
e1, e2, a1, a2: arith
IHe1: size (Times a1 a2) <= size e1
n: nat
IHe2: size (Const (S n)) <= size e2
size
  match n with
  | 0 => Times a1 a2
  | S _ => Times (Times a1 a2) (Const (S n))
  end <= S (S (size a1 + size a2 + 1))
e1, e2, a1, a2: arith
IHe1: size (Times a1 a2) <= size e1
x: var
IHe2: size (Var x) <= size e2
S (S (size a1 + size a2 + 1)) <=
S (S (size a1 + size a2 + 1))
e1, e2, a1, a2: arith
IHe1: size (Times a1 a2) <= size e1
a3, a4: arith
IHe2: size (Plus a3 a4) <= size e2
S (S (size a1 + size a2 + S (size a3 + size a4))) <=
S (S (size a1 + size a2 + S (size a3 + size a4)))
e1, e2, a1, a2: arith
IHe1: size (Times a1 a2) <= size e1
a3, a4: arith
IHe2: size (Times a3 a4) <= size e2
S (S (size a1 + size a2 + S (size a3 + size a4))) <=
S (S (size a1 + size a2 + S (size a3 + size a4)))
      all: try destruct n; simpl.e1, e2: arith
IHe1: size (Const 0) <= size e1
n0: nat
IHe2: size (Const n0) <= size e2
1 <= 3
e1, e2: arith
IHe1: size (Const 1) <= size e1
n0: nat
IHe2: size (Const n0) <= size e2
1 <= 3
e1, e2: arith
n: nat
IHe1: size (Const (S (S n))) <= size e1
n0: nat
IHe2: size (Const n0) <= size e2
1 <= 3
e1, e2: arith
IHe1: size (Const 0) <= size e1
x: var
IHe2: size (Var x) <= size e2
1 <= 3
e1, e2: arith
IHe1: size (Const 1) <= size e1
x: var
IHe2: size (Var x) <= size e2
1 <= 3
e1, e2: arith
n: nat
IHe1: size (Const (S (S n))) <= size e1
x: var
IHe2: size (Var x) <= size e2
3 <= 3
e1, e2: arith
IHe1: size (Const 0) <= size e1
a1, a2: arith
IHe2: size (Plus a1 a2) <= size e2
1 <= S (S (S (size a1 + size a2)))
e1, e2: arith
IHe1: size (Const 1) <= size e1
a1, a2: arith
IHe2: size (Plus a1 a2) <= size e2
S (size a1 + size a2) <= S (S (S (size a1 + size a2)))
e1, e2: arith
n: nat
IHe1: size (Const (S (S n))) <= size e1
a1, a2: arith
IHe2: size (Plus a1 a2) <= size e2
S (S (S (size a1 + size a2))) <=
S (S (S (size a1 + size a2)))
e1, e2: arith
IHe1: size (Const 0) <= size e1
a1, a2: arith
IHe2: size (Times a1 a2) <= size e2
1 <= S (S (S (size a1 + size a2)))
e1, e2: arith
IHe1: size (Const 1) <= size e1
a1, a2: arith
IHe2: size (Times a1 a2) <= size e2
S (size a1 + size a2) <= S (S (S (size a1 + size a2)))
e1, e2: arith
n: nat
IHe1: size (Const (S (S n))) <= size e1
a1, a2: arith
IHe2: size (Times a1 a2) <= size e2
S (S (S (size a1 + size a2))) <=
S (S (S (size a1 + size a2)))
e1, e2: arith
x: var
IHe1: size (Var x) <= size e1
IHe2: size (Const 0) <= size e2
1 <= 3
e1, e2: arith
x: var
IHe1: size (Var x) <= size e1
IHe2: size (Const 1) <= size e2
1 <= 3
e1, e2: arith
x: var
IHe1: size (Var x) <= size e1
n: nat
IHe2: size (Const (S (S n))) <= size e2
3 <= 3
e1, e2: arith
x: var
IHe1: size (Var x) <= size e1
x0: var
IHe2: size (Var x0) <= size e2
3 <= 3
e1, e2: arith
x: var
IHe1: size (Var x) <= size e1
a1, a2: arith
IHe2: size (Plus a1 a2) <= size e2
S (S (S (size a1 + size a2))) <=
S (S (S (size a1 + size a2)))
e1, e2: arith
x: var
IHe1: size (Var x) <= size e1
a1, a2: arith
IHe2: size (Times a1 a2) <= size e2
S (S (S (size a1 + size a2))) <=
S (S (S (size a1 + size a2)))
e1, e2, a1, a2: arith
IHe1: size (Plus a1 a2) <= size e1
IHe2: size (Const 0) <= size e2
1 <= S (S (size a1 + size a2 + 1))
e1, e2, a1, a2: arith
IHe1: size (Plus a1 a2) <= size e1
IHe2: size (Const 1) <= size e2
S (size a1 + size a2) <= S (S (size a1 + size a2 + 1))
e1, e2, a1, a2: arith
IHe1: size (Plus a1 a2) <= size e1
n: nat
IHe2: size (Const (S (S n))) <= size e2
S (S (size a1 + size a2 + 1)) <=
S (S (size a1 + size a2 + 1))
e1, e2, a1, a2: arith
IHe1: size (Plus a1 a2) <= size e1
x: var
IHe2: size (Var x) <= size e2
S (S (size a1 + size a2 + 1)) <=
S (S (size a1 + size a2 + 1))
e1, e2, a1, a2: arith
IHe1: size (Plus a1 a2) <= size e1
a3, a4: arith
IHe2: size (Plus a3 a4) <= size e2
S (S (size a1 + size a2 + S (size a3 + size a4))) <=
S (S (size a1 + size a2 + S (size a3 + size a4)))
e1, e2, a1, a2: arith
IHe1: size (Plus a1 a2) <= size e1
a3, a4: arith
IHe2: size (Times a3 a4) <= size e2
S (S (size a1 + size a2 + S (size a3 + size a4))) <=
S (S (size a1 + size a2 + S (size a3 + size a4)))
e1, e2, a1, a2: arith
IHe1: size (Times a1 a2) <= size e1
IHe2: size (Const 0) <= size e2
1 <= S (S (size a1 + size a2 + 1))
e1, e2, a1, a2: arith
IHe1: size (Times a1 a2) <= size e1
IHe2: size (Const 1) <= size e2
S (size a1 + size a2) <= S (S (size a1 + size a2 + 1))
e1, e2, a1, a2: arith
IHe1: size (Times a1 a2) <= size e1
n: nat
IHe2: size (Const (S (S n))) <= size e2
S (S (size a1 + size a2 + 1)) <=
S (S (size a1 + size a2 + 1))
e1, e2, a1, a2: arith
IHe1: size (Times a1 a2) <= size e1
x: var
IHe2: size (Var x) <= size e2
S (S (size a1 + size a2 + 1)) <=
S (S (size a1 + size a2 + 1))
e1, e2, a1, a2: arith
IHe1: size (Times a1 a2) <= size e1
a3, a4: arith
IHe2: size (Plus a3 a4) <= size e2
S (S (size a1 + size a2 + S (size a3 + size a4))) <=
S (S (size a1 + size a2 + S (size a3 + size a4)))
e1, e2, a1, a2: arith
IHe1: size (Times a1 a2) <= size e1
a3, a4: arith
IHe2: size (Times a3 a4) <= size e2
S (S (size a1 + size a2 + S (size a3 + size a4))) <=
S (S (size a1 + size a2 + S (size a3 + size a4)))
      all: lia.
    +e1, e2: arith
IHe1: size (constantFold e1) <= size e1
IHe2: size (constantFold e2) <= size e2
S (size (constantFold e1) + size (constantFold e2)) <=
S (size e1 + size e2) lia.
Qed.

The same principle applies for eval:

Theorem eval_constantFold : forall (vn: val) (e: arith),
    eval vn (constantFold e) = eval vn e.forall (vn : val) (e : arith),
eval vn (constantFold e) = eval vn e
Proof.forall (vn : val) (e : arith),
eval vn (constantFold e) = eval vn e
  induction e; simpl;
    repeat match goal with
      | [ |- context[match ?E with _ => _ end] ] =>
          destruct E; simpl in *
      end; lia.
Qed.

And it's business as usual for commuter, with just two simple added cases:

Theorem commuter_constantFold : forall e,
    commuter (constantFold e) = constantFold (commuter e).forall e : arith,
commuter (constantFold e) = constantFold (commuter e)
Proof.forall e : arith,
commuter (constantFold e) = constantFold (commuter e)
  induction e; simpl;
    repeat match goal with
      | [ |- context[match ?E with _ => _ end] ] =>
          destruct E; simpl in *
      | [ H : ?f _ = ?f _ |- _ ] =>
          injection H as H; subst
      | [ |- ?f _ = ?f _ ] =>
          f_equal
      end; try (lia || congruence).

injection H as H

Replace a hypothesis H of the form f x = f y with x = y, when f is a constructor of an inductive type.

f_equal

Replace a goal of the form f x = f y with x = y, for any function f.

Qed.

Exercise: Eliminating automation

Rewrite the proof above step by step, using no repeat automation.

Theorem eval_constantFold_manual : forall (vn: val) (e: arith),
    eval vn (constantFold e) = eval vn e.forall (vn : val) (e : arith),
eval vn (constantFold e) = eval vn e

Solution

Proof.forall (vn : val) (e : arith),
eval vn (constantFold e) = eval vn e
  induction e; simpl.vn: val
n: nat
n = n
vn: val
x: var
vn x = vn x
vn: val
e1, e2: arith
IHe1: eval vn (constantFold e1) = eval vn e1
IHe2: eval vn (constantFold e2) = eval vn e2
eval vn
  match constantFold e1 with
  | Const (0 as n1) =>
      match constantFold e2 with
      | Const n2 => Const (n1 + n2)
      | _ => constantFold e2
      end
  | Const (S _ as n1) =>
      match constantFold e2 with
      | Const n2 => Const (n1 + n2)
      | _ => Plus (constantFold e1) (constantFold e2)
      end
  | _ =>
      match constantFold e2 with
      | Const 0 => constantFold e1
      | _ => Plus (constantFold e1) (constantFold e2)
      end
  end = eval vn e1 + eval vn e2
vn: val
e1, e2: arith
IHe1: eval vn (constantFold e1) = eval vn e1
IHe2: eval vn (constantFold e2) = eval vn e2
eval vn
  match constantFold e1 with
  | Const (0 as n1) =>
      match constantFold e2 with
      | Const n2 => Const (n1 * n2)
      | _ => Const 0
      end
  | Const (1 as n1) =>
      match constantFold e2 with
      | Const n2 => Const (n1 * n2)
      | _ => constantFold e2
      end
  | Const (S (S _) as n1) =>
      match constantFold e2 with
      | Const n2 => Const (n1 * n2)
      | _ => Times (constantFold e1) (constantFold e2)
      end
  | _ =>
      match constantFold e2 with
      | Const 0 => Const 0
      | Const 1 => constantFold e1
      | _ => Times (constantFold e1) (constantFold e2)
      end
  end = eval vn e1 * eval vn e2
  -vn: val
n: nat
n = n congruence.
  -vn: val
x: var
vn x = vn x congruence.
  -vn: val
e1, e2: arith
IHe1: eval vn (constantFold e1) = eval vn e1
IHe2: eval vn (constantFold e2) = eval vn e2
eval vn
  match constantFold e1 with
  | Const (0 as n1) =>
      match constantFold e2 with
      | Const n2 => Const (n1 + n2)
      | _ => constantFold e2
      end
  | Const (S _ as n1) =>
      match constantFold e2 with
      | Const n2 => Const (n1 + n2)
      | _ => Plus (constantFold e1) (constantFold e2)
      end
  | _ =>
      match constantFold e2 with
      | Const 0 => constantFold e1
      | _ => Plus (constantFold e1) (constantFold e2)
      end
  end = eval vn e1 + eval vn e2 rewrite <- IHe1, <- IHe2.vn: val
e1, e2: arith
IHe1: eval vn (constantFold e1) = eval vn e1
IHe2: eval vn (constantFold e2) = eval vn e2
eval vn
  match constantFold e1 with
  | Const (0 as n1) =>
      match constantFold e2 with
      | Const n2 => Const (n1 + n2)
      | _ => constantFold e2
      end
  | Const (S _ as n1) =>
      match constantFold e2 with
      | Const n2 => Const (n1 + n2)
      | _ => Plus (constantFold e1) (constantFold e2)
      end
  | _ =>
      match constantFold e2 with
      | Const 0 => constantFold e1
      | _ => Plus (constantFold e1) (constantFold e2)
      end
  end =
eval vn (constantFold e1) + eval vn (constantFold e2)
    destruct (constantFold e1), (constantFold e2).vn: val
e1, e2: arith
n: nat
IHe1: eval vn (Const n) = eval vn e1
n0: nat
IHe2: eval vn (Const n0) = eval vn e2
eval vn match n with
        | 0 | _ => Const (n + n0)
        end = eval vn (Const n) + eval vn (Const n0)
vn: val
e1, e2: arith
n: nat
IHe1: eval vn (Const n) = eval vn e1
x: var
IHe2: eval vn (Var x) = eval vn e2
eval vn
  match n with
  | 0 => Var x
  | S _ => Plus (Const n) (Var x)
  end = eval vn (Const n) + eval vn (Var x)
vn: val
e1, e2: arith
n: nat
IHe1: eval vn (Const n) = eval vn e1
a1, a2: arith
IHe2: eval vn (Plus a1 a2) = eval vn e2
eval vn
  match n with
  | 0 => Plus a1 a2
  | S _ => Plus (Const n) (Plus a1 a2)
  end = eval vn (Const n) + eval vn (Plus a1 a2)
vn: val
e1, e2: arith
n: nat
IHe1: eval vn (Const n) = eval vn e1
a1, a2: arith
IHe2: eval vn (Times a1 a2) = eval vn e2
eval vn
  match n with
  | 0 => Times a1 a2
  | S _ => Plus (Const n) (Times a1 a2)
  end = eval vn (Const n) + eval vn (Times a1 a2)
vn: val
e1, e2: arith
x: var
IHe1: eval vn (Var x) = eval vn e1
n: nat
IHe2: eval vn (Const n) = eval vn e2
eval vn
  match n with
  | 0 => Var x
  | S _ => Plus (Var x) (Const n)
  end = eval vn (Var x) + eval vn (Const n)
vn: val
e1, e2: arith
x: var
IHe1: eval vn (Var x) = eval vn e1
x0: var
IHe2: eval vn (Var x0) = eval vn e2
eval vn (Plus (Var x) (Var x0)) =
eval vn (Var x) + eval vn (Var x0)
vn: val
e1, e2: arith
x: var
IHe1: eval vn (Var x) = eval vn e1
a1, a2: arith
IHe2: eval vn (Plus a1 a2) = eval vn e2
eval vn (Plus (Var x) (Plus a1 a2)) =
eval vn (Var x) + eval vn (Plus a1 a2)
vn: val
e1, e2: arith
x: var
IHe1: eval vn (Var x) = eval vn e1
a1, a2: arith
IHe2: eval vn (Times a1 a2) = eval vn e2
eval vn (Plus (Var x) (Times a1 a2)) =
eval vn (Var x) + eval vn (Times a1 a2)
vn: val
e1, e2, a1, a2: arith
IHe1: eval vn (Plus a1 a2) = eval vn e1
n: nat
IHe2: eval vn (Const n) = eval vn e2
eval vn
  match n with
  | 0 => Plus a1 a2
  | S _ => Plus (Plus a1 a2) (Const n)
  end = eval vn (Plus a1 a2) + eval vn (Const n)
vn: val
e1, e2, a1, a2: arith
IHe1: eval vn (Plus a1 a2) = eval vn e1
x: var
IHe2: eval vn (Var x) = eval vn e2
eval vn (Plus (Plus a1 a2) (Var x)) =
eval vn (Plus a1 a2) + eval vn (Var x)
vn: val
e1, e2, a1, a2: arith
IHe1: eval vn (Plus a1 a2) = eval vn e1
a3, a4: arith
IHe2: eval vn (Plus a3 a4) = eval vn e2
eval vn (Plus (Plus a1 a2) (Plus a3 a4)) =
eval vn (Plus a1 a2) + eval vn (Plus a3 a4)
vn: val
e1, e2, a1, a2: arith
IHe1: eval vn (Plus a1 a2) = eval vn e1
a3, a4: arith
IHe2: eval vn (Times a3 a4) = eval vn e2
eval vn (Plus (Plus a1 a2) (Times a3 a4)) =
eval vn (Plus a1 a2) + eval vn (Times a3 a4)
vn: val
e1, e2, a1, a2: arith
IHe1: eval vn (Times a1 a2) = eval vn e1
n: nat
IHe2: eval vn (Const n) = eval vn e2
eval vn
  match n with
  | 0 => Times a1 a2
  | S _ => Plus (Times a1 a2) (Const n)
  end = eval vn (Times a1 a2) + eval vn (Const n)
vn: val
e1, e2, a1, a2: arith
IHe1: eval vn (Times a1 a2) = eval vn e1
x: var
IHe2: eval vn (Var x) = eval vn e2
eval vn (Plus (Times a1 a2) (Var x)) =
eval vn (Times a1 a2) + eval vn (Var x)
vn: val
e1, e2, a1, a2: arith
IHe1: eval vn (Times a1 a2) = eval vn e1
a3, a4: arith
IHe2: eval vn (Plus a3 a4) = eval vn e2
eval vn (Plus (Times a1 a2) (Plus a3 a4)) =
eval vn (Times a1 a2) + eval vn (Plus a3 a4)
vn: val
e1, e2, a1, a2: arith
IHe1: eval vn (Times a1 a2) = eval vn e1
a3, a4: arith
IHe2: eval vn (Times a3 a4) = eval vn e2
eval vn (Plus (Times a1 a2) (Times a3 a4)) =
eval vn (Times a1 a2) + eval vn (Times a3 a4)
    all: try destruct n; simpl.vn: val
e1, e2: arith
IHe1: eval vn (Const 0) = eval vn e1
n0: nat
IHe2: eval vn (Const n0) = eval vn e2
n0 = n0
vn: val
e1, e2: arith
n: nat
IHe1: eval vn (Const (S n)) = eval vn e1
n0: nat
IHe2: eval vn (Const n0) = eval vn e2
S (n + n0) = S (n + n0)
vn: val
e1, e2: arith
IHe1: eval vn (Const 0) = eval vn e1
x: var
IHe2: eval vn (Var x) = eval vn e2
vn x = vn x
vn: val
e1, e2: arith
n: nat
IHe1: eval vn (Const (S n)) = eval vn e1
x: var
IHe2: eval vn (Var x) = eval vn e2
S (n + vn x) = S (n + vn x)
vn: val
e1, e2: arith
IHe1: eval vn (Const 0) = eval vn e1
a1, a2: arith
IHe2: eval vn (Plus a1 a2) = eval vn e2
eval vn a1 + eval vn a2 = eval vn a1 + eval vn a2
vn: val
e1, e2: arith
n: nat
IHe1: eval vn (Const (S n)) = eval vn e1
a1, a2: arith
IHe2: eval vn (Plus a1 a2) = eval vn e2
S (n + (eval vn a1 + eval vn a2)) =
S (n + (eval vn a1 + eval vn a2))
vn: val
e1, e2: arith
IHe1: eval vn (Const 0) = eval vn e1
a1, a2: arith
IHe2: eval vn (Times a1 a2) = eval vn e2
eval vn a1 * eval vn a2 = eval vn a1 * eval vn a2
vn: val
e1, e2: arith
n: nat
IHe1: eval vn (Const (S n)) = eval vn e1
a1, a2: arith
IHe2: eval vn (Times a1 a2) = eval vn e2
S (n + eval vn a1 * eval vn a2) =
S (n + eval vn a1 * eval vn a2)
vn: val
e1, e2: arith
x: var
IHe1: eval vn (Var x) = eval vn e1
IHe2: eval vn (Const 0) = eval vn e2
vn x = vn x + 0
vn: val
e1, e2: arith
x: var
IHe1: eval vn (Var x) = eval vn e1
n: nat
IHe2: eval vn (Const (S n)) = eval vn e2
vn x + S n = vn x + S n
vn: val
e1, e2: arith
x: var
IHe1: eval vn (Var x) = eval vn e1
x0: var
IHe2: eval vn (Var x0) = eval vn e2
vn x + vn x0 = vn x + vn x0
vn: val
e1, e2: arith
x: var
IHe1: eval vn (Var x) = eval vn e1
a1, a2: arith
IHe2: eval vn (Plus a1 a2) = eval vn e2
vn x + (eval vn a1 + eval vn a2) =
vn x + (eval vn a1 + eval vn a2)
vn: val
e1, e2: arith
x: var
IHe1: eval vn (Var x) = eval vn e1
a1, a2: arith
IHe2: eval vn (Times a1 a2) = eval vn e2
vn x + eval vn a1 * eval vn a2 =
vn x + eval vn a1 * eval vn a2
vn: val
e1, e2, a1, a2: arith
IHe1: eval vn (Plus a1 a2) = eval vn e1
IHe2: eval vn (Const 0) = eval vn e2
eval vn a1 + eval vn a2 = eval vn a1 + eval vn a2 + 0
vn: val
e1, e2, a1, a2: arith
IHe1: eval vn (Plus a1 a2) = eval vn e1
n: nat
IHe2: eval vn (Const (S n)) = eval vn e2
eval vn a1 + eval vn a2 + S n =
eval vn a1 + eval vn a2 + S n
vn: val
e1, e2, a1, a2: arith
IHe1: eval vn (Plus a1 a2) = eval vn e1
x: var
IHe2: eval vn (Var x) = eval vn e2
eval vn a1 + eval vn a2 + vn x =
eval vn a1 + eval vn a2 + vn x
vn: val
e1, e2, a1, a2: arith
IHe1: eval vn (Plus a1 a2) = eval vn e1
a3, a4: arith
IHe2: eval vn (Plus a3 a4) = eval vn e2
eval vn a1 + eval vn a2 + (eval vn a3 + eval vn a4) =
eval vn a1 + eval vn a2 + (eval vn a3 + eval vn a4)
vn: val
e1, e2, a1, a2: arith
IHe1: eval vn (Plus a1 a2) = eval vn e1
a3, a4: arith
IHe2: eval vn (Times a3 a4) = eval vn e2
eval vn a1 + eval vn a2 + eval vn a3 * eval vn a4 =
eval vn a1 + eval vn a2 + eval vn a3 * eval vn a4
vn: val
e1, e2, a1, a2: arith
IHe1: eval vn (Times a1 a2) = eval vn e1
IHe2: eval vn (Const 0) = eval vn e2
eval vn a1 * eval vn a2 = eval vn a1 * eval vn a2 + 0
vn: val
e1, e2, a1, a2: arith
IHe1: eval vn (Times a1 a2) = eval vn e1
n: nat
IHe2: eval vn (Const (S n)) = eval vn e2
eval vn a1 * eval vn a2 + S n =
eval vn a1 * eval vn a2 + S n
vn: val
e1, e2, a1, a2: arith
IHe1: eval vn (Times a1 a2) = eval vn e1
x: var
IHe2: eval vn (Var x) = eval vn e2
eval vn a1 * eval vn a2 + vn x =
eval vn a1 * eval vn a2 + vn x
vn: val
e1, e2, a1, a2: arith
IHe1: eval vn (Times a1 a2) = eval vn e1
a3, a4: arith
IHe2: eval vn (Plus a3 a4) = eval vn e2
eval vn a1 * eval vn a2 + (eval vn a3 + eval vn a4) =
eval vn a1 * eval vn a2 + (eval vn a3 + eval vn a4)
vn: val
e1, e2, a1, a2: arith
IHe1: eval vn (Times a1 a2) = eval vn e1
a3, a4: arith
IHe2: eval vn (Times a3 a4) = eval vn e2
eval vn a1 * eval vn a2 + eval vn a3 * eval vn a4 =
eval vn a1 * eval vn a2 + eval vn a3 * eval vn a4
    all: lia.
  -vn: val
e1, e2: arith
IHe1: eval vn (constantFold e1) = eval vn e1
IHe2: eval vn (constantFold e2) = eval vn e2
eval vn
  match constantFold e1 with
  | Const (0 as n1) =>
      match constantFold e2 with
      | Const n2 => Const (n1 * n2)
      | _ => Const 0
      end
  | Const (1 as n1) =>
      match constantFold e2 with
      | Const n2 => Const (n1 * n2)
      | _ => constantFold e2
      end
  | Const (S (S _) as n1) =>
      match constantFold e2 with
      | Const n2 => Const (n1 * n2)
      | _ => Times (constantFold e1) (constantFold e2)
      end
  | _ =>
      match constantFold e2 with
      | Const 0 => Const 0
      | Const 1 => constantFold e1
      | _ => Times (constantFold e1) (constantFold e2)
      end
  end = eval vn e1 * eval vn e2 rewrite <- IHe1, <- IHe2.vn: val
e1, e2: arith
IHe1: eval vn (constantFold e1) = eval vn e1
IHe2: eval vn (constantFold e2) = eval vn e2
eval vn
  match constantFold e1 with
  | Const (0 as n1) =>
      match constantFold e2 with
      | Const n2 => Const (n1 * n2)
      | _ => Const 0
      end
  | Const (1 as n1) =>
      match constantFold e2 with
      | Const n2 => Const (n1 * n2)
      | _ => constantFold e2
      end
  | Const (S (S _) as n1) =>
      match constantFold e2 with
      | Const n2 => Const (n1 * n2)
      | _ => Times (constantFold e1) (constantFold e2)
      end
  | _ =>
      match constantFold e2 with
      | Const 0 => Const 0
      | Const 1 => constantFold e1
      | _ => Times (constantFold e1) (constantFold e2)
      end
  end =
eval vn (constantFold e1) * eval vn (constantFold e2)
    destruct (constantFold e1), (constantFold e2).vn: val
e1, e2: arith
n: nat
IHe1: eval vn (Const n) = eval vn e1
n0: nat
IHe2: eval vn (Const n0) = eval vn e2
eval vn match n with
        | 0 | _ => Const (n * n0)
        end = eval vn (Const n) * eval vn (Const n0)
vn: val
e1, e2: arith
n: nat
IHe1: eval vn (Const n) = eval vn e1
x: var
IHe2: eval vn (Var x) = eval vn e2
eval vn
  match n with
  | 0 => Const 0
  | 1 => Var x
  | S (S _) => Times (Const n) (Var x)
  end = eval vn (Const n) * eval vn (Var x)
vn: val
e1, e2: arith
n: nat
IHe1: eval vn (Const n) = eval vn e1
a1, a2: arith
IHe2: eval vn (Plus a1 a2) = eval vn e2
eval vn
  match n with
  | 0 => Const 0
  | 1 => Plus a1 a2
  | S (S _) => Times (Const n) (Plus a1 a2)
  end = eval vn (Const n) * eval vn (Plus a1 a2)
vn: val
e1, e2: arith
n: nat
IHe1: eval vn (Const n) = eval vn e1
a1, a2: arith
IHe2: eval vn (Times a1 a2) = eval vn e2
eval vn
  match n with
  | 0 => Const 0
  | 1 => Times a1 a2
  | S (S _) => Times (Const n) (Times a1 a2)
  end = eval vn (Const n) * eval vn (Times a1 a2)
vn: val
e1, e2: arith
x: var
IHe1: eval vn (Var x) = eval vn e1
n: nat
IHe2: eval vn (Const n) = eval vn e2
eval vn
  match n with
  | 0 => Const 0
  | 1 => Var x
  | S (S _) => Times (Var x) (Const n)
  end = eval vn (Var x) * eval vn (Const n)
vn: val
e1, e2: arith
x: var
IHe1: eval vn (Var x) = eval vn e1
x0: var
IHe2: eval vn (Var x0) = eval vn e2
eval vn (Times (Var x) (Var x0)) =
eval vn (Var x) * eval vn (Var x0)
vn: val
e1, e2: arith
x: var
IHe1: eval vn (Var x) = eval vn e1
a1, a2: arith
IHe2: eval vn (Plus a1 a2) = eval vn e2
eval vn (Times (Var x) (Plus a1 a2)) =
eval vn (Var x) * eval vn (Plus a1 a2)
vn: val
e1, e2: arith
x: var
IHe1: eval vn (Var x) = eval vn e1
a1, a2: arith
IHe2: eval vn (Times a1 a2) = eval vn e2
eval vn (Times (Var x) (Times a1 a2)) =
eval vn (Var x) * eval vn (Times a1 a2)
vn: val
e1, e2, a1, a2: arith
IHe1: eval vn (Plus a1 a2) = eval vn e1
n: nat
IHe2: eval vn (Const n) = eval vn e2
eval vn
  match n with
  | 0 => Const 0
  | 1 => Plus a1 a2
  | S (S _) => Times (Plus a1 a2) (Const n)
  end = eval vn (Plus a1 a2) * eval vn (Const n)
vn: val
e1, e2, a1, a2: arith
IHe1: eval vn (Plus a1 a2) = eval vn e1
x: var
IHe2: eval vn (Var x) = eval vn e2
eval vn (Times (Plus a1 a2) (Var x)) =
eval vn (Plus a1 a2) * eval vn (Var x)
vn: val
e1, e2, a1, a2: arith
IHe1: eval vn (Plus a1 a2) = eval vn e1
a3, a4: arith
IHe2: eval vn (Plus a3 a4) = eval vn e2
eval vn (Times (Plus a1 a2) (Plus a3 a4)) =
eval vn (Plus a1 a2) * eval vn (Plus a3 a4)
vn: val
e1, e2, a1, a2: arith
IHe1: eval vn (Plus a1 a2) = eval vn e1
a3, a4: arith
IHe2: eval vn (Times a3 a4) = eval vn e2
eval vn (Times (Plus a1 a2) (Times a3 a4)) =
eval vn (Plus a1 a2) * eval vn (Times a3 a4)
vn: val
e1, e2, a1, a2: arith
IHe1: eval vn (Times a1 a2) = eval vn e1
n: nat
IHe2: eval vn (Const n) = eval vn e2
eval vn
  match n with
  | 0 => Const 0
  | 1 => Times a1 a2
  | S (S _) => Times (Times a1 a2) (Const n)
  end = eval vn (Times a1 a2) * eval vn (Const n)
vn: val
e1, e2, a1, a2: arith
IHe1: eval vn (Times a1 a2) = eval vn e1
x: var
IHe2: eval vn (Var x) = eval vn e2
eval vn (Times (Times a1 a2) (Var x)) =
eval vn (Times a1 a2) * eval vn (Var x)
vn: val
e1, e2, a1, a2: arith
IHe1: eval vn (Times a1 a2) = eval vn e1
a3, a4: arith
IHe2: eval vn (Plus a3 a4) = eval vn e2
eval vn (Times (Times a1 a2) (Plus a3 a4)) =
eval vn (Times a1 a2) * eval vn (Plus a3 a4)
vn: val
e1, e2, a1, a2: arith
IHe1: eval vn (Times a1 a2) = eval vn e1
a3, a4: arith
IHe2: eval vn (Times a3 a4) = eval vn e2
eval vn (Times (Times a1 a2) (Times a3 a4)) =
eval vn (Times a1 a2) * eval vn (Times a3 a4)
    all: try destruct n; simpl.vn: val
e1, e2: arith
IHe1: eval vn (Const 0) = eval vn e1
n0: nat
IHe2: eval vn (Const n0) = eval vn e2
0 = 0
vn: val
e1, e2: arith
n: nat
IHe1: eval vn (Const (S n)) = eval vn e1
n0: nat
IHe2: eval vn (Const n0) = eval vn e2
eval vn
  match n with
  | 0 | _ => Const (n0 + n * n0)
  end = n0 + n * n0
vn: val
e1, e2: arith
IHe1: eval vn (Const 0) = eval vn e1
x: var
IHe2: eval vn (Var x) = eval vn e2
0 = 0
vn: val
e1, e2: arith
n: nat
IHe1: eval vn (Const (S n)) = eval vn e1
x: var
IHe2: eval vn (Var x) = eval vn e2
eval vn
  match n with
  | 0 => Var x
  | S _ => Times (Const (S n)) (Var x)
  end = vn x + n * vn x
vn: val
e1, e2: arith
IHe1: eval vn (Const 0) = eval vn e1
a1, a2: arith
IHe2: eval vn (Plus a1 a2) = eval vn e2
0 = 0
vn: val
e1, e2: arith
n: nat
IHe1: eval vn (Const (S n)) = eval vn e1
a1, a2: arith
IHe2: eval vn (Plus a1 a2) = eval vn e2
eval vn
  match n with
  | 0 => Plus a1 a2
  | S _ => Times (Const (S n)) (Plus a1 a2)
  end =
eval vn a1 + eval vn a2 +
n * (eval vn a1 + eval vn a2)
vn: val
e1, e2: arith
IHe1: eval vn (Const 0) = eval vn e1
a1, a2: arith
IHe2: eval vn (Times a1 a2) = eval vn e2
0 = 0
vn: val
e1, e2: arith
n: nat
IHe1: eval vn (Const (S n)) = eval vn e1
a1, a2: arith
IHe2: eval vn (Times a1 a2) = eval vn e2
eval vn
  match n with
  | 0 => Times a1 a2
  | S _ => Times (Const (S n)) (Times a1 a2)
  end =
eval vn a1 * eval vn a2 +
n * (eval vn a1 * eval vn a2)
vn: val
e1, e2: arith
x: var
IHe1: eval vn (Var x) = eval vn e1
IHe2: eval vn (Const 0) = eval vn e2
0 = vn x * 0
vn: val
e1, e2: arith
x: var
IHe1: eval vn (Var x) = eval vn e1
n: nat
IHe2: eval vn (Const (S n)) = eval vn e2
eval vn
  match n with
  | 0 => Var x
  | S _ => Times (Var x) (Const (S n))
  end = vn x * S n
vn: val
e1, e2: arith
x: var
IHe1: eval vn (Var x) = eval vn e1
x0: var
IHe2: eval vn (Var x0) = eval vn e2
vn x * vn x0 = vn x * vn x0
vn: val
e1, e2: arith
x: var
IHe1: eval vn (Var x) = eval vn e1
a1, a2: arith
IHe2: eval vn (Plus a1 a2) = eval vn e2
vn x * (eval vn a1 + eval vn a2) =
vn x * (eval vn a1 + eval vn a2)
vn: val
e1, e2: arith
x: var
IHe1: eval vn (Var x) = eval vn e1
a1, a2: arith
IHe2: eval vn (Times a1 a2) = eval vn e2
vn x * (eval vn a1 * eval vn a2) =
vn x * (eval vn a1 * eval vn a2)
vn: val
e1, e2, a1, a2: arith
IHe1: eval vn (Plus a1 a2) = eval vn e1
IHe2: eval vn (Const 0) = eval vn e2
0 = (eval vn a1 + eval vn a2) * 0
vn: val
e1, e2, a1, a2: arith
IHe1: eval vn (Plus a1 a2) = eval vn e1
n: nat
IHe2: eval vn (Const (S n)) = eval vn e2
eval vn
  match n with
  | 0 => Plus a1 a2
  | S _ => Times (Plus a1 a2) (Const (S n))
  end = (eval vn a1 + eval vn a2) * S n
vn: val
e1, e2, a1, a2: arith
IHe1: eval vn (Plus a1 a2) = eval vn e1
x: var
IHe2: eval vn (Var x) = eval vn e2
(eval vn a1 + eval vn a2) * vn x =
(eval vn a1 + eval vn a2) * vn x
vn: val
e1, e2, a1, a2: arith
IHe1: eval vn (Plus a1 a2) = eval vn e1
a3, a4: arith
IHe2: eval vn (Plus a3 a4) = eval vn e2
(eval vn a1 + eval vn a2) * (eval vn a3 + eval vn a4) =
(eval vn a1 + eval vn a2) * (eval vn a3 + eval vn a4)
vn: val
e1, e2, a1, a2: arith
IHe1: eval vn (Plus a1 a2) = eval vn e1
a3, a4: arith
IHe2: eval vn (Times a3 a4) = eval vn e2
(eval vn a1 + eval vn a2) * (eval vn a3 * eval vn a4) =
(eval vn a1 + eval vn a2) * (eval vn a3 * eval vn a4)
vn: val
e1, e2, a1, a2: arith
IHe1: eval vn (Times a1 a2) = eval vn e1
IHe2: eval vn (Const 0) = eval vn e2
0 = eval vn a1 * eval vn a2 * 0
vn: val
e1, e2, a1, a2: arith
IHe1: eval vn (Times a1 a2) = eval vn e1
n: nat
IHe2: eval vn (Const (S n)) = eval vn e2
eval vn
  match n with
  | 0 => Times a1 a2
  | S _ => Times (Times a1 a2) (Const (S n))
  end = eval vn a1 * eval vn a2 * S n
vn: val
e1, e2, a1, a2: arith
IHe1: eval vn (Times a1 a2) = eval vn e1
x: var
IHe2: eval vn (Var x) = eval vn e2
eval vn a1 * eval vn a2 * vn x =
eval vn a1 * eval vn a2 * vn x
vn: val
e1, e2, a1, a2: arith
IHe1: eval vn (Times a1 a2) = eval vn e1
a3, a4: arith
IHe2: eval vn (Plus a3 a4) = eval vn e2
eval vn a1 * eval vn a2 * (eval vn a3 + eval vn a4) =
eval vn a1 * eval vn a2 * (eval vn a3 + eval vn a4)
vn: val
e1, e2, a1, a2: arith
IHe1: eval vn (Times a1 a2) = eval vn e1
a3, a4: arith
IHe2: eval vn (Times a3 a4) = eval vn e2
eval vn a1 * eval vn a2 * (eval vn a3 * eval vn a4) =
eval vn a1 * eval vn a2 * (eval vn a3 * eval vn a4)
    all: try destruct n; simpl.vn: val
e1, e2: arith
IHe1: eval vn (Const 0) = eval vn e1
n0: nat
IHe2: eval vn (Const n0) = eval vn e2
0 = 0
vn: val
e1, e2: arith
IHe1: eval vn (Const 1) = eval vn e1
n0: nat
IHe2: eval vn (Const n0) = eval vn e2
n0 + 0 = n0 + 0
vn: val
e1, e2: arith
n: nat
IHe1: eval vn (Const (S (S n))) = eval vn e1
n0: nat
IHe2: eval vn (Const n0) = eval vn e2
n0 + (n0 + n * n0) = n0 + (n0 + n * n0)
vn: val
e1, e2: arith
IHe1: eval vn (Const 0) = eval vn e1
x: var
IHe2: eval vn (Var x) = eval vn e2
0 = 0
vn: val
e1, e2: arith
IHe1: eval vn (Const 1) = eval vn e1
x: var
IHe2: eval vn (Var x) = eval vn e2
vn x = vn x + 0
vn: val
e1, e2: arith
n: nat
IHe1: eval vn (Const (S (S n))) = eval vn e1
x: var
IHe2: eval vn (Var x) = eval vn e2
vn x + (vn x + n * vn x) = vn x + (vn x + n * vn x)
vn: val
e1, e2: arith
IHe1: eval vn (Const 0) = eval vn e1
a1, a2: arith
IHe2: eval vn (Plus a1 a2) = eval vn e2
0 = 0
vn: val
e1, e2: arith
IHe1: eval vn (Const 1) = eval vn e1
a1, a2: arith
IHe2: eval vn (Plus a1 a2) = eval vn e2
eval vn a1 + eval vn a2 = eval vn a1 + eval vn a2 + 0
vn: val
e1, e2: arith
n: nat
IHe1: eval vn (Const (S (S n))) = eval vn e1
a1, a2: arith
IHe2: eval vn (Plus a1 a2) = eval vn e2
eval vn a1 + eval vn a2 +
(eval vn a1 + eval vn a2 +
 n * (eval vn a1 + eval vn a2)) =
eval vn a1 + eval vn a2 +
(eval vn a1 + eval vn a2 +
 n * (eval vn a1 + eval vn a2))
vn: val
e1, e2: arith
IHe1: eval vn (Const 0) = eval vn e1
a1, a2: arith
IHe2: eval vn (Times a1 a2) = eval vn e2
0 = 0
vn: val
e1, e2: arith
IHe1: eval vn (Const 1) = eval vn e1
a1, a2: arith
IHe2: eval vn (Times a1 a2) = eval vn e2
eval vn a1 * eval vn a2 = eval vn a1 * eval vn a2 + 0
vn: val
e1, e2: arith
n: nat
IHe1: eval vn (Const (S (S n))) = eval vn e1
a1, a2: arith
IHe2: eval vn (Times a1 a2) = eval vn e2
eval vn a1 * eval vn a2 +
(eval vn a1 * eval vn a2 +
 n * (eval vn a1 * eval vn a2)) =
eval vn a1 * eval vn a2 +
(eval vn a1 * eval vn a2 +
 n * (eval vn a1 * eval vn a2))
vn: val
e1, e2: arith
x: var
IHe1: eval vn (Var x) = eval vn e1
IHe2: eval vn (Const 0) = eval vn e2
0 = vn x * 0
vn: val
e1, e2: arith
x: var
IHe1: eval vn (Var x) = eval vn e1
IHe2: eval vn (Const 1) = eval vn e2
vn x = vn x * 1
vn: val
e1, e2: arith
x: var
IHe1: eval vn (Var x) = eval vn e1
n: nat
IHe2: eval vn (Const (S (S n))) = eval vn e2
vn x * S (S n) = vn x * S (S n)
vn: val
e1, e2: arith
x: var
IHe1: eval vn (Var x) = eval vn e1
x0: var
IHe2: eval vn (Var x0) = eval vn e2
vn x * vn x0 = vn x * vn x0
vn: val
e1, e2: arith
x: var
IHe1: eval vn (Var x) = eval vn e1
a1, a2: arith
IHe2: eval vn (Plus a1 a2) = eval vn e2
vn x * (eval vn a1 + eval vn a2) =
vn x * (eval vn a1 + eval vn a2)
vn: val
e1, e2: arith
x: var
IHe1: eval vn (Var x) = eval vn e1
a1, a2: arith
IHe2: eval vn (Times a1 a2) = eval vn e2
vn x * (eval vn a1 * eval vn a2) =
vn x * (eval vn a1 * eval vn a2)
vn: val
e1, e2, a1, a2: arith
IHe1: eval vn (Plus a1 a2) = eval vn e1
IHe2: eval vn (Const 0) = eval vn e2
0 = (eval vn a1 + eval vn a2) * 0
vn: val
e1, e2, a1, a2: arith
IHe1: eval vn (Plus a1 a2) = eval vn e1
IHe2: eval vn (Const 1) = eval vn e2
eval vn a1 + eval vn a2 =
(eval vn a1 + eval vn a2) * 1
vn: val
e1, e2, a1, a2: arith
IHe1: eval vn (Plus a1 a2) = eval vn e1
n: nat
IHe2: eval vn (Const (S (S n))) = eval vn e2
(eval vn a1 + eval vn a2) * S (S n) =
(eval vn a1 + eval vn a2) * S (S n)
vn: val
e1, e2, a1, a2: arith
IHe1: eval vn (Plus a1 a2) = eval vn e1
x: var
IHe2: eval vn (Var x) = eval vn e2
(eval vn a1 + eval vn a2) * vn x =
(eval vn a1 + eval vn a2) * vn x
vn: val
e1, e2, a1, a2: arith
IHe1: eval vn (Plus a1 a2) = eval vn e1
a3, a4: arith
IHe2: eval vn (Plus a3 a4) = eval vn e2
(eval vn a1 + eval vn a2) * (eval vn a3 + eval vn a4) =
(eval vn a1 + eval vn a2) * (eval vn a3 + eval vn a4)
vn: val
e1, e2, a1, a2: arith
IHe1: eval vn (Plus a1 a2) = eval vn e1
a3, a4: arith
IHe2: eval vn (Times a3 a4) = eval vn e2
(eval vn a1 + eval vn a2) * (eval vn a3 * eval vn a4) =
(eval vn a1 + eval vn a2) * (eval vn a3 * eval vn a4)
vn: val
e1, e2, a1, a2: arith
IHe1: eval vn (Times a1 a2) = eval vn e1
IHe2: eval vn (Const 0) = eval vn e2
0 = eval vn a1 * eval vn a2 * 0
vn: val
e1, e2, a1, a2: arith
IHe1: eval vn (Times a1 a2) = eval vn e1
IHe2: eval vn (Const 1) = eval vn e2
eval vn a1 * eval vn a2 = eval vn a1 * eval vn a2 * 1
vn: val
e1, e2, a1, a2: arith
IHe1: eval vn (Times a1 a2) = eval vn e1
n: nat
IHe2: eval vn (Const (S (S n))) = eval vn e2
eval vn a1 * eval vn a2 * S (S n) =
eval vn a1 * eval vn a2 * S (S n)
vn: val
e1, e2, a1, a2: arith
IHe1: eval vn (Times a1 a2) = eval vn e1
x: var
IHe2: eval vn (Var x) = eval vn e2
eval vn a1 * eval vn a2 * vn x =
eval vn a1 * eval vn a2 * vn x
vn: val
e1, e2, a1, a2: arith
IHe1: eval vn (Times a1 a2) = eval vn e1
a3, a4: arith
IHe2: eval vn (Plus a3 a4) = eval vn e2
eval vn a1 * eval vn a2 * (eval vn a3 + eval vn a4) =
eval vn a1 * eval vn a2 * (eval vn a3 + eval vn a4)
vn: val
e1, e2, a1, a2: arith
IHe1: eval vn (Times a1 a2) = eval vn e1
a3, a4: arith
IHe2: eval vn (Times a3 a4) = eval vn e2
eval vn a1 * eval vn a2 * (eval vn a3 * eval vn a4) =
eval vn a1 * eval vn a2 * (eval vn a3 * eval vn a4)
    all: lia.
Qed.

Pushing constants into multiplications

To define our last transformation, we first write a roundabout way of testing whether an expression is a constant. This detour happens to be useful to avoid overhead in concert with pattern matching, since Coq internally elaborates wildcard _ patterns into separate destruct for all constructors not considered beforehand. That expansion can create serious code blow-ups, leading to serious proof blow-ups!

Definition isConst (e : arith) : option nat :=
  match e with
  | Const n => Some n
  | _ => None
  end.

Our next target is a function that finds multiplications by constants and pushes the multiplications to the leaves of syntax trees, ideally finding constants, which can be replaced by larger constants, not affecting the meanings of expressions. This helper function takes a coefficient multiplyBy that should be applied to an expression.

Fixpoint pushMultiplicationInside'
  (multiplyBy : nat) (e : arith) : arith :=
  match e with
  | Const n => Const (multiplyBy * n)
  | Var _ => Times (Const multiplyBy) e
  | Plus e1 e2 => Plus (pushMultiplicationInside' multiplyBy e1)
                    (pushMultiplicationInside' multiplyBy e2)
  | Times e1 e2 =>
      match isConst e1 with
      | Some k => pushMultiplicationInside' (k * multiplyBy) e2
      | None => Times (pushMultiplicationInside' multiplyBy e1) e2
      end
  end.

The overall transformation just fixes the initial coefficient as 1.

Definition pushMultiplicationInside (e : arith) : arith :=
  pushMultiplicationInside' 1 e.

A fun fact about pushing multiplication inside: the coefficient has no effect on depth! Let's start by showing any coefficient is equivalent to coefficient 0.

Lemma depth_pushMultiplicationInside'_irrelevance0 :
  forall e multiplyBy,
    depth (pushMultiplicationInside' multiplyBy e)
    = depth (pushMultiplicationInside' 0 e).forall (e : arith) (multiplyBy : nat),
depth (pushMultiplicationInside' multiplyBy e) =
depth (pushMultiplicationInside' 0 e)
Proof.forall (e : arith) (multiplyBy : nat),
depth (pushMultiplicationInside' multiplyBy e) =
depth (pushMultiplicationInside' 0 e)
  induction e; intros; simpl in *.n, multiplyBy: nat
1 = 1
x: var
multiplyBy: nat
2 = 2
e1, e2: arith
IHe1: forall multiplyBy : nat,
depth (pushMultiplicationInside' multiplyBy e1) =
depth (pushMultiplicationInside' 0 e1)
IHe2: forall multiplyBy : nat,
depth (pushMultiplicationInside' multiplyBy e2) =
depth (pushMultiplicationInside' 0 e2)
multiplyBy: nat
S
  (max
     (depth (pushMultiplicationInside' multiplyBy e1))
     (depth (pushMultiplicationInside' multiplyBy e2))) =
S
  (max (depth (pushMultiplicationInside' 0 e1))
     (depth (pushMultiplicationInside' 0 e2)))
e1, e2: arith
IHe1: forall multiplyBy : nat,
depth (pushMultiplicationInside' multiplyBy e1) =
depth (pushMultiplicationInside' 0 e1)
IHe2: forall multiplyBy : nat,
depth (pushMultiplicationInside' multiplyBy e2) =
depth (pushMultiplicationInside' 0 e2)
multiplyBy: nat
depth
  match isConst e1 with
  | Some k =>
      pushMultiplicationInside' (k * multiplyBy) e2
  | None =>
      Times (pushMultiplicationInside' multiplyBy e1)
        e2
  end =
depth
  match isConst e1 with
  | Some k => pushMultiplicationInside' (k * 0) e2
  | None => Times (pushMultiplicationInside' 0 e1) e2
  end

  -n, multiplyBy: nat
1 = 1 lia.
  -x: var
multiplyBy: nat
2 = 2 lia.
  - (* Plus *)e1, e2: arith
IHe1: forall multiplyBy : nat,
depth (pushMultiplicationInside' multiplyBy e1) =
depth (pushMultiplicationInside' 0 e1)
IHe2: forall multiplyBy : nat,
depth (pushMultiplicationInside' multiplyBy e2) =
depth (pushMultiplicationInside' 0 e2)
multiplyBy: nat
S
  (max
     (depth (pushMultiplicationInside' multiplyBy e1))
     (depth (pushMultiplicationInside' multiplyBy e2))) =
S
  (max (depth (pushMultiplicationInside' 0 e1))
     (depth (pushMultiplicationInside' 0 e2)))

    rewrite IHe1.e1, e2: arith
IHe1: forall multiplyBy : nat,
depth (pushMultiplicationInside' multiplyBy e1) =
depth (pushMultiplicationInside' 0 e1)
IHe2: forall multiplyBy : nat,
depth (pushMultiplicationInside' multiplyBy e2) =
depth (pushMultiplicationInside' 0 e2)
multiplyBy: nat
S
  (max (depth (pushMultiplicationInside' 0 e1))
     (depth (pushMultiplicationInside' multiplyBy e2))) =
S
  (max (depth (pushMultiplicationInside' 0 e1))
     (depth (pushMultiplicationInside' 0 e2)))

rewrite H: Where H is a hypothesis or previously proved theorem, establishing forall x1 .. xN, e1 = e2, find a subterm of the goal that equals e1, given the right choices of xi values, and replace that subterm with e2.

    rewrite IHe2.e1, e2: arith
IHe1: forall multiplyBy : nat,
depth (pushMultiplicationInside' multiplyBy e1) =
depth (pushMultiplicationInside' 0 e1)
IHe2: forall multiplyBy : nat,
depth (pushMultiplicationInside' multiplyBy e2) =
depth (pushMultiplicationInside' 0 e2)
multiplyBy: nat
S
  (max (depth (pushMultiplicationInside' 0 e1))
     (depth (pushMultiplicationInside' 0 e2))) =
S
  (max (depth (pushMultiplicationInside' 0 e1))
     (depth (pushMultiplicationInside' 0 e2)))
    lia.

  -e1, e2: arith
IHe1: forall multiplyBy : nat,
depth (pushMultiplicationInside' multiplyBy e1) =
depth (pushMultiplicationInside' 0 e1)
IHe2: forall multiplyBy : nat,
depth (pushMultiplicationInside' multiplyBy e2) =
depth (pushMultiplicationInside' 0 e2)
multiplyBy: nat
depth
  match isConst e1 with
  | Some k =>
      pushMultiplicationInside' (k * multiplyBy) e2
  | None =>
      Times (pushMultiplicationInside' multiplyBy e1)
        e2
  end =
depth
  match isConst e1 with
  | Some k => pushMultiplicationInside' (k * 0) e2
  | None => Times (pushMultiplicationInside' 0 e1) e2
  end destruct (isConst e1); simpl.e1, e2: arith
IHe1: forall multiplyBy : nat,
depth (pushMultiplicationInside' multiplyBy e1) =
depth (pushMultiplicationInside' 0 e1)
IHe2: forall multiplyBy : nat,
depth (pushMultiplicationInside' multiplyBy e2) =
depth (pushMultiplicationInside' 0 e2)
multiplyBy, n: nat
depth (pushMultiplicationInside' (n * multiplyBy) e2) =
depth (pushMultiplicationInside' (n * 0) e2)
e1, e2: arith
IHe1: forall multiplyBy : nat,
depth (pushMultiplicationInside' multiplyBy e1) =
depth (pushMultiplicationInside' 0 e1)
IHe2: forall multiplyBy : nat,
depth (pushMultiplicationInside' multiplyBy e2) =
depth (pushMultiplicationInside' 0 e2)
multiplyBy: nat
S
  (max
     (depth (pushMultiplicationInside' multiplyBy e1))
     (depth e2)) =
S
  (max (depth (pushMultiplicationInside' 0 e1))
     (depth e2))
    +e1, e2: arith
IHe1: forall multiplyBy : nat,
depth (pushMultiplicationInside' multiplyBy e1) =
depth (pushMultiplicationInside' 0 e1)
IHe2: forall multiplyBy : nat,
depth (pushMultiplicationInside' multiplyBy e2) =
depth (pushMultiplicationInside' 0 e2)
multiplyBy, n: nat
depth (pushMultiplicationInside' (n * multiplyBy) e2) =
depth (pushMultiplicationInside' (n * 0) e2) rewrite IHe2.e1, e2: arith
IHe1: forall multiplyBy : nat,
depth (pushMultiplicationInside' multiplyBy e1) =
depth (pushMultiplicationInside' 0 e1)
IHe2: forall multiplyBy : nat,
depth (pushMultiplicationInside' multiplyBy e2) =
depth (pushMultiplicationInside' 0 e2)
multiplyBy, n: nat
depth (pushMultiplicationInside' 0 e2) =
depth (pushMultiplicationInside' (n * 0) e2)

Neither lia nor congruence is powerful enough on its own here, so we use a separate lemma to simplify n * 0:

      Search (_ * 0 = 0).mul_0_r: forall n : nat, n * 0 = 0
e1, e2: arith
IHe1: forall multiplyBy : nat,
depth (pushMultiplicationInside' multiplyBy e1) =
depth (pushMultiplicationInside' 0 e1)
IHe2: forall multiplyBy : nat,
depth (pushMultiplicationInside' multiplyBy e2) =
depth (pushMultiplicationInside' 0 e2)
multiplyBy, n: nat
depth (pushMultiplicationInside' 0 e2) =
depth (pushMultiplicationInside' (n * 0) e2)

      rewrite mul_0_r.e1, e2: arith
IHe1: forall multiplyBy : nat,
depth (pushMultiplicationInside' multiplyBy e1) =
depth (pushMultiplicationInside' 0 e1)
IHe2: forall multiplyBy : nat,
depth (pushMultiplicationInside' multiplyBy e2) =
depth (pushMultiplicationInside' 0 e2)
multiplyBy, n: nat
depth (pushMultiplicationInside' 0 e2) =
depth (pushMultiplicationInside' 0 e2)
      lia.
    +e1, e2: arith
IHe1: forall multiplyBy : nat,
depth (pushMultiplicationInside' multiplyBy e1) =
depth (pushMultiplicationInside' 0 e1)
IHe2: forall multiplyBy : nat,
depth (pushMultiplicationInside' multiplyBy e2) =
depth (pushMultiplicationInside' 0 e2)
multiplyBy: nat
S
  (max
     (depth (pushMultiplicationInside' multiplyBy e1))
     (depth e2)) =
S
  (max (depth (pushMultiplicationInside' 0 e1))
     (depth e2)) rewrite IHe1.e1, e2: arith
IHe1: forall multiplyBy : nat,
depth (pushMultiplicationInside' multiplyBy e1) =
depth (pushMultiplicationInside' 0 e1)
IHe2: forall multiplyBy : nat,
depth (pushMultiplicationInside' multiplyBy e2) =
depth (pushMultiplicationInside' 0 e2)
multiplyBy: nat
S
  (max (depth (pushMultiplicationInside' 0 e1))
     (depth e2)) =
S
  (max (depth (pushMultiplicationInside' 0 e1))
     (depth e2))
      lia.
Qed.

It can be remarkably hard to get Coq's automation to be dumb enough to help us demonstrate all of the primitive tactics. ;-) In particular, we can redo the proof in an automated way, without the explicit rewrites.

Lemma depth_pushMultiplicationInside'_irrelevance0_snazzy :
  forall e multiplyBy,
    depth (pushMultiplicationInside' multiplyBy e)
    = depth (pushMultiplicationInside' 0 e).forall (e : arith) (multiplyBy : nat),
depth (pushMultiplicationInside' multiplyBy e) =
depth (pushMultiplicationInside' 0 e)
Proof.forall (e : arith) (multiplyBy : nat),
depth (pushMultiplicationInside' multiplyBy e) =
depth (pushMultiplicationInside' 0 e)
  induction e; simpl;
    try match goal with
      | [ |- context[match ?E with _ => _ end] ] =>
          destruct E; simpl
      end; congruence.
Qed.

Now the general corollary about irrelevance of coefficients for depth.

Lemma depth_pushMultiplicationInside'_irrelevance :
  forall e multiplyBy1 multiplyBy2,
    depth (pushMultiplicationInside' multiplyBy1 e)
    = depth (pushMultiplicationInside' multiplyBy2 e).forall (e : arith) (multiplyBy1 multiplyBy2 : nat),
depth (pushMultiplicationInside' multiplyBy1 e) =
depth (pushMultiplicationInside' multiplyBy2 e)
Proof.forall (e : arith) (multiplyBy1 multiplyBy2 : nat),
depth (pushMultiplicationInside' multiplyBy1 e) =
depth (pushMultiplicationInside' multiplyBy2 e)
  intros.e: arith
multiplyBy1, multiplyBy2: nat
depth (pushMultiplicationInside' multiplyBy1 e) =
depth (pushMultiplicationInside' multiplyBy2 e)
  transitivity (depth (pushMultiplicationInside' 0 e)).e: arith
multiplyBy1, multiplyBy2: nat
depth (pushMultiplicationInside' multiplyBy1 e) =
depth (pushMultiplicationInside' 0 e)
e: arith
multiplyBy1, multiplyBy2: nat
depth (pushMultiplicationInside' 0 e) =
depth (pushMultiplicationInside' multiplyBy2 e)

  -e: arith
multiplyBy1, multiplyBy2: nat
depth (pushMultiplicationInside' multiplyBy1 e) =
depth (pushMultiplicationInside' 0 e) apply depth_pushMultiplicationInside'_irrelevance0.

apply H: For H a hypothesis or previously proved theorem, establishing some fact that matches the structure of the current conclusion, switch to proving H's own hypotheses. This is backwards reasoning via a known fact.

  -e: arith
multiplyBy1, multiplyBy2: nat
depth (pushMultiplicationInside' 0 e) =
depth (pushMultiplicationInside' multiplyBy2 e) symmetry.e: arith
multiplyBy1, multiplyBy2: nat
depth (pushMultiplicationInside' multiplyBy2 e) =
depth (pushMultiplicationInside' 0 e)

symmetry: When proving X ℛ Y, switch to proving Y ℛ X (here ℛ is =).

    apply depth_pushMultiplicationInside'_irrelevance0.
Qed.

Let's prove that pushing-inside has only a small effect on depth, considering for now only coefficient 0.

Lemma depth_pushMultiplicationInside' :
  forall e,
    depth (pushMultiplicationInside' 0 e) <= S (depth e).forall e : arith,
depth (pushMultiplicationInside' 0 e) <= S (depth e)
Proof.forall e : arith,
depth (pushMultiplicationInside' 0 e) <= S (depth e)
  induction e; simpl.n: nat
1 <= 2
x: var
2 <= 2
e1, e2: arith
IHe1: depth (pushMultiplicationInside' 0 e1) <=
S (depth e1)
IHe2: depth (pushMultiplicationInside' 0 e2) <=
S (depth e2)
S
  (max (depth (pushMultiplicationInside' 0 e1))
     (depth (pushMultiplicationInside' 0 e2))) <=
S (S (max (depth e1) (depth e2)))
e1, e2: arith
IHe1: depth (pushMultiplicationInside' 0 e1) <=
S (depth e1)
IHe2: depth (pushMultiplicationInside' 0 e2) <=
S (depth e2)
depth
  match isConst e1 with
  | Some k => pushMultiplicationInside' (k * 0) e2
  | None => Times (pushMultiplicationInside' 0 e1) e2
  end <= S (S (max (depth e1) (depth e2)))

  -n: nat
1 <= 2 lia.
  -x: var
2 <= 2 lia.
  -e1, e2: arith
IHe1: depth (pushMultiplicationInside' 0 e1) <=
S (depth e1)
IHe2: depth (pushMultiplicationInside' 0 e2) <=
S (depth e2)
S
  (max (depth (pushMultiplicationInside' 0 e1))
     (depth (pushMultiplicationInside' 0 e2))) <=
S (S (max (depth e1) (depth e2))) lia.
  -e1, e2: arith
IHe1: depth (pushMultiplicationInside' 0 e1) <=
S (depth e1)
IHe2: depth (pushMultiplicationInside' 0 e2) <=
S (depth e2)
depth
  match isConst e1 with
  | Some k => pushMultiplicationInside' (k * 0) e2
  | None => Times (pushMultiplicationInside' 0 e1) e2
  end <= S (S (max (depth e1) (depth e2))) destruct (isConst e1); simpl.e1, e2: arith
IHe1: depth (pushMultiplicationInside' 0 e1) <=
S (depth e1)
IHe2: depth (pushMultiplicationInside' 0 e2) <=
S (depth e2)
n: nat
depth (pushMultiplicationInside' (n * 0) e2) <=
S (S (max (depth e1) (depth e2)))
e1, e2: arith
IHe1: depth (pushMultiplicationInside' 0 e1) <=
S (depth e1)
IHe2: depth (pushMultiplicationInside' 0 e2) <=
S (depth e2)
S
  (max (depth (pushMultiplicationInside' 0 e1))
     (depth e2)) <= S (S (max (depth e1) (depth e2)))
    +e1, e2: arith
IHe1: depth (pushMultiplicationInside' 0 e1) <=
S (depth e1)
IHe2: depth (pushMultiplicationInside' 0 e2) <=
S (depth e2)
n: nat
depth (pushMultiplicationInside' (n * 0) e2) <=
S (S (max (depth e1) (depth e2))) rewrite mul_0_r.e1, e2: arith
IHe1: depth (pushMultiplicationInside' 0 e1) <=
S (depth e1)
IHe2: depth (pushMultiplicationInside' 0 e2) <=
S (depth e2)
n: nat
depth (pushMultiplicationInside' 0 e2) <=
S (S (max (depth e1) (depth e2)))
      lia.
    +e1, e2: arith
IHe1: depth (pushMultiplicationInside' 0 e1) <=
S (depth e1)
IHe2: depth (pushMultiplicationInside' 0 e2) <=
S (depth e2)
S
  (max (depth (pushMultiplicationInside' 0 e1))
     (depth e2)) <= S (S (max (depth e1) (depth e2))) lia.
Qed.

#[local] Hint Rewrite mul_0_r : arith.

Registering rewrite hints lets us use autorewrite to apply them for us automatically!

Lemma depth_pushMultiplicationInside'_snazzy :
  forall e,
    depth (pushMultiplicationInside' 0 e) <= S (depth e).forall e : arith,
depth (pushMultiplicationInside' 0 e) <= S (depth e)
Proof.forall e : arith,
depth (pushMultiplicationInside' 0 e) <= S (depth e)
  induction e; intros; simpl in *;
    try match goal with
      | [ |- context[match ?E with _ => _ end] ] =>
          destruct E; simpl; autorewrite with arith
      end; lia.
Qed.

Theorem depth_pushMultiplicationInside :
  forall e,
    depth (pushMultiplicationInside e) <= S (depth e).forall e : arith,
depth (pushMultiplicationInside e) <= S (depth e)
Proof.forall e : arith,
depth (pushMultiplicationInside e) <= S (depth e)
  intros.e: arith
depth (pushMultiplicationInside e) <= S (depth e)
  unfold pushMultiplicationInside.e: arith
depth (pushMultiplicationInside' 1 e) <= S (depth e)

unfold X: Replace X by its definition.

  rewrite depth_pushMultiplicationInside'_irrelevance0.e: arith
depth (pushMultiplicationInside' 0 e) <= S (depth e)
  apply depth_pushMultiplicationInside'.
Qed.

End ArithWithVariables.