第33回 #ProofCafe での練習問題のssreflectを使った解答例。
第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/
Author And Source
この問題について(第33回 #ProofCafe での練習問題のssreflectを使った解答例。), 我々は、より多くの情報をここで見つけました https://qiita.com/yoshihiro503/items/0bca75e5ab52e40f01f6著者帰属:元の著者の情報は、元のURLに含まれています。著作権は原作者に属する。
Content is automatically searched and collected through network algorithms . If there is a violation . Please contact us . We will adjust (correct author information ,or delete content ) as soon as possible .