Commits

Konstantin Solomatov committed cad953e

Working through Imp.v

Comments (0)

Files changed (1)

 Qed.
 (** [] *)
 
-(** Kostik **)
-
 (** **** Exercise: 4 stars, optional (optimizer) *)
 (** _Design exercise_: The optimization implemented by our
     [optimize_0plus] function is only one of many imaginable
 
 (* FILL IN HERE *)
 *)
+
+Fixpoint const_calc_a (e : aexp) :=
+  match e with 
+  | ANum n => ANum n
+  | APlus e1 e2 => 
+    match APlus (const_calc_a e1) (const_calc_a e2) with
+    | APlus (ANum n1) (ANum n2) => ANum (n1 + n2)
+    | e => e
+    end
+  | AMinus e1 e2 => 
+    match AMinus (const_calc_a e1) (const_calc_a e2) with
+    | AMinus (ANum n1) (ANum n2) => ANum (n1 - n2)
+    | e => e
+    end
+  | AMult e1 e2 => 
+    match AMult (const_calc_a e1) (const_calc_a e2) with
+    | AMult (ANum n1) (ANum n2) => ANum (n1 * n2)
+    | e => e
+    end
+  end.
+
+Fixpoint const_calc_b (e : bexp) :=
+  match e with 
+  | BTrue => BTrue
+  | BFalse => BFalse
+  | BEq e1 e2 => 
+    match BEq (const_calc_a e1) (const_calc_a e2) with 
+    | BEq (ANum n1) (ANum n2) => if beq_nat n1 n2 then BTrue else BFalse
+    | e => e
+    end
+  | BLe e1 e2 => 
+    match BLe (const_calc_a e1) (const_calc_a e2) with
+    | BLe (ANum n1) (ANum n2) => if ble_nat n1 n2 then BTrue else BFalse
+    | e => e
+    end
+  | BNot e => 
+    match const_calc_b e with 
+    | BTrue => BFalse
+    | BFalse => BTrue
+    | ex => (BNot ex)
+    end
+  | BAnd e1 e2 => 
+    match BAnd (const_calc_b e1) (const_calc_b e2) with
+    | BAnd BTrue BTrue => BTrue
+    | BAnd BFalse _ => BFalse
+    | BAnd _ BFalse => BFalse 
+    | e => e
+    end
+  end.
+
+Theorem optimize_const_calc_sound_a: forall e,
+  aeval (const_calc_a e) = aeval e.
+Proof.
+  induction e; 
+    simpl; try (reflexivity); try (destruct (const_calc_a e1); destruct (const_calc_a e2));
+    simpl; rewrite <- IHe1; rewrite <- IHe2; simpl; reflexivity.
+Qed.
+
+Theorem optimize_const_calc_sound_b: forall e,
+  beval (const_calc_b e) = beval e.
+Proof.
+  assert (A1 : forall b, b && false = false). destruct b; reflexivity.
+  assert (A2 : forall a e, e = const_calc_a a -> aeval a = aeval e). intros a e H. rewrite H. simpl. symmetry. rewrite optimize_const_calc_sound_a. reflexivity.
+
+  induction e.
+  Case "BTrue". reflexivity.
+  Case "BFalse". reflexivity.
+  Case "BEq". 
+    simpl. remember (const_calc_a a) as ac. remember (const_calc_a a0) as ac0. 
+    destruct ac; destruct ac0; apply A2 in Heqac; apply A2 in Heqac0; rewrite Heqac; rewrite Heqac0; try (reflexivity); simpl. 
+    destruct (beq_nat n n0); reflexivity.
+  Case "BLe".
+    simpl. remember (const_calc_a a) as ac. remember (const_calc_a a0) as ac0. 
+    destruct ac; destruct ac0; apply A2 in Heqac; apply A2 in Heqac0; rewrite Heqac; rewrite Heqac0; try (reflexivity); simpl. 
+    destruct (ble_nat n n0); reflexivity.
+  Case "BNot". 
+    simpl. rewrite <- IHe. destruct (const_calc_b e); reflexivity.
+  Case "BAnd". 
+    simpl. rewrite <- IHe1. rewrite <- IHe2. 
+    destruct (const_calc_b e1); destruct (const_calc_b e2); try(reflexivity); simpl; rewrite A1; reflexivity.
+Qed.
+
 (** [] *)
 
 (* ####################################################### *)
 
     We'll see many examples of these in the proofs below. *)
 
+(** Kostik **)
+
 (* ####################################################### *)
 (** * Evaluation as a Relation *)