diff options
| author | emakarov | 2007-11-14 19:47:46 +0000 |
|---|---|---|
| committer | emakarov | 2007-11-14 19:47:46 +0000 |
| commit | 87bfa992d0373cd1bfeb046f5a3fc38775837e83 (patch) | |
| tree | 5a222411c15652daf51a6405e2334a44a9c95bea | |
| parent | d04ad26f4bb424581db2bbadef715fef491243b3 (diff) | |
Update on Numbers; renamed ZOrder.v to ZLt to remove clash with ZArith/Zorder on MacOS.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10323 85f007b7-540e-0410-9357-904b9bb8a0f7
24 files changed, 758 insertions, 539 deletions
diff --git a/Makefile.common b/Makefile.common index a28b456b98..032a6d5d0b 100644 --- a/Makefile.common +++ b/Makefile.common @@ -685,7 +685,7 @@ INTEGERABSTRACTVO:=\ $(INTABSTRACTDIR)/ZBase.vo\ $(INTABSTRACTDIR)/ZPlus.vo\ $(INTABSTRACTDIR)/ZTimes.vo\ - $(INTABSTRACTDIR)/ZOrder.vo\ + $(INTABSTRACTDIR)/ZLt.vo\ $(INTABSTRACTDIR)/ZPlusOrder.vo\ $(INTABSTRACTDIR)/ZTimesOrder.vo diff --git a/theories/Numbers/Integer/Abstract/ZAxioms.v b/theories/Numbers/Integer/Abstract/ZAxioms.v index e81cffe4f3..fdc7bab4cb 100644 --- a/theories/Numbers/Integer/Abstract/ZAxioms.v +++ b/theories/Numbers/Integer/Abstract/ZAxioms.v @@ -45,9 +45,13 @@ Notation "x >= y" := (NZle y x) (only parsing) : IntScope. Parameter Zopp : Z -> Z. +(*Notation "- 1" := (Zopp 1) : IntScope. +Check (-1).*) + Add Morphism Zopp with signature Zeq ==> Zeq as Zopp_wd. Notation "- x" := (Zopp x) (at level 35, right associativity) : IntScope. +Notation "- 1" := (Zopp (NZsucc NZ0)) : IntScope. Open Local Scope IntScope. diff --git a/theories/Numbers/Integer/Abstract/ZBase.v b/theories/Numbers/Integer/Abstract/ZBase.v index ace49428d2..db5bc99f92 100644 --- a/theories/Numbers/Integer/Abstract/ZBase.v +++ b/theories/Numbers/Integer/Abstract/ZBase.v @@ -10,10 +10,15 @@ (*i i*) +Require Export Decidable. Require Export ZAxioms. Require Import NZTimesOrder. -Module ZBasePropFunct (Export ZAxiomsMod : ZAxiomsSig). +Module ZBasePropFunct (Import ZAxiomsMod : ZAxiomsSig). + +(* Note: writing "Export" instead of "Import" on the previous line leads to +some warnings about hiding repeated declarations and results in the loss of +notations in Zplus and later *) Open Local Scope IntScope. @@ -43,8 +48,8 @@ Proof NZsucc_inj_wd_neg. (* Decidability and stability of equality was proved only in NZOrder, but since it does not mention order, we'll put it here *) -Theorem Zeq_em : forall n m : Z, n == m \/ n ~= m. -Proof NZeq_em. +Theorem Zeq_dec : forall n m : Z, decidable (n == m). +Proof NZeq_dec. Theorem Zeq_dne : forall n m : Z, ~ ~ n == m <-> n == m. Proof NZeq_dne. diff --git a/theories/Numbers/Integer/Abstract/ZOrder.v b/theories/Numbers/Integer/Abstract/ZLt.v index 9b452039cb..a81b3a4196 100644 --- a/theories/Numbers/Integer/Abstract/ZOrder.v +++ b/theories/Numbers/Integer/Abstract/ZLt.v @@ -34,14 +34,14 @@ Theorem Zmax_wd : forall n1 n2 : Z, n1 == n2 -> forall m1 m2 : Z, m1 == m2 -> Zmax n1 m1 == Zmax n2 m2. Proof NZmax_wd. -Theorem Zle_lt_or_eq : forall n m : Z, n <= m <-> n < m \/ n == m. -Proof NZle_lt_or_eq. +Theorem Zlt_eq_cases : forall n m : Z, n <= m <-> n < m \/ n == m. +Proof NZlt_eq_cases. Theorem Zlt_irrefl : forall n : Z, ~ n < n. Proof NZlt_irrefl. -Theorem Zlt_succ_le : forall n m : Z, n < S m <-> n <= m. -Proof NZlt_succ_le. +Theorem Zlt_succ_r : forall n m : Z, n < S m <-> n <= m. +Proof NZlt_succ_r. Theorem Zmin_l : forall n m : Z, n <= m -> Zmin n m == n. Proof NZmin_l. @@ -63,44 +63,44 @@ 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_neq : forall n m : Z, n < m <-> n <= m /\ n ~= m. +Proof NZle_neq. Theorem Zle_refl : forall n : Z, n <= n. Proof NZle_refl. -Theorem Zlt_succ_r : forall n : Z, n < S n. -Proof NZlt_succ_r. +Theorem Zlt_succ_diag_r : forall n : Z, n < S n. +Proof NZlt_succ_diag_r. -Theorem Zle_succ_r : forall n : Z, n <= S n. -Proof NZle_succ_r. +Theorem Zle_succ_diag_r : forall n : Z, n <= S n. +Proof NZle_succ_diag_r. -Theorem Zlt_lt_succ : forall n m : Z, n < m -> n < S m. -Proof NZlt_lt_succ. +Theorem Zlt_lt_succ_r : forall n m : Z, n < m -> n < S m. +Proof NZlt_lt_succ_r. -Theorem Zle_le_succ : forall n m : Z, n <= m -> n <= S m. -Proof NZle_le_succ. +Theorem Zle_le_succ_r : forall n m : Z, n <= m -> n <= S m. +Proof NZle_le_succ_r. -Theorem Zle_succ_le_or_eq_succ : forall n m : Z, n <= S m <-> n <= m \/ n == S m. -Proof NZle_succ_le_or_eq_succ. +Theorem Zle_succ_r : forall n m : Z, n <= S m <-> n <= m \/ n == S m. +Proof NZle_succ_r. -Theorem Zneq_succ_l : forall n : Z, S n ~= n. -Proof NZneq_succ_l. +Theorem Zneq_succ_diag_l : forall n : Z, S n ~= n. +Proof NZneq_succ_diag_l. -Theorem Znlt_succ_l : forall n : Z, ~ S n < n. -Proof NZnlt_succ_l. +Theorem Zneq_succ_diag_r : forall n : Z, n ~= S n. +Proof NZneq_succ_diag_r. -Theorem Znle_succ_l : forall n : Z, ~ S n <= n. -Proof NZnle_succ_l. +Theorem Znlt_succ_diag_l : forall n : Z, ~ S n < n. +Proof NZnlt_succ_diag_l. -Theorem Zlt_le_succ : forall n m : Z, n < m <-> S n <= m. -Proof NZlt_le_succ. +Theorem Znle_succ_diag_l : forall n : Z, ~ S n <= n. +Proof NZnle_succ_diag_l. -Theorem Zlt_succ_lt : forall n m : Z, S n < m -> n < m. -Proof NZlt_succ_lt. +Theorem Zle_succ_l : forall n m : Z, S n <= m <-> n < m. +Proof NZle_succ_l. -Theorem Zle_succ_le : forall n m : Z, S n <= m -> n <= m. -Proof NZle_succ_le. +Theorem Zlt_succ_l : forall n m : Z, S n < m -> n < m. +Proof NZlt_succ_l. Theorem Zsucc_lt_mono : forall n m : Z, n < m <-> S n < S m. Proof NZsucc_lt_mono. @@ -111,6 +111,8 @@ Proof NZsucc_le_mono. Theorem Zlt_asymm : forall n m, n < m -> ~ m < n. Proof NZlt_asymm. +Notation Zlt_ngt := Zlt_asymm (only parsing). + Theorem Zlt_trans : forall n m p : Z, n < m -> m < p -> n < p. Proof NZlt_trans. @@ -126,11 +128,16 @@ Proof NZlt_le_trans. Theorem Zle_antisymm : forall n m : Z, n <= m -> m <= n -> n == m. Proof NZle_antisymm. +Theorem Zlt_1_l : forall n m : Z, 0 < n -> n < m -> 1 < m. +Proof NZlt_1_l. + (** Trichotomy, decidability, and double negation elimination *) Theorem Zlt_trichotomy : forall n m : Z, n < m \/ n == m \/ m < n. Proof NZlt_trichotomy. +Notation Zlt_eq_gt_cases := Zlt_trichotomy (only parsing). + Theorem Zlt_gt_cases : forall n m : Z, n ~= m <-> n < m \/ n > m. Proof NZlt_gt_cases. @@ -149,8 +156,8 @@ Proof NZle_ngt. Theorem Znlt_ge : forall n m : Z, ~ n < m <-> n >= m. Proof NZnlt_ge. -Theorem Zlt_em : forall n m : Z, n < m \/ ~ n < m. -Proof NZlt_em. +Theorem Zlt_dec : forall n m : Z, decidable (n < m). +Proof NZlt_dec. Theorem Zlt_dne : forall n m, ~ ~ n < m <-> n < m. Proof NZlt_dne. @@ -161,14 +168,14 @@ Proof NZnle_gt. Theorem Zlt_nge : forall n m : Z, n < m <-> ~ n >= m. Proof NZlt_nge. -Theorem Zle_em : forall n m : Z, n <= m \/ ~ n <= m. -Proof NZle_em. +Theorem Zle_dec : forall n m : Z, decidable (n <= m). +Proof NZle_dec. Theorem Zle_dne : forall n m : Z, ~ ~ n <= m <-> n <= m. Proof NZle_dne. -Theorem Zlt_nlt_succ : forall n m : Z, n < m <-> ~ m < S n. -Proof NZlt_nlt_succ. +Theorem Znlt_succ_r : forall n m : Z, ~ m < S n <-> n < m. +Proof NZnlt_succ_r. Theorem Zlt_exists_pred : forall z n : Z, z < n -> exists k : Z, n == S k /\ z <= k. @@ -307,17 +314,17 @@ Proof NZgt_wf. Theorem Zlt_pred_l : forall n : Z, P n < n. Proof. -intro n; pattern n at 2; qsetoid_rewrite <- (Zsucc_pred n); apply Zlt_succ_r. +intro n; pattern n at 2; qsetoid_rewrite <- (Zsucc_pred n); apply Zlt_succ_diag_r. Qed. Theorem Zle_pred_l : forall n : Z, P n <= n. Proof. -intro; le_less; apply Zlt_pred_l. +intro; apply Zlt_le_incl; apply Zlt_pred_l. Qed. Theorem Zlt_le_pred : forall n m : Z, n < m <-> n <= P m. Proof. -intros n m; rewrite <- (Zsucc_pred m); rewrite Zpred_succ. apply Zlt_succ_le. +intros n m; rewrite <- (Zsucc_pred m); rewrite Zpred_succ. apply Zlt_succ_r. Qed. Theorem Znle_pred_r : forall n : Z, ~ n <= P n. @@ -328,17 +335,17 @@ Qed. Theorem Zlt_pred_le : forall n m : Z, P n < m <-> n <= m. Proof. intros n m; pattern n at 2; qsetoid_rewrite <- (Zsucc_pred n). -apply Zlt_le_succ. +symmetry; apply Zle_succ_l. Qed. Theorem Zlt_lt_pred : forall n m : Z, n < m -> P n < m. Proof. -intros; apply <- Zlt_pred_le; le_less. +intros; apply <- Zlt_pred_le; now apply Zlt_le_incl. Qed. Theorem Zle_le_pred : forall n m : Z, n <= m -> P n <= m. Proof. -intros; le_less; now apply <- Zlt_pred_le. +intros; apply Zlt_le_incl; now apply <- Zlt_pred_le. Qed. Theorem Zlt_pred_lt : forall n m : Z, n < P m -> n < m. @@ -348,7 +355,7 @@ Qed. Theorem Zle_pred_lt : forall n m : Z, n <= P m -> n <= m. Proof. -intros; le_less; now apply <- Zlt_le_pred. +intros; apply Zlt_le_incl; now apply <- Zlt_le_pred. Qed. Theorem Zpred_lt_mono : forall n m : Z, n < m <-> P n < P m. @@ -373,7 +380,7 @@ Qed. Theorem Zlt_pred_lt_succ : forall n m : Z, P n < m <-> n < S m. Proof. -intros; rewrite Zlt_pred_le; symmetry; apply Zlt_succ_le. +intros; rewrite Zlt_pred_le; symmetry; apply Zlt_succ_r. Qed. Theorem Zle_pred_lt_succ : forall n m : Z, P n <= m <-> n <= S m. @@ -386,5 +393,12 @@ Proof. intro; apply Zlt_neq; apply Zlt_pred_l. Qed. +Theorem Zlt_n1_r : forall n m : Z, n < m -> m < 0 -> n < -1. +Proof. +intros n m H1 H2. apply -> Zlt_le_pred in H2. +setoid_replace (P 0) with (-1) in H2. now apply NZlt_le_trans with m. +apply <- Zeq_opp_r. now rewrite Zopp_pred, Zopp_0. +Qed. + End ZOrderPropFunct. diff --git a/theories/Numbers/Integer/Abstract/ZPlus.v b/theories/Numbers/Integer/Abstract/ZPlus.v index 16fe114313..b0cebd482d 100644 --- a/theories/Numbers/Integer/Abstract/ZPlus.v +++ b/theories/Numbers/Integer/Abstract/ZPlus.v @@ -85,7 +85,7 @@ intros n m; rewrite (Zplus_comm n (P m)), (Zplus_comm n m); apply Zplus_pred_l. Qed. -Theorem Zplus_opp_minus : forall n m : Z, n + (- m) == n - m. +Theorem Zplus_opp_r : forall n m : Z, n + (- m) == n - m. Proof. NZinduct m. rewrite Zopp_0; rewrite Zminus_0_r; now rewrite Zplus_0_r. @@ -94,12 +94,12 @@ Qed. Theorem Zminus_0_l : forall n : Z, 0 - n == - n. Proof. -intro n; rewrite <- Zplus_opp_minus; now rewrite Zplus_0_l. +intro n; rewrite <- Zplus_opp_r; now rewrite Zplus_0_l. Qed. Theorem Zminus_succ_l : forall n m : Z, S n - m == S (n - m). Proof. -intros n m; do 2 rewrite <- Zplus_opp_minus; now rewrite Zplus_succ_l. +intros n m; do 2 rewrite <- Zplus_opp_r; now rewrite Zplus_succ_l. Qed. Theorem Zminus_pred_l : forall n m : Z, P n - m == P (n - m). @@ -127,24 +127,24 @@ now rewrite Zminus_0_r. intro n. rewrite Zminus_succ_r, Zminus_succ_l; now rewrite Zpred_succ. Qed. -Theorem Zplus_opp_r : forall n : Z, n + (- n) == 0. +Theorem Zplus_opp_diag_l : forall n : Z, - n + n == 0. Proof. -intro n; rewrite Zplus_opp_minus; now rewrite Zminus_diag. +intro n; now rewrite Zplus_comm, Zplus_opp_r, Zminus_diag. Qed. -Theorem Zplus_opp_l : forall n : Z, - n + n == 0. +Theorem Zplus_opp_diag_r : forall n : Z, n + (- n) == 0. Proof. -intro n; rewrite Zplus_comm; apply Zplus_opp_r. +intro n; rewrite Zplus_comm; apply Zplus_opp_diag_l. Qed. -Theorem Zminus_swap : forall n m : Z, - m + n == n - m. +Theorem Zplus_opp_l : forall n m : Z, - m + n == n - m. Proof. -intros n m; rewrite <- Zplus_opp_minus; now rewrite Zplus_comm. +intros n m; rewrite <- Zplus_opp_r; now rewrite Zplus_comm. Qed. Theorem Zplus_minus_assoc : forall n m p : Z, n + (m - p) == (n + m) - p. Proof. -intros n m p; do 2 rewrite <- Zplus_opp_minus; now rewrite Zplus_assoc. +intros n m p; do 2 rewrite <- Zplus_opp_r; now rewrite Zplus_assoc. Qed. Theorem Zopp_involutive : forall n : Z, - (- n) == n. @@ -164,7 +164,7 @@ Qed. Theorem Zopp_minus_distr : forall n m : Z, - (n - m) == - n + m. Proof. -intros n m; rewrite <- Zplus_opp_minus, Zopp_plus_distr. +intros n m; rewrite <- Zplus_opp_r, Zopp_plus_distr. now rewrite Zopp_involutive. Qed. @@ -178,57 +178,163 @@ Proof. intros n m; split; [apply Zopp_inj | apply Zopp_wd]. Qed. +Theorem Zeq_opp_l : forall n m : Z, - n == m <-> n == - m. +Proof. +intros n m. now rewrite <- (Zopp_inj_wd (- n) m), Zopp_involutive. +Qed. + +Theorem Zeq_opp_r : forall n m : Z, n == - m <-> - n == m. +Proof. +symmetry; apply Zeq_opp_l. +Qed. + Theorem Zminus_plus_distr : forall n m p : Z, n - (m + p) == (n - m) - p. Proof. -intros n m p; rewrite <- Zplus_opp_minus, Zopp_plus_distr, Zplus_assoc. -now do 2 rewrite Zplus_opp_minus. +intros n m p; rewrite <- Zplus_opp_r, Zopp_plus_distr, Zplus_assoc. +now do 2 rewrite Zplus_opp_r. Qed. Theorem Zminus_minus_distr : forall n m p : Z, n - (m - p) == (n - m) + p. Proof. -intros n m p; rewrite <- Zplus_opp_minus, Zopp_minus_distr, Zplus_assoc. -now rewrite Zplus_opp_minus. +intros n m p; rewrite <- Zplus_opp_r, Zopp_minus_distr, Zplus_assoc. +now rewrite Zplus_opp_r. Qed. -Theorem Zminus_opp : forall n m : Z, n - (- m) == n + m. +Theorem Zminus_opp_r : forall n m : Z, n - (- m) == n + m. Proof. -intros n m; rewrite <- Zplus_opp_minus; now rewrite Zopp_involutive. +intros n m; rewrite <- Zplus_opp_r; now rewrite Zopp_involutive. Qed. Theorem Zplus_minus_swap : forall n m p : Z, n + m - p == n - p + m. Proof. -intros n m p. rewrite <- Zplus_minus_assoc, <- (Zplus_opp_minus n p), <- Zplus_assoc. -now rewrite Zminus_swap. +intros n m p. rewrite <- Zplus_minus_assoc, <- (Zplus_opp_r n p), <- Zplus_assoc. +now rewrite Zplus_opp_l. Qed. -Theorem Zminus_plus_diag : forall n m : Z, n - m + m == n. +Theorem Zminus_cancel_l : forall n m p : Z, n - m == n - p <-> m == p. Proof. -intros; rewrite <- Zplus_minus_swap; rewrite <- Zplus_minus_assoc; -rewrite Zminus_diag; now rewrite Zplus_0_r. +intros n m p. rewrite <- (Zplus_cancel_l (n - m) (n - p) (- n)). +do 2 rewrite Zplus_minus_assoc. rewrite Zplus_opp_diag_l; do 2 rewrite Zminus_0_l. +apply Zopp_inj_wd. Qed. -Theorem Zplus_minus_diag : forall n m : Z, n + m - m == n. +Theorem Zminus_cancel_r : forall n m p : Z, n - p == m - p <-> n == m. Proof. -intros; rewrite <- Zplus_minus_assoc; rewrite Zminus_diag; now rewrite Zplus_0_r. +intros n m p. +stepl (n - p + p == m - p + p) by apply Zplus_cancel_r. +now do 2 rewrite <- Zminus_minus_distr, Zminus_diag, Zminus_0_r. Qed. -Theorem Zplus_minus_eq_l : forall n m p : Z, m + p == n <-> n - m == p. +(* The next several theorems are devoted to moving terms from one side of +an equation to the other. The name contains the operation in the original +equation (plus or minus) and the indication whether the left or right term +is moved. *) + +Theorem Zplus_move_l : forall n m p : Z, n + m == p <-> m == p - n. Proof. intros n m p. -stepl (-m + (m + p) == -m + n) by apply Zplus_cancel_l. -stepr (p == n - m) by now split. -rewrite Zplus_assoc, Zplus_opp_l, Zplus_0_l. now rewrite Zminus_swap. +stepl (n + m - n == p - n) by apply Zminus_cancel_r. +now rewrite Zplus_comm, <- Zplus_minus_assoc, Zminus_diag, Zplus_0_r. +Qed. + +Theorem Zplus_move_r : forall n m p : Z, n + m == p <-> n == p - m. +Proof. +intros n m p; rewrite Zplus_comm; now apply Zplus_move_l. +Qed. + +(* The two theorems above do not allow rewriting subformulas of the form +n - m == p to n == p + m since subtraction is in the right-hand side of +the equation. Hence the following two theorems. *) + +Theorem Zminus_move_l : forall n m p : Z, n - m == p <-> - m == p - n. +Proof. +intros n m p; rewrite <- (Zplus_opp_r n m); apply Zplus_move_l. Qed. -Theorem Zplus_minus_eq_r : forall n m p : Z, m + p == n <-> n - p == m. +Theorem Zminus_move_r : forall n m p : Z, n - m == p <-> n == p + m. Proof. -intros n m p; rewrite Zplus_comm; now apply Zplus_minus_eq_l. +intros n m p; rewrite <- (Zplus_opp_r n m). now rewrite Zplus_move_r, Zminus_opp_r. Qed. -Theorem Zminus_eq : forall n m : Z, n - m == 0 <-> n == m. +Theorem Zplus_move_0_l : forall n m : Z, n + m == 0 <-> m == - n. Proof. -intros n m. rewrite <- Zplus_minus_eq_l, Zplus_0_r; now split. +intros n m; now rewrite Zplus_move_l, Zminus_0_l. Qed. +Theorem Zplus_move_0_r : forall n m : Z, n + m == 0 <-> n == - m. +Proof. +intros n m; now rewrite Zplus_move_r, Zminus_0_l. +Qed. + +Theorem Zminus_move_0_l : forall n m : Z, n - m == 0 <-> - m == - n. +Proof. +intros n m. now rewrite Zminus_move_l, Zminus_0_l. +Qed. + +Theorem Zminus_move_0_r : forall n m : Z, n - m == 0 <-> n == m. +Proof. +intros n m. now rewrite Zminus_move_r, Zplus_0_l. +Qed. + +(* The following section is devoted to cancellation of like terms. The name +includes the first operator and the position of the term being canceled. *) + +Theorem Zplus_simpl_l : forall n m : Z, n + m - n == m. +Proof. +intros; now rewrite Zplus_minus_swap, Zminus_diag, Zplus_0_l. +Qed. + +Theorem Zplus_simpl_r : forall n m : Z, n + m - m == n. +Proof. +intros; now rewrite <- Zplus_minus_assoc, Zminus_diag, Zplus_0_r. +Qed. + +Theorem Zminus_simpl_l : forall n m : Z, - n - m + n == - m. +Proof. +intros; now rewrite <- Zplus_minus_swap, Zplus_opp_diag_l, Zminus_0_l. +Qed. + +Theorem Zminus_simpl_r : forall n m : Z, n - m + m == n. +Proof. +intros; now rewrite <- Zminus_minus_distr, Zminus_diag, Zminus_0_r. +Qed. + +(* Now we have two sums or differences; the name includes the two operators +and the position of the terms being canceled *) + +Theorem Zplus_plus_simpl_l_l : forall n m p : Z, (n + m) - (n + p) == m - p. +Proof. +intros n m p. now rewrite (Zplus_comm n m), <- Zplus_minus_assoc, +Zminus_plus_distr, Zminus_diag, Zminus_0_l, Zplus_opp_r. +Qed. + +Theorem Zplus_plus_simpl_l_r : forall n m p : Z, (n + m) - (p + n) == m - p. +Proof. +intros n m p. rewrite (Zplus_comm p n); apply Zplus_plus_simpl_l_l. +Qed. + +Theorem Zplus_plus_simpl_r_l : forall n m p : Z, (n + m) - (m + p) == n - p. +Proof. +intros n m p. rewrite (Zplus_comm n m); apply Zplus_plus_simpl_l_l. +Qed. + +Theorem Zplus_plus_simpl_r_r : forall n m p : Z, (n + m) - (p + m) == n - p. +Proof. +intros n m p. rewrite (Zplus_comm p m); apply Zplus_plus_simpl_r_l. +Qed. + +Theorem Zminus_plus_simpl_r_l : forall n m p : Z, (n - m) + (m + p) == n + p. +Proof. +intros n m p. now rewrite <- Zminus_minus_distr, Zminus_plus_distr, Zminus_diag, +Zminus_0_l, Zminus_opp_r. +Qed. + +Theorem Zminus_plus_simpl_r_r : forall n m p : Z, (n - m) + (p + m) == n + p. +Proof. +intros n m p. rewrite (Zplus_comm p m); apply Zminus_plus_simpl_r_l. +Qed. + +(* Of course, there are many other variants *) + End ZPlusPropFunct. diff --git a/theories/Numbers/Integer/Abstract/ZPlusOrder.v b/theories/Numbers/Integer/Abstract/ZPlusOrder.v index 01226b1218..ce79055a71 100644 --- a/theories/Numbers/Integer/Abstract/ZPlusOrder.v +++ b/theories/Numbers/Integer/Abstract/ZPlusOrder.v @@ -10,7 +10,7 @@ (*i i*) -Require Export ZOrder. +Require Export ZLt. Module ZPlusOrderPropFunct (Import ZAxiomsMod : ZAxiomsSig). Module Export ZOrderPropMod := ZOrderPropFunct ZAxiomsMod. @@ -94,25 +94,25 @@ Proof NZplus_nonneg_cases. Theorem Zlt_lt_minus : forall n m : Z, n < m <-> 0 < m - n. Proof. intros n m. stepr (0 + n < m - n + n) by symmetry; apply Zplus_lt_mono_r. -rewrite Zplus_0_l; now rewrite Zminus_plus_diag. +rewrite Zplus_0_l; now rewrite Zminus_simpl_r. Qed. Theorem Zle_le_minus : forall n m : Z, n <= m <-> 0 <= m - n. Proof. intros n m; stepr (0 + n <= m - n + n) by symmetry; apply Zplus_le_mono_r. -rewrite Zplus_0_l; now rewrite Zminus_plus_diag. +rewrite Zplus_0_l; now rewrite Zminus_simpl_r. Qed. Theorem Zopp_lt_mono : forall n m : Z, n < m <-> - m < - n. Proof. intros n m. stepr (m + - m < m + - n) by symmetry; apply Zplus_lt_mono_l. -do 2 rewrite Zplus_opp_minus. rewrite Zminus_diag. apply Zlt_lt_minus. +do 2 rewrite Zplus_opp_r. rewrite Zminus_diag. apply Zlt_lt_minus. Qed. Theorem Zopp_le_mono : forall n m : Z, n <= m <-> - m <= - n. Proof. intros n m. stepr (m + - m <= m + - n) by symmetry; apply Zplus_le_mono_l. -do 2 rewrite Zplus_opp_minus. rewrite Zminus_diag. apply Zle_le_minus. +do 2 rewrite Zplus_opp_r. rewrite Zminus_diag. apply Zle_le_minus. Qed. Theorem Zopp_pos_neg : forall n : Z, 0 < - n <-> n < 0. @@ -137,13 +137,13 @@ Qed. Theorem Zminus_lt_mono_l : forall n m p : Z, n < m <-> p - m < p - n. Proof. -intros n m p. do 2 rewrite <- Zplus_opp_minus. rewrite <- Zplus_lt_mono_l. +intros n m p. do 2 rewrite <- Zplus_opp_r. rewrite <- Zplus_lt_mono_l. apply Zopp_lt_mono. Qed. Theorem Zminus_lt_mono_r : forall n m p : Z, n < m <-> n - p < m - p. Proof. -intros n m p; do 2 rewrite <- Zplus_opp_minus; apply Zplus_lt_mono_r. +intros n m p; do 2 rewrite <- Zplus_opp_r; apply Zplus_lt_mono_r. Qed. Theorem Zminus_lt_mono : forall n m p q : Z, n < m -> q < p -> n - p < m - q. @@ -155,13 +155,13 @@ Qed. Theorem Zminus_le_mono_l : forall n m p : Z, n <= m <-> p - m <= p - n. Proof. -intros n m p; do 2 rewrite <- Zplus_opp_minus; rewrite <- Zplus_le_mono_l; +intros n m p; do 2 rewrite <- Zplus_opp_r; rewrite <- Zplus_le_mono_l; apply Zopp_le_mono. Qed. Theorem Zminus_le_mono_r : forall n m p : Z, n <= m <-> n - p <= m - p. Proof. -intros n m p; do 2 rewrite <- Zplus_opp_minus; apply Zplus_le_mono_r. +intros n m p; do 2 rewrite <- Zplus_opp_r; apply Zplus_le_mono_r. Qed. Theorem Zminus_le_mono : forall n m p q : Z, n <= m -> q <= p -> n - p <= m - q. @@ -188,31 +188,31 @@ Qed. Theorem Zle_lt_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_lt_plus_lt (- m) (- n)); -[now apply -> Zopp_le_mono | now do 2 rewrite Zplus_opp_minus]. +[now apply -> Zopp_le_mono | now do 2 rewrite Zplus_opp_r]. Qed. Theorem Zlt_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 (Zlt_le_plus_lt (- m) (- n)); -[now apply -> Zopp_lt_mono | now do 2 rewrite Zplus_opp_minus]. +[now apply -> Zopp_lt_mono | now do 2 rewrite Zplus_opp_r]. 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_le (- m) (- n)); -[now apply -> Zopp_le_mono | now do 2 rewrite Zplus_opp_minus]. +[now apply -> Zopp_le_mono | now do 2 rewrite Zplus_opp_r]. Qed. Theorem Zlt_plus_lt_minus_r : forall n m p : Z, n + p < m <-> n < m - p. Proof. intros n m p. stepl (n + p - p < m - p) by symmetry; apply Zminus_lt_mono_r. -now rewrite Zplus_minus_diag. +now rewrite Zplus_simpl_r. Qed. Theorem Zle_plus_le_minus_r : forall n m p : Z, n + p <= m <-> n <= m - p. Proof. intros n m p. stepl (n + p - p <= m - p) by symmetry; apply Zminus_le_mono_r. -now rewrite Zplus_minus_diag. +now rewrite Zplus_simpl_r. Qed. Theorem Zlt_plus_lt_minus_l : forall n m p : Z, n + p < m <-> p < m - n. @@ -228,13 +228,13 @@ Qed. Theorem Zlt_minus_lt_plus_r : forall n m p : Z, n - p < m <-> n < m + p. Proof. intros n m p. stepl (n - p + p < m + p) by symmetry; apply Zplus_lt_mono_r. -now rewrite Zminus_plus_diag. +now rewrite Zminus_simpl_r. Qed. Theorem Zle_minus_le_plus_r : forall n m p : Z, n - p <= m <-> n <= m + p. Proof. intros n m p. stepl (n - p + p <= m + p) by symmetry; apply Zplus_le_mono_r. -now rewrite Zminus_plus_diag. +now rewrite Zminus_simpl_r. Qed. Theorem Zlt_minus_lt_plus_l : forall n m p : Z, n - m < p <-> n < m + p. @@ -281,32 +281,53 @@ Qed. Theorem Zminus_neg_cases : forall n m : Z, n - m < 0 -> n < 0 \/ 0 < m. Proof. -intros n m H; rewrite <- Zplus_opp_minus in H. +intros n m H; rewrite <- Zplus_opp_r in H. setoid_replace (0 < m) with (- m < 0) using relation iff by (symmetry; apply Zopp_neg_pos). now apply Zplus_neg_cases. Qed. Theorem Zminus_pos_cases : forall n m : Z, 0 < n - m -> 0 < n \/ m < 0. Proof. -intros n m H; rewrite <- Zplus_opp_minus in H. +intros n m H; rewrite <- Zplus_opp_r in H. setoid_replace (m < 0) with (0 < - m) using relation iff by (symmetry; apply Zopp_pos_neg). now apply Zplus_pos_cases. Qed. Theorem Zminus_nonpos_cases : forall n m : Z, n - m <= 0 -> n <= 0 \/ 0 <= m. Proof. -intros n m H; rewrite <- Zplus_opp_minus in H. +intros n m H; rewrite <- Zplus_opp_r in H. setoid_replace (0 <= m) with (- m <= 0) using relation iff by (symmetry; apply Zopp_nonpos_nonneg). now apply Zplus_nonpos_cases. Qed. Theorem Zminus_nonneg_cases : forall n m : Z, 0 <= n - m -> 0 <= n \/ m <= 0. Proof. -intros n m H; rewrite <- Zplus_opp_minus in H. +intros n m H; rewrite <- Zplus_opp_r in H. setoid_replace (m <= 0) with (0 <= - m) using relation iff by (symmetry; apply Zopp_nonneg_nonpos). now apply Zplus_nonneg_cases. Qed. +Section PosNeg. + +Variable P : Z -> Prop. +Hypothesis P_wd : predicate_wd Zeq P. + +Add Morphism P with signature Zeq ==> iff as P_morph. Proof. exact P_wd. Qed. + +Theorem Z0_pos_neg : + P 0 -> (forall n : Z, 0 < n -> P n /\ P (- n)) -> forall n : Z, P n. +Proof. +intros H1 H2 n. destruct (Zlt_trichotomy n 0) as [H3 | [H3 | H3]]. +apply <- Zopp_pos_neg in H3. apply H2 in H3. destruct H3 as [_ H3]. +now rewrite Zopp_involutive in H3. +now rewrite H3. +apply H2 in H3; now destruct H3. +Qed. + +End PosNeg. + +Ltac Z0_pos_neg n := induction_maker n ltac:(apply Z0_pos_neg). + End ZPlusOrderPropFunct. diff --git a/theories/Numbers/Integer/Abstract/ZTimes.v b/theories/Numbers/Integer/Abstract/ZTimes.v index 14c59fcfa0..89249d1ed9 100644 --- a/theories/Numbers/Integer/Abstract/ZTimes.v +++ b/theories/Numbers/Integer/Abstract/ZTimes.v @@ -10,7 +10,6 @@ (*i i*) -Require Export Ring. Require Export ZPlus. Module ZTimesPropFunct (Import ZAxiomsMod : ZAxiomsSig). @@ -21,20 +20,20 @@ Theorem Ztimes_wd : forall n1 n2 : Z, n1 == n2 -> forall m1 m2 : Z, m1 == m2 -> n1 * m1 == n2 * m2. Proof NZtimes_wd. -Theorem Ztimes_0_r : forall n : Z, n * 0 == 0. -Proof NZtimes_0_r. - -Theorem Ztimes_succ_r : forall n m : Z, n * (S m) == n * m + n. -Proof NZtimes_succ_r. - -(** Theorems that are valid for both natural numbers and integers *) - Theorem Ztimes_0_l : forall n : Z, 0 * n == 0. Proof NZtimes_0_l. Theorem Ztimes_succ_l : forall n m : Z, (S n) * m == n * m + m. Proof NZtimes_succ_l. +(** Theorems that are valid for both natural numbers and integers *) + +Theorem Ztimes_0_r : forall n : Z, n * 0 == 0. +Proof NZtimes_0_r. + +Theorem Ztimes_succ_r : forall n m : Z, n * (S m) == n * m + n. +Proof NZtimes_succ_r. + Theorem Ztimes_comm : forall n m : Z, n * m == m * n. Proof NZtimes_comm. @@ -44,6 +43,13 @@ Proof NZtimes_plus_distr_r. Theorem Ztimes_plus_distr_l : forall n m p : Z, n * (m + p) == n * m + n * p. Proof NZtimes_plus_distr_l. +(* A note on naming: right (correspondingly, left) distributivity happens +when the sum is multiplied by a number on the right (left), not when the +sum itself is the right (left) factor in the product (see planetmath.org +and mathworld.wolfram.com). In the old library BinInt, distributivity over +subtraction was named correctly, but distributivity over addition was named +incorrectly. The names in Isabelle/HOL library are also incorrect. *) + Theorem Ztimes_assoc : forall n m p : Z, n * (m * p) == (n * m) * p. Proof NZtimes_assoc. @@ -56,29 +62,11 @@ Proof NZtimes_1_r. (* The following two theorems are true in an ordered ring, but since they don't mention order, we'll put them here *) -Theorem Ztimes_eq_0 : forall n m : Z, n * m == 0 -> n == 0 \/ m == 0. -Proof NZtimes_eq_0. +Theorem Zeq_times_0 : forall n m : Z, n * m == 0 <-> n == 0 \/ m == 0. +Proof NZeq_times_0. -Theorem Ztimes_neq_0 : forall n m : Z, n ~= 0 /\ m ~= 0 <-> n * m ~= 0. -Proof NZtimes_neq_0. - -(** Z forms a ring *) - -Lemma Zring : ring_theory 0 1 NZplus NZtimes NZminus Zopp NZeq. -Proof. -constructor. -exact Zplus_0_l. -exact Zplus_comm. -exact Zplus_assoc. -exact Ztimes_1_l. -exact Ztimes_comm. -exact Ztimes_assoc. -exact Ztimes_plus_distr_r. -intros; now rewrite Zplus_opp_minus. -exact Zplus_opp_r. -Qed. - -Add Ring ZR : Zring. +Theorem Zneq_times_0 : forall n m : Z, n ~= 0 /\ m ~= 0 <-> n * m ~= 0. +Proof NZneq_times_0. (** Theorems that are either not valid on N or have different proofs on N and Z *) @@ -94,29 +82,32 @@ Proof. intros n m; rewrite (Ztimes_comm (P n) m), (Ztimes_comm n m). apply Ztimes_pred_r. Qed. -Theorem Ztimes_opp_r : forall n m : Z, n * (- m) == - (n * m). +Theorem Ztimes_opp_l : forall n m : Z, (- n) * m == - (n * m). Proof. -intros; ring. +intros n m. apply -> Zplus_move_0_r. +now rewrite <- Ztimes_plus_distr_r, Zplus_opp_diag_l, Ztimes_0_l. Qed. -Theorem Ztimes_opp_l : forall n m : Z, (- n) * m == - (n * m). +Theorem Ztimes_opp_r : forall n m : Z, n * (- m) == - (n * m). Proof. -intros; ring. +intros n m; rewrite (Ztimes_comm n (- m)), (Ztimes_comm n m); apply Ztimes_opp_l. Qed. Theorem Ztimes_opp_opp : forall n m : Z, (- n) * (- m) == n * m. Proof. -intros; ring. +intros n m; now rewrite Ztimes_opp_l, Ztimes_opp_r, Zopp_involutive. Qed. -Theorem Ztimes_minus_distr_r : forall n m p : Z, n * (m - p) == n * m - n * p. +Theorem Ztimes_minus_distr_l : forall n m p : Z, n * (m - p) == n * m - n * p. Proof. -intros; ring. +intros n m p. do 2 rewrite <- Zplus_opp_r. rewrite Ztimes_plus_distr_l. +now rewrite Ztimes_opp_r. Qed. -Theorem Ztimes_minus_distr_l : forall n m p : Z, (n - m) * p == n * p - m * p. +Theorem Ztimes_minus_distr_r : forall n m p : Z, (n - m) * p == n * p - m * p. Proof. -intros; ring. +intros n m p; rewrite (Ztimes_comm (n - m) p), (Ztimes_comm n p), (Ztimes_comm m p); +now apply Ztimes_minus_distr_l. Qed. End ZTimesPropFunct. diff --git a/theories/Numbers/Integer/Abstract/ZTimesOrder.v b/theories/Numbers/Integer/Abstract/ZTimesOrder.v index 1b9e9b5192..287fdb7f19 100644 --- a/theories/Numbers/Integer/Abstract/ZTimesOrder.v +++ b/theories/Numbers/Integer/Abstract/ZTimesOrder.v @@ -96,11 +96,20 @@ 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 Zlt_1_times_pos : forall n m : Z, 1 < n -> 0 < m -> 1 < n * m. +Proof NZlt_1_times_pos. -Theorem Ztimes_neq_0 : forall n m : Z, n ~= 0 /\ m ~= 0 <-> n * m ~= 0. -Proof NZtimes_neq_0. +Theorem Zeq_times_0 : forall n m : Z, n * m == 0 <-> n == 0 \/ m == 0. +Proof NZeq_times_0. + +Theorem Zneq_times_0 : forall n m : Z, n ~= 0 /\ m ~= 0 <-> n * m ~= 0. +Proof NZneq_times_0. + +Theorem Zeq_times_0_l : forall n m : Z, n * m == 0 -> m ~= 0 -> n == 0. +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. @@ -114,7 +123,64 @@ Proof NZtimes_2_mono_l. (** Theorems that are either not valid on N or have different proofs on N and Z *) -(* None? *) +Theorem Zlt_1_times_neg : forall n m : Z, n < -1 -> m < 0 -> 1 < n * m. +Proof. +intros n m H1 H2. apply -> (NZtimes_lt_mono_neg_r m) in H1. +apply <- Zopp_pos_neg in H2. rewrite Ztimes_opp_l, Ztimes_1_l in H1. +now apply Zlt_1_l with (- m). +assumption. +Qed. + +Theorem Zlt_times_n1_neg : forall n m : Z, 1 < n -> m < 0 -> n * m < -1. +Proof. +intros n m H1 H2. apply -> (NZtimes_lt_mono_neg_r m) in H1. +rewrite Ztimes_1_l in H1. now apply Zlt_n1_r with m. +assumption. +Qed. + +Theorem Zlt_times_n1_pos : forall n m : Z, n < -1 -> 0 < m -> n * m < -1. +Proof. +intros n m H1 H2. apply -> (NZtimes_lt_mono_pos_r m) in H1. +rewrite Ztimes_opp_l, Ztimes_1_l in H1. +apply <- Zopp_neg_pos in H2. now apply Zlt_n1_r with (- m). +assumption. +Qed. + +Theorem Zlt_1_l_times : forall n m : Z, 1 < n -> n * m < -1 \/ n * m == 0 \/ 1 < n * m. +Proof. +intros n m H; destruct (Zlt_trichotomy m 0) as [H1 | [H1 | H1]]. +left. now apply Zlt_times_n1_neg. +right; left; now rewrite H1, Ztimes_0_r. +right; right; now apply Zlt_1_times_pos. +Qed. + +Theorem Zlt_n1_r_times : forall n m : Z, n < -1 -> n * m < -1 \/ n * m == 0 \/ 1 < n * m. +Proof. +intros n m H; destruct (Zlt_trichotomy m 0) as [H1 | [H1 | H1]]. +right; right. now apply Zlt_1_times_neg. +right; left; now rewrite H1, Ztimes_0_r. +left. now apply Zlt_times_n1_pos. +Qed. + +Theorem Zeq_times_1 : forall n m : Z, n * m == 1 -> n == 1 \/ n == -1. +Proof. +assert (F : ~ 1 < -1). +intro H. +assert (H1 : -1 < 0). apply <- Zopp_neg_pos. apply Zlt_succ_diag_r. +assert (H2 : 1 < 0) by now apply Zlt_trans with (-1). false_hyp H2 Znlt_succ_diag_l. +Z0_pos_neg n. +intros m H; rewrite Ztimes_0_l in H; false_hyp H Zneq_succ_diag_r. +intros n H; split; apply <- Zle_succ_l in H; le_elim H. +intros m H1; apply (Zlt_1_l_times n m) in H. +rewrite H1 in H; destruct H as [H | [H | H]]. +false_hyp H F. false_hyp H Zneq_succ_diag_l. false_hyp H Zlt_irrefl. +intros; now left. +intros m H1; apply (Zlt_1_l_times n m) in H. rewrite Ztimes_opp_l in H1; +apply -> Zeq_opp_l in H1. rewrite H1 in H; destruct H as [H | [H | H]]. +false_hyp H Zlt_irrefl. apply -> Zeq_opp_l in H. rewrite Zopp_0 in H. +false_hyp H Zneq_succ_diag_l. false_hyp H F. +intros; right; symmetry; now apply Zopp_wd. +Qed. End ZTimesOrderPropFunct. diff --git a/theories/Numbers/Integer/Binary/ZBinary.v b/theories/Numbers/Integer/Binary/ZBinary.v index 3c680ec918..96e01a731c 100644 --- a/theories/Numbers/Integer/Binary/ZBinary.v +++ b/theories/Numbers/Integer/Binary/ZBinary.v @@ -100,14 +100,14 @@ intros; rewrite <- Zsucc_succ'; rewrite <- Zpred_pred'; apply Zminus_succ_r. Qed. -Theorem NZtimes_0_r : forall n : Z, n * 0 = 0. +Theorem NZtimes_0_l : forall n : Z, 0 * n = 0. Proof. -exact Zmult_0_r. +reflexivity. Qed. -Theorem NZtimes_succ_r : forall n m : Z, n * (NZsucc m) = n * m + n. +Theorem NZtimes_succ_l : forall n m : Z, (NZsucc n) * m = n * m + m. Proof. -intros; rewrite <- Zsucc_succ'; apply Zmult_succ_r. +intros; rewrite <- Zsucc_succ'; apply Zmult_succ_l. Qed. End NZAxiomsMod. @@ -137,7 +137,7 @@ Proof. congruence. Qed. -Theorem NZle_lt_or_eq : forall n m : Z, n <= m <-> n < m \/ n = m. +Theorem NZlt_eq_cases : forall n m : Z, n <= m <-> n < m \/ n = m. Proof. intros n m; split. apply Zle_lt_or_eq. intro H; destruct H as [H | H]. now apply Zlt_le_weak. rewrite H; apply Zle_refl. @@ -148,7 +148,7 @@ Proof. exact Zlt_irrefl. Qed. -Theorem NZlt_succ_le : forall n m : Z, n < (NZsucc m) <-> n <= m. +Theorem NZlt_succ_r : forall n m : Z, n < (NZsucc m) <-> n <= m. Proof. intros; unfold NZsucc; rewrite <- Zsucc_succ'; split; [apply Zlt_succ_le | apply Zle_lt_succ]. @@ -215,6 +215,23 @@ End ZBinAxiomsMod. Module Export ZBinTimesOrderPropMod := ZTimesOrderPropFunct ZBinAxiomsMod. +(** Z forms a ring *) + +(*Lemma Zring : ring_theory 0 1 NZplus NZtimes NZminus Zopp NZeq. +Proof. +constructor. +exact Zplus_0_l. +exact Zplus_comm. +exact Zplus_assoc. +exact Ztimes_1_l. +exact Ztimes_comm. +exact Ztimes_assoc. +exact Ztimes_plus_distr_r. +intros; now rewrite Zplus_opp_minus. +exact Zplus_opp_r. +Qed. + +Add Ring ZR : Zring.*) diff --git a/theories/Numbers/Integer/NatPairs/ZNatPairs.v b/theories/Numbers/Integer/NatPairs/ZNatPairs.v index 8e31331b4b..fc9115e20f 100644 --- a/theories/Numbers/Integer/NatPairs/ZNatPairs.v +++ b/theories/Numbers/Integer/NatPairs/ZNatPairs.v @@ -12,6 +12,7 @@ Require Import NMinus. (* The most complete file for natural numbers *) Require Export ZTimesOrder. (* The most complete file for integers *) +Require Export Ring. Module ZPairsAxiomsMod (Import NAxiomsMod : NAxiomsSig) <: ZAxiomsSig. Module Import NPropMod := NMinusPropFunct NAxiomsMod. (* Get all properties of natural numbers *) @@ -251,16 +252,16 @@ Proof. intros n m; unfold NZminus, Zeq; simpl. symmetry; now rewrite plus_succ_r. Qed. -Theorem NZtimes_0_r : forall n : Z, n * 0 == 0. +Theorem NZtimes_0_l : forall n : Z, 0 * n == 0. Proof. intro n; unfold NZtimes, Zeq; simpl. -repeat rewrite times_0_r. now rewrite plus_assoc. +repeat rewrite times_0_l. now rewrite plus_assoc. Qed. -Theorem NZtimes_succ_r : forall n m : Z, n * (Zsucc m) == n * m + n. +Theorem NZtimes_succ_l : forall n m : Z, (Zsucc n) * m == n * m + m. Proof. intros n m; unfold NZtimes, NZsucc, Zeq; simpl. -do 2 rewrite times_succ_r. ring. +do 2 rewrite times_succ_l. ring. Qed. End NZAxiomsMod. @@ -292,7 +293,7 @@ Qed. Add Morphism NZle with signature Zeq ==> Zeq ==> iff as NZle_wd. Proof. 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. +do 2 rewrite lt_eq_cases. 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. @@ -331,9 +332,9 @@ Qed. Open Local Scope IntScope. -Theorem NZle_lt_or_eq : forall n m : Z, n <= m <-> n < m \/ n == m. +Theorem NZlt_eq_cases : forall n m : Z, n <= m <-> n < m \/ n == m. Proof. -intros n m; unfold Zlt, Zle, Zeq; simpl. apply le_lt_or_eq. +intros n m; unfold Zlt, Zle, Zeq; simpl. apply lt_eq_cases. Qed. Theorem NZlt_irrefl : forall n : Z, ~ (n < n). @@ -341,9 +342,9 @@ Proof. intros n; unfold Zlt, Zeq; simpl. apply lt_irrefl. Qed. -Theorem NZlt_succ_le : forall n m : Z, n < (Zsucc m) <-> n <= m. +Theorem NZlt_succ_r : forall n m : Z, n < (Zsucc m) <-> n <= m. Proof. -intros n m; unfold Zlt, Zle, Zeq; simpl. rewrite plus_succ_l; apply lt_succ_le. +intros n m; unfold Zlt, Zle, Zeq; simpl. rewrite plus_succ_l; apply lt_succ_r. Qed. Theorem NZmin_l : forall n m : Z, n <= m -> Zmin n m == n. diff --git a/theories/Numbers/Integer/TreeMod/ZTreeMod.v b/theories/Numbers/Integer/TreeMod/ZTreeMod.v index 75e9c9f77e..db09c2ec7a 100644 --- a/theories/Numbers/Integer/TreeMod/ZTreeMod.v +++ b/theories/Numbers/Integer/TreeMod/ZTreeMod.v @@ -212,18 +212,18 @@ rewrite Zminus_mod_idemp_l. now replace ([|n|] - ([|m|] + 1))%Z with ([|n|] - [|m|] - 1)%Z by auto with zarith. Qed. -Theorem NZtimes_0_r : forall n : NZ, n * 0 == 0. +Theorem NZtimes_0_l : forall n : NZ, 0 * n == 0. Proof. intro n; unfold NZtimes, NZ0, NZ, NZeq. rewrite w_spec.(spec_mul). -rewrite w_spec.(spec_0). now rewrite Zmult_0_r. +rewrite w_spec.(spec_0). now rewrite Zmult_0_l. Qed. -Theorem NZtimes_succ_r : forall n m : NZ, n * (S m) == n * m + n. +Theorem NZtimes_succ_l : forall n m : NZ, (S n) * m == n * m + m. Proof. intros n m; unfold NZtimes, NZsucc, NZplus, NZeq. rewrite w_spec.(spec_mul). -rewrite w_spec.(spec_add). rewrite w_spec.(spec_mul). rewrite w_spec.(spec_succ). -rewrite Zplus_mod_idemp_l. rewrite Zmult_mod_idemp_r. -rewrite Zmult_plus_distr_r. now rewrite Zmult_1_r. +rewrite w_spec.(spec_add), w_spec.(spec_mul), w_spec.(spec_succ). +rewrite Zplus_mod_idemp_l, Zmult_mod_idemp_l. +now rewrite Zmult_plus_distr_l, Zmult_1_l. Qed. End NZBigIntsAxiomsMod. diff --git a/theories/Numbers/NatInt/NZAxioms.v b/theories/Numbers/NatInt/NZAxioms.v index 9c9161e2b3..f218ed6a64 100644 --- a/theories/Numbers/NatInt/NZAxioms.v +++ b/theories/Numbers/NatInt/NZAxioms.v @@ -60,8 +60,8 @@ Axiom NZplus_succ_l : forall n m : NZ, (S n) + m == S (n + m). Axiom NZminus_0_r : forall n : NZ, n - 0 == n. Axiom NZminus_succ_r : forall n m : NZ, n - (S m) == P (n - m). -Axiom NZtimes_0_r : forall n : NZ, n * 0 == 0. -Axiom NZtimes_succ_r : forall n m : NZ, n * (S m) == n * m + n. +Axiom NZtimes_0_l : forall n : NZ, 0 * n == 0. +Axiom NZtimes_succ_l : forall n m : NZ, S n * m == n * m + m. End NZAxiomsSig. @@ -84,9 +84,9 @@ Notation "x <= y" := (NZle x y) : NatIntScope. Notation "x > y" := (NZlt y x) (only parsing) : NatIntScope. Notation "x >= y" := (NZle y x) (only parsing) : NatIntScope. -Axiom NZle_lt_or_eq : forall n m : NZ, n <= m <-> n < m \/ n == m. +Axiom NZlt_eq_cases : forall n m : NZ, n <= m <-> n < m \/ n == m. Axiom NZlt_irrefl : forall n : NZ, ~ (n < n). -Axiom NZlt_succ_le : forall n m : NZ, n < S m <-> n <= m. +Axiom NZlt_succ_r : forall n m : NZ, n < S m <-> n <= m. Axiom NZmin_l : forall n m : NZ, n <= m -> NZmin n m == n. Axiom NZmin_r : forall n m : NZ, m <= n -> NZmin n m == m. diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v index 4ded2b8928..df2f224f49 100644 --- a/theories/Numbers/NatInt/NZOrder.v +++ b/theories/Numbers/NatInt/NZOrder.v @@ -12,14 +12,23 @@ Require Import NZAxioms. Require Import NZTimes. +Require Import Decidable. Module NZOrderPropFunct (Import NZOrdAxiomsMod : NZOrdAxiomsSig). Module Export NZTimesPropMod := NZTimesPropFunct NZAxiomsMod. Open Local Scope NatIntScope. -Ltac le_less := rewrite NZle_lt_or_eq; left; try assumption. -Ltac le_equal := rewrite NZle_lt_or_eq; right; try reflexivity; try assumption. -Ltac le_elim H := rewrite NZle_lt_or_eq in H; destruct H as [H | H]. +Ltac le_elim H := rewrite NZlt_eq_cases in H; destruct H as [H | H]. + +Theorem NZlt_le_incl : forall n m : NZ, n < m -> n <= m. +Proof. +intros; apply <- NZlt_eq_cases; now left. +Qed. + +Theorem NZeq_le_incl : forall n m : NZ, n == m -> n <= m. +Proof. +intros; apply <- NZlt_eq_cases; now right. +Qed. Lemma NZlt_stepl : forall x y z : NZ, x < y -> x == z -> z < y. Proof. @@ -46,106 +55,101 @@ Declare Right Step NZlt_stepr. Declare Left Step NZle_stepl. Declare Right Step NZle_stepr. -Theorem NZlt_le_incl : forall n m : NZ, n < m -> n <= m. -Proof. -intros; now le_less. -Qed. - Theorem NZlt_neq : forall n m : NZ, n < m -> n ~= m. 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. +Theorem NZle_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. +split. now apply NZlt_le_incl. 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. +intro; now apply NZeq_le_incl. Qed. -Theorem NZlt_succ_r : forall n : NZ, n < S n. +Theorem NZlt_succ_diag_r : forall n : NZ, n < S n. Proof. -intro n. rewrite NZlt_succ_le. now le_equal. +intro n. rewrite NZlt_succ_r. now apply NZeq_le_incl. Qed. -Theorem NZle_succ_r : forall n : NZ, n <= S n. +Theorem NZle_succ_diag_r : forall n : NZ, n <= S n. Proof. -intro; le_less; apply NZlt_succ_r. +intro; apply NZlt_le_incl; apply NZlt_succ_diag_r. Qed. -Theorem NZlt_lt_succ : forall n m : NZ, n < m -> n < S m. +Theorem NZlt_lt_succ_r : forall n m : NZ, n < m -> n < S m. Proof. -intros. rewrite NZlt_succ_le. now le_less. +intros. rewrite NZlt_succ_r. now apply NZlt_le_incl. Qed. -Theorem NZle_le_succ : forall n m : NZ, n <= m -> n <= S m. +Theorem NZle_le_succ_r : forall n m : NZ, n <= m -> n <= S m. Proof. -intros n m H; rewrite <- NZlt_succ_le in H; now le_less. +intros n m H. rewrite <- NZlt_succ_r in H. now apply NZlt_le_incl. Qed. -Theorem NZle_succ_le_or_eq_succ : forall n m : NZ, n <= S m <-> n <= m \/ n == S m. +Theorem NZle_succ_r : forall n m : NZ, n <= S m <-> n <= m \/ n == S m. Proof. -intros n m; rewrite NZle_lt_or_eq. now rewrite NZlt_succ_le. +intros n m; rewrite NZlt_eq_cases. now rewrite NZlt_succ_r. Qed. (* The following theorem is a special case of neq_succ_iter_l below, -but we prove it independently *) +but we prove it separately *) -Theorem NZneq_succ_l : forall n : NZ, S n ~= n. +Theorem NZneq_succ_diag_l : forall n : NZ, S n ~= n. Proof. -intros n H. pose proof (NZlt_succ_r n) as H1. rewrite H in H1. +intros n H. pose proof (NZlt_succ_diag_r n) as H1. rewrite H in H1. false_hyp H1 NZlt_irrefl. Qed. -Theorem NZnlt_succ_l : forall n : NZ, ~ S n < n. +Theorem NZneq_succ_diag_r : forall n : NZ, n ~= S n. Proof. -intros n H; apply NZlt_lt_succ in H. false_hyp H NZlt_irrefl. +intro n; apply NZneq_symm; apply NZneq_succ_diag_l. Qed. -Theorem NZnle_succ_l : forall n : NZ, ~ S n <= n. +Theorem NZnlt_succ_diag_l : forall n : NZ, ~ S n < n. +Proof. +intros n H; apply NZlt_lt_succ_r in H. false_hyp H NZlt_irrefl. +Qed. + +Theorem NZnle_succ_diag_l : forall n : NZ, ~ S n <= n. Proof. intros n H; le_elim H. -false_hyp H NZnlt_succ_l. false_hyp H NZneq_succ_l. +false_hyp H NZnlt_succ_diag_l. false_hyp H NZneq_succ_diag_l. Qed. -Theorem NZlt_le_succ : forall n m : NZ, n < m <-> S n <= m. +Theorem NZle_succ_l : forall n m : NZ, S n <= m <-> n < m. Proof. intro n; NZinduct m n. setoid_replace (n < n) with False using relation iff by (apply -> neg_false; apply NZlt_irrefl). now setoid_replace (S n <= n) with False using relation iff by - (apply -> neg_false; apply NZnle_succ_l). -intro m. rewrite NZlt_succ_le. rewrite NZle_succ_le_or_eq_succ. -rewrite NZsucc_inj_wd. rewrite (NZle_lt_or_eq n m). + (apply -> neg_false; apply NZnle_succ_diag_l). +intro m. rewrite NZlt_succ_r. rewrite NZle_succ_r. +rewrite NZsucc_inj_wd. rewrite (NZlt_eq_cases n m). rewrite or_cancel_r. +intros H1 H2; rewrite H2 in H1; false_hyp H1 NZnle_succ_diag_l. apply NZlt_neq. -intros H1 H2; rewrite H2 in H1; false_hyp H1 NZnle_succ_l. reflexivity. Qed. -Theorem NZlt_succ_lt : forall n m : NZ, S n < m -> n < m. -Proof. -intros n m H; apply <- NZlt_le_succ; now le_less. -Qed. - -Theorem NZle_succ_le : forall n m : NZ, S n <= m -> n <= m. +Theorem NZlt_succ_l : forall n m : NZ, S n < m -> n < m. Proof. -intros n m H; le_less; now apply <- NZlt_le_succ. +intros n m H; apply -> NZle_succ_l; now apply NZlt_le_incl. Qed. Theorem NZsucc_lt_mono : forall n m : NZ, n < m <-> S n < S m. Proof. -intros n m. rewrite NZlt_le_succ. symmetry. apply NZlt_succ_le. +intros n m. rewrite <- NZle_succ_l. symmetry. apply NZlt_succ_r. Qed. Theorem NZsucc_le_mono : forall n m : NZ, n <= m <-> S n <= S m. Proof. -intros n m. do 2 rewrite NZle_lt_or_eq. +intros n m. do 2 rewrite NZlt_eq_cases. rewrite <- NZsucc_lt_mono; now rewrite NZsucc_inj_wd. Qed. @@ -154,9 +158,9 @@ Proof. intros n m; NZinduct n m. intros H _; false_hyp H NZlt_irrefl. intro n; split; intros H H1 H2. -apply NZlt_succ_lt in H1. apply -> NZlt_succ_le in H2. le_elim H2. +apply NZlt_succ_l in H1. apply -> NZlt_succ_r in H2. le_elim H2. now apply H. rewrite H2 in H1; false_hyp H1 NZlt_irrefl. -apply NZlt_lt_succ in H2. apply -> NZlt_le_succ in H1. le_elim H1. +apply NZlt_lt_succ_r in H2. apply <- NZle_succ_l in H1. le_elim H1. now apply H. rewrite H1 in H2; false_hyp H2 NZlt_irrefl. Qed. @@ -164,10 +168,10 @@ Theorem NZlt_trans : forall n m p : NZ, n < m -> m < p -> n < p. Proof. intros n m p; NZinduct p m. intros _ H; false_hyp H NZlt_irrefl. -intro p. do 2 rewrite NZlt_succ_le. +intro p. do 2 rewrite NZlt_succ_r. split; intros H H1 H2. -le_less; le_elim H2; [now apply H | now rewrite H2 in H1]. -assert (n <= p) as H3. apply H. assumption. now le_less. +apply NZlt_le_incl; le_elim H2; [now apply H | now rewrite H2 in H1]. +assert (n <= p) as H3. apply H. assumption. now apply NZlt_le_incl. le_elim H3. assumption. rewrite <- H3 in H2. elimtype False; now apply (NZlt_asymm n m). Qed. @@ -175,8 +179,8 @@ Qed. Theorem NZle_trans : forall n m p : NZ, n <= m -> m <= p -> n <= p. Proof. intros n m p H1 H2; le_elim H1. -le_elim H2. le_less; now apply NZlt_trans with (m := m). -le_less; now rewrite <- H2. now rewrite H1. +le_elim H2. apply NZlt_le_incl; now apply NZlt_trans with (m := m). +apply NZlt_le_incl; now rewrite <- H2. now rewrite H1. Qed. Theorem NZle_lt_trans : forall n m p : NZ, n <= m -> m < p -> n < p. @@ -197,17 +201,22 @@ intros n m H1 H2; now (le_elim H1; le_elim H2); [elimtype False; apply (NZlt_asymm n m) | | |]. Qed. +Theorem NZlt_1_l : forall n m : NZ, 0 < n -> n < m -> 1 < m. +Proof. +intros n m H1 H2. apply <- NZle_succ_l in H1. now apply NZle_lt_trans with n. +Qed. + (** Trichotomy, decidability, and double negation elimination *) Theorem NZlt_trichotomy : forall n m : NZ, n < m \/ n == m \/ m < n. Proof. intros n m; NZinduct n m. right; now left. -intro n; rewrite NZlt_succ_le. stepr ((S n < m \/ S n == m) \/ m <= n) by tauto. -rewrite <- (NZle_lt_or_eq (S n) m). +intro n; rewrite NZlt_succ_r. stepr ((S n < m \/ S n == m) \/ m <= n) by tauto. +rewrite <- (NZlt_eq_cases (S n) m). setoid_replace (n == m) with (m == n) using relation iff by now split. -stepl (n < m \/ m < n \/ m == n) by tauto. rewrite <- NZle_lt_or_eq. -apply or_iff_compat_r. apply NZlt_le_succ. +stepl (n < m \/ m < n \/ m == n) by tauto. rewrite <- NZlt_eq_cases. +apply or_iff_compat_r. symmetry; apply NZle_succ_l. Qed. (* Decidability of equality, even though true in each finite ring, does not @@ -215,7 +224,8 @@ have a uniform proof. Otherwise, the proof for two fixed numbers would reduce to a normal form that will say if the numbers are equal or not, which cannot be true in all finite rings. Therefore, we prove decidability in the presence of order. *) -Theorem NZeq_em : forall n m : NZ, n == m \/ n ~= m. + +Theorem NZeq_dec : forall n m : NZ, decidable (n == m). Proof. intros n m; destruct (NZlt_trichotomy n m) as [H | [H | H]]. right; intro H1; rewrite H1 in H; false_hyp H NZlt_irrefl. @@ -226,7 +236,7 @@ Qed. Theorem NZeq_dne : forall n m, ~ ~ n == m <-> n == m. Proof. intros n m; split; intro H. -destruct (NZeq_em n m) as [H1 | H1]. +destruct (NZeq_dec n m) as [H1 | H1]. assumption. false_hyp H1 H. intro H1; now apply H1. Qed. @@ -241,7 +251,7 @@ Qed. Theorem NZle_gt_cases : forall n m : NZ, n <= m \/ n > m. Proof. intros n m; destruct (NZlt_trichotomy n m) as [H | [H | H]]. -left; now le_less. left; now le_equal. now right. +left; now apply NZlt_le_incl. left; now apply NZeq_le_incl. now right. Qed. (* The following theorem is cleary redundant, but helps not to @@ -255,7 +265,7 @@ Qed. Theorem NZle_ge_cases : forall n m : NZ, n <= m \/ n >= m. Proof. intros n m; destruct (NZle_gt_cases n m) as [H | H]. -now left. right; le_less. +now left. right; now apply NZlt_le_incl. Qed. Theorem NZle_ngt : forall n m : NZ, n <= m <-> ~ n > m. @@ -267,12 +277,13 @@ assumption. false_hyp H1 H. Qed. (* Redundant but useful *) + Theorem NZnlt_ge : forall n m : NZ, ~ n < m <-> n >= m. Proof. intros n m; symmetry; apply NZle_ngt. Qed. -Theorem NZlt_em : forall n m : NZ, n < m \/ ~ n < m. +Theorem NZlt_dec : forall n m : NZ, decidable (n < m). Proof. intros n m; destruct (NZle_gt_cases m n); [right; now apply -> NZle_ngt | now left]. @@ -281,7 +292,7 @@ Qed. Theorem NZlt_dne : forall n m, ~ ~ n < m <-> n < m. Proof. intros n m; split; intro H; -[destruct (NZlt_em n m) as [H1 | H1]; [assumption | false_hyp H1 H] | +[destruct (NZlt_dec n m) as [H1 | H1]; [assumption | false_hyp H1 H] | intro H1; false_hyp H H1]. Qed. @@ -291,12 +302,13 @@ intros n m. rewrite NZle_ngt. apply NZlt_dne. Qed. (* Redundant but useful *) + Theorem NZlt_nge : forall n m : NZ, n < m <-> ~ n >= m. Proof. intros n m; symmetry; apply NZnle_gt. Qed. -Theorem NZle_em : forall n m : NZ, n <= m \/ ~ n <= m. +Theorem NZle_dec : forall n m : NZ, decidable (n <= m). Proof. intros n m; destruct (NZle_gt_cases n m); [now left | right; now apply <- NZnle_gt]. @@ -305,13 +317,13 @@ Qed. Theorem NZle_dne : forall n m : NZ, ~ ~ n <= m <-> n <= m. Proof. intros n m; split; intro H; -[destruct (NZle_em n m) as [H1 | H1]; [assumption | false_hyp H1 H] | +[destruct (NZle_dec n m) as [H1 | H1]; [assumption | false_hyp H1 H] | intro H1; false_hyp H H1]. Qed. -Theorem NZlt_nlt_succ : forall n m : NZ, n < m <-> ~ m < S n. +Theorem NZnlt_succ_r : forall n m : NZ, ~ m < S n <-> n < m. Proof. -intros n m; rewrite NZlt_succ_le; symmetry; apply NZnle_gt. +intros n m; rewrite NZlt_succ_r; apply NZnle_gt. Qed. (* The difference between integers and natural numbers is that for @@ -327,9 +339,9 @@ Proof. intro z; NZinduct n z. intros m H1 H2; apply <- NZnle_gt in H1; false_hyp H2 H1. intro n; split; intros IH m H1 H2. -apply -> NZle_succ_le_or_eq_succ in H2; destruct H2 as [H2 | H2]. -now apply IH. exists n. now split; [| rewrite <- NZlt_succ_le; rewrite <- H2]. -apply IH. assumption. now apply NZle_le_succ. +apply -> NZle_succ_r in H2; destruct H2 as [H2 | H2]. +now apply IH. exists n. now split; [| rewrite <- NZlt_succ_r; rewrite <- H2]. +apply IH. assumption. now apply NZle_le_succ_r. Qed. Theorem NZlt_exists_pred : @@ -351,7 +363,7 @@ Theorem NZlt_succ_iter_r : forall (n : nat) (m : NZ), m < NZsucc_iter (Datatypes.S n) m. Proof. intros n m; induction n as [| n IH]; simpl in *. -apply NZlt_succ_r. now apply NZlt_lt_succ. +apply NZlt_succ_diag_r. now apply NZlt_lt_succ_r. Qed. Theorem NZneq_succ_iter_l : @@ -389,16 +401,16 @@ Lemma NZrs_rs' : A z -> right_step -> right_step'. Proof. intros Az RS n H1 H2. le_elim H1. apply NZlt_exists_pred in H1. destruct H1 as [k [H3 H4]]. -rewrite H3. apply RS; [assumption | apply H2; [assumption | rewrite H3; apply NZlt_succ_r]]. +rewrite H3. apply RS; [assumption | apply H2; [assumption | rewrite H3; apply NZlt_succ_diag_r]]. rewrite <- H1; apply Az. Qed. Lemma NZrs'_rs'' : right_step' -> right_step''. Proof. intros RS' n; split; intros H1 m H2 H3. -apply -> NZlt_succ_le in H3; le_elim H3; +apply -> NZlt_succ_r in H3; le_elim H3; [now apply H1 | rewrite H3 in *; now apply RS']. -apply H1; [assumption | now apply NZlt_lt_succ]. +apply H1; [assumption | now apply NZlt_lt_succ_r]. Qed. Lemma NZrbase : A' z. @@ -408,7 +420,7 @@ Qed. Lemma NZA'A_right : (forall n : NZ, A' n) -> forall n : NZ, z <= n -> A n. Proof. -intros H1 n H2. apply H1 with (n := S n); [assumption | apply NZlt_succ_r]. +intros H1 n H2. apply H1 with (n := S n); [assumption | apply NZlt_succ_diag_r]. Qed. Theorem NZstrong_right_induction: right_step' -> forall n : NZ, z <= n -> A n. @@ -427,9 +439,9 @@ Theorem NZright_induction' : Proof. intros L R n. destruct (NZlt_trichotomy n z) as [H | [H | H]]. -apply L; now le_less. -apply L; now le_equal. -apply NZright_induction. apply L; now le_equal. assumption. now le_less. +apply L; now apply NZlt_le_incl. +apply L; now apply NZeq_le_incl. +apply NZright_induction. apply L; now apply NZeq_le_incl. assumption. now apply NZlt_le_incl. Qed. Theorem NZstrong_right_induction' : @@ -437,9 +449,9 @@ Theorem NZstrong_right_induction' : Proof. intros L R n. destruct (NZlt_trichotomy n z) as [H | [H | H]]. -apply L; now le_less. -apply L; now le_equal. -apply NZstrong_right_induction. assumption. now le_less. +apply L; now apply NZlt_le_incl. +apply L; now apply NZeq_le_incl. +apply NZstrong_right_induction. assumption. now apply NZlt_le_incl. Qed. End RightInduction. @@ -454,28 +466,28 @@ Let left_step'' := forall n : NZ, A' n <-> A' (S n). Lemma NZls_ls' : A z -> left_step -> left_step'. Proof. intros Az LS n H1 H2. le_elim H1. -apply LS; [assumption | apply H2; [now apply -> NZlt_le_succ | now le_equal]]. +apply LS; [assumption | apply H2; [now apply <- NZle_succ_l | now apply NZeq_le_incl]]. rewrite H1; apply Az. Qed. Lemma NZls'_ls'' : left_step' -> left_step''. Proof. intros LS' n; split; intros H1 m H2 H3. -apply NZle_succ_le in H3. now apply H1. +apply -> NZle_succ_l in H3. apply NZlt_le_incl in H3. now apply H1. le_elim H3. -apply -> NZlt_le_succ in H3. now apply H1. +apply <- NZle_succ_l in H3. now apply H1. rewrite <- H3 in *; now apply LS'. Qed. Lemma NZlbase : A' (S z). Proof. -intros m H1 H2. apply <- NZlt_le_succ in H2. +intros m H1 H2. apply -> NZle_succ_l in H2. apply -> NZle_ngt in H1. false_hyp H2 H1. Qed. Lemma NZA'A_left : (forall n : NZ, A' n) -> forall n : NZ, n <= z -> A n. Proof. -intros H1 n H2. apply H1 with (n := n); [assumption | now le_equal]. +intros H1 n H2. apply H1 with (n := n); [assumption | now apply NZeq_le_incl]. Qed. Theorem NZstrong_left_induction: left_step' -> forall n : NZ, n <= z -> A n. @@ -494,9 +506,9 @@ Theorem NZleft_induction' : Proof. intros R L n. destruct (NZlt_trichotomy n z) as [H | [H | H]]. -apply NZleft_induction. apply R. now le_equal. assumption. now le_less. -rewrite H; apply R; le_equal. -apply R; le_less. +apply NZleft_induction. apply R. now apply NZeq_le_incl. assumption. now apply NZlt_le_incl. +rewrite H; apply R; now apply NZeq_le_incl. +apply R; now apply NZlt_le_incl. Qed. Theorem NZstrong_left_induction' : @@ -504,9 +516,9 @@ Theorem NZstrong_left_induction' : Proof. intros R L n. destruct (NZlt_trichotomy n z) as [H | [H | H]]. -apply NZstrong_left_induction; auto. le_less. -rewrite H; apply R; le_equal. -apply R; le_less. +apply NZstrong_left_induction; auto. now apply NZlt_le_incl. +rewrite H; apply R; now apply NZeq_le_incl. +apply R; now apply NZlt_le_incl. Qed. End LeftInduction. @@ -519,9 +531,9 @@ Theorem NZorder_induction : Proof. intros Az RS LS n. destruct (NZlt_trichotomy n z) as [H | [H | H]]. -now apply NZleft_induction; [| | le_less]. +now apply NZleft_induction; [| | apply NZlt_le_incl]. now rewrite H. -now apply NZright_induction; [| | le_less]. +now apply NZright_induction; [| | apply NZlt_le_incl]. Qed. Theorem NZorder_induction' : @@ -531,7 +543,7 @@ Theorem NZorder_induction' : forall n : NZ, A n. Proof. intros Az AS AP n; apply NZorder_induction; try assumption. -intros m H1 H2. apply AP in H2; [| now apply -> NZlt_le_succ]. +intros m H1 H2. apply AP in H2; [| now apply <- NZle_succ_l]. unfold predicate_wd, fun_wd in A_wd; apply -> (A_wd (P (S m)) m); [assumption | apply NZpred_succ]. Qed. @@ -560,8 +572,8 @@ Theorem NZlt_ind : forall (n : NZ), forall m : NZ, n < m -> A m. Proof. intros n H1 H2 m H3. -apply NZright_induction with (S n); [assumption | | now apply -> NZlt_le_succ]. -intros; apply H2; try assumption. now apply <- NZlt_le_succ. +apply NZright_induction with (S n); [assumption | | now apply <- NZle_succ_l]. +intros; apply H2; try assumption. now apply -> NZle_succ_l. Qed. (** Elimintation principle for <= *) @@ -632,7 +644,7 @@ apply NZAcc_gt_wd. intros n H; constructor; intros y [H1 H2]. apply <- NZnle_gt in H2. elim H2. now apply NZle_lt_trans with n. intros n H1 H2; constructor; intros m [H3 H4]. -apply H2. assumption. now apply -> NZlt_le_succ. +apply H2. assumption. now apply <- NZle_succ_l. Qed. End WF. diff --git a/theories/Numbers/NatInt/NZTimes.v b/theories/Numbers/NatInt/NZTimes.v index e0d1f63501..20bd3cdc61 100644 --- a/theories/Numbers/NatInt/NZTimes.v +++ b/theories/Numbers/NatInt/NZTimes.v @@ -17,20 +17,20 @@ Module NZTimesPropFunct (Import NZAxiomsMod : NZAxiomsSig). Module Export NZPlusPropMod := NZPlusPropFunct NZAxiomsMod. Open Local Scope NatIntScope. -Theorem NZtimes_0_l : forall n : NZ, 0 * n == 0. +Theorem NZtimes_0_r : forall n : NZ, n * 0 == 0. Proof. NZinduct n. -now rewrite NZtimes_0_r. -intro. rewrite NZtimes_succ_r. now rewrite NZplus_0_r. +now rewrite NZtimes_0_l. +intro. rewrite NZtimes_succ_l. now rewrite NZplus_0_r. Qed. -Theorem NZtimes_succ_l : forall n m : NZ, (S n) * m == n * m + m. +Theorem NZtimes_succ_r : forall n m : NZ, n * (S m) == n * m + n. Proof. -intros n m; NZinduct m. -do 2 rewrite NZtimes_0_r; now rewrite NZplus_0_l. -intro m. do 2 rewrite NZtimes_succ_r. do 2 rewrite NZplus_succ_r. -rewrite NZsucc_inj_wd. rewrite <- (NZplus_assoc (n * m) n m). -rewrite (NZplus_comm n m). rewrite NZplus_assoc. +intros n m; NZinduct n. +do 2 rewrite NZtimes_0_l; now rewrite NZplus_0_l. +intro n. do 2 rewrite NZtimes_succ_l. do 2 rewrite NZplus_succ_r. +rewrite NZsucc_inj_wd. rewrite <- (NZplus_assoc (n * m) m n). +rewrite (NZplus_comm m n). rewrite NZplus_assoc. now rewrite NZplus_cancel_r. Qed. diff --git a/theories/Numbers/NatInt/NZTimesOrder.v b/theories/Numbers/NatInt/NZTimesOrder.v index 6fc0078c04..4b4516069e 100644 --- a/theories/Numbers/NatInt/NZTimesOrder.v +++ b/theories/Numbers/NatInt/NZTimesOrder.v @@ -200,11 +200,11 @@ Theorem NZtimes_lt_mono_neg_l : forall p n m : NZ, p < 0 -> (n < m <-> p * m < p Proof. NZord_induct p. intros n m H; false_hyp H NZlt_irrefl. -intros p H1 _ n m H2. apply NZlt_succ_lt in H2. apply <- NZnle_gt in H2. false_hyp H1 H2. -intros p H IH n m H1. apply -> NZlt_le_succ in H. +intros p H1 _ n m H2. apply NZlt_succ_l in H2. apply <- NZnle_gt in H2. false_hyp H1 H2. +intros p H IH n m H1. apply <- NZle_succ_l in H. le_elim H. assert (LR : forall n m : NZ, n < m -> p * m < p * n). intros n1 m1 H2. apply (NZle_lt_plus_lt n1 m1). -now le_less. do 2 rewrite <- NZtimes_succ_l. now apply -> IH. +now apply NZlt_le_incl. do 2 rewrite <- NZtimes_succ_l. now apply -> IH. split; [apply LR |]. intro H2. apply -> NZlt_dne; intro H3. apply <- NZle_ngt in H3. le_elim H3. apply NZlt_asymm in H2. apply H2. now apply LR. @@ -222,17 +222,17 @@ Qed. Theorem NZtimes_le_mono_nonneg_l : forall n m p : NZ, 0 <= p -> n <= m -> p * n <= p * m. Proof. intros n m p H1 H2. le_elim H1. -le_elim H2. le_less. now apply -> NZtimes_lt_mono_pos_l. -le_equal; now rewrite H2. -le_equal; rewrite <- H1; now do 2 rewrite NZtimes_0_l. +le_elim H2. apply NZlt_le_incl. now apply -> NZtimes_lt_mono_pos_l. +apply NZeq_le_incl; now rewrite H2. +apply NZeq_le_incl; rewrite <- H1; now do 2 rewrite NZtimes_0_l. Qed. Theorem NZtimes_le_mono_nonpos_l : forall n m p : NZ, p <= 0 -> n <= m -> p * m <= p * n. Proof. intros n m p H1 H2. le_elim H1. -le_elim H2. le_less. now apply -> NZtimes_lt_mono_neg_l. -le_equal; now rewrite H2. -le_equal; rewrite H1; now do 2 rewrite NZtimes_0_l. +le_elim H2. apply NZlt_le_incl. now apply -> NZtimes_lt_mono_neg_l. +apply NZeq_le_incl; now rewrite H2. +apply NZeq_le_incl; rewrite H1; now do 2 rewrite NZtimes_0_l. Qed. Theorem NZtimes_le_mono_nonneg_r : forall n m p : NZ, 0 <= p -> n <= m -> n * p <= m * p. @@ -272,7 +272,7 @@ Qed. Theorem NZtimes_le_mono_pos_l : forall n m p : NZ, 0 < p -> (n <= m <-> p * n <= p * m). Proof. -intros n m p H; do 2 rewrite NZle_lt_or_eq. +intros n m p H; do 2 rewrite NZlt_eq_cases. rewrite (NZtimes_lt_mono_pos_l p n m); [assumption |]. now rewrite -> (NZtimes_cancel_l n m p); [intro H1; rewrite H1 in H; false_hyp H NZlt_irrefl |]. @@ -286,7 +286,7 @@ Qed. Theorem NZtimes_le_mono_neg_l : forall n m p : NZ, p < 0 -> (n <= m <-> p * m <= p * n). Proof. -intros n m p H; do 2 rewrite NZle_lt_or_eq. +intros n m p H; do 2 rewrite NZlt_eq_cases. rewrite (NZtimes_lt_mono_neg_l p n m); [assumption |]. rewrite -> (NZtimes_cancel_l m n p); [intro H1; rewrite H1 in H; false_hyp H NZlt_irrefl |]. @@ -304,7 +304,7 @@ Theorem NZtimes_lt_mono : Proof. intros n m p q H1 H2 H3 H4. apply NZle_lt_trans with (m * p). -apply NZtimes_le_mono_nonneg_r; [assumption | now le_less]. +apply NZtimes_le_mono_nonneg_r; [assumption | now apply NZlt_le_incl]. apply -> NZtimes_lt_mono_pos_l; [assumption | now apply NZle_lt_trans with n]. Qed. @@ -316,10 +316,10 @@ Theorem NZtimes_le_mono : Proof. intros n m p q H1 H2 H3 H4. le_elim H2; le_elim H4. -le_less; now apply NZtimes_lt_mono. -rewrite <- H4; apply NZtimes_le_mono_nonneg_r; [assumption | now le_less]. -rewrite <- H2; apply NZtimes_le_mono_nonneg_l; [assumption | now le_less]. -rewrite H2; rewrite H4; now le_equal. +apply NZlt_le_incl; now apply NZtimes_lt_mono. +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. Qed. Theorem NZtimes_pos_pos : forall n m : NZ, 0 < n -> 0 < m -> 0 < n * m. @@ -368,25 +368,46 @@ Proof. intros; rewrite NZtimes_comm; now apply NZtimes_nonneg_nonpos. Qed. -Theorem NZtimes_eq_0 : forall n m : NZ, n * m == 0 -> n == 0 \/ m == 0. +Theorem NZlt_1_times_pos : forall n m : NZ, 1 < n -> 0 < m -> 1 < n * m. Proof. -intros n m H; destruct (NZlt_trichotomy n 0) as [H1 | [H1 | H1]]; +intros n m H1 H2. apply -> (NZtimes_lt_mono_pos_r m) in H1. +rewrite NZtimes_1_l in H1. now apply NZlt_1_l with m. +assumption. +Qed. + +Theorem NZeq_times_0 : forall n m : NZ, n * m == 0 <-> n == 0 \/ m == 0. +Proof. +intros n m; split. +intro H; destruct (NZlt_trichotomy n 0) as [H1 | [H1 | H1]]; destruct (NZlt_trichotomy m 0) as [H2 | [H2 | H2]]; try (now right); try (now left). elimtype False; now apply (NZlt_neq 0 (n * m)); [apply NZtimes_neg_neg |]. elimtype False; now apply (NZlt_neq (n * m) 0); [apply NZtimes_neg_pos |]. elimtype False; now apply (NZlt_neq (n * m) 0); [apply NZtimes_pos_neg |]. elimtype False; now apply (NZlt_neq 0 (n * m)); [apply NZtimes_pos_pos |]. +intros [H | H]. now rewrite H, NZtimes_0_l. now rewrite H, NZtimes_0_r. Qed. -Theorem NZtimes_neq_0 : forall n m : NZ, n ~= 0 /\ m ~= 0 <-> n * m ~= 0. +Theorem NZneq_times_0 : forall n m : NZ, n ~= 0 /\ m ~= 0 <-> n * m ~= 0. Proof. intros n m; split; intro H. -intro H1; apply NZtimes_eq_0 in H1. tauto. +intro H1; apply -> NZeq_times_0 in H1. tauto. split; intro H1; rewrite H1 in H; (rewrite NZtimes_0_l in H || rewrite NZtimes_0_r in H); now apply H. Qed. +Theorem NZeq_times_0_l : forall n m : NZ, n * m == 0 -> m ~= 0 -> n == 0. +Proof. +intros n m H1 H2. apply -> NZeq_times_0 in H1. destruct H1 as [H1 | H1]. +assumption. false_hyp H1 H2. +Qed. + +Theorem NZeq_times_0_r : forall n m : NZ, n * m == 0 -> n ~= 0 -> m == 0. +Proof. +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). Proof. intros n m; split; [intro H | intros [[H1 H2] | [H1 H2]]]. @@ -420,12 +441,12 @@ 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. +intros n m H. apply <- NZle_succ_l 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. +now apply -> NZle_succ_l. +apply NZplus_pos_pos; now apply NZlt_succ_diag_r. Qed. End NZTimesOrderPropFunct. diff --git a/theories/Numbers/Natural/Abstract/NAxioms.v b/theories/Numbers/Natural/Abstract/NAxioms.v index 7cfff8e030..86a828d037 100644 --- a/theories/Numbers/Natural/Abstract/NAxioms.v +++ b/theories/Numbers/Natural/Abstract/NAxioms.v @@ -64,5 +64,8 @@ Axiom recursion_succ : Aeq a a -> fun2_wd Neq Aeq Aeq f -> forall n : N, Aeq (recursion a f (S n)) (f n (recursion a f n)). +(*Axiom dep_rec : + forall A : N -> Type, A 0 -> (forall n : N, A n -> A (S n)) -> forall n : N, A n.*) + End NAxiomsSig. diff --git a/theories/Numbers/Natural/Abstract/NBase.v b/theories/Numbers/Natural/Abstract/NBase.v index d71f98057f..bcef668677 100644 --- a/theories/Numbers/Natural/Abstract/NBase.v +++ b/theories/Numbers/Natural/Abstract/NBase.v @@ -10,6 +10,7 @@ (*i i*) +Require Export Decidable. Require Export NAxioms. Require Import NZTimesOrder. (* The last property functor on NZ, which subsumes all others *) @@ -59,8 +60,8 @@ Proof NZsucc_inj_wd_neg. (* Decidability and stability of equality was proved only in NZOrder, but since it does not mention order, we'll put it here *) -Theorem eq_em : forall n m : N, n == m \/ n ~= m. -Proof NZeq_em. +Theorem eq_dec : forall n m : N, decidable (n == m). +Proof NZeq_dec. Theorem eq_dne : forall n m : N, ~ ~ n == m <-> n == m. Proof NZeq_dne. @@ -99,16 +100,21 @@ pattern false at 2; replace false with (if_zero false true 0) by apply if_zero_0 now rewrite H. Qed. +Theorem neq_0_succ : forall n : N, 0 ~= S n. +Proof. +intro n; apply neq_symm; apply neq_succ_0. +Qed. + (* Next, we show that all numbers are nonnegative and recover regular induction from the bidirectional induction on NZ *) Theorem le_0_l : forall n : N, 0 <= n. Proof. NZinduct n. -le_equal. +now apply NZeq_le_incl. intro n; split. -apply NZle_le_succ. -intro H; apply -> NZle_succ_le_or_eq_succ in H; destruct H as [H | H]. +apply NZle_le_succ_r. +intro H; apply -> NZle_succ_r in H; destruct H as [H | H]. assumption. symmetry in H; false_hyp H neq_succ_0. Qed. @@ -144,7 +150,7 @@ Proof. intro H; apply (neq_succ_0 0). apply H. Qed. -Theorem neq_0_succ : forall n, n ~= 0 <-> exists m, n == S m. +Theorem neq_0_r : forall n, n ~= 0 <-> exists m, n == S m. Proof. cases n. split; intro H; [now elim H | destruct H as [m H]; symmetry in H; false_hyp H neq_succ_0]. diff --git a/theories/Numbers/Natural/Abstract/NMinus.v b/theories/Numbers/Natural/Abstract/NMinus.v index c109ff904a..f7c9cf19bb 100644 --- a/theories/Numbers/Natural/Abstract/NMinus.v +++ b/theories/Numbers/Natural/Abstract/NMinus.v @@ -63,8 +63,8 @@ Proof. intros n m p; induct p. intro; now do 2 rewrite minus_0_r. intros p IH H. do 2 rewrite minus_succ_r. -rewrite <- IH; [now apply le_succ_le |]. -rewrite plus_pred_r. apply minus_gt. now apply <- lt_le_succ. +rewrite <- IH; [apply lt_le_incl; now apply -> le_succ_l |]. +rewrite plus_pred_r. apply minus_gt. now apply -> le_succ_l. reflexivity. Qed. @@ -129,7 +129,7 @@ Qed. Theorem le_minus_l : forall n m : N, n - m <= n. Proof. intro n; induct m. -rewrite minus_0_r; le_equal. +rewrite minus_0_r; now apply eq_le_incl. intros m IH. rewrite minus_succ_r. apply le_trans with (n - m); [apply le_pred_l | assumption]. Qed. @@ -150,7 +150,7 @@ Proof. intros n m; cases m. now rewrite pred_0, times_0_r, minus_0_l. intro m; rewrite pred_succ, times_succ_r, <- plus_minus_assoc. -le_equal. +now apply eq_le_incl. now rewrite minus_diag, plus_0_r. Qed. @@ -163,7 +163,7 @@ rewrite minus_succ_l; [assumption |]. do 2 rewrite times_succ_l. rewrite (plus_comm ((n - m) * p) p), (plus_comm (n * p) p). rewrite <- (plus_minus_assoc p (n * p) (m * p)); [now apply times_le_mono_r |]. now apply <- plus_cancel_l. -assert (H1 : S n <= m); [now apply -> lt_le_succ |]. +assert (H1 : S n <= m); [now apply <- le_succ_l |]. setoid_replace (S n - m) with 0 by now apply <- minus_0_le. setoid_replace ((S n * p) - m * p) with 0 by (apply <- minus_0_le; now apply times_le_mono_r). apply times_0_l. diff --git a/theories/Numbers/Natural/Abstract/NOrder.v b/theories/Numbers/Natural/Abstract/NOrder.v index bc3aace381..33214cd1bf 100644 --- a/theories/Numbers/Natural/Abstract/NOrder.v +++ b/theories/Numbers/Natural/Abstract/NOrder.v @@ -36,14 +36,14 @@ Theorem max_wd : forall n1 n2 : N, n1 == n2 -> forall m1 m2 : N, m1 == m2 -> max n1 m1 == max n2 m2. Proof NZmax_wd. -Theorem le_lt_or_eq : forall n m : N, n <= m <-> n < m \/ n == m. -Proof NZle_lt_or_eq. +Theorem lt_eq_cases : forall n m : N, n <= m <-> n < m \/ n == m. +Proof NZlt_eq_cases. Theorem lt_irrefl : forall n : N, ~ n < n. Proof NZlt_irrefl. -Theorem lt_succ_le : forall n m : N, n < S m <-> n <= m. -Proof NZlt_succ_le. +Theorem lt_succ_r : forall n m : N, n < S m <-> n <= m. +Proof NZlt_succ_r. Theorem min_l : forall n m : N, n <= m -> min n m == n. Proof NZmin_l. @@ -62,47 +62,50 @@ Proof NZmax_r. Theorem lt_le_incl : forall n m : N, n < m -> n <= m. Proof NZlt_le_incl. +Theorem eq_le_incl : forall n m : N, n == m -> n <= m. +Proof NZeq_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_neq : forall n m : N, n < m <-> n <= m /\ n ~= m. +Proof NZle_neq. Theorem le_refl : forall n : N, n <= n. Proof NZle_refl. -Theorem lt_succ_r : forall n : N, n < S n. -Proof NZlt_succ_r. +Theorem lt_succ_diag_r : forall n : N, n < S n. +Proof NZlt_succ_diag_r. -Theorem le_succ_r : forall n : N, n <= S n. -Proof NZle_succ_r. +Theorem le_succ_diag_r : forall n : N, n <= S n. +Proof NZle_succ_diag_r. -Theorem lt_lt_succ : forall n m : N, n < m -> n < S m. -Proof NZlt_lt_succ. +Theorem lt_lt_succ_r : forall n m : N, n < m -> n < S m. +Proof NZlt_lt_succ_r. -Theorem le_le_succ : forall n m : N, n <= m -> n <= S m. -Proof NZle_le_succ. +Theorem le_le_succ_r : forall n m : N, n <= m -> n <= S m. +Proof NZle_le_succ_r. -Theorem le_succ_le_or_eq_succ : forall n m : N, n <= S m <-> n <= m \/ n == S m. -Proof NZle_succ_le_or_eq_succ. +Theorem le_succ_r : forall n m : N, n <= S m <-> n <= m \/ n == S m. +Proof NZle_succ_r. -Theorem neq_succ_l : forall n : N, S n ~= n. -Proof NZneq_succ_l. +Theorem neq_succ_diag_l : forall n : N, S n ~= n. +Proof NZneq_succ_diag_l. -Theorem nlt_succ_l : forall n : N, ~ S n < n. -Proof NZnlt_succ_l. +Theorem neq_succ_diag_r : forall n : N, n ~= S n. +Proof NZneq_succ_diag_r. -Theorem nle_succ_l : forall n : N, ~ S n <= n. -Proof NZnle_succ_l. +Theorem nlt_succ_diag_l : forall n : N, ~ S n < n. +Proof NZnlt_succ_diag_l. -Theorem lt_le_succ : forall n m : N, n < m <-> S n <= m. -Proof NZlt_le_succ. +Theorem nle_succ_diag_l : forall n : N, ~ S n <= n. +Proof NZnle_succ_diag_l. -Theorem lt_succ_lt : forall n m : N, S n < m -> n < m. -Proof NZlt_succ_lt. +Theorem le_succ_l : forall n m : N, S n <= m <-> n < m. +Proof NZle_succ_l. -Theorem le_succ_le : forall n m : N, S n <= m -> n <= m. -Proof NZle_succ_le. +Theorem lt_succ_l : forall n m : N, S n < m -> n < m. +Proof NZlt_succ_l. Theorem succ_lt_mono : forall n m : N, n < m <-> S n < S m. Proof NZsucc_lt_mono. @@ -110,9 +113,11 @@ Proof NZsucc_lt_mono. Theorem succ_le_mono : forall n m : N, n <= m <-> S n <= S m. Proof NZsucc_le_mono. -Theorem lt_asymm : forall n m, n < m -> ~ m < n. +Theorem lt_asymm : forall n m : N, n < m -> ~ m < n. Proof NZlt_asymm. +Notation lt_ngt := lt_asymm (only parsing). + Theorem lt_trans : forall n m p : N, n < m -> m < p -> n < p. Proof NZlt_trans. @@ -133,6 +138,8 @@ Proof NZle_antisymm. Theorem lt_trichotomy : forall n m : N, n < m \/ n == m \/ m < n. Proof NZlt_trichotomy. +Notation lt_eq_gt_cases := lt_trichotomy (only parsing). + Theorem lt_gt_cases : forall n m : N, n ~= m <-> n < m \/ n > m. Proof NZlt_gt_cases. @@ -151,10 +158,10 @@ Proof NZle_ngt. Theorem nlt_ge : forall n m : N, ~ n < m <-> n >= m. Proof NZnlt_ge. -Theorem lt_em : forall n m : N, n < m \/ ~ n < m. -Proof NZlt_em. +Theorem lt_dec : forall n m : N, decidable (n < m). +Proof NZlt_dec. -Theorem lt_dne : forall n m, ~ ~ n < m <-> n < m. +Theorem lt_dne : forall n m : N, ~ ~ n < m <-> n < m. Proof NZlt_dne. Theorem nle_gt : forall n m : N, ~ n <= m <-> n > m. @@ -163,14 +170,14 @@ Proof NZnle_gt. Theorem lt_nge : forall n m : N, n < m <-> ~ n >= m. Proof NZlt_nge. -Theorem le_em : forall n m : N, n <= m \/ ~ n <= m. -Proof NZle_em. +Theorem le_dec : forall n m : N, decidable (n <= m). +Proof NZle_dec. Theorem le_dne : forall n m : N, ~ ~ n <= m <-> n <= m. Proof NZle_dne. -Theorem lt_nlt_succ : forall n m : N, n < m <-> ~ m < S n. -Proof NZlt_nlt_succ. +Theorem nlt_succ_r : forall n m : N, ~ m < S n <-> n < m. +Proof NZnlt_succ_r. Theorem lt_exists_pred : forall z n : N, z < n -> exists k : N, n == S k /\ z <= k. @@ -212,9 +219,9 @@ Proof NZright_induction'. Theorem left_induction' : forall A : N -> Prop, predicate_wd Neq A -> forall z : N, - (forall n : NZ, z <= n -> A n) -> + (forall n : N, z <= n -> A n) -> (forall n : N, n < z -> A (S n) -> A n) -> - forall n : NZ, A n. + forall n : N, A n. Proof NZleft_induction'. Theorem strong_right_induction : @@ -313,35 +320,75 @@ Proof. intro n; apply -> le_ngt. apply le_0_l. Qed. -Theorem nle_succ_0 : forall n, ~ (S n <= 0). +Theorem nle_succ_0 : forall n : N, ~ (S n <= 0). Proof. -intros n H; apply <- lt_le_succ in H; false_hyp H nlt_0_r. +intros n H; apply -> le_succ_l in H; false_hyp H nlt_0_r. Qed. -Theorem le_0_eq_0 : forall n, n <= 0 <-> n == 0. +Theorem le_0_r : forall n : N, n <= 0 <-> n == 0. Proof. intros n; split; intro H. le_elim H; [false_hyp H nlt_0_r | assumption]. -le_equal. +now apply eq_le_incl. Qed. -Theorem lt_0_succ : forall n, 0 < S n. +Theorem lt_0_succ : forall n : N, 0 < S n. Proof. -induct n; [apply lt_succ_r | intros n H; now apply lt_lt_succ]. +induct n; [apply lt_succ_diag_r | intros n H; now apply lt_lt_succ_r]. Qed. -Theorem lt_lt_0 : forall n m, n < m -> 0 < m. +Theorem neq_0_lt_0 : forall n : N, n ~= 0 <-> 0 < n. +Proof. +cases n. +split; intro H; [now elim H | intro; now apply lt_irrefl with 0]. +intro n; split; intro H; [apply lt_0_succ | apply neq_succ_0]. +Qed. + +Theorem eq_0_gt_0_cases : forall n : N, n == 0 \/ 0 < n. +Proof. +cases n. +now left. +intro; right; apply lt_0_succ. +Qed. + +Theorem zero_one : forall n : N, n == 0 \/ n == 1 \/ 1 < n. +Proof. +induct n. now left. +cases n. intros; right; now left. +intros n IH. destruct IH as [H | [H | H]]. +false_hyp H neq_succ_0. +right; right. rewrite H. apply lt_succ_diag_r. +right; right. now apply lt_lt_succ_r. +Qed. + +Theorem lt_1_r : forall n : N, n < 1 <-> n == 0. +Proof. +cases n. +split; intro; [reflexivity | apply lt_succ_diag_r]. +intros n. rewrite <- succ_lt_mono. +split; intro H; [false_hyp H nlt_0_r | false_hyp H neq_succ_0]. +Qed. + +Theorem le_1_r : forall n : N, n <= 1 <-> n == 0 \/ n == 1. +Proof. +cases n. +split; intro; [now left | apply le_succ_diag_r]. +intro n. rewrite <- succ_le_mono, le_0_r, succ_inj_wd. +split; [intro; now right | intros [H | H]; [false_hyp H neq_succ_0 | assumption]]. +Qed. + +Theorem lt_lt_0 : forall n m : N, n < m -> 0 < m. Proof. intros n m; induct n. trivial. -intros n IH H. apply IH; now apply lt_succ_lt. +intros n IH H. apply IH; now apply lt_succ_l. Qed. -Theorem neq_0_lt_0 : forall n, n ~= 0 <-> 0 < n. +Theorem lt_1_l : forall n m p : N, n < m -> m < p -> 1 < p. Proof. -cases n. -split; intro H; [now elim H | intro; now apply lt_irrefl with 0]. -intro n; split; intro H; [apply lt_0_succ | apply neq_succ_0]. +intros n m p H1 H2. +apply le_lt_trans with m. apply <- le_succ_l. apply le_lt_trans with n. +apply le_0_l. assumption. assumption. Qed. (** Elimination principlies for < and <= for relations *) @@ -357,30 +404,30 @@ Add Morphism R with signature Neq ==> Neq ==> iff as R_morph2. Proof R_wd. Theorem le_ind_rel : - (forall m, R 0 m) -> - (forall n m, n <= m -> R n m -> R (S n) (S m)) -> - forall n m, n <= m -> R n m. + (forall m : N, R 0 m) -> + (forall n m : N, n <= m -> R n m -> R (S n) (S m)) -> + forall n m : N, n <= m -> R n m. Proof. intros Base Step; induct n. intros; apply Base. intros n IH m H. elim H using le_ind. solve_predicate_wd. -apply Step; [| apply IH]; now le_equal. -intros k H1 H2. apply le_succ_le in H1. auto. +apply Step; [| apply IH]; now apply eq_le_incl. +intros k H1 H2. apply -> le_succ_l in H1. apply lt_le_incl in H1. auto. Qed. Theorem lt_ind_rel : - (forall m, R 0 (S m)) -> - (forall n m, n < m -> R n m -> R (S n) (S m)) -> - forall n m, n < m -> R n m. + (forall m : N, R 0 (S m)) -> + (forall n m : N, n < m -> R n m -> R (S n) (S m)) -> + forall n m : N, n < m -> R n m. Proof. intros Base Step; induct n. intros m H. apply lt_exists_pred in H; destruct H as [m' [H _]]. rewrite H; apply Base. intros n IH m H. elim H using lt_ind. solve_predicate_wd. -apply Step; [| apply IH]; now apply lt_succ_r. -intros k H1 H2. apply lt_succ_lt in H1. auto. +apply Step; [| apply IH]; now apply lt_succ_diag_r. +intros k H1 H2. apply lt_succ_l in H1. auto. Qed. End RelElim. @@ -396,15 +443,15 @@ Qed. Theorem le_pred_l : forall n : N, P n <= n. Proof. cases n. -rewrite pred_0; le_equal. -intros; rewrite pred_succ; apply le_succ_r. +rewrite pred_0; now apply eq_le_incl. +intros; rewrite pred_succ; apply le_succ_diag_r. Qed. Theorem lt_pred_l : forall n : N, n ~= 0 -> P n < n. Proof. cases n. intro H; elimtype False; now apply H. -intros; rewrite pred_succ; apply lt_succ_r. +intros; rewrite pred_succ; apply lt_succ_diag_r. Qed. Theorem le_le_pred : forall n m : N, n <= m -> P n <= m. @@ -421,14 +468,14 @@ Theorem lt_le_pred : forall n m : N, n < m -> n <= P m. (* Converse is false for Proof. intro n; cases m. intro H; false_hyp H nlt_0_r. -intros m IH. rewrite pred_succ; now apply -> lt_succ_le. +intros m IH. rewrite pred_succ; now apply -> lt_succ_r. Qed. Theorem lt_pred_le : forall n m : N, P n < m -> n <= m. (* Converse is false for n == m == 0 *) Proof. intros n m; cases n. -rewrite pred_0; intro H; le_less. -intros n IH. rewrite pred_succ in IH. now apply -> lt_le_succ. +rewrite pred_0; intro H; now apply lt_le_incl. +intros n IH. rewrite pred_succ in IH. now apply <- le_succ_l. Qed. Theorem lt_pred_lt : forall n m : N, n < P m -> n < m. @@ -467,12 +514,12 @@ Qed. Theorem le_succ_le_pred : forall n m : N, S n <= m -> n <= P m. (* Converse is false for n == m == 0 *) Proof. -intros n m H. apply lt_le_pred. now apply <- lt_le_succ. +intros n m H. apply lt_le_pred. now apply -> le_succ_l. Qed. Theorem lt_pred_lt_succ : forall n m : N, P n < m -> n < S m. (* Converse is false for n == m == 0 *) Proof. -intros n m H. apply <- lt_succ_le. now apply lt_pred_le. +intros n m H. apply <- lt_succ_r. now apply lt_pred_le. Qed. Theorem le_pred_le_succ : forall n m : N, P n <= m <-> n <= S m. diff --git a/theories/Numbers/Natural/Abstract/NPlus.v b/theories/Numbers/Natural/Abstract/NPlus.v index a033d95a09..d1269cf03f 100644 --- a/theories/Numbers/Natural/Abstract/NPlus.v +++ b/theories/Numbers/Natural/Abstract/NPlus.v @@ -61,7 +61,7 @@ Proof NZplus_cancel_r. (** Theorems that are valid for natural numbers but cannot be proved for Z *) -Theorem plus_eq_0 : forall n m : N, n + m == 0 <-> n == 0 /\ m == 0. +Theorem eq_plus_0 : forall n m : N, n + m == 0 <-> n == 0 /\ m == 0. Proof. intros n m; induct n. (* The next command does not work with the axiom plus_0_l from NPlusSig *) @@ -73,7 +73,7 @@ setoid_replace (S n == 0) with False using relation iff by (apply -> neg_false; apply neq_succ_0). tauto. Qed. -Theorem plus_eq_succ : +Theorem eq_plus_succ : forall n m : N, (exists p : N, n + m == S p) <-> (exists n' : N, n == S n') \/ (exists m' : N, m == S m'). Proof. @@ -88,16 +88,16 @@ left; now exists n. exists (n + m); now rewrite plus_succ_l. Qed. -Theorem plus_eq_1 : forall n m : N, +Theorem eq_plus_1 : forall n m : N, n + m == 1 -> n == 1 /\ m == 0 \/ n == 0 /\ m == 1. Proof. intros n m H. assert (H1 : exists p : N, n + m == S p) by now exists 0. -apply -> plus_eq_succ in H1. destruct H1 as [[n' H1] | [m' H1]]. +apply -> eq_plus_succ in H1. destruct H1 as [[n' H1] | [m' H1]]. left. rewrite H1 in H; rewrite plus_succ_l in H; apply succ_inj in H. -apply -> plus_eq_0 in H. destruct H as [H2 H3]; rewrite H2 in H1; now split. +apply -> eq_plus_0 in H. destruct H as [H2 H3]; rewrite H2 in H1; now split. right. rewrite H1 in H; rewrite plus_succ_r in H; apply succ_inj in H. -apply -> plus_eq_0 in H. destruct H as [H2 H3]; rewrite H3 in H1; now split. +apply -> eq_plus_0 in H. destruct H as [H2 H3]; rewrite H3 in H1; now split. Qed. Theorem succ_plus_discr : forall n m : N, m ~= S (n + m). diff --git a/theories/Numbers/Natural/Abstract/NTimes.v b/theories/Numbers/Natural/Abstract/NTimes.v index 6a22e476da..e15f02a1ef 100644 --- a/theories/Numbers/Natural/Abstract/NTimes.v +++ b/theories/Numbers/Natural/Abstract/NTimes.v @@ -20,20 +20,20 @@ Theorem times_wd : forall n1 n2 : N, n1 == n2 -> forall m1 m2 : N, m1 == m2 -> n1 * m1 == n2 * m2. Proof NZtimes_wd. -Theorem times_0_r : forall n, n * 0 == 0. -Proof NZtimes_0_r. - -Theorem times_succ_r : forall n m, n * (S m) == n * m + n. -Proof NZtimes_succ_r. - -(** Theorems that are valid for both natural numbers and integers *) - Theorem times_0_l : forall n : N, 0 * n == 0. Proof NZtimes_0_l. Theorem times_succ_l : forall n m : N, (S n) * m == n * m + m. Proof NZtimes_succ_l. +(** Theorems that are valid for both natural numbers and integers *) + +Theorem times_0_r : forall n, n * 0 == 0. +Proof NZtimes_0_r. + +Theorem times_succ_r : forall n m, n * (S m) == n * m + n. +Proof NZtimes_succ_r. + Theorem times_comm : forall n m : N, n * m == m * n. Proof NZtimes_comm. @@ -54,28 +54,6 @@ Proof NZtimes_1_r. (** Theorems that cannot be proved in NZTimes *) -Theorem times_eq_0 : forall n m, n * m == 0 -> n == 0 \/ m == 0. -Proof. -induct n; induct m. -intros; now left. -intros; now left. -intros; now right. -intros m IH H1. rewrite times_succ_l in H1. -rewrite plus_succ_r in H1. now apply neq_succ_0 in H1. -Qed. - -Theorem times_eq_1 : forall n m : N, n * m == 1 -> n == 1 /\ m == 1. -Proof. -intros n m; induct n. -intro H; rewrite times_0_l in H; symmetry in H; false_hyp H neq_succ_0. -intros n IH H. rewrite times_succ_l in H. apply plus_eq_1 in H. -destruct H as [[H1 H2] | [H1 H2]]. -apply IH in H1. destruct H1 as [_ H1]. rewrite H1 in H2; false_hyp H2 neq_succ_0. -apply times_eq_0 in H1. destruct H1 as [H1 | H1]. -rewrite H1; now split. -rewrite H2 in H1; false_hyp H1 neq_succ_0. -Qed. - (* In proving the correctness of the definition of multiplication on integers constructed from pairs of natural numbers, we'll need the following fact about natural numbers: diff --git a/theories/Numbers/Natural/Abstract/NTimesOrder.v b/theories/Numbers/Natural/Abstract/NTimesOrder.v index ec010ecee9..d6c0bfafa1 100644 --- a/theories/Numbers/Natural/Abstract/NTimesOrder.v +++ b/theories/Numbers/Natural/Abstract/NTimesOrder.v @@ -10,118 +10,56 @@ (*i i*) -Require Export NOrder. +Require Export NPlusOrder. Module NTimesOrderPropFunct (Import NAxiomsMod : NAxiomsSig). -Module Export NOrderPropMod := NOrderPropFunct NAxiomsMod. +Module Export NPlusOrderPropMod := NPlusOrderPropFunct NAxiomsMod. Open Local Scope NatScope. -Theorem plus_lt_mono_l : forall n m p : N, n < m <-> p + n < p + m. -Proof NZplus_lt_mono_l. - -Theorem plus_lt_mono_r : forall n m p : N, n < m <-> n + p < m + p. -Proof NZplus_lt_mono_r. - -Theorem plus_lt_mono : forall n m p q : N, n < m -> p < q -> n + p < m + q. -Proof NZplus_lt_mono. - -Theorem plus_le_mono_l : forall n m p : N, n <= m <-> p + n <= p + m. -Proof NZplus_le_mono_l. - -Theorem plus_le_mono_r : forall n m p : N, n <= m <-> n + p <= m + p. -Proof NZplus_le_mono_r. - -Theorem plus_le_mono : forall n m p q : N, n <= m -> p <= q -> n + p <= m + q. -Proof NZplus_le_mono. - -Theorem plus_lt_le_mono : forall n m p q : N, n < m -> p <= q -> n + p < m + q. -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_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 times_lt_pred : + forall p q n m : N, S p == q -> (p * n < p * m <-> q * n + m < q * m + n). +Proof NZtimes_lt_pred. -Theorem plus_le_cases : forall n m p q : N, n + m <= p + q -> n <= p \/ m <= q. -Proof NZplus_le_cases. +Theorem times_lt_mono_pos_l : forall p n m : N, 0 < p -> (n < m <-> p * n < p * m). +Proof NZtimes_lt_mono_pos_l. -Theorem plus_pos_cases : forall n m : N, 0 < n + m -> 0 < n \/ 0 < m. -Proof NZplus_pos_cases. +Theorem times_lt_mono_pos_r : forall p n m : N, 0 < p -> (n < m <-> n * p < m * p). +Proof NZtimes_lt_mono_pos_r. -(** Theorems true for natural numbers *) +Theorem times_cancel_l : forall n m p : N, p ~= 0 -> (p * n == p * m <-> n == m). +Proof NZtimes_cancel_l. -Theorem le_plus_r : forall n m : N, n <= n + m. -Proof. -intro n; induct m. -rewrite plus_0_r; le_equal. -intros m IH. rewrite plus_succ_r; now apply le_le_succ. -Qed. +Theorem times_cancel_r : forall n m p : N, p ~= 0 -> (n * p == m * p <-> n == m). +Proof NZtimes_cancel_r. -Theorem lt_lt_plus_r : forall n m p : N, n < m -> n < m + p. -Proof. -intros n m p H; rewrite <- (plus_0_r n). -apply plus_lt_le_mono; [assumption | apply le_0_l]. -Qed. +Theorem times_le_mono_pos_l : forall n m p : N, 0 < p -> (n <= m <-> p * n <= p * m). +Proof NZtimes_le_mono_pos_l. -Theorem lt_lt_plus_l : forall n m p : N, n < m -> n < p + m. -Proof. -intros n m p; rewrite plus_comm; apply lt_lt_plus_r. -Qed. +Theorem times_le_mono_pos_r : forall n m p : N, 0 < p -> (n <= m <-> n * p <= m * p). +Proof NZtimes_le_mono_pos_r. -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 times_pos_pos : forall n m : N, 0 < n -> 0 < m -> 0 < n * m. +Proof NZtimes_pos_pos. -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. +Theorem lt_1_times_pos : forall n m : N, 1 < n -> 0 < m -> 1 < n * m. +Proof NZlt_1_times_pos. -(* The following property is used to prove the correctness of the -definition of order on integers constructed from pairs of natural numbers *) +Theorem eq_times_0 : forall n m : N, n * m == 0 <-> n == 0 \/ m == 0. +Proof NZeq_times_0. -Theorem plus_lt_repl_pair : forall n m n' m' u v : N, - n + u < m + v -> n + m' == n' + m -> n' + u < m' + v. -Proof. -intros n m n' m' u v H1 H2. -symmetry in H2. assert (H3 : n' + m <= n + m') by now le_equal. -pose proof (plus_lt_le_mono _ _ _ _ H1 H3) as H4. -rewrite (plus_shuffle2 n u), (plus_shuffle1 m v), (plus_comm m n) in H4. -do 2 rewrite <- plus_assoc in H4. do 2 apply <- plus_lt_mono_l in H4. -now rewrite (plus_comm n' u), (plus_comm m' v). -Qed. +Theorem neq_times_0 : forall n m : N, n ~= 0 /\ m ~= 0 <-> n * m ~= 0. +Proof NZneq_times_0. -(** Multiplication and order *) +Theorem eq_times_0_l : forall n m : N, n * m == 0 -> m ~= 0 -> n == 0. +Proof NZeq_times_0_l. -Theorem times_lt_pred : - forall p q n m : N, S p == q -> (p * n < p * m <-> q * n + m < q * m + n). -Proof NZtimes_lt_pred. +Theorem eq_times_0_r : forall n m : N, n * m == 0 -> n ~= 0 -> m == 0. +Proof NZeq_times_0_r. -Theorem times_lt_mono_pos_l : forall p n m : N, 0 < p -> (n < m <-> p * n < p * m). -Proof NZtimes_lt_mono_pos_l. +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_lt_mono_pos_r : forall p n m : N, 0 < p -> (n < m <-> n * p < m * p). -Proof NZtimes_lt_mono_pos_r. +(** Theorems that are either not valid on Z or have different proofs on N and Z *) Theorem times_le_mono_l : forall n m p : N, n <= m -> p * n <= p * m. Proof. @@ -133,18 +71,6 @@ Proof. intros; apply NZtimes_le_mono_nonneg_r. apply le_0_l. assumption. Qed. -Theorem times_cancel_l : forall n m p : N, p ~= 0 -> (p * n == p * m <-> n == m). -Proof NZtimes_cancel_l. - -Theorem times_cancel_r : forall n m p : N, p ~= 0 -> (n * p == m * p <-> n == m). -Proof NZtimes_cancel_r. - -Theorem times_le_mono_pos_l : forall n m p : N, 0 < p -> (n <= m <-> p * n <= p * m). -Proof NZtimes_le_mono_pos_l. - -Theorem times_le_mono_pos_r : forall n m p : N, 0 < p -> (n <= m <-> n * p <= m * p). -Proof NZtimes_le_mono_pos_r. - 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. @@ -155,18 +81,6 @@ Proof. intros; apply NZtimes_le_mono; try assumption; apply le_0_l. Qed. -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. -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]]. @@ -174,5 +88,19 @@ apply -> NZtimes_pos in H. destruct H as [[H1 H2] | [H1 H2]]. now split. false_h now apply NZtimes_pos_pos. Qed. +Theorem eq_times_1 : forall n m : N, n * m == 1 <-> n == 1 /\ m == 1. +Proof. +intros n m. +split; [| intros [H1 H2]; now rewrite H1, H2, times_1_l]. +intro H; destruct (NZlt_trichotomy n 1) as [H1 | [H1 | H1]]. +apply -> lt_1_r in H1. rewrite H1, times_0_l in H. false_hyp H neq_0_succ. +rewrite H1, times_1_l in H; now split. +destruct (eq_0_gt_0_cases m) as [H2 | H2]. +rewrite H2, times_0_r in H; false_hyp H neq_0_succ. +apply -> (times_lt_mono_pos_r m) in H1; [| assumption]. rewrite times_1_l in H1. +assert (H3 : 1 < n * m) by now apply (lt_1_l 0 m). +rewrite H in H3; false_hyp H3 lt_irrefl. +Qed. + End NTimesOrderPropFunct. diff --git a/theories/Numbers/Natural/Binary/NBinDefs.v b/theories/Numbers/Natural/Binary/NBinDefs.v index 9a5ff0e4ba..66402f7614 100644 --- a/theories/Numbers/Natural/Binary/NBinDefs.v +++ b/theories/Numbers/Natural/Binary/NBinDefs.v @@ -247,16 +247,15 @@ simpl. rewrite Pminus_mask_succ_r, Pminus_mask_carry_spec. now destruct (Pminus_mask p q) as [| r |]; [| destruct r |]. Qed. -Theorem NZtimes_0_r : forall n : NZ, n * N0 = N0. +Theorem NZtimes_0_l : forall n : NZ, N0 * n = N0. Proof. destruct n; reflexivity. Qed. -Theorem NZtimes_succ_r : forall n m : NZ, n * (NZsucc m) = n * m + n. +Theorem NZtimes_succ_l : forall n m : NZ, (NZsucc n) * m = n * m + m. Proof. destruct n as [| n]; destruct m as [| m]; simpl; try reflexivity. -now rewrite Pmult_1_r. -now rewrite (Pmult_comm n (Psucc m)), Pmult_Sn_m, (Pplus_comm n), Pmult_comm. +now rewrite Pmult_Sn_m, Pplus_comm. Qed. End NZAxiomsMod. @@ -286,7 +285,7 @@ Proof. congruence. Qed. -Theorem NZle_lt_or_eq : forall n m : N, n <= m <-> n < m \/ n = m. +Theorem NZlt_eq_cases : forall n m : N, n <= m <-> n < m \/ n = m. Proof. intros n m. unfold le, lt. rewrite <- Ncompare_eq_correct. destruct (n ?= m); split; intro H1; (try discriminate); try (now left); try now right. @@ -298,7 +297,7 @@ Proof. intro n; unfold lt; now rewrite Ncompare_diag. Qed. -Theorem NZlt_succ_le : forall n m : NZ, n < (NZsucc m) <-> n <= m. +Theorem NZlt_succ_r : forall n m : NZ, n < (NZsucc m) <-> n <= m. Proof. intros n m; unfold lt, le; destruct n as [| p]; destruct m as [| q]; simpl; split; intro H; try reflexivity; try discriminate. diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v index 14899ed1dc..26a6053eb1 100644 --- a/theories/Numbers/Natural/Peano/NPeano.v +++ b/theories/Numbers/Natural/Peano/NPeano.v @@ -98,14 +98,14 @@ Proof. intros n m; induction n m using nat_double_ind; simpl; auto. apply NZminus_0_r. Qed. -Theorem NZtimes_0_r : forall n : nat, n * 0 = 0. +Theorem NZtimes_0_l : forall n : nat, 0 * n = 0. Proof. -exact mult_0_r. +reflexivity. Qed. -Theorem NZtimes_succ_r : forall n m : nat, n * (S m) = n * m + n. +Theorem NZtimes_succ_l : forall n m : nat, S n * m = n * m + m. Proof. -intros n m; symmetry; apply mult_n_Sm. +intros n m; now rewrite plus_comm. Qed. End NZAxiomsMod. @@ -135,7 +135,7 @@ Proof. congruence. Qed. -Theorem NZle_lt_or_eq : forall n m : nat, n <= m <-> n < m \/ n = m. +Theorem NZlt_eq_cases : forall n m : nat, n <= m <-> n < m \/ n = m. Proof. intros n m; split. apply le_lt_or_eq. @@ -148,7 +148,7 @@ Proof. exact lt_irrefl. Qed. -Theorem NZlt_succ_le : forall n m : nat, n < S m <-> n <= m. +Theorem NZlt_succ_r : forall n m : nat, n < S m <-> n <= m. Proof. intros n m; split; [apply lt_n_Sm_le | apply le_lt_n_Sm]. Qed. |