第33回 #ProofCafe での練習問題のssreflectを使った解答例。 #Coq

第33回 #ProofCafe での練習問題のssreflectを使った解答例。

Equiv_J.v

Require Import ssreflect.
(* **** Exercise: 3 stars (swap_if_branches) *)
(** **** 練習問題: ★★★ (swap_if_branches) *)
Theorem swap_if_branches: forall b e1 e2,
  cequiv
    (IFB b THEN e1 ELSE e2 FI)
    (IFB BNot b THEN e2 ELSE e1 FI).
Proof.
  move => b e1 e2.
  split => H.
  - inversion H; subst.
    + by apply E_IfFalse; [simpl; rewrite H5 |].
    + by apply E_IfTrue;  [simpl; rewrite H5 |].
  - inversion H; subst.
    + apply E_IfFalse; [| assumption].
      rewrite  (negb_involutive_reverse (beval st b)).
      simpl in H5. by rewrite H5.
    + apply E_IfTrue; [| assumption].
      rewrite (negb_involutive_reverse (beval st b)).
      simpl in H5. by rewrite H5.
Qed.

ProofCafe: http://proofcafe.org/wiki/