More than 5 years have passed since last update.
第33回 #ProofCafe での練習問題のssreflectを使った解答例。
Equiv_J.v
RequireImportssreflect.(* **** Exercise: 3 stars (swap_if_branches) *)(** **** 練習問題: ★★★ (swap_if_branches) *)Theoremswap_if_branches:forallbe1e2,cequiv(IFBbTHENe1ELSEe2FI)(IFBBNotbTHENe2ELSEe1FI).Proof.move=>be1e2.split=>H.-inversionH;subst.+byapplyE_IfFalse;[simpl;rewriteH5|].+byapplyE_IfTrue;[simpl;rewriteH5|].-inversionH;subst.+applyE_IfFalse;[|assumption].rewrite(negb_involutive_reverse(bevalstb)).simplinH5.byrewriteH5.+applyE_IfTrue;[|assumption].rewrite(negb_involutive_reverse(bevalstb)).simplinH5.byrewriteH5.Qed.ProofCafe: http://proofcafe.org/wiki/
Register as a new user and use Qiita more conveniently
- You get articles that match your needs
- You can efficiently read back useful information
- You can use dark theme