From 828e60cae73eb7153d1f585f80b125f679dc0461 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Wed, 19 Aug 2020 16:33:32 +0200 Subject: Adding contra lemmas with orders - Adding contra lemmas between `leq`, `ltn`, `Order.le` ("le"), `Order.lt` ("lt"), `b` ("T"), `~~ b` ("N"), `b = false` ("F"), and `~ P` ("not"). - Changelog for contra lemmas with orders Co-authored-by: Reynald Affeldt --- mathcomp/ssreflect/order.v | 172 ++++++++++++++++++++++++++++++++++++++++++++ mathcomp/ssreflect/ssrnat.v | 71 ++++++++++++++++++ 2 files changed, 243 insertions(+) (limited to 'mathcomp') 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. -- cgit v1.2.3