(* NB: coqdoc begin/end hide does not work well in combination with proviola... *)
(** * 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.
(* intros e H.
induction H.
constructor.
repeat constructor.
constructor.
apply IHNormal. *)
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 (* will not happen if e is in Standard form *)
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 [list]s. 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 (* will not happen if e is in Standard form *)
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))#. *)
Variable x y z :nat.
(**
A simple proof of the equivalence makes use of the automated tactic [ring]:
*)
Lemma equiv1: (x + x) + (y + z) = y + (x + 0) + (z + x).
Proof.
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.
*)
(** The two terms above #((x + x) + (y + z))# and
#((y + (x + 0)) + (z + x))# 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)).
(** We define a valuation that sends the appropriate indices to x, y and z *)
Definition rho : Val := fun n: nat =>
match n with
| 0 => x
| 1 => y
| 2 => z
| _ => 0
end.
Lemma equiv2 : (x + x) + (y + z) = y + (x + 0) + (z + x).
Proof.
change (I rho term1 = I rho term2).
rewrite <- (normalize_I rho term1).
(* Also rewrite <- normalize_I. works *)
rewrite <- (normalize_I rho term2).
simpl.
reflexivity.
Qed.
(* NB: a final coqdoc comment block is required to prevent "This page has been generated by
coqdoc" appearing below the final prover output frame *)
(** *)