diff options
Diffstat (limited to 'theories/Numbers/Integer')
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZAdd.v | 345 | ||||
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZAddOrder.v | 373 | ||||
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZAxioms.v | 65 | ||||
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZBase.v | 86 | ||||
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZDomain.v | 69 | ||||
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZLt.v | 432 | ||||
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZMul.v | 115 | ||||
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZMulOrder.v | 343 | ||||
| -rw-r--r-- | theories/Numbers/Integer/BigZ/BigZ.v | 109 | ||||
| -rw-r--r-- | theories/Numbers/Integer/BigZ/ZMake.v | 491 | ||||
| -rw-r--r-- | theories/Numbers/Integer/Binary/ZBinary.v | 249 | ||||
| -rw-r--r-- | theories/Numbers/Integer/NatPairs/ZNatPairs.v | 422 | ||||
| -rw-r--r-- | theories/Numbers/Integer/SpecViaZ/ZSig.v | 117 | ||||
| -rw-r--r-- | theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v | 306 |
14 files changed, 3522 insertions, 0 deletions
diff --git a/theories/Numbers/Integer/Abstract/ZAdd.v b/theories/Numbers/Integer/Abstract/ZAdd.v new file mode 100644 index 00000000..df941d90 --- /dev/null +++ b/theories/Numbers/Integer/Abstract/ZAdd.v @@ -0,0 +1,345 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +(* Evgeny Makarov, INRIA, 2007 *) +(************************************************************************) + +(*i $Id: ZAdd.v 11040 2008-06-03 00:04:16Z letouzey $ i*) + +Require Export ZBase. + +Module ZAddPropFunct (Import ZAxiomsMod : ZAxiomsSig). +Module Export ZBasePropMod := ZBasePropFunct ZAxiomsMod. +Open Local Scope IntScope. + +Theorem Zadd_wd : + forall n1 n2 : Z, n1 == n2 -> forall m1 m2 : Z, m1 == m2 -> n1 + m1 == n2 + m2. +Proof NZadd_wd. + +Theorem Zadd_0_l : forall n : Z, 0 + n == n. +Proof NZadd_0_l. + +Theorem Zadd_succ_l : forall n m : Z, (S n) + m == S (n + m). +Proof NZadd_succ_l. + +Theorem Zsub_0_r : forall n : Z, n - 0 == n. +Proof NZsub_0_r. + +Theorem Zsub_succ_r : forall n m : Z, n - (S m) == P (n - m). +Proof NZsub_succ_r. + +Theorem Zopp_0 : - 0 == 0. +Proof Zopp_0. + +Theorem Zopp_succ : forall n : Z, - (S n) == P (- n). +Proof Zopp_succ. + +(* Theorems that are valid for both natural numbers and integers *) + +Theorem Zadd_0_r : forall n : Z, n + 0 == n. +Proof NZadd_0_r. + +Theorem Zadd_succ_r : forall n m : Z, n + S m == S (n + m). +Proof NZadd_succ_r. + +Theorem Zadd_comm : forall n m : Z, n + m == m + n. +Proof NZadd_comm. + +Theorem Zadd_assoc : forall n m p : Z, n + (m + p) == (n + m) + p. +Proof NZadd_assoc. + +Theorem Zadd_shuffle1 : forall n m p q : Z, (n + m) + (p + q) == (n + p) + (m + q). +Proof NZadd_shuffle1. + +Theorem Zadd_shuffle2 : forall n m p q : Z, (n + m) + (p + q) == (n + q) + (m + p). +Proof NZadd_shuffle2. + +Theorem Zadd_1_l : forall n : Z, 1 + n == S n. +Proof NZadd_1_l. + +Theorem Zadd_1_r : forall n : Z, n + 1 == S n. +Proof NZadd_1_r. + +Theorem Zadd_cancel_l : forall n m p : Z, p + n == p + m <-> n == m. +Proof NZadd_cancel_l. + +Theorem Zadd_cancel_r : forall n m p : Z, n + p == m + p <-> n == m. +Proof NZadd_cancel_r. + +(* Theorems that are either not valid on N or have different proofs on N and Z *) + +Theorem Zadd_pred_l : forall n m : Z, P n + m == P (n + m). +Proof. +intros n m. +rewrite <- (Zsucc_pred n) at 2. +rewrite Zadd_succ_l. now rewrite Zpred_succ. +Qed. + +Theorem Zadd_pred_r : forall n m : Z, n + P m == P (n + m). +Proof. +intros n m; rewrite (Zadd_comm n (P m)), (Zadd_comm n m); +apply Zadd_pred_l. +Qed. + +Theorem Zadd_opp_r : forall n m : Z, n + (- m) == n - m. +Proof. +NZinduct m. +rewrite Zopp_0; rewrite Zsub_0_r; now rewrite Zadd_0_r. +intro m. rewrite Zopp_succ, Zsub_succ_r, Zadd_pred_r; now rewrite Zpred_inj_wd. +Qed. + +Theorem Zsub_0_l : forall n : Z, 0 - n == - n. +Proof. +intro n; rewrite <- Zadd_opp_r; now rewrite Zadd_0_l. +Qed. + +Theorem Zsub_succ_l : forall n m : Z, S n - m == S (n - m). +Proof. +intros n m; do 2 rewrite <- Zadd_opp_r; now rewrite Zadd_succ_l. +Qed. + +Theorem Zsub_pred_l : forall n m : Z, P n - m == P (n - m). +Proof. +intros n m. rewrite <- (Zsucc_pred n) at 2. +rewrite Zsub_succ_l; now rewrite Zpred_succ. +Qed. + +Theorem Zsub_pred_r : forall n m : Z, n - (P m) == S (n - m). +Proof. +intros n m. rewrite <- (Zsucc_pred m) at 2. +rewrite Zsub_succ_r; now rewrite Zsucc_pred. +Qed. + +Theorem Zopp_pred : forall n : Z, - (P n) == S (- n). +Proof. +intro n. rewrite <- (Zsucc_pred n) at 2. +rewrite Zopp_succ. now rewrite Zsucc_pred. +Qed. + +Theorem Zsub_diag : forall n : Z, n - n == 0. +Proof. +NZinduct n. +now rewrite Zsub_0_r. +intro n. rewrite Zsub_succ_r, Zsub_succ_l; now rewrite Zpred_succ. +Qed. + +Theorem Zadd_opp_diag_l : forall n : Z, - n + n == 0. +Proof. +intro n; now rewrite Zadd_comm, Zadd_opp_r, Zsub_diag. +Qed. + +Theorem Zadd_opp_diag_r : forall n : Z, n + (- n) == 0. +Proof. +intro n; rewrite Zadd_comm; apply Zadd_opp_diag_l. +Qed. + +Theorem Zadd_opp_l : forall n m : Z, - m + n == n - m. +Proof. +intros n m; rewrite <- Zadd_opp_r; now rewrite Zadd_comm. +Qed. + +Theorem Zadd_sub_assoc : forall n m p : Z, n + (m - p) == (n + m) - p. +Proof. +intros n m p; do 2 rewrite <- Zadd_opp_r; now rewrite Zadd_assoc. +Qed. + +Theorem Zopp_involutive : forall n : Z, - (- n) == n. +Proof. +NZinduct n. +now do 2 rewrite Zopp_0. +intro n. rewrite Zopp_succ, Zopp_pred; now rewrite Zsucc_inj_wd. +Qed. + +Theorem Zopp_add_distr : forall n m : Z, - (n + m) == - n + (- m). +Proof. +intros n m; NZinduct n. +rewrite Zopp_0; now do 2 rewrite Zadd_0_l. +intro n. rewrite Zadd_succ_l; do 2 rewrite Zopp_succ; rewrite Zadd_pred_l. +now rewrite Zpred_inj_wd. +Qed. + +Theorem Zopp_sub_distr : forall n m : Z, - (n - m) == - n + m. +Proof. +intros n m; rewrite <- Zadd_opp_r, Zopp_add_distr. +now rewrite Zopp_involutive. +Qed. + +Theorem Zopp_inj : forall n m : Z, - n == - m -> n == m. +Proof. +intros n m H. apply Zopp_wd in H. now do 2 rewrite Zopp_involutive in H. +Qed. + +Theorem Zopp_inj_wd : forall n m : Z, - n == - m <-> n == m. +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 Zsub_add_distr : forall n m p : Z, n - (m + p) == (n - m) - p. +Proof. +intros n m p; rewrite <- Zadd_opp_r, Zopp_add_distr, Zadd_assoc. +now do 2 rewrite Zadd_opp_r. +Qed. + +Theorem Zsub_sub_distr : forall n m p : Z, n - (m - p) == (n - m) + p. +Proof. +intros n m p; rewrite <- Zadd_opp_r, Zopp_sub_distr, Zadd_assoc. +now rewrite Zadd_opp_r. +Qed. + +Theorem sub_opp_l : forall n m : Z, - n - m == - m - n. +Proof. +intros n m. do 2 rewrite <- Zadd_opp_r. now rewrite Zadd_comm. +Qed. + +Theorem Zsub_opp_r : forall n m : Z, n - (- m) == n + m. +Proof. +intros n m; rewrite <- Zadd_opp_r; now rewrite Zopp_involutive. +Qed. + +Theorem Zadd_sub_swap : forall n m p : Z, n + m - p == n - p + m. +Proof. +intros n m p. rewrite <- Zadd_sub_assoc, <- (Zadd_opp_r n p), <- Zadd_assoc. +now rewrite Zadd_opp_l. +Qed. + +Theorem Zsub_cancel_l : forall n m p : Z, n - m == n - p <-> m == p. +Proof. +intros n m p. rewrite <- (Zadd_cancel_l (n - m) (n - p) (- n)). +do 2 rewrite Zadd_sub_assoc. rewrite Zadd_opp_diag_l; do 2 rewrite Zsub_0_l. +apply Zopp_inj_wd. +Qed. + +Theorem Zsub_cancel_r : forall n m p : Z, n - p == m - p <-> n == m. +Proof. +intros n m p. +stepl (n - p + p == m - p + p) by apply Zadd_cancel_r. +now do 2 rewrite <- Zsub_sub_distr, Zsub_diag, Zsub_0_r. +Qed. + +(* 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 (add or sub) and the indication whether the left or right term +is moved. *) + +Theorem Zadd_move_l : forall n m p : Z, n + m == p <-> m == p - n. +Proof. +intros n m p. +stepl (n + m - n == p - n) by apply Zsub_cancel_r. +now rewrite Zadd_comm, <- Zadd_sub_assoc, Zsub_diag, Zadd_0_r. +Qed. + +Theorem Zadd_move_r : forall n m p : Z, n + m == p <-> n == p - m. +Proof. +intros n m p; rewrite Zadd_comm; now apply Zadd_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 Zsub_move_l : forall n m p : Z, n - m == p <-> - m == p - n. +Proof. +intros n m p; rewrite <- (Zadd_opp_r n m); apply Zadd_move_l. +Qed. + +Theorem Zsub_move_r : forall n m p : Z, n - m == p <-> n == p + m. +Proof. +intros n m p; rewrite <- (Zadd_opp_r n m). now rewrite Zadd_move_r, Zsub_opp_r. +Qed. + +Theorem Zadd_move_0_l : forall n m : Z, n + m == 0 <-> m == - n. +Proof. +intros n m; now rewrite Zadd_move_l, Zsub_0_l. +Qed. + +Theorem Zadd_move_0_r : forall n m : Z, n + m == 0 <-> n == - m. +Proof. +intros n m; now rewrite Zadd_move_r, Zsub_0_l. +Qed. + +Theorem Zsub_move_0_l : forall n m : Z, n - m == 0 <-> - m == - n. +Proof. +intros n m. now rewrite Zsub_move_l, Zsub_0_l. +Qed. + +Theorem Zsub_move_0_r : forall n m : Z, n - m == 0 <-> n == m. +Proof. +intros n m. now rewrite Zsub_move_r, Zadd_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 Zadd_simpl_l : forall n m : Z, n + m - n == m. +Proof. +intros; now rewrite Zadd_sub_swap, Zsub_diag, Zadd_0_l. +Qed. + +Theorem Zadd_simpl_r : forall n m : Z, n + m - m == n. +Proof. +intros; now rewrite <- Zadd_sub_assoc, Zsub_diag, Zadd_0_r. +Qed. + +Theorem Zsub_simpl_l : forall n m : Z, - n - m + n == - m. +Proof. +intros; now rewrite <- Zadd_sub_swap, Zadd_opp_diag_l, Zsub_0_l. +Qed. + +Theorem Zsub_simpl_r : forall n m : Z, n - m + m == n. +Proof. +intros; now rewrite <- Zsub_sub_distr, Zsub_diag, Zsub_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 Zadd_add_simpl_l_l : forall n m p : Z, (n + m) - (n + p) == m - p. +Proof. +intros n m p. now rewrite (Zadd_comm n m), <- Zadd_sub_assoc, +Zsub_add_distr, Zsub_diag, Zsub_0_l, Zadd_opp_r. +Qed. + +Theorem Zadd_add_simpl_l_r : forall n m p : Z, (n + m) - (p + n) == m - p. +Proof. +intros n m p. rewrite (Zadd_comm p n); apply Zadd_add_simpl_l_l. +Qed. + +Theorem Zadd_add_simpl_r_l : forall n m p : Z, (n + m) - (m + p) == n - p. +Proof. +intros n m p. rewrite (Zadd_comm n m); apply Zadd_add_simpl_l_l. +Qed. + +Theorem Zadd_add_simpl_r_r : forall n m p : Z, (n + m) - (p + m) == n - p. +Proof. +intros n m p. rewrite (Zadd_comm p m); apply Zadd_add_simpl_r_l. +Qed. + +Theorem Zsub_add_simpl_r_l : forall n m p : Z, (n - m) + (m + p) == n + p. +Proof. +intros n m p. now rewrite <- Zsub_sub_distr, Zsub_add_distr, Zsub_diag, +Zsub_0_l, Zsub_opp_r. +Qed. + +Theorem Zsub_add_simpl_r_r : forall n m p : Z, (n - m) + (p + m) == n + p. +Proof. +intros n m p. rewrite (Zadd_comm p m); apply Zsub_add_simpl_r_l. +Qed. + +(* Of course, there are many other variants *) + +End ZAddPropFunct. + diff --git a/theories/Numbers/Integer/Abstract/ZAddOrder.v b/theories/Numbers/Integer/Abstract/ZAddOrder.v new file mode 100644 index 00000000..101ea634 --- /dev/null +++ b/theories/Numbers/Integer/Abstract/ZAddOrder.v @@ -0,0 +1,373 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +(* Evgeny Makarov, INRIA, 2007 *) +(************************************************************************) + +(*i $Id: ZAddOrder.v 11040 2008-06-03 00:04:16Z letouzey $ i*) + +Require Export ZLt. + +Module ZAddOrderPropFunct (Import ZAxiomsMod : ZAxiomsSig). +Module Export ZOrderPropMod := ZOrderPropFunct ZAxiomsMod. +Open Local Scope IntScope. + +(* Theorems that are true on both natural numbers and integers *) + +Theorem Zadd_lt_mono_l : forall n m p : Z, n < m <-> p + n < p + m. +Proof NZadd_lt_mono_l. + +Theorem Zadd_lt_mono_r : forall n m p : Z, n < m <-> n + p < m + p. +Proof NZadd_lt_mono_r. + +Theorem Zadd_lt_mono : forall n m p q : Z, n < m -> p < q -> n + p < m + q. +Proof NZadd_lt_mono. + +Theorem Zadd_le_mono_l : forall n m p : Z, n <= m <-> p + n <= p + m. +Proof NZadd_le_mono_l. + +Theorem Zadd_le_mono_r : forall n m p : Z, n <= m <-> n + p <= m + p. +Proof NZadd_le_mono_r. + +Theorem Zadd_le_mono : forall n m p q : Z, n <= m -> p <= q -> n + p <= m + q. +Proof NZadd_le_mono. + +Theorem Zadd_lt_le_mono : forall n m p q : Z, n < m -> p <= q -> n + p < m + q. +Proof NZadd_lt_le_mono. + +Theorem Zadd_le_lt_mono : forall n m p q : Z, n <= m -> p < q -> n + p < m + q. +Proof NZadd_le_lt_mono. + +Theorem Zadd_pos_pos : forall n m : Z, 0 < n -> 0 < m -> 0 < n + m. +Proof NZadd_pos_pos. + +Theorem Zadd_pos_nonneg : forall n m : Z, 0 < n -> 0 <= m -> 0 < n + m. +Proof NZadd_pos_nonneg. + +Theorem Zadd_nonneg_pos : forall n m : Z, 0 <= n -> 0 < m -> 0 < n + m. +Proof NZadd_nonneg_pos. + +Theorem Zadd_nonneg_nonneg : forall n m : Z, 0 <= n -> 0 <= m -> 0 <= n + m. +Proof NZadd_nonneg_nonneg. + +Theorem Zlt_add_pos_l : forall n m : Z, 0 < n -> m < n + m. +Proof NZlt_add_pos_l. + +Theorem Zlt_add_pos_r : forall n m : Z, 0 < n -> m < m + n. +Proof NZlt_add_pos_r. + +Theorem Zle_lt_add_lt : forall n m p q : Z, n <= m -> p + m < q + n -> p < q. +Proof NZle_lt_add_lt. + +Theorem Zlt_le_add_lt : forall n m p q : Z, n < m -> p + m <= q + n -> p < q. +Proof NZlt_le_add_lt. + +Theorem Zle_le_add_le : forall n m p q : Z, n <= m -> p + m <= q + n -> p <= q. +Proof NZle_le_add_le. + +Theorem Zadd_lt_cases : forall n m p q : Z, n + m < p + q -> n < p \/ m < q. +Proof NZadd_lt_cases. + +Theorem Zadd_le_cases : forall n m p q : Z, n + m <= p + q -> n <= p \/ m <= q. +Proof NZadd_le_cases. + +Theorem Zadd_neg_cases : forall n m : Z, n + m < 0 -> n < 0 \/ m < 0. +Proof NZadd_neg_cases. + +Theorem Zadd_pos_cases : forall n m : Z, 0 < n + m -> 0 < n \/ 0 < m. +Proof NZadd_pos_cases. + +Theorem Zadd_nonpos_cases : forall n m : Z, n + m <= 0 -> n <= 0 \/ m <= 0. +Proof NZadd_nonpos_cases. + +Theorem Zadd_nonneg_cases : forall n m : Z, 0 <= n + m -> 0 <= n \/ 0 <= m. +Proof NZadd_nonneg_cases. + +(* Theorems that are either not valid on N or have different proofs on N and Z *) + +Theorem Zadd_neg_neg : forall n m : Z, n < 0 -> m < 0 -> n + m < 0. +Proof. +intros n m H1 H2. rewrite <- (Zadd_0_l 0). now apply Zadd_lt_mono. +Qed. + +Theorem Zadd_neg_nonpos : forall n m : Z, n < 0 -> m <= 0 -> n + m < 0. +Proof. +intros n m H1 H2. rewrite <- (Zadd_0_l 0). now apply Zadd_lt_le_mono. +Qed. + +Theorem Zadd_nonpos_neg : forall n m : Z, n <= 0 -> m < 0 -> n + m < 0. +Proof. +intros n m H1 H2. rewrite <- (Zadd_0_l 0). now apply Zadd_le_lt_mono. +Qed. + +Theorem Zadd_nonpos_nonpos : forall n m : Z, n <= 0 -> m <= 0 -> n + m <= 0. +Proof. +intros n m H1 H2. rewrite <- (Zadd_0_l 0). now apply Zadd_le_mono. +Qed. + +(** Sub and order *) + +Theorem Zlt_0_sub : forall n m : Z, 0 < m - n <-> n < m. +Proof. +intros n m. stepl (0 + n < m - n + n) by symmetry; apply Zadd_lt_mono_r. +rewrite Zadd_0_l; now rewrite Zsub_simpl_r. +Qed. + +Notation Zsub_pos := Zlt_0_sub (only parsing). + +Theorem Zle_0_sub : forall n m : Z, 0 <= m - n <-> n <= m. +Proof. +intros n m; stepl (0 + n <= m - n + n) by symmetry; apply Zadd_le_mono_r. +rewrite Zadd_0_l; now rewrite Zsub_simpl_r. +Qed. + +Notation Zsub_nonneg := Zle_0_sub (only parsing). + +Theorem Zlt_sub_0 : forall n m : Z, n - m < 0 <-> n < m. +Proof. +intros n m. stepl (n - m + m < 0 + m) by symmetry; apply Zadd_lt_mono_r. +rewrite Zadd_0_l; now rewrite Zsub_simpl_r. +Qed. + +Notation Zsub_neg := Zlt_sub_0 (only parsing). + +Theorem Zle_sub_0 : forall n m : Z, n - m <= 0 <-> n <= m. +Proof. +intros n m. stepl (n - m + m <= 0 + m) by symmetry; apply Zadd_le_mono_r. +rewrite Zadd_0_l; now rewrite Zsub_simpl_r. +Qed. + +Notation Zsub_nonpos := Zle_sub_0 (only parsing). + +Theorem Zopp_lt_mono : forall n m : Z, n < m <-> - m < - n. +Proof. +intros n m. stepr (m + - m < m + - n) by symmetry; apply Zadd_lt_mono_l. +do 2 rewrite Zadd_opp_r. rewrite Zsub_diag. symmetry; apply Zlt_0_sub. +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 Zadd_le_mono_l. +do 2 rewrite Zadd_opp_r. rewrite Zsub_diag. symmetry; apply Zle_0_sub. +Qed. + +Theorem Zopp_pos_neg : forall n : Z, 0 < - n <-> n < 0. +Proof. +intro n; rewrite (Zopp_lt_mono n 0); now rewrite Zopp_0. +Qed. + +Theorem Zopp_neg_pos : forall n : Z, - n < 0 <-> 0 < n. +Proof. +intro n. rewrite (Zopp_lt_mono 0 n). now rewrite Zopp_0. +Qed. + +Theorem Zopp_nonneg_nonpos : forall n : Z, 0 <= - n <-> n <= 0. +Proof. +intro n; rewrite (Zopp_le_mono n 0); now rewrite Zopp_0. +Qed. + +Theorem Zopp_nonpos_nonneg : forall n : Z, - n <= 0 <-> 0 <= n. +Proof. +intro n. rewrite (Zopp_le_mono 0 n). now rewrite Zopp_0. +Qed. + +Theorem Zsub_lt_mono_l : forall n m p : Z, n < m <-> p - m < p - n. +Proof. +intros n m p. do 2 rewrite <- Zadd_opp_r. rewrite <- Zadd_lt_mono_l. +apply Zopp_lt_mono. +Qed. + +Theorem Zsub_lt_mono_r : forall n m p : Z, n < m <-> n - p < m - p. +Proof. +intros n m p; do 2 rewrite <- Zadd_opp_r; apply Zadd_lt_mono_r. +Qed. + +Theorem Zsub_lt_mono : forall n m p q : Z, n < m -> q < p -> n - p < m - q. +Proof. +intros n m p q H1 H2. +apply NZlt_trans with (m - p); +[now apply -> Zsub_lt_mono_r | now apply -> Zsub_lt_mono_l]. +Qed. + +Theorem Zsub_le_mono_l : forall n m p : Z, n <= m <-> p - m <= p - n. +Proof. +intros n m p; do 2 rewrite <- Zadd_opp_r; rewrite <- Zadd_le_mono_l; +apply Zopp_le_mono. +Qed. + +Theorem Zsub_le_mono_r : forall n m p : Z, n <= m <-> n - p <= m - p. +Proof. +intros n m p; do 2 rewrite <- Zadd_opp_r; apply Zadd_le_mono_r. +Qed. + +Theorem Zsub_le_mono : forall n m p q : Z, n <= m -> q <= p -> n - p <= m - q. +Proof. +intros n m p q H1 H2. +apply NZle_trans with (m - p); +[now apply -> Zsub_le_mono_r | now apply -> Zsub_le_mono_l]. +Qed. + +Theorem Zsub_lt_le_mono : forall n m p q : Z, n < m -> q <= p -> n - p < m - q. +Proof. +intros n m p q H1 H2. +apply NZlt_le_trans with (m - p); +[now apply -> Zsub_lt_mono_r | now apply -> Zsub_le_mono_l]. +Qed. + +Theorem Zsub_le_lt_mono : forall n m p q : Z, n <= m -> q < p -> n - p < m - q. +Proof. +intros n m p q H1 H2. +apply NZle_lt_trans with (m - p); +[now apply -> Zsub_le_mono_r | now apply -> Zsub_lt_mono_l]. +Qed. + +Theorem Zle_lt_sub_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_add_lt (- m) (- n)); +[now apply -> Zopp_le_mono | now do 2 rewrite Zadd_opp_r]. +Qed. + +Theorem Zlt_le_sub_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_add_lt (- m) (- n)); +[now apply -> Zopp_lt_mono | now do 2 rewrite Zadd_opp_r]. +Qed. + +Theorem Zle_le_sub_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_add_le (- m) (- n)); +[now apply -> Zopp_le_mono | now do 2 rewrite Zadd_opp_r]. +Qed. + +Theorem Zlt_add_lt_sub_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 Zsub_lt_mono_r. +now rewrite Zadd_simpl_r. +Qed. + +Theorem Zle_add_le_sub_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 Zsub_le_mono_r. +now rewrite Zadd_simpl_r. +Qed. + +Theorem Zlt_add_lt_sub_l : forall n m p : Z, n + p < m <-> p < m - n. +Proof. +intros n m p. rewrite Zadd_comm; apply Zlt_add_lt_sub_r. +Qed. + +Theorem Zle_add_le_sub_l : forall n m p : Z, n + p <= m <-> p <= m - n. +Proof. +intros n m p. rewrite Zadd_comm; apply Zle_add_le_sub_r. +Qed. + +Theorem Zlt_sub_lt_add_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 Zadd_lt_mono_r. +now rewrite Zsub_simpl_r. +Qed. + +Theorem Zle_sub_le_add_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 Zadd_le_mono_r. +now rewrite Zsub_simpl_r. +Qed. + +Theorem Zlt_sub_lt_add_l : forall n m p : Z, n - m < p <-> n < m + p. +Proof. +intros n m p. rewrite Zadd_comm; apply Zlt_sub_lt_add_r. +Qed. + +Theorem Zle_sub_le_add_l : forall n m p : Z, n - m <= p <-> n <= m + p. +Proof. +intros n m p. rewrite Zadd_comm; apply Zle_sub_le_add_r. +Qed. + +Theorem Zlt_sub_lt_add : forall n m p q : Z, n - m < p - q <-> n + q < m + p. +Proof. +intros n m p q. rewrite Zlt_sub_lt_add_l. rewrite Zadd_sub_assoc. +now rewrite <- Zlt_add_lt_sub_r. +Qed. + +Theorem Zle_sub_le_add : forall n m p q : Z, n - m <= p - q <-> n + q <= m + p. +Proof. +intros n m p q. rewrite Zle_sub_le_add_l. rewrite Zadd_sub_assoc. +now rewrite <- Zle_add_le_sub_r. +Qed. + +Theorem Zlt_sub_pos : forall n m : Z, 0 < m <-> n - m < n. +Proof. +intros n m. stepr (n - m < n - 0) by now rewrite Zsub_0_r. apply Zsub_lt_mono_l. +Qed. + +Theorem Zle_sub_nonneg : forall n m : Z, 0 <= m <-> n - m <= n. +Proof. +intros n m. stepr (n - m <= n - 0) by now rewrite Zsub_0_r. apply Zsub_le_mono_l. +Qed. + +Theorem Zsub_lt_cases : forall n m p q : Z, n - m < p - q -> n < m \/ q < p. +Proof. +intros n m p q H. rewrite Zlt_sub_lt_add in H. now apply Zadd_lt_cases. +Qed. + +Theorem Zsub_le_cases : forall n m p q : Z, n - m <= p - q -> n <= m \/ q <= p. +Proof. +intros n m p q H. rewrite Zle_sub_le_add in H. now apply Zadd_le_cases. +Qed. + +Theorem Zsub_neg_cases : forall n m : Z, n - m < 0 -> n < 0 \/ 0 < m. +Proof. +intros n m H; rewrite <- Zadd_opp_r in H. +setoid_replace (0 < m) with (- m < 0) using relation iff by (symmetry; apply Zopp_neg_pos). +now apply Zadd_neg_cases. +Qed. + +Theorem Zsub_pos_cases : forall n m : Z, 0 < n - m -> 0 < n \/ m < 0. +Proof. +intros n m H; rewrite <- Zadd_opp_r in H. +setoid_replace (m < 0) with (0 < - m) using relation iff by (symmetry; apply Zopp_pos_neg). +now apply Zadd_pos_cases. +Qed. + +Theorem Zsub_nonpos_cases : forall n m : Z, n - m <= 0 -> n <= 0 \/ 0 <= m. +Proof. +intros n m H; rewrite <- Zadd_opp_r in H. +setoid_replace (0 <= m) with (- m <= 0) using relation iff by (symmetry; apply Zopp_nonpos_nonneg). +now apply Zadd_nonpos_cases. +Qed. + +Theorem Zsub_nonneg_cases : forall n m : Z, 0 <= n - m -> 0 <= n \/ m <= 0. +Proof. +intros n m H; rewrite <- Zadd_opp_r in H. +setoid_replace (m <= 0) with (0 <= - m) using relation iff by (symmetry; apply Zopp_nonneg_nonpos). +now apply Zadd_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 ZAddOrderPropFunct. + + diff --git a/theories/Numbers/Integer/Abstract/ZAxioms.v b/theories/Numbers/Integer/Abstract/ZAxioms.v new file mode 100644 index 00000000..c4a4b6b8 --- /dev/null +++ b/theories/Numbers/Integer/Abstract/ZAxioms.v @@ -0,0 +1,65 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +(* Evgeny Makarov, INRIA, 2007 *) +(************************************************************************) + +(*i $Id: ZAxioms.v 11040 2008-06-03 00:04:16Z letouzey $ i*) + +Require Export NZAxioms. + +Set Implicit Arguments. + +Module Type ZAxiomsSig. +Declare Module Export NZOrdAxiomsMod : NZOrdAxiomsSig. + +Delimit Scope IntScope with Int. +Notation Z := NZ. +Notation Zeq := NZeq. +Notation Z0 := NZ0. +Notation Z1 := (NZsucc NZ0). +Notation S := NZsucc. +Notation P := NZpred. +Notation Zadd := NZadd. +Notation Zmul := NZmul. +Notation Zsub := NZsub. +Notation Zlt := NZlt. +Notation Zle := NZle. +Notation Zmin := NZmin. +Notation Zmax := NZmax. +Notation "x == y" := (NZeq x y) (at level 70) : IntScope. +Notation "x ~= y" := (~ NZeq x y) (at level 70) : IntScope. +Notation "0" := NZ0 : IntScope. +Notation "1" := (NZsucc NZ0) : IntScope. +Notation "x + y" := (NZadd x y) : IntScope. +Notation "x - y" := (NZsub x y) : IntScope. +Notation "x * y" := (NZmul x y) : IntScope. +Notation "x < y" := (NZlt x y) : IntScope. +Notation "x <= y" := (NZle x y) : IntScope. +Notation "x > y" := (NZlt y x) (only parsing) : IntScope. +Notation "x >= y" := (NZle y x) (only parsing) : IntScope. + +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. + +(* Integers are obtained by postulating that every number has a predecessor *) +Axiom Zsucc_pred : forall n : Z, S (P n) == n. + +Axiom Zopp_0 : - 0 == 0. +Axiom Zopp_succ : forall n : Z, - (S n) == P (- n). + +End ZAxiomsSig. + diff --git a/theories/Numbers/Integer/Abstract/ZBase.v b/theories/Numbers/Integer/Abstract/ZBase.v new file mode 100644 index 00000000..29e18548 --- /dev/null +++ b/theories/Numbers/Integer/Abstract/ZBase.v @@ -0,0 +1,86 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +(* Evgeny Makarov, INRIA, 2007 *) +(************************************************************************) + +(*i $Id: ZBase.v 11040 2008-06-03 00:04:16Z letouzey $ i*) + +Require Export Decidable. +Require Export ZAxioms. +Require Import NZMulOrder. + +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 Zadd and later *) + +Open Local Scope IntScope. + +Module Export NZMulOrderMod := NZMulOrderPropFunct NZOrdAxiomsMod. + +Theorem Zsucc_wd : forall n1 n2 : Z, n1 == n2 -> S n1 == S n2. +Proof NZsucc_wd. + +Theorem Zpred_wd : forall n1 n2 : Z, n1 == n2 -> P n1 == P n2. +Proof NZpred_wd. + +Theorem Zpred_succ : forall n : Z, P (S n) == n. +Proof NZpred_succ. + +Theorem Zeq_refl : forall n : Z, n == n. +Proof (proj1 NZeq_equiv). + +Theorem Zeq_symm : forall n m : Z, n == m -> m == n. +Proof (proj2 (proj2 NZeq_equiv)). + +Theorem Zeq_trans : forall n m p : Z, n == m -> m == p -> n == p. +Proof (proj1 (proj2 NZeq_equiv)). + +Theorem Zneq_symm : forall n m : Z, n ~= m -> m ~= n. +Proof NZneq_symm. + +Theorem Zsucc_inj : forall n1 n2 : Z, S n1 == S n2 -> n1 == n2. +Proof NZsucc_inj. + +Theorem Zsucc_inj_wd : forall n1 n2 : Z, S n1 == S n2 <-> n1 == n2. +Proof NZsucc_inj_wd. + +Theorem Zsucc_inj_wd_neg : forall n m : Z, S n ~= S m <-> n ~= m. +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_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. + +Theorem Zcentral_induction : +forall A : Z -> Prop, predicate_wd Zeq A -> + forall z : Z, A z -> + (forall n : Z, A n <-> A (S n)) -> + forall n : Z, A n. +Proof NZcentral_induction. + +(* Theorems that are true for integers but not for natural numbers *) + +Theorem Zpred_inj : forall n m : Z, P n == P m -> n == m. +Proof. +intros n m H. apply NZsucc_wd in H. now do 2 rewrite Zsucc_pred in H. +Qed. + +Theorem Zpred_inj_wd : forall n1 n2 : Z, P n1 == P n2 <-> n1 == n2. +Proof. +intros n1 n2; split; [apply Zpred_inj | apply NZpred_wd]. +Qed. + +End ZBasePropFunct. + diff --git a/theories/Numbers/Integer/Abstract/ZDomain.v b/theories/Numbers/Integer/Abstract/ZDomain.v new file mode 100644 index 00000000..15beb2b9 --- /dev/null +++ b/theories/Numbers/Integer/Abstract/ZDomain.v @@ -0,0 +1,69 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +(* Evgeny Makarov, INRIA, 2007 *) +(************************************************************************) + +(*i $Id: ZDomain.v 10934 2008-05-15 21:58:20Z letouzey $ i*) + +Require Export NumPrelude. + +Module Type ZDomainSignature. + +Parameter Inline Z : Set. +Parameter Inline Zeq : Z -> Z -> Prop. +Parameter Inline e : Z -> Z -> bool. + +Axiom eq_equiv_e : forall x y : Z, Zeq x y <-> e x y. +Axiom eq_equiv : equiv Z Zeq. + +Add Relation Z Zeq + reflexivity proved by (proj1 eq_equiv) + symmetry proved by (proj2 (proj2 eq_equiv)) + transitivity proved by (proj1 (proj2 eq_equiv)) +as eq_rel. + +Delimit Scope IntScope with Int. +Bind Scope IntScope with Z. +Notation "x == y" := (Zeq x y) (at level 70) : IntScope. +Notation "x # y" := (~ Zeq x y) (at level 70) : IntScope. + +End ZDomainSignature. + +Module ZDomainProperties (Import ZDomainModule : ZDomainSignature). +Open Local Scope IntScope. + +Add Morphism e with signature Zeq ==> Zeq ==> eq_bool as e_wd. +Proof. +intros x x' Exx' y y' Eyy'. +case_eq (e x y); case_eq (e x' y'); intros H1 H2; trivial. +assert (x == y); [apply <- eq_equiv_e; now rewrite H2 | +assert (x' == y'); [rewrite <- Exx'; now rewrite <- Eyy' | +rewrite <- H1; assert (H3 : e x' y'); [now apply -> eq_equiv_e | now inversion H3]]]. +assert (x' == y'); [apply <- eq_equiv_e; now rewrite H1 | +assert (x == y); [rewrite Exx'; now rewrite Eyy' | +rewrite <- H2; assert (H3 : e x y); [now apply -> eq_equiv_e | now inversion H3]]]. +Qed. + +Theorem neq_symm : forall n m, n # m -> m # n. +Proof. +intros n m H1 H2; symmetry in H2; false_hyp H2 H1. +Qed. + +Theorem ZE_stepl : forall x y z : Z, x == y -> x == z -> z == y. +Proof. +intros x y z H1 H2; now rewrite <- H1. +Qed. + +Declare Left Step ZE_stepl. + +(* The right step lemma is just transitivity of Zeq *) +Declare Right Step (proj1 (proj2 eq_equiv)). + +End ZDomainProperties. + + diff --git a/theories/Numbers/Integer/Abstract/ZLt.v b/theories/Numbers/Integer/Abstract/ZLt.v new file mode 100644 index 00000000..2a88a535 --- /dev/null +++ b/theories/Numbers/Integer/Abstract/ZLt.v @@ -0,0 +1,432 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +(* Evgeny Makarov, INRIA, 2007 *) +(************************************************************************) + +(*i $Id: ZLt.v 11040 2008-06-03 00:04:16Z letouzey $ i*) + +Require Export ZMul. + +Module ZOrderPropFunct (Import ZAxiomsMod : ZAxiomsSig). +Module Export ZMulPropMod := ZMulPropFunct ZAxiomsMod. +Open Local Scope IntScope. + +(* Axioms *) + +Theorem Zlt_wd : + forall n1 n2 : Z, n1 == n2 -> forall m1 m2 : Z, m1 == m2 -> (n1 < m1 <-> n2 < m2). +Proof NZlt_wd. + +Theorem Zle_wd : + forall n1 n2 : Z, n1 == n2 -> forall m1 m2 : Z, m1 == m2 -> (n1 <= m1 <-> n2 <= m2). +Proof NZle_wd. + +Theorem Zmin_wd : + forall n1 n2 : Z, n1 == n2 -> forall m1 m2 : Z, m1 == m2 -> Zmin n1 m1 == Zmin n2 m2. +Proof NZmin_wd. + +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 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_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. + +Theorem Zmin_r : forall n m : Z, m <= n -> Zmin n m == m. +Proof NZmin_r. + +Theorem Zmax_l : forall n m : Z, m <= n -> Zmax n m == n. +Proof NZmax_l. + +Theorem Zmax_r : forall n m : Z, n <= m -> Zmax n m == m. +Proof NZmax_r. + +(* Renaming theorems from NZOrder.v *) + +Theorem Zlt_le_incl : forall n m : Z, n < m -> n <= m. +Proof NZlt_le_incl. + +Theorem Zlt_neq : forall n m : Z, n < m -> n ~= m. +Proof NZlt_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_diag_r : forall n : Z, n < S n. +Proof NZlt_succ_diag_r. + +Theorem Zle_succ_diag_r : forall n : Z, n <= S n. +Proof NZle_succ_diag_r. + +Theorem Zlt_0_1 : 0 < 1. +Proof NZlt_0_1. + +Theorem Zle_0_1 : 0 <= 1. +Proof NZle_0_1. + +Theorem Zlt_lt_succ_r : forall n m : Z, n < m -> n < S m. +Proof NZlt_lt_succ_r. + +Theorem Zle_le_succ_r : forall n m : Z, n <= m -> n <= S m. +Proof NZle_le_succ_r. + +Theorem Zle_succ_r : forall n m : Z, n <= S m <-> n <= m \/ n == S m. +Proof NZle_succ_r. + +Theorem Zneq_succ_diag_l : forall n : Z, S n ~= n. +Proof NZneq_succ_diag_l. + +Theorem Zneq_succ_diag_r : forall n : Z, n ~= S n. +Proof NZneq_succ_diag_r. + +Theorem Znlt_succ_diag_l : forall n : Z, ~ S n < n. +Proof NZnlt_succ_diag_l. + +Theorem Znle_succ_diag_l : forall n : Z, ~ S n <= n. +Proof NZnle_succ_diag_l. + +Theorem Zle_succ_l : forall n m : Z, S n <= m <-> n < m. +Proof NZle_succ_l. + +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. + +Theorem Zsucc_le_mono : forall n m : Z, n <= m <-> S n <= S m. +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. + +Theorem Zle_trans : forall n m p : Z, n <= m -> m <= p -> n <= p. +Proof NZle_trans. + +Theorem Zle_lt_trans : forall n m p : Z, n <= m -> m < p -> n < p. +Proof NZle_lt_trans. + +Theorem Zlt_le_trans : forall n m p : Z, n < m -> m <= p -> n < p. +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. + +Theorem Zle_gt_cases : forall n m : Z, n <= m \/ n > m. +Proof NZle_gt_cases. + +Theorem Zlt_ge_cases : forall n m : Z, n < m \/ n >= m. +Proof NZlt_ge_cases. + +Theorem Zle_ge_cases : forall n m : Z, n <= m \/ n >= m. +Proof NZle_ge_cases. + +(** Instances of the previous theorems for m == 0 *) + +Theorem Zneg_pos_cases : forall n : Z, n ~= 0 <-> n < 0 \/ n > 0. +Proof. +intro; apply Zlt_gt_cases. +Qed. + +Theorem Znonpos_pos_cases : forall n : Z, n <= 0 \/ n > 0. +Proof. +intro; apply Zle_gt_cases. +Qed. + +Theorem Zneg_nonneg_cases : forall n : Z, n < 0 \/ n >= 0. +Proof. +intro; apply Zlt_ge_cases. +Qed. + +Theorem Znonpos_nonneg_cases : forall n : Z, n <= 0 \/ n >= 0. +Proof. +intro; apply Zle_ge_cases. +Qed. + +Theorem Zle_ngt : forall n m : Z, n <= m <-> ~ n > m. +Proof NZle_ngt. + +Theorem Znlt_ge : forall n m : Z, ~ n < m <-> n >= m. +Proof NZnlt_ge. + +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. + +Theorem Znle_gt : forall n m : Z, ~ n <= m <-> n > m. +Proof NZnle_gt. + +Theorem Zlt_nge : forall n m : Z, n < m <-> ~ n >= m. +Proof NZlt_nge. + +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 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. +Proof NZlt_exists_pred. + +Theorem Zlt_succ_iter_r : + forall (n : nat) (m : Z), m < NZsucc_iter (Datatypes.S n) m. +Proof NZlt_succ_iter_r. + +Theorem Zneq_succ_iter_l : + forall (n : nat) (m : Z), NZsucc_iter (Datatypes.S n) m ~= m. +Proof NZneq_succ_iter_l. + +(** Stronger variant of induction with assumptions n >= 0 (n < 0) +in the induction step *) + +Theorem Zright_induction : + forall A : Z -> Prop, predicate_wd Zeq A -> + forall z : Z, A z -> + (forall n : Z, z <= n -> A n -> A (S n)) -> + forall n : Z, z <= n -> A n. +Proof NZright_induction. + +Theorem Zleft_induction : + forall A : Z -> Prop, predicate_wd Zeq A -> + forall z : Z, A z -> + (forall n : Z, n < z -> A (S n) -> A n) -> + forall n : Z, n <= z -> A n. +Proof NZleft_induction. + +Theorem Zright_induction' : + forall A : Z -> Prop, predicate_wd Zeq A -> + forall z : Z, + (forall n : Z, n <= z -> A n) -> + (forall n : Z, z <= n -> A n -> A (S n)) -> + forall n : Z, A n. +Proof NZright_induction'. + +Theorem Zleft_induction' : + forall A : Z -> Prop, predicate_wd Zeq A -> + forall z : Z, + (forall n : Z, z <= n -> A n) -> + (forall n : Z, n < z -> A (S n) -> A n) -> + forall n : Z, A n. +Proof NZleft_induction'. + +Theorem Zstrong_right_induction : + forall A : Z -> Prop, predicate_wd Zeq A -> + forall z : Z, + (forall n : Z, z <= n -> (forall m : Z, z <= m -> m < n -> A m) -> A n) -> + forall n : Z, z <= n -> A n. +Proof NZstrong_right_induction. + +Theorem Zstrong_left_induction : + forall A : Z -> Prop, predicate_wd Zeq A -> + forall z : Z, + (forall n : Z, n <= z -> (forall m : Z, m <= z -> S n <= m -> A m) -> A n) -> + forall n : Z, n <= z -> A n. +Proof NZstrong_left_induction. + +Theorem Zstrong_right_induction' : + forall A : Z -> Prop, predicate_wd Zeq A -> + forall z : Z, + (forall n : Z, n <= z -> A n) -> + (forall n : Z, z <= n -> (forall m : Z, z <= m -> m < n -> A m) -> A n) -> + forall n : Z, A n. +Proof NZstrong_right_induction'. + +Theorem Zstrong_left_induction' : + forall A : Z -> Prop, predicate_wd Zeq A -> + forall z : Z, + (forall n : Z, z <= n -> A n) -> + (forall n : Z, n <= z -> (forall m : Z, m <= z -> S n <= m -> A m) -> A n) -> + forall n : Z, A n. +Proof NZstrong_left_induction'. + +Theorem Zorder_induction : + forall A : Z -> Prop, predicate_wd Zeq A -> + forall z : Z, A z -> + (forall n : Z, z <= n -> A n -> A (S n)) -> + (forall n : Z, n < z -> A (S n) -> A n) -> + forall n : Z, A n. +Proof NZorder_induction. + +Theorem Zorder_induction' : + forall A : Z -> Prop, predicate_wd Zeq A -> + forall z : Z, A z -> + (forall n : Z, z <= n -> A n -> A (S n)) -> + (forall n : Z, n <= z -> A n -> A (P n)) -> + forall n : Z, A n. +Proof NZorder_induction'. + +Theorem Zorder_induction_0 : + forall A : Z -> Prop, predicate_wd Zeq A -> + A 0 -> + (forall n : Z, 0 <= n -> A n -> A (S n)) -> + (forall n : Z, n < 0 -> A (S n) -> A n) -> + forall n : Z, A n. +Proof NZorder_induction_0. + +Theorem Zorder_induction'_0 : + forall A : Z -> Prop, predicate_wd Zeq A -> + A 0 -> + (forall n : Z, 0 <= n -> A n -> A (S n)) -> + (forall n : Z, n <= 0 -> A n -> A (P n)) -> + forall n : Z, A n. +Proof NZorder_induction'_0. + +Ltac Zinduct n := induction_maker n ltac:(apply Zorder_induction_0). + +(** Elimintation principle for < *) + +Theorem Zlt_ind : + forall A : Z -> Prop, predicate_wd Zeq A -> + forall n : Z, A (S n) -> + (forall m : Z, n < m -> A m -> A (S m)) -> forall m : Z, n < m -> A m. +Proof NZlt_ind. + +(** Elimintation principle for <= *) + +Theorem Zle_ind : + forall A : Z -> Prop, predicate_wd Zeq A -> + forall n : Z, A n -> + (forall m : Z, n <= m -> A m -> A (S m)) -> forall m : Z, n <= m -> A m. +Proof NZle_ind. + +(** Well-founded relations *) + +Theorem Zlt_wf : forall z : Z, well_founded (fun n m : Z => z <= n /\ n < m). +Proof NZlt_wf. + +Theorem Zgt_wf : forall z : Z, well_founded (fun n m : Z => m < n /\ n <= z). +Proof NZgt_wf. + +(* Theorems that are either not valid on N or have different proofs on N and Z *) + +Theorem Zlt_pred_l : forall n : Z, P n < n. +Proof. +intro n; rewrite <- (Zsucc_pred n) at 2; apply Zlt_succ_diag_r. +Qed. + +Theorem Zle_pred_l : forall n : Z, P n <= n. +Proof. +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_r. +Qed. + +Theorem Znle_pred_r : forall n : Z, ~ n <= P n. +Proof. +intro; rewrite <- Zlt_le_pred; apply Zlt_irrefl. +Qed. + +Theorem Zlt_pred_le : forall n m : Z, P n < m <-> n <= m. +Proof. +intros n m; rewrite <- (Zsucc_pred n) at 2. +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; now apply Zlt_le_incl. +Qed. + +Theorem Zle_le_pred : forall n m : Z, n <= m -> P n <= m. +Proof. +intros; apply Zlt_le_incl; now apply <- Zlt_pred_le. +Qed. + +Theorem Zlt_pred_lt : forall n m : Z, n < P m -> n < m. +Proof. +intros n m H; apply Zlt_trans with (P m); [assumption | apply Zlt_pred_l]. +Qed. + +Theorem Zle_pred_lt : forall n m : Z, n <= P m -> n <= m. +Proof. +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. +Proof. +intros; rewrite Zlt_le_pred; symmetry; apply Zlt_pred_le. +Qed. + +Theorem Zpred_le_mono : forall n m : Z, n <= m <-> P n <= P m. +Proof. +intros; rewrite <- Zlt_pred_le; now rewrite Zlt_le_pred. +Qed. + +Theorem Zlt_succ_lt_pred : forall n m : Z, S n < m <-> n < P m. +Proof. +intros n m; now rewrite (Zpred_lt_mono (S n) m), Zpred_succ. +Qed. + +Theorem Zle_succ_le_pred : forall n m : Z, S n <= m <-> n <= P m. +Proof. +intros n m; now rewrite (Zpred_le_mono (S n) m), Zpred_succ. +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_r. +Qed. + +Theorem Zle_pred_lt_succ : forall n m : Z, P n <= m <-> n <= S m. +Proof. +intros n m; now rewrite (Zpred_le_mono n (S m)), Zpred_succ. +Qed. + +Theorem Zneq_pred_l : forall n : Z, P n ~= n. +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/ZMul.v b/theories/Numbers/Integer/Abstract/ZMul.v new file mode 100644 index 00000000..c48d1b4c --- /dev/null +++ b/theories/Numbers/Integer/Abstract/ZMul.v @@ -0,0 +1,115 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +(* Evgeny Makarov, INRIA, 2007 *) +(************************************************************************) + +(*i $Id: ZMul.v 11040 2008-06-03 00:04:16Z letouzey $ i*) + +Require Export ZAdd. + +Module ZMulPropFunct (Import ZAxiomsMod : ZAxiomsSig). +Module Export ZAddPropMod := ZAddPropFunct ZAxiomsMod. +Open Local Scope IntScope. + +Theorem Zmul_wd : + forall n1 n2 : Z, n1 == n2 -> forall m1 m2 : Z, m1 == m2 -> n1 * m1 == n2 * m2. +Proof NZmul_wd. + +Theorem Zmul_0_l : forall n : Z, 0 * n == 0. +Proof NZmul_0_l. + +Theorem Zmul_succ_l : forall n m : Z, (S n) * m == n * m + m. +Proof NZmul_succ_l. + +(* Theorems that are valid for both natural numbers and integers *) + +Theorem Zmul_0_r : forall n : Z, n * 0 == 0. +Proof NZmul_0_r. + +Theorem Zmul_succ_r : forall n m : Z, n * (S m) == n * m + n. +Proof NZmul_succ_r. + +Theorem Zmul_comm : forall n m : Z, n * m == m * n. +Proof NZmul_comm. + +Theorem Zmul_add_distr_r : forall n m p : Z, (n + m) * p == n * p + m * p. +Proof NZmul_add_distr_r. + +Theorem Zmul_add_distr_l : forall n m p : Z, n * (m + p) == n * m + n * p. +Proof NZmul_add_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 Zmul_assoc : forall n m p : Z, n * (m * p) == (n * m) * p. +Proof NZmul_assoc. + +Theorem Zmul_1_l : forall n : Z, 1 * n == n. +Proof NZmul_1_l. + +Theorem Zmul_1_r : forall n : Z, n * 1 == n. +Proof NZmul_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 Zeq_mul_0 : forall n m : Z, n * m == 0 <-> n == 0 \/ m == 0. +Proof NZeq_mul_0. + +Theorem Zneq_mul_0 : forall n m : Z, n ~= 0 /\ m ~= 0 <-> n * m ~= 0. +Proof NZneq_mul_0. + +(* Theorems that are either not valid on N or have different proofs on N and Z *) + +Theorem Zmul_pred_r : forall n m : Z, n * (P m) == n * m - n. +Proof. +intros n m. +rewrite <- (Zsucc_pred m) at 2. +now rewrite Zmul_succ_r, <- Zadd_sub_assoc, Zsub_diag, Zadd_0_r. +Qed. + +Theorem Zmul_pred_l : forall n m : Z, (P n) * m == n * m - m. +Proof. +intros n m; rewrite (Zmul_comm (P n) m), (Zmul_comm n m). apply Zmul_pred_r. +Qed. + +Theorem Zmul_opp_l : forall n m : Z, (- n) * m == - (n * m). +Proof. +intros n m. apply -> Zadd_move_0_r. +now rewrite <- Zmul_add_distr_r, Zadd_opp_diag_l, Zmul_0_l. +Qed. + +Theorem Zmul_opp_r : forall n m : Z, n * (- m) == - (n * m). +Proof. +intros n m; rewrite (Zmul_comm n (- m)), (Zmul_comm n m); apply Zmul_opp_l. +Qed. + +Theorem Zmul_opp_opp : forall n m : Z, (- n) * (- m) == n * m. +Proof. +intros n m; now rewrite Zmul_opp_l, Zmul_opp_r, Zopp_involutive. +Qed. + +Theorem Zmul_sub_distr_l : forall n m p : Z, n * (m - p) == n * m - n * p. +Proof. +intros n m p. do 2 rewrite <- Zadd_opp_r. rewrite Zmul_add_distr_l. +now rewrite Zmul_opp_r. +Qed. + +Theorem Zmul_sub_distr_r : forall n m p : Z, (n - m) * p == n * p - m * p. +Proof. +intros n m p; rewrite (Zmul_comm (n - m) p), (Zmul_comm n p), (Zmul_comm m p); +now apply Zmul_sub_distr_l. +Qed. + +End ZMulPropFunct. + + diff --git a/theories/Numbers/Integer/Abstract/ZMulOrder.v b/theories/Numbers/Integer/Abstract/ZMulOrder.v new file mode 100644 index 00000000..e3f1d9aa --- /dev/null +++ b/theories/Numbers/Integer/Abstract/ZMulOrder.v @@ -0,0 +1,343 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +(* Evgeny Makarov, INRIA, 2007 *) +(************************************************************************) + +(*i $Id: ZMulOrder.v 11040 2008-06-03 00:04:16Z letouzey $ i*) + +Require Export ZAddOrder. + +Module ZMulOrderPropFunct (Import ZAxiomsMod : ZAxiomsSig). +Module Export ZAddOrderPropMod := ZAddOrderPropFunct ZAxiomsMod. +Open Local Scope IntScope. + +Theorem Zmul_lt_pred : + forall p q n m : Z, S p == q -> (p * n < p * m <-> q * n + m < q * m + n). +Proof NZmul_lt_pred. + +Theorem Zmul_lt_mono_pos_l : forall p n m : Z, 0 < p -> (n < m <-> p * n < p * m). +Proof NZmul_lt_mono_pos_l. + +Theorem Zmul_lt_mono_pos_r : forall p n m : Z, 0 < p -> (n < m <-> n * p < m * p). +Proof NZmul_lt_mono_pos_r. + +Theorem Zmul_lt_mono_neg_l : forall p n m : Z, p < 0 -> (n < m <-> p * m < p * n). +Proof NZmul_lt_mono_neg_l. + +Theorem Zmul_lt_mono_neg_r : forall p n m : Z, p < 0 -> (n < m <-> m * p < n * p). +Proof NZmul_lt_mono_neg_r. + +Theorem Zmul_le_mono_nonneg_l : forall n m p : Z, 0 <= p -> n <= m -> p * n <= p * m. +Proof NZmul_le_mono_nonneg_l. + +Theorem Zmul_le_mono_nonpos_l : forall n m p : Z, p <= 0 -> n <= m -> p * m <= p * n. +Proof NZmul_le_mono_nonpos_l. + +Theorem Zmul_le_mono_nonneg_r : forall n m p : Z, 0 <= p -> n <= m -> n * p <= m * p. +Proof NZmul_le_mono_nonneg_r. + +Theorem Zmul_le_mono_nonpos_r : forall n m p : Z, p <= 0 -> n <= m -> m * p <= n * p. +Proof NZmul_le_mono_nonpos_r. + +Theorem Zmul_cancel_l : forall n m p : Z, p ~= 0 -> (p * n == p * m <-> n == m). +Proof NZmul_cancel_l. + +Theorem Zmul_cancel_r : forall n m p : Z, p ~= 0 -> (n * p == m * p <-> n == m). +Proof NZmul_cancel_r. + +Theorem Zmul_id_l : forall n m : Z, m ~= 0 -> (n * m == m <-> n == 1). +Proof NZmul_id_l. + +Theorem Zmul_id_r : forall n m : Z, n ~= 0 -> (n * m == n <-> m == 1). +Proof NZmul_id_r. + +Theorem Zmul_le_mono_pos_l : forall n m p : Z, 0 < p -> (n <= m <-> p * n <= p * m). +Proof NZmul_le_mono_pos_l. + +Theorem Zmul_le_mono_pos_r : forall n m p : Z, 0 < p -> (n <= m <-> n * p <= m * p). +Proof NZmul_le_mono_pos_r. + +Theorem Zmul_le_mono_neg_l : forall n m p : Z, p < 0 -> (n <= m <-> p * m <= p * n). +Proof NZmul_le_mono_neg_l. + +Theorem Zmul_le_mono_neg_r : forall n m p : Z, p < 0 -> (n <= m <-> m * p <= n * p). +Proof NZmul_le_mono_neg_r. + +Theorem Zmul_lt_mono_nonneg : + forall n m p q : Z, 0 <= n -> n < m -> 0 <= p -> p < q -> n * p < m * q. +Proof NZmul_lt_mono_nonneg. + +Theorem Zmul_lt_mono_nonpos : + forall n m p q : Z, m <= 0 -> n < m -> q <= 0 -> p < q -> m * q < n * p. +Proof. +intros n m p q H1 H2 H3 H4. +apply Zle_lt_trans with (m * p). +apply Zmul_le_mono_nonpos_l; [assumption | now apply Zlt_le_incl]. +apply -> Zmul_lt_mono_neg_r; [assumption | now apply Zlt_le_trans with q]. +Qed. + +Theorem Zmul_le_mono_nonneg : + forall n m p q : Z, 0 <= n -> n <= m -> 0 <= p -> p <= q -> n * p <= m * q. +Proof NZmul_le_mono_nonneg. + +Theorem Zmul_le_mono_nonpos : + forall n m p q : Z, m <= 0 -> n <= m -> q <= 0 -> p <= q -> m * q <= n * p. +Proof. +intros n m p q H1 H2 H3 H4. +apply Zle_trans with (m * p). +now apply Zmul_le_mono_nonpos_l. +apply Zmul_le_mono_nonpos_r; [now apply Zle_trans with q | assumption]. +Qed. + +Theorem Zmul_pos_pos : forall n m : Z, 0 < n -> 0 < m -> 0 < n * m. +Proof NZmul_pos_pos. + +Theorem Zmul_neg_neg : forall n m : Z, n < 0 -> m < 0 -> 0 < n * m. +Proof NZmul_neg_neg. + +Theorem Zmul_pos_neg : forall n m : Z, 0 < n -> m < 0 -> n * m < 0. +Proof NZmul_pos_neg. + +Theorem Zmul_neg_pos : forall n m : Z, n < 0 -> 0 < m -> n * m < 0. +Proof NZmul_neg_pos. + +Theorem Zmul_nonneg_nonneg : forall n m : Z, 0 <= n -> 0 <= m -> 0 <= n * m. +Proof. +intros n m H1 H2. +rewrite <- (Zmul_0_l m). now apply Zmul_le_mono_nonneg_r. +Qed. + +Theorem Zmul_nonpos_nonpos : forall n m : Z, n <= 0 -> m <= 0 -> 0 <= n * m. +Proof. +intros n m H1 H2. +rewrite <- (Zmul_0_l m). now apply Zmul_le_mono_nonpos_r. +Qed. + +Theorem Zmul_nonneg_nonpos : forall n m : Z, 0 <= n -> m <= 0 -> n * m <= 0. +Proof. +intros n m H1 H2. +rewrite <- (Zmul_0_l m). now apply Zmul_le_mono_nonpos_r. +Qed. + +Theorem Zmul_nonpos_nonneg : forall n m : Z, n <= 0 -> 0 <= m -> n * m <= 0. +Proof. +intros; rewrite Zmul_comm; now apply Zmul_nonneg_nonpos. +Qed. + +Theorem Zlt_1_mul_pos : forall n m : Z, 1 < n -> 0 < m -> 1 < n * m. +Proof NZlt_1_mul_pos. + +Theorem Zeq_mul_0 : forall n m : Z, n * m == 0 <-> n == 0 \/ m == 0. +Proof NZeq_mul_0. + +Theorem Zneq_mul_0 : forall n m : Z, n ~= 0 /\ m ~= 0 <-> n * m ~= 0. +Proof NZneq_mul_0. + +Theorem Zeq_square_0 : forall n : Z, n * n == 0 <-> n == 0. +Proof NZeq_square_0. + +Theorem Zeq_mul_0_l : forall n m : Z, n * m == 0 -> m ~= 0 -> n == 0. +Proof NZeq_mul_0_l. + +Theorem Zeq_mul_0_r : forall n m : Z, n * m == 0 -> n ~= 0 -> m == 0. +Proof NZeq_mul_0_r. + +Theorem Zlt_0_mul : forall n m : Z, 0 < n * m <-> 0 < n /\ 0 < m \/ m < 0 /\ n < 0. +Proof NZlt_0_mul. + +Notation Zmul_pos := Zlt_0_mul (only parsing). + +Theorem Zlt_mul_0 : + forall n m : Z, n * m < 0 <-> n < 0 /\ m > 0 \/ n > 0 /\ m < 0. +Proof. +intros n m; split; [intro H | intros [[H1 H2] | [H1 H2]]]. +destruct (Zlt_trichotomy n 0) as [H1 | [H1 | H1]]; +[| rewrite H1 in H; rewrite Zmul_0_l in H; false_hyp H Zlt_irrefl |]; +(destruct (Zlt_trichotomy m 0) as [H2 | [H2 | H2]]; +[| rewrite H2 in H; rewrite Zmul_0_r in H; false_hyp H Zlt_irrefl |]); +try (left; now split); try (right; now split). +assert (H3 : n * m > 0) by now apply Zmul_neg_neg. +elimtype False; now apply (Zlt_asymm (n * m) 0). +assert (H3 : n * m > 0) by now apply Zmul_pos_pos. +elimtype False; now apply (Zlt_asymm (n * m) 0). +now apply Zmul_neg_pos. now apply Zmul_pos_neg. +Qed. + +Notation Zmul_neg := Zlt_mul_0 (only parsing). + +Theorem Zle_0_mul : + forall n m : Z, 0 <= n * m -> 0 <= n /\ 0 <= m \/ n <= 0 /\ m <= 0. +Proof. +assert (R : forall n : Z, 0 == n <-> n == 0) by (intros; split; apply Zeq_symm). +intros n m. repeat rewrite Zlt_eq_cases. repeat rewrite R. +rewrite Zlt_0_mul, Zeq_mul_0. +pose proof (Zlt_trichotomy n 0); pose proof (Zlt_trichotomy m 0). tauto. +Qed. + +Notation Zmul_nonneg := Zle_0_mul (only parsing). + +Theorem Zle_mul_0 : + forall n m : Z, n * m <= 0 -> 0 <= n /\ m <= 0 \/ n <= 0 /\ 0 <= m. +Proof. +assert (R : forall n : Z, 0 == n <-> n == 0) by (intros; split; apply Zeq_symm). +intros n m. repeat rewrite Zlt_eq_cases. repeat rewrite R. +rewrite Zlt_mul_0, Zeq_mul_0. +pose proof (Zlt_trichotomy n 0); pose proof (Zlt_trichotomy m 0). tauto. +Qed. + +Notation Zmul_nonpos := Zle_mul_0 (only parsing). + +Theorem Zle_0_square : forall n : Z, 0 <= n * n. +Proof. +intro n; destruct (Zneg_nonneg_cases n). +apply Zlt_le_incl; now apply Zmul_neg_neg. +now apply Zmul_nonneg_nonneg. +Qed. + +Notation Zsquare_nonneg := Zle_0_square (only parsing). + +Theorem Znlt_square_0 : forall n : Z, ~ n * n < 0. +Proof. +intros n H. apply -> Zlt_nge in H. apply H. apply Zsquare_nonneg. +Qed. + +Theorem Zsquare_lt_mono_nonneg : forall n m : Z, 0 <= n -> n < m -> n * n < m * m. +Proof NZsquare_lt_mono_nonneg. + +Theorem Zsquare_lt_mono_nonpos : forall n m : Z, n <= 0 -> m < n -> n * n < m * m. +Proof. +intros n m H1 H2. now apply Zmul_lt_mono_nonpos. +Qed. + +Theorem Zsquare_le_mono_nonneg : forall n m : Z, 0 <= n -> n <= m -> n * n <= m * m. +Proof NZsquare_le_mono_nonneg. + +Theorem Zsquare_le_mono_nonpos : forall n m : Z, n <= 0 -> m <= n -> n * n <= m * m. +Proof. +intros n m H1 H2. now apply Zmul_le_mono_nonpos. +Qed. + +Theorem Zsquare_lt_simpl_nonneg : forall n m : Z, 0 <= m -> n * n < m * m -> n < m. +Proof NZsquare_lt_simpl_nonneg. + +Theorem Zsquare_le_simpl_nonneg : forall n m : Z, 0 <= m -> n * n <= m * m -> n <= m. +Proof NZsquare_le_simpl_nonneg. + +Theorem Zsquare_lt_simpl_nonpos : forall n m : Z, m <= 0 -> n * n < m * m -> m < n. +Proof. +intros n m H1 H2. destruct (Zle_gt_cases n 0). +destruct (NZlt_ge_cases m n). +assumption. assert (F : m * m <= n * n) by now apply Zsquare_le_mono_nonpos. +apply -> NZle_ngt in F. false_hyp H2 F. +now apply Zle_lt_trans with 0. +Qed. + +Theorem Zsquare_le_simpl_nonpos : forall n m : NZ, m <= 0 -> n * n <= m * m -> m <= n. +Proof. +intros n m H1 H2. destruct (NZle_gt_cases n 0). +destruct (NZle_gt_cases m n). +assumption. assert (F : m * m < n * n) by now apply Zsquare_lt_mono_nonpos. +apply -> NZlt_nge in F. false_hyp H2 F. +apply Zlt_le_incl; now apply NZle_lt_trans with 0. +Qed. + +Theorem Zmul_2_mono_l : forall n m : Z, n < m -> 1 + (1 + 1) * n < (1 + 1) * m. +Proof NZmul_2_mono_l. + +Theorem Zlt_1_mul_neg : forall n m : Z, n < -1 -> m < 0 -> 1 < n * m. +Proof. +intros n m H1 H2. apply -> (NZmul_lt_mono_neg_r m) in H1. +apply <- Zopp_pos_neg in H2. rewrite Zmul_opp_l, Zmul_1_l in H1. +now apply Zlt_1_l with (- m). +assumption. +Qed. + +Theorem Zlt_mul_n1_neg : forall n m : Z, 1 < n -> m < 0 -> n * m < -1. +Proof. +intros n m H1 H2. apply -> (NZmul_lt_mono_neg_r m) in H1. +rewrite Zmul_1_l in H1. now apply Zlt_n1_r with m. +assumption. +Qed. + +Theorem Zlt_mul_n1_pos : forall n m : Z, n < -1 -> 0 < m -> n * m < -1. +Proof. +intros n m H1 H2. apply -> (NZmul_lt_mono_pos_r m) in H1. +rewrite Zmul_opp_l, Zmul_1_l in H1. +apply <- Zopp_neg_pos in H2. now apply Zlt_n1_r with (- m). +assumption. +Qed. + +Theorem Zlt_1_mul_l : 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_mul_n1_neg. +right; left; now rewrite H1, Zmul_0_r. +right; right; now apply Zlt_1_mul_pos. +Qed. + +Theorem Zlt_n1_mul_r : 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_mul_neg. +right; left; now rewrite H1, Zmul_0_r. +left. now apply Zlt_mul_n1_pos. +Qed. + +Theorem Zeq_mul_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 Zmul_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_mul_l 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_mul_l n m) in H. rewrite Zmul_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. + +Theorem Zlt_mul_diag_l : forall n m : Z, n < 0 -> (1 < m <-> n * m < n). +Proof. +intros n m H. stepr (n * m < n * 1) by now rewrite Zmul_1_r. +now apply Zmul_lt_mono_neg_l. +Qed. + +Theorem Zlt_mul_diag_r : forall n m : Z, 0 < n -> (1 < m <-> n < n * m). +Proof. +intros n m H. stepr (n * 1 < n * m) by now rewrite Zmul_1_r. +now apply Zmul_lt_mono_pos_l. +Qed. + +Theorem Zle_mul_diag_l : forall n m : Z, n < 0 -> (1 <= m <-> n * m <= n). +Proof. +intros n m H. stepr (n * m <= n * 1) by now rewrite Zmul_1_r. +now apply Zmul_le_mono_neg_l. +Qed. + +Theorem Zle_mul_diag_r : forall n m : Z, 0 < n -> (1 <= m <-> n <= n * m). +Proof. +intros n m H. stepr (n * 1 <= n * m) by now rewrite Zmul_1_r. +now apply Zmul_le_mono_pos_l. +Qed. + +Theorem Zlt_mul_r : forall n m p : Z, 0 < n -> 1 < p -> n < m -> n < m * p. +Proof. +intros. stepl (n * 1) by now rewrite Zmul_1_r. +apply Zmul_lt_mono_nonneg. +now apply Zlt_le_incl. assumption. apply Zle_0_1. assumption. +Qed. + +End ZMulOrderPropFunct. + diff --git a/theories/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v new file mode 100644 index 00000000..09abf424 --- /dev/null +++ b/theories/Numbers/Integer/BigZ/BigZ.v @@ -0,0 +1,109 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +(* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) +(************************************************************************) + +(*i $Id: BigZ.v 11040 2008-06-03 00:04:16Z letouzey $ i*) + +Require Export BigN. +Require Import ZMulOrder. +Require Import ZSig. +Require Import ZSigZAxioms. +Require Import ZMake. + +Module BigZ <: ZType := ZMake.Make BigN. + +(** Module [BigZ] implements [ZAxiomsSig] *) + +Module Export BigZAxiomsMod := ZSig_ZAxioms BigZ. +Module Export BigZMulOrderPropMod := ZMulOrderPropFunct BigZAxiomsMod. + +(** Notations about [BigZ] *) + +Notation bigZ := BigZ.t. + +Delimit Scope bigZ_scope with bigZ. +Bind Scope bigZ_scope with bigZ. +Bind Scope bigZ_scope with BigZ.t. +Bind Scope bigZ_scope with BigZ.t_. + +Notation Local "0" := BigZ.zero : bigZ_scope. +Infix "+" := BigZ.add : bigZ_scope. +Infix "-" := BigZ.sub : bigZ_scope. +Notation "- x" := (BigZ.opp x) : bigZ_scope. +Infix "*" := BigZ.mul : bigZ_scope. +Infix "/" := BigZ.div : bigZ_scope. +Infix "?=" := BigZ.compare : bigZ_scope. +Infix "==" := BigZ.eq (at level 70, no associativity) : bigZ_scope. +Infix "<" := BigZ.lt : bigZ_scope. +Infix "<=" := BigZ.le : bigZ_scope. +Notation "[ i ]" := (BigZ.to_Z i) : bigZ_scope. + +Open Scope bigZ_scope. + +(** Some additional results about [BigZ] *) + +Theorem spec_to_Z: forall n:bigZ, + BigN.to_Z (BigZ.to_N n) = ((Zsgn [n]) * [n])%Z. +Proof. +intros n; case n; simpl; intros p; + generalize (BigN.spec_pos p); case (BigN.to_Z p); auto. +intros p1 H1; case H1; auto. +intros p1 H1; case H1; auto. +Qed. + +Theorem spec_to_N n: + ([n] = Zsgn [n] * (BigN.to_Z (BigZ.to_N n)))%Z. +Proof. +intros n; case n; simpl; intros p; + generalize (BigN.spec_pos p); case (BigN.to_Z p); auto. +intros p1 H1; case H1; auto. +intros p1 H1; case H1; auto. +Qed. + +Theorem spec_to_Z_pos: forall n, (0 <= [n])%Z -> + BigN.to_Z (BigZ.to_N n) = [n]. +Proof. +intros n; case n; simpl; intros p; + generalize (BigN.spec_pos p); case (BigN.to_Z p); auto. +intros p1 _ H1; case H1; auto. +intros p1 H1; case H1; auto. +Qed. + +Lemma sub_opp : forall x y : bigZ, x - y == x + (- y). +Proof. +red; intros; zsimpl; auto. +Qed. + +Lemma add_opp : forall x : bigZ, x + (- x) == 0. +Proof. +red; intros; zsimpl; auto with zarith. +Qed. + +(** [BigZ] is a ring *) + +Lemma BigZring : + ring_theory BigZ.zero BigZ.one BigZ.add BigZ.mul BigZ.sub BigZ.opp BigZ.eq. +Proof. +constructor. +exact Zadd_0_l. +exact Zadd_comm. +exact Zadd_assoc. +exact Zmul_1_l. +exact Zmul_comm. +exact Zmul_assoc. +exact Zmul_add_distr_r. +exact sub_opp. +exact add_opp. +Qed. + +Add Ring BigZr : BigZring. + +(** Todo: tactic translating from [BigZ] to [Z] + omega *) + +(** Todo: micromega *) diff --git a/theories/Numbers/Integer/BigZ/ZMake.v b/theories/Numbers/Integer/BigZ/ZMake.v new file mode 100644 index 00000000..1f2b12bb --- /dev/null +++ b/theories/Numbers/Integer/BigZ/ZMake.v @@ -0,0 +1,491 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +(* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) +(************************************************************************) + +(*i $Id: ZMake.v 11027 2008-06-01 13:28:59Z letouzey $ i*) + +Require Import ZArith. +Require Import BigNumPrelude. +Require Import NSig. +Require Import ZSig. + +Open Scope Z_scope. + +(** * ZMake + + A generic transformation from a structure of natural numbers + [NSig.NType] to a structure of integers [ZSig.ZType]. +*) + +Module Make (N:NType) <: ZType. + + Inductive t_ := + | Pos : N.t -> t_ + | Neg : N.t -> t_. + + Definition t := t_. + + Definition zero := Pos N.zero. + Definition one := Pos N.one. + Definition minus_one := Neg N.one. + + Definition of_Z x := + match x with + | Zpos x => Pos (N.of_N (Npos x)) + | Z0 => zero + | Zneg x => Neg (N.of_N (Npos x)) + end. + + Definition to_Z x := + match x with + | Pos nx => N.to_Z nx + | Neg nx => Zopp (N.to_Z nx) + end. + + Theorem spec_of_Z: forall x, to_Z (of_Z x) = x. + intros x; case x; unfold to_Z, of_Z, zero. + exact N.spec_0. + intros; rewrite N.spec_of_N; auto. + intros; rewrite N.spec_of_N; auto. + Qed. + + Definition eq x y := (to_Z x = to_Z y). + + Theorem spec_0: to_Z zero = 0. + exact N.spec_0. + Qed. + + Theorem spec_1: to_Z one = 1. + exact N.spec_1. + Qed. + + Theorem spec_m1: to_Z minus_one = -1. + simpl; rewrite N.spec_1; auto. + Qed. + + Definition compare x y := + match x, y with + | Pos nx, Pos ny => N.compare nx ny + | Pos nx, Neg ny => + match N.compare nx N.zero with + | Gt => Gt + | _ => N.compare ny N.zero + end + | Neg nx, Pos ny => + match N.compare N.zero nx with + | Lt => Lt + | _ => N.compare N.zero ny + end + | Neg nx, Neg ny => N.compare ny nx + end. + + Definition lt n m := compare n m = Lt. + Definition le n m := compare n m <> Gt. + Definition min n m := match compare n m with Gt => m | _ => n end. + Definition max n m := match compare n m with Lt => m | _ => n end. + + Theorem spec_compare: forall x y, + match compare x y with + Eq => to_Z x = to_Z y + | Lt => to_Z x < to_Z y + | Gt => to_Z x > to_Z y + end. + unfold compare, to_Z; intros x y; case x; case y; clear x y; + intros x y; auto; generalize (N.spec_pos x) (N.spec_pos y). + generalize (N.spec_compare y x); case N.compare; auto with zarith. + generalize (N.spec_compare y N.zero); case N.compare; + try rewrite N.spec_0; auto with zarith. + generalize (N.spec_compare x N.zero); case N.compare; + rewrite N.spec_0; auto with zarith. + generalize (N.spec_compare x N.zero); case N.compare; + rewrite N.spec_0; auto with zarith. + generalize (N.spec_compare N.zero y); case N.compare; + try rewrite N.spec_0; auto with zarith. + generalize (N.spec_compare N.zero x); case N.compare; + rewrite N.spec_0; auto with zarith. + generalize (N.spec_compare N.zero x); case N.compare; + rewrite N.spec_0; auto with zarith. + generalize (N.spec_compare x y); case N.compare; auto with zarith. + Qed. + + Definition eq_bool x y := + match compare x y with + | Eq => true + | _ => false + end. + + Theorem spec_eq_bool: forall x y, + if eq_bool x y then to_Z x = to_Z y else to_Z x <> to_Z y. + intros x y; unfold eq_bool; + generalize (spec_compare x y); case compare; auto with zarith. + Qed. + + Definition cmp_sign x y := + match x, y with + | Pos nx, Neg ny => + if N.eq_bool ny N.zero then Eq else Gt + | Neg nx, Pos ny => + if N.eq_bool nx N.zero then Eq else Lt + | _, _ => Eq + end. + + Theorem spec_cmp_sign: forall x y, + match cmp_sign x y with + | Gt => 0 <= to_Z x /\ to_Z y < 0 + | Lt => to_Z x < 0 /\ 0 <= to_Z y + | Eq => True + end. + Proof. + intros [x | x] [y | y]; unfold cmp_sign; auto. + generalize (N.spec_eq_bool y N.zero); case N.eq_bool; auto. + rewrite N.spec_0; unfold to_Z. + generalize (N.spec_pos x) (N.spec_pos y); auto with zarith. + generalize (N.spec_eq_bool x N.zero); case N.eq_bool; auto. + rewrite N.spec_0; unfold to_Z. + generalize (N.spec_pos x) (N.spec_pos y); auto with zarith. + Qed. + + Definition to_N x := + match x with + | Pos nx => nx + | Neg nx => nx + end. + + Definition abs x := Pos (to_N x). + + Theorem spec_abs: forall x, to_Z (abs x) = Zabs (to_Z x). + intros x; case x; clear x; intros x; assert (F:=N.spec_pos x). + simpl; rewrite Zabs_eq; auto. + simpl; rewrite Zabs_non_eq; simpl; auto with zarith. + Qed. + + Definition opp x := + match x with + | Pos nx => Neg nx + | Neg nx => Pos nx + end. + + Theorem spec_opp: forall x, to_Z (opp x) = - to_Z x. + intros x; case x; simpl; auto with zarith. + Qed. + + Definition succ x := + match x with + | Pos n => Pos (N.succ n) + | Neg n => + match N.compare N.zero n with + | Lt => Neg (N.pred n) + | _ => one + end + end. + + Theorem spec_succ: forall n, to_Z (succ n) = to_Z n + 1. + intros x; case x; clear x; intros x. + exact (N.spec_succ x). + simpl; generalize (N.spec_compare N.zero x); case N.compare; + rewrite N.spec_0; simpl. + intros HH; rewrite <- HH; rewrite N.spec_1; ring. + intros HH; rewrite N.spec_pred; auto with zarith. + generalize (N.spec_pos x); auto with zarith. + Qed. + + Definition add x y := + match x, y with + | Pos nx, Pos ny => Pos (N.add nx ny) + | Pos nx, Neg ny => + match N.compare nx ny with + | Gt => Pos (N.sub nx ny) + | Eq => zero + | Lt => Neg (N.sub ny nx) + end + | Neg nx, Pos ny => + match N.compare nx ny with + | Gt => Neg (N.sub nx ny) + | Eq => zero + | Lt => Pos (N.sub ny nx) + end + | Neg nx, Neg ny => Neg (N.add nx ny) + end. + + Theorem spec_add: forall x y, to_Z (add x y) = to_Z x + to_Z y. + unfold add, to_Z; intros [x | x] [y | y]. + exact (N.spec_add x y). + unfold zero; generalize (N.spec_compare x y); case N.compare. + rewrite N.spec_0; auto with zarith. + intros; rewrite N.spec_sub; try ring; auto with zarith. + intros; rewrite N.spec_sub; try ring; auto with zarith. + unfold zero; generalize (N.spec_compare x y); case N.compare. + rewrite N.spec_0; auto with zarith. + intros; rewrite N.spec_sub; try ring; auto with zarith. + intros; rewrite N.spec_sub; try ring; auto with zarith. + intros; rewrite N.spec_add; try ring; auto with zarith. + Qed. + + Definition pred x := + match x with + | Pos nx => + match N.compare N.zero nx with + | Lt => Pos (N.pred nx) + | _ => minus_one + end + | Neg nx => Neg (N.succ nx) + end. + + Theorem spec_pred: forall x, to_Z (pred x) = to_Z x - 1. + unfold pred, to_Z, minus_one; intros [x | x]. + generalize (N.spec_compare N.zero x); case N.compare; + rewrite N.spec_0; try rewrite N.spec_1; auto with zarith. + intros H; exact (N.spec_pred _ H). + generalize (N.spec_pos x); auto with zarith. + rewrite N.spec_succ; ring. + Qed. + + Definition sub x y := + match x, y with + | Pos nx, Pos ny => + match N.compare nx ny with + | Gt => Pos (N.sub nx ny) + | Eq => zero + | Lt => Neg (N.sub ny nx) + end + | Pos nx, Neg ny => Pos (N.add nx ny) + | Neg nx, Pos ny => Neg (N.add nx ny) + | Neg nx, Neg ny => + match N.compare nx ny with + | Gt => Neg (N.sub nx ny) + | Eq => zero + | Lt => Pos (N.sub ny nx) + end + end. + + Theorem spec_sub: forall x y, to_Z (sub x y) = to_Z x - to_Z y. + unfold sub, to_Z; intros [x | x] [y | y]. + unfold zero; generalize (N.spec_compare x y); case N.compare. + rewrite N.spec_0; auto with zarith. + intros; rewrite N.spec_sub; try ring; auto with zarith. + intros; rewrite N.spec_sub; try ring; auto with zarith. + rewrite N.spec_add; ring. + rewrite N.spec_add; ring. + unfold zero; generalize (N.spec_compare x y); case N.compare. + rewrite N.spec_0; auto with zarith. + intros; rewrite N.spec_sub; try ring; auto with zarith. + intros; rewrite N.spec_sub; try ring; auto with zarith. + Qed. + + Definition mul x y := + match x, y with + | Pos nx, Pos ny => Pos (N.mul nx ny) + | Pos nx, Neg ny => Neg (N.mul nx ny) + | Neg nx, Pos ny => Neg (N.mul nx ny) + | Neg nx, Neg ny => Pos (N.mul nx ny) + end. + + + Theorem spec_mul: forall x y, to_Z (mul x y) = to_Z x * to_Z y. + unfold mul, to_Z; intros [x | x] [y | y]; rewrite N.spec_mul; ring. + Qed. + + Definition square x := + match x with + | Pos nx => Pos (N.square nx) + | Neg nx => Pos (N.square nx) + end. + + Theorem spec_square: forall x, to_Z (square x) = to_Z x * to_Z x. + unfold square, to_Z; intros [x | x]; rewrite N.spec_square; ring. + Qed. + + Definition power_pos x p := + match x with + | Pos nx => Pos (N.power_pos nx p) + | Neg nx => + match p with + | xH => x + | xO _ => Pos (N.power_pos nx p) + | xI _ => Neg (N.power_pos nx p) + end + end. + + Theorem spec_power_pos: forall x n, to_Z (power_pos x n) = to_Z x ^ Zpos n. + assert (F0: forall x, (-x)^2 = x^2). + intros x; rewrite Zpower_2; ring. + unfold power_pos, to_Z; intros [x | x] [p | p |]; + try rewrite N.spec_power_pos; try ring. + assert (F: 0 <= 2 * Zpos p). + assert (0 <= Zpos p); auto with zarith. + rewrite Zpos_xI; repeat rewrite Zpower_exp; auto with zarith. + repeat rewrite Zpower_mult; auto with zarith. + rewrite F0; ring. + assert (F: 0 <= 2 * Zpos p). + assert (0 <= Zpos p); auto with zarith. + rewrite Zpos_xO; repeat rewrite Zpower_exp; auto with zarith. + repeat rewrite Zpower_mult; auto with zarith. + rewrite F0; ring. + Qed. + + Definition sqrt x := + match x with + | Pos nx => Pos (N.sqrt nx) + | Neg nx => Neg N.zero + end. + + + Theorem spec_sqrt: forall x, 0 <= to_Z x -> + to_Z (sqrt x) ^ 2 <= to_Z x < (to_Z (sqrt x) + 1) ^ 2. + unfold to_Z, sqrt; intros [x | x] H. + exact (N.spec_sqrt x). + replace (N.to_Z x) with 0. + rewrite N.spec_0; simpl Zpower; unfold Zpower_pos, iter_pos; + auto with zarith. + generalize (N.spec_pos x); auto with zarith. + Qed. + + Definition div_eucl x y := + match x, y with + | Pos nx, Pos ny => + let (q, r) := N.div_eucl nx ny in + (Pos q, Pos r) + | Pos nx, Neg ny => + let (q, r) := N.div_eucl nx ny in + match N.compare N.zero r with + | Eq => (Neg q, zero) + | _ => (Neg (N.succ q), Neg (N.sub ny r)) + end + | Neg nx, Pos ny => + let (q, r) := N.div_eucl nx ny in + match N.compare N.zero r with + | Eq => (Neg q, zero) + | _ => (Neg (N.succ q), Pos (N.sub ny r)) + end + | Neg nx, Neg ny => + let (q, r) := N.div_eucl nx ny in + (Pos q, Neg r) + end. + + + Theorem spec_div_eucl: forall x y, + to_Z y <> 0 -> + let (q,r) := div_eucl x y in + (to_Z q, to_Z r) = Zdiv_eucl (to_Z x) (to_Z y). + unfold div_eucl, to_Z; intros [x | x] [y | y] H. + assert (H1: 0 < N.to_Z y). + generalize (N.spec_pos y); auto with zarith. + generalize (N.spec_div_eucl x y H1); case N.div_eucl; auto. + assert (HH: 0 < N.to_Z y). + generalize (N.spec_pos y); auto with zarith. + generalize (N.spec_div_eucl x y HH); case N.div_eucl; auto. + intros q r; generalize (N.spec_pos x) HH; unfold Zdiv_eucl; + case_eq (N.to_Z x); case_eq (N.to_Z y); + try (intros; apply False_ind; auto with zarith; fail). + intros p He1 He2 _ _ H1; injection H1; intros H2 H3. + generalize (N.spec_compare N.zero r); case N.compare; + unfold zero; rewrite N.spec_0; try rewrite H3; auto. + rewrite H2; intros; apply False_ind; auto with zarith. + rewrite H2; intros; apply False_ind; auto with zarith. + intros p _ _ _ H1; discriminate H1. + intros p He p1 He1 H1 _. + generalize (N.spec_compare N.zero r); case N.compare. + change (- Zpos p) with (Zneg p). + unfold zero; lazy zeta. + rewrite N.spec_0; intros H2; rewrite <- H2. + intros H3; rewrite <- H3; auto. + rewrite N.spec_0; intros H2. + change (- Zpos p) with (Zneg p); lazy iota beta. + intros H3; rewrite <- H3; auto. + rewrite N.spec_succ; rewrite N.spec_sub. + generalize H2; case (N.to_Z r). + intros; apply False_ind; auto with zarith. + intros p2 _; rewrite He; auto with zarith. + change (Zneg p) with (- (Zpos p)); apply f_equal2 with (f := @pair Z Z); ring. + intros p2 H4; discriminate H4. + assert (N.to_Z r = (Zpos p1 mod (Zpos p))). + unfold Zmod, Zdiv_eucl; rewrite <- H3; auto. + case (Z_mod_lt (Zpos p1) (Zpos p)); auto with zarith. + rewrite N.spec_0; intros H2; generalize (N.spec_pos r); + intros; apply False_ind; auto with zarith. + assert (HH: 0 < N.to_Z y). + generalize (N.spec_pos y); auto with zarith. + generalize (N.spec_div_eucl x y HH); case N.div_eucl; auto. + intros q r; generalize (N.spec_pos x) HH; unfold Zdiv_eucl; + case_eq (N.to_Z x); case_eq (N.to_Z y); + try (intros; apply False_ind; auto with zarith; fail). + intros p He1 He2 _ _ H1; injection H1; intros H2 H3. + generalize (N.spec_compare N.zero r); case N.compare; + unfold zero; rewrite N.spec_0; try rewrite H3; auto. + rewrite H2; intros; apply False_ind; auto with zarith. + rewrite H2; intros; apply False_ind; auto with zarith. + intros p _ _ _ H1; discriminate H1. + intros p He p1 He1 H1 _. + generalize (N.spec_compare N.zero r); case N.compare. + change (- Zpos p1) with (Zneg p1). + unfold zero; lazy zeta. + rewrite N.spec_0; intros H2; rewrite <- H2. + intros H3; rewrite <- H3; auto. + rewrite N.spec_0; intros H2. + change (- Zpos p1) with (Zneg p1); lazy iota beta. + intros H3; rewrite <- H3; auto. + rewrite N.spec_succ; rewrite N.spec_sub. + generalize H2; case (N.to_Z r). + intros; apply False_ind; auto with zarith. + intros p2 _; rewrite He; auto with zarith. + intros p2 H4; discriminate H4. + assert (N.to_Z r = (Zpos p1 mod (Zpos p))). + unfold Zmod, Zdiv_eucl; rewrite <- H3; auto. + case (Z_mod_lt (Zpos p1) (Zpos p)); auto with zarith. + rewrite N.spec_0; generalize (N.spec_pos r); intros; apply False_ind; auto with zarith. + assert (H1: 0 < N.to_Z y). + generalize (N.spec_pos y); auto with zarith. + generalize (N.spec_div_eucl x y H1); case N.div_eucl; auto. + intros q r; generalize (N.spec_pos x) H1; unfold Zdiv_eucl; + case_eq (N.to_Z x); case_eq (N.to_Z y); + try (intros; apply False_ind; auto with zarith; fail). + change (-0) with 0; lazy iota beta; auto. + intros p _ _ _ _ H2; injection H2. + intros H3 H4; rewrite H3; rewrite H4; auto. + intros p _ _ _ H2; discriminate H2. + intros p He p1 He1 _ _ H2. + change (- Zpos p1) with (Zneg p1); lazy iota beta. + change (- Zpos p) with (Zneg p); lazy iota beta. + rewrite <- H2; auto. + Qed. + + Definition div x y := fst (div_eucl x y). + + Definition spec_div: forall x y, + to_Z y <> 0 -> to_Z (div x y) = to_Z x / to_Z y. + intros x y H1; generalize (spec_div_eucl x y H1); unfold div, Zdiv. + case div_eucl; case Zdiv_eucl; simpl; auto. + intros q r q11 r1 H; injection H; auto. + Qed. + + Definition modulo x y := snd (div_eucl x y). + + Theorem spec_modulo: + forall x y, to_Z y <> 0 -> to_Z (modulo x y) = to_Z x mod to_Z y. + intros x y H1; generalize (spec_div_eucl x y H1); unfold modulo, Zmod. + case div_eucl; case Zdiv_eucl; simpl; auto. + intros q r q11 r1 H; injection H; auto. + Qed. + + Definition gcd x y := + match x, y with + | Pos nx, Pos ny => Pos (N.gcd nx ny) + | Pos nx, Neg ny => Pos (N.gcd nx ny) + | Neg nx, Pos ny => Pos (N.gcd nx ny) + | Neg nx, Neg ny => Pos (N.gcd nx ny) + end. + + Theorem spec_gcd: forall a b, to_Z (gcd a b) = Zgcd (to_Z a) (to_Z b). + unfold gcd, Zgcd, to_Z; intros [x | x] [y | y]; rewrite N.spec_gcd; unfold Zgcd; + auto; case N.to_Z; simpl; auto with zarith; + try rewrite Zabs_Zopp; auto; + case N.to_Z; simpl; auto with zarith. + Qed. + +End Make. diff --git a/theories/Numbers/Integer/Binary/ZBinary.v b/theories/Numbers/Integer/Binary/ZBinary.v new file mode 100644 index 00000000..66d2a96a --- /dev/null +++ b/theories/Numbers/Integer/Binary/ZBinary.v @@ -0,0 +1,249 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +(* Evgeny Makarov, INRIA, 2007 *) +(************************************************************************) + +(*i $Id: ZBinary.v 11040 2008-06-03 00:04:16Z letouzey $ i*) + +Require Import ZMulOrder. +Require Import ZArith. + +Open Local Scope Z_scope. + +Module ZBinAxiomsMod <: ZAxiomsSig. +Module Export NZOrdAxiomsMod <: NZOrdAxiomsSig. +Module Export NZAxiomsMod <: NZAxiomsSig. + +Definition NZ := Z. +Definition NZeq := (@eq Z). +Definition NZ0 := 0. +Definition NZsucc := Zsucc'. +Definition NZpred := Zpred'. +Definition NZadd := Zplus. +Definition NZsub := Zminus. +Definition NZmul := Zmult. + +Theorem NZeq_equiv : equiv Z NZeq. +Proof. +exact (@eq_equiv Z). +Qed. + +Add Relation Z NZeq + reflexivity proved by (proj1 NZeq_equiv) + symmetry proved by (proj2 (proj2 NZeq_equiv)) + transitivity proved by (proj1 (proj2 NZeq_equiv)) +as NZeq_rel. + +Add Morphism NZsucc with signature NZeq ==> NZeq as NZsucc_wd. +Proof. +congruence. +Qed. + +Add Morphism NZpred with signature NZeq ==> NZeq as NZpred_wd. +Proof. +congruence. +Qed. + +Add Morphism NZadd with signature NZeq ==> NZeq ==> NZeq as NZadd_wd. +Proof. +congruence. +Qed. + +Add Morphism NZsub with signature NZeq ==> NZeq ==> NZeq as NZsub_wd. +Proof. +congruence. +Qed. + +Add Morphism NZmul with signature NZeq ==> NZeq ==> NZeq as NZmul_wd. +Proof. +congruence. +Qed. + +Theorem NZpred_succ : forall n : Z, NZpred (NZsucc n) = n. +Proof. +exact Zpred'_succ'. +Qed. + +Theorem NZinduction : + forall A : Z -> Prop, predicate_wd NZeq A -> + A 0 -> (forall n : Z, A n <-> A (NZsucc n)) -> forall n : Z, A n. +Proof. +intros A A_wd A0 AS n; apply Zind; clear n. +assumption. +intros; now apply -> AS. +intros n H. rewrite <- (Zsucc'_pred' n) in H. now apply <- AS. +Qed. + +Theorem NZadd_0_l : forall n : Z, 0 + n = n. +Proof. +exact Zplus_0_l. +Qed. + +Theorem NZadd_succ_l : forall n m : Z, (NZsucc n) + m = NZsucc (n + m). +Proof. +intros; do 2 rewrite <- Zsucc_succ'; apply Zplus_succ_l. +Qed. + +Theorem NZsub_0_r : forall n : Z, n - 0 = n. +Proof. +exact Zminus_0_r. +Qed. + +Theorem NZsub_succ_r : forall n m : Z, n - (NZsucc m) = NZpred (n - m). +Proof. +intros; rewrite <- Zsucc_succ'; rewrite <- Zpred_pred'; +apply Zminus_succ_r. +Qed. + +Theorem NZmul_0_l : forall n : Z, 0 * n = 0. +Proof. +reflexivity. +Qed. + +Theorem NZmul_succ_l : forall n m : Z, (NZsucc n) * m = n * m + m. +Proof. +intros; rewrite <- Zsucc_succ'; apply Zmult_succ_l. +Qed. + +End NZAxiomsMod. + +Definition NZlt := Zlt. +Definition NZle := Zle. +Definition NZmin := Zmin. +Definition NZmax := Zmax. + +Add Morphism NZlt with signature NZeq ==> NZeq ==> iff as NZlt_wd. +Proof. +unfold NZeq. intros n1 n2 H1 m1 m2 H2; rewrite H1; now rewrite H2. +Qed. + +Add Morphism NZle with signature NZeq ==> NZeq ==> iff as NZle_wd. +Proof. +unfold NZeq. intros n1 n2 H1 m1 m2 H2; rewrite H1; now rewrite H2. +Qed. + +Add Morphism NZmin with signature NZeq ==> NZeq ==> NZeq as NZmin_wd. +Proof. +congruence. +Qed. + +Add Morphism NZmax with signature NZeq ==> NZeq ==> NZeq as NZmax_wd. +Proof. +congruence. +Qed. + +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. +Qed. + +Theorem NZlt_irrefl : forall n : Z, ~ n < n. +Proof. +exact Zlt_irrefl. +Qed. + +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]. +Qed. + +Theorem NZmin_l : forall n m : NZ, n <= m -> NZmin n m = n. +Proof. +unfold NZmin, Zmin, Zle; intros n m H. +destruct (n ?= m); try reflexivity. now elim H. +Qed. + +Theorem NZmin_r : forall n m : NZ, m <= n -> NZmin n m = m. +Proof. +unfold NZmin, Zmin, Zle; intros n m H. +case_eq (n ?= m); intro H1; try reflexivity. +now apply Zcompare_Eq_eq. +apply <- Zcompare_Gt_Lt_antisym in H1. now elim H. +Qed. + +Theorem NZmax_l : forall n m : NZ, m <= n -> NZmax n m = n. +Proof. +unfold NZmax, Zmax, Zle; intros n m H. +case_eq (n ?= m); intro H1; try reflexivity. +apply <- Zcompare_Gt_Lt_antisym in H1. now elim H. +Qed. + +Theorem NZmax_r : forall n m : NZ, n <= m -> NZmax n m = m. +Proof. +unfold NZmax, Zmax, Zle; intros n m H. +case_eq (n ?= m); intro H1. +now apply Zcompare_Eq_eq. reflexivity. now elim H. +Qed. + +End NZOrdAxiomsMod. + +Definition Zopp (x : Z) := +match x with +| Z0 => Z0 +| Zpos x => Zneg x +| Zneg x => Zpos x +end. + +Add Morphism Zopp with signature NZeq ==> NZeq as Zopp_wd. +Proof. +congruence. +Qed. + +Theorem Zsucc_pred : forall n : Z, NZsucc (NZpred n) = n. +Proof. +exact Zsucc'_pred'. +Qed. + +Theorem Zopp_0 : - 0 = 0. +Proof. +reflexivity. +Qed. + +Theorem Zopp_succ : forall n : Z, - (NZsucc n) = NZpred (- n). +Proof. +intro; rewrite <- Zsucc_succ'; rewrite <- Zpred_pred'. apply Zopp_succ. +Qed. + +End ZBinAxiomsMod. + +Module Export ZBinMulOrderPropMod := ZMulOrderPropFunct ZBinAxiomsMod. + +(** Z forms a ring *) + +(*Lemma Zring : ring_theory 0 1 NZadd NZmul NZsub Zopp NZeq. +Proof. +constructor. +exact Zadd_0_l. +exact Zadd_comm. +exact Zadd_assoc. +exact Zmul_1_l. +exact Zmul_comm. +exact Zmul_assoc. +exact Zmul_add_distr_r. +intros; now rewrite Zadd_opp_minus. +exact Zadd_opp_r. +Qed. + +Add Ring ZR : Zring.*) + + + +(* +Theorem eq_equiv_e : forall x y : Z, E x y <-> e x y. +Proof. +intros x y; unfold E, e, Zeq_bool; split; intro H. +rewrite H; now rewrite Zcompare_refl. +rewrite eq_true_unfold_pos in H. +assert (H1 : (x ?= y) = Eq). +case_eq (x ?= y); intro H1; rewrite H1 in H; simpl in H; +[reflexivity | discriminate H | discriminate H]. +now apply Zcompare_Eq_eq. +Qed. +*) diff --git a/theories/Numbers/Integer/NatPairs/ZNatPairs.v b/theories/Numbers/Integer/NatPairs/ZNatPairs.v new file mode 100644 index 00000000..8b3d815d --- /dev/null +++ b/theories/Numbers/Integer/NatPairs/ZNatPairs.v @@ -0,0 +1,422 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +(* Evgeny Makarov, INRIA, 2007 *) +(************************************************************************) + +(*i $Id: ZNatPairs.v 11040 2008-06-03 00:04:16Z letouzey $ i*) + +Require Import NSub. (* The most complete file for natural numbers *) +Require Export ZMulOrder. (* The most complete file for integers *) +Require Export Ring. + +Module ZPairsAxiomsMod (Import NAxiomsMod : NAxiomsSig) <: ZAxiomsSig. +Module Import NPropMod := NSubPropFunct NAxiomsMod. (* Get all properties of natural numbers *) + +(* We do not declare ring in Natural/Abstract for two reasons. First, some +of the properties proved in NAdd and NMul are used in the new BinNat, +and it is in turn used in Ring. Using ring in Natural/Abstract would be +circular. It is possible, however, not to make BinNat dependent on +Numbers/Natural and prove the properties necessary for ring from scratch +(this is, of course, how it used to be). In addition, if we define semiring +structures in the implementation subdirectories of Natural, we are able to +specify binary natural numbers as the type of coefficients. For these +reasons we define an abstract semiring here. *) + +Open Local Scope NatScope. + +Lemma Nsemi_ring : semi_ring_theory 0 1 add mul Neq. +Proof. +constructor. +exact add_0_l. +exact add_comm. +exact add_assoc. +exact mul_1_l. +exact mul_0_l. +exact mul_comm. +exact mul_assoc. +exact mul_add_distr_r. +Qed. + +Add Ring NSR : Nsemi_ring. + +(* The definitios of functions (NZadd, NZmul, etc.) will be unfolded by +the properties functor. Since we don't want Zadd_comm to refer to unfolded +definitions of equality: fun p1 p2 : NZ => (fst p1 + snd p2) = (fst p2 + snd p1), +we will provide an extra layer of definitions. *) + +Definition Z := (N * N)%type. +Definition Z0 : Z := (0, 0). +Definition Zeq (p1 p2 : Z) := ((fst p1) + (snd p2) == (fst p2) + (snd p1)). +Definition Zsucc (n : Z) : Z := (S (fst n), snd n). +Definition Zpred (n : Z) : Z := (fst n, S (snd n)). + +(* We do not have Zpred (Zsucc n) = n but only Zpred (Zsucc n) == n. It +could be possible to consider as canonical only pairs where one of the +elements is 0, and make all operations convert canonical values into other +canonical values. In that case, we could get rid of setoids and arrive at +integers as signed natural numbers. *) + +Definition Zadd (n m : Z) : Z := ((fst n) + (fst m), (snd n) + (snd m)). +Definition Zsub (n m : Z) : Z := ((fst n) + (snd m), (snd n) + (fst m)). + +(* Unfortunately, the elements of the pair keep increasing, even during +subtraction *) + +Definition Zmul (n m : Z) : Z := + ((fst n) * (fst m) + (snd n) * (snd m), (fst n) * (snd m) + (snd n) * (fst m)). +Definition Zlt (n m : Z) := (fst n) + (snd m) < (fst m) + (snd n). +Definition Zle (n m : Z) := (fst n) + (snd m) <= (fst m) + (snd n). +Definition Zmin (n m : Z) := (min ((fst n) + (snd m)) ((fst m) + (snd n)), (snd n) + (snd m)). +Definition Zmax (n m : Z) := (max ((fst n) + (snd m)) ((fst m) + (snd n)), (snd n) + (snd m)). + +Delimit Scope IntScope with Int. +Bind Scope IntScope with Z. +Notation "x == y" := (Zeq x y) (at level 70) : IntScope. +Notation "x ~= y" := (~ Zeq x y) (at level 70) : IntScope. +Notation "0" := Z0 : IntScope. +Notation "1" := (Zsucc Z0) : IntScope. +Notation "x + y" := (Zadd x y) : IntScope. +Notation "x - y" := (Zsub x y) : IntScope. +Notation "x * y" := (Zmul x y) : IntScope. +Notation "x < y" := (Zlt x y) : IntScope. +Notation "x <= y" := (Zle x y) : IntScope. +Notation "x > y" := (Zlt y x) (only parsing) : IntScope. +Notation "x >= y" := (Zle y x) (only parsing) : IntScope. + +Notation Local N := NZ. +(* To remember N without having to use a long qualifying name. since NZ will be redefined *) +Notation Local NE := NZeq (only parsing). +Notation Local add_wd := NZadd_wd (only parsing). + +Module Export NZOrdAxiomsMod <: NZOrdAxiomsSig. +Module Export NZAxiomsMod <: NZAxiomsSig. + +Definition NZ : Type := Z. +Definition NZeq := Zeq. +Definition NZ0 := Z0. +Definition NZsucc := Zsucc. +Definition NZpred := Zpred. +Definition NZadd := Zadd. +Definition NZsub := Zsub. +Definition NZmul := Zmul. + +Theorem ZE_refl : reflexive Z Zeq. +Proof. +unfold reflexive, Zeq. reflexivity. +Qed. + +Theorem ZE_symm : symmetric Z Zeq. +Proof. +unfold symmetric, Zeq; now symmetry. +Qed. + +Theorem ZE_trans : transitive Z Zeq. +Proof. +unfold transitive, Zeq. intros n m p H1 H2. +assert (H3 : (fst n + snd m) + (fst m + snd p) == (fst m + snd n) + (fst p + snd m)) +by now apply add_wd. +stepl ((fst n + snd p) + (fst m + snd m)) in H3 by ring. +stepr ((fst p + snd n) + (fst m + snd m)) in H3 by ring. +now apply -> add_cancel_r in H3. +Qed. + +Theorem NZeq_equiv : equiv Z Zeq. +Proof. +unfold equiv; repeat split; [apply ZE_refl | apply ZE_trans | apply ZE_symm]. +Qed. + +Add Relation Z Zeq + reflexivity proved by (proj1 NZeq_equiv) + symmetry proved by (proj2 (proj2 NZeq_equiv)) + transitivity proved by (proj1 (proj2 NZeq_equiv)) +as NZeq_rel. + +Add Morphism (@pair N N) with signature NE ==> NE ==> Zeq as Zpair_wd. +Proof. +intros n1 n2 H1 m1 m2 H2; unfold Zeq; simpl; rewrite H1; now rewrite H2. +Qed. + +Add Morphism NZsucc with signature Zeq ==> Zeq as NZsucc_wd. +Proof. +unfold NZsucc, Zeq; intros n m H; simpl. +do 2 rewrite add_succ_l; now rewrite H. +Qed. + +Add Morphism NZpred with signature Zeq ==> Zeq as NZpred_wd. +Proof. +unfold NZpred, Zeq; intros n m H; simpl. +do 2 rewrite add_succ_r; now rewrite H. +Qed. + +Add Morphism NZadd with signature Zeq ==> Zeq ==> Zeq as NZadd_wd. +Proof. +unfold Zeq, NZadd; intros n1 m1 H1 n2 m2 H2; simpl. +assert (H3 : (fst n1 + snd m1) + (fst n2 + snd m2) == (fst m1 + snd n1) + (fst m2 + snd n2)) +by now apply add_wd. +stepl (fst n1 + snd m1 + (fst n2 + snd m2)) by ring. +now stepr (fst m1 + snd n1 + (fst m2 + snd n2)) by ring. +Qed. + +Add Morphism NZsub with signature Zeq ==> Zeq ==> Zeq as NZsub_wd. +Proof. +unfold Zeq, NZsub; intros n1 m1 H1 n2 m2 H2; simpl. +symmetry in H2. +assert (H3 : (fst n1 + snd m1) + (fst m2 + snd n2) == (fst m1 + snd n1) + (fst n2 + snd m2)) +by now apply add_wd. +stepl (fst n1 + snd m1 + (fst m2 + snd n2)) by ring. +now stepr (fst m1 + snd n1 + (fst n2 + snd m2)) by ring. +Qed. + +Add Morphism NZmul with signature Zeq ==> Zeq ==> Zeq as NZmul_wd. +Proof. +unfold NZmul, Zeq; intros n1 m1 H1 n2 m2 H2; simpl. +stepl (fst n1 * fst n2 + (snd n1 * snd n2 + fst m1 * snd m2 + snd m1 * fst m2)) by ring. +stepr (fst n1 * snd n2 + (fst m1 * fst m2 + snd m1 * snd m2 + snd n1 * fst n2)) by ring. +apply add_mul_repl_pair with (n := fst m2) (m := snd m2); [| now idtac]. +stepl (snd n1 * snd n2 + (fst n1 * fst m2 + fst m1 * snd m2 + snd m1 * fst m2)) by ring. +stepr (snd n1 * fst n2 + (fst n1 * snd m2 + fst m1 * fst m2 + snd m1 * snd m2)) by ring. +apply add_mul_repl_pair with (n := snd m2) (m := fst m2); +[| (stepl (fst n2 + snd m2) by ring); now stepr (fst m2 + snd n2) by ring]. +stepl (snd m2 * snd n1 + (fst n1 * fst m2 + fst m1 * snd m2 + snd m1 * fst m2)) by ring. +stepr (snd m2 * fst n1 + (snd n1 * fst m2 + fst m1 * fst m2 + snd m1 * snd m2)) by ring. +apply add_mul_repl_pair with (n := snd m1) (m := fst m1); +[ | (stepl (fst n1 + snd m1) by ring); now stepr (fst m1 + snd n1) by ring]. +stepl (fst m2 * fst n1 + (snd m2 * snd m1 + fst m1 * snd m2 + snd m1 * fst m2)) by ring. +stepr (fst m2 * snd n1 + (snd m2 * fst m1 + fst m1 * fst m2 + snd m1 * snd m2)) by ring. +apply add_mul_repl_pair with (n := fst m1) (m := snd m1); [| now idtac]. +ring. +Qed. + +Section Induction. +Open Scope NatScope. (* automatically closes at the end of the section *) +Variable A : Z -> Prop. +Hypothesis A_wd : predicate_wd Zeq A. + +Add Morphism A with signature Zeq ==> iff as A_morph. +Proof. +exact A_wd. +Qed. + +Theorem NZinduction : + A 0 -> (forall n : Z, A n <-> A (Zsucc n)) -> forall n : Z, A n. (* 0 is interpreted as in Z due to "Bind" directive *) +Proof. +intros A0 AS n; unfold NZ0, Zsucc, predicate_wd, fun_wd, Zeq in *. +destruct n as [n m]. +cut (forall p : N, A (p, 0)); [intro H1 |]. +cut (forall p : N, A (0, p)); [intro H2 |]. +destruct (add_dichotomy n m) as [[p H] | [p H]]. +rewrite (A_wd (n, m) (0, p)) by (rewrite add_0_l; now rewrite add_comm). +apply H2. +rewrite (A_wd (n, m) (p, 0)) by now rewrite add_0_r. apply H1. +induct p. assumption. intros p IH. +apply -> (A_wd (0, p) (1, S p)) in IH; [| now rewrite add_0_l, add_1_l]. +now apply <- AS. +induct p. assumption. intros p IH. +replace 0 with (snd (p, 0)); [| reflexivity]. +replace (S p) with (S (fst (p, 0))); [| reflexivity]. now apply -> AS. +Qed. + +End Induction. + +(* Time to prove theorems in the language of Z *) + +Open Local Scope IntScope. + +Theorem NZpred_succ : forall n : Z, Zpred (Zsucc n) == n. +Proof. +unfold NZpred, NZsucc, Zeq; intro n; simpl. +rewrite add_succ_l; now rewrite add_succ_r. +Qed. + +Theorem NZadd_0_l : forall n : Z, 0 + n == n. +Proof. +intro n; unfold NZadd, Zeq; simpl. now do 2 rewrite add_0_l. +Qed. + +Theorem NZadd_succ_l : forall n m : Z, (Zsucc n) + m == Zsucc (n + m). +Proof. +intros n m; unfold NZadd, Zeq; simpl. now do 2 rewrite add_succ_l. +Qed. + +Theorem NZsub_0_r : forall n : Z, n - 0 == n. +Proof. +intro n; unfold NZsub, Zeq; simpl. now do 2 rewrite add_0_r. +Qed. + +Theorem NZsub_succ_r : forall n m : Z, n - (Zsucc m) == Zpred (n - m). +Proof. +intros n m; unfold NZsub, Zeq; simpl. symmetry; now rewrite add_succ_r. +Qed. + +Theorem NZmul_0_l : forall n : Z, 0 * n == 0. +Proof. +intro n; unfold NZmul, Zeq; simpl. +repeat rewrite mul_0_l. now rewrite add_assoc. +Qed. + +Theorem NZmul_succ_l : forall n m : Z, (Zsucc n) * m == n * m + m. +Proof. +intros n m; unfold NZmul, NZsucc, Zeq; simpl. +do 2 rewrite mul_succ_l. ring. +Qed. + +End NZAxiomsMod. + +Definition NZlt := Zlt. +Definition NZle := Zle. +Definition NZmin := Zmin. +Definition NZmax := Zmax. + +Add Morphism NZlt with signature Zeq ==> Zeq ==> iff as NZlt_wd. +Proof. +unfold NZlt, Zlt, Zeq; intros n1 m1 H1 n2 m2 H2; simpl. split; intro H. +stepr (snd m1 + fst m2) by apply add_comm. +apply (add_lt_repl_pair (fst n1) (snd n1)); [| assumption]. +stepl (snd m2 + fst n1) by apply add_comm. +stepr (fst m2 + snd n1) by apply add_comm. +apply (add_lt_repl_pair (snd n2) (fst n2)). +now stepl (fst n1 + snd n2) by apply add_comm. +stepl (fst m2 + snd n2) by apply add_comm. now stepr (fst n2 + snd m2) by apply add_comm. +stepr (snd n1 + fst n2) by apply add_comm. +apply (add_lt_repl_pair (fst m1) (snd m1)); [| now symmetry]. +stepl (snd n2 + fst m1) by apply add_comm. +stepr (fst n2 + snd m1) by apply add_comm. +apply (add_lt_repl_pair (snd m2) (fst m2)). +now stepl (fst m1 + snd m2) by apply add_comm. +stepl (fst n2 + snd m2) by apply add_comm. now stepr (fst m2 + snd n2) by apply add_comm. +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 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. + +Add Morphism NZmin with signature Zeq ==> Zeq ==> Zeq as NZmin_wd. +Proof. +intros n1 m1 H1 n2 m2 H2; unfold NZmin, Zeq; simpl. +destruct (le_ge_cases (fst n1 + snd n2) (fst n2 + snd n1)) as [H | H]. +rewrite (min_l (fst n1 + snd n2) (fst n2 + snd n1)) by assumption. +rewrite (min_l (fst m1 + snd m2) (fst m2 + snd m1)) by +now apply -> (NZle_wd n1 m1 H1 n2 m2 H2). +stepl ((fst n1 + snd m1) + (snd n2 + snd m2)) by ring. +unfold Zeq in H1. rewrite H1. ring. +rewrite (min_r (fst n1 + snd n2) (fst n2 + snd n1)) by assumption. +rewrite (min_r (fst m1 + snd m2) (fst m2 + snd m1)) by +now apply -> (NZle_wd n2 m2 H2 n1 m1 H1). +stepl ((fst n2 + snd m2) + (snd n1 + snd m1)) by ring. +unfold Zeq in H2. rewrite H2. ring. +Qed. + +Add Morphism NZmax with signature Zeq ==> Zeq ==> Zeq as NZmax_wd. +Proof. +intros n1 m1 H1 n2 m2 H2; unfold NZmax, Zeq; simpl. +destruct (le_ge_cases (fst n1 + snd n2) (fst n2 + snd n1)) as [H | H]. +rewrite (max_r (fst n1 + snd n2) (fst n2 + snd n1)) by assumption. +rewrite (max_r (fst m1 + snd m2) (fst m2 + snd m1)) by +now apply -> (NZle_wd n1 m1 H1 n2 m2 H2). +stepl ((fst n2 + snd m2) + (snd n1 + snd m1)) by ring. +unfold Zeq in H2. rewrite H2. ring. +rewrite (max_l (fst n1 + snd n2) (fst n2 + snd n1)) by assumption. +rewrite (max_l (fst m1 + snd m2) (fst m2 + snd m1)) by +now apply -> (NZle_wd n2 m2 H2 n1 m1 H1). +stepl ((fst n1 + snd m1) + (snd n2 + snd m2)) by ring. +unfold Zeq in H1. rewrite H1. ring. +Qed. + +Open Local Scope IntScope. + +Theorem NZlt_eq_cases : forall n m : Z, n <= m <-> n < m \/ n == m. +Proof. +intros n m; unfold Zlt, Zle, Zeq; simpl. apply lt_eq_cases. +Qed. + +Theorem NZlt_irrefl : forall n : Z, ~ (n < n). +Proof. +intros n; unfold Zlt, Zeq; simpl. apply lt_irrefl. +Qed. + +Theorem NZlt_succ_r : forall n m : Z, n < (Zsucc m) <-> n <= m. +Proof. +intros n m; unfold Zlt, Zle, Zeq; simpl. rewrite add_succ_l; apply lt_succ_r. +Qed. + +Theorem NZmin_l : forall n m : Z, n <= m -> Zmin n m == n. +Proof. +unfold Zmin, Zle, Zeq; simpl; intros n m H. +rewrite min_l by assumption. ring. +Qed. + +Theorem NZmin_r : forall n m : Z, m <= n -> Zmin n m == m. +Proof. +unfold Zmin, Zle, Zeq; simpl; intros n m H. +rewrite min_r by assumption. ring. +Qed. + +Theorem NZmax_l : forall n m : Z, m <= n -> Zmax n m == n. +Proof. +unfold Zmax, Zle, Zeq; simpl; intros n m H. +rewrite max_l by assumption. ring. +Qed. + +Theorem NZmax_r : forall n m : Z, n <= m -> Zmax n m == m. +Proof. +unfold Zmax, Zle, Zeq; simpl; intros n m H. +rewrite max_r by assumption. ring. +Qed. + +End NZOrdAxiomsMod. + +Definition Zopp (n : Z) : Z := (snd n, fst n). + +Notation "- x" := (Zopp x) : IntScope. + +Add Morphism Zopp with signature Zeq ==> Zeq as Zopp_wd. +Proof. +unfold Zeq; intros n m H; simpl. symmetry. +stepl (fst n + snd m) by apply add_comm. +now stepr (fst m + snd n) by apply add_comm. +Qed. + +Open Local Scope IntScope. + +Theorem Zsucc_pred : forall n : Z, Zsucc (Zpred n) == n. +Proof. +intro n; unfold Zsucc, Zpred, Zeq; simpl. +rewrite add_succ_l; now rewrite add_succ_r. +Qed. + +Theorem Zopp_0 : - 0 == 0. +Proof. +unfold Zopp, Zeq; simpl. now rewrite add_0_l. +Qed. + +Theorem Zopp_succ : forall n, - (Zsucc n) == Zpred (- n). +Proof. +reflexivity. +Qed. + +End ZPairsAxiomsMod. + +(* For example, let's build integers out of pairs of Peano natural numbers +and get their properties *) + +(* The following lines increase the compilation time at least twice *) +(* +Require Import NPeano. + +Module Export ZPairsPeanoAxiomsMod := ZPairsAxiomsMod NPeanoAxiomsMod. +Module Export ZPairsMulOrderPropMod := ZMulOrderPropFunct ZPairsPeanoAxiomsMod. + +Open Local Scope IntScope. + +Eval compute in (3, 5) * (4, 6). +*) + diff --git a/theories/Numbers/Integer/SpecViaZ/ZSig.v b/theories/Numbers/Integer/SpecViaZ/ZSig.v new file mode 100644 index 00000000..0af98c74 --- /dev/null +++ b/theories/Numbers/Integer/SpecViaZ/ZSig.v @@ -0,0 +1,117 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +(* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) +(************************************************************************) + +(*i $Id: ZSig.v 11027 2008-06-01 13:28:59Z letouzey $ i*) + +Require Import ZArith Znumtheory. + +Open Scope Z_scope. + +(** * ZSig *) + +(** Interface of a rich structure about integers. + Specifications are written via translation to Z. +*) + +Module Type ZType. + + Parameter t : Type. + + Parameter to_Z : t -> Z. + Notation "[ x ]" := (to_Z x). + + Definition eq x y := ([x] = [y]). + + Parameter of_Z : Z -> t. + Parameter spec_of_Z: forall x, to_Z (of_Z x) = x. + + Parameter zero : t. + Parameter one : t. + Parameter minus_one : t. + + Parameter spec_0: [zero] = 0. + Parameter spec_1: [one] = 1. + Parameter spec_m1: [minus_one] = -1. + + Parameter compare : t -> t -> comparison. + + Parameter spec_compare: forall x y, + match compare x y with + | Eq => [x] = [y] + | Lt => [x] < [y] + | Gt => [x] > [y] + end. + + Definition lt n m := compare n m = Lt. + Definition le n m := compare n m <> Gt. + Definition min n m := match compare n m with Gt => m | _ => n end. + Definition max n m := match compare n m with Lt => m | _ => n end. + + Parameter eq_bool : t -> t -> bool. + + Parameter spec_eq_bool: forall x y, + if eq_bool x y then [x] = [y] else [x] <> [y]. + + Parameter succ : t -> t. + + Parameter spec_succ: forall n, [succ n] = [n] + 1. + + Parameter add : t -> t -> t. + + Parameter spec_add: forall x y, [add x y] = [x] + [y]. + + Parameter pred : t -> t. + + Parameter spec_pred: forall x, [pred x] = [x] - 1. + + Parameter sub : t -> t -> t. + + Parameter spec_sub: forall x y, [sub x y] = [x] - [y]. + + Parameter opp : t -> t. + + Parameter spec_opp: forall x, [opp x] = - [x]. + + Parameter mul : t -> t -> t. + + Parameter spec_mul: forall x y, [mul x y] = [x] * [y]. + + Parameter square : t -> t. + + Parameter spec_square: forall x, [square x] = [x] * [x]. + + Parameter power_pos : t -> positive -> t. + + Parameter spec_power_pos: forall x n, [power_pos x n] = [x] ^ Zpos n. + + Parameter sqrt : t -> t. + + Parameter spec_sqrt: forall x, 0 <= [x] -> + [sqrt x] ^ 2 <= [x] < ([sqrt x] + 1) ^ 2. + + Parameter div_eucl : t -> t -> t * t. + + Parameter spec_div_eucl: forall x y, [y] <> 0 -> + let (q,r) := div_eucl x y in ([q], [r]) = Zdiv_eucl [x] [y]. + + Parameter div : t -> t -> t. + + Parameter spec_div: forall x y, [y] <> 0 -> [div x y] = [x] / [y]. + + Parameter modulo : t -> t -> t. + + Parameter spec_modulo: forall x y, [y] <> 0 -> + [modulo x y] = [x] mod [y]. + + Parameter gcd : t -> t -> t. + + Parameter spec_gcd: forall a b, [gcd a b] = Zgcd (to_Z a) (to_Z b). + +End ZType. diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v new file mode 100644 index 00000000..d7c56267 --- /dev/null +++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v @@ -0,0 +1,306 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: ZSigZAxioms.v 11040 2008-06-03 00:04:16Z letouzey $ i*) + +Require Import ZArith. +Require Import ZAxioms. +Require Import ZSig. + +(** * The interface [ZSig.ZType] implies the interface [ZAxiomsSig] *) + +Module ZSig_ZAxioms (Z:ZType) <: ZAxiomsSig. + +Delimit Scope IntScope with Int. +Bind Scope IntScope with Z.t. +Open Local Scope IntScope. +Notation "[ x ]" := (Z.to_Z x) : IntScope. +Infix "==" := Z.eq (at level 70) : IntScope. +Notation "0" := Z.zero : IntScope. +Infix "+" := Z.add : IntScope. +Infix "-" := Z.sub : IntScope. +Infix "*" := Z.mul : IntScope. +Notation "- x" := (Z.opp x) : IntScope. + +Hint Rewrite + Z.spec_0 Z.spec_1 Z.spec_add Z.spec_sub Z.spec_pred Z.spec_succ + Z.spec_mul Z.spec_opp Z.spec_of_Z : Zspec. + +Ltac zsimpl := unfold Z.eq in *; autorewrite with Zspec. + +Module Export NZOrdAxiomsMod <: NZOrdAxiomsSig. +Module Export NZAxiomsMod <: NZAxiomsSig. + +Definition NZ := Z.t. +Definition NZeq := Z.eq. +Definition NZ0 := Z.zero. +Definition NZsucc := Z.succ. +Definition NZpred := Z.pred. +Definition NZadd := Z.add. +Definition NZsub := Z.sub. +Definition NZmul := Z.mul. + +Theorem NZeq_equiv : equiv Z.t Z.eq. +Proof. +repeat split; repeat red; intros; auto; congruence. +Qed. + +Add Relation Z.t Z.eq + reflexivity proved by (proj1 NZeq_equiv) + symmetry proved by (proj2 (proj2 NZeq_equiv)) + transitivity proved by (proj1 (proj2 NZeq_equiv)) + as NZeq_rel. + +Add Morphism NZsucc with signature Z.eq ==> Z.eq as NZsucc_wd. +Proof. +intros; zsimpl; f_equal; assumption. +Qed. + +Add Morphism NZpred with signature Z.eq ==> Z.eq as NZpred_wd. +Proof. +intros; zsimpl; f_equal; assumption. +Qed. + +Add Morphism NZadd with signature Z.eq ==> Z.eq ==> Z.eq as NZadd_wd. +Proof. +intros; zsimpl; f_equal; assumption. +Qed. + +Add Morphism NZsub with signature Z.eq ==> Z.eq ==> Z.eq as NZsub_wd. +Proof. +intros; zsimpl; f_equal; assumption. +Qed. + +Add Morphism NZmul with signature Z.eq ==> Z.eq ==> Z.eq as NZmul_wd. +Proof. +intros; zsimpl; f_equal; assumption. +Qed. + +Theorem NZpred_succ : forall n, Z.pred (Z.succ n) == n. +Proof. +intros; zsimpl; auto with zarith. +Qed. + +Section Induction. + +Variable A : Z.t -> Prop. +Hypothesis A_wd : predicate_wd Z.eq A. +Hypothesis A0 : A 0. +Hypothesis AS : forall n, A n <-> A (Z.succ n). + +Add Morphism A with signature Z.eq ==> iff as A_morph. +Proof. apply A_wd. Qed. + +Let B (z : Z) := A (Z.of_Z z). + +Lemma B0 : B 0. +Proof. +unfold B; simpl. +rewrite <- (A_wd 0); auto. +zsimpl; auto. +Qed. + +Lemma BS : forall z : Z, B z -> B (z + 1). +Proof. +intros z H. +unfold B in *. apply -> AS in H. +setoid_replace (Z.of_Z (z + 1)) with (Z.succ (Z.of_Z z)); auto. +zsimpl; auto. +Qed. + +Lemma BP : forall z : Z, B z -> B (z - 1). +Proof. +intros z H. +unfold B in *. rewrite AS. +setoid_replace (Z.succ (Z.of_Z (z - 1))) with (Z.of_Z z); auto. +zsimpl; auto with zarith. +Qed. + +Lemma B_holds : forall z : Z, B z. +Proof. +intros; destruct (Z_lt_le_dec 0 z). +apply natlike_ind; auto with zarith. +apply B0. +intros; apply BS; auto. +replace z with (-(-z))%Z in * by (auto with zarith). +remember (-z)%Z as z'. +pattern z'; apply natlike_ind. +apply B0. +intros; rewrite Zopp_succ; unfold Zpred; apply BP; auto. +subst z'; auto with zarith. +Qed. + +Theorem NZinduction : forall n, A n. +Proof. +intro n. setoid_replace n with (Z.of_Z (Z.to_Z n)). +apply B_holds. +zsimpl; auto. +Qed. + +End Induction. + +Theorem NZadd_0_l : forall n, 0 + n == n. +Proof. +intros; zsimpl; auto with zarith. +Qed. + +Theorem NZadd_succ_l : forall n m, (Z.succ n) + m == Z.succ (n + m). +Proof. +intros; zsimpl; auto with zarith. +Qed. + +Theorem NZsub_0_r : forall n, n - 0 == n. +Proof. +intros; zsimpl; auto with zarith. +Qed. + +Theorem NZsub_succ_r : forall n m, n - (Z.succ m) == Z.pred (n - m). +Proof. +intros; zsimpl; auto with zarith. +Qed. + +Theorem NZmul_0_l : forall n, 0 * n == 0. +Proof. +intros; zsimpl; auto with zarith. +Qed. + +Theorem NZmul_succ_l : forall n m, (Z.succ n) * m == n * m + m. +Proof. +intros; zsimpl; ring. +Qed. + +End NZAxiomsMod. + +Definition NZlt := Z.lt. +Definition NZle := Z.le. +Definition NZmin := Z.min. +Definition NZmax := Z.max. + +Infix "<=" := Z.le : IntScope. +Infix "<" := Z.lt : IntScope. + +Lemma spec_compare_alt : forall x y, Z.compare x y = ([x] ?= [y])%Z. +Proof. + intros; generalize (Z.spec_compare x y). + destruct (Z.compare x y); auto. + intros H; rewrite H; symmetry; apply Zcompare_refl. +Qed. + +Lemma spec_lt : forall x y, (x<y) <-> ([x]<[y])%Z. +Proof. + intros; unfold Z.lt, Zlt; rewrite spec_compare_alt; intuition. +Qed. + +Lemma spec_le : forall x y, (x<=y) <-> ([x]<=[y])%Z. +Proof. + intros; unfold Z.le, Zle; rewrite spec_compare_alt; intuition. +Qed. + +Lemma spec_min : forall x y, [Z.min x y] = Zmin [x] [y]. +Proof. + intros; unfold Z.min, Zmin. + rewrite spec_compare_alt; destruct Zcompare; auto. +Qed. + +Lemma spec_max : forall x y, [Z.max x y] = Zmax [x] [y]. +Proof. + intros; unfold Z.max, Zmax. + rewrite spec_compare_alt; destruct Zcompare; auto. +Qed. + +Add Morphism Z.compare with signature Z.eq ==> Z.eq ==> (@eq comparison) as compare_wd. +Proof. +intros x x' Hx y y' Hy. +rewrite 2 spec_compare_alt; rewrite Hx, Hy; intuition. +Qed. + +Add Morphism Z.lt with signature Z.eq ==> Z.eq ==> iff as NZlt_wd. +Proof. +intros x x' Hx y y' Hy; unfold Z.lt; rewrite Hx, Hy; intuition. +Qed. + +Add Morphism Z.le with signature Z.eq ==> Z.eq ==> iff as NZle_wd. +Proof. +intros x x' Hx y y' Hy; unfold Z.le; rewrite Hx, Hy; intuition. +Qed. + +Add Morphism Z.min with signature Z.eq ==> Z.eq ==> Z.eq as NZmin_wd. +Proof. +intros; red; rewrite 2 spec_min; congruence. +Qed. + +Add Morphism Z.max with signature Z.eq ==> Z.eq ==> Z.eq as NZmax_wd. +Proof. +intros; red; rewrite 2 spec_max; congruence. +Qed. + +Theorem NZlt_eq_cases : forall n m, n <= m <-> n < m \/ n == m. +Proof. +intros. +unfold Z.eq; rewrite spec_lt, spec_le; omega. +Qed. + +Theorem NZlt_irrefl : forall n, ~ n < n. +Proof. +intros; rewrite spec_lt; auto with zarith. +Qed. + +Theorem NZlt_succ_r : forall n m, n < (Z.succ m) <-> n <= m. +Proof. +intros; rewrite spec_lt, spec_le, Z.spec_succ; omega. +Qed. + +Theorem NZmin_l : forall n m, n <= m -> Z.min n m == n. +Proof. +intros n m; unfold Z.eq; rewrite spec_le, spec_min. +generalize (Zmin_spec [n] [m]); omega. +Qed. + +Theorem NZmin_r : forall n m, m <= n -> Z.min n m == m. +Proof. +intros n m; unfold Z.eq; rewrite spec_le, spec_min. +generalize (Zmin_spec [n] [m]); omega. +Qed. + +Theorem NZmax_l : forall n m, m <= n -> Z.max n m == n. +Proof. +intros n m; unfold Z.eq; rewrite spec_le, spec_max. +generalize (Zmax_spec [n] [m]); omega. +Qed. + +Theorem NZmax_r : forall n m, n <= m -> Z.max n m == m. +Proof. +intros n m; unfold Z.eq; rewrite spec_le, spec_max. +generalize (Zmax_spec [n] [m]); omega. +Qed. + +End NZOrdAxiomsMod. + +Definition Zopp := Z.opp. + +Add Morphism Z.opp with signature Z.eq ==> Z.eq as Zopp_wd. +Proof. +intros; zsimpl; auto with zarith. +Qed. + +Theorem Zsucc_pred : forall n, Z.succ (Z.pred n) == n. +Proof. +red; intros; zsimpl; auto with zarith. +Qed. + +Theorem Zopp_0 : - 0 == 0. +Proof. +red; intros; zsimpl; auto with zarith. +Qed. + +Theorem Zopp_succ : forall n, - (Z.succ n) == Z.pred (- n). +Proof. +intros; zsimpl; auto with zarith. +Qed. + +End ZSig_ZAxioms. |