Simplifying Expressions

In this assignment we study simple integer expressions, and the rewriting of such expressions to normal form. To better understand the structure of the proofs, you can "mouse over" individual proof steps to see the state of the proof assistant after each step.

Expressions

We define the inductive type of integer expressions, Exp, which contains zero, variables xi, and plus:

Require Import Arith.

Inductive Exp : Set :=
| ezero : Exp
| evar : nat -> Exp
| eplus : Exp -> Exp -> Exp.

The expression "(x+0)+y" can be encoded in this type as (eplus (eplus (evar 0) ezero) (evar 1)).

We define the set of valuations (assigning integers to variables) as:

Definition Val := nat -> nat.

The interpretation function I computes the value of an integer expression under a valuation.

Fixpoint I (r: Val)(e:Exp): nat :=
match e with
| evar n => r n
| ezero => 0
| eplus e1 e2 => (I r e1) + (I r e2)
end.

Two expressions are said to be equivalent if they have the same interpretation under all valuations.

Normal Forms

One of the tasks of this assignment will be to rewrite expressions to normal form. We say that an expression is in standard form if it is of the form "xi + (xj + ... (xn + 0)...)".

An expression is in normal form if it is in standard form, and the variable indices i, j, ..., n are in non-decreasing order.

Assignment

The assignment consists of the following tasks:
• Prove that (eplus e1 e2) is equivalent to (eplus e2 e1), and that (eplus e ezero) is equivalent to e.
• Define inductive predicates Standard and Normal that hold for expressions of the correct form.
• Define functions standardize and normalize that rewrite expressions to standard and normal form, respectively.
• Prove that the results of standardize and normalize are of the correct form, and that the resulting expressions are equivalent to the original expressions.
• Using normalize, show that the expressions "(x + x) + (y + z)" and "(y + (x + 0)) + (z + x)" are equivalent.

Solution

Properties of eplus

First we prove two properties of eplus and I, using the corresponding properties of plus. We start with the commutativity of eplus:

Lemma eplus_comm : forall r e1 e2, I r (eplus e1 e2) = I r (eplus e2 e1).
Proof.
intros r e1 e2.

simpl.

apply plus_comm.

Qed.

And ezero is a right zero for eplus, again using a property of plus:

Lemma eplus_zero : forall r e, I r (eplus e ezero) = I r e.
Proof.
intros r e.

simpl.

apply plus_0_r.

Qed.

Predicates Standard and Normal

We want to express the property of being in standard or normal form using inductive predicates.

There are two ways to construct an expression in standard form: it can be zero, or it can consist of a single variable added to the front of another expression in standard form. Note that this is analogous to the structure of a Coq list.

Inductive Standard : Exp -> Prop :=
| st_ezero : Standard ezero
| st_eplus : forall e : Exp, forall n : nat, Standard e ->
Standard (eplus (evar n) e).

To construct an expression in normal form, we can have either zero, a single variable plus zero (the "base" case below), or a single variable added to the front of another expression in normal form. In the latter case, the index of the new variable must be less than or equal to the index of the leftmost variable in the previous expression, to ensure that the indices are non-decreasing.

Inductive Normal : Exp -> Prop :=
| norm_ezero : Normal ezero
| norm_base : forall n:nat, Normal (eplus (evar n) ezero)
| norm_eplus : forall e : Exp, forall (n m: nat),
Normal (eplus (evar m) e) -> n <= m ->
Normal (eplus (evar n) (eplus (evar m) e)).

We prove that any expression in normal form is also in standard form. The proof is by induction on the structure of the proof of Normal e:

Lemma Normal_Standard : forall e, Normal e -> Standard e.
Proof.
induction 1 as [ | | ? ? ? ? IH].

constructor.

repeat constructor.

constructor.

apply IH.

Qed.

Rewriting to Standard Form

We shall now study the transformation of expressions to standard form.

We first define a recursive helper function, flatten, that takes two arguments. The second argument, the expression f, is an accumulating parameter to which we add the variables from the expression e one by one, discarding occurrences of ezero. The idea is that if the second argument of flatten is in standard form, the result will also be in standard form (we prove this below).

Fixpoint flatten (e f:Exp) : Exp :=
match e with
| ezero => f
| evar n => eplus (evar n) f
| eplus e1 e2 => flatten e1 (flatten e2 f)
end.

To transform an expression into standard form, we flatten it, using ezero as the initial value of the accumulating parameter.

Definition standardize (e:Exp) : Exp := flatten e ezero.

An important property of flatten is that its result is in standard form, provided that the second argument is in standard form. The proof is by induction on the first argument e1.

Lemma flatten_Standard : forall e1 e2, Standard e2 -> Standard (flatten e1 e2).
Proof.
induction e1 as [ | | d1 IHd1 d2 IHd2]; intros.

simpl.
assumption.
constructor.
assumption.
simpl.

apply IHd1.

apply IHd2.

assumption.

Qed.

From the above lemma and the fact that ezero is in standard form, it follows that the result of standardize is always in standard form.

Theorem standardize_Standard : forall e, Standard (standardize e).
Proof.
intros.

unfold standardize.

apply flatten_Standard.

constructor.

Qed.

The previous two properties could be satisfied trivially by functions that always return ezero. Therefore, we also want to prove that the transformation functions produce expressions that are equivalent to the input expressions: the transformation should preserve the interpretation of expressions under all valuations.

In the case of flatten e1 e2, the variables in e1 are added in front of e2, so we require it to be equivalent to eplus e1 e2:

Lemma flatten_I : forall r e1 e2, I r (flatten e1 e2) = I r (eplus e1 e2).
Proof.
induction e1 as [ | | d1 IHd1 d2 IHd2 ]; intros; simpl; try reflexivity.

rewrite IHd1; simpl.

rewrite IHd2; simpl.

ring.

Qed.

The expression standardize e is equivalent to e itself.

Theorem standardize_I : forall r e, I r (standardize e) = I r e.
Proof.
intros.

unfold standardize.

rewrite flatten_I.

apply eplus_zero.

Qed.

Rewriting to Normal Form.

Now we turn to the transformation to normal form.

We define a helper function insert, which inserts a variable with index n at the correct position in an expression in normal form, preserving the ordering of the indices. If insert is applied to an expression that is not in standard form, the third branch of the match may be reached, producing ezero as a result.

Fixpoint insert (n : nat)(e : Exp) : Exp :=
match e with
| ezero => eplus (evar n) ezero
| eplus (evar m) f => if le_gt_dec n m
then eplus (evar n) e
else eplus (evar m) (insert n f)
| _ => ezero
end.

Arguably, it would be nicer to give insert a stronger type, expressing the condition that e is in standard form (or even normal form). However, since insert is used only as a helper function, on expressions that are in normal form by construction, it is simpler to use the "uninformative" type given above. We shall prove that insert has the correct behaviour in a separate lemma.

Next we define the function norm, which orders the variables of an expression in standard form by inserting them into the result expression one by one. This is analogous to insertion sort on lists. As before, norm does not behave correctly for input that is not in standard form.

Fixpoint norm (e : Exp) : Exp :=
match e with
| ezero => ezero
| eplus (evar n) f => insert n (norm f)
| _ => ezero
end.

To transform arbitrary expressions to normal form, we define normalize. This first standardizes its input and then sorts the result using norm. Unlike insert and norm, the function normalize has no implicit constraints on its input.

Definition normalize (e : Exp) : Exp := norm (standardize e).

We shall now prove that the three functions defined above lead to expressions in normal form that are equivalent to the input expressions.

First we prove that the insert function preserves the normalization of its argument. We have factored the recurring pattern "repeat constructor; auto with arith" out of the proof. This tactic is implied by the "..." following each destruct. The proof is by induction on the structure of the proof of Normal e; this leads to a shorter proof than induction on e itself.

Lemma insert_Normal : forall (n : nat) (e : Exp), Normal e -> Normal (insert n e).
Proof with repeat constructor; auto with arith.
induction 1 as [ | m | d m1 m2 ].

simpl.
constructor.
simpl.
destruct (le_gt_dec n m)...
simpl.
destruct (le_gt_dec n m1)...
simpl in *.

destruct (le_gt_dec n m2)...

Qed.

Note that the proof of the above lemma depends on the comparison operator le_gt_dec used in the definition of insert. As far as the computational behaviour of insert is concerned, we could just as well have used leb n m, which returns a boolean, to compare indices. However, in the above lemma, we must prove that the result is Normal, which requires proofs of n <= m for consecutive indices. When destructing leb n m we would not get proofs of these inequalities, so we would have to invoke additional lemmas to bring them into the proof context. Because we have instead defined insert with le_gt_dec, which gives not only the result of the comparison but also the corresponding proofs, lemma insert_Normal becomes simpler to prove.

The next lemma proves that the result of norm is in normal form if the input is in standard form. The proof is by induction on the proof of Standard e.

Lemma norm_Normal : forall e : Exp, Standard e -> Normal (norm e).
Proof.
induction 1.

simpl.
constructor.
simpl.
apply insert_Normal.
assumption.

Qed.

Finally, we use properties of standardize and norm to show that the result of normalize is always in normal form.

Theorem normalize_Normal : forall e : Exp, Normal (normalize e).
Proof.
intros.

unfold normalize.

apply norm_Normal.

apply standardize_Standard.

Qed.

Like we did for the transformation to standard form, we shall prove that the normalization functions produce results that are equivalent to the input.

For insert, the interpretation of the resulting expression is equal to the interpretation of the original expression e plus the value of the variable xn.

Lemma insert_I : forall r n e, Standard e -> I r (insert n e) = r n + I r e.
Proof.
induction 1 as [ | d m Std_d IH].

trivial.

simpl; destruct (le_gt_dec n m).

trivial.

simpl; rewrite IH.

ring.

Qed.

For norm, the resulting expression is equivalent to the input expression. The proof is by induction on the "list structure" of expression e.

Lemma norm_I : forall r e, Standard e -> I r (norm e) = I r e.
Proof.
induction 1 as [ | d m Std_d IH].

trivial.

simpl; rewrite insert_I.

rewrite IH.

trivial.

apply Normal_Standard.

apply norm_Normal.

assumption.

Qed.

Finally, because both norm and standardize preserve the interpretation of their input, so does normalize.

Theorem normalize_I : forall r e, I r (normalize e) = I r e.
Proof.
intros r e.

unfold normalize.

rewrite norm_I.

rewrite standardize_I.

trivial.

apply standardize_Standard.

Qed.

Using normalize to prove equivalence.

We can use the normalization function defined in the previous section to prove the equivalence of expressions such as ((x + x) + (y + z)) and ((y + (x + 0)) + (z + x)).

The two terms above can be encoded as:

Definition term1 := eplus (eplus (evar 0) (evar 0)) (eplus (evar 1) (evar 2)).
Definition term2 := eplus (eplus (evar 1) (eplus (evar 0) ezero)) (eplus (evar 2) (evar 0)).

A simple proof of the equivalence makes use of the automated tactic ring:

Lemma equiv1: forall r, I r term1 = I r term2.
Proof.
intro r.

simpl.

ring.

Qed.

In the final step of this proof, ring uses commutativity and associativity laws for "+" behind the scenes to rewrite both sides of the equality to normal form. When these normal forms turn out to be the same, the equality is trivial.

Using this same technique at the level of Exp instead of nat enables us to prove the lemma without resorting to ring. By theorem normalize_I, we are allowed to normalize terms under the interpretation function. We rewrite both sides of the equality to normalize the terms and then apply simpl to perform computation. Because both terms have the same normal form, this leads to an equality that can be proved by reflexivity.

Lemma equiv2: forall r, I r term1 = I r term2.
Proof.
intro r.

rewrite <- normalize_I.

rewrite <- normalize_I with (e:=term2).

simpl.

reflexivity.

Qed.