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 x_i, and plus:

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:

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

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 "x_i + (x_j + ... (x_n + 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:

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

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.

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.

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:

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).

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

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.

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.

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:

The expression standardize e is equivalent to e itself.

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.

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.

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.

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.

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.

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

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 x_n.

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

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

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:

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

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.