(* 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 *) (** *)