(* The following definition applies optimize_0plus to Boolean expressions. *) Fixpoint optimize_0plus_b (b : bexp) : bexp := match b 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 b1 => BNot (optimize_0plus_b b1) | BAnd b1 b2 => BAnd (optimize_0plus_b b1) (optimize_0plus_b b2) end. Tactic Notation "bexp_cases" tactic(first) ident(c) := first; [ Case_aux c "BTrue" | Case_aux c "BFalse" | Case_aux c "BEq" | Case_aux c "BLe" | Case_aux c "BNot" | Case_aux c "BAnd" ]. Theorem optimize_0plus_b_sound : forall b, beval (optimize_0plus_b b) = beval b. Proof. Admitted. Theorem update_neq : forall V2 V1 n st, beq_id V2 V1 = false -> (update st V2 n) V1 = (st V1). Proof. Admitted. Theorem update_shadow : forall x1 x2 k1 k2 (f : state), (update (update f k2 x1) k2 x2) k1 = (update f k2 x2) k1. Proof. Admitted. Theorem update_permute : forall x1 x2 k1 k2 k3 f, beq_id k2 k1 = false -> (update (update f k2 x1) k1 x2) k3 = (update (update f k1 x2) k2 x1) k3. Proof. Admitted.