diff options
Diffstat (limited to 'theories/Numbers')
32 files changed, 422 insertions, 422 deletions
diff --git a/theories/Numbers/Cyclic/Abstract/NZCyclic.v b/theories/Numbers/Cyclic/Abstract/NZCyclic.v index 113945e0d..92ada3d74 100644 --- a/theories/Numbers/Cyclic/Abstract/NZCyclic.v +++ b/theories/Numbers/Cyclic/Abstract/NZCyclic.v @@ -40,7 +40,7 @@ Definition NZ0 := w_op.(znz_0). Definition NZsucc := w_op.(znz_succ). Definition NZpred := w_op.(znz_pred). Definition NZadd := w_op.(znz_add). -Definition NZminus := w_op.(znz_sub). +Definition NZsub := w_op.(znz_sub). Definition NZmul := w_op.(znz_mul). Theorem NZeq_equiv : equiv NZ NZeq. @@ -71,7 +71,7 @@ unfold NZeq; intros n1 n2 H1 m1 m2 H2. do 2 rewrite w_spec.(spec_add). now rewrite H1, H2. Qed. -Add Morphism NZminus with signature NZeq ==> NZeq ==> NZeq as NZminus_wd. +Add Morphism NZsub with signature NZeq ==> NZeq ==> NZeq as NZsub_wd. Proof. unfold NZeq; intros n1 n2 H1 m1 m2 H2. do 2 rewrite w_spec.(spec_sub). now rewrite H1, H2. @@ -93,7 +93,7 @@ Notation "'S'" := NZsucc : IntScope. Notation "'P'" := NZpred : IntScope. (*Notation "1" := (S 0) : IntScope.*) Notation "x + y" := (NZadd x y) : IntScope. -Notation "x - y" := (NZminus x y) : IntScope. +Notation "x - y" := (NZsub x y) : IntScope. Notation "x * y" := (NZmul x y) : IntScope. Theorem gt_wB_1 : 1 < wB. @@ -204,15 +204,15 @@ rewrite <- (Zplus_assoc ([| n |] mod wB) 1 [| m |]). rewrite Zplus_mod_idemp_l. rewrite (Zplus_comm 1 [| m |]); now rewrite Zplus_assoc. Qed. -Theorem NZminus_0_r : forall n : NZ, n - 0 == n. +Theorem NZsub_0_r : forall n : NZ, n - 0 == n. Proof. -intro n; unfold NZminus, NZ0, NZeq. rewrite w_spec.(spec_sub). +intro n; unfold NZsub, NZ0, NZeq. rewrite w_spec.(spec_sub). rewrite w_spec.(spec_0). rewrite Zminus_0_r. apply NZ_to_Z_mod. Qed. -Theorem NZminus_succ_r : forall n m : NZ, n - (S m) == P (n - m). +Theorem NZsub_succ_r : forall n m : NZ, n - (S m) == P (n - m). Proof. -intros n m; unfold NZminus, NZsucc, NZpred, NZeq. +intros n m; unfold NZsub, NZsucc, NZpred, NZeq. rewrite w_spec.(spec_pred). do 2 rewrite w_spec.(spec_sub). rewrite w_spec.(spec_succ). rewrite Zminus_mod_idemp_r. rewrite Zminus_mod_idemp_l. diff --git a/theories/Numbers/Integer/Abstract/ZPlus.v b/theories/Numbers/Integer/Abstract/ZAdd.v index d72d00379..daa7c530b 100644 --- a/theories/Numbers/Integer/Abstract/ZPlus.v +++ b/theories/Numbers/Integer/Abstract/ZAdd.v @@ -12,7 +12,7 @@ Require Export ZBase. -Module ZPlusPropFunct (Import ZAxiomsMod : ZAxiomsSig). +Module ZAddPropFunct (Import ZAxiomsMod : ZAxiomsSig). Module Export ZBasePropMod := ZBasePropFunct ZAxiomsMod. Open Local Scope IntScope. @@ -26,11 +26,11 @@ Proof NZadd_0_l. Theorem Zadd_succ_l : forall n m : Z, (S n) + m == S (n + m). Proof NZadd_succ_l. -Theorem Zminus_0_r : forall n : Z, n - 0 == n. -Proof NZminus_0_r. +Theorem Zsub_0_r : forall n : Z, n - 0 == n. +Proof NZsub_0_r. -Theorem Zminus_succ_r : forall n m : Z, n - (S m) == P (n - m). -Proof NZminus_succ_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. @@ -88,30 +88,30 @@ Qed. Theorem Zadd_opp_r : forall n m : Z, n + (- m) == n - m. Proof. NZinduct m. -rewrite Zopp_0; rewrite Zminus_0_r; now rewrite Zadd_0_r. -intro m. rewrite Zopp_succ, Zminus_succ_r, Zadd_pred_r; now rewrite Zpred_inj_wd. +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 Zminus_0_l : forall n : Z, 0 - n == - n. +Theorem Zsub_0_l : forall n : Z, 0 - n == - n. Proof. intro n; rewrite <- Zadd_opp_r; now rewrite Zadd_0_l. Qed. -Theorem Zminus_succ_l : forall n m : Z, S n - m == S (n - m). +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 Zminus_pred_l : forall n m : Z, P n - m == P (n - m). +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 Zminus_succ_l; now rewrite Zpred_succ. +rewrite Zsub_succ_l; now rewrite Zpred_succ. Qed. -Theorem Zminus_pred_r : forall n m : Z, n - (P m) == S (n - m). +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 Zminus_succ_r; now rewrite Zsucc_pred. +rewrite Zsub_succ_r; now rewrite Zsucc_pred. Qed. Theorem Zopp_pred : forall n : Z, - (P n) == S (- n). @@ -120,16 +120,16 @@ intro n. rewrite <- (Zsucc_pred n) at 2. rewrite Zopp_succ. now rewrite Zsucc_pred. Qed. -Theorem Zminus_diag : forall n : Z, n - n == 0. +Theorem Zsub_diag : forall n : Z, n - n == 0. Proof. NZinduct n. -now rewrite Zminus_0_r. -intro n. rewrite Zminus_succ_r, Zminus_succ_l; now rewrite Zpred_succ. +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, Zminus_diag. +intro n; now rewrite Zadd_comm, Zadd_opp_r, Zsub_diag. Qed. Theorem Zadd_opp_diag_r : forall n : Z, n + (- n) == 0. @@ -142,7 +142,7 @@ Proof. intros n m; rewrite <- Zadd_opp_r; now rewrite Zadd_comm. Qed. -Theorem Zadd_minus_assoc : forall n m p : Z, n + (m - p) == (n + m) - p. +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. @@ -162,7 +162,7 @@ intro n. rewrite Zadd_succ_l; do 2 rewrite Zopp_succ; rewrite Zadd_pred_l. now rewrite Zpred_inj_wd. Qed. -Theorem Zopp_minus_distr : forall n m : Z, - (n - m) == - n + m. +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. @@ -188,58 +188,58 @@ Proof. symmetry; apply Zeq_opp_l. Qed. -Theorem Zminus_add_distr : forall n m p : Z, n - (m + p) == (n - m) - p. +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 Zminus_minus_distr : forall n m p : Z, n - (m - p) == (n - m) + p. +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_minus_distr, Zadd_assoc. +intros n m p; rewrite <- Zadd_opp_r, Zopp_sub_distr, Zadd_assoc. now rewrite Zadd_opp_r. Qed. -Theorem minus_opp_l : forall n m : Z, - n - m == - m - n. +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 Zminus_opp_r : forall n m : Z, n - (- m) == n + m. +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_minus_swap : forall n m p : Z, n + m - p == n - p + m. +Theorem Zadd_sub_swap : forall n m p : Z, n + m - p == n - p + m. Proof. -intros n m p. rewrite <- Zadd_minus_assoc, <- (Zadd_opp_r n p), <- Zadd_assoc. +intros n m p. rewrite <- Zadd_sub_assoc, <- (Zadd_opp_r n p), <- Zadd_assoc. now rewrite Zadd_opp_l. Qed. -Theorem Zminus_cancel_l : forall n m p : Z, n - m == n - p <-> m == p. +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_minus_assoc. rewrite Zadd_opp_diag_l; do 2 rewrite Zminus_0_l. +do 2 rewrite Zadd_sub_assoc. rewrite Zadd_opp_diag_l; do 2 rewrite Zsub_0_l. apply Zopp_inj_wd. Qed. -Theorem Zminus_cancel_r : forall n m p : Z, n - p == m - p <-> n == m. +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 <- Zminus_minus_distr, Zminus_diag, Zminus_0_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 minus) and the indication whether the left or right term +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 Zminus_cancel_r. -now rewrite Zadd_comm, <- Zadd_minus_assoc, Zminus_diag, Zadd_0_r. +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. @@ -251,34 +251,34 @@ Qed. n - m == p to n == p + m since subtraction is in the right-hand side of the equation. Hence the following two theorems. *) -Theorem Zminus_move_l : forall n m p : Z, n - m == p <-> - m == p - n. +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 Zminus_move_r : forall n m p : Z, n - m == p <-> n == p + m. +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, Zminus_opp_r. +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, Zminus_0_l. +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, Zminus_0_l. +intros n m; now rewrite Zadd_move_r, Zsub_0_l. Qed. -Theorem Zminus_move_0_l : forall n m : Z, n - m == 0 <-> - m == - n. +Theorem Zsub_move_0_l : forall n m : Z, n - m == 0 <-> - m == - n. Proof. -intros n m. now rewrite Zminus_move_l, Zminus_0_l. +intros n m. now rewrite Zsub_move_l, Zsub_0_l. Qed. -Theorem Zminus_move_0_r : forall n m : Z, n - m == 0 <-> n == m. +Theorem Zsub_move_0_r : forall n m : Z, n - m == 0 <-> n == m. Proof. -intros n m. now rewrite Zminus_move_r, Zadd_0_l. +intros n m. now rewrite Zsub_move_r, Zadd_0_l. Qed. (* The following section is devoted to cancellation of like terms. The name @@ -286,22 +286,22 @@ 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_minus_swap, Zminus_diag, Zadd_0_l. +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_minus_assoc, Zminus_diag, Zadd_0_r. +intros; now rewrite <- Zadd_sub_assoc, Zsub_diag, Zadd_0_r. Qed. -Theorem Zminus_simpl_l : forall n m : Z, - n - m + n == - m. +Theorem Zsub_simpl_l : forall n m : Z, - n - m + n == - m. Proof. -intros; now rewrite <- Zadd_minus_swap, Zadd_opp_diag_l, Zminus_0_l. +intros; now rewrite <- Zadd_sub_swap, Zadd_opp_diag_l, Zsub_0_l. Qed. -Theorem Zminus_simpl_r : forall n m : Z, n - m + m == n. +Theorem Zsub_simpl_r : forall n m : Z, n - m + m == n. Proof. -intros; now rewrite <- Zminus_minus_distr, Zminus_diag, Zminus_0_r. +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 @@ -309,8 +309,8 @@ 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_minus_assoc, -Zminus_add_distr, Zminus_diag, Zminus_0_l, Zadd_opp_r. +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. @@ -328,18 +328,18 @@ Proof. intros n m p. rewrite (Zadd_comm p m); apply Zadd_add_simpl_r_l. Qed. -Theorem Zminus_add_simpl_r_l : forall n m p : Z, (n - m) + (m + p) == n + p. +Theorem Zsub_add_simpl_r_l : forall n m p : Z, (n - m) + (m + p) == n + p. Proof. -intros n m p. now rewrite <- Zminus_minus_distr, Zminus_add_distr, Zminus_diag, -Zminus_0_l, Zminus_opp_r. +intros n m p. now rewrite <- Zsub_sub_distr, Zsub_add_distr, Zsub_diag, +Zsub_0_l, Zsub_opp_r. Qed. -Theorem Zminus_add_simpl_r_r : forall n m p : Z, (n - m) + (p + m) == n + p. +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 Zminus_add_simpl_r_l. +intros n m p. rewrite (Zadd_comm p m); apply Zsub_add_simpl_r_l. Qed. (* Of course, there are many other variants *) -End ZPlusPropFunct. +End ZAddPropFunct. diff --git a/theories/Numbers/Integer/Abstract/ZPlusOrder.v b/theories/Numbers/Integer/Abstract/ZAddOrder.v index 85f671498..917e3fc12 100644 --- a/theories/Numbers/Integer/Abstract/ZPlusOrder.v +++ b/theories/Numbers/Integer/Abstract/ZAddOrder.v @@ -12,7 +12,7 @@ Require Export ZLt. -Module ZPlusOrderPropFunct (Import ZAxiomsMod : ZAxiomsSig). +Module ZAddOrderPropFunct (Import ZAxiomsMod : ZAxiomsSig). Module Export ZOrderPropMod := ZOrderPropFunct ZAxiomsMod. Open Local Scope IntScope. @@ -109,50 +109,50 @@ Proof. intros n m H1 H2. rewrite <- (Zadd_0_l 0). now apply Zadd_le_mono. Qed. -(** Minus and order *) +(** Sub and order *) -Theorem Zlt_0_minus : forall n m : Z, 0 < m - n <-> n < m. +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 Zminus_simpl_r. +rewrite Zadd_0_l; now rewrite Zsub_simpl_r. Qed. -Notation Zminus_pos := Zlt_0_minus (only parsing). +Notation Zsub_pos := Zlt_0_sub (only parsing). -Theorem Zle_0_minus : forall n m : Z, 0 <= m - n <-> n <= m. +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 Zminus_simpl_r. +rewrite Zadd_0_l; now rewrite Zsub_simpl_r. Qed. -Notation Zminus_nonneg := Zle_0_minus (only parsing). +Notation Zsub_nonneg := Zle_0_sub (only parsing). -Theorem Zlt_minus_0 : forall n m : Z, n - m < 0 <-> n < m. +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 Zminus_simpl_r. +rewrite Zadd_0_l; now rewrite Zsub_simpl_r. Qed. -Notation Zminus_neg := Zlt_minus_0 (only parsing). +Notation Zsub_neg := Zlt_sub_0 (only parsing). -Theorem Zle_minus_0 : forall n m : Z, n - m <= 0 <-> n <= m. +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 Zminus_simpl_r. +rewrite Zadd_0_l; now rewrite Zsub_simpl_r. Qed. -Notation Zminus_nonpos := Zle_minus_0 (only parsing). +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 Zminus_diag. symmetry; apply Zlt_0_minus. +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 Zminus_diag. symmetry; apply Zle_0_minus. +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. @@ -175,172 +175,172 @@ Proof. intro n. rewrite (Zopp_le_mono 0 n). now rewrite Zopp_0. Qed. -Theorem Zminus_lt_mono_l : forall n m p : Z, n < m <-> p - m < p - n. +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 Zminus_lt_mono_r : forall n m p : Z, n < m <-> n - p < m - p. +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 Zminus_lt_mono : forall n m p q : Z, n < m -> q < p -> n - p < m - q. +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 -> Zminus_lt_mono_r | now apply -> Zminus_lt_mono_l]. +[now apply -> Zsub_lt_mono_r | now apply -> Zsub_lt_mono_l]. Qed. -Theorem Zminus_le_mono_l : forall n m p : Z, n <= m <-> p - m <= p - n. +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 Zminus_le_mono_r : forall n m p : Z, n <= m <-> n - p <= m - p. +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 Zminus_le_mono : forall n m p q : Z, n <= m -> q <= p -> n - p <= m - q. +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 -> Zminus_le_mono_r | now apply -> Zminus_le_mono_l]. +[now apply -> Zsub_le_mono_r | now apply -> Zsub_le_mono_l]. Qed. -Theorem Zminus_lt_le_mono : forall n m p q : Z, n < m -> q <= p -> n - p < m - q. +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 -> Zminus_lt_mono_r | now apply -> Zminus_le_mono_l]. +[now apply -> Zsub_lt_mono_r | now apply -> Zsub_le_mono_l]. Qed. -Theorem Zminus_le_lt_mono : forall n m p q : Z, n <= m -> q < p -> n - p < m - q. +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 -> Zminus_le_mono_r | now apply -> Zminus_lt_mono_l]. +[now apply -> Zsub_le_mono_r | now apply -> Zsub_lt_mono_l]. Qed. -Theorem Zle_lt_minus_lt : forall n m p q : Z, n <= m -> p - n < q - m -> p < q. +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_minus_lt : forall n m p q : Z, n < m -> p - n <= q - m -> p < q. +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_minus_lt : forall n m p q : Z, n <= m -> p - n <= q - m -> p <= q. +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_minus_r : forall n m p : Z, n + p < m <-> n < m - p. +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 Zminus_lt_mono_r. +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_minus_r : forall n m p : Z, n + p <= m <-> n <= m - p. +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 Zminus_le_mono_r. +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_minus_l : forall n m p : Z, n + p < m <-> p < m - n. +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_minus_r. +intros n m p. rewrite Zadd_comm; apply Zlt_add_lt_sub_r. Qed. -Theorem Zle_add_le_minus_l : forall n m p : Z, n + p <= m <-> p <= m - n. +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_minus_r. +intros n m p. rewrite Zadd_comm; apply Zle_add_le_sub_r. Qed. -Theorem Zlt_minus_lt_add_r : forall n m p : Z, n - p < m <-> n < m + p. +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 Zminus_simpl_r. +now rewrite Zsub_simpl_r. Qed. -Theorem Zle_minus_le_add_r : forall n m p : Z, n - p <= m <-> n <= m + p. +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 Zminus_simpl_r. +now rewrite Zsub_simpl_r. Qed. -Theorem Zlt_minus_lt_add_l : forall n m p : Z, n - m < p <-> n < m + p. +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_minus_lt_add_r. +intros n m p. rewrite Zadd_comm; apply Zlt_sub_lt_add_r. Qed. -Theorem Zle_minus_le_add_l : forall n m p : Z, n - m <= p <-> n <= m + p. +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_minus_le_add_r. +intros n m p. rewrite Zadd_comm; apply Zle_sub_le_add_r. Qed. -Theorem Zlt_minus_lt_add : forall n m p q : Z, n - m < p - q <-> n + q < m + p. +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_minus_lt_add_l. rewrite Zadd_minus_assoc. -now rewrite <- Zlt_add_lt_minus_r. +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_minus_le_add : forall n m p q : Z, n - m <= p - q <-> n + q <= m + p. +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_minus_le_add_l. rewrite Zadd_minus_assoc. -now rewrite <- Zle_add_le_minus_r. +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_minus_pos : forall n m : Z, 0 < m <-> n - m < n. +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 Zminus_0_r. apply Zminus_lt_mono_l. +intros n m. stepr (n - m < n - 0) by now rewrite Zsub_0_r. apply Zsub_lt_mono_l. Qed. -Theorem Zle_minus_nonneg : forall n m : Z, 0 <= m <-> n - m <= n. +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 Zminus_0_r. apply Zminus_le_mono_l. +intros n m. stepr (n - m <= n - 0) by now rewrite Zsub_0_r. apply Zsub_le_mono_l. Qed. -Theorem Zminus_lt_cases : forall n m p q : Z, n - m < p - q -> n < m \/ q < p. +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_minus_lt_add in H. now apply Zadd_lt_cases. +intros n m p q H. rewrite Zlt_sub_lt_add in H. now apply Zadd_lt_cases. Qed. -Theorem Zminus_le_cases : forall n m p q : Z, n - m <= p - q -> n <= m \/ q <= p. +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_minus_le_add in H. now apply Zadd_le_cases. +intros n m p q H. rewrite Zle_sub_le_add in H. now apply Zadd_le_cases. Qed. -Theorem Zminus_neg_cases : forall n m : Z, n - m < 0 -> n < 0 \/ 0 < m. +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 Zminus_pos_cases : forall n m : Z, 0 < n - m -> 0 < n \/ m < 0. +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 Zminus_nonpos_cases : forall n m : Z, n - m <= 0 -> n <= 0 \/ 0 <= m. +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 Zminus_nonneg_cases : forall n m : Z, 0 <= n - m -> 0 <= n \/ m <= 0. +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). @@ -368,6 +368,6 @@ End PosNeg. Ltac Z0_pos_neg n := induction_maker n ltac:(apply Z0_pos_neg). -End ZPlusOrderPropFunct. +End ZAddOrderPropFunct. diff --git a/theories/Numbers/Integer/Abstract/ZAxioms.v b/theories/Numbers/Integer/Abstract/ZAxioms.v index 19fb40dfe..dfffe9a7f 100644 --- a/theories/Numbers/Integer/Abstract/ZAxioms.v +++ b/theories/Numbers/Integer/Abstract/ZAxioms.v @@ -26,7 +26,7 @@ Notation S := NZsucc. Notation P := NZpred. Notation Zadd := NZadd. Notation Zmul := NZmul. -Notation Zminus := NZminus. +Notation Zsub := NZsub. Notation Zlt := NZlt. Notation Zle := NZle. Notation Zmin := NZmin. @@ -36,7 +36,7 @@ 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" := (NZminus 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. diff --git a/theories/Numbers/Integer/Abstract/ZBase.v b/theories/Numbers/Integer/Abstract/ZBase.v index 0b8538873..d175c358c 100644 --- a/theories/Numbers/Integer/Abstract/ZBase.v +++ b/theories/Numbers/Integer/Abstract/ZBase.v @@ -12,7 +12,7 @@ Require Export Decidable. Require Export ZAxioms. -Require Import NZTimesOrder. +Require Import NZMulOrder. Module ZBasePropFunct (Import ZAxiomsMod : ZAxiomsSig). @@ -22,7 +22,7 @@ notations in Zadd and later *) Open Local Scope IntScope. -Module Export NZTimesOrderMod := NZTimesOrderPropFunct NZOrdAxiomsMod. +Module Export NZMulOrderMod := NZMulOrderPropFunct NZOrdAxiomsMod. Theorem Zsucc_wd : forall n1 n2 : Z, n1 == n2 -> S n1 == S n2. Proof NZsucc_wd. diff --git a/theories/Numbers/Integer/Abstract/ZLt.v b/theories/Numbers/Integer/Abstract/ZLt.v index 8ceecdbf2..1b8bdda40 100644 --- a/theories/Numbers/Integer/Abstract/ZLt.v +++ b/theories/Numbers/Integer/Abstract/ZLt.v @@ -10,10 +10,10 @@ (*i $Id$ i*) -Require Export ZTimes. +Require Export ZMul. Module ZOrderPropFunct (Import ZAxiomsMod : ZAxiomsSig). -Module Export ZTimesPropMod := ZTimesPropFunct ZAxiomsMod. +Module Export ZMulPropMod := ZMulPropFunct ZAxiomsMod. Open Local Scope IntScope. (* Axioms *) diff --git a/theories/Numbers/Integer/Abstract/ZTimes.v b/theories/Numbers/Integer/Abstract/ZMul.v index ccf324a06..785c0f41b 100644 --- a/theories/Numbers/Integer/Abstract/ZTimes.v +++ b/theories/Numbers/Integer/Abstract/ZMul.v @@ -10,10 +10,10 @@ (*i $Id$ i*) -Require Export ZPlus. +Require Export ZAdd. -Module ZTimesPropFunct (Import ZAxiomsMod : ZAxiomsSig). -Module Export ZPlusPropMod := ZPlusPropFunct ZAxiomsMod. +Module ZMulPropFunct (Import ZAxiomsMod : ZAxiomsSig). +Module Export ZAddPropMod := ZAddPropFunct ZAxiomsMod. Open Local Scope IntScope. Theorem Zmul_wd : @@ -74,7 +74,7 @@ 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_minus_assoc, Zminus_diag, Zadd_0_r. +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. @@ -98,18 +98,18 @@ Proof. intros n m; now rewrite Zmul_opp_l, Zmul_opp_r, Zopp_involutive. Qed. -Theorem Zmul_minus_distr_l : forall n m p : Z, n * (m - p) == n * m - n * p. +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_minus_distr_r : forall n m p : Z, (n - m) * p == n * p - m * p. +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_minus_distr_l. +now apply Zmul_sub_distr_l. Qed. -End ZTimesPropFunct. +End ZMulPropFunct. diff --git a/theories/Numbers/Integer/Abstract/ZTimesOrder.v b/theories/Numbers/Integer/Abstract/ZMulOrder.v index d3f5a0396..46a8a38af 100644 --- a/theories/Numbers/Integer/Abstract/ZTimesOrder.v +++ b/theories/Numbers/Integer/Abstract/ZMulOrder.v @@ -10,10 +10,10 @@ (*i $Id$ i*) -Require Export ZPlusOrder. +Require Export ZAddOrder. -Module ZTimesOrderPropFunct (Import ZAxiomsMod : ZAxiomsSig). -Module Export ZPlusOrderPropMod := ZPlusOrderPropFunct ZAxiomsMod. +Module ZMulOrderPropFunct (Import ZAxiomsMod : ZAxiomsSig). +Module Export ZAddOrderPropMod := ZAddOrderPropFunct ZAxiomsMod. Open Local Scope IntScope. Theorem Zmul_lt_pred : @@ -339,5 +339,5 @@ apply Zmul_lt_mono_nonneg. now apply Zlt_le_incl. assumption. apply Zle_0_1. assumption. Qed. -End ZTimesOrderPropFunct. +End ZMulOrderPropFunct. diff --git a/theories/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v index f54737036..947dc818e 100644 --- a/theories/Numbers/Integer/BigZ/BigZ.v +++ b/theories/Numbers/Integer/BigZ/BigZ.v @@ -11,7 +11,7 @@ (*i $Id$ i*) Require Export BigN. -Require Import ZTimesOrder. +Require Import ZMulOrder. Require Import ZSig. Require Import ZSigZAxioms. Require Import ZMake. @@ -21,7 +21,7 @@ Module BigZ <: ZType := ZMake.Make BigN. (** Module [BigZ] implements [ZAxiomsSig] *) Module Export BigZAxiomsMod := ZSig_ZAxioms BigZ. -Module Export BigZTimesOrderPropMod := ZTimesOrderPropFunct BigZAxiomsMod. +Module Export BigZMulOrderPropMod := ZMulOrderPropFunct BigZAxiomsMod. (** Notations about [BigZ] *) diff --git a/theories/Numbers/Integer/Binary/ZBinary.v b/theories/Numbers/Integer/Binary/ZBinary.v index acc77b3e7..0ff896367 100644 --- a/theories/Numbers/Integer/Binary/ZBinary.v +++ b/theories/Numbers/Integer/Binary/ZBinary.v @@ -10,7 +10,7 @@ (*i $Id$ i*) -Require Import ZTimesOrder. +Require Import ZMulOrder. Require Import ZArith. Open Local Scope Z_scope. @@ -25,7 +25,7 @@ Definition NZ0 := 0. Definition NZsucc := Zsucc'. Definition NZpred := Zpred'. Definition NZadd := Zplus. -Definition NZminus := Zminus. +Definition NZsub := Zminus. Definition NZmul := Zmult. Theorem NZeq_equiv : equiv Z NZeq. @@ -54,7 +54,7 @@ Proof. congruence. Qed. -Add Morphism NZminus with signature NZeq ==> NZeq ==> NZeq as NZminus_wd. +Add Morphism NZsub with signature NZeq ==> NZeq ==> NZeq as NZsub_wd. Proof. congruence. Qed. @@ -89,12 +89,12 @@ Proof. intros; do 2 rewrite <- Zsucc_succ'; apply Zplus_succ_l. Qed. -Theorem NZminus_0_r : forall n : Z, n - 0 = n. +Theorem NZsub_0_r : forall n : Z, n - 0 = n. Proof. exact Zminus_0_r. Qed. -Theorem NZminus_succ_r : forall n m : Z, n - (NZsucc m) = NZpred (n - m). +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. @@ -213,11 +213,11 @@ Qed. End ZBinAxiomsMod. -Module Export ZBinTimesOrderPropMod := ZTimesOrderPropFunct ZBinAxiomsMod. +Module Export ZBinMulOrderPropMod := ZMulOrderPropFunct ZBinAxiomsMod. (** Z forms a ring *) -(*Lemma Zring : ring_theory 0 1 NZadd NZmul NZminus Zopp NZeq. +(*Lemma Zring : ring_theory 0 1 NZadd NZmul NZsub Zopp NZeq. Proof. constructor. exact Zadd_0_l. diff --git a/theories/Numbers/Integer/NatPairs/ZNatPairs.v b/theories/Numbers/Integer/NatPairs/ZNatPairs.v index 97a72e087..aa027103f 100644 --- a/theories/Numbers/Integer/NatPairs/ZNatPairs.v +++ b/theories/Numbers/Integer/NatPairs/ZNatPairs.v @@ -10,15 +10,15 @@ (*i $Id$ i*) -Require Import NMinus. (* The most complete file for natural numbers *) -Require Export ZTimesOrder. (* The most complete file for integers *) +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 := NMinusPropFunct NAxiomsMod. (* Get all properties of natural numbers *) +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 NPlus and NTimes are used in the new BinNat, +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 @@ -62,7 +62,7 @@ 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 Zminus (n m : Z) : Z := ((fst n) + (snd m), (snd n) + (fst 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 *) @@ -81,7 +81,7 @@ 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" := (Zminus 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. @@ -102,7 +102,7 @@ Definition NZ0 := Z0. Definition NZsucc := Zsucc. Definition NZpred := Zpred. Definition NZadd := Zadd. -Definition NZminus := Zminus. +Definition NZsub := Zsub. Definition NZmul := Zmul. Theorem ZE_refl : reflexive Z Zeq. @@ -162,9 +162,9 @@ stepl (fst n1 + snd m1 + (fst n2 + snd m2)) by ring. now stepr (fst m1 + snd n1 + (fst m2 + snd n2)) by ring. Qed. -Add Morphism NZminus with signature Zeq ==> Zeq ==> Zeq as NZminus_wd. +Add Morphism NZsub with signature Zeq ==> Zeq ==> Zeq as NZsub_wd. Proof. -unfold Zeq, NZminus; intros n1 m1 H1 n2 m2 H2; simpl. +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. @@ -243,14 +243,14 @@ Proof. intros n m; unfold NZadd, Zeq; simpl. now do 2 rewrite add_succ_l. Qed. -Theorem NZminus_0_r : forall n : Z, n - 0 == n. +Theorem NZsub_0_r : forall n : Z, n - 0 == n. Proof. -intro n; unfold NZminus, Zeq; simpl. now do 2 rewrite add_0_r. +intro n; unfold NZsub, Zeq; simpl. now do 2 rewrite add_0_r. Qed. -Theorem NZminus_succ_r : forall n m : Z, n - (Zsucc m) == Zpred (n - m). +Theorem NZsub_succ_r : forall n m : Z, n - (Zsucc m) == Zpred (n - m). Proof. -intros n m; unfold NZminus, Zeq; simpl. symmetry; now rewrite add_succ_r. +intros n m; unfold NZsub, Zeq; simpl. symmetry; now rewrite add_succ_r. Qed. Theorem NZmul_0_l : forall n : Z, 0 * n == 0. @@ -413,7 +413,7 @@ and get their properties *) Require Import NPeano. Module Export ZPairsPeanoAxiomsMod := ZPairsAxiomsMod NPeanoAxiomsMod. -Module Export ZPairsTimesOrderPropMod := ZTimesOrderPropFunct ZPairsPeanoAxiomsMod. +Module Export ZPairsMulOrderPropMod := ZMulOrderPropFunct ZPairsPeanoAxiomsMod. Open Local Scope IntScope. diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v index bb56e6997..e1f04e45a 100644 --- a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v +++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v @@ -42,7 +42,7 @@ Definition NZ0 := Z.zero. Definition NZsucc := Z.succ. Definition NZpred := Z.pred. Definition NZadd := Z.add. -Definition NZminus := Z.sub. +Definition NZsub := Z.sub. Definition NZmul := Z.mul. Theorem NZeq_equiv : equiv Z.t Z.eq. @@ -71,7 +71,7 @@ Proof. intros; zsimpl; f_equal; assumption. Qed. -Add Morphism NZminus with signature Z.eq ==> Z.eq ==> Z.eq as NZminus_wd. +Add Morphism NZsub with signature Z.eq ==> Z.eq ==> Z.eq as NZsub_wd. Proof. intros; zsimpl; f_equal; assumption. Qed. @@ -154,12 +154,12 @@ Proof. intros; zsimpl; auto with zarith. Qed. -Theorem NZminus_0_r : forall n, n - 0 == n. +Theorem NZsub_0_r : forall n, n - 0 == n. Proof. intros; zsimpl; auto with zarith. Qed. -Theorem NZminus_succ_r : forall n m, n - (Z.succ m) == Z.pred (n - m). +Theorem NZsub_succ_r : forall n m, n - (Z.succ m) == Z.pred (n - m). Proof. intros; zsimpl; auto with zarith. Qed. diff --git a/theories/Numbers/NatInt/NZPlus.v b/theories/Numbers/NatInt/NZAdd.v index 6fb72ed4a..9c852bf90 100644 --- a/theories/Numbers/NatInt/NZPlus.v +++ b/theories/Numbers/NatInt/NZAdd.v @@ -13,7 +13,7 @@ Require Import NZAxioms. Require Import NZBase. -Module NZPlusPropFunct (Import NZAxiomsMod : NZAxiomsSig). +Module NZAddPropFunct (Import NZAxiomsMod : NZAxiomsSig). Module Export NZBasePropMod := NZBasePropFunct NZAxiomsMod. Open Local Scope NatIntScope. @@ -82,10 +82,10 @@ intros n m p. rewrite (NZadd_comm n p); rewrite (NZadd_comm m p). apply NZadd_cancel_l. Qed. -Theorem NZminus_1_r : forall n : NZ, n - 1 == P n. +Theorem NZsub_1_r : forall n : NZ, n - 1 == P n. Proof. -intro n; rewrite NZminus_succ_r; now rewrite NZminus_0_r. +intro n; rewrite NZsub_succ_r; now rewrite NZsub_0_r. Qed. -End NZPlusPropFunct. +End NZAddPropFunct. diff --git a/theories/Numbers/NatInt/NZPlusOrder.v b/theories/Numbers/NatInt/NZAddOrder.v index 00d178c0d..d1caa83ee 100644 --- a/theories/Numbers/NatInt/NZPlusOrder.v +++ b/theories/Numbers/NatInt/NZAddOrder.v @@ -13,7 +13,7 @@ Require Import NZAxioms. Require Import NZOrder. -Module NZPlusOrderPropFunct (Import NZOrdAxiomsMod : NZOrdAxiomsSig). +Module NZAddOrderPropFunct (Import NZOrdAxiomsMod : NZOrdAxiomsSig). Module Export NZOrderPropMod := NZOrderPropFunct NZOrdAxiomsMod. Open Local Scope NatIntScope. @@ -162,5 +162,5 @@ Proof. intros n m H; apply NZadd_le_cases; now rewrite NZadd_0_l. Qed. -End NZPlusOrderPropFunct. +End NZAddOrderPropFunct. diff --git a/theories/Numbers/NatInt/NZAxioms.v b/theories/Numbers/NatInt/NZAxioms.v index 516cf5b42..1ef780986 100644 --- a/theories/Numbers/NatInt/NZAxioms.v +++ b/theories/Numbers/NatInt/NZAxioms.v @@ -20,11 +20,11 @@ Parameter Inline NZ0 : NZ. Parameter Inline NZsucc : NZ -> NZ. Parameter Inline NZpred : NZ -> NZ. Parameter Inline NZadd : NZ -> NZ -> NZ. -Parameter Inline NZminus : NZ -> NZ -> NZ. +Parameter Inline NZsub : NZ -> NZ -> NZ. Parameter Inline NZmul : NZ -> NZ -> NZ. -(* Unary minus (opp) is not defined on natural numbers, so we have it for -integers only *) +(* Unary subtraction (opp) is not defined on natural numbers, so we have + it for integers only *) Axiom NZeq_equiv : equiv NZ NZeq. Add Relation NZ NZeq @@ -36,7 +36,7 @@ as NZeq_rel. Add Morphism NZsucc with signature NZeq ==> NZeq as NZsucc_wd. Add Morphism NZpred with signature NZeq ==> NZeq as NZpred_wd. Add Morphism NZadd with signature NZeq ==> NZeq ==> NZeq as NZadd_wd. -Add Morphism NZminus with signature NZeq ==> NZeq ==> NZeq as NZminus_wd. +Add Morphism NZsub with signature NZeq ==> NZeq ==> NZeq as NZsub_wd. Add Morphism NZmul with signature NZeq ==> NZeq ==> NZeq as NZmul_wd. Delimit Scope NatIntScope with NatInt. @@ -48,7 +48,7 @@ Notation S := NZsucc. Notation P := NZpred. Notation "1" := (S 0) : NatIntScope. Notation "x + y" := (NZadd x y) : NatIntScope. -Notation "x - y" := (NZminus x y) : NatIntScope. +Notation "x - y" := (NZsub x y) : NatIntScope. Notation "x * y" := (NZmul x y) : NatIntScope. Axiom NZpred_succ : forall n : NZ, P (S n) == n. @@ -60,8 +60,8 @@ Axiom NZinduction : Axiom NZadd_0_l : forall n : NZ, 0 + n == n. Axiom NZadd_succ_l : forall n m : NZ, (S n) + m == S (n + m). -Axiom NZminus_0_r : forall n : NZ, n - 0 == n. -Axiom NZminus_succ_r : forall n m : NZ, n - (S m) == P (n - m). +Axiom NZsub_0_r : forall n : NZ, n - 0 == n. +Axiom NZsub_succ_r : forall n m : NZ, n - (S m) == P (n - m). Axiom NZmul_0_l : forall n : NZ, 0 * n == 0. Axiom NZmul_succ_l : forall n m : NZ, S n * m == n * m + m. diff --git a/theories/Numbers/NatInt/NZTimes.v b/theories/Numbers/NatInt/NZMul.v index 9f93e0a1b..7d9b1aabd 100644 --- a/theories/Numbers/NatInt/NZTimes.v +++ b/theories/Numbers/NatInt/NZMul.v @@ -11,10 +11,10 @@ (*i $Id$ i*) Require Import NZAxioms. -Require Import NZPlus. +Require Import NZAdd. -Module NZTimesPropFunct (Import NZAxiomsMod : NZAxiomsSig). -Module Export NZPlusPropMod := NZPlusPropFunct NZAxiomsMod. +Module NZMulPropFunct (Import NZAxiomsMod : NZAxiomsSig). +Module Export NZAddPropMod := NZAddPropFunct NZAxiomsMod. Open Local Scope NatIntScope. Theorem NZmul_0_r : forall n : NZ, n * 0 == 0. @@ -76,5 +76,5 @@ Proof. intro n; rewrite NZmul_comm; apply NZmul_1_l. Qed. -End NZTimesPropFunct. +End NZMulPropFunct. diff --git a/theories/Numbers/NatInt/NZTimesOrder.v b/theories/Numbers/NatInt/NZMulOrder.v index ebb2a9b5d..ae5e2d444 100644 --- a/theories/Numbers/NatInt/NZTimesOrder.v +++ b/theories/Numbers/NatInt/NZMulOrder.v @@ -11,10 +11,10 @@ (*i $Id$ i*) Require Import NZAxioms. -Require Import NZPlusOrder. +Require Import NZAddOrder. -Module NZTimesOrderPropFunct (Import NZOrdAxiomsMod : NZOrdAxiomsSig). -Module Export NZPlusOrderPropMod := NZPlusOrderPropFunct NZOrdAxiomsMod. +Module NZMulOrderPropFunct (Import NZOrdAxiomsMod : NZOrdAxiomsSig). +Module Export NZAddOrderPropMod := NZAddOrderPropFunct NZOrdAxiomsMod. Open Local Scope NatIntScope. Theorem NZmul_lt_pred : @@ -307,4 +307,4 @@ now apply -> NZle_succ_l. apply NZadd_pos_pos; now apply NZlt_succ_diag_r. Qed. -End NZTimesOrderPropFunct. +End NZMulOrderPropFunct. diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v index f76fa9480..d8eaeb99c 100644 --- a/theories/Numbers/NatInt/NZOrder.v +++ b/theories/Numbers/NatInt/NZOrder.v @@ -11,11 +11,11 @@ (*i $Id$ i*) Require Import NZAxioms. -Require Import NZTimes. +Require Import NZMul. Require Import Decidable. Module NZOrderPropFunct (Import NZOrdAxiomsMod : NZOrdAxiomsSig). -Module Export NZTimesPropMod := NZTimesPropFunct NZAxiomsMod. +Module Export NZMulPropMod := NZMulPropFunct NZAxiomsMod. Open Local Scope NatIntScope. Ltac le_elim H := rewrite NZlt_eq_cases in H; destruct H as [H | H]. diff --git a/theories/Numbers/Natural/Abstract/NPlus.v b/theories/Numbers/Natural/Abstract/NAdd.v index 67443acff..37244159f 100644 --- a/theories/Numbers/Natural/Abstract/NPlus.v +++ b/theories/Numbers/Natural/Abstract/NAdd.v @@ -12,7 +12,7 @@ Require Export NBase. -Module NPlusPropFunct (Import NAxiomsMod : NAxiomsSig). +Module NAddPropFunct (Import NAxiomsMod : NAxiomsSig). Module Export NBasePropMod := NBasePropFunct NAxiomsMod. Open Local Scope NatScope. @@ -64,7 +64,7 @@ Proof NZadd_cancel_r. Theorem eq_add_0 : forall n m : N, n + m == 0 <-> n == 0 /\ m == 0. Proof. intros n m; induct n. -(* The next command does not work with the axiom add_0_l from NPlusSig *) +(* The next command does not work with the axiom add_0_l from NAddSig *) rewrite add_0_l. intuition reflexivity. intros n IH. rewrite add_succ_l. setoid_replace (S (n + m) == 0) with False using relation iff by @@ -133,10 +133,10 @@ forall n m : N, (exists p : N, p + n == m) \/ (exists p : N, p + m == n) (1) We will need (1) in the proof of induction principle for integers constructed as pairs of natural numbers. The formula (1) can be proved using properties of order and truncated subtraction. Thus, p would be -m - n or n - m and (1) would hold by theorem minus_add from Minus.v +m - n or n - m and (1) would hold by theorem sub_add from Sub.v depending on whether n <= m or m <= n. However, in proving induction for integers constructed from natural numbers we do not need to -require implementations of order and minus; it is enough to prove (1) +require implementations of order and sub; it is enough to prove (1) here. *) Theorem add_dichotomy : @@ -152,5 +152,5 @@ left; exists p'; rewrite add_succ_r; now rewrite add_succ_l in H. right; exists (S p). rewrite add_succ_l; now rewrite H. Qed. -End NPlusPropFunct. +End NAddPropFunct. diff --git a/theories/Numbers/Natural/Abstract/NPlusOrder.v b/theories/Numbers/Natural/Abstract/NAddOrder.v index 07eeffdfd..59f1c9347 100644 --- a/theories/Numbers/Natural/Abstract/NPlusOrder.v +++ b/theories/Numbers/Natural/Abstract/NAddOrder.v @@ -12,7 +12,7 @@ Require Export NOrder. -Module NPlusOrderPropFunct (Import NAxiomsMod : NAxiomsSig). +Module NAddOrderPropFunct (Import NAxiomsMod : NAxiomsSig). Module Export NOrderPropMod := NOrderPropFunct NAxiomsMod. Open Local Scope NatScope. @@ -111,4 +111,4 @@ do 2 rewrite <- add_assoc in H4. do 2 apply <- add_lt_mono_l in H4. now rewrite (add_comm n' u), (add_comm m' v). Qed. -End NPlusOrderPropFunct. +End NAddOrderPropFunct. diff --git a/theories/Numbers/Natural/Abstract/NAxioms.v b/theories/Numbers/Natural/Abstract/NAxioms.v index c31f216a3..60f2aae7d 100644 --- a/theories/Numbers/Natural/Abstract/NAxioms.v +++ b/theories/Numbers/Natural/Abstract/NAxioms.v @@ -26,7 +26,7 @@ Notation S := NZsucc. Notation P := NZpred. Notation add := NZadd. Notation mul := NZmul. -Notation minus := NZminus. +Notation sub := NZsub. Notation lt := NZlt. Notation le := NZle. Notation min := NZmin. @@ -36,7 +36,7 @@ Notation "x ~= y" := (~ Neq x y) (at level 70) : NatScope. Notation "0" := NZ0 : NatScope. Notation "1" := (NZsucc NZ0) : NatScope. Notation "x + y" := (NZadd x y) : NatScope. -Notation "x - y" := (NZminus x y) : NatScope. +Notation "x - y" := (NZsub x y) : NatScope. Notation "x * y" := (NZmul x y) : NatScope. Notation "x < y" := (NZlt x y) : NatScope. Notation "x <= y" := (NZle x y) : NatScope. diff --git a/theories/Numbers/Natural/Abstract/NBase.v b/theories/Numbers/Natural/Abstract/NBase.v index eb46e69de..0d7bc63eb 100644 --- a/theories/Numbers/Natural/Abstract/NBase.v +++ b/theories/Numbers/Natural/Abstract/NBase.v @@ -12,7 +12,7 @@ Require Export Decidable. Require Export NAxioms. -Require Import NZTimesOrder. (* The last property functor on NZ, which subsumes all others *) +Require Import NZMulOrder. (* The last property functor on NZ, which subsumes all others *) Module NBasePropFunct (Import NAxiomsMod : NAxiomsSig). @@ -22,16 +22,16 @@ Open Local Scope NatScope. ones, to get all properties of NZ at once. This way we will include them only one time. *) -Module Export NZTimesOrderMod := NZTimesOrderPropFunct NZOrdAxiomsMod. +Module Export NZMulOrderMod := NZMulOrderPropFunct NZOrdAxiomsMod. (* Here we probably need to re-prove all axioms declared in NAxioms.v to make sure that the definitions like N, S and add are unfolded in them, since unfolding is done only inside a functor. In fact, we'll do it in the files that prove the corresponding properties. In those files, we will also rename properties proved in NZ files by removing NZ from their names. In -this way, one only has to consult, for example, NPlus.v to see all +this way, one only has to consult, for example, NAdd.v to see all available properties for add, i.e., one does not have to go to NAxioms.v -for axioms and NZPlus.v for theorems. *) +for axioms and NZAdd.v for theorems. *) Theorem succ_wd : forall n1 n2 : N, n1 == n2 -> S n1 == S n2. Proof NZsucc_wd. diff --git a/theories/Numbers/Natural/Abstract/NMinus.v b/theories/Numbers/Natural/Abstract/NMinus.v deleted file mode 100644 index 81b41dc03..000000000 --- a/theories/Numbers/Natural/Abstract/NMinus.v +++ /dev/null @@ -1,180 +0,0 @@ -(************************************************************************) -(* 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$ i*) - -Require Export NTimesOrder. - -Module NMinusPropFunct (Import NAxiomsMod : NAxiomsSig). -Module Export NTimesOrderPropMod := NTimesOrderPropFunct NAxiomsMod. -Open Local Scope NatScope. - -Theorem minus_wd : - forall n1 n2 : N, n1 == n2 -> forall m1 m2 : N, m1 == m2 -> n1 - m1 == n2 - m2. -Proof NZminus_wd. - -Theorem minus_0_r : forall n : N, n - 0 == n. -Proof NZminus_0_r. - -Theorem minus_succ_r : forall n m : N, n - (S m) == P (n - m). -Proof NZminus_succ_r. - -Theorem minus_1_r : forall n : N, n - 1 == P n. -Proof. -intro n; rewrite minus_succ_r; now rewrite minus_0_r. -Qed. - -Theorem minus_0_l : forall n : N, 0 - n == 0. -Proof. -induct n. -apply minus_0_r. -intros n IH; rewrite minus_succ_r; rewrite IH. now apply pred_0. -Qed. - -Theorem minus_succ : forall n m : N, S n - S m == n - m. -Proof. -intro n; induct m. -rewrite minus_succ_r. do 2 rewrite minus_0_r. now rewrite pred_succ. -intros m IH. rewrite minus_succ_r. rewrite IH. now rewrite minus_succ_r. -Qed. - -Theorem minus_diag : forall n : N, n - n == 0. -Proof. -induct n. apply minus_0_r. intros n IH; rewrite minus_succ; now rewrite IH. -Qed. - -Theorem minus_gt : forall n m : N, n > m -> n - m ~= 0. -Proof. -intros n m H; elim H using lt_ind_rel; clear n m H. -solve_relation_wd. -intro; rewrite minus_0_r; apply neq_succ_0. -intros; now rewrite minus_succ. -Qed. - -Theorem add_minus_assoc : forall n m p : N, p <= m -> n + (m - p) == (n + m) - p. -Proof. -intros n m p; induct p. -intro; now do 2 rewrite minus_0_r. -intros p IH H. do 2 rewrite minus_succ_r. -rewrite <- IH by (apply lt_le_incl; now apply -> le_succ_l). -rewrite add_pred_r by (apply minus_gt; now apply -> le_succ_l). -reflexivity. -Qed. - -Theorem minus_succ_l : forall n m : N, n <= m -> S m - n == S (m - n). -Proof. -intros n m H. rewrite <- (add_1_l m). rewrite <- (add_1_l (m - n)). -symmetry; now apply add_minus_assoc. -Qed. - -Theorem add_minus : forall n m : N, (n + m) - m == n. -Proof. -intros n m. rewrite <- add_minus_assoc by (apply le_refl). -rewrite minus_diag; now rewrite add_0_r. -Qed. - -Theorem minus_add : forall n m : N, n <= m -> (m - n) + n == m. -Proof. -intros n m H. rewrite add_comm. rewrite add_minus_assoc by assumption. -rewrite add_comm. apply add_minus. -Qed. - -Theorem add_minus_eq_l : forall n m p : N, m + p == n -> n - m == p. -Proof. -intros n m p H. symmetry. -assert (H1 : m + p - m == n - m) by now rewrite H. -rewrite add_comm in H1. now rewrite add_minus in H1. -Qed. - -Theorem add_minus_eq_r : forall n m p : N, m + p == n -> n - p == m. -Proof. -intros n m p H; rewrite add_comm in H; now apply add_minus_eq_l. -Qed. - -(* This could be proved by adding m to both sides. Then the proof would -use add_minus_assoc and minus_0_le, which is proven below. *) - -Theorem add_minus_eq_nz : forall n m p : N, p ~= 0 -> n - m == p -> m + p == n. -Proof. -intros n m p H; double_induct n m. -intros m H1; rewrite minus_0_l in H1. symmetry in H1; false_hyp H1 H. -intro n; rewrite minus_0_r; now rewrite add_0_l. -intros n m IH H1. rewrite minus_succ in H1. apply IH in H1. -rewrite add_succ_l; now rewrite H1. -Qed. - -Theorem minus_add_distr : forall n m p : N, n - (m + p) == (n - m) - p. -Proof. -intros n m; induct p. -rewrite add_0_r; now rewrite minus_0_r. -intros p IH. rewrite add_succ_r; do 2 rewrite minus_succ_r. now rewrite IH. -Qed. - -Theorem add_minus_swap : forall n m p : N, p <= n -> n + m - p == n - p + m. -Proof. -intros n m p H. -rewrite (add_comm n m). -rewrite <- add_minus_assoc by assumption. -now rewrite (add_comm m (n - p)). -Qed. - -(** Minus and order *) - -Theorem le_minus_l : forall n m : N, n - m <= n. -Proof. -intro n; induct m. -rewrite minus_0_r; now apply eq_le_incl. -intros m IH. rewrite minus_succ_r. -apply le_trans with (n - m); [apply le_pred_l | assumption]. -Qed. - -Theorem minus_0_le : forall n m : N, n - m == 0 <-> n <= m. -Proof. -double_induct n m. -intro m; split; intro; [apply le_0_l | apply minus_0_l]. -intro m; rewrite minus_0_r; split; intro H; -[false_hyp H neq_succ_0 | false_hyp H nle_succ_0]. -intros n m H. rewrite <- succ_le_mono. now rewrite minus_succ. -Qed. - -(** Minus and mul *) - -Theorem mul_pred_r : forall n m : N, n * (P m) == n * m - n. -Proof. -intros n m; cases m. -now rewrite pred_0, mul_0_r, minus_0_l. -intro m; rewrite pred_succ, mul_succ_r, <- add_minus_assoc. -now rewrite minus_diag, add_0_r. -now apply eq_le_incl. -Qed. - -Theorem mul_minus_distr_r : forall n m p : N, (n - m) * p == n * p - m * p. -Proof. -intros n m p; induct n. -now rewrite minus_0_l, mul_0_l, minus_0_l. -intros n IH. destruct (le_gt_cases m n) as [H | H]. -rewrite minus_succ_l by assumption. do 2 rewrite mul_succ_l. -rewrite (add_comm ((n - m) * p) p), (add_comm (n * p) p). -rewrite <- (add_minus_assoc p (n * p) (m * p)) by now apply mul_le_mono_r. -now apply <- add_cancel_l. -assert (H1 : S n <= m); [now apply <- le_succ_l |]. -setoid_replace (S n - m) with 0 by now apply <- minus_0_le. -setoid_replace ((S n * p) - m * p) with 0 by (apply <- minus_0_le; now apply mul_le_mono_r). -apply mul_0_l. -Qed. - -Theorem mul_minus_distr_l : forall n m p : N, p * (n - m) == p * n - p * m. -Proof. -intros n m p; rewrite (mul_comm p (n - m)), (mul_comm p n), (mul_comm p m). -apply mul_minus_distr_r. -Qed. - -End NMinusPropFunct. - diff --git a/theories/Numbers/Natural/Abstract/NTimes.v b/theories/Numbers/Natural/Abstract/NMul.v index 3b1ffa79e..69b284fdc 100644 --- a/theories/Numbers/Natural/Abstract/NTimes.v +++ b/theories/Numbers/Natural/Abstract/NMul.v @@ -10,10 +10,10 @@ (*i $Id$ i*) -Require Export NPlus. +Require Export NAdd. -Module NTimesPropFunct (Import NAxiomsMod : NAxiomsSig). -Module Export NPlusPropMod := NPlusPropFunct NAxiomsMod. +Module NMulPropFunct (Import NAxiomsMod : NAxiomsSig). +Module Export NAddPropMod := NAddPropFunct NAxiomsMod. Open Local Scope NatScope. Theorem mul_wd : @@ -52,7 +52,7 @@ Proof NZmul_1_l. Theorem mul_1_r : forall n : N, n * 1 == n. Proof NZmul_1_r. -(* Theorems that cannot be proved in NZTimes *) +(* Theorems that cannot be proved in NZMul *) (* In proving the correctness of the definition of multiplication on integers constructed from pairs of natural numbers, we'll need the @@ -83,5 +83,5 @@ apply -> add_cancel_r in H3. now rewrite (add_comm (a * n') u), (add_comm (a * m') v). Qed. -End NTimesPropFunct. +End NMulPropFunct. diff --git a/theories/Numbers/Natural/Abstract/NTimesOrder.v b/theories/Numbers/Natural/Abstract/NMulOrder.v index 31f417733..ac4cc5e9e 100644 --- a/theories/Numbers/Natural/Abstract/NTimesOrder.v +++ b/theories/Numbers/Natural/Abstract/NMulOrder.v @@ -10,10 +10,10 @@ (*i $Id$ i*) -Require Export NPlusOrder. +Require Export NAddOrder. -Module NTimesOrderPropFunct (Import NAxiomsMod : NAxiomsSig). -Module Export NPlusOrderPropMod := NPlusOrderPropFunct NAxiomsMod. +Module NMulOrderPropFunct (Import NAxiomsMod : NAxiomsSig). +Module Export NAddOrderPropMod := NAddOrderPropFunct NAxiomsMod. Open Local Scope NatScope. Theorem mul_lt_pred : @@ -127,5 +127,5 @@ assert (H3 : 1 < n * m) by now apply (lt_1_l 0 m). rewrite H in H3; false_hyp H3 lt_irrefl. Qed. -End NTimesOrderPropFunct. +End NMulOrderPropFunct. diff --git a/theories/Numbers/Natural/Abstract/NOrder.v b/theories/Numbers/Natural/Abstract/NOrder.v index bc5753d16..bcd4b92d6 100644 --- a/theories/Numbers/Natural/Abstract/NOrder.v +++ b/theories/Numbers/Natural/Abstract/NOrder.v @@ -10,10 +10,10 @@ (*i $Id$ i*) -Require Export NTimes. +Require Export NMul. Module NOrderPropFunct (Import NAxiomsMod : NAxiomsSig). -Module Export NTimesPropMod := NTimesPropFunct NAxiomsMod. +Module Export NMulPropMod := NMulPropFunct NAxiomsMod. Open Local Scope NatScope. (* The tactics le_less, le_equal and le_elim are inherited from NZOrder.v *) diff --git a/theories/Numbers/Natural/Abstract/NStrongRec.v b/theories/Numbers/Natural/Abstract/NStrongRec.v index 78b647d99..5303bf8e5 100644 --- a/theories/Numbers/Natural/Abstract/NStrongRec.v +++ b/theories/Numbers/Natural/Abstract/NStrongRec.v @@ -13,10 +13,10 @@ (** This file defined the strong (course-of-value, well-founded) recursion and proves its properties *) -Require Export NMinus. +Require Export NSub. Module NStrongRecPropFunct (Import NAxiomsMod : NAxiomsSig). -Module Export NMinusPropMod := NMinusPropFunct NAxiomsMod. +Module Export NSubPropMod := NSubPropFunct NAxiomsMod. Open Local Scope NatScope. Section StrongRecursion. diff --git a/theories/Numbers/Natural/Abstract/NSub.v b/theories/Numbers/Natural/Abstract/NSub.v new file mode 100644 index 000000000..cfeb6709b --- /dev/null +++ b/theories/Numbers/Natural/Abstract/NSub.v @@ -0,0 +1,180 @@ +(************************************************************************) +(* 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$ i*) + +Require Export NMulOrder. + +Module NSubPropFunct (Import NAxiomsMod : NAxiomsSig). +Module Export NMulOrderPropMod := NMulOrderPropFunct NAxiomsMod. +Open Local Scope NatScope. + +Theorem sub_wd : + forall n1 n2 : N, n1 == n2 -> forall m1 m2 : N, m1 == m2 -> n1 - m1 == n2 - m2. +Proof NZsub_wd. + +Theorem sub_0_r : forall n : N, n - 0 == n. +Proof NZsub_0_r. + +Theorem sub_succ_r : forall n m : N, n - (S m) == P (n - m). +Proof NZsub_succ_r. + +Theorem sub_1_r : forall n : N, n - 1 == P n. +Proof. +intro n; rewrite sub_succ_r; now rewrite sub_0_r. +Qed. + +Theorem sub_0_l : forall n : N, 0 - n == 0. +Proof. +induct n. +apply sub_0_r. +intros n IH; rewrite sub_succ_r; rewrite IH. now apply pred_0. +Qed. + +Theorem sub_succ : forall n m : N, S n - S m == n - m. +Proof. +intro n; induct m. +rewrite sub_succ_r. do 2 rewrite sub_0_r. now rewrite pred_succ. +intros m IH. rewrite sub_succ_r. rewrite IH. now rewrite sub_succ_r. +Qed. + +Theorem sub_diag : forall n : N, n - n == 0. +Proof. +induct n. apply sub_0_r. intros n IH; rewrite sub_succ; now rewrite IH. +Qed. + +Theorem sub_gt : forall n m : N, n > m -> n - m ~= 0. +Proof. +intros n m H; elim H using lt_ind_rel; clear n m H. +solve_relation_wd. +intro; rewrite sub_0_r; apply neq_succ_0. +intros; now rewrite sub_succ. +Qed. + +Theorem add_sub_assoc : forall n m p : N, p <= m -> n + (m - p) == (n + m) - p. +Proof. +intros n m p; induct p. +intro; now do 2 rewrite sub_0_r. +intros p IH H. do 2 rewrite sub_succ_r. +rewrite <- IH by (apply lt_le_incl; now apply -> le_succ_l). +rewrite add_pred_r by (apply sub_gt; now apply -> le_succ_l). +reflexivity. +Qed. + +Theorem sub_succ_l : forall n m : N, n <= m -> S m - n == S (m - n). +Proof. +intros n m H. rewrite <- (add_1_l m). rewrite <- (add_1_l (m - n)). +symmetry; now apply add_sub_assoc. +Qed. + +Theorem add_sub : forall n m : N, (n + m) - m == n. +Proof. +intros n m. rewrite <- add_sub_assoc by (apply le_refl). +rewrite sub_diag; now rewrite add_0_r. +Qed. + +Theorem sub_add : forall n m : N, n <= m -> (m - n) + n == m. +Proof. +intros n m H. rewrite add_comm. rewrite add_sub_assoc by assumption. +rewrite add_comm. apply add_sub. +Qed. + +Theorem add_sub_eq_l : forall n m p : N, m + p == n -> n - m == p. +Proof. +intros n m p H. symmetry. +assert (H1 : m + p - m == n - m) by now rewrite H. +rewrite add_comm in H1. now rewrite add_sub in H1. +Qed. + +Theorem add_sub_eq_r : forall n m p : N, m + p == n -> n - p == m. +Proof. +intros n m p H; rewrite add_comm in H; now apply add_sub_eq_l. +Qed. + +(* This could be proved by adding m to both sides. Then the proof would +use add_sub_assoc and sub_0_le, which is proven below. *) + +Theorem add_sub_eq_nz : forall n m p : N, p ~= 0 -> n - m == p -> m + p == n. +Proof. +intros n m p H; double_induct n m. +intros m H1; rewrite sub_0_l in H1. symmetry in H1; false_hyp H1 H. +intro n; rewrite sub_0_r; now rewrite add_0_l. +intros n m IH H1. rewrite sub_succ in H1. apply IH in H1. +rewrite add_succ_l; now rewrite H1. +Qed. + +Theorem sub_add_distr : forall n m p : N, n - (m + p) == (n - m) - p. +Proof. +intros n m; induct p. +rewrite add_0_r; now rewrite sub_0_r. +intros p IH. rewrite add_succ_r; do 2 rewrite sub_succ_r. now rewrite IH. +Qed. + +Theorem add_sub_swap : forall n m p : N, p <= n -> n + m - p == n - p + m. +Proof. +intros n m p H. +rewrite (add_comm n m). +rewrite <- add_sub_assoc by assumption. +now rewrite (add_comm m (n - p)). +Qed. + +(** Sub and order *) + +Theorem le_sub_l : forall n m : N, n - m <= n. +Proof. +intro n; induct m. +rewrite sub_0_r; now apply eq_le_incl. +intros m IH. rewrite sub_succ_r. +apply le_trans with (n - m); [apply le_pred_l | assumption]. +Qed. + +Theorem sub_0_le : forall n m : N, n - m == 0 <-> n <= m. +Proof. +double_induct n m. +intro m; split; intro; [apply le_0_l | apply sub_0_l]. +intro m; rewrite sub_0_r; split; intro H; +[false_hyp H neq_succ_0 | false_hyp H nle_succ_0]. +intros n m H. rewrite <- succ_le_mono. now rewrite sub_succ. +Qed. + +(** Sub and mul *) + +Theorem mul_pred_r : forall n m : N, n * (P m) == n * m - n. +Proof. +intros n m; cases m. +now rewrite pred_0, mul_0_r, sub_0_l. +intro m; rewrite pred_succ, mul_succ_r, <- add_sub_assoc. +now rewrite sub_diag, add_0_r. +now apply eq_le_incl. +Qed. + +Theorem mul_sub_distr_r : forall n m p : N, (n - m) * p == n * p - m * p. +Proof. +intros n m p; induct n. +now rewrite sub_0_l, mul_0_l, sub_0_l. +intros n IH. destruct (le_gt_cases m n) as [H | H]. +rewrite sub_succ_l by assumption. do 2 rewrite mul_succ_l. +rewrite (add_comm ((n - m) * p) p), (add_comm (n * p) p). +rewrite <- (add_sub_assoc p (n * p) (m * p)) by now apply mul_le_mono_r. +now apply <- add_cancel_l. +assert (H1 : S n <= m); [now apply <- le_succ_l |]. +setoid_replace (S n - m) with 0 by now apply <- sub_0_le. +setoid_replace ((S n * p) - m * p) with 0 by (apply <- sub_0_le; now apply mul_le_mono_r). +apply mul_0_l. +Qed. + +Theorem mul_sub_distr_l : forall n m p : N, p * (n - m) == p * n - p * m. +Proof. +intros n m p; rewrite (mul_comm p (n - m)), (mul_comm p n), (mul_comm p m). +apply mul_sub_distr_r. +Qed. + +End NSubPropFunct. + diff --git a/theories/Numbers/Natural/BigN/BigN.v b/theories/Numbers/Natural/BigN/BigN.v index 330a97ab5..485480fa0 100644 --- a/theories/Numbers/Natural/BigN/BigN.v +++ b/theories/Numbers/Natural/BigN/BigN.v @@ -20,14 +20,14 @@ Require Import Cyclic31. Require Import NSig. Require Import NSigNAxioms. Require Import NMake. -Require Import NMinus. +Require Import NSub. Module BigN <: NType := NMake.Make Int31Cyclic. (** Module [BigN] implements [NAxiomsSig] *) Module Export BigNAxiomsMod := NSig_NAxioms BigN. -Module Export BigNMinusPropMod := NMinusPropFunct BigNAxiomsMod. +Module Export BigNSubPropMod := NSubPropFunct BigNAxiomsMod. (** Notations about [BigN] *) diff --git a/theories/Numbers/Natural/Binary/NBinDefs.v b/theories/Numbers/Natural/Binary/NBinDefs.v index 268879aa4..e0f3fdf4b 100644 --- a/theories/Numbers/Natural/Binary/NBinDefs.v +++ b/theories/Numbers/Natural/Binary/NBinDefs.v @@ -12,7 +12,7 @@ Require Import BinPos. Require Export BinNat. -Require Import NMinus. +Require Import NSub. Open Local Scope N_scope. @@ -28,7 +28,7 @@ Definition NZ0 := N0. Definition NZsucc := Nsucc. Definition NZpred := Npred. Definition NZadd := Nplus. -Definition NZminus := Nminus. +Definition NZsub := Nminus. Definition NZmul := Nmult. Theorem NZeq_equiv : equiv N NZeq. @@ -55,7 +55,7 @@ Proof. congruence. Qed. -Add Morphism NZminus with signature NZeq ==> NZeq ==> NZeq as NZminus_wd. +Add Morphism NZsub with signature NZeq ==> NZeq ==> NZeq as NZsub_wd. Proof. congruence. Qed. @@ -93,12 +93,12 @@ simpl in |- *; reflexivity. simpl in |- *; rewrite Pplus_succ_permute_l; reflexivity. Qed. -Theorem NZminus_0_r : forall n : NZ, n - N0 = n. +Theorem NZsub_0_r : forall n : NZ, n - N0 = n. Proof. now destruct n. Qed. -Theorem NZminus_succ_r : forall n m : NZ, n - (NZsucc m) = NZpred (n - m). +Theorem NZsub_succ_r : forall n m : NZ, n - (NZsucc m) = NZpred (n - m). Proof. destruct n as [| p]; destruct m as [| q]; try reflexivity. now destruct p. @@ -242,7 +242,7 @@ Qed. End NBinaryAxiomsMod. -Module Export NBinaryMinusPropMod := NMinusPropFunct NBinaryAxiomsMod. +Module Export NBinarySubPropMod := NSubPropFunct NBinaryAxiomsMod. (* Some fun comparing the efficiency of the generic log defined by strong (course-of-value) recursion and the log defined by recursion diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v index 0b3586888..8d9e17fb0 100644 --- a/theories/Numbers/Natural/Peano/NPeano.v +++ b/theories/Numbers/Natural/Peano/NPeano.v @@ -13,7 +13,7 @@ Require Import Arith. Require Import Min. Require Import Max. -Require Import NMinus. +Require Import NSub. Module NPeanoAxiomsMod <: NAxiomsSig. Module Export NZOrdAxiomsMod <: NZOrdAxiomsSig. @@ -25,7 +25,7 @@ Definition NZ0 := 0. Definition NZsucc := S. Definition NZpred := pred. Definition NZadd := plus. -Definition NZminus := minus. +Definition NZsub := minus. Definition NZmul := mult. Theorem NZeq_equiv : equiv nat NZeq. @@ -56,7 +56,7 @@ Proof. congruence. Qed. -Add Morphism NZminus with signature NZeq ==> NZeq ==> NZeq as NZminus_wd. +Add Morphism NZsub with signature NZeq ==> NZeq ==> NZeq as NZsub_wd. Proof. congruence. Qed. @@ -88,14 +88,14 @@ Proof. reflexivity. Qed. -Theorem NZminus_0_r : forall n : nat, n - 0 = n. +Theorem NZsub_0_r : forall n : nat, n - 0 = n. Proof. intro n; now destruct n. Qed. -Theorem NZminus_succ_r : forall n m : nat, n - (S m) = pred (n - m). +Theorem NZsub_succ_r : forall n m : nat, n - (S m) = pred (n - m). Proof. -intros n m; induction n m using nat_double_ind; simpl; auto. apply NZminus_0_r. +intros n m; induction n m using nat_double_ind; simpl; auto. apply NZsub_0_r. Qed. Theorem NZmul_0_l : forall n : nat, 0 * n = 0. @@ -216,5 +216,5 @@ End NPeanoAxiomsMod. (* Now we apply the largest property functor *) -Module Export NPeanoMinusPropMod := NMinusPropFunct NPeanoAxiomsMod. +Module Export NPeanoSubPropMod := NSubPropFunct NPeanoAxiomsMod. diff --git a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v index 54d7aec52..4f558e80a 100644 --- a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v +++ b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v @@ -36,7 +36,7 @@ Definition NZ0 := N.zero. Definition NZsucc := N.succ. Definition NZpred := N.pred. Definition NZadd := N.add. -Definition NZminus := N.sub. +Definition NZsub := N.sub. Definition NZmul := N.mul. Theorem NZeq_equiv : equiv N.t N.eq. @@ -69,7 +69,7 @@ Proof. unfold N.eq; intros; rewrite 2 N.spec_add; f_equal; auto. Qed. -Add Morphism NZminus with signature N.eq ==> N.eq ==> N.eq as NZminus_wd. +Add Morphism NZsub with signature N.eq ==> N.eq ==> N.eq as NZsub_wd. Proof. unfold N.eq; intros x x' Hx y y' Hy. destruct (Z_lt_le_dec [x] [y]). @@ -147,13 +147,13 @@ Proof. intros; red; rewrite N.spec_add, 2 N.spec_succ, N.spec_add; auto with zarith. Qed. -Theorem NZminus_0_r : forall n, n - 0 == n. +Theorem NZsub_0_r : forall n, n - 0 == n. Proof. intros; red; rewrite N.spec_sub; rewrite N.spec_0; auto with zarith. apply N.spec_pos. Qed. -Theorem NZminus_succ_r : forall n m, n - (N.succ m) == N.pred (n - m). +Theorem NZsub_succ_r : forall n m, n - (N.succ m) == N.pred (n - m). Proof. intros; red. destruct (Z_lt_le_dec [n] [N.succ m]) as [H|H]. |