Merge pull request #578 from CohenCyril/contra_le

Adding contra lemmas with orders

3 files changed, 262 insertions, 1 deletions

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index be208bb..9108947 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -10,7 +10,25 @@ 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
+- Added contraposition 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
+- Contraposition lemmas involving inequalities:
+  + in `order.v`:
+    `comparable_contraTle`, `comparable_contraTlt`, `comparable_contraNle`, `comparable_contraNlt`, `comparable_contraFle`, `comparable_contraFlt`,
+    `contra_leT`, `contra_ltT`, `contra_leN`, `contra_ltN`, `contra_leF`, `contra_ltF`,
+    `comparable_contra_leq_le`, `comparable_contra_leq_lt`, `comparable_contra_ltn_le`, `comparable_contra_ltn_lt`,
+    `contra_le_leq`, `contra_le_ltn`, `contra_lt_leq`, `contra_lt_ltn`,
+    `comparable_contra_le`, `comparable_contra_le_lt`, `comparable_contra_lt_le`, `comparable_contra_lt`,
+    `contraTle`, `contraTlt`, `contraNle`, `contraNlt`, `contraFle`, `contraFlt`,
+    `contra_leq_le`, `contra_leq_lt`, `contra_ltn_le`, `contra_ltn_lt`,
+    `contra_le`, `contra_le_lt`, `contra_lt_le`, `contra_lt`,
+    `contra_le_not`, `contra_lt_not`,
+    `comparable_contraPle`, `comparable_contraPlt`, `comparable_contra_not_le`, `comparable_contra_not_lt`,
+    `contraPle`, `contraPlt`, `contra_not_le`, `contra_not_lt`
+  + in `ssrnat.v`:
+    `contraTleq`, `contraTltn`, `contraNleq`, `contraNltn`, `contraFleq`, `contraFltn`,
+    `contra_leqT`, `contra_ltnT`, `contra_leqN`, `contra_ltnN`, `contra_leqF`, `contra_ltnF`,
+    `contra_leq`, `contra_ltn`, `contra_leq_ltn`, `contra_ltn_leq`,
+    `contraPleq`, `contraPltn`, `contra_not_leq`, `contra_not_ltn`, `contra_leq_not`, `contra_ltn_not`
 - in `ssralg.v`, new lemma `sumr_const_nat` and `iter_addr_0`
 - in `ssrnum.v`, new lemma `ler_sum_nat`
 
diff --git a/mathcomp/ssreflect/order.v b/mathcomp/ssreflect/order.v
index cd54fd3..846885e 100644
--- a/mathcomp/ssreflect/order.v
+++ b/mathcomp/ssreflect/order.v
@@ -3130,6 +3130,111 @@ Lemma nmono_leif (f : T -> T) C :
 Proof. by move=> mf x y; rewrite /leif !eq_le !mf. Qed.
 
 End POrderTheory.
+
+Section ContraTheory.
+Context {disp1 disp2 : unit} {T1 : porderType disp1} {T2 : porderType disp2}.
+Implicit Types (x y : T1) (z t : T2) (b : bool) (m n : nat) (P : Prop).
+
+Lemma comparable_contraTle b x y : x >=< y -> (y < x -> ~~ b) -> (b -> x <= y).
+Proof. by case: comparableP; case: b. Qed.
+
+Lemma comparable_contraTlt b x y : x >=< y -> (y <= x -> ~~ b) -> (b -> x < y).
+Proof. by case: comparableP; case: b. Qed.
+
+Lemma comparable_contraPle P x y : x >=< y -> (y < x -> ~ P) -> (P -> x <= y).
+Proof. by case: comparableP => // _ _ /(_ isT). Qed.
+
+Lemma comparable_contraPlt P x y : x >=< y -> (y <= x -> ~ P) -> (P -> x < y).
+Proof. by case: comparableP => // _ _ /(_ isT). Qed.
+
+Lemma comparable_contraNle b x y : x >=< y -> (y < x -> b) -> (~~ b -> x <= y).
+Proof. by case: comparableP; case: b. Qed.
+
+Lemma comparable_contraNlt b x y : x >=< y -> (y <= x -> b) -> (~~ b -> x < y).
+Proof. by case: comparableP; case: b. Qed.
+
+Lemma comparable_contra_not_le P x y : x >=< y -> (y < x -> P) -> (~ P -> x <= y).
+Proof. by case: comparableP => // _ _ /(_ isT). Qed.
+
+Lemma comparable_contra_not_lt P x y : x >=< y -> (y <= x -> P) -> (~ P -> x < y).
+Proof. by case: comparableP => // _ _ /(_ isT). Qed.
+
+Lemma comparable_contraFle b x y : x >=< y -> (y < x -> b) -> (b = false -> x <= y).
+Proof. by case: comparableP; case: b => // _ _ /implyP. Qed.
+
+Lemma comparable_contraFlt b x y : x >=< y -> (y <= x -> b) -> (b = false -> x < y).
+Proof. by case: comparableP; case: b => // _ _ /implyP. Qed.
+
+Lemma contra_leT b x y : (~~ b -> x < y) -> (y <= x -> b).
+Proof. by case: comparableP; case: b. Qed.
+
+Lemma contra_ltT b x y : (~~ b -> x <= y) -> (y < x -> b).
+Proof. by case: comparableP; case: b. Qed.
+
+Lemma contra_leN b x y : (b -> x < y) -> (y <= x -> ~~ b).
+Proof. by case: comparableP; case: b. Qed.
+
+Lemma contra_ltN b x y : (b -> x <= y) -> (y < x -> ~~ b).
+Proof. by case: comparableP; case: b. Qed.
+
+Lemma contra_le_not P x y : (P -> x < y) -> (y <= x -> ~ P).
+Proof. by case: comparableP => // _ PF _ /PF. Qed.
+
+Lemma contra_lt_not P x y : (P -> x <= y) -> (y < x -> ~ P).
+Proof. by case: comparableP => // _ PF _ /PF. Qed.
+
+Lemma contra_leF b x y : (b -> x < y) -> (y <= x -> b = false).
+Proof. by case: comparableP; case: b => // _ /implyP. Qed.
+
+Lemma contra_ltF b x y : (b -> x <= y) -> (y < x -> b = false).
+Proof. by case: comparableP; case: b => // _ /implyP. Qed.
+
+Lemma comparable_contra_leq_le m n x y : x >=< y ->
+  (y < x -> (n < m)%N) -> ((m <= n)%N -> x <= y).
+Proof. by case: comparableP; case: ltngtP. Qed.
+
+Lemma comparable_contra_leq_lt m n x y : x >=< y ->
+  (y <= x -> (n < m)%N) -> ((m <= n)%N -> x < y).
+Proof. by case: comparableP; case: ltngtP. Qed.
+
+Lemma comparable_contra_ltn_le m n x y : x >=< y ->
+  (y < x -> (n <= m)%N) -> ((m < n)%N -> x <= y).
+Proof. by case: comparableP; case: ltngtP. Qed.
+
+Lemma comparable_contra_ltn_lt m n x y : x >=< y ->
+  (y <= x -> (n <= m)%N) -> ((m < n)%N -> x < y).
+Proof. by case: comparableP; case: ltngtP. Qed.
+
+Lemma contra_le_leq x y m n : ((n < m)%N -> y < x) -> (x <= y -> (m <= n)%N).
+Proof. by case: comparableP; case: ltngtP. Qed.
+
+Lemma contra_le_ltn x y m n : ((n <= m)%N -> y < x) -> (x <= y -> (m < n)%N).
+Proof. by case: comparableP; case: ltngtP. Qed.
+
+Lemma contra_lt_leq x y m n : ((n < m)%N -> y <= x) -> (x < y -> (m <= n)%N).
+Proof. by case: comparableP; case: ltngtP. Qed.
+
+Lemma contra_lt_ltn x y m n : ((n <= m)%N -> y <= x) -> (x < y -> (m < n)%N).
+Proof. by case: comparableP; case: ltngtP. Qed.
+
+Lemma comparable_contra_le x y z t : z >=< t ->
+  (t < z -> y < x) -> (x <= y -> z <= t).
+Proof. by do 2![case: comparableP => //= ?]. Qed.
+
+Lemma comparable_contra_le_lt x y z t : z >=< t ->
+  (t <= z -> y < x) -> (x <= y -> z < t).
+Proof. by do 2![case: comparableP => //= ?]. Qed.
+
+Lemma comparable_contra_lt_le x y z t : z >=< t ->
+  (t < z -> y <= x) -> (x < y -> z <= t).
+Proof. by do 2![case: comparableP => //= ?]. Qed.
+
+Lemma comparable_contra_lt x y z t : z >=< t ->
+ (t <= z -> y <= x) -> (x < y -> z < t).
+Proof. by do 2![case: comparableP => //= ?]. Qed.
+
+End ContraTheory.
+
 Section POrderMonotonyTheory.
 
 Context {disp disp' : unit}.
@@ -3695,9 +3800,76 @@ End ArgExtremum.
 
 End TotalTheory.
 
+Hint Resolve le_total : core.
+Hint Resolve ge_total : core.
+Hint Resolve comparableT : core.
+Hint Resolve sort_le_sorted : core.
+
 Arguments min_idPr {disp T x y}.
 Arguments max_idPl {disp T x y}.
 
+(* contra lemmas *)
+
+Section ContraTheory.
+Context {disp1 disp2 : unit} {T1 : porderType disp1} {T2 : orderType disp2}.
+Implicit Types (x y : T1) (z t : T2) (b : bool) (m n : nat) (P : Prop).
+
+Lemma contraTle b z t : (t < z -> ~~ b) -> (b -> z <= t).
+Proof. exact: comparable_contraTle. Qed.
+
+Lemma contraTlt b z t : (t <= z -> ~~ b) -> (b -> z < t).
+Proof. exact: comparable_contraTlt. Qed.
+
+Lemma contraPle P z t : (t < z -> ~ P) -> (P -> z <= t).
+Proof. exact: comparable_contraPle. Qed.
+
+Lemma contraPlt P z t : (t <= z -> ~ P) -> (P -> z < t).
+Proof. exact: comparable_contraPlt. Qed.
+
+Lemma contraNle b z t : (t < z -> b) -> (~~ b -> z <= t).
+Proof. exact: comparable_contraNle. Qed.
+
+Lemma contraNlt b z t : (t <= z -> b) -> (~~ b -> z < t).
+Proof. exact: comparable_contraNlt. Qed.
+
+Lemma contra_not_le P z t : (t < z -> P) -> (~ P -> z <= t).
+Proof. exact: comparable_contra_not_le. Qed.
+
+Lemma contra_not_lt P z t : (t <= z -> P) -> (~ P -> z < t).
+Proof. exact: comparable_contra_not_lt. Qed.
+
+Lemma contraFle b z t : (t < z -> b) -> (b = false -> z <= t).
+Proof. exact: comparable_contraFle. Qed.
+
+Lemma contraFlt b z t : (t <= z -> b) -> (b = false -> z < t).
+Proof. exact: comparable_contraFlt. Qed.
+
+Lemma contra_leq_le m n z t : (t < z -> (n < m)%N) -> ((m <= n)%N -> z <= t).
+Proof. exact: comparable_contra_leq_le. Qed.
+
+Lemma contra_leq_lt m n z t : (t <= z -> (n < m)%N) -> ((m <= n)%N -> z < t).
+Proof. exact: comparable_contra_leq_lt. Qed.
+
+Lemma contra_ltn_le m n z t : (t < z -> (n <= m)%N) -> ((m < n)%N -> z <= t).
+Proof. exact: comparable_contra_ltn_le. Qed.
+
+Lemma contra_ltn_lt m n z t : (t <= z -> (n <= m)%N) -> ((m < n)%N -> z < t).
+Proof. exact: comparable_contra_ltn_lt. Qed.
+
+Lemma contra_le x y z t : (t < z -> y < x) -> (x <= y -> z <= t).
+Proof. exact: comparable_contra_le. Qed.
+
+Lemma contra_le_lt x y z t : (t <= z -> y < x) -> (x <= y -> z < t).
+Proof. exact: comparable_contra_le_lt. Qed.
+
+Lemma contra_lt_le x y z t : (t < z -> y <= x) -> (x < y -> z <= t).
+Proof. exact: comparable_contra_lt_le. Qed.
+
+Lemma contra_lt x y z t : (t <= z -> y <= x) -> (x < y -> z < t).
+Proof. exact: comparable_contra_lt. Qed.
+
+End ContraTheory.
+
 Section TotalMonotonyTheory.
 
 Context {disp : unit} {disp' : unit}.
diff --git a/mathcomp/ssreflect/ssrnat.v b/mathcomp/ssreflect/ssrnat.v
index 8b4d39f..7a996d1 100644
--- a/mathcomp/ssreflect/ssrnat.v
+++ b/mathcomp/ssreflect/ssrnat.v
@@ -1513,6 +1513,77 @@ rewrite -[4]/(2 * 2) -mulnA mul2n -addnn sqrnD; apply/leqifP.
 by rewrite ltn_add2r eqn_add2r ltn_neqAle !nat_Cauchy; case: eqVneq.
 Qed.
 
+Section ContraLeq.
+Implicit Types (b : bool) (m n : nat) (P : Prop).
+
+Lemma contraTleq b m n : (n < m -> ~~ b) -> (b -> m <= n).
+Proof. by rewrite ltnNge; apply: contraTT. Qed.
+
+Lemma contraTltn b m n : (n <= m -> ~~ b) -> (b -> m < n).
+Proof. by rewrite ltnNge; apply: contraTN. Qed.
+
+Lemma contraPleq P m n : (n < m -> ~ P) -> (P -> m <= n).
+Proof. by rewrite ltnNge; apply: contraPT. Qed.
+
+Lemma contraPltn P m n : (n <= m -> ~ P) -> (P -> m < n).
+Proof. by rewrite ltnNge; apply: contraPN. Qed.
+
+Lemma contraNleq b m n : (n < m -> b) -> (~~ b -> m <= n).
+Proof. by rewrite ltnNge; apply: contraNT. Qed.
+
+Lemma contraNltn b m n : (n <= m -> b) -> (~~ b -> m < n).
+Proof. by rewrite ltnNge; apply: contraNN. Qed.
+
+Lemma contra_not_leq P m n : (n < m -> P) -> (~ P -> m <= n).
+Proof. by rewrite ltnNge; apply: contra_notT. Qed.
+
+Lemma contra_not_ltn P m n : (n <= m -> P) -> (~ P -> m < n).
+Proof. by rewrite ltnNge; apply: contra_notN. Qed.
+
+Lemma contraFleq b m n : (n < m -> b) -> (b = false -> m <= n).
+Proof. by rewrite ltnNge; apply: contraFT. Qed.
+
+Lemma contraFltn b m n : (n <= m -> b) -> (b = false -> m < n).
+Proof. by rewrite ltnNge; apply: contraFN. Qed.
+
+Lemma contra_leqT b m n : (~~ b -> m < n) -> (n <= m -> b).
+Proof. by rewrite ltnNge; apply: contraTT. Qed.
+
+Lemma contra_ltnT b m n : (~~ b -> m <= n) -> (n < m -> b).
+Proof. by rewrite ltnNge; apply: contraNT. Qed.
+
+Lemma contra_leqN b m n : (b -> m < n) -> (n <= m -> ~~ b).
+Proof. by rewrite ltnNge; apply: contraTN. Qed.
+
+Lemma contra_ltnN b m n : (b -> m <= n) -> (n < m -> ~~ b).
+Proof. by rewrite ltnNge; apply: contraNN. Qed.
+
+Lemma contra_leq_not P m n : (P -> m < n) -> (n <= m -> ~ P).
+Proof. by rewrite ltnNge; apply: contraTnot. Qed.
+
+Lemma contra_ltn_not P m n : (P -> m <= n) -> (n < m -> ~ P).
+Proof. by rewrite ltnNge; apply: contraNnot. Qed.
+
+Lemma contra_leqF b m n : (b -> m < n) -> (n <= m -> b = false).
+Proof. by rewrite ltnNge; apply: contraTF. Qed.
+
+Lemma contra_ltnF b m n : (b -> m <= n) -> (n < m -> b = false).
+Proof. by rewrite ltnNge; apply: contraNF. Qed.
+
+Lemma contra_leq m n p q : (q < p -> n < m) -> (m <= n -> p <= q).
+Proof. by rewrite !ltnNge; apply: contraTT. Qed.
+
+Lemma contra_leq_ltn m n p q : (q <= p -> n < m) -> (m <= n -> p < q).
+Proof. by rewrite !ltnNge; apply: contraTN. Qed.
+
+Lemma contra_ltn_leq m n p q : (q < p -> n <= m) -> (m < n -> p <= q).
+Proof. by rewrite !ltnNge; apply: contraNT. Qed.
+
+Lemma contra_ltn m n p q : (q <= p -> n <= m) -> (m < n -> p < q).
+Proof. by rewrite !ltnNge; apply: contraNN. Qed.
+
+End ContraLeq.
+
 Section Monotonicity.
 Variable T : Type.