(*|
============================
Week 1: Basic Program Syntax
============================
Author
`Adam Chlipala `__, with modifications by CS-428 staff.
License
No redistribution allowed (usage by permission in CS-428).
.. contents::
.. coq:: none
|*)
From Coq Require Import Arith Lia String.
Open Scope string_scope.
Import Nat.
(*|
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)).
(*|
.. sidebar:: Notations
We can make this expression more readable using `notations `__.
There are two ways to do this:
1. The simplest way allows us to freely mix our own syntax with Coq's usual syntax:
.. coq::
|*)
Module SimpleNotations. (* .none *)
Notation "'$' n" := (Const n)
(at level 1, format "'$' n").
Infix "+" := Plus.
Infix "*" := Times.
Print ex2. (* .unfold *)
End SimpleNotations. (* .none *)
(*|
2. More elaborate, but also more powerful, are “custom entries”, which let us define our own mini-language betweeen custom delimiters.
Here, we use ``« … »``.
|*)
Module CustomNotations. (* .none *)
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. (* .unfold *)
End CustomNotations. (* .none *)
(*|
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. (* .unfold *)
Compute eval ex2. (* .unfold *)
(*|
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. (* .unfold *)
Compute size ex2. (* .unfold *)
(*|
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. (* .unfold *)
Compute depth ex2. (* .unfold *)
(*|
Proofs by induction
-------------------
Our first proof!
Size is an upper bound on depth:
|*)
Theorem depth_le_size : forall e,
depth e <= size e.
Proof.
(*|
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.
(*|
`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 *) (* .unfold *)
simpl. (* .unfold *)
(*|
`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.
.. coq::
|*)
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.)
.. coq::
|*)
- (* Plus case *) (* .unfold *)
simpl. (* .unfold *)
lia.
- (* Times *) (* .unfold *)
simpl.
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.
Proof.
induction e. (* .unfold *)
all: simpl. (* .unfold *)
all: lia.
Qed.
(*|
Or even better, look at that!
|*)
Theorem depth_le_size_super_snazzy : forall e,
depth e <= size e.
Proof.
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. (* .unfold *)
Compute commuter ex1. (* .unfold *)
Print ex2. (* .unfold *)
Compute commuter ex2. (* .unfold *)
(*|
`commuter` has all the appropriate interactions with other functions (and itself).
|*)
Theorem commuter_correct : forall e,
eval (commuter e) = eval e.
Proof.
induction e; simpl; lia.
Qed.
Theorem size_commuter : forall e,
size (commuter e) = size e.
Proof.
induction e; simpl; lia.
Qed.
Theorem depth_commuter : forall e,
depth (commuter e) = depth e.
Proof.
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.
Proof.
induction e; simpl. (* .unfold *)
(*|
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.
.. coq::
|*)
Qed.
(*|
.. exercise:: Working without `lia`
:difficulty: 1
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.
Proof.
induction e; simpl. (* .unfold *)
(*|
.. solution::
We need three new ingredients:
- A tactic to solve a goal of the form ``a == a``:
.. coq::
|*)
- reflexivity.
(*|
- A theorem to rewrite `a + b`:
.. coq:: unfold
|*)
- (* Plus *)
rewrite Nat.add_comm.
rewrite IHe1.
rewrite IHe2.
reflexivity.
(*|
- A theorem to rewrite `a * b`:
.. coq:: unfold
|*)
- (* Times *)
rewrite Nat.mul_comm.
rewrite IHe1.
rewrite IHe2.
reflexivity.
Qed.
(*|
Here is a more succinct way to write this:
|*)
Theorem commuter_correct_shorter : forall e,
eval (commuter e) = eval e.
Proof.
induction e; simpl.
2: rewrite Nat.add_comm.
3: rewrite Nat.mul_comm.
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.
Proof.
induction e; simpl.
all: try match goal with
| [ |- context[_ + _] ] => rewrite Nat.add_comm
| [ |- context[_ * _] ] => rewrite Nat.mul_comm
end.
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 `string`\s, 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". (* .unfold *)
Compute eval val0 ex2. (* .unfold *)
(*|
… but we can also pass a more complex function:
|*)
Compute eval
(fun v => match v with
| "x" => 2
| "y" => 3
| _ => 0
end)
ex2.
(*|
.. sidebar:: Computing with open terms
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. (* .unfold *)
(*|
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")). (* .unfold *)
(*|
.. massert::
.s(Compute).msg(?vn)
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. (* .unfold *)
Compute size ex2. (* .unfold *)
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. (* .unfold *)
Compute depth ex2. (* .unfold *)
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. (* .unfold *)
Compute commuter ex2. (* .unfold *)
(*|
Due to the automation, the proofs are unchanged:
|*)
Theorem depth_le_size : forall e,
depth e <= size e.
Proof.
induction e; simpl; lia.
Qed.
Theorem commuter_correct : forall vn e,
eval vn (commuter e) = eval vn e.
Proof.
induction e; simpl; lia.
Qed.
Theorem size_commuter : forall e,
size (commuter e) = size e.
Proof.
induction e; simpl; lia.
Qed.
Theorem depth_commuter : forall e,
depth (commuter e) = depth e.
Proof.
induction e; simpl; lia.
Qed.
Theorem commuter_involutive : forall e,
commuter (commuter e) = e.
Proof.
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).
(*|
.. coq:: none
|*)
(* Some magic to make the output of `string_dec` more readable. *)
Notation yes := (left _).
Notation no := (right _).
(*|
.. coq:: unfold
|*)
Compute "x" == "x".
Compute "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.
Proof.
induction inThis; simpl.
- lia.
- (* Var *) (* .unfold *)
destruct (x == replaceThis); simpl.
(*|
`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.
.. coq::
|*)
+ (* = case *) (* .unfold *)
lia.
+ (* ≠ case *) (* .unfold *)
lia.
- lia.
- 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.
Proof.
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.
Proof.
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).
Proof.
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.
Proof.
induction e; simpl;
repeat match goal with
| [ |- context[match ?E with _ => _ end] ] =>
destruct E; simpl in *
end; lia.
Qed.
(*|
.. sidebar:: Transitivity and homogeneity
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.
Proof.
induction e; simpl; try lia.
- (* Plus *) (* .unfold *)
(*|
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. (* -.g#* .g#1 .unfold *)
(*|
(… 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.
Proof.
induction e; simpl; try lia.
- (* Plus *) (* .unfold *)
(*|
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))). (* .unfold *)
(*|
`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.
|*)
+ destruct (constantFold e1), (constantFold e2).
all: try destruct n; simpl.
all: lia.
+ lia.
- transitivity (S (size (constantFold e1) + size (constantFold e2))).
+ destruct (constantFold e1), (constantFold e2).
all: try destruct n; simpl.
all: try destruct n; simpl.
all: lia.
+ lia.
Qed.
(*|
The same principle applies for `eval`:
|*)
Theorem eval_constantFold : forall (vn: val) (e: arith),
eval vn (constantFold e) = eval vn e.
Proof.
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).
Proof.
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
:difficulty: 1
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.
(*|
.. solution::
.. coq::
|*)
Proof.
induction e; simpl.
- congruence.
- congruence.
- rewrite <- IHe1, <- IHe2.
destruct (constantFold e1), (constantFold e2).
all: try destruct n; simpl.
all: lia.
- rewrite <- IHe1, <- IHe2.
destruct (constantFold e1), (constantFold e2).
all: try destruct n; simpl.
all: try destruct n; simpl.
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).
Proof.
induction e; intros; simpl in *.
- lia.
- lia.
- (* Plus *) (* .unfold *)
rewrite IHe1. (* .unfold *)
(*|
`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`.
.. coq::
|*)
rewrite IHe2.
lia.
- destruct (isConst e1); simpl.
+ rewrite IHe2. (* .unfold *)
(*|
Neither `lia` nor `congruence` is powerful enough on its own here,
so we use a separate lemma to simplify `n * 0`:
|*)
Search (_ * 0 = 0). (* .unfold *)
rewrite mul_0_r.
lia.
+ rewrite IHe1.
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).
Proof.
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).
Proof.
intros.
transitivity (depth (pushMultiplicationInside' 0 e)). (* .unfold *)
- apply depth_pushMultiplicationInside'_irrelevance0. (* .unfold *)
(*|
`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.
.. coq::
|*)
- symmetry. (* .unfold *)
(*|
`symmetry`
When proving `X ℛ Y`, switch to proving `Y ℛ X` (here `ℛ` is `=`).
.. coq::
|*)
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).
Proof.
induction e; simpl.
- lia.
- lia.
- lia.
- destruct (isConst e1); simpl.
+ rewrite mul_0_r.
lia.
+ 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).
Proof.
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).
Proof.
intros.
unfold pushMultiplicationInside. (* .unfold *)
(*|
`unfold X`
Replace `X` by its definition.
.. coq::
|*)
rewrite depth_pushMultiplicationInside'_irrelevance0.
apply depth_pushMultiplicationInside'.
Qed.
End ArithWithVariables.
(*|
.. coq:: none
|*)
(* Local Variables: *)
(* coq-indent-modulestart: 0 *)
(* End: *)