diff options
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/Init/Datatypes.v | 27 | ||||
| -rw-r--r-- | theories/Init/Logic.v | 84 | ||||
| -rw-r--r-- | theories/Init/Specif.v | 2 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/Abstract/CyclicAxioms.v | 8 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/Abstract/DoubleType.v | 2 | ||||
| -rw-r--r-- | theories/micromega/Lia.v | 5 | ||||
| -rw-r--r-- | theories/nsatz/Nsatz.v | 40 | ||||
| -rw-r--r-- | theories/nsatz/NsatzTactic.v | 40 | ||||
| -rw-r--r-- | theories/ssr/ssrbool.v | 153 |
9 files changed, 238 insertions, 123 deletions
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v index 77be679070..9984bff0c2 100644 --- a/theories/Init/Datatypes.v +++ b/theories/Init/Datatypes.v @@ -79,7 +79,7 @@ Register negb as core.bool.negb. (** Basic properties of [andb] *) -Lemma andb_prop : forall a b:bool, andb a b = true -> a = true /\ b = true. +Lemma andb_prop (a b:bool) : andb a b = true -> a = true /\ b = true. Proof. destruct a, b; repeat split; assumption. Qed. @@ -87,8 +87,8 @@ Hint Resolve andb_prop: bool. Register andb_prop as core.bool.andb_prop. -Lemma andb_true_intro : - forall b1 b2:bool, b1 = true /\ b2 = true -> andb b1 b2 = true. +Lemma andb_true_intro (b1 b2:bool) : + b1 = true /\ b2 = true -> andb b1 b2 = true. Proof. destruct b1; destruct b2; simpl; intros [? ?]; assumption. Qed. @@ -245,25 +245,22 @@ End projections. Hint Resolve pair inl inr: core. -Lemma surjective_pairing : - forall (A B:Type) (p:A * B), p = (fst p, snd p). +Lemma surjective_pairing (A B:Type) (p:A * B) : p = (fst p, snd p). Proof. destruct p; reflexivity. Qed. -Lemma injective_projections : - forall (A B:Type) (p1 p2:A * B), +Lemma injective_projections (A B:Type) (p1 p2:A * B) : fst p1 = fst p2 -> snd p1 = snd p2 -> p1 = p2. Proof. destruct p1; destruct p2; simpl; intros Hfst Hsnd. rewrite Hfst; rewrite Hsnd; reflexivity. Qed. -Lemma pair_equal_spec : - forall (A B : Type) (a1 a2 : A) (b1 b2 : B), +Lemma pair_equal_spec (A B : Type) (a1 a2 : A) (b1 b2 : B) : (a1, b1) = (a2, b2) <-> a1 = a2 /\ b1 = b2. Proof with auto. - split; intros. + split; intro H. - split. + replace a1 with (fst (a1, b1)); replace a2 with (fst (a2, b2))... rewrite H... @@ -286,7 +283,7 @@ Definition prod_curry (A B C:Type) : (A -> B -> C) -> A * B -> C := uncurry. Import EqNotations. -Lemma rew_pair : forall A (P Q : A->Type) x1 x2 (y1:P x1) (y2:Q x1) (H:x1=x2), +Lemma rew_pair A (P Q : A->Type) x1 x2 (y1:P x1) (y2:Q x1) (H:x1=x2) : (rew H in y1, rew H in y2) = rew [fun x => (P x * Q x)%type] H in (y1,y2). Proof. destruct H. reflexivity. @@ -347,7 +344,7 @@ Register Eq as core.comparison.Eq. Register Lt as core.comparison.Lt. Register Gt as core.comparison.Gt. -Lemma comparison_eq_stable : forall c c' : comparison, ~~ c = c' -> c = c'. +Lemma comparison_eq_stable (c c' : comparison) : ~~ c = c' -> c = c'. Proof. destruct c, c'; intro H; reflexivity || destruct H; discriminate. Qed. @@ -359,12 +356,12 @@ Definition CompOpp (r:comparison) := | Gt => Lt end. -Lemma CompOpp_involutive : forall c, CompOpp (CompOpp c) = c. +Lemma CompOpp_involutive c : CompOpp (CompOpp c) = c. Proof. destruct c; reflexivity. Qed. -Lemma CompOpp_inj : forall c c', CompOpp c = CompOpp c' -> c = c'. +Lemma CompOpp_inj c c' : CompOpp c = CompOpp c' -> c = c'. Proof. destruct c; destruct c'; auto; discriminate. Qed. @@ -405,7 +402,7 @@ Register CompEqT as core.CompareSpecT.CompEqT. Register CompLtT as core.CompareSpecT.CompLtT. Register CompGtT as core.CompareSpecT.CompGtT. -Lemma CompareSpec2Type : forall Peq Plt Pgt c, +Lemma CompareSpec2Type Peq Plt Pgt c : CompareSpec Peq Plt Pgt c -> CompareSpecT Peq Plt Pgt c. Proof. destruct c; intros H; constructor; inversion_clear H; auto. diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index 8f9f68a292..8012235143 100644 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -523,41 +523,28 @@ Section equality_dep. Variable f : forall x, B x. Variables x y : A. - Theorem f_equal_dep : forall (H: x = y), rew H in f x = f y. + Theorem f_equal_dep (H: x = y) : rew H in f x = f y. Proof. destruct H; reflexivity. Defined. End equality_dep. -Section equality_dep2. - - Variable A A' : Type. - Variable B : A -> Type. - Variable B' : A' -> Type. - Variable f : A -> A'. - Variable g : forall a:A, B a -> B' (f a). - Variables x y : A. - - Lemma f_equal_dep2 : forall {A A' B B'} (f : A -> A') (g : forall a:A, B a -> B' (f a)) - {x1 x2 : A} {y1 : B x1} {y2 : B x2} (H : x1 = x2), +Lemma f_equal_dep2 {A A' B B'} (f : A -> A') (g : forall a:A, B a -> B' (f a)) + {x1 x2 : A} {y1 : B x1} {y2 : B x2} (H : x1 = x2) : rew H in y1 = y2 -> rew f_equal f H in g x1 y1 = g x2 y2. - Proof. - destruct H, 1. reflexivity. - Defined. - -End equality_dep2. +Proof. + destruct H, 1. reflexivity. +Defined. -Lemma rew_opp_r : forall A (P:A->Type) (x y:A) (H:x=y) (a:P y), rew H in rew <- H in a = a. +Lemma rew_opp_r A (P:A->Type) (x y:A) (H:x=y) (a:P y) : rew H in rew <- H in a = a. Proof. -intros. destruct H. reflexivity. Defined. -Lemma rew_opp_l : forall A (P:A->Type) (x y:A) (H:x=y) (a:P x), rew <- H in rew H in a = a. +Lemma rew_opp_l A (P:A->Type) (x y:A) (H:x=y) (a:P x) : rew <- H in rew H in a = a. Proof. -intros. destruct H. reflexivity. Defined. @@ -597,7 +584,7 @@ Proof. destruct 1; destruct 1; destruct 1; destruct 1; destruct 1; reflexivity. Qed. -Theorem f_equal_compose : forall A B C (a b:A) (f:A->B) (g:B->C) (e:a=b), +Theorem f_equal_compose A B C (a b:A) (f:A->B) (g:B->C) (e:a=b) : f_equal g (f_equal f e) = f_equal (fun a => g (f a)) e. Proof. destruct e. reflexivity. @@ -605,68 +592,69 @@ Defined. (** The groupoid structure of equality *) -Theorem eq_trans_refl_l : forall A (x y:A) (e:x=y), eq_trans eq_refl e = e. +Theorem eq_trans_refl_l A (x y:A) (e:x=y) : eq_trans eq_refl e = e. Proof. destruct e. reflexivity. Defined. -Theorem eq_trans_refl_r : forall A (x y:A) (e:x=y), eq_trans e eq_refl = e. +Theorem eq_trans_refl_r A (x y:A) (e:x=y) : eq_trans e eq_refl = e. Proof. destruct e. reflexivity. Defined. -Theorem eq_sym_involutive : forall A (x y:A) (e:x=y), eq_sym (eq_sym e) = e. +Theorem eq_sym_involutive A (x y:A) (e:x=y) : eq_sym (eq_sym e) = e. Proof. destruct e; reflexivity. Defined. -Theorem eq_trans_sym_inv_l : forall A (x y:A) (e:x=y), eq_trans (eq_sym e) e = eq_refl. +Theorem eq_trans_sym_inv_l A (x y:A) (e:x=y) : eq_trans (eq_sym e) e = eq_refl. Proof. destruct e; reflexivity. Defined. -Theorem eq_trans_sym_inv_r : forall A (x y:A) (e:x=y), eq_trans e (eq_sym e) = eq_refl. +Theorem eq_trans_sym_inv_r A (x y:A) (e:x=y) : eq_trans e (eq_sym e) = eq_refl. Proof. destruct e; reflexivity. Defined. -Theorem eq_trans_assoc : forall A (x y z t:A) (e:x=y) (e':y=z) (e'':z=t), +Theorem eq_trans_assoc A (x y z t:A) (e:x=y) (e':y=z) (e'':z=t) : eq_trans e (eq_trans e' e'') = eq_trans (eq_trans e e') e''. Proof. destruct e''; reflexivity. Defined. -Theorem rew_map : forall A B (P:B->Type) (f:A->B) x1 x2 (H:x1=x2) (y:P (f x1)), +Theorem rew_map A B (P:B->Type) (f:A->B) x1 x2 (H:x1=x2) (y:P (f x1)) : rew [fun x => P (f x)] H in y = rew f_equal f H in y. Proof. destruct H; reflexivity. Defined. -Theorem eq_trans_map : forall {A B} {x1 x2 x3:A} {y1:B x1} {y2:B x2} {y3:B x3}, - forall (H1:x1=x2) (H2:x2=x3) (H1': rew H1 in y1 = y2) (H2': rew H2 in y2 = y3), +Theorem eq_trans_map {A B} {x1 x2 x3:A} {y1:B x1} {y2:B x2} {y3:B x3} + (H1:x1=x2) (H2:x2=x3) (H1': rew H1 in y1 = y2) (H2': rew H2 in y2 = y3) : rew eq_trans H1 H2 in y1 = y3. Proof. - intros. destruct H2. exact (eq_trans H1' H2'). + destruct H2. exact (eq_trans H1' H2'). Defined. -Lemma map_subst : forall {A} {P Q:A->Type} (f : forall x, P x -> Q x) {x y} (H:x=y) (z:P x), +Lemma map_subst {A} {P Q:A->Type} (f : forall x, P x -> Q x) {x y} (H:x=y) (z:P x) : rew H in f x z = f y (rew H in z). Proof. destruct H. reflexivity. Defined. -Lemma map_subst_map : forall {A B} {P:A->Type} {Q:B->Type} (f:A->B) (g : forall x, P x -> Q (f x)), - forall {x y} (H:x=y) (z:P x), rew f_equal f H in g x z = g y (rew H in z). +Lemma map_subst_map {A B} {P:A->Type} {Q:B->Type} (f:A->B) (g : forall x, P x -> Q (f x)) + {x y} (H:x=y) (z:P x) : + rew f_equal f H in g x z = g y (rew H in z). Proof. destruct H. reflexivity. Defined. -Lemma rew_swap : forall A (P:A->Type) x1 x2 (H:x1=x2) (y1:P x1) (y2:P x2), rew H in y1 = y2 -> y1 = rew <- H in y2. +Lemma rew_swap A (P:A->Type) x1 x2 (H:x1=x2) (y1:P x1) (y2:P x2) : rew H in y1 = y2 -> y1 = rew <- H in y2. Proof. destruct H. trivial. Defined. -Lemma rew_compose : forall A (P:A->Type) x1 x2 x3 (H1:x1=x2) (H2:x2=x3) (y:P x1), +Lemma rew_compose A (P:A->Type) x1 x2 x3 (H1:x1=x2) (H2:x2=x3) (y:P x1) : rew H2 in rew H1 in y = rew (eq_trans H1 H2) in y. Proof. destruct H2. reflexivity. @@ -674,9 +662,8 @@ Defined. (** Extra properties of equality *) -Theorem eq_id_comm_l : forall A (f:A->A) (Hf:forall a, a = f a), forall a, f_equal f (Hf a) = Hf (f a). +Theorem eq_id_comm_l A (f:A->A) (Hf:forall a, a = f a) a : f_equal f (Hf a) = Hf (f a). Proof. - intros. unfold f_equal. rewrite <- (eq_trans_sym_inv_l (Hf a)). destruct (Hf a) at 1 2. @@ -684,9 +671,8 @@ Proof. reflexivity. Defined. -Theorem eq_id_comm_r : forall A (f:A->A) (Hf:forall a, f a = a), forall a, f_equal f (Hf a) = Hf (f a). +Theorem eq_id_comm_r A (f:A->A) (Hf:forall a, f a = a) a : f_equal f (Hf a) = Hf (f a). Proof. - intros. unfold f_equal. rewrite <- (eq_trans_sym_inv_l (Hf (f (f a)))). set (Hfsymf := fun a => eq_sym (Hf a)). @@ -700,36 +686,36 @@ Proof. reflexivity. Defined. -Lemma eq_refl_map_distr : forall A B x (f:A->B), f_equal f (eq_refl x) = eq_refl (f x). +Lemma eq_refl_map_distr A B x (f:A->B) : f_equal f (eq_refl x) = eq_refl (f x). Proof. reflexivity. Qed. -Lemma eq_trans_map_distr : forall A B x y z (f:A->B) (e:x=y) (e':y=z), f_equal f (eq_trans e e') = eq_trans (f_equal f e) (f_equal f e'). +Lemma eq_trans_map_distr A B x y z (f:A->B) (e:x=y) (e':y=z) : f_equal f (eq_trans e e') = eq_trans (f_equal f e) (f_equal f e'). Proof. destruct e'. reflexivity. Defined. -Lemma eq_sym_map_distr : forall A B (x y:A) (f:A->B) (e:x=y), eq_sym (f_equal f e) = f_equal f (eq_sym e). +Lemma eq_sym_map_distr A B (x y:A) (f:A->B) (e:x=y) : eq_sym (f_equal f e) = f_equal f (eq_sym e). Proof. destruct e. reflexivity. Defined. -Lemma eq_trans_sym_distr : forall A (x y z:A) (e:x=y) (e':y=z), eq_sym (eq_trans e e') = eq_trans (eq_sym e') (eq_sym e). +Lemma eq_trans_sym_distr A (x y z:A) (e:x=y) (e':y=z) : eq_sym (eq_trans e e') = eq_trans (eq_sym e') (eq_sym e). Proof. destruct e, e'. reflexivity. Defined. -Lemma eq_trans_rew_distr : forall A (P:A -> Type) (x y z:A) (e:x=y) (e':y=z) (k:P x), +Lemma eq_trans_rew_distr A (P:A -> Type) (x y z:A) (e:x=y) (e':y=z) (k:P x) : rew (eq_trans e e') in k = rew e' in rew e in k. Proof. destruct e, e'; reflexivity. Qed. -Lemma rew_const : forall A P (x y:A) (e:x=y) (k:P), +Lemma rew_const A P (x y:A) (e:x=y) (k:P) : rew [fun _ => P] e in k = k. Proof. destruct e; reflexivity. @@ -797,9 +783,9 @@ Lemma forall_exists_coincide_unique_domain : -> (exists! x, P x). Proof. intros A P H. - destruct H with (Q:=P) as ((x & Hx & _),_); [trivial|]. + destruct (H P) as ((x & Hx & _),_); [trivial|]. exists x. split; [trivial|]. - destruct H with (Q:=fun x'=>x=x') as (_,Huniq). + destruct (H (fun x'=>x=x')) as (_,Huniq). apply Huniq. exists x; auto. Qed. diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v index 4ff007570e..1fb6dabe6f 100644 --- a/theories/Init/Specif.v +++ b/theories/Init/Specif.v @@ -765,7 +765,7 @@ Section Dependent_choice_lemmas. exists f. split. - reflexivity. - - induction n; simpl; apply proj2_sig. + - intro n; induction n; simpl; apply proj2_sig. Defined. End Dependent_choice_lemmas. diff --git a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v index 6470cd6c81..e3e8f532b3 100644 --- a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v +++ b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v @@ -99,7 +99,7 @@ Module ZnZ. lxor : t -> t -> t }. Section Specs. - Context {t : Type}{ops : Ops t}. + Context {t : Set}{ops : Ops t}. Notation "[| x |]" := (to_Z x) (at level 0, x at level 99). @@ -221,7 +221,7 @@ Module ZnZ. Section WW. - Context {t : Type}{ops : Ops t}{specs : Specs ops}. + Context {t : Set}{ops : Ops t}{specs : Specs ops}. Let wB := base digits. @@ -284,7 +284,7 @@ Module ZnZ. Section Of_Z. - Context {t : Type}{ops : Ops t}{specs : Specs ops}. + Context {t : Set}{ops : Ops t}{specs : Specs ops}. Notation "[| x |]" := (to_Z x) (at level 0, x at level 99). @@ -325,7 +325,7 @@ End ZnZ. (** A modular specification grouping the earlier records. *) Module Type CyclicType. - Parameter t : Type. + Parameter t : Set. Declare Instance ops : ZnZ.Ops t. Declare Instance specs : ZnZ.Specs ops. End CyclicType. diff --git a/theories/Numbers/Cyclic/Abstract/DoubleType.v b/theories/Numbers/Cyclic/Abstract/DoubleType.v index 3232e3afe0..165f9893ca 100644 --- a/theories/Numbers/Cyclic/Abstract/DoubleType.v +++ b/theories/Numbers/Cyclic/Abstract/DoubleType.v @@ -54,7 +54,7 @@ Arguments W0 {znz}. (if depth = n). *) -Fixpoint word (w:Type) (n:nat) : Type := +Fixpoint word (w:Set) (n:nat) : Set := match n with | O => w | S n => zn2z (word w n) diff --git a/theories/micromega/Lia.v b/theories/micromega/Lia.v index b2c5884ed7..ef2f139133 100644 --- a/theories/micromega/Lia.v +++ b/theories/micromega/Lia.v @@ -20,7 +20,10 @@ Require Coq.micromega.Tauto. Declare ML Module "micromega_plugin". Ltac zchecker := - intros ?__wit ?__varmap ?__ff ; + let __wit := fresh "__wit" in + let __varmap := fresh "__varmap" in + let __ff := fresh "__ff" in + intros __wit __varmap __ff ; exact (ZTautoChecker_sound __ff __wit (@eq_refl bool true <: @eq bool (ZTautoChecker __ff __wit) true) (@find Z Z0 __varmap)). diff --git a/theories/nsatz/Nsatz.v b/theories/nsatz/Nsatz.v index 70180f47c7..b684775bb4 100644 --- a/theories/nsatz/Nsatz.v +++ b/theories/nsatz/Nsatz.v @@ -75,43 +75,3 @@ red. exact Rmult_comm. Defined. Instance Rdi : (Integral_domain (Rcr:=Rcri)). constructor. exact Rmult_integral. exact R_one_zero. Defined. - -(* Rational numbers *) -Require Import QArith. - -Instance Qops: (@Ring_ops Q 0%Q 1%Q Qplus Qmult Qminus Qopp Qeq). -Defined. - -Instance Qri : (Ring (Ro:=Qops)). -constructor. -try apply Q_Setoid. -apply Qplus_comp. -apply Qmult_comp. -apply Qminus_comp. -apply Qopp_comp. - exact Qplus_0_l. exact Qplus_comm. apply Qplus_assoc. - exact Qmult_1_l. exact Qmult_1_r. apply Qmult_assoc. - apply Qmult_plus_distr_l. intros. apply Qmult_plus_distr_r. -reflexivity. exact Qplus_opp_r. -Defined. - -Lemma Q_one_zero: not (Qeq 1%Q 0%Q). -Proof. unfold Qeq. simpl. lia. Qed. - -Instance Qcri: (Cring (Rr:=Qri)). -red. exact Qmult_comm. Defined. - -Instance Qdi : (Integral_domain (Rcr:=Qcri)). -constructor. -exact Qmult_integral. exact Q_one_zero. Defined. - -(* Integers *) -Lemma Z_one_zero: 1%Z <> 0%Z. -Proof. lia. Qed. - -Instance Zcri: (Cring (Rr:=Zr)). -red. exact Z.mul_comm. Defined. - -Instance Zdi : (Integral_domain (Rcr:=Zcri)). -constructor. -exact Zmult_integral. exact Z_one_zero. Defined. diff --git a/theories/nsatz/NsatzTactic.v b/theories/nsatz/NsatzTactic.v index db7dab2c46..0d24de39d1 100644 --- a/theories/nsatz/NsatzTactic.v +++ b/theories/nsatz/NsatzTactic.v @@ -447,3 +447,43 @@ Tactic Notation "nsatz" "with" repeat equalities_to_goal; nsatz_generic radicalmax info lparam lvar end. + +(* Rational numbers *) +Require Import QArith. + +Instance Qops: (@Ring_ops Q 0%Q 1%Q Qplus Qmult Qminus Qopp Qeq). +Defined. + +Instance Qri : (Ring (Ro:=Qops)). +constructor. +try apply Q_Setoid. +apply Qplus_comp. +apply Qmult_comp. +apply Qminus_comp. +apply Qopp_comp. + exact Qplus_0_l. exact Qplus_comm. apply Qplus_assoc. + exact Qmult_1_l. exact Qmult_1_r. apply Qmult_assoc. + apply Qmult_plus_distr_l. intros. apply Qmult_plus_distr_r. +reflexivity. exact Qplus_opp_r. +Defined. + +Lemma Q_one_zero: not (Qeq 1%Q 0%Q). +Proof. unfold Qeq. simpl. lia. Qed. + +Instance Qcri: (Cring (Rr:=Qri)). +red. exact Qmult_comm. Defined. + +Instance Qdi : (Integral_domain (Rcr:=Qcri)). +constructor. +exact Qmult_integral. exact Q_one_zero. Defined. + +(* Integers *) +Lemma Z_one_zero: 1%Z <> 0%Z. +Proof. lia. Qed. + +Instance Zcri: (Cring (Rr:=Zr)). +red. exact Z.mul_comm. Defined. + +Instance Zdi : (Integral_domain (Rcr:=Zcri)). +constructor. +exact Zmult_integral. exact Z_one_zero. Defined. diff --git a/theories/ssr/ssrbool.v b/theories/ssr/ssrbool.v index be84e217a5..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,7 +1342,8 @@ 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. +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. @@ -1980,12 +2013,10 @@ 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]. - 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}}. @@ -1996,17 +2027,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 +2046,119 @@ 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}. |