Skip to content

Instantly share code, notes, and snippets.

@yoshihiro503

yoshihiro503/contrapositive_bool.v

Created September 25, 2022 11:55
Show Gist options
  • Save yoshihiro503/bc7229f5d4792249055da01a346b7444 to your computer and use it in GitHub Desktop.
Save yoshihiro503/bc7229f5d4792249055da01a346b7444 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
contrapositive_bool.v
Theorem contrapositive_bool : forall (p q : bool),
(p = true -> q = true) -> (q = false -> p = false).
Proof.
intros p q H Hq.
destruct p. (* pで場合分け*)
- (* pがtrueのとき *)
rewrite H in Hq.
+ discriminate Hq.
+ reflexivity.
- (* pがfalseのとき*)
reflexivity.
Qed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment