optimize_bexp_0plus.v

(* **** Exercise: 3 stars (optimize_0plus_b) *)
(** **** 練習問題: ★★★ (optimize_0plus_b) *)
Fixpoint optimize_bexp_0plus (e: bexp) : bexp :=
  match e with
  | BTrue => BTrue
  | BFalse => BFalse
  | BEq a1 a2 => BEq (optimize_0plus a1) (optimize_0plus a2)
  | BLe a1 a2 => BLe (optimize_0plus a1) (optimize_0plus a2)
  | BNot b => BNot (optimize_bexp_0plus b)
  | BAnd b1 b2 => BAnd (optimize_bexp_0plus b1) (optimize_bexp_0plus b2)
  end.

Theorem optimize_bexp_0plus_sound: forall e,
  beval (optimize_bexp_0plus e) = beval e.
Proof.
  intros e. induction e; 
    try reflexivity; 
    try(unfold optimize_bexp_0plus; simpl;
        repeat (rewrite optimize_0plus_sound); reflexivity);
    try simpl.
  rewrite IHe. reflexivity.
  rewrite IHe1. rewrite IHe2. reflexivity.
Qed.    
(** [] *)