ソフトウェアの基礎 Imp_J.v 練習問題

sf_imp_optimize_0plus_b.v

(* **** Exercise: 3 stars (optimize_0plus_b) *)
(** **** 練習問題: ★★★ (optimize_0plus_b) *)
(* Since the [optimize_0plus] tranformation doesn't change the value
    of [aexp]s, we should be able to apply it to all the [aexp]s that
    appear in a [bexp] without changing the [bexp]'s value.  Write a
    function which performs that transformation on [bexp]s, and prove
    it is sound.  Use the tacticals we've just seen to make the proof
    as elegant as possible. *)
(** [optimize_0plus]の変換が[aexp]の値を変えないことから、
    [bexp]の値を変えずに、[bexp]に現れる[aexp]をすべて変換するために
    [optimize_0plus]が適用できるべきでしょう。
    [bexp]についてこの変換をする関数を記述しなさい。そして、
    それが健全であることを証明しなさい。
    ここまで見てきたタクティカルを使って証明を可能な限りエレガントにしなさい。*)

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.

Theorem optimize_0plus_b_sound : forall b, beval (optimize_0plus_b b) = beval b.
Proof.
 intro b. induction b.
  Case "BTrue".  reflexivity.
  Case "BFalse". reflexivity.
  Case "BEq". simpl. repeat rewrite optimize_0plus_sound. reflexivity.
  Case "BLe". simpl. repeat rewrite optimize_0plus_sound. reflexivity. 
  Case "BNot". simpl. rewrite IHb. reflexivity.
  Case "BAnd". simpl. rewrite IHb1,IHb2. reflexivity.
Qed.

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.
 intro b. bexp_cases (induction b) Case;
  try reflexivity;
  try (simpl; repeat rewrite optimize_0plus_sound; reflexivity);
  idtac.

  simpl. rewrite IHb. reflexivity.

  simpl. rewrite IHb1, IHb2. reflexivity.
Qed.