# Commits

Working through Imp.v

# Imp.v

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