diff options
Diffstat (limited to 'theories/Numbers')
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZAxioms.v | 2 | ||||
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZOrder.v | 3 | ||||
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZPlusOrder.v | 107 | ||||
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZTimesOrder.v | 3 | ||||
| -rw-r--r-- | theories/Numbers/Integer/Binary/ZBinary.v | 9 | ||||
| -rw-r--r-- | theories/Numbers/Integer/NatPairs/ZNatPairs.v | 220 | ||||
| -rw-r--r-- | theories/Numbers/NatInt/NZOrder.v | 7 | ||||
| -rw-r--r-- | theories/Numbers/NatInt/NZPlusOrder.v | 67 | ||||
| -rw-r--r-- | theories/Numbers/NatInt/NZTimesOrder.v | 43 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NOrder.v | 3 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NPlusOrder.v | 87 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NTimesOrder.v | 46 |
12 files changed, 241 insertions, 356 deletions
diff --git a/theories/Numbers/Integer/Abstract/ZAxioms.v b/theories/Numbers/Integer/Abstract/ZAxioms.v index ab863eb1f6..bde3d9a920 100644 --- a/theories/Numbers/Integer/Abstract/ZAxioms.v +++ b/theories/Numbers/Integer/Abstract/ZAxioms.v @@ -10,7 +10,7 @@ Open Local Scope NatIntScope. Notation Z := NZ (only parsing). Notation E := NZE (only parsing). -Parameter Inline Zopp : Z -> Z. +Parameter Zopp : Z -> Z. Add Morphism Zopp with signature E ==> E as Zopp_wd. diff --git a/theories/Numbers/Integer/Abstract/ZOrder.v b/theories/Numbers/Integer/Abstract/ZOrder.v index 295f5355aa..e0ef2f15d9 100644 --- a/theories/Numbers/Integer/Abstract/ZOrder.v +++ b/theories/Numbers/Integer/Abstract/ZOrder.v @@ -23,6 +23,9 @@ Proof NZlt_le_incl. Theorem Zlt_neq : forall n m : Z, n < m -> n ~= m. Proof NZlt_neq. +Theorem Zlt_le_neq : forall n m : Z, n < m <-> n <= m /\ n ~= m. +Proof NZlt_le_neq. + Theorem Zle_refl : forall n : Z, n <= n. Proof NZle_refl. diff --git a/theories/Numbers/Integer/Abstract/ZPlusOrder.v b/theories/Numbers/Integer/Abstract/ZPlusOrder.v index bab1bb4a08..6a13aa3db6 100644 --- a/theories/Numbers/Integer/Abstract/ZPlusOrder.v +++ b/theories/Numbers/Integer/Abstract/ZPlusOrder.v @@ -30,14 +30,32 @@ Proof NZplus_lt_le_mono. Theorem Zplus_le_lt_mono : forall n m p q : Z, n <= m -> p < q -> n + p < m + q. Proof NZplus_le_lt_mono. +Theorem Zplus_pos_pos : forall n m : Z, 0 < n -> 0 < m -> 0 < n + m. +Proof NZplus_pos_pos. + +Theorem Zplus_pos_nonneg : forall n m : Z, 0 < n -> 0 <= m -> 0 < n + m. +Proof NZplus_pos_nonneg. + +Theorem Zplus_nonneg_pos : forall n m : Z, 0 <= n -> 0 < m -> 0 < n + m. +Proof NZplus_nonneg_pos. + +Theorem Zplus_nonneg_nonneg : forall n m : Z, 0 <= n -> 0 <= m -> 0 <= n + m. +Proof NZplus_nonneg_nonneg. + +Theorem Zlt_plus_pos_l : forall n m : Z, 0 < n -> m < n + m. +Proof NZlt_plus_pos_l. + +Theorem Zlt_plus_pos_r : forall n m : Z, 0 < n -> m < m + n. +Proof NZlt_plus_pos_r. + Theorem Zle_lt_plus_lt : forall n m p q : Z, n <= m -> p + m < q + n -> p < q. Proof NZle_lt_plus_lt. Theorem Zlt_le_plus_lt : forall n m p q : Z, n < m -> p + m <= q + n -> p < q. Proof NZlt_le_plus_lt. -Theorem Zle_le_plus_lt : forall n m p q : Z, n <= m -> p + m <= q + n -> p <= q. -Proof NZle_le_plus_lt. +Theorem Zle_le_plus_le : forall n m p q : Z, n <= m -> p + m <= q + n -> p <= q. +Proof NZle_le_plus_le. Theorem Zplus_lt_cases : forall n m p q : Z, n + m < p + q -> n < p \/ m < q. Proof NZplus_lt_cases. @@ -57,89 +75,6 @@ Proof NZplus_nonpos_cases. Theorem Zplus_nonneg_cases : forall n m : Z, 0 <= n + m -> 0 <= n \/ 0 <= m. Proof NZplus_nonneg_cases. -(** Multiplication and order *) - -Theorem Ztimes_lt_pred : - forall p q n m : Z, S p == q -> (p * n < p * m <-> q * n + m < q * m + n). -Proof NZtimes_lt_pred. - -Theorem Ztimes_lt_mono_pos_l : forall p n m : Z, 0 < p -> (n < m <-> p * n < p * m). -Proof NZtimes_lt_mono_pos_l. - -Theorem Ztimes_lt_mono_pos_r : forall p n m : Z, 0 < p -> (n < m <-> n * p < m * p). -Proof NZtimes_lt_mono_pos_r. - -Theorem Ztimes_lt_mono_neg_l : forall p n m : Z, p < 0 -> (n < m <-> p * m < p * n). -Proof NZtimes_lt_mono_neg_l. - -Theorem Ztimes_lt_mono_neg_r : forall p n m : Z, p < 0 -> (n < m <-> m * p < n * p). -Proof NZtimes_lt_mono_neg_r. - -Theorem Ztimes_le_mono_nonneg_l : forall n m p : Z, 0 <= p -> n <= m -> p * n <= p * m. -Proof NZtimes_le_mono_nonneg_l. - -Theorem Ztimes_le_mono_nonpos_l : forall n m p : Z, p <= 0 -> n <= m -> p * m <= p * n. -Proof NZtimes_le_mono_nonpos_l. - -Theorem Ztimes_le_mono_nonneg_r : forall n m p : Z, 0 <= p -> n <= m -> n * p <= m * p. -Proof NZtimes_le_mono_nonneg_r. - -Theorem Ztimes_le_mono_nonpos_r : forall n m p : Z, p <= 0 -> n <= m -> m * p <= n * p. -Proof NZtimes_le_mono_nonpos_r. - -Theorem Ztimes_cancel_l : forall n m p : Z, p ~= 0 -> (p * n == p * m <-> n == m). -Proof NZtimes_cancel_l. - -Theorem Ztimes_le_mono_pos_l : forall n m p : Z, 0 < p -> (n <= m <-> p * n <= p * m). -Proof NZtimes_le_mono_pos_l. - -Theorem Ztimes_le_mono_pos_r : forall n m p : Z, 0 < p -> (n <= m <-> n * p <= m * p). -Proof NZtimes_le_mono_pos_r. - -Theorem Ztimes_le_mono_neg_l : forall n m p : Z, p < 0 -> (n <= m <-> p * m <= p * n). -Proof NZtimes_le_mono_neg_l. - -Theorem Ztimes_le_mono_neg_r : forall n m p : Z, p < 0 -> (n <= m <-> m * p <= n * p). -Proof NZtimes_le_mono_neg_r. - -Theorem Ztimes_lt_mono : - forall n m p q : Z, 0 <= n -> n < m -> 0 <= p -> p < q -> n * p < m * q. -Proof NZtimes_lt_mono. - -Theorem Ztimes_le_mono : - forall n m p q : Z, 0 <= n -> n <= m -> 0 <= p -> p <= q -> n * p <= m * q. -Proof NZtimes_le_mono. - -Theorem Ztimes_pos_pos : forall n m : Z, 0 < n -> 0 < m -> 0 < n * m. -Proof NZtimes_pos_pos. - -Theorem Ztimes_nonneg_nonneg : forall n m : Z, 0 <= n -> 0 <= m -> 0 <= n * m. -Proof NZtimes_nonneg_nonneg. - -Theorem Ztimes_neg_neg : forall n m : Z, n < 0 -> m < 0 -> 0 < n * m. -Proof NZtimes_neg_neg. - -Theorem Ztimes_nonpos_nonpos : forall n m : Z, n <= 0 -> m <= 0 -> 0 <= n * m. -Proof NZtimes_nonpos_nonpos. - -Theorem Ztimes_pos_neg : forall n m : Z, 0 < n -> m < 0 -> n * m < 0. -Proof NZtimes_pos_neg. - -Theorem Ztimes_nonneg_nonpos : forall n m : Z, 0 <= n -> m <= 0 -> n * m <= 0. -Proof NZtimes_nonneg_nonpos. - -Theorem Ztimes_neg_pos : forall n m : Z, n < 0 -> 0 < m -> n * m < 0. -Proof NZtimes_neg_pos. - -Theorem Ztimes_nonpos_nonneg : forall n m : Z, n <= 0 -> 0 <= m -> n * m <= 0. -Proof NZtimes_nonpos_nonneg. - -Theorem Ztimes_eq_0 : forall n m : Z, n * m == 0 -> n == 0 \/ m == 0. -Proof NZtimes_eq_0. - -Theorem Ztimes_neq_0 : forall n m : Z, n ~= 0 /\ m ~= 0 <-> n * m ~= 0. -Proof NZtimes_neq_0. - (** Theorems that are either not valid on N or have different proofs on N and Z *) (** Minus and order *) @@ -252,7 +187,7 @@ Qed. Theorem Zle_le_minus_lt : forall n m p q : Z, n <= m -> p - n <= q - m -> p <= q. Proof. -intros n m p q H1 H2. apply (Zle_le_plus_lt (- m) (- n)); +intros n m p q H1 H2. apply (Zle_le_plus_le (- m) (- n)); [now apply -> Zopp_le_mono | now do 2 rewrite Zplus_opp_minus]. Qed. diff --git a/theories/Numbers/Integer/Abstract/ZTimesOrder.v b/theories/Numbers/Integer/Abstract/ZTimesOrder.v index d63dc0d8c6..4381420950 100644 --- a/theories/Numbers/Integer/Abstract/ZTimesOrder.v +++ b/theories/Numbers/Integer/Abstract/ZTimesOrder.v @@ -94,6 +94,9 @@ Theorem Ztimes_neg : forall n m : Z, n * m < 0 <-> (n < 0 /\ m > 0) \/ (n > 0 /\ m < 0). Proof NZtimes_neg. +Theorem Ztimes_2_mono_l : forall n m : Z, n < m -> 1 + (1 + 1) * n < (1 + 1) * m. +Proof NZtimes_2_mono_l. + (** Theorems that are either not valid on N or have different proofs on N and Z *) (* None? *) diff --git a/theories/Numbers/Integer/Binary/ZBinary.v b/theories/Numbers/Integer/Binary/ZBinary.v index cb8ac3b5b1..0a52d214a2 100644 --- a/theories/Numbers/Integer/Binary/ZBinary.v +++ b/theories/Numbers/Integer/Binary/ZBinary.v @@ -132,7 +132,14 @@ Qed. End NZOrdAxiomsMod. -Definition Zopp := Zopp. +Definition Zopp (x : Z) := +match x with +| Z0 => Z0 +| Zpos x => Zneg x +| Zneg x => Zpos x +end. + +Notation "- x" := (Zopp x) : Z_scope. Add Morphism Zopp with signature NZE ==> NZE as Zopp_wd. Proof. diff --git a/theories/Numbers/Integer/NatPairs/ZNatPairs.v b/theories/Numbers/Integer/NatPairs/ZNatPairs.v index 5c8b5890d5..9a012b26cf 100644 --- a/theories/Numbers/Integer/NatPairs/ZNatPairs.v +++ b/theories/Numbers/Integer/NatPairs/ZNatPairs.v @@ -1,48 +1,82 @@ Require Import NMinus. (* The most complete file for natural numbers *) -Require Import ZTimesOrder. (* The most complete file for integers *) +Require Export ZTimesOrder. (* The most complete file for integers *) Module ZPairsAxiomsMod (Import NAxiomsMod : NAxiomsSig) <: ZAxiomsSig. Module Import NPropMod := NMinusPropFunct NAxiomsMod. (* Get all properties of natural numbers *) -Notation Local N := NZ. (* To remember N without having to use a long qualifying name *) -Notation Local NE := NZE (only parsing). -Notation Local plus_wd := NZplus_wd (only parsing). + +(* The definitios of functions (NZplus, NZtimes, etc.) will be unfolded by +the properties functor. Since we don't want Zplus_comm to refer to unfolded +definitions of equality: fun p1 p2 : NZ => (fst p1 + snd p2) = (fst p2 + snd p1), +we will provide an extra layer of definitions. *) + Open Local Scope NatIntScope. +Definition Z := (N * N)%type. +Definition Z0 : Z := (0, 0). +Definition Zeq (p1 p2 : Z) := ((fst p1) + (snd p2) == (fst p2) + (snd p1)). +Definition Zsucc (n : Z) : Z := (S (fst n), snd n). +Definition Zpred (n : Z) : Z := (fst n, S (snd n)). -Module Export NZOrdAxiomsMod <: NZOrdAxiomsSig. -Module Export NZAxiomsMod <: NZAxiomsSig. +(* We do not have Zpred (Zsucc n) = n but only Zpred (Zsucc n) = n. It +could be possible to consider as canonical only pairs where one of the +elements is 0, and make all operations convert canonical values into other +canonical values. In that case, we could get rid of setoids as well as +arrive at integers as signed natural numbers. *) + +Definition Zplus (n m : Z) : Z := ((fst n) + (fst m), (snd n) + (snd m)). +Definition Zminus (n m : Z) : Z := ((fst n) + (snd m), (snd n) + (fst m)). -Definition NZ : Set := (NZ * NZ)%type. -Definition NZE (p1 p2 : NZ) := ((fst p1) + (snd p2) == (fst p2) + (snd p1)). -Notation Z := NZ (only parsing). -Notation E := NZE (only parsing). -Definition NZ0 := (0, 0). -Definition NZsucc (n : Z) := (S (fst n), snd n). -Definition NZpred (n : Z) := (fst n, S (snd n)). -(* We do not have P (S n) = n but only P (S n) == n. It could be possible -to consider as canonical only pairs where one of the elements is 0, and -make all operations convert canonical values into other canonical values. -In that case, we could get rid of setoids as well as arrive at integers as -signed natural numbers. *) -Definition NZplus (n m : Z) := ((fst n) + (fst m), (snd n) + (snd m)). -Definition NZminus (n m : Z) := ((fst n) + (snd m), (snd n) + (fst m)). (* Unfortunately, the elements of the pair keep increasing, even during subtraction *) -Definition NZtimes (n m : Z) := + +Definition Ztimes (n m : Z) : Z := ((fst n) * (fst m) + (snd n) * (snd m), (fst n) * (snd m) + (snd n) * (fst m)). +Definition Zlt (n m : Z) := (fst n) + (snd m) < (fst m) + (snd n). +Definition Zle (n m : Z) := (fst n) + (snd m) <= (fst m) + (snd n). -Theorem ZE_refl : reflexive Z E. +Delimit Scope IntScope with Int. +Bind Scope IntScope with Z. +Notation "x == y" := (Zeq x y) (at level 70) : IntScope. +Notation "x ~= y" := (~ Zeq x y) (at level 70) : IntScope. +Notation "0" := Z0 : IntScope. +Notation "1" := (Zsucc Z0) : IntScope. +Notation "x + y" := (Zplus x y) : IntScope. +Notation "x - y" := (Zminus x y) : IntScope. +Notation "x * y" := (Ztimes x y) : IntScope. +Notation "x < y" := (Zlt x y) : IntScope. +Notation "x <= y" := (Zle x y) : IntScope. +Notation "x > y" := (Zlt y x) (only parsing) : IntScope. +Notation "x >= y" := (Zle y x) (only parsing) : IntScope. + +Notation Local N := NZ. +(* To remember N without having to use a long qualifying name. since NZ will be redefined *) +Notation Local NE := NZE (only parsing). +Notation Local plus_wd := NZplus_wd (only parsing). + +Module Export NZOrdAxiomsMod <: NZOrdAxiomsSig. +Module Export NZAxiomsMod <: NZAxiomsSig. + +Definition NZ : Set := Z. +Definition NZE := Zeq. +Definition NZ0 := Z0. +Definition NZsucc := Zsucc. +Definition NZpred := Zpred. +Definition NZplus := Zplus. +Definition NZminus := Zminus. +Definition NZtimes := Ztimes. + +Theorem ZE_refl : reflexive Z Zeq. Proof. -unfold reflexive, E; reflexivity. +unfold reflexive, Zeq. reflexivity. Qed. -Theorem ZE_symm : symmetric Z E. +Theorem ZE_symm : symmetric Z Zeq. Proof. -unfold symmetric, E; now symmetry. +unfold symmetric, Zeq; now symmetry. Qed. -Theorem ZE_trans : transitive Z E. +Theorem ZE_trans : transitive Z Zeq. Proof. -unfold transitive, E. intros n m p H1 H2. +unfold transitive, Zeq. intros n m p H1 H2. assert (H3 : (fst n + snd m) + (fst m + snd p) == (fst m + snd n) + (fst p + snd m)) by now apply plus_wd. stepl ((fst n + snd p) + (fst m + snd m)) in H3 by ring. @@ -50,46 +84,46 @@ stepr ((fst p + snd n) + (fst m + snd m)) in H3 by ring. now apply -> plus_cancel_r in H3. Qed. -Theorem NZE_equiv : equiv Z E. +Theorem NZE_equiv : equiv Z Zeq. Proof. unfold equiv; repeat split; [apply ZE_refl | apply ZE_trans | apply ZE_symm]. Qed. -Add Relation Z E +Add Relation Z Zeq reflexivity proved by (proj1 NZE_equiv) symmetry proved by (proj2 (proj2 NZE_equiv)) transitivity proved by (proj1 (proj2 NZE_equiv)) as NZE_rel. -Add Morphism (@pair N N) with signature NE ==> NE ==> E as Zpair_wd. +Add Morphism (@pair N N) with signature NE ==> NE ==> Zeq as Zpair_wd. Proof. -intros n1 n2 H1 m1 m2 H2; unfold E; simpl; rewrite H1; now rewrite H2. +intros n1 n2 H1 m1 m2 H2; unfold Zeq; simpl; rewrite H1; now rewrite H2. Qed. -Add Morphism NZsucc with signature E ==> E as NZsucc_wd. +Add Morphism NZsucc with signature Zeq ==> Zeq as NZsucc_wd. Proof. -unfold NZsucc, E; intros n m H; simpl. +unfold NZsucc, Zeq; intros n m H; simpl. do 2 rewrite plus_succ_l; now rewrite H. Qed. -Add Morphism NZpred with signature E ==> E as NZpred_wd. +Add Morphism NZpred with signature Zeq ==> Zeq as NZpred_wd. Proof. -unfold NZpred, E; intros n m H; simpl. +unfold NZpred, Zeq; intros n m H; simpl. do 2 rewrite plus_succ_r; now rewrite H. Qed. -Add Morphism NZplus with signature E ==> E ==> E as NZplus_wd. +Add Morphism NZplus with signature Zeq ==> Zeq ==> Zeq as NZplus_wd. Proof. -unfold E, NZplus; intros n1 m1 H1 n2 m2 H2; simpl. +unfold Zeq, NZplus; intros n1 m1 H1 n2 m2 H2; simpl. assert (H3 : (fst n1 + snd m1) + (fst n2 + snd m2) == (fst m1 + snd n1) + (fst m2 + snd n2)) by now apply plus_wd. stepl (fst n1 + snd m1 + (fst n2 + snd m2)) by ring. now stepr (fst m1 + snd n1 + (fst m2 + snd n2)) by ring. Qed. -Add Morphism NZminus with signature E ==> E ==> E as NZminus_wd. +Add Morphism NZminus with signature Zeq ==> Zeq ==> Zeq as NZminus_wd. Proof. -unfold E, NZminus; intros n1 m1 H1 n2 m2 H2; simpl. +unfold Zeq, NZminus; intros n1 m1 H1 n2 m2 H2; simpl. symmetry in H2. assert (H3 : (fst n1 + snd m1) + (fst m2 + snd n2) == (fst m1 + snd n1) + (fst n2 + snd m2)) by now apply plus_wd. @@ -97,9 +131,9 @@ stepl (fst n1 + snd m1 + (fst m2 + snd n2)) by ring. now stepr (fst m1 + snd n1 + (fst n2 + snd m2)) by ring. Qed. -Add Morphism NZtimes with signature E ==> E ==> E as NZtimes_wd. +Add Morphism NZtimes with signature Zeq ==> Zeq ==> Zeq as NZtimes_wd. Proof. -unfold NZtimes, E; intros n1 m1 H1 n2 m2 H2; simpl. +unfold NZtimes, Zeq; intros n1 m1 H1 n2 m2 H2; simpl. stepl (fst n1 * fst n2 + (snd n1 * snd n2 + fst m1 * snd m2 + snd m1 * fst m2)) by ring. stepr (fst n1 * snd n2 + (fst m1 * fst m2 + snd m1 * snd m2 + snd n1 * fst n2)) by ring. apply plus_times_repl_pair with (n := fst m2) (m := snd m2); [| now idtac]. @@ -117,39 +151,20 @@ apply plus_times_repl_pair with (n := fst m1) (m := snd m1); [| now idtac]. ring. Qed. -Delimit Scope IntScope with Int. -Bind Scope IntScope with NZ. -Open Local Scope IntScope. -Notation "x == y" := (NZE x y) (at level 70) : IntScope. -Notation "x ~= y" := (~ NZE x y) (at level 70) : IntScope. -Notation "0" := NZ0 : IntScope. -Notation "'S'" := NZsucc : IntScope. -Notation "'P'" := NZpred : IntScope. -Notation "1" := (S 0) : IntScope. -Notation "x + y" := (NZplus x y) : IntScope. -Notation "x - y" := (NZminus x y) : IntScope. -Notation "x * y" := (NZtimes x y) : IntScope. - -Theorem NZpred_succ : forall n : Z, P (S n) == n. -Proof. -unfold NZpred, NZsucc, E; intro n; simpl. -rewrite plus_succ_l; now rewrite plus_succ_r. -Qed. - Section Induction. Open Scope NatIntScope. (* automatically closes at the end of the section *) Variable A : Z -> Prop. -Hypothesis A_wd : predicate_wd E A. +Hypothesis A_wd : predicate_wd Zeq A. -Add Morphism A with signature E ==> iff as A_morph. +Add Morphism A with signature Zeq ==> iff as A_morph. Proof. exact A_wd. Qed. Theorem NZinduction : - A 0 -> (forall n : Z, A n <-> A (S n)) -> forall n : Z, A n. (* 0 is interpreted as in Z due to "Bind" directive *) + A 0 -> (forall n : Z, A n <-> A (Zsucc n)) -> forall n : Z, A n. (* 0 is interpreted as in Z due to "Bind" directive *) Proof. -intros A0 AS n; unfold NZ0, NZsucc, predicate_wd, fun_wd, E in *. +intros A0 AS n; unfold NZ0, Zsucc, predicate_wd, fun_wd, Zeq in *. destruct n as [n m]. cut (forall p : N, A (p, 0)); [intro H1 |]. cut (forall p : N, A (0, p)); [intro H2 |]. @@ -166,51 +181,56 @@ Qed. End Induction. +(* Time to prove theorems in the language of Z *) + +Open Local Scope IntScope. + +Theorem NZpred_succ : forall n : Z, Zpred (Zsucc n) == n. +Proof. +unfold NZpred, NZsucc, Zeq; intro n; simpl. +rewrite plus_succ_l; now rewrite plus_succ_r. +Qed. + Theorem NZplus_0_l : forall n : Z, 0 + n == n. Proof. -intro n; unfold NZplus, E; simpl. now do 2 rewrite plus_0_l. +intro n; unfold NZplus, Zeq; simpl. now do 2 rewrite plus_0_l. Qed. -Theorem NZplus_succ_l : forall n m : Z, (S n) + m == S (n + m). +Theorem NZplus_succ_l : forall n m : Z, (Zsucc n) + m == Zsucc (n + m). Proof. -intros n m; unfold NZplus, E; simpl. now do 2 rewrite plus_succ_l. +intros n m; unfold NZplus, Zeq; simpl. now do 2 rewrite plus_succ_l. Qed. Theorem NZminus_0_r : forall n : Z, n - 0 == n. Proof. -intro n; unfold NZminus, E; simpl. now do 2 rewrite plus_0_r. +intro n; unfold NZminus, Zeq; simpl. now do 2 rewrite plus_0_r. Qed. -Theorem NZminus_succ_r : forall n m : Z, n - (S m) == P (n - m). +Theorem NZminus_succ_r : forall n m : Z, n - (Zsucc m) == Zpred (n - m). Proof. -intros n m; unfold NZminus, E; simpl. symmetry; now rewrite plus_succ_r. +intros n m; unfold NZminus, Zeq; simpl. symmetry; now rewrite plus_succ_r. Qed. Theorem NZtimes_0_r : forall n : Z, n * 0 == 0. Proof. -intro n; unfold NZtimes, E; simpl. +intro n; unfold NZtimes, Zeq; simpl. repeat rewrite times_0_r. now rewrite plus_assoc. Qed. -Theorem NZtimes_succ_r : forall n m : Z, n * (S m) == n * m + n. +Theorem NZtimes_succ_r : forall n m : Z, n * (Zsucc m) == n * m + n. Proof. -intros n m; unfold NZtimes, NZsucc, E; simpl. +intros n m; unfold NZtimes, NZsucc, Zeq; simpl. do 2 rewrite times_succ_r. ring. Qed. End NZAxiomsMod. -Definition NZlt (n m : Z) := (fst n) + (snd m) < (fst m) + (snd n). -Definition NZle (n m : Z) := (fst n) + (snd m) <= (fst m) + (snd n). - -Notation "x < y" := (NZlt x y) : IntScope. -Notation "x <= y" := (NZle x y) : IntScope. -Notation "x > y" := (NZlt y x) (only parsing) : IntScope. -Notation "x >= y" := (NZle y x) (only parsing) : IntScope. +Definition NZlt := Zlt. +Definition NZle := Zle. -Add Morphism NZlt with signature E ==> E ==> iff as NZlt_wd. +Add Morphism NZlt with signature Zeq ==> Zeq ==> iff as NZlt_wd. Proof. -unfold NZlt, E; intros n1 m1 H1 n2 m2 H2; simpl. split; intro H. +unfold NZlt, Zlt, Zeq; intros n1 m1 H1 n2 m2 H2; simpl. split; intro H. stepr (snd m1 + fst m2) by apply plus_comm. apply (plus_lt_repl_pair (fst n1) (snd n1)); [| assumption]. stepl (snd m2 + fst n1) by apply plus_comm. @@ -227,58 +247,58 @@ now stepl (fst m1 + snd m2) by apply plus_comm. stepl (fst n2 + snd m2) by apply plus_comm. now stepr (fst m2 + snd n2) by apply plus_comm. Qed. -Open Local Scope IntScope. - -Add Morphism NZle with signature E ==> E ==> iff as NZle_wd. +Add Morphism NZle with signature Zeq ==> Zeq ==> iff as NZle_wd. Proof. -unfold NZle, E; intros n1 m1 H1 n2 m2 H2; simpl. -do 2 rewrite le_lt_or_eq. rewrite (NZlt_wd n1 m1 H1 n2 m2 H2). fold (m1 < m2). -fold (n1 == n2) (m1 == m2); fold (n1 == m1) in H1; fold (n2 == m2) in H2. +unfold NZle, Zle, Zeq; intros n1 m1 H1 n2 m2 H2; simpl. +do 2 rewrite le_lt_or_eq. rewrite (NZlt_wd n1 m1 H1 n2 m2 H2). fold (m1 < m2)%Int. +fold (n1 == n2)%Int (m1 == m2)%Int; fold (n1 == m1)%Int in H1; fold (n2 == m2)%Int in H2. now rewrite H1, H2. Qed. +Open Local Scope IntScope. + Theorem NZle_lt_or_eq : forall n m : Z, n <= m <-> n < m \/ n == m. Proof. -intros n m; unfold NZlt, NZle, E; simpl. apply le_lt_or_eq. +intros n m; unfold Zlt, Zle, Zeq; simpl. apply le_lt_or_eq. Qed. Theorem NZlt_irrefl : forall n : Z, ~ (n < n). Proof. -intros n; unfold NZlt, E; simpl. apply lt_irrefl. +intros n; unfold Zlt, Zeq; simpl. apply lt_irrefl. Qed. -Theorem NZlt_succ_le : forall n m : Z, n < (S m) <-> n <= m. +Theorem NZlt_succ_le : forall n m : Z, n < (Zsucc m) <-> n <= m. Proof. -intros n m; unfold NZlt, NZle, E; simpl. rewrite plus_succ_l; apply lt_succ_le. +intros n m; unfold Zlt, Zle, Zeq; simpl. rewrite plus_succ_l; apply lt_succ_le. Qed. End NZOrdAxiomsMod. -Definition Zopp (n : Z) := (snd n, fst n). +Definition Zopp (n : Z) : Z := (snd n, fst n). -Notation "- x" := (Zopp x) (at level 35, right associativity) : IntScope. +Notation "- x" := (Zopp x) : IntScope. -Add Morphism Zopp with signature E ==> E as Zopp_wd. +Add Morphism Zopp with signature Zeq ==> Zeq as Zopp_wd. Proof. -unfold E; intros n m H; simpl. symmetry. +unfold Zeq; intros n m H; simpl. symmetry. stepl (fst n + snd m) by apply plus_comm. now stepr (fst m + snd n) by apply plus_comm. Qed. Open Local Scope IntScope. -Theorem Zsucc_pred : forall n : Z, S (P n) == n. +Theorem Zsucc_pred : forall n : Z, Zsucc (Zpred n) == n. Proof. -intro n; unfold NZsucc, NZpred, E; simpl. +intro n; unfold Zsucc, Zpred, Zeq; simpl. rewrite plus_succ_l; now rewrite plus_succ_r. Qed. Theorem Zopp_0 : - 0 == 0. Proof. -unfold Zopp, E; simpl. now rewrite plus_0_l. +unfold Zopp, Zeq; simpl. now rewrite plus_0_l. Qed. -Theorem Zopp_succ : forall n, - (S n) == P (- n). +Theorem Zopp_succ : forall n, - (Zsucc n) == Zpred (- n). Proof. reflexivity. Qed. diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v index 5c6369fe49..cb3dd3093f 100644 --- a/theories/Numbers/NatInt/NZOrder.v +++ b/theories/Numbers/NatInt/NZOrder.v @@ -44,6 +44,13 @@ Proof. intros n m H1 H2; rewrite H2 in H1; false_hyp H1 NZlt_irrefl. Qed. +Theorem NZlt_le_neq : forall n m : NZ, n < m <-> n <= m /\ n ~= m. +Proof. +intros n m; split; [intro H | intros [H1 H2]]. +split. le_less. now apply NZlt_neq. +le_elim H1. assumption. false_hyp H1 H2. +Qed. + Theorem NZle_refl : forall n : NZ, n <= n. Proof. intro; now le_equal. diff --git a/theories/Numbers/NatInt/NZPlusOrder.v b/theories/Numbers/NatInt/NZPlusOrder.v deleted file mode 100644 index 6368fa5578..0000000000 --- a/theories/Numbers/NatInt/NZPlusOrder.v +++ /dev/null @@ -1,67 +0,0 @@ -Require Export NZPlus. -Require Export NZOrder. - -Module NZPlusOrderPropFunct - (Import NZPlusMod : NZPlusSig) - (Import NZOrderMod : NZOrderSig with Module NZBaseMod := NZPlusMod.NZBaseMod). - -Module Export NZPlusPropMod := NZPlusPropFunct NZPlusMod. -Module Export NZOrderPropMod := NZOrderPropFunct NZOrderMod. -Open Local Scope NatIntScope. - -Theorem NZplus_lt_mono_l : forall n m p, n < m <-> p + n < p + m. -Proof. -intros n m p; NZinduct p. -now do 2 rewrite NZplus_0_l. -intro p. do 2 rewrite NZplus_succ_l. now rewrite <- NZsucc_lt_mono. -Qed. - -Theorem NZplus_lt_mono_r : forall n m p, n < m <-> n + p < m + p. -Proof. -intros n m p. -rewrite (NZplus_comm n p); rewrite (NZplus_comm m p); apply NZplus_lt_mono_l. -Qed. - -Theorem NZplus_lt_mono : forall n m p q, n < m -> p < q -> n + p < m + q. -Proof. -intros n m p q H1 H2. -apply NZlt_trans with (m + p); -[now apply -> NZplus_lt_mono_r | now apply -> NZplus_lt_mono_l]. -Qed. - -Theorem NZplus_le_mono_l : forall n m p, n <= m <-> p + n <= p + m. -Proof. -intros n m p; NZinduct p. -now do 2 rewrite NZplus_0_l. -intro p. do 2 rewrite NZplus_succ_l. now rewrite <- NZsucc_le_mono. -Qed. - -Theorem NZplus_le_mono_r : forall n m p, n <= m <-> n + p <= m + p. -Proof. -intros n m p. -rewrite (NZplus_comm n p); rewrite (NZplus_comm m p); apply NZplus_le_mono_l. -Qed. - -Theorem NZplus_le_mono : forall n m p q, n <= m -> p <= q -> n + p <= m + q. -Proof. -intros n m p q H1 H2. -apply NZle_trans with (m + p); -[now apply -> NZplus_le_mono_r | now apply -> NZplus_le_mono_l]. -Qed. - -Theorem NZplus_lt_le_mono : forall n m p q, n < m -> p <= q -> n + p < m + q. -Proof. -intros n m p q H1 H2. -apply NZlt_le_trans with (m + p); -[now apply -> NZplus_lt_mono_r | now apply -> NZplus_le_mono_l]. -Qed. - -Theorem NZplus_le_lt_mono : forall n m p q, n <= m -> p < q -> n + p < m + q. -Proof. -intros n m p q H1 H2. -apply NZle_lt_trans with (m + p); -[now apply -> NZplus_le_mono_r | now apply -> NZplus_lt_mono_l]. -Qed. - -End NZPlusOrderPropFunct. - diff --git a/theories/Numbers/NatInt/NZTimesOrder.v b/theories/Numbers/NatInt/NZTimesOrder.v index 6f702067da..2f3cf678b9 100644 --- a/theories/Numbers/NatInt/NZTimesOrder.v +++ b/theories/Numbers/NatInt/NZTimesOrder.v @@ -61,6 +61,37 @@ apply NZle_lt_trans with (m + p); [now apply -> NZplus_le_mono_r | now apply -> NZplus_lt_mono_l]. Qed. +Theorem NZplus_pos_pos : forall n m : NZ, 0 < n -> 0 < m -> 0 < n + m. +Proof. +intros n m H1 H2. rewrite <- (NZplus_0_l 0). now apply NZplus_lt_mono. +Qed. + +Theorem NZplus_pos_nonneg : forall n m : NZ, 0 < n -> 0 <= m -> 0 < n + m. +Proof. +intros n m H1 H2. rewrite <- (NZplus_0_l 0). now apply NZplus_lt_le_mono. +Qed. + +Theorem NZplus_nonneg_pos : forall n m : NZ, 0 <= n -> 0 < m -> 0 < n + m. +Proof. +intros n m H1 H2. rewrite <- (NZplus_0_l 0). now apply NZplus_le_lt_mono. +Qed. + +Theorem NZplus_nonneg_nonneg : forall n m : NZ, 0 <= n -> 0 <= m -> 0 <= n + m. +Proof. +intros n m H1 H2. rewrite <- (NZplus_0_l 0). now apply NZplus_le_mono. +Qed. + +Theorem NZlt_plus_pos_l : forall n m : NZ, 0 < n -> m < n + m. +Proof. +intros n m H. apply -> (NZplus_lt_mono_r 0 n m) in H. +now rewrite NZplus_0_l in H. +Qed. + +Theorem NZlt_plus_pos_r : forall n m : NZ, 0 < n -> m < m + n. +Proof. +intros; rewrite NZplus_comm; now apply NZlt_plus_pos_l. +Qed. + Theorem NZle_lt_plus_lt : forall n m p q : NZ, n <= m -> p + m < q + n -> p < q. Proof. intros n m p q H1 H2. destruct (NZle_gt_cases q p); [| assumption]. @@ -75,7 +106,7 @@ pose proof (NZplus_le_lt_mono q p n m H H1) as H3. apply <- NZnle_gt in H3. false_hyp H2 H3. Qed. -Theorem NZle_le_plus_lt : forall n m p q : NZ, n <= m -> p + m <= q + n -> p <= q. +Theorem NZle_le_plus_le : forall n m p q : NZ, n <= m -> p + m <= q + n -> p <= q. Proof. intros n m p q H1 H2. destruct (NZle_gt_cases p q); [assumption |]. pose proof (NZplus_lt_le_mono q p n m H H1) as H3. apply <- NZnle_gt in H3. @@ -370,4 +401,14 @@ elimtype False; now apply (NZlt_asymm (n * m) 0). now apply NZtimes_neg_pos. now apply NZtimes_pos_neg. Qed. +Theorem NZtimes_2_mono_l : forall n m : NZ, n < m -> 1 + (1 + 1) * n < (1 + 1) * m. +Proof. +intros n m H. apply -> NZlt_le_succ in H. +apply -> (NZtimes_le_mono_pos_l (S n) m (1 + 1)) in H. +repeat rewrite NZtimes_plus_distr_r in *; repeat rewrite NZtimes_1_l in *. +repeat rewrite NZplus_succ_r in *. repeat rewrite NZplus_succ_l in *. rewrite NZplus_0_l. +now apply <- NZlt_le_succ. +apply NZplus_pos_pos; now apply NZlt_succ_r. +Qed. + End NZTimesOrderPropFunct. diff --git a/theories/Numbers/Natural/Abstract/NOrder.v b/theories/Numbers/Natural/Abstract/NOrder.v index f62b5ecb2a..7c2610ccc6 100644 --- a/theories/Numbers/Natural/Abstract/NOrder.v +++ b/theories/Numbers/Natural/Abstract/NOrder.v @@ -25,6 +25,9 @@ Proof NZlt_le_incl. Theorem lt_neq : forall n m : N, n < m -> n ~= m. Proof NZlt_neq. +Theorem lt_le_neq : forall n m : N, n < m <-> n <= m /\ n ~= m. +Proof NZlt_le_neq. + Theorem le_refl : forall n : N, n <= n. Proof NZle_refl. diff --git a/theories/Numbers/Natural/Abstract/NPlusOrder.v b/theories/Numbers/Natural/Abstract/NPlusOrder.v deleted file mode 100644 index c4640858e0..0000000000 --- a/theories/Numbers/Natural/Abstract/NPlusOrder.v +++ /dev/null @@ -1,87 +0,0 @@ -Require Export NPlus. -Require Export NOrder. -Require Import NZPlusOrder. - -Module NPlusOrderPropFunct - (Import NPlusMod : NPlusSig) - (Import NOrderMod : NOrderSig with Module NAxiomsMod := NPlusMod.NAxiomsMod). -Module Export NPlusPropMod := NPlusPropFunct NPlusMod. -Module Export NOrderPropMod := NOrderPropFunct NOrderMod. -Module Export NZPlusOrderPropMod := NZPlusOrderPropFunct NZPlusMod NZOrderMod. -Open Local Scope NatScope. - -(* Print All locks up here !!! *) -Theorem lt_plus_trans : forall n m p, n < m -> n < m + p. -Proof. -intros n m p; induct p. -now rewrite plus_0_r. -intros x IH H. -rewrite plus_succ_r. apply lt_closed_succ. apply IH; apply H. -Qed. - -Theorem plus_lt_compat_l : forall n m p, n < m -> p + n < p + m. -Proof. -intros n m p H; induct p. -do 2 rewrite plus_0_l; assumption. -intros x IH. do 2 rewrite plus_succ_l. now apply <- lt_resp_succ. -Qed. - -Theorem plus_lt_compat_r : forall n m p, n < m -> n + p < m + p. -Proof. -intros n m p H; rewrite plus_comm. -set (k := p + n); rewrite plus_comm; unfold k; clear k. -now apply plus_lt_compat_l. -Qed. - -Theorem plus_lt_compat : forall n m p q, n < m -> p < q -> n + p < m + q. -Proof. -intros n m p q H1 H2. -apply lt_trans with (m := m + p); -[now apply plus_lt_compat_r | now apply plus_lt_compat_l]. -Qed. - -Theorem plus_lt_cancel_l : forall p n m, p + n < p + m <-> n < m. -Proof. -intros p n m; induct p. -now do 2 rewrite plus_0_l. -intros p IH. -do 2 rewrite plus_succ_l. now rewrite lt_resp_succ. -Qed. - -Theorem plus_lt_cancel_r : forall p n m, n + p < m + p <-> n < m. -Proof. -intros p n m; -setoid_replace (n + p) with (p + n) by apply plus_comm; -setoid_replace (m + p) with (p + m) by apply plus_comm; -apply plus_lt_cancel_l. -Qed. - -(* The following property is similar to plus_repl_pair in NPlus.v -and is used to prove the correctness of the definition of order -on integers constructed from pairs of natural numbers *) - -Theorem plus_lt_repl_pair : forall n m n' m' u v, - n + u < m + v -> n + m' == n' + m -> n' + u < m' + v. -Proof. -intros n m n' m' u v H1 H2. -apply <- (plus_lt_cancel_r (n + m')) in H1. -set (k := n + m') in H1 at 2; rewrite H2 in H1; unfold k in H1; clear k. -rewrite <- plus_assoc in H1. -setoid_replace (m + v + (n + m')) with (n + m' + (m + v)) in H1 by apply plus_comm. -rewrite <- plus_assoc in H1. apply -> plus_lt_cancel_l in H1. -rewrite plus_assoc in H1. setoid_replace (m + v) with (v + m) in H1 by apply plus_comm. -rewrite plus_assoc in H1. apply -> plus_lt_cancel_r in H1. -now rewrite plus_comm in H1. -Qed. - -Theorem plus_gt_succ : - forall n m p, S p < n + m -> (exists n', n == S n') \/ (exists m', m == S m'). -Proof. -intros n m p H. -apply <- lt_le_succ in H. -apply lt_exists_pred in H. destruct H as [q H]. -now apply plus_eq_succ in H. -Qed. - -End NPlusOrderProperties. - diff --git a/theories/Numbers/Natural/Abstract/NTimesOrder.v b/theories/Numbers/Natural/Abstract/NTimesOrder.v index 2dbfd8f977..dc1b977aa4 100644 --- a/theories/Numbers/Natural/Abstract/NTimesOrder.v +++ b/theories/Numbers/Natural/Abstract/NTimesOrder.v @@ -28,22 +28,31 @@ Proof NZplus_lt_le_mono. Theorem plus_le_lt_mono : forall n m p q : N, n <= m -> p < q -> n + p < m + q. Proof NZplus_le_lt_mono. +Theorem plus_pos_pos : forall n m : N, 0 < n -> 0 < m -> 0 < n + m. +Proof NZplus_pos_pos. + +Theorem lt_plus_pos_l : forall n m : N, 0 < n -> m < n + m. +Proof NZlt_plus_pos_l. + +Theorem lt_plus_pos_r : forall n m : N, 0 < n -> m < m + n. +Proof NZlt_plus_pos_r. + Theorem le_lt_plus_lt : forall n m p q : N, n <= m -> p + m < q + n -> p < q. Proof NZle_lt_plus_lt. Theorem lt_le_plus_lt : forall n m p q : N, n < m -> p + m <= q + n -> p < q. Proof NZlt_le_plus_lt. -Theorem le_le_plus_lt : forall n m p q : N, n <= m -> p + m <= q + n -> p <= q. -Proof NZle_le_plus_lt. +Theorem le_le_plus_le : forall n m p q : N, n <= m -> p + m <= q + n -> p <= q. +Proof NZle_le_plus_le. Theorem plus_lt_cases : forall n m p q : N, n + m < p + q -> n < p \/ m < q. Proof NZplus_lt_cases. -Theorem plus_le_cases : forall n m p q : NZ, n + m <= p + q -> n <= p \/ m <= q. +Theorem plus_le_cases : forall n m p q : N, n + m <= p + q -> n <= p \/ m <= q. Proof NZplus_le_cases. -Theorem plus_pos_cases : forall n m : NZ, 0 < n + m -> 0 < n \/ 0 < m. +Theorem plus_pos_cases : forall n m : N, 0 < n + m -> 0 < n \/ 0 < m. Proof NZplus_pos_cases. (** Theorems true for natural numbers *) @@ -55,17 +64,25 @@ rewrite plus_0_r; le_equal. intros m IH. rewrite plus_succ_r; now apply le_le_succ. Qed. -Theorem lt_plus_r : forall n m : N, m ~= 0 -> n < n + m. +Theorem lt_lt_plus_r : forall n m p : N, n < m -> n < m + p. Proof. -intros n m; cases m. -intro H; elimtype False; now apply H. -intros. rewrite plus_succ_r. apply <- lt_succ_le. apply le_plus_r. +intros n m p H; rewrite <- (plus_0_r n). +apply plus_lt_le_mono; [assumption | apply le_0_l]. Qed. -Theorem lt_lt_plus : forall n m p : N, n < m -> n < m + p. +Theorem lt_lt_plus_l : forall n m p : N, n < m -> n < p + m. Proof. -intros n m p H; rewrite <- (plus_0_r n). -apply plus_lt_le_mono; [assumption | apply le_0_l]. +intros n m p; rewrite plus_comm; apply lt_lt_plus_r. +Qed. + +Theorem plus_pos_l : forall n m : N, 0 < n -> 0 < n + m. +Proof. +intros; apply NZplus_pos_nonneg. assumption. apply le_0_l. +Qed. + +Theorem plus_pos_r : forall n m : N, 0 < m -> 0 < n + m. +Proof. +intros; apply NZplus_nonneg_pos. apply le_0_l. assumption. Qed. (* The following property is similar to plus_repl_pair in NPlus.v @@ -123,7 +140,7 @@ Proof. intros; apply NZtimes_le_mono; try assumption; apply le_0_l. Qed. -Theorem times_pos_pos : forall n m : N, 0 < n -> 0 < m -> 0 < n * m. +Theorem Ztimes_pos_pos : forall n m : N, 0 < n -> 0 < m -> 0 < n * m. Proof NZtimes_pos_pos. Theorem times_eq_0 : forall n m : N, n * m == 0 -> n == 0 \/ m == 0. @@ -132,11 +149,14 @@ Proof NZtimes_eq_0. Theorem times_neq_0 : forall n m : N, n ~= 0 /\ m ~= 0 <-> n * m ~= 0. Proof NZtimes_neq_0. +Theorem times_2_mono_l : forall n m : N, n < m -> 1 + (1 + 1) * n < (1 + 1) * m. +Proof NZtimes_2_mono_l. + Theorem times_pos : forall n m : N, n * m > 0 <-> n > 0 /\ m > 0. Proof. intros n m; split; [intro H | intros [H1 H2]]. apply -> NZtimes_pos in H. destruct H as [[H1 H2] | [H1 H2]]. now split. false_hyp H1 nlt_0_r. -now apply times_pos_pos. +now apply NZtimes_pos_pos. Qed. End NTimesOrderPropFunct. |