diff options
| -rwxr-xr-x | theories/Arith/Compare_dec.v | 48 | ||||
| -rwxr-xr-x | theories/Arith/Minus.v | 13 | ||||
| -rwxr-xr-x | theories/Arith/Mult.v | 32 | ||||
| -rwxr-xr-x | theories/Arith/Peano_dec.v | 7 | ||||
| -rwxr-xr-x | theories/Arith/Plus.v | 44 | ||||
| -rw-r--r-- | theories/Zarith/auxiliary.v | 275 | ||||
| -rw-r--r-- | theories/Zarith/zarith_aux.v | 77 |
7 files changed, 376 insertions, 120 deletions
diff --git a/theories/Arith/Compare_dec.v b/theories/Arith/Compare_dec.v index 8ef796eef5..72baafe3ac 100755 --- a/theories/Arith/Compare_dec.v +++ b/theories/Arith/Compare_dec.v @@ -10,6 +10,8 @@ Require Le. Require Lt. +Require Gt. +Require Decidable. Theorem zerop : (n:nat){n=O}+{lt O n}. Destruct n; Auto with arith. @@ -52,3 +54,49 @@ Proof. Intros; Elim (lt_eq_lt_dec n m); Auto with arith. Intros; Absurd (lt m n); Auto with arith. Qed. + +(* Proofs of decidability *) + +Theorem dec_le:(x,y:nat)(decidable (le x y)). +Intros x y; Unfold decidable ; Elim (le_gt_dec x y); [ + Auto with arith +| Intro; Right; Apply gt_not_le; Assumption]. +Save. + +Theorem dec_lt:(x,y:nat)(decidable (lt x y)). +Intros x y; Unfold lt; Apply dec_le. +Save. + +Theorem dec_gt:(x,y:nat)(decidable (gt x y)). +Intros x y; Unfold gt; Apply dec_lt. +Save. + +Theorem dec_ge:(x,y:nat)(decidable (ge x y)). +Intros x y; Unfold ge; Apply dec_le. +Save. + +Theorem not_eq : (x,y:nat) ~ x=y -> (lt x y) \/ (lt y x). +Intros x y H; Elim (lt_eq_lt_dec x y); [ + Intros H1; Elim H1; [ Auto with arith | Intros H2; Absurd x=y; Assumption] +| Auto with arith]. +Save. + + +Theorem not_le : (x,y:nat) ~(le x y) -> (gt x y). +Intros x y H; Elim (le_gt_dec x y); + [ Intros H1; Absurd (le x y); Assumption | Trivial with arith ]. +Save. + +Theorem not_gt : (x,y:nat) ~(gt x y) -> (le x y). +Intros x y H; Elim (le_gt_dec x y); + [ Trivial with arith | Intros H1; Absurd (gt x y); Assumption]. +Save. + +Theorem not_ge : (x,y:nat) ~(ge x y) -> (lt x y). +Intros x y H; Exact (not_le y x H). +Save. + +Theorem not_lt : (x,y:nat) ~(lt x y) -> (ge x y). +Intros x y H; Exact (not_gt y x H). +Save. + diff --git a/theories/Arith/Minus.v b/theories/Arith/Minus.v index 29a9780702..afb5a19844 100755 --- a/theories/Arith/Minus.v +++ b/theories/Arith/Minus.v @@ -94,3 +94,16 @@ Intros n m; Pattern n m; Apply nat_double_ind; Simpl; Auto with arith. Intros; Absurd (lt O O); Trivial with arith. Qed. Hints Immediate lt_O_minus_lt : arith v62. + +Theorem pred_of_minus : (x:nat)(pred x)=(minus x (S O)). +Induction x; Auto with arith. +Save. + + +Theorem inj_minus_aux: (x,y:nat) ~(le y x) -> (minus x y) = O. +Intros y x; Pattern y x ; Apply nat_double_ind; [ + Simpl; Trivial with arith +| Intros n H; Absurd (le O (S n)); [ Assumption | Apply le_O_n] +| Simpl; Intros n m H1 H2; Apply H1; + Unfold not ; Intros H3; Apply H2; Apply le_n_S; Assumption]. +Save. diff --git a/theories/Arith/Mult.v b/theories/Arith/Mult.v index ff38eef695..e90cec6612 100755 --- a/theories/Arith/Mult.v +++ b/theories/Arith/Mult.v @@ -10,6 +10,7 @@ Require Export Plus. Require Export Minus. +Require Export Lt. (**********************************************************) (* Multiplication *) @@ -23,6 +24,12 @@ Elim plus_assoc_l; Elim H; Auto with arith. Qed. Hints Resolve mult_plus_distr : arith v62. +Lemma mult_plus_distr_r : (n,m,p:nat) (mult n (plus m p))=(plus (mult n m) (mult n p)). +Proof. + Induction n. Trivial. + Intros. Simpl. Rewrite (H m p). Apply sym_eq. Apply plus_permute_2_in_4. +Qed. + Lemma mult_minus_distr : (n,m,p:nat)((mult (minus n m) p)=(minus (mult n p) (mult m p))). Proof. Intros; Pattern n m; Apply nat_double_ind; Simpl; Intros; Auto with arith. @@ -65,3 +72,28 @@ Lemma mult_n_1 : (n:nat)(mult n (S O))=n. Intro; Elim mult_sym; Auto with arith. Save. Hints Resolve mult_n_1 : arith v62. + + +Lemma mult_le : (m,n,p:nat) (le n p) -> (le (mult m n) (mult m p)). +Proof. + Induction m. Intros. Simpl. Apply le_n. + Intros. Simpl. Apply le_plus_plus. Assumption. + Apply H. Assumption. +Qed. +Hints Resolve mult_le : arith. + +Lemma mult_lt : (m,n,p:nat) (lt n p) -> (lt (mult (S m) n) (mult (S m) p)). +Proof. + Induction m. Intros. Simpl. Rewrite <- plus_n_O. Rewrite <- plus_n_O. Assumption. + Intros. Exact (lt_plus_plus ? ? ? ? H0 (H ? ? H0)). +Qed. + +Hints Resolve mult_lt : arith. + +Lemma mult_le_conv_1 : (m,n,p:nat) (le (mult (S m) n) (mult (S m) p)) -> (le n p). +Proof. + Intros. Elim (le_or_lt n p). Trivial. + Intro H0. Cut (lt (mult (S m) n) (mult (S m) n)). Intro. Elim (lt_n_n ? H1). + Apply le_lt_trans with m:=(mult (S m) p). Assumption. + Apply mult_lt. Assumption. +Qed. diff --git a/theories/Arith/Peano_dec.v b/theories/Arith/Peano_dec.v index 913d6dd371..5ee33d1563 100755 --- a/theories/Arith/Peano_dec.v +++ b/theories/Arith/Peano_dec.v @@ -6,8 +6,10 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) +Require Decidable. (* $Id$ *) + Theorem O_or_S : (n:nat)({m:nat|(S m)=n})+{O=n}. Proof. Induction n. @@ -22,3 +24,8 @@ Intros q H'; Elim (H q); Auto. Qed. Hints Resolve O_or_S eq_nat_dec : arith. + +Theorem dec_eq_nat:(x,y:nat)(decidable (x=y)). +Intros x y; Unfold decidable; Elim (eq_nat_dec x y); Auto with arith. +Save. + diff --git a/theories/Arith/Plus.v b/theories/Arith/Plus.v index 2f96112c38..c070e3645e 100755 --- a/theories/Arith/Plus.v +++ b/theories/Arith/Plus.v @@ -15,7 +15,7 @@ Require Le. Require Lt. -Lemma plus_sym : (n,m:nat)((plus n m)=(plus m n)). +Lemma plus_sym : (n,m:nat)(plus n m)=(plus m n). Proof. Intros n m ; Elim n ; Simpl ; Auto with arith. Intros y H ; Elim (plus_n_Sm m y) ; Auto with arith. @@ -118,3 +118,45 @@ Proof. Intros; Apply lt_le_trans with m; Auto with arith. Qed. Hints Immediate lt_plus_trans : arith v62. + +Lemma le_lt_plus_plus : (n,m,p,q:nat) (le n m)->(lt p q)->(lt (plus n p) (plus m q)). +Proof. + Unfold lt. Intros. Change (le (plus (S n) p) (plus m q)). Rewrite plus_Snm_nSm. + Apply le_plus_plus; Assumption. +Qed. + +Lemma lt_le_plus_plus : (n,m,p,q:nat) (lt n m)->(le p q)->(lt (plus n p) (plus m q)). +Proof. + Unfold lt. Intros. Change (le (plus (S n) p) (plus m q)). Apply le_plus_plus; Assumption. +Qed. + +Lemma lt_plus_plus : (n,m,p,q:nat) (lt n m)->(lt p q)->(lt (plus n p) (plus m q)). +Proof. + Intros. Apply lt_le_plus_plus. Assumption. + Apply lt_le_weak. Assumption. +Qed. + + +Lemma plus_is_O : (m,n:nat) (plus m n)=O -> m=O /\ n=O. +Proof. + Destruct m; Auto. + Intros. Discriminate H. +Qed. + +Lemma plus_is_one : (m,n:nat) (plus m n)=(S O) -> {m=O /\ n=(S O)}+{m=(S O) /\ n=O}. +Proof. + Destruct m; Auto. + Destruct n; Auto. + Intros. + Simpl in H. Discriminate H. +Qed. + +Lemma plus_permute_2_in_4 : (a,b,c,d:nat) + (plus (plus a b) (plus c d))=(plus (plus a c) (plus b d)). +Proof. + Intros. + Rewrite <- (plus_assoc_l a b (plus c d)). Rewrite (plus_assoc_l b c d). + Rewrite (plus_sym b c). Rewrite <- (plus_assoc_l c b d). Apply plus_assoc_l. +Qed. + + diff --git a/theories/Zarith/auxiliary.v b/theories/Zarith/auxiliary.v index be642fa676..9a827f104e 100644 --- a/theories/Zarith/auxiliary.v +++ b/theories/Zarith/auxiliary.v @@ -18,6 +18,7 @@ Require Export Arith. Require fast_integer. Require zarith_aux. +Require Decidable. Require Peano_dec. Require Export Compare_dec. @@ -27,10 +28,6 @@ Theorem add_un_Zs : (x:positive) (POS (add_un x)) = (Zs (POS x)). Intro; Rewrite -> ZL12; Unfold Zs; Simpl; Trivial with arith. Save. -Theorem pred_of_minus : (x:nat)(pred x)=(minus x (S O)). -Induction x; Auto with arith. -Save. - Theorem inj_S : (y:nat) (inject_nat (S y)) = (Zs (inject_nat y)). Induction y; [ Unfold Zs ; Simpl; Trivial with arith @@ -75,6 +72,7 @@ Case x; Case y; Intros; [ | Discriminate H0 | Simpl in H0; Injection H0; Do 2 Rewrite <- bij1; Intros E; Rewrite E; Auto with arith]. Save. + Theorem inj_le: (x,y:nat) (le x y) -> (Zle (inject_nat x) (inject_nat y)). @@ -110,6 +108,7 @@ Intros x; Exists (inject_nat x); Split; [ | Rewrite Zmult_sym; Rewrite Zmult_one; Rewrite Zero_right; Unfold Zle ; Elim x; Intros;Simpl; Discriminate ]. Save. + Theorem inj_minus1 : (x,y:nat) (le y x) -> (inject_nat (minus x y)) = (Zminus (inject_nat x) (inject_nat y)). @@ -118,36 +117,10 @@ Rewrite Zplus_permute; Rewrite Zplus_inverse_r; Rewrite <- inj_plus; Rewrite <- (le_plus_minus y x H);Rewrite Zero_right; Trivial with arith. Save. -Theorem inj_minus_aux: (x,y:nat) ~(le y x) -> (minus x y) = O. -Intros y x; Pattern y x ; Apply nat_double_ind; [ - Simpl; Trivial with arith -| Intros n H; Absurd (le O (S n)); [ Assumption | Apply le_O_n] -| Simpl; Intros n m H1 H2; Apply H1; - Unfold not ; Intros H3; Apply H2; Apply le_n_S; Assumption]. -Save. - Theorem inj_minus2: (x,y:nat) (gt y x) -> (inject_nat (minus x y)) = ZERO. Intros x y H; Rewrite inj_minus_aux; [ Trivial with arith | Apply gt_not_le; Assumption]. Save. -Definition decidable := [P:Prop] P \/ ~P. - -Theorem dec_not_not : (P:Prop)(decidable P) -> (~P -> False) -> P. -Unfold decidable; Tauto. Save. - -Theorem dec_True: (decidable True). -Unfold decidable; Auto with arith. Save. -Theorem dec_False: (decidable False). -Unfold decidable not; Auto with arith. Save. -Theorem dec_or: (A,B:Prop)(decidable A) -> (decidable B) -> (decidable (A\/B)). -Unfold decidable; Tauto. Save. -Theorem dec_and: (A,B:Prop)(decidable A) -> (decidable B) ->(decidable (A/\B)). -Unfold decidable; Tauto. Save. -Theorem dec_not: (A:Prop)(decidable A) -> (decidable ~A). -Unfold decidable; Tauto. Save. -Theorem dec_imp: (A,B:Prop)(decidable A) -> (decidable B) ->(decidable (A->B)). -Unfold decidable; Tauto. Save. - Theorem dec_eq: (x,y:Z) (decidable (x=y)). Intros x y; Unfold decidable ; Elim (Zcompare_EGAL x y); Intros H1 H2; Elim (Dcompare (Zcompare x y)); [ @@ -192,41 +165,6 @@ Theorem dec_eq_nat:(x,y:nat)(decidable (x=y)). Intros x y; Unfold decidable; Elim (eq_nat_dec x y); Auto with arith. Save. -Theorem dec_le:(x,y:nat)(decidable (le x y)). -Intros x y; Unfold decidable ; Elim (le_gt_dec x y); [ - Auto with arith -| Intro; Right; Apply gt_not_le; Assumption]. -Save. - -Theorem dec_lt:(x,y:nat)(decidable (lt x y)). -Intros x y; Unfold lt; Apply dec_le. -Save. - -Theorem dec_gt:(x,y:nat)(decidable (gt x y)). -Intros x y; Unfold gt; Apply dec_lt. -Save. - -Theorem dec_ge:(x,y:nat)(decidable (ge x y)). -Intros x y; Unfold ge; Apply dec_le. -Save. - -Theorem not_not : (P:Prop)(decidable P) -> (~(~P)) -> P. -Unfold decidable; Tauto. Save. - -Theorem not_or : (A,B:Prop) ~(A\/B) -> ~A /\ ~B. -Tauto. Save. - -Theorem not_and : (A,B:Prop) (decidable A) -> ~(A/\B) -> ~A \/ ~B. -Unfold decidable; Tauto. Save. - -Theorem not_imp : (A,B:Prop) (decidable A) -> ~(A -> B) -> A /\ ~B. -Unfold decidable;Tauto. -Save. - -Theorem imp_simp : (A,B:Prop) (decidable A) -> (A -> B) -> ~A \/ B. -Unfold decidable; Tauto. -Save. - Theorem not_Zge : (x,y:Z) ~(Zge x y) -> (Zlt x y). Unfold Zge Zlt ; Intros x y H; Apply dec_not_not; [ Exact (dec_Zlt x y) | Assumption]. @@ -253,41 +191,10 @@ Intros x y; Elim (Dcompare (Zcompare x y)); [ [Auto with arith | Right; Elim (Zcompare_ANTISYM x y); Auto with arith]]. Save. -Theorem not_le : (x,y:nat) ~(le x y) -> (gt x y). -Intros x y H; Elim (le_gt_dec x y); - [ Intros H1; Absurd (le x y); Assumption | Trivial with arith ]. -Save. - -Theorem not_ge : (x,y:nat) ~(ge x y) -> (lt x y). -Intros x y H; Exact (not_le y x H). -Save. - -Theorem not_gt : (x,y:nat) ~(gt x y) -> (le x y). -Intros x y H; Elim (le_gt_dec x y); - [ Trivial with arith | Intros H1; Absurd (gt x y); Assumption]. -Save. - -Theorem not_lt : (x,y:nat) ~(lt x y) -> (ge x y). -Intros x y H; Exact (not_gt y x H). -Save. - -Theorem not_eq : (x,y:nat) ~ x=y -> (lt x y) \/ (lt y x). -Intros x y H; Elim (lt_eq_lt_dec x y); [ - Intros H1; Elim H1; [ Auto with arith | Intros H2; Absurd x=y; Assumption] -| Auto with arith]. -Save. - -Theorem eq_ind_r : (A:Set)(x:A)(P:A->Prop)(P x)->(y:A)y=x -> (P y). -Intros A x P H y H0; Elim (sym_eq A y x H0); Assumption. -Save. - -Theorem eqT_ind_r : (A:Type)(x:A)(P:A->Prop)(P x)->(y:A)y==x -> (P y). -Intros A x P H y H0; Elim (sym_eqT A y x H0); Assumption. -Save. Lemma new_var: (x:Z) (EX y:Z |(x=y)). - Intros x; Exists x; Trivial with arith. Save. + Theorem Zne_left : (x,y:Z) (Zne x y) -> (Zne (Zplus x (Zopp y)) ZERO). Intros x y; Unfold Zne; Unfold not; Intros H1 H2; Apply H1; Apply Zsimpl_plus_l with (Zopp y); Rewrite Zplus_inverse_l; Rewrite Zplus_sym; @@ -295,13 +202,27 @@ Trivial with arith. Save. Theorem Zegal_left : (x,y:Z) (x=y) -> (Zplus x (Zopp y)) = ZERO. -Intros x y H;Apply (Zsimpl_plus_l y);Rewrite -> Zplus_permute; +Intros x y H; +Apply (Zsimpl_plus_l y);Rewrite -> Zplus_permute; Rewrite -> Zplus_inverse_r;Do 2 Rewrite -> Zero_right;Assumption. Save. Theorem Zle_left : (x,y:Z) (Zle x y) -> (Zle ZERO (Zplus y (Zopp x))). -Intros x y H; Apply (Zsimpl_le_plus_l x); Rewrite Zplus_permute; -Rewrite Zplus_inverse_r; Do 2 Rewrite Zero_right; Assumption. +Intros x y H; Replace ZERO with (Zplus x (Zopp x)). +Apply Zle_reg_r; Trivial. +Apply Zplus_inverse_r. +Save. + +Theorem Zle_left_rev : (x,y:Z) (Zle ZERO (Zplus y (Zopp x))) + -> (Zle x y). +Intros x y H; Apply (Zsimpl_le_plus_r (Zopp x)). +Rewrite Zplus_inverse_r; Trivial. +Save. + +Theorem Zlt_left_rev : (x,y:Z) (Zlt ZERO (Zplus y (Zopp x))) + -> (Zlt x y). +Intros x y H; Apply Zsimpl_lt_plus_r with (Zopp x). +Rewrite Zplus_inverse_r; Trivial. Save. Theorem Zlt_left : @@ -311,6 +232,13 @@ Change (Zle (Zs x) (Zs (Zpred y))); Rewrite <- Zs_pred; Apply Zlt_le_S; Assumption. Save. +Theorem Zlt_left_lt : + (x,y:Z) (Zlt x y) -> (Zlt ZERO (Zplus y (Zopp x))). +Intros x y H; Replace ZERO with (Zplus x (Zopp x)). +Apply Zlt_reg_r; Trivial. +Apply Zplus_inverse_r. +Save. + Theorem Zge_left : (x,y:Z) (Zge x y) -> (Zle ZERO (Zplus x (Zopp y))). Intros x y H; Apply Zle_left; Apply Zge_le; Assumption. Save. @@ -319,6 +247,20 @@ Theorem Zgt_left : (x,y:Z) (Zgt x y) -> (Zle ZERO (Zplus (Zplus x (NEG xH)) (Zopp y))). Intros x y H; Apply Zlt_left; Apply Zgt_lt; Assumption. Save. + +Theorem Zgt_left_gt : + (x,y:Z) (Zgt x y) -> (Zgt (Zplus x (Zopp y)) ZERO). +Intros x y H; Replace ZERO with (Zplus y (Zopp y)). +Apply Zgt_reg_r; Trivial. +Apply Zplus_inverse_r. +Save. + +Theorem Zgt_left_rev : (x,y:Z) (Zgt (Zplus x (Zopp y)) ZERO) + -> (Zgt x y). +Intros x y H; Apply Zsimpl_gt_plus_r with (Zopp y). +Rewrite Zplus_inverse_r; Trivial. +Save. + Theorem Zopp_one : (x:Z)(Zopp x)=(Zmult x (NEG xH)). Induction x; Intros; Rewrite Zmult_sym; Auto with arith. Save. @@ -331,6 +273,10 @@ Theorem Zmult_Zopp_left : (x,y:Z)(Zmult (Zopp x) y) = (Zmult x (Zopp y)). Intros; Rewrite Zopp_Zmult; Rewrite Zopp_Zmult_r; Trivial with arith. Save. +Theorem Zopp_Zmult_l : (x,y:Z)(Zopp (Zmult x y)) = (Zmult (Zopp x) y). +Intros x y; Symmetry; Apply Zopp_Zmult. +Save. + Theorem Zred_factor0 : (x:Z) x = (Zmult x (POS xH)). Intro x; Rewrite (Zmult_n_1 x); Trivial with arith. Save. @@ -439,6 +385,7 @@ Theorem Z_eq_mult: (x,y:Z) y = ZERO -> (Zmult y x) = ZERO. Intros x y H; Rewrite H; Auto with arith. Save. + Theorem Zmult_le: (x,y:Z) (Zgt x ZERO) -> (Zle ZERO (Zmult y x)) -> (Zle ZERO y). @@ -450,18 +397,33 @@ Intros x y; Case x; [ | Intros p; Unfold Zgt ; Simpl; Intros H; Discriminate H]. Save. +Theorem Zle_ZERO_mult : + (x,y:Z) (Zle ZERO x) -> (Zle ZERO y) -> (Zle ZERO (Zmult x y)). +Intros x y; Case x. +Intros; Rewrite Zero_mult_left; Trivial. +Intros p H1; Unfold Zle. + Pattern 2 ZERO ; Rewrite <- (Zero_mult_right (POS p)). + Rewrite Zcompare_Zmult_compatible; Trivial. +Intros p H1 H2; Absurd (Zgt ZERO (NEG p)); Trivial. +Unfold Zgt; Simpl; Auto with zarith. +Save. + +Lemma Zgt_ZERO_mult: (a,b:Z) (Zgt a ZERO)->(Zgt b ZERO) + ->(Zgt (Zmult a b) ZERO). +Intros x y; Case x. +Intros H; Discriminate H. +Intros p H1; Unfold Zgt; +Pattern 2 ZERO ; Rewrite <- (Zero_mult_right (POS p)). + Rewrite Zcompare_Zmult_compatible; Trivial. +Intros p H; Discriminate H. +Save. + Theorem Zle_mult: (x,y:Z) (Zgt x ZERO) -> (Zle ZERO y) -> (Zle ZERO (Zmult y x)). - -Intros x y; Case x; [ - Simpl; Unfold Zgt ; Simpl; Intros H; Discriminate H -| Intros p H1; Unfold Zle; Rewrite -> Zmult_sym; - Pattern 2 ZERO ; Rewrite <- (Zero_mult_right (POS p)); - Rewrite Zcompare_Zmult_compatible; Auto with arith -| Intros p; Unfold Zgt ; Simpl; Intros H; Discriminate H]. +Intros x y H1 H2; Apply Zle_ZERO_mult; Trivial. +Apply Zlt_le_weak; Apply Zgt_lt; Trivial. Save. - - + Theorem Zmult_lt: (x,y:Z) (Zgt x ZERO) -> (Zlt ZERO (Zmult y x)) -> (Zlt ZERO y). @@ -473,6 +435,17 @@ Intros x y; Case x; [ | Intros p; Unfold Zgt ; Simpl; Intros H; Discriminate H]. Save. +Theorem Zmult_gt: + (x,y:Z) (Zgt x ZERO) -> (Zgt (Zmult x y) ZERO) -> (Zgt y ZERO). + +Intros x y; Case x. + Intros H; Discriminate H. + Intros p H1; Unfold Zgt. + Pattern 1 ZERO ; Rewrite <- (Zero_mult_right (POS p)). + Rewrite Zcompare_Zmult_compatible; Trivial. +Intros p H; Discriminate H. +Save. + Theorem Zle_mult_approx: (x,y,z:Z) (Zgt x ZERO) -> (Zgt z ZERO) -> (Zle ZERO y) -> (Zle ZERO (Zplus (Zmult y x) z)). @@ -481,9 +454,91 @@ Intros x y z H1 H2 H3; Apply Zle_trans with m:=(Zmult y x) ; [ Apply Zle_mult; Assumption | Pattern 1 (Zmult y x) ; Rewrite <- Zero_right; Apply Zle_reg_l; Apply Zlt_le_weak; Apply Zgt_lt; Assumption]. - Save. +Lemma Zle_Zmult_pos_right : + (a,b,c : Z) + (Zle a b) -> (Zle ZERO c) -> (Zle (Zmult a c) (Zmult b c)). +Intros a b c H1 H2; Apply Zle_left_rev. +Rewrite Zopp_Zmult_l. +Rewrite <- Zmult_plus_distr_l. +Apply Zle_ZERO_mult; Trivial. +Apply Zle_left; Trivial. +Save. + +Lemma Zle_Zmult_pos_left : + (a,b,c : Z) + (Zle a b) -> (Zle ZERO c) -> (Zle (Zmult c a) (Zmult c b)). +Intros a b c H1 H2; Rewrite (Zmult_sym c a);Rewrite (Zmult_sym c b). +Apply Zle_Zmult_pos_right; Trivial. +Save. + +Lemma Zge_Zmult_pos_right : + (a,b,c : Z) + (Zge a b) -> (Zge c ZERO) -> (Zge (Zmult a c) (Zmult b c)). +Intros a b c H1 H2; Apply Zle_ge. +Apply Zle_Zmult_pos_right; Apply Zge_le; Trivial. +Save. + +Lemma Zge_Zmult_pos_left : + (a,b,c : Z) + (Zge a b) -> (Zge c ZERO) -> (Zge (Zmult c a) (Zmult c b)). +Intros a b c H1 H2; Apply Zle_ge. +Apply Zle_Zmult_pos_left; Apply Zge_le; Trivial. +Save. + +Lemma Zge_Zmult_pos_compat : + (a,b,c,d : Z) + (Zge a c) -> (Zge b d) -> (Zge c ZERO) -> (Zge d ZERO) + -> (Zge (Zmult a b) (Zmult c d)). +Intros a b c d H0 H1 H2 H3. +Apply Zge_trans with (Zmult a d). +Apply Zge_Zmult_pos_left; Trivial. +Apply Zge_trans with c; Trivial. +Apply Zge_Zmult_pos_right; Trivial. +Save. + +Lemma Zle_mult_simpl + : (a,b,c:Z) (Zgt c ZERO)->(Zle (Zmult a c) (Zmult b c))->(Zle a b). +Intros a b c H1 H2; Apply Zle_left_rev. +Apply Zmult_le with c; Trivial. +Rewrite Zmult_plus_distr_l. +Rewrite <- Zopp_Zmult_l. +Apply Zle_left; Trivial. +Save. + + +Lemma Zge_mult_simpl + : (a,b,c:Z) (Zgt c ZERO)->(Zge (Zmult a c) (Zmult b c))->(Zge a b). +Intros a b c H1 H2; Apply Zle_ge; Apply Zle_mult_simpl with c; Trivial. +Apply Zge_le; Trivial. +Save. + +Lemma Zgt_mult_simpl + : (a,b,c:Z) (Zgt c ZERO)->(Zgt (Zmult a c) (Zmult b c))->(Zgt a b). +Intros a b c H1 H2; Apply Zgt_left_rev. +Apply Zmult_gt with c; Trivial. +Rewrite Zmult_sym. +Rewrite Zmult_plus_distr_l. +Rewrite <- Zopp_Zmult_l. +Apply Zgt_left_gt; Trivial. +Save. + +Lemma Zgt_square_simpl: +(x, y : Z) (Zge x ZERO) -> (Zge y ZERO) + -> (Zgt (Zmult x x) (Zmult y y)) -> (Zgt x y). +Intros x y H0 H1 H2. +Case (dec_Zlt y x). +Intro; Apply Zlt_gt; Trivial. +Intros H3; Cut (Zge y x). +Intros H. +Elim Zgt_not_le with 1 := H2. +Apply Zge_le. +Apply Zge_Zmult_pos_compat; Auto. +Apply not_Zlt; Trivial. +Qed. + + Theorem Zmult_le_approx: (x,y,z:Z) (Zgt x ZERO) -> (Zgt x z) -> (Zle ZERO (Zplus (Zmult y x) z)) -> (Zle ZERO y). diff --git a/theories/Zarith/zarith_aux.v b/theories/Zarith/zarith_aux.v index a9c0c99760..856082b926 100644 --- a/theories/Zarith/zarith_aux.v +++ b/theories/Zarith/zarith_aux.v @@ -144,7 +144,8 @@ Unfold Zle Zgt ;Intros n p H; (ElimCompare 'n 'p); [ | Intros H1;Absurd (Zcompare n p)=SUPERIEUR;Assumption ]. Save. -Lemma Zgt_pred : (n,p:Z)(Zgt p (Zs n))->(Zgt (Zpred p) n). +Lemma Zgt_pred + : (n,p:Z)(Zgt p (Zs n))->(Zgt (Zpred p) n). Unfold Zgt Zs Zpred ;Intros n p H; Rewrite <- [x,y:Z](Zcompare_Zplus_compatible x y (POS xH)); @@ -152,17 +153,32 @@ Rewrite (Zplus_sym p); Rewrite Zplus_assoc; Rewrite [x:Z](Zplus_sym x n); Simpl; Assumption. Save. -Lemma Zsimpl_gt_plus_l : (n,m,p:Z)(Zgt (Zplus p n) (Zplus p m))->(Zgt n m). +Lemma Zsimpl_gt_plus_l + : (n,m,p:Z)(Zgt (Zplus p n) (Zplus p m))->(Zgt n m). + +Unfold Zgt; Intros n m p H; + Rewrite <- (Zcompare_Zplus_compatible n m p); Assumption. +Save. + +Lemma Zsimpl_gt_plus_r + : (n,m,p:Z)(Zgt (Zplus n p) (Zplus m p))->(Zgt n m). + +Intros n m p H; Apply Zsimpl_gt_plus_l with p. +Rewrite (Zplus_sym p n); Rewrite (Zplus_sym p m); Trivial. -Unfold Zgt; Intros n m p H; Rewrite <- (Zcompare_Zplus_compatible n m p); -Assumption. Save. -Lemma Zgt_reg_l : (n,m,p:Z)(Zgt n m)->(Zgt (Zplus p n) (Zplus p m)). +Lemma Zgt_reg_l + : (n,m,p:Z)(Zgt n m)->(Zgt (Zplus p n) (Zplus p m)). Unfold Zgt; Intros n m p H; Rewrite (Zcompare_Zplus_compatible n m p); Assumption. Save. + +Lemma Zgt_reg_r : (n,m,p:Z)(Zgt n m)->(Zgt (Zplus n p) (Zplus m p)). +Intros n m p H; Rewrite (Zplus_sym n p); Rewrite (Zplus_sym m p); Apply Zgt_reg_l; Trivial. +Save. + Theorem Zcompare_et_un: (x,y:Z) (Zcompare x y)=SUPERIEUR <-> ~(Zcompare x (Zplus y (POS xH)))=INFERIEUR. @@ -243,7 +259,6 @@ Rewrite Zplus_sym; Auto with arith. Save. Theorem Zeq_add_S : (n,m:Z) (Zs n)=(Zs m) -> n=m. - Intros n m H. Change (Zplus (Zplus (NEG xH) (POS xH)) n)= (Zplus (Zplus (NEG xH) (POS xH)) m); @@ -379,6 +394,12 @@ Intros m n; Change ~(Zgt m n)-> ~(Zlt n m); Unfold not; Intros H1 H2; Apply H1; Apply Zlt_gt; Assumption. Save. +Theorem Zge_trans : (n, m, p : Z) (Zge n m) -> (Zge m p) -> (Zge n p). +Intros n m p H1 H2. +Apply Zle_ge. +Apply Zle_trans with m; Apply Zge_le; Trivial. +Save. + Theorem Zlt_n_Sn : (n:Z)(Zlt n (Zs n)). Intro n; Apply Zgt_lt; Apply Zgt_Sn_n. Save. @@ -543,6 +564,12 @@ Intros p n m; Unfold Zle not ;Intros H1 H2;Apply H1; Rewrite (Zcompare_Zplus_compatible n m p); Assumption. Save. +Lemma Zsimpl_le_plus_r : (p,n,m:Z)(Zle (Zplus n p) (Zplus m p))->(Zle n m). + +Intros p n m H; Apply Zsimpl_le_plus_l with p. +Rewrite (Zplus_sym p n); Rewrite (Zplus_sym p m); Trivial. +Save. + Lemma Zle_reg_l : (n,m,p:Z)(Zle n m)->(Zle (Zplus p n) (Zplus p m)). Intros n m p; Unfold Zle not ;Intros H1 H2;Apply H1; @@ -567,17 +594,46 @@ Unfold Zs ;Intros n m; Rewrite <- Zplus_assoc; Rewrite (Zplus_sym (POS xH)); Trivial with arith. Save. -Lemma Zsimpl_lt_plus_l : (n,m,p:Z)(Zlt (Zplus p n) (Zplus p m))->(Zlt n m). +Lemma Zsimpl_lt_plus_l + : (n,m,p:Z)(Zlt (Zplus p n) (Zplus p m))->(Zlt n m). -Unfold Zlt ;Intros n m p; Rewrite Zcompare_Zplus_compatible;Trivial with arith. +Unfold Zlt ;Intros n m p; + Rewrite Zcompare_Zplus_compatible;Trivial with arith. Save. +Lemma Zsimpl_lt_plus_r + : (n,m,p:Z)(Zlt (Zplus n p) (Zplus m p))->(Zlt n m). +Intros n m p H; Apply Zsimpl_lt_plus_l with p. +Rewrite (Zplus_sym p n); Rewrite (Zplus_sym p m); Trivial. +Save. + Lemma Zlt_reg_l : (n,m,p:Z)(Zlt n m)->(Zlt (Zplus p n) (Zplus p m)). - Unfold Zlt ;Intros n m p; Rewrite Zcompare_Zplus_compatible;Trivial with arith. Save. +Lemma Zlt_reg_r : (n,m,p:Z)(Zlt n m)->(Zlt (Zplus n p) (Zplus m p)). +Intros n m p H; Rewrite (Zplus_sym n p); Rewrite (Zplus_sym m p); Apply Zlt_reg_l; Trivial. +Save. + +Lemma Zlt_le_reg : + (a,b,c,d:Z) (Zlt a b)->(Zle c d)->(Zlt (Zplus a c) (Zplus b d)). +Intros a b c d H0 H1. +Apply Zlt_le_trans with (Zplus b c). +Apply Zlt_reg_r; Trivial. +Apply Zle_reg_l; Trivial. +Save. + + +Lemma Zle_lt_reg : + (a,b,c,d:Z) (Zle a b)->(Zlt c d)->(Zlt (Zplus a c) (Zplus b d)). +Intros a b c d H0 H1. +Apply Zle_lt_trans with (Zplus b c). +Apply Zle_reg_r; Trivial. +Apply Zlt_reg_l; Trivial. +Save. + + Definition Zminus := [m,n:Z](Zplus m (Zopp n)). Lemma Zminus_plus_simpl : @@ -673,6 +729,9 @@ Intros n m; Unfold Zs; Rewrite Zmult_plus_distr_l; Rewrite Zmult_1_n; Trivial with arith. Save. + + + (* Just for compatibility with previous versions Use [Zmult_plus_distr_r] and [Zmult_plus_distr_l] rather than |