diff options
| -rw-r--r-- | theories/PArith/BinPos.v | 6 | ||||
| -rw-r--r-- | theories/PArith/Pnat.v | 23 | ||||
| -rw-r--r-- | theories/QArith/QArith_base.v | 159 | ||||
| -rw-r--r-- | theories/QArith/Qabs.v | 35 | ||||
| -rw-r--r-- | theories/QArith/Qround.v | 13 | ||||
| -rw-r--r-- | theories/ZArith/BinInt.v | 10 | ||||
| -rw-r--r-- | theories/ZArith/Zdiv.v | 26 |
7 files changed, 270 insertions, 2 deletions
diff --git a/theories/PArith/BinPos.v b/theories/PArith/BinPos.v index 663233c57..9c8775f82 100644 --- a/theories/PArith/BinPos.v +++ b/theories/PArith/BinPos.v @@ -1025,6 +1025,11 @@ Proof. destruct ((p ?= q) Eq); intuition; discriminate. Qed. +Lemma Ple_refl : forall p, Ple p p. +Proof. + intros. unfold Ple. rewrite Pcompare_refl_id. discriminate. +Qed. + (** Strict order and operations *) Lemma Pplus_lt_mono_l : forall p q r, q<r <-> p+q < p+r. @@ -1070,7 +1075,6 @@ Proof. apply Plt_trans with (p+q); auto using Plt_plus_r. Qed. - (**********************************************************************) (** Properties of subtraction on binary positive numbers *) diff --git a/theories/PArith/Pnat.v b/theories/PArith/Pnat.v index 715c4484d..b3f2493b2 100644 --- a/theories/PArith/Pnat.v +++ b/theories/PArith/Pnat.v @@ -227,6 +227,13 @@ rewrite nat_of_P_compare_morphism. apply <- nat_compare_eq_iff; auto. Qed. +(** Stating this bidirectionally lets us reason equationally with it: *) + +Lemma nat_of_P_inj_iff : forall p q, nat_of_P p = nat_of_P q <-> p = q. +Proof. + split; intro. now apply nat_of_P_inj. now subst. +Qed. + (** [nat_of_P] is a morphism from [positive] to [nat] for [lt] (expressed from [compare] on [positive]) @@ -240,6 +247,22 @@ Proof. apply -> nat_compare_lt; auto. Qed. +(** Again, stating this bidirectionally lets us reason equationally with it: *) + +Lemma Plt_lt : forall p q, Plt p q <-> lt (nat_of_P p) (nat_of_P q). +Proof. + intros. unfold Plt. rewrite nat_of_P_compare_morphism. + apply iff_sym, nat_compare_lt. +Qed. + +(** And the same for Ple *) + +Lemma Ple_le : forall p q, Ple p q <-> le (nat_of_P p) (nat_of_P q). +Proof. + intros. unfold Ple. rewrite nat_of_P_compare_morphism. + apply iff_sym, nat_compare_le. +Qed. + (** [nat_of_P] is a morphism from [positive] to [nat] for [gt] (expressed from [compare] on [positive]) diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v index b07d3d512..fe37fccb8 100644 --- a/theories/QArith/QArith_base.v +++ b/theories/QArith/QArith_base.v @@ -46,6 +46,13 @@ Notation "x > y" := (Qlt y x)(only parsing) : Q_scope. Notation "x >= y" := (Qle y x)(only parsing) : Q_scope. Notation "x <= y <= z" := (x<=y/\y<=z) : Q_scope. +(** injection from Z is injective. *) + +Lemma inject_Z_injective (a b: Z): inject_Z a == inject_Z b <-> a = b. +Proof. + unfold Qeq. simpl. omega. +Qed. + (** Another approach : using Qcompare for defining order relations. *) Definition Qcompare (p q : Q) := (Qnum p * QDen q ?= Qnum q * QDen p)%Z. @@ -385,6 +392,26 @@ Proof. red; simpl; intro; ring. Qed. +(** Injectivity of addition (uses theory about Qopp above): *) + +Lemma Qplus_inj_r (x y z: Q): + x + z == y + z <-> x == y. +Proof. + split; intro E. + rewrite <- (Qplus_0_r x), <- (Qplus_0_r y). + rewrite <- (Qplus_opp_r z); auto. + do 2 rewrite Qplus_assoc. + rewrite E. reflexivity. + rewrite E. reflexivity. +Qed. + +Lemma Qplus_inj_l (x y z: Q): + z + x == z + y <-> x == y. +Proof. + rewrite (Qplus_comm z x), (Qplus_comm z y). + apply Qplus_inj_r. +Qed. + (** * Properties of [Qmult] *) @@ -460,6 +487,21 @@ Proof. rewrite <- H0; ring. Qed. + +(** * inject_Z is a ring homomorphism: *) + +Lemma inject_Z_plus (x y: Z): inject_Z (x + y) = inject_Z x + inject_Z y. +Proof. + unfold Qplus, inject_Z. simpl. f_equal. ring. +Qed. + +Lemma inject_Z_mult (x y: Z): inject_Z (x * y) = inject_Z x * inject_Z y. +Proof. reflexivity. Qed. + +Lemma inject_Z_opp (x: Z): inject_Z (- x) = - inject_Z x. +Proof. reflexivity. Qed. + + (** * Inverse and division. *) Lemma Qinv_involutive : forall q, (/ / q) == q. @@ -498,6 +540,25 @@ Proof. apply Qdiv_mult_l; auto. Qed. +(** Injectivity of Qmult (requires theory about Qinv above): *) + +Lemma Qmult_inj_r (x y z: Q): ~ z == 0 -> (x * z == y * z <-> x == y). +Proof. + intro z_ne_0. + split; intro E. + rewrite <- (Qmult_1_r x), <- (Qmult_1_r y). + rewrite <- (Qmult_inv_r z); auto. + do 2 rewrite Qmult_assoc. + rewrite E. reflexivity. + rewrite E. reflexivity. +Qed. + +Lemma Qmult_inj_l (x y z: Q): ~ z == 0 -> (z * x == z * y <-> x == y). +Proof. + rewrite (Qmult_comm z x), (Qmult_comm z y). + apply Qmult_inj_r. +Qed. + (** * Properties of order upon Q. *) Lemma Qle_refl : forall x, x<=x. @@ -537,6 +598,19 @@ Proof. unfold Qlt, Qeq; auto with zarith. Qed. +Lemma Zle_Qle (x y: Z): (x <= y)%Z = (inject_Z x <= inject_Z y). +Proof. + unfold Qle. intros. simpl. + do 2 rewrite Zmult_1_r. reflexivity. +Qed. + +Lemma Zlt_Qlt (x y: Z): (x < y)%Z = (inject_Z x < inject_Z y). +Proof. + unfold Qlt. intros. simpl. + do 2 rewrite Zmult_1_r. reflexivity. +Qed. + + (** Large = strict or equal *) Lemma Qle_lteq : forall x y, x<=y <-> x<y \/ x==y. @@ -675,6 +749,54 @@ Proof. Close Scope Z_scope. Qed. +Lemma Qplus_lt_le_compat : + forall x y z t, x<y -> z<=t -> x+z < y+t. +Proof. + unfold Qplus, Qle, Qlt; intros (x1, x2) (y1, y2) (z1, z2) (t1, t2); + simpl; simpl_mult. + Open Scope Z_scope. + intros. + match goal with |- ?a < ?b => ring_simplify a b end. + rewrite Zplus_comm. + apply Zplus_le_lt_compat. + match goal with |- ?a <= ?b => ring_simplify z1 t1 ('z2) ('t2) a b end. + auto with zarith. + match goal with |- ?a < ?b => ring_simplify x1 y1 ('x2) ('y2) a b end. + assert (forall p, 0 < ' p) by reflexivity. + repeat (apply Zmult_lt_compat_r; auto). + Close Scope Z_scope. +Qed. + +Lemma Qplus_le_l (x y z: Q): x + z <= y + z <-> x <= y. +Proof. + split; intros. + rewrite <- (Qplus_0_r x), <- (Qplus_0_r y), <- (Qplus_opp_r z). + do 2 rewrite Qplus_assoc. + apply Qplus_le_compat; auto with *. + apply Qplus_le_compat; auto with *. +Qed. + +Lemma Qplus_le_r (x y z: Q): z + x <= z + y <-> x <= y. +Proof. + rewrite (Qplus_comm z x), (Qplus_comm z y). + apply Qplus_le_l. +Qed. + +Lemma Qplus_lt_l (x y z: Q): x + z < y + z <-> x < y. +Proof. + split; intros. + rewrite <- (Qplus_0_r x), <- (Qplus_0_r y), <- (Qplus_opp_r z). + do 2 rewrite Qplus_assoc. + apply Qplus_lt_le_compat; auto with *. + apply Qplus_lt_le_compat; auto with *. +Qed. + +Lemma Qplus_lt_r (x y z: Q): z + x < z + y <-> x < y. +Proof. + rewrite (Qplus_comm z x), (Qplus_comm z y). + apply Qplus_lt_l. +Qed. + Lemma Qmult_le_compat_r : forall x y z, x <= y -> 0 <= z -> x*z <= y*z. Proof. intros (a1,a2) (b1,b2) (c1,c2); unfold Qle, Qlt; simpl. @@ -697,6 +819,19 @@ Proof. Close Scope Z_scope. Qed. +Lemma Qmult_le_r (x y z: Q): 0 < z -> (x*z <= y*z <-> x <= y). +Proof. + split; intro. + now apply Qmult_lt_0_le_reg_r with z. + apply Qmult_le_compat_r; auto with qarith. +Qed. + +Lemma Qmult_le_l (x y z: Q): 0 < z -> (z*x <= z*y <-> x <= y). +Proof. + rewrite (Qmult_comm z x), (Qmult_comm z y). + apply Qmult_le_r. +Qed. + Lemma Qmult_lt_compat_r : forall x y z, 0 < z -> x < y -> x*z < y*z. Proof. intros (a1,a2) (b1,b2) (c1,c2); unfold Qle, Qlt; simpl. @@ -711,6 +846,30 @@ Proof. Close Scope Z_scope. Qed. +Lemma Qmult_lt_r: forall x y z, 0 < z -> (x*z < y*z <-> x < y). +Proof. + Open Scope Z_scope. + intros (a1,a2) (b1,b2) (c1,c2). + unfold Qle, Qlt; simpl. + simpl_mult. + replace (a1*c1*('b2*'c2)) with ((a1*'b2)*(c1*'c2)) by ring. + replace (b1*c1*('a2*'c2)) with ((b1*'a2)*(c1*'c2)) by ring. + assert (forall p, 0 < ' p) by reflexivity. + split; intros. + apply Zmult_lt_reg_r with (c1*'c2); auto with zarith. + apply Zmult_lt_0_compat; auto with zarith. + apply Zmult_lt_compat_r; auto with zarith. + apply Zmult_lt_0_compat. omega. + compute; auto. + Close Scope Z_scope. +Qed. + +Lemma Qmult_lt_l (x y z: Q): 0 < z -> (z*x < z*y <-> x < y). +Proof. + rewrite (Qmult_comm z x), (Qmult_comm z y). + apply Qmult_lt_r. +Qed. + Lemma Qmult_le_0_compat : forall a b, 0 <= a -> 0 <= b -> 0 <= a*b. Proof. intros a b Ha Hb. diff --git a/theories/QArith/Qabs.v b/theories/QArith/Qabs.v index 53528ec74..557fabc89 100644 --- a/theories/QArith/Qabs.v +++ b/theories/QArith/Qabs.v @@ -100,6 +100,13 @@ rewrite Zabs_Zmult. reflexivity. Qed. +Lemma Qabs_Qminus x y: Qabs (x - y) = Qabs (y - x). +Proof. + unfold Qminus, Qopp. simpl. + rewrite Pmult_comm, <- Zabs_Zopp. + do 2 f_equal. ring. +Qed. + Lemma Qle_Qabs : forall a, a <= Qabs a. Proof. intros a. @@ -122,3 +129,31 @@ apply Qabs_triangle. apply Qabs_wd. ring. Qed. + +Lemma Qabs_Qle_condition x y: Qabs x <= y <-> -y <= x <= y. +Proof. + split. + split. + rewrite <- (Qopp_opp x). + apply Qopp_le_compat. + apply Qle_trans with (Qabs (-x)). + apply Qle_Qabs. + now rewrite Qabs_opp. + apply Qle_trans with (Qabs x); auto using Qle_Qabs. + intros (H,H'). + apply Qabs_case; trivial. + intros. rewrite <- (Qopp_opp y). now apply Qopp_le_compat. +Qed. + +Lemma Qabs_diff_Qle_condition x y r: Qabs (x - y) <= r <-> x - r <= y <= x + r. +Proof. + intros. unfold Qminus. + rewrite Qabs_Qle_condition. + rewrite <- (Qplus_le_l (-r) (x+-y) (y+r)). + rewrite <- (Qplus_le_l (x+-y) r (y-r)). + setoid_replace (-r + (y + r)) with y by ring. + setoid_replace (r + (y - r)) with y by ring. + setoid_replace (x + - y + (y + r)) with (x + r) by ring. + setoid_replace (x + - y + (y - r)) with (x - r) by ring. + intuition. +Qed. diff --git a/theories/QArith/Qround.v b/theories/QArith/Qround.v index 58a7967ed..ce363a33b 100644 --- a/theories/QArith/Qround.v +++ b/theories/QArith/Qround.v @@ -136,4 +136,15 @@ intros x y H. apply Zle_antisym. auto with *. symmetry in H; auto with *. -Qed.
\ No newline at end of file +Qed. + +Lemma Zdiv_Qdiv (n m: Z): (n / m)%Z = Qfloor (n / m). +Proof. + unfold Qfloor. intros. simpl. + destruct m as [?|?|p]; simpl. + now rewrite Zdiv_0_r, Zmult_0_r. + now rewrite Zmult_1_r. + rewrite <- Zopp_eq_mult_neg_1. + rewrite <- (Zopp_involutive (Zpos p)). + now rewrite Zdiv_opp_opp. +Qed. diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v index a162ce775..c39edf30f 100644 --- a/theories/ZArith/BinInt.v +++ b/theories/ZArith/BinInt.v @@ -1115,6 +1115,16 @@ Notation "x <= y < z" := (x <= y /\ y < z) : Z_scope. Notation "x < y < z" := (x < y /\ y < z) : Z_scope. Notation "x < y <= z" := (x < y /\ y <= z) : Z_scope. +Lemma Zpos_lt : forall p q, Zlt (Zpos p) (Zpos q) <-> Plt p q. +Proof. + intros. apply iff_refl. +Qed. + +Lemma Zpos_le : forall p q, Zle (Zpos p) (Zpos q) <-> Ple p q. +Proof. + intros. apply iff_refl. +Qed. + (**********************************************************************) (** * Minimum and maximum *) diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v index 83e3d8320..fbedaa3d7 100644 --- a/theories/ZArith/Zdiv.v +++ b/theories/ZArith/Zdiv.v @@ -875,3 +875,29 @@ Implicit Arguments Zdiv_eucl_extended. a mod (-b) = a mod b And: |r| < |b| and sgn(r) = sgn(a) (notice the a here instead of b). *) + +(** * Division and modulo in Z agree with same in nat: *) + +Require Import NPeano. + +Lemma div_Zdiv (n m: nat): m <> O -> + Z_of_nat (n / m) = Z_of_nat n / Z_of_nat m. +Proof. + intros. + apply (Zdiv_unique _ _ _ (Z_of_nat (n mod m)%nat)). + split. auto with zarith. + now apply inj_lt, Nat.mod_upper_bound. + rewrite <- inj_mult, <- inj_plus. + now apply inj_eq, Nat.div_mod. +Qed. + +Lemma mod_Zmod (n m: nat): m <> O -> + Z_of_nat (n mod m)%nat = (Z_of_nat n mod Z_of_nat m). +Proof. + intros. + apply (Zmod_unique _ _ (Z_of_nat n / Z_of_nat m)). + split. auto with zarith. + now apply inj_lt, Nat.mod_upper_bound. + rewrite <- div_Zdiv, <- inj_mult, <- inj_plus by trivial. + now apply inj_eq, Nat.div_mod. +Qed. |