Merge pull request #499 from chdoc/contra-prop

contra lemmas involving propositions

3 files changed, 53 insertions, 1 deletions

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 13e1d1b..415fc10 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -10,6 +10,8 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
 
 ### Added
 
+- Added contrapostion lemmas involving propositions: `contra_not`, `contraPnot`, `contraTnot`, `contraNnot`, `contraPT`, `contra_notT`, `contra_notN`, `contraPN`, `contraFnot`, `contraPF` and `contra_notF` in ssrbool.v and `contraPeq`, `contra_not_eq`, `contraPneq`, and `contra_neq_not` in eqtype.v
+
 ### Changed
 
 ### Renamed
diff --git a/mathcomp/ssreflect/eqtype.v b/mathcomp/ssreflect/eqtype.v
index bd58e01..1391b5b 100644
--- a/mathcomp/ssreflect/eqtype.v
+++ b/mathcomp/ssreflect/eqtype.v
@@ -208,7 +208,7 @@ Arguments eqVneq {T} x y, {T x y}.
 Section Contrapositives.
 
 Variables (T1 T2 : eqType).
-Implicit Types (A : pred T1) (b : bool) (x : T1) (z : T2).
+Implicit Types (A : pred T1) (b : bool) (P : Prop) (x : T1) (z : T2).
 
 Lemma contraTeq b x y : (x != y -> ~~ b) -> b -> x = y.
 Proof. by move=> imp hyp; apply/eqP; apply: contraTT hyp. Qed.
@@ -219,6 +219,12 @@ Proof. by move=> imp hyp; apply/eqP; apply: contraNT hyp. Qed.
 Lemma contraFeq b x y : (x != y -> b) -> b = false -> x = y.
 Proof. by move=> imp /negbT; apply: contraNeq. Qed.
 
+Lemma contraPeq P x y : (x != y -> ~ P) -> P -> x = y.
+Proof. by move => imp HP; apply: contraTeq isT => /imp /(_ HP). Qed.
+
+Lemma contra_not_eq P x y : (x != y -> P) -> ~ P -> x = y.
+Proof. by move => imp; apply: contraPeq => /imp HP /(_ HP). Qed.
+
 Lemma contraTneq b x y : (x = y -> ~~ b) -> b -> x != y.
 Proof. by move=> imp; apply: contraTN => /eqP. Qed.
 
@@ -228,6 +234,9 @@ Proof. by move=> imp; apply: contraNN => /eqP. Qed.
 Lemma contraFneq b x y : (x = y -> b) -> b = false -> x != y.
 Proof. by move=> imp /negbT; apply: contraNneq. Qed.
 
+Lemma contraPneq P x y : (x = y -> ~ P) -> P -> x != y.
+Proof. by move => imp; apply: contraPN => /eqP. Qed.
+
 Lemma contra_eqN b x y : (b -> x != y) -> x = y -> ~~ b.
 Proof. by move=> imp /eqP; apply: contraL. Qed.
 
@@ -246,6 +255,9 @@ Proof. by move=> imp; apply: contraNF => /imp->. Qed.
 Lemma contra_neqT b x y : (~~ b -> x = y) -> x != y -> b.
 Proof. by move=> imp; apply: contraNT => /imp->. Qed.
 
+Lemma contra_neq_not P x y : (P -> x = y) -> x != y -> ~ P.
+Proof. by move => imp;apply: contraNnot => /imp->. Qed.
+
 Lemma contra_eq z1 z2 x1 x2 : (x1 != x2 -> z1 != z2) -> z1 = z2 -> x1 = x2.
 Proof. by move=> imp /eqP; apply: contraTeq. Qed.
 
diff --git a/mathcomp/ssreflect/ssrbool.v b/mathcomp/ssreflect/ssrbool.v
index b1498cd..892705b 100644
--- a/mathcomp/ssreflect/ssrbool.v
+++ b/mathcomp/ssreflect/ssrbool.v
@@ -202,3 +202,41 @@ 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.
+