From 3405ab8405e141dd0a28c72c8ca221ed6f50dfed Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Sun, 7 Jun 2020 19:56:13 +0900 Subject: tentative backport of ssrbool from MathComp 1.11 --- theories/ssr/ssrbool.v | 117 +++++++++++++++++++++++++++++++++++++++++++++---- 1 file changed, 108 insertions(+), 9 deletions(-) diff --git a/theories/ssr/ssrbool.v b/theories/ssr/ssrbool.v index be84e217a5..701b604637 100644 --- a/theories/ssr/ssrbool.v +++ b/theories/ssr/ssrbool.v @@ -1980,8 +1980,8 @@ End MonoHomoMorphismTheory. Section MonoHomoMorphismTheory_in. -Variables (aT rT sT : predArgType) (f : aT -> rT) (g : rT -> aT). -Variable (aD : {pred aT}). +Variables (aT rT : predArgType) (f : aT -> rT) (g : rT -> aT). +Variables (aD : {pred aT}) (rD : {pred rT}). Variable (aP : pred aT) (rP : pred rT) (aR : rel aT) (rR : rel rT). Notation rD := [pred x | g x \in aD]. @@ -1996,17 +1996,18 @@ Lemma mono2W_in : {in aD, {homo f : x / aP x >-> rP x}}. Proof. by move=> hf x hx ax; rewrite hf. Qed. -Hypothesis fgK_on : {on aD, cancel g & f}. +Hypothesis fgK : {in rD, {on aD, cancel g & f}}. +Hypothesis mem_g : {homo g : x / x \in rD >-> x \in aD}. Lemma homoRL_in : {in aD &, {homo f : x y / aR x y >-> rR x y}} -> {in rD & aD, forall x y, aR (g x) y -> rR x (f y)}. -Proof. by move=> Hf x y hx hy /Hf; rewrite fgK_on //; apply. Qed. +Proof. by move=> Hf x y hx hy /Hf; rewrite fgK ?mem_g// ?inE; apply. Qed. Lemma homoLR_in : {in aD &, {homo f : x y / aR x y >-> rR x y}} -> {in aD & rD, forall x y, aR x (g y) -> rR (f x) y}. -Proof. by move=> Hf x y hx hy /Hf; rewrite fgK_on //; apply. Qed. +Proof. by move=> Hf x y hx hy /Hf; rewrite fgK ?mem_g// ?inE; apply. Qed. Lemma homo_mono_in : {in aD &, {homo f : x y / aR x y >-> rR x y}} -> @@ -2014,22 +2015,120 @@ Lemma homo_mono_in : {in rD &, {mono g : x y / rR x y >-> aR x y}}. Proof. move=> mf mg x y hx hy; case: (boolP (rR _ _))=> [/mg //|]; first exact. -by apply: contraNF=> /mf; rewrite !fgK_on //; apply. +by apply: contraNF=> /mf; rewrite !fgK ?mem_g//; apply. Qed. Lemma monoLR_in : {in aD &, {mono f : x y / aR x y >-> rR x y}} -> {in aD & rD, forall x y, rR (f x) y = aR x (g y)}. -Proof. by move=> mf x y hx hy; rewrite -{1}[y]fgK_on // mf. Qed. +Proof. by move=> mf x y hx hy; rewrite -{1}[y]fgK ?mem_g// mf ?mem_g. Qed. Lemma monoRL_in : {in aD &, {mono f : x y / aR x y >-> rR x y}} -> {in rD & aD, forall x y, rR x (f y) = aR (g x) y}. -Proof. by move=> mf x y hx hy; rewrite -{1}[x]fgK_on // mf. Qed. +Proof. by move=> mf x y hx hy; rewrite -{1}[x]fgK ?mem_g// mf ?mem_g. Qed. Lemma can_mono_in : {in aD &, {mono f : x y / aR x y >-> rR x y}} -> {in rD &, {mono g : x y / rR x y >-> aR x y}}. -Proof. by move=> mf x y hx hy /=; rewrite -mf // !fgK_on. Qed. +Proof. by move=> mf x y hx hy; rewrite -mf ?mem_g// !fgK ?mem_g. Qed. End MonoHomoMorphismTheory_in. +Arguments homoRL_in {aT rT f g aD rD aR rR}. +Arguments homoLR_in {aT rT f g aD rD aR rR}. +Arguments homo_mono_in {aT rT f g aD rD aR rR}. +Arguments monoLR_in {aT rT f g aD rD aR rR}. +Arguments monoRL_in {aT rT f g aD rD aR rR}. +Arguments can_mono_in {aT rT f g aD rD aR rR}. + + +Section HomoMonoMorphismFlip. +Variables (aT rT : Type) (aR : rel aT) (rR : rel rT) (f : aT -> rT). +Variable (aD aD' : {pred aT}). + +Lemma homo_sym : {homo f : x y / aR x y >-> rR x y} -> + {homo f : y x / aR x y >-> rR x y}. +Proof. by move=> fR y x; apply: fR. Qed. + +Lemma mono_sym : {mono f : x y / aR x y >-> rR x y} -> + {mono f : y x / aR x y >-> rR x y}. +Proof. by move=> fR y x; apply: fR. Qed. + +Lemma homo_sym_in : {in aD &, {homo f : x y / aR x y >-> rR x y}} -> + {in aD &, {homo f : y x / aR x y >-> rR x y}}. +Proof. by move=> fR y x yD xD; apply: fR. Qed. + +Lemma mono_sym_in : {in aD &, {mono f : x y / aR x y >-> rR x y}} -> + {in aD &, {mono f : y x / aR x y >-> rR x y}}. +Proof. by move=> fR y x yD xD; apply: fR. Qed. + +Lemma homo_sym_in11 : {in aD & aD', {homo f : x y / aR x y >-> rR x y}} -> + {in aD' & aD, {homo f : y x / aR x y >-> rR x y}}. +Proof. by move=> fR y x yD xD; apply: fR. Qed. + +Lemma mono_sym_in11 : {in aD & aD', {mono f : x y / aR x y >-> rR x y}} -> + {in aD' & aD, {mono f : y x / aR x y >-> rR x y}}. +Proof. by move=> fR y x yD xD; apply: fR. Qed. + +End HomoMonoMorphismFlip. +Arguments homo_sym {aT rT} [aR rR f]. +Arguments mono_sym {aT rT} [aR rR f]. +Arguments homo_sym_in {aT rT} [aR rR f aD]. +Arguments mono_sym_in {aT rT} [aR rR f aD]. +Arguments homo_sym_in11 {aT rT} [aR rR f aD aD']. +Arguments mono_sym_in11 {aT rT} [aR rR f aD aD']. + +Section CancelOn. + +Variables (aT rT : predArgType) (aD : {pred aT}) (rD : {pred rT}). +Variables (f : aT -> rT) (g : rT -> aT). + +Lemma onW_can : cancel g f -> {on aD, cancel g & f}. +Proof. by move=> fgK x xaD; apply: fgK. Qed. + +Lemma onW_can_in : {in rD, cancel g f} -> {in rD, {on aD, cancel g & f}}. +Proof. by move=> fgK x xrD xaD; apply: fgK. Qed. + +Lemma in_onW_can : cancel g f -> {in rD, {on aD, cancel g & f}}. +Proof. by move=> fgK x xrD xaD; apply: fgK. Qed. + +Lemma onS_can : (forall x, g x \in aD) -> {on aD, cancel g & f} -> cancel g f. +Proof. by move=> mem_g fgK x; apply: fgK. Qed. + +Lemma onS_can_in : {homo g : x / x \in rD >-> x \in aD} -> + {in rD, {on aD, cancel g & f}} -> {in rD, cancel g f}. +Proof. by move=> mem_g fgK x x_rD; apply/fgK/mem_g. Qed. + +Lemma in_onS_can : (forall x, g x \in aD) -> + {in rT, {on aD, cancel g & f}} -> cancel g f. +Proof. by move=> mem_g fgK x; apply/fgK. Qed. + +End CancelOn. +Arguments onW_can {aT rT} aD {f g}. +Arguments onW_can_in {aT rT} aD {rD f g}. +Arguments in_onW_can {aT rT} aD rD {f g}. +Arguments onS_can {aT rT} aD {f g}. +Arguments onS_can_in {aT rT} aD {rD f g}. +Arguments in_onS_can {aT rT} aD {f g}. + +Section inj_can_sym_in_on. +Variables (aT rT : predArgType) (aD : {pred aT}) (rD : {pred rT}). +Variables (f : aT -> rT) (g : rT -> aT). + +Lemma inj_can_sym_in_on : + {homo f : x / x \in aD >-> x \in rD} -> {in aD, {on rD, cancel f & g}} -> + {in rD &, {on aD &, injective g}} -> {in rD, {on aD, cancel g & f}}. +Proof. by move=> fD fK gI x x_rD gx_aD; apply: gI; rewrite ?inE ?fK ?fD. Qed. + +Lemma inj_can_sym_on : {in aD, cancel f g} -> + {on aD &, injective g} -> {on aD, cancel g & f}. +Proof. by move=> fK gI x gx_aD; apply: gI; rewrite ?inE ?fK. Qed. + +Lemma inj_can_sym_in : {homo f \o g : x / x \in rD} -> {on rD, cancel f & g} -> + {in rD &, injective g} -> {in rD, cancel g f}. +Proof. by move=> fgD fK gI x x_rD; apply: gI; rewrite ?fK ?fgD. Qed. + +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}. -- cgit v1.2.3 From a334a9405ee1706747715616f6c5c244036f877a Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 18 Jun 2020 19:21:14 +0900 Subject: add contra lemmas introduced by MathComp's PR #499 (https://github.com/math-comp/math-comp/pull/499/) --- theories/ssr/ssrbool.v | 37 +++++++++++++++++++++++++++++++++++++ 1 file changed, 37 insertions(+) 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. -- cgit v1.2.3 From bfd384ed5f7af818f6b893b50d0f8de49477c144 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 25 Aug 2020 23:07:15 +0900 Subject: fix notation-incompatible-format warnings (mathcomp commit 1bbfe3429a07bee2478fd15adf45b982fdfb5d2b) --- theories/ssr/ssrbool.v | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/theories/ssr/ssrbool.v b/theories/ssr/ssrbool.v index 8c881b1f89..468854f364 100644 --- a/theories/ssr/ssrbool.v +++ b/theories/ssr/ssrbool.v @@ -1310,7 +1310,12 @@ Definition SimplRel {T} (r : rel T) : simpl_rel T := fun x => SimplPred (r x). Definition relU {T} (r1 r2 : rel T) := SimplRel (xrelU r1 r2). Definition relpre {aT rT} (f : aT -> rT) (r : rel rT) := SimplRel (xrelpre f r). -Notation "[ 'rel' x y | E ]" := (SimplRel (fun x y => E%B)) : fun_scope. +(* Required to avoid an incompatible format warning with coq-8.12 *) +Reserved Notation "[ 'rel' x y : T | E ]" (at level 0, x ident, y ident, + format "'[hv' [ 'rel' x y : T | '/ ' E ] ']'"). + +Notation "[ 'rel' x y | E ]" := (SimplRel (fun x y => E%B)) + (only parsing) : fun_scope. Notation "[ 'rel' x y : T | E ]" := (SimplRel (fun x y : T => E%B)) (only parsing) : fun_scope. -- cgit v1.2.3 From 40140bfc872b104d184ba05a85f6ce918559a6ba Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 25 Aug 2020 23:42:09 +0900 Subject: address comments and fixups --- theories/ssr/ssrbool.v | 76 +++++++++++++++++++++----------------------------- 1 file changed, 32 insertions(+), 44 deletions(-) diff --git a/theories/ssr/ssrbool.v b/theories/ssr/ssrbool.v index 468854f364..f35da63fd6 100644 --- a/theories/ssr/ssrbool.v +++ b/theories/ssr/ssrbool.v @@ -546,6 +546,38 @@ Proof. by move/contra=> notb_notc /notb_notc/negbTE. Qed. Lemma contraFF (c b : bool) : (c -> b) -> b = false -> c = false. Proof. by move/contraFN=> bF_notc /bF_notc/negbTE. Qed. +(* additional contra lemmas involving [P,Q : Prop] *) +Lemma contra_not (P Q : Prop) : (Q -> P) -> (~ P -> ~ Q). Proof. by auto. Qed. + +Lemma contraPnot (P Q : Prop) : (Q -> ~ P) -> (P -> ~ Q). Proof. by auto. Qed. + +Lemma contraTnot (b : bool) (P : Prop) : (P -> ~~ b) -> (b -> ~ P). +Proof. by case: b; auto. Qed. + +Lemma contraNnot (P : Prop) (b : bool) : (P -> b) -> (~~ b -> ~ P). +Proof. rewrite -{1}[b]negbK; exact: contraTnot. Qed. + +Lemma contraPT (P : Prop) (b : bool) : (~~ b -> ~ P) -> P -> b. +Proof. by case: b => //= /(_ isT) nP /nP. Qed. + +Lemma contra_notT (P : Prop) (b : bool) : (~~ b -> P) -> ~ P -> b. +Proof. by case: b => //= /(_ isT) HP /(_ HP). Qed. + +Lemma contra_notN (P : Prop) (b : bool) : (b -> P) -> ~ P -> ~~ b. +Proof. rewrite -{1}[b]negbK; exact: contra_notT. Qed. + +Lemma contraPN (P : Prop) (b : bool) : (b -> ~ P) -> (P -> ~~ b). +Proof. by case: b => //=; move/(_ isT) => HP /HP. Qed. + +Lemma contraFnot (P : Prop) (b : bool) : (P -> b) -> b = false -> ~ P. +Proof. by case: b => //; auto. Qed. + +Lemma contraPF (P : Prop) (b : bool) : (b -> ~ P) -> P -> b = false. +Proof. by case: b => // /(_ isT). Qed. + +Lemma contra_notF (P : Prop) (b : bool) : (b -> P) -> ~ P -> b = false. +Proof. by case: b => // /(_ isT). Qed. + (** Coercion of sum-style datatypes into bool, which makes it possible to use ssr's boolean if rather than Coq's "generic" if. **) @@ -1310,10 +1342,6 @@ Definition SimplRel {T} (r : rel T) : simpl_rel T := fun x => SimplPred (r x). Definition relU {T} (r1 r2 : rel T) := SimplRel (xrelU r1 r2). Definition relpre {aT rT} (f : aT -> rT) (r : rel rT) := SimplRel (xrelpre f r). -(* Required to avoid an incompatible format warning with coq-8.12 *) -Reserved Notation "[ 'rel' x y : T | E ]" (at level 0, x ident, y ident, - format "'[hv' [ 'rel' x y : T | '/ ' E ] ']'"). - Notation "[ 'rel' x y | E ]" := (SimplRel (fun x y => E%B)) (only parsing) : fun_scope. Notation "[ 'rel' x y : T | E ]" := @@ -1989,8 +2017,6 @@ Variables (aT rT : predArgType) (f : aT -> rT) (g : rT -> aT). Variables (aD : {pred aT}) (rD : {pred rT}). Variable (aP : pred aT) (rP : pred rT) (aR : rel aT) (rR : rel rT). -Notation rD := [pred x | g x \in aD]. - Lemma monoW_in : {in aD &, {mono f : x y / aR x y >-> rR x y}} -> {in aD &, {homo f : x y / aR x y >-> rR x y}}. @@ -2046,7 +2072,6 @@ Arguments monoLR_in {aT rT f g aD rD aR rR}. Arguments monoRL_in {aT rT f g aD rD aR rR}. Arguments can_mono_in {aT rT f g aD rD aR rR}. - Section HomoMonoMorphismFlip. Variables (aT rT : Type) (aR : rel aT) (rR : rel rT) (f : aT -> rT). Variable (aD aD' : {pred aT}). @@ -2137,40 +2162,3 @@ 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. -- cgit v1.2.3