add contra lemmas introduced by MathComp's PR #499

(https://github.com/math-comp/math-comp/pull/499/)

1 files changed, 37 insertions, 0 deletions

diff --git a/theories/ssr/ssrbool.v b/theories/ssr/ssrbool.v
index 701b604637..8c881b1f89 100644
--- a/theories/ssr/ssrbool.v
+++ b/theories/ssr/ssrbool.v
@@ -2132,3 +2132,40 @@ End inj_can_sym_in_on.
 Arguments inj_can_sym_in_on {aT rT aD rD f g}.
 Arguments inj_can_sym_on {aT rT aD f g}.
 Arguments inj_can_sym_in {aT rT rD f g}.
+
+(* additional contra lemmas involving [P,Q : Prop] *)
+
+Section Contra.
+Implicit Types (P Q : Prop) (b : bool).
+
+Lemma contra_not P Q : (Q -> P) -> (~ P -> ~ Q). Proof. by auto. Qed.
+
+Lemma contraPnot P Q : (Q -> ~ P) -> (P -> ~ Q). Proof. by auto. Qed.
+
+Lemma contraTnot b P : (P -> ~~ b) -> (b -> ~ P).
+Proof. by case: b; auto. Qed.
+
+Lemma contraNnot P b : (P -> b) -> (~~ b -> ~ P).
+Proof. rewrite -{1}[b]negbK; exact: contraTnot. Qed.
+
+Lemma contraPT P b : (~~ b -> ~ P) -> P -> b.
+Proof. by case: b => //= /(_ isT) nP /nP. Qed.
+
+Lemma contra_notT P b : (~~ b -> P) -> ~ P -> b.
+Proof. by case: b => //= /(_ isT) HP /(_ HP). Qed.
+
+Lemma contra_notN P b : (b -> P) -> ~ P -> ~~ b.
+Proof. rewrite -{1}[b]negbK; exact: contra_notT. Qed.
+
+Lemma contraPN P b : (b -> ~ P) -> (P -> ~~ b).
+Proof. by case: b => //=; move/(_ isT) => HP /HP. Qed.
+
+Lemma contraFnot P b : (P -> b) -> b = false -> ~ P.
+Proof. by case: b => //; auto. Qed.
+
+Lemma contraPF P b : (b -> ~ P) -> P -> b = false.
+Proof. by case: b => // /(_ isT). Qed.
+
+Lemma contra_notF P b : (b -> P) -> ~ P -> b = false.
+Proof. by case: b => // /(_ isT). Qed.
+End Contra.