diff options
| -rw-r--r-- | Makefile.common | 1 | ||||
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZBase.v | 9 | ||||
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZLt.v | 28 | ||||
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZPlusOrder.v | 21 | ||||
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZTimesOrder.v | 145 | ||||
| -rw-r--r-- | theories/Numbers/NatInt/NZOrder.v | 10 | ||||
| -rw-r--r-- | theories/Numbers/NatInt/NZPlusOrder.v | 166 | ||||
| -rw-r--r-- | theories/Numbers/NatInt/NZTimesOrder.v | 225 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NBase.v | 9 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NOrder.v | 6 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NTimesOrder.v | 24 |
11 files changed, 430 insertions, 214 deletions
diff --git a/Makefile.common b/Makefile.common index 474296232..22466fe10 100644 --- a/Makefile.common +++ b/Makefile.common @@ -656,6 +656,7 @@ NATINTVO:=\ $(NATINTDIR)/NZPlus.vo\ $(NATINTDIR)/NZTimes.vo\ $(NATINTDIR)/NZOrder.vo\ + $(NATINTDIR)/NZPlusOrder.vo\ $(NATINTDIR)/NZTimesOrder.vo NATURALDIR:=$(NUMBERSDIR)/Natural diff --git a/theories/Numbers/Integer/Abstract/ZBase.v b/theories/Numbers/Integer/Abstract/ZBase.v index db5bc99f9..0813a3caa 100644 --- a/theories/Numbers/Integer/Abstract/ZBase.v +++ b/theories/Numbers/Integer/Abstract/ZBase.v @@ -33,6 +33,15 @@ Proof NZpred_wd. Theorem Zpred_succ : forall n : Z, P (S n) == n. Proof NZpred_succ. +Theorem Zeq_refl : forall n : Z, n == n. +Proof (proj1 NZeq_equiv). + +Theorem Zeq_symm : forall n m : Z, n == m -> m == n. +Proof (proj2 (proj2 NZeq_equiv)). + +Theorem Zeq_trans : forall n m p : Z, n == m -> m == p -> n == p. +Proof (proj1 (proj2 NZeq_equiv)). + Theorem Zneq_symm : forall n m : Z, n ~= m -> m ~= n. Proof NZneq_symm. diff --git a/theories/Numbers/Integer/Abstract/ZLt.v b/theories/Numbers/Integer/Abstract/ZLt.v index a81b3a419..27cbe085e 100644 --- a/theories/Numbers/Integer/Abstract/ZLt.v +++ b/theories/Numbers/Integer/Abstract/ZLt.v @@ -75,6 +75,12 @@ Proof NZlt_succ_diag_r. Theorem Zle_succ_diag_r : forall n : Z, n <= S n. Proof NZle_succ_diag_r. +Theorem Zlt_0_1 : 0 < 1. +Proof NZlt_0_1. + +Theorem Zle_0_1 : 0 <= 1. +Proof NZle_0_1. + Theorem Zlt_lt_succ_r : forall n m : Z, n < m -> n < S m. Proof NZlt_lt_succ_r. @@ -150,6 +156,28 @@ Proof NZlt_ge_cases. Theorem Zle_ge_cases : forall n m : Z, n <= m \/ n >= m. Proof NZle_ge_cases. +(** Instances of the previous theorems for m == 0 *) + +Theorem Zneg_pos_cases : forall n : Z, n ~= 0 <-> n < 0 \/ n > 0. +Proof. +intro; apply Zlt_gt_cases. +Qed. + +Theorem Znonpos_pos_cases : forall n : Z, n <= 0 \/ n > 0. +Proof. +intro; apply Zle_gt_cases. +Qed. + +Theorem Zneg_nonneg_cases : forall n : Z, n < 0 \/ n >= 0. +Proof. +intro; apply Zlt_ge_cases. +Qed. + +Theorem Znonpos_nonneg_cases : forall n : Z, n <= 0 \/ n >= 0. +Proof. +intro; apply Zle_ge_cases. +Qed. + Theorem Zle_ngt : forall n m : Z, n <= m <-> ~ n > m. Proof NZle_ngt. diff --git a/theories/Numbers/Integer/Abstract/ZPlusOrder.v b/theories/Numbers/Integer/Abstract/ZPlusOrder.v index ce79055a7..c6d0efe45 100644 --- a/theories/Numbers/Integer/Abstract/ZPlusOrder.v +++ b/theories/Numbers/Integer/Abstract/ZPlusOrder.v @@ -89,6 +89,27 @@ Proof NZplus_nonneg_cases. (** Theorems that are either not valid on N or have different proofs on N and Z *) +Theorem Zplus_neg_neg : forall n m : Z, n < 0 -> m < 0 -> n + m < 0. +Proof. +intros n m H1 H2. rewrite <- (Zplus_0_l 0). now apply Zplus_lt_mono. +Qed. + +Theorem Zplus_neg_nonpos : forall n m : Z, n < 0 -> m <= 0 -> n + m < 0. +Proof. +intros n m H1 H2. rewrite <- (Zplus_0_l 0). now apply Zplus_lt_le_mono. +Qed. + +Theorem Zplus_nonpos_neg : forall n m : Z, n <= 0 -> m < 0 -> n + m < 0. +Proof. +intros n m H1 H2. rewrite <- (Zplus_0_l 0). now apply Zplus_le_lt_mono. +Qed. + +Theorem Zplus_nonpos_nonpos : forall n m : Z, n <= 0 -> m <= 0 -> n + m <= 0. +Proof. +intros n m H1 H2. rewrite <- (Zplus_0_l 0). now apply Zplus_le_mono. +Qed. + + (** Minus and order *) Theorem Zlt_lt_minus : forall n m : Z, n < m <-> 0 < m - n. diff --git a/theories/Numbers/Integer/Abstract/ZTimesOrder.v b/theories/Numbers/Integer/Abstract/ZTimesOrder.v index 287fdb7f1..a2360dd72 100644 --- a/theories/Numbers/Integer/Abstract/ZTimesOrder.v +++ b/theories/Numbers/Integer/Abstract/ZTimesOrder.v @@ -64,37 +64,66 @@ 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 : +Theorem Ztimes_lt_mono_nonneg : forall n m p q : Z, 0 <= n -> n < m -> 0 <= p -> p < q -> n * p < m * q. -Proof NZtimes_lt_mono. +Proof NZtimes_lt_mono_nonneg. -Theorem Ztimes_le_mono : +Theorem Ztimes_lt_mono_nonpos : + forall n m p q : Z, m <= 0 -> n < m -> q <= 0 -> p < q -> m * q < n * p. +Proof. +intros n m p q H1 H2 H3 H4. +apply Zle_lt_trans with (m * p). +apply Ztimes_le_mono_nonpos_l; [assumption | now apply Zlt_le_incl]. +apply -> Ztimes_lt_mono_neg_r; [assumption | now apply Zlt_le_trans with q]. +Qed. + +Theorem Ztimes_le_mono_nonneg : forall n m p q : Z, 0 <= n -> n <= m -> 0 <= p -> p <= q -> n * p <= m * q. -Proof NZtimes_le_mono. +Proof NZtimes_le_mono_nonneg. + +Theorem Ztimes_le_mono_nonpos : + forall n m p q : Z, m <= 0 -> n <= m -> q <= 0 -> p <= q -> m * q <= n * p. +Proof. +intros n m p q H1 H2 H3 H4. +apply Zle_trans with (m * p). +now apply Ztimes_le_mono_nonpos_l. +apply Ztimes_le_mono_nonpos_r; [now apply Zle_trans with q | assumption]. +Qed. 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_nonneg_nonneg : forall n m : Z, 0 <= n -> 0 <= m -> 0 <= n * m. +Proof. +intros n m H1 H2. +rewrite <- (Ztimes_0_l m). now apply Ztimes_le_mono_nonneg_r. +Qed. + +Theorem Ztimes_nonpos_nonpos : forall n m : Z, n <= 0 -> m <= 0 -> 0 <= n * m. +Proof. +intros n m H1 H2. +rewrite <- (Ztimes_0_l m). now apply Ztimes_le_mono_nonpos_r. +Qed. + +Theorem Ztimes_nonneg_nonpos : forall n m : Z, 0 <= n -> m <= 0 -> n * m <= 0. +Proof. +intros n m H1 H2. +rewrite <- (Ztimes_0_l m). now apply Ztimes_le_mono_nonpos_r. +Qed. + Theorem Ztimes_nonpos_nonneg : forall n m : Z, n <= 0 -> 0 <= m -> n * m <= 0. -Proof NZtimes_nonpos_nonneg. +Proof. +intros; rewrite Ztimes_comm; now apply Ztimes_nonneg_nonpos. +Qed. Theorem Zlt_1_times_pos : forall n m : Z, 1 < n -> 0 < m -> 1 < n * m. Proof NZlt_1_times_pos. @@ -111,12 +140,90 @@ Proof NZeq_times_0_l. Theorem Zeq_times_0_r : forall n m : Z, n * m == 0 -> n ~= 0 -> m == 0. Proof NZeq_times_0_r. -Theorem Ztimes_pos : forall n m : Z, 0 < n * m <-> (0 < n /\ 0 < m) \/ (m < 0 /\ n < 0). -Proof NZtimes_pos. +Theorem Zlt_0_times : forall n m : Z, 0 < n * m <-> 0 < n /\ 0 < m \/ m < 0 /\ n < 0. +Proof NZlt_0_times. + +Notation Ztimes_pos := Zlt_0_times (only parsing). -Theorem Ztimes_neg : - forall n m : Z, n * m < 0 <-> (n < 0 /\ m > 0) \/ (n > 0 /\ m < 0). -Proof NZtimes_neg. +Theorem Zlt_times_0 : + forall n m : Z, n * m < 0 <-> n < 0 /\ m > 0 \/ n > 0 /\ m < 0. +Proof. +intros n m; split; [intro H | intros [[H1 H2] | [H1 H2]]]. +destruct (Zlt_trichotomy n 0) as [H1 | [H1 | H1]]; +[| rewrite H1 in H; rewrite Ztimes_0_l in H; false_hyp H Zlt_irrefl |]; +(destruct (Zlt_trichotomy m 0) as [H2 | [H2 | H2]]; +[| rewrite H2 in H; rewrite Ztimes_0_r in H; false_hyp H Zlt_irrefl |]); +try (left; now split); try (right; now split). +assert (H3 : n * m > 0) by now apply Ztimes_neg_neg. +elimtype False; now apply (Zlt_asymm (n * m) 0). +assert (H3 : n * m > 0) by now apply Ztimes_pos_pos. +elimtype False; now apply (Zlt_asymm (n * m) 0). +now apply Ztimes_neg_pos. now apply Ztimes_pos_neg. +Qed. + +Notation Ztimes_neg := Zlt_times_0 (only parsing). + +Theorem Zle_0_times : + forall n m : Z, 0 <= n * m -> 0 <= n /\ 0 <= m \/ n <= 0 /\ m <= 0. +Proof. +assert (R : forall n : Z, 0 == n <-> n == 0) by (intros; split; apply Zeq_symm). +intros n m. repeat rewrite Zlt_eq_cases. repeat rewrite R. +rewrite Zlt_0_times, Zeq_times_0. +pose proof (Zlt_trichotomy n 0); pose proof (Zlt_trichotomy m 0). tauto. +Qed. + +Notation Ztimes_nonneg := Zle_0_times (only parsing). + +Theorem Zle_times_0 : + forall n m : Z, n * m <= 0 -> 0 <= n /\ m <= 0 \/ n <= 0 /\ 0 <= m. +Proof. +assert (R : forall n : Z, 0 == n <-> n == 0) by (intros; split; apply Zeq_symm). +intros n m. repeat rewrite Zlt_eq_cases. repeat rewrite R. +rewrite Zlt_times_0, Zeq_times_0. +pose proof (Zlt_trichotomy n 0); pose proof (Zlt_trichotomy m 0). tauto. +Qed. + +Notation Ztimes_nonpos := Zle_times_0 (only parsing). + +Theorem Zsquare_lt_mono_nonneg : forall n m : Z, 0 <= n -> n < m -> n * n < m * m. +Proof NZsquare_lt_mono_nonneg. + +Theorem Zsquare_lt_mono_nonpos : forall n m : Z, n <= 0 -> m < n -> n * n < m * m. +Proof. +intros n m H1 H2. now apply Ztimes_lt_mono_nonpos. +Qed. + +Theorem Zsquare_le_mono_nonneg : forall n m : Z, 0 <= n -> n <= m -> n * n <= m * m. +Proof NZsquare_le_mono_nonneg. + +Theorem Zsquare_le_mono_nonpos : forall n m : Z, n <= 0 -> m <= n -> n * n <= m * m. +Proof. +intros n m H1 H2. now apply Ztimes_le_mono_nonpos. +Qed. + +Theorem Zsquare_lt_simpl_nonneg : forall n m : Z, 0 <= m -> n * n < m * m -> n < m. +Proof NZsquare_lt_simpl_nonneg. + +Theorem Zsquare_le_simpl_nonneg : forall n m : Z, 0 <= m -> n * n <= m * m -> n <= m. +Proof NZsquare_le_simpl_nonneg. + +Theorem Zsquare_lt_simpl_nonpos : forall n m : Z, m <= 0 -> n * n < m * m -> m < n. +Proof. +intros n m H1 H2. destruct (Zle_gt_cases n 0). +destruct (NZlt_ge_cases m n). +assumption. assert (F : m * m <= n * n) by now apply Zsquare_le_mono_nonpos. +apply -> NZle_ngt in F. false_hyp H2 F. +now apply Zle_lt_trans with 0. +Qed. + +Theorem Zsquare_le_simpl_nonpos : forall n m : NZ, m <= 0 -> n * n <= m * m -> m <= n. +Proof. +intros n m H1 H2. destruct (NZle_gt_cases n 0). +destruct (NZle_gt_cases m n). +assumption. assert (F : m * m < n * n) by now apply Zsquare_lt_mono_nonpos. +apply -> NZlt_nge in F. false_hyp H2 F. +apply Zlt_le_incl; now apply NZle_lt_trans with 0. +Qed. Theorem Ztimes_2_mono_l : forall n m : Z, n < m -> 1 + (1 + 1) * n < (1 + 1) * m. Proof NZtimes_2_mono_l. diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v index df2f224f4..95df8e747 100644 --- a/theories/Numbers/NatInt/NZOrder.v +++ b/theories/Numbers/NatInt/NZOrder.v @@ -82,6 +82,16 @@ Proof. intro; apply NZlt_le_incl; apply NZlt_succ_diag_r. Qed. +Theorem NZlt_0_1 : 0 < 1. +Proof. +apply NZlt_succ_diag_r. +Qed. + +Theorem NZle_0_1 : 0 <= 1. +Proof. +apply NZle_succ_diag_r. +Qed. + Theorem NZlt_lt_succ_r : forall n m : NZ, n < m -> n < S m. Proof. intros. rewrite NZlt_succ_r. now apply NZlt_le_incl. diff --git a/theories/Numbers/NatInt/NZPlusOrder.v b/theories/Numbers/NatInt/NZPlusOrder.v new file mode 100644 index 000000000..9f1ba0f84 --- /dev/null +++ b/theories/Numbers/NatInt/NZPlusOrder.v @@ -0,0 +1,166 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +(* Evgeny Makarov, INRIA, 2007 *) +(************************************************************************) + +(*i i*) + +Require Import NZAxioms. +Require Import NZOrder. + +Module NZPlusOrderPropFunct (Import NZOrdAxiomsMod : NZOrdAxiomsSig). +Module Export NZOrderPropMod := NZOrderPropFunct NZOrdAxiomsMod. +Open Local Scope NatIntScope. + +Theorem NZplus_lt_mono_l : forall n m p : NZ, 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 : NZ, 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 : NZ, 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 : NZ, 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 : NZ, 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 : NZ, 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 : NZ, 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 : NZ, 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. + +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]. +pose proof (NZplus_le_mono q p n m H H1) as H3. apply <- NZnle_gt in H2. +false_hyp H3 H2. +Qed. + +Theorem NZlt_le_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]. +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_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. +false_hyp H2 H3. +Qed. + +Theorem NZplus_lt_cases : forall n m p q : NZ, n + m < p + q -> n < p \/ m < q. +Proof. +intros n m p q H; +destruct (NZle_gt_cases p n) as [H1 | H1]. +destruct (NZle_gt_cases q m) as [H2 | H2]. +pose proof (NZplus_le_mono p n q m H1 H2) as H3. apply -> NZle_ngt in H3. +false_hyp H H3. +now right. now left. +Qed. + +Theorem NZplus_le_cases : forall n m p q : NZ, n + m <= p + q -> n <= p \/ m <= q. +Proof. +intros n m p q H. +destruct (NZle_gt_cases n p) as [H1 | H1]. now left. +destruct (NZle_gt_cases m q) as [H2 | H2]. now right. +assert (H3 : p + q < n + m) by now apply NZplus_lt_mono. +apply -> NZle_ngt in H. false_hyp H3 H. +Qed. + +Theorem NZplus_neg_cases : forall n m : NZ, n + m < 0 -> n < 0 \/ m < 0. +Proof. +intros n m H; apply NZplus_lt_cases; now rewrite NZplus_0_l. +Qed. + +Theorem NZplus_pos_cases : forall n m : NZ, 0 < n + m -> 0 < n \/ 0 < m. +Proof. +intros n m H; apply NZplus_lt_cases; now rewrite NZplus_0_l. +Qed. + +Theorem NZplus_nonpos_cases : forall n m : NZ, n + m <= 0 -> n <= 0 \/ m <= 0. +Proof. +intros n m H; apply NZplus_le_cases; now rewrite NZplus_0_l. +Qed. + +Theorem NZplus_nonneg_cases : forall n m : NZ, 0 <= n + m -> 0 <= n \/ 0 <= m. +Proof. +intros n m H; apply NZplus_le_cases; now rewrite NZplus_0_l. +Qed. + +End NZPlusOrderPropFunct. + diff --git a/theories/Numbers/NatInt/NZTimesOrder.v b/theories/Numbers/NatInt/NZTimesOrder.v index 4b4516069..aac823dc4 100644 --- a/theories/Numbers/NatInt/NZTimesOrder.v +++ b/theories/Numbers/NatInt/NZTimesOrder.v @@ -11,161 +11,12 @@ (*i i*) Require Import NZAxioms. -Require Import NZOrder. +Require Import NZPlusOrder. Module NZTimesOrderPropFunct (Import NZOrdAxiomsMod : NZOrdAxiomsSig). -Module Export NZOrderPropMod := NZOrderPropFunct NZOrdAxiomsMod. +Module Export NZPlusOrderPropMod := NZPlusOrderPropFunct NZOrdAxiomsMod. Open Local Scope NatIntScope. -(** Addition and order *) - -Theorem NZplus_lt_mono_l : forall n m p : NZ, 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 : NZ, 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 : NZ, 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 : NZ, 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 : NZ, 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 : NZ, 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 : NZ, 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 : NZ, 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. - -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]. -pose proof (NZplus_le_mono q p n m H H1) as H3. apply <- NZnle_gt in H2. -false_hyp H3 H2. -Qed. - -Theorem NZlt_le_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]. -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_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. -false_hyp H2 H3. -Qed. - -Theorem NZplus_lt_cases : forall n m p q : NZ, n + m < p + q -> n < p \/ m < q. -Proof. -intros n m p q H; -destruct (NZle_gt_cases p n) as [H1 | H1]. -destruct (NZle_gt_cases q m) as [H2 | H2]. -pose proof (NZplus_le_mono p n q m H1 H2) as H3. apply -> NZle_ngt in H3. -false_hyp H H3. -now right. now left. -Qed. - -Theorem NZplus_le_cases : forall n m p q : NZ, n + m <= p + q -> n <= p \/ m <= q. -Proof. -intros n m p q H. -destruct (NZle_gt_cases n p) as [H1 | H1]. now left. -destruct (NZle_gt_cases m q) as [H2 | H2]. now right. -assert (H3 : p + q < n + m) by now apply NZplus_lt_mono. -apply -> NZle_ngt in H. false_hyp H3 H. -Qed. - -Theorem NZplus_neg_cases : forall n m : NZ, n + m < 0 -> n < 0 \/ m < 0. -Proof. -intros n m H; apply NZplus_lt_cases; now rewrite NZplus_0_l. -Qed. - -Theorem NZplus_pos_cases : forall n m : NZ, 0 < n + m -> 0 < n \/ 0 < m. -Proof. -intros n m H; apply NZplus_lt_cases; now rewrite NZplus_0_l. -Qed. - -Theorem NZplus_nonpos_cases : forall n m : NZ, n + m <= 0 -> n <= 0 \/ m <= 0. -Proof. -intros n m H; apply NZplus_le_cases; now rewrite NZplus_0_l. -Qed. - -Theorem NZplus_nonneg_cases : forall n m : NZ, 0 <= n + m -> 0 <= n \/ 0 <= m. -Proof. -intros n m H; apply NZplus_le_cases; now rewrite NZplus_0_l. -Qed. - -(** Multiplication and order *) - Theorem NZtimes_lt_pred : forall p q n m : NZ, S p == q -> (p * n < p * m <-> q * n + m < q * m + n). Proof. @@ -299,7 +150,7 @@ intros n m p. rewrite (NZtimes_comm n p); rewrite (NZtimes_comm m p); apply NZtimes_le_mono_neg_l. Qed. -Theorem NZtimes_lt_mono : +Theorem NZtimes_lt_mono_nonneg : forall n m p q : NZ, 0 <= n -> n < m -> 0 <= p -> p < q -> n * p < m * q. Proof. intros n m p q H1 H2 H3 H4. @@ -311,12 +162,12 @@ Qed. (* There are still many variants of the theorem above. One can assume 0 < n or 0 < p or n <= m or p <= q. *) -Theorem NZtimes_le_mono : +Theorem NZtimes_le_mono_nonneg : forall n m p q : NZ, 0 <= n -> n <= m -> 0 <= p -> p <= q -> n * p <= m * q. Proof. intros n m p q H1 H2 H3 H4. le_elim H2; le_elim H4. -apply NZlt_le_incl; now apply NZtimes_lt_mono. +apply NZlt_le_incl; now apply NZtimes_lt_mono_nonneg. rewrite <- H4; apply NZtimes_le_mono_nonneg_r; [assumption | now apply NZlt_le_incl]. rewrite <- H2; apply NZtimes_le_mono_nonneg_l; [assumption | now apply NZlt_le_incl]. rewrite H2; rewrite H4; now apply NZeq_le_incl. @@ -328,46 +179,23 @@ intros n m H1 H2. rewrite <- (NZtimes_0_l m). now apply -> NZtimes_lt_mono_pos_r. Qed. -Theorem NZtimes_nonneg_nonneg : forall n m : NZ, 0 <= n -> 0 <= m -> 0 <= n * m. -Proof. -intros n m H1 H2. -rewrite <- (NZtimes_0_l m). now apply NZtimes_le_mono_nonneg_r. -Qed. - Theorem NZtimes_neg_neg : forall n m : NZ, n < 0 -> m < 0 -> 0 < n * m. Proof. intros n m H1 H2. rewrite <- (NZtimes_0_l m). now apply -> NZtimes_lt_mono_neg_r. Qed. -Theorem NZtimes_nonpos_nonpos : forall n m : NZ, n <= 0 -> m <= 0 -> 0 <= n * m. -Proof. -intros n m H1 H2. -rewrite <- (NZtimes_0_l m). now apply NZtimes_le_mono_nonpos_r. -Qed. - Theorem NZtimes_pos_neg : forall n m : NZ, 0 < n -> m < 0 -> n * m < 0. Proof. intros n m H1 H2. rewrite <- (NZtimes_0_l m). now apply -> NZtimes_lt_mono_neg_r. Qed. -Theorem NZtimes_nonneg_nonpos : forall n m : NZ, 0 <= n -> m <= 0 -> n * m <= 0. -Proof. -intros n m H1 H2. -rewrite <- (NZtimes_0_l m). now apply NZtimes_le_mono_nonpos_r. -Qed. - Theorem NZtimes_neg_pos : forall n m : NZ, n < 0 -> 0 < m -> n * m < 0. Proof. intros; rewrite NZtimes_comm; now apply NZtimes_pos_neg. Qed. -Theorem NZtimes_nonpos_nonneg : forall n m : NZ, n <= 0 -> 0 <= m -> n * m <= 0. -Proof. -intros; rewrite NZtimes_comm; now apply NZtimes_nonneg_nonpos. -Qed. - Theorem NZlt_1_times_pos : forall n m : NZ, 1 < n -> 0 < m -> 1 < n * m. Proof. intros n m H1 H2. apply -> (NZtimes_lt_mono_pos_r m) in H1. @@ -408,7 +236,7 @@ intros n m H1 H2; apply -> NZeq_times_0 in H1. destruct H1 as [H1 | H1]. false_hyp H1 H2. assumption. Qed. -Theorem NZtimes_pos : forall n m : NZ, 0 < n * m <-> (0 < n /\ 0 < m) \/ (m < 0 /\ n < 0). +Theorem NZlt_0_times : forall n m : NZ, 0 < n * m <-> (0 < n /\ 0 < m) \/ (m < 0 /\ n < 0). Proof. intros n m; split; [intro H | intros [[H1 H2] | [H1 H2]]]. destruct (NZlt_trichotomy n 0) as [H1 | [H1 | H1]]; @@ -423,20 +251,35 @@ elimtype False; now apply (NZlt_asymm (n * m) 0). now apply NZtimes_pos_pos. now apply NZtimes_neg_neg. Qed. -Theorem NZtimes_neg : - forall n m : NZ, n * m < 0 <-> (n < 0 /\ m > 0) \/ (n > 0 /\ m < 0). +Theorem NZsquare_lt_mono_nonneg : forall n m : NZ, 0 <= n -> n < m -> n * n < m * m. Proof. -intros n m; split; [intro H | intros [[H1 H2] | [H1 H2]]]. -destruct (NZlt_trichotomy n 0) as [H1 | [H1 | H1]]; -[| rewrite H1 in H; rewrite NZtimes_0_l in H; false_hyp H NZlt_irrefl |]; -(destruct (NZlt_trichotomy m 0) as [H2 | [H2 | H2]]; -[| rewrite H2 in H; rewrite NZtimes_0_r in H; false_hyp H NZlt_irrefl |]); -try (left; now split); try (right; now split). -assert (H3 : n * m > 0) by now apply NZtimes_neg_neg. -elimtype False; now apply (NZlt_asymm (n * m) 0). -assert (H3 : n * m > 0) by now apply NZtimes_pos_pos. -elimtype False; now apply (NZlt_asymm (n * m) 0). -now apply NZtimes_neg_pos. now apply NZtimes_pos_neg. +intros n m H1 H2. now apply NZtimes_lt_mono_nonneg. +Qed. + +Theorem NZsquare_le_mono_nonneg : forall n m : NZ, 0 <= n -> n <= m -> n * n <= m * m. +Proof. +intros n m H1 H2. now apply NZtimes_le_mono_nonneg. +Qed. + +(* The converse theorems require nonnegativity (or nonpositivity) of the +other variable *) + +Theorem NZsquare_lt_simpl_nonneg : forall n m : NZ, 0 <= m -> n * n < m * m -> n < m. +Proof. +intros n m H1 H2. destruct (NZlt_ge_cases n 0). +now apply NZlt_le_trans with 0. +destruct (NZlt_ge_cases n m). +assumption. assert (F : m * m <= n * n) by now apply NZsquare_le_mono_nonneg. +apply -> NZle_ngt in F. false_hyp H2 F. +Qed. + +Theorem NZsquare_le_simpl_nonneg : forall n m : NZ, 0 <= m -> n * n <= m * m -> n <= m. +Proof. +intros n m H1 H2. destruct (NZlt_ge_cases n 0). +apply NZlt_le_incl; now apply NZlt_le_trans with 0. +destruct (NZle_gt_cases n m). +assumption. assert (F : m * m < n * n) by now apply NZsquare_lt_mono_nonneg. +apply -> NZlt_nge in F. false_hyp H2 F. Qed. Theorem NZtimes_2_mono_l : forall n m : NZ, n < m -> 1 + (1 + 1) * n < (1 + 1) * m. diff --git a/theories/Numbers/Natural/Abstract/NBase.v b/theories/Numbers/Natural/Abstract/NBase.v index bcef66867..956eca896 100644 --- a/theories/Numbers/Natural/Abstract/NBase.v +++ b/theories/Numbers/Natural/Abstract/NBase.v @@ -45,6 +45,15 @@ Proof NZpred_succ. Theorem pred_0 : P 0 == 0. Proof pred_0. +Theorem Neq_refl : forall n : N, n == n. +Proof (proj1 NZeq_equiv). + +Theorem Neq_symm : forall n m : N, n == m -> m == n. +Proof (proj2 (proj2 NZeq_equiv)). + +Theorem Neq_trans : forall n m p : N, n == m -> m == p -> n == p. +Proof (proj1 (proj2 NZeq_equiv)). + Theorem neq_symm : forall n m : N, n ~= m -> m ~= n. Proof NZneq_symm. diff --git a/theories/Numbers/Natural/Abstract/NOrder.v b/theories/Numbers/Natural/Abstract/NOrder.v index 33214cd1b..c7b7d495f 100644 --- a/theories/Numbers/Natural/Abstract/NOrder.v +++ b/theories/Numbers/Natural/Abstract/NOrder.v @@ -80,6 +80,12 @@ Proof NZlt_succ_diag_r. Theorem le_succ_diag_r : forall n : N, n <= S n. Proof NZle_succ_diag_r. +Theorem lt_0_1 : 0 < 1. +Proof NZlt_0_1. + +Theorem le_0_1 : 0 <= 1. +Proof NZle_0_1. + Theorem lt_lt_succ_r : forall n m : N, n < m -> n < S m. Proof NZlt_lt_succ_r. diff --git a/theories/Numbers/Natural/Abstract/NTimesOrder.v b/theories/Numbers/Natural/Abstract/NTimesOrder.v index d6c0bfafa..502f99417 100644 --- a/theories/Numbers/Natural/Abstract/NTimesOrder.v +++ b/theories/Numbers/Natural/Abstract/NTimesOrder.v @@ -56,6 +56,20 @@ Proof NZeq_times_0_l. Theorem eq_times_0_r : forall n m : N, n * m == 0 -> n ~= 0 -> m == 0. Proof NZeq_times_0_r. +Theorem square_lt_mono : forall n m : N, n < m <-> n * n < m * m. +Proof. +intros n m; split; intro; +[apply NZsquare_lt_mono_nonneg | apply NZsquare_lt_simpl_nonneg]; +try assumption; apply le_0_l. +Qed. + +Theorem square_le_mono : forall n m : N, n <= m <-> n * n <= m * m. +Proof. +intros n m; split; intro; +[apply NZsquare_le_mono_nonneg | apply NZsquare_le_simpl_nonneg]; +try assumption; apply le_0_l. +Qed. + Theorem times_2_mono_l : forall n m : N, n < m -> 1 + (1 + 1) * n < (1 + 1) * m. Proof NZtimes_2_mono_l. @@ -73,21 +87,23 @@ Qed. Theorem times_lt_mono : forall n m p q : N, n < m -> p < q -> n * p < m * q. Proof. -intros; apply NZtimes_lt_mono; try assumption; apply le_0_l. +intros; apply NZtimes_lt_mono_nonneg; try assumption; apply le_0_l. Qed. Theorem times_le_mono : forall n m p q : N, n <= m -> p <= q -> n * p <= m * q. Proof. -intros; apply NZtimes_le_mono; try assumption; apply le_0_l. +intros; apply NZtimes_le_mono_nonneg; try assumption; apply le_0_l. Qed. -Theorem times_pos : forall n m : N, n * m > 0 <-> n > 0 /\ m > 0. +Theorem lt_0_times : 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. +apply -> NZlt_0_times in H. destruct H as [[H1 H2] | [H1 H2]]. now split. false_hyp H1 nlt_0_r. now apply NZtimes_pos_pos. Qed. +Notation times_pos := lt_0_times (only parsing). + Theorem eq_times_1 : forall n m : N, n * m == 1 <-> n == 1 /\ m == 1. Proof. intros n m. |