diff options
Diffstat (limited to 'theories/Numbers/Integer/Abstract/ZPlus.v')
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZPlus.v | 182 |
1 files changed, 91 insertions, 91 deletions
diff --git a/theories/Numbers/Integer/Abstract/ZPlus.v b/theories/Numbers/Integer/Abstract/ZPlus.v index 2520d62e1..d72d00379 100644 --- a/theories/Numbers/Integer/Abstract/ZPlus.v +++ b/theories/Numbers/Integer/Abstract/ZPlus.v @@ -16,15 +16,15 @@ Module ZPlusPropFunct (Import ZAxiomsMod : ZAxiomsSig). Module Export ZBasePropMod := ZBasePropFunct ZAxiomsMod. Open Local Scope IntScope. -Theorem Zplus_wd : +Theorem Zadd_wd : forall n1 n2 : Z, n1 == n2 -> forall m1 m2 : Z, m1 == m2 -> n1 + m1 == n2 + m2. -Proof NZplus_wd. +Proof NZadd_wd. -Theorem Zplus_0_l : forall n : Z, 0 + n == n. -Proof NZplus_0_l. +Theorem Zadd_0_l : forall n : Z, 0 + n == n. +Proof NZadd_0_l. -Theorem Zplus_succ_l : forall n m : Z, (S n) + m == S (n + m). -Proof NZplus_succ_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. @@ -40,66 +40,66 @@ Proof Zopp_succ. (* Theorems that are valid for both natural numbers and integers *) -Theorem Zplus_0_r : forall n : Z, n + 0 == n. -Proof NZplus_0_r. +Theorem Zadd_0_r : forall n : Z, n + 0 == n. +Proof NZadd_0_r. -Theorem Zplus_succ_r : forall n m : Z, n + S m == S (n + m). -Proof NZplus_succ_r. +Theorem Zadd_succ_r : forall n m : Z, n + S m == S (n + m). +Proof NZadd_succ_r. -Theorem Zplus_comm : forall n m : Z, n + m == m + n. -Proof NZplus_comm. +Theorem Zadd_comm : forall n m : Z, n + m == m + n. +Proof NZadd_comm. -Theorem Zplus_assoc : forall n m p : Z, n + (m + p) == (n + m) + p. -Proof NZplus_assoc. +Theorem Zadd_assoc : forall n m p : Z, n + (m + p) == (n + m) + p. +Proof NZadd_assoc. -Theorem Zplus_shuffle1 : forall n m p q : Z, (n + m) + (p + q) == (n + p) + (m + q). -Proof NZplus_shuffle1. +Theorem Zadd_shuffle1 : forall n m p q : Z, (n + m) + (p + q) == (n + p) + (m + q). +Proof NZadd_shuffle1. -Theorem Zplus_shuffle2 : forall n m p q : Z, (n + m) + (p + q) == (n + q) + (m + p). -Proof NZplus_shuffle2. +Theorem Zadd_shuffle2 : forall n m p q : Z, (n + m) + (p + q) == (n + q) + (m + p). +Proof NZadd_shuffle2. -Theorem Zplus_1_l : forall n : Z, 1 + n == S n. -Proof NZplus_1_l. +Theorem Zadd_1_l : forall n : Z, 1 + n == S n. +Proof NZadd_1_l. -Theorem Zplus_1_r : forall n : Z, n + 1 == S n. -Proof NZplus_1_r. +Theorem Zadd_1_r : forall n : Z, n + 1 == S n. +Proof NZadd_1_r. -Theorem Zplus_cancel_l : forall n m p : Z, p + n == p + m <-> n == m. -Proof NZplus_cancel_l. +Theorem Zadd_cancel_l : forall n m p : Z, p + n == p + m <-> n == m. +Proof NZadd_cancel_l. -Theorem Zplus_cancel_r : forall n m p : Z, n + p == m + p <-> n == m. -Proof NZplus_cancel_r. +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 Zplus_pred_l : forall n m : Z, P n + m == P (n + m). +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 Zplus_succ_l. now rewrite Zpred_succ. +rewrite Zadd_succ_l. now rewrite Zpred_succ. Qed. -Theorem Zplus_pred_r : forall n m : Z, n + P m == P (n + m). +Theorem Zadd_pred_r : forall n m : Z, n + P m == P (n + m). Proof. -intros n m; rewrite (Zplus_comm n (P m)), (Zplus_comm n m); -apply Zplus_pred_l. +intros n m; rewrite (Zadd_comm n (P m)), (Zadd_comm n m); +apply Zadd_pred_l. Qed. -Theorem Zplus_opp_r : forall n m : Z, n + (- m) == n - m. +Theorem Zadd_opp_r : forall n m : Z, n + (- m) == n - m. Proof. NZinduct m. -rewrite Zopp_0; rewrite Zminus_0_r; now rewrite Zplus_0_r. -intro m. rewrite Zopp_succ, Zminus_succ_r, Zplus_pred_r; now rewrite Zpred_inj_wd. +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. Qed. Theorem Zminus_0_l : forall n : Z, 0 - n == - n. Proof. -intro n; rewrite <- Zplus_opp_r; now rewrite Zplus_0_l. +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). Proof. -intros n m; do 2 rewrite <- Zplus_opp_r; now rewrite Zplus_succ_l. +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). @@ -127,24 +127,24 @@ now rewrite Zminus_0_r. intro n. rewrite Zminus_succ_r, Zminus_succ_l; now rewrite Zpred_succ. Qed. -Theorem Zplus_opp_diag_l : forall n : Z, - n + n == 0. +Theorem Zadd_opp_diag_l : forall n : Z, - n + n == 0. Proof. -intro n; now rewrite Zplus_comm, Zplus_opp_r, Zminus_diag. +intro n; now rewrite Zadd_comm, Zadd_opp_r, Zminus_diag. Qed. -Theorem Zplus_opp_diag_r : forall n : Z, n + (- n) == 0. +Theorem Zadd_opp_diag_r : forall n : Z, n + (- n) == 0. Proof. -intro n; rewrite Zplus_comm; apply Zplus_opp_diag_l. +intro n; rewrite Zadd_comm; apply Zadd_opp_diag_l. Qed. -Theorem Zplus_opp_l : forall n m : Z, - m + n == n - m. +Theorem Zadd_opp_l : forall n m : Z, - m + n == n - m. Proof. -intros n m; rewrite <- Zplus_opp_r; now rewrite Zplus_comm. +intros n m; rewrite <- Zadd_opp_r; now rewrite Zadd_comm. Qed. -Theorem Zplus_minus_assoc : forall n m p : Z, n + (m - p) == (n + m) - p. +Theorem Zadd_minus_assoc : forall n m p : Z, n + (m - p) == (n + m) - p. Proof. -intros n m p; do 2 rewrite <- Zplus_opp_r; now rewrite Zplus_assoc. +intros n m p; do 2 rewrite <- Zadd_opp_r; now rewrite Zadd_assoc. Qed. Theorem Zopp_involutive : forall n : Z, - (- n) == n. @@ -154,17 +154,17 @@ now do 2 rewrite Zopp_0. intro n. rewrite Zopp_succ, Zopp_pred; now rewrite Zsucc_inj_wd. Qed. -Theorem Zopp_plus_distr : forall n m : Z, - (n + m) == - n + (- m). +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 Zplus_0_l. -intro n. rewrite Zplus_succ_l; do 2 rewrite Zopp_succ; rewrite Zplus_pred_l. +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_minus_distr : forall n m : Z, - (n - m) == - n + m. Proof. -intros n m; rewrite <- Zplus_opp_r, Zopp_plus_distr. +intros n m; rewrite <- Zadd_opp_r, Zopp_add_distr. now rewrite Zopp_involutive. Qed. @@ -188,63 +188,63 @@ Proof. symmetry; apply Zeq_opp_l. Qed. -Theorem Zminus_plus_distr : forall n m p : Z, n - (m + p) == (n - m) - p. +Theorem Zminus_add_distr : forall n m p : Z, n - (m + p) == (n - m) - p. Proof. -intros n m p; rewrite <- Zplus_opp_r, Zopp_plus_distr, Zplus_assoc. -now do 2 rewrite Zplus_opp_r. +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. Proof. -intros n m p; rewrite <- Zplus_opp_r, Zopp_minus_distr, Zplus_assoc. -now rewrite Zplus_opp_r. +intros n m p; rewrite <- Zadd_opp_r, Zopp_minus_distr, Zadd_assoc. +now rewrite Zadd_opp_r. Qed. Theorem minus_opp_l : forall n m : Z, - n - m == - m - n. Proof. -intros n m. do 2 rewrite <- Zplus_opp_r. now rewrite Zplus_comm. +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. Proof. -intros n m; rewrite <- Zplus_opp_r; now rewrite Zopp_involutive. +intros n m; rewrite <- Zadd_opp_r; now rewrite Zopp_involutive. Qed. -Theorem Zplus_minus_swap : forall n m p : Z, n + m - p == n - p + m. +Theorem Zadd_minus_swap : forall n m p : Z, n + m - p == n - p + m. Proof. -intros n m p. rewrite <- Zplus_minus_assoc, <- (Zplus_opp_r n p), <- Zplus_assoc. -now rewrite Zplus_opp_l. +intros n m p. rewrite <- Zadd_minus_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. Proof. -intros n m p. rewrite <- (Zplus_cancel_l (n - m) (n - p) (- n)). -do 2 rewrite Zplus_minus_assoc. rewrite Zplus_opp_diag_l; do 2 rewrite Zminus_0_l. +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. apply Zopp_inj_wd. Qed. Theorem Zminus_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 Zplus_cancel_r. +stepl (n - p + p == m - p + p) by apply Zadd_cancel_r. now do 2 rewrite <- Zminus_minus_distr, Zminus_diag, Zminus_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 (plus or minus) and the indication whether the left or right term +equation (add or minus) and the indication whether the left or right term is moved. *) -Theorem Zplus_move_l : forall n m p : Z, n + m == p <-> m == p - n. +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 Zplus_comm, <- Zplus_minus_assoc, Zminus_diag, Zplus_0_r. +now rewrite Zadd_comm, <- Zadd_minus_assoc, Zminus_diag, Zadd_0_r. Qed. -Theorem Zplus_move_r : forall n m p : Z, n + m == p <-> n == p - m. +Theorem Zadd_move_r : forall n m p : Z, n + m == p <-> n == p - m. Proof. -intros n m p; rewrite Zplus_comm; now apply Zplus_move_l. +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 @@ -253,22 +253,22 @@ the equation. Hence the following two theorems. *) Theorem Zminus_move_l : forall n m p : Z, n - m == p <-> - m == p - n. Proof. -intros n m p; rewrite <- (Zplus_opp_r n m); apply Zplus_move_l. +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. Proof. -intros n m p; rewrite <- (Zplus_opp_r n m). now rewrite Zplus_move_r, Zminus_opp_r. +intros n m p; rewrite <- (Zadd_opp_r n m). now rewrite Zadd_move_r, Zminus_opp_r. Qed. -Theorem Zplus_move_0_l : forall n m : Z, n + m == 0 <-> m == - n. +Theorem Zadd_move_0_l : forall n m : Z, n + m == 0 <-> m == - n. Proof. -intros n m; now rewrite Zplus_move_l, Zminus_0_l. +intros n m; now rewrite Zadd_move_l, Zminus_0_l. Qed. -Theorem Zplus_move_0_r : forall n m : Z, n + m == 0 <-> n == - m. +Theorem Zadd_move_0_r : forall n m : Z, n + m == 0 <-> n == - m. Proof. -intros n m; now rewrite Zplus_move_r, Zminus_0_l. +intros n m; now rewrite Zadd_move_r, Zminus_0_l. Qed. Theorem Zminus_move_0_l : forall n m : Z, n - m == 0 <-> - m == - n. @@ -278,25 +278,25 @@ Qed. Theorem Zminus_move_0_r : forall n m : Z, n - m == 0 <-> n == m. Proof. -intros n m. now rewrite Zminus_move_r, Zplus_0_l. +intros n m. now rewrite Zminus_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 Zplus_simpl_l : forall n m : Z, n + m - n == m. +Theorem Zadd_simpl_l : forall n m : Z, n + m - n == m. Proof. -intros; now rewrite Zplus_minus_swap, Zminus_diag, Zplus_0_l. +intros; now rewrite Zadd_minus_swap, Zminus_diag, Zadd_0_l. Qed. -Theorem Zplus_simpl_r : forall n m : Z, n + m - m == n. +Theorem Zadd_simpl_r : forall n m : Z, n + m - m == n. Proof. -intros; now rewrite <- Zplus_minus_assoc, Zminus_diag, Zplus_0_r. +intros; now rewrite <- Zadd_minus_assoc, Zminus_diag, Zadd_0_r. Qed. Theorem Zminus_simpl_l : forall n m : Z, - n - m + n == - m. Proof. -intros; now rewrite <- Zplus_minus_swap, Zplus_opp_diag_l, Zminus_0_l. +intros; now rewrite <- Zadd_minus_swap, Zadd_opp_diag_l, Zminus_0_l. Qed. Theorem Zminus_simpl_r : forall n m : Z, n - m + m == n. @@ -307,36 +307,36 @@ Qed. (* Now we have two sums or differences; the name includes the two operators and the position of the terms being canceled *) -Theorem Zplus_plus_simpl_l_l : forall n m p : Z, (n + m) - (n + p) == m - p. +Theorem Zadd_add_simpl_l_l : forall n m p : Z, (n + m) - (n + p) == m - p. Proof. -intros n m p. now rewrite (Zplus_comm n m), <- Zplus_minus_assoc, -Zminus_plus_distr, Zminus_diag, Zminus_0_l, Zplus_opp_r. +intros n m p. now rewrite (Zadd_comm n m), <- Zadd_minus_assoc, +Zminus_add_distr, Zminus_diag, Zminus_0_l, Zadd_opp_r. Qed. -Theorem Zplus_plus_simpl_l_r : forall n m p : Z, (n + m) - (p + n) == m - p. +Theorem Zadd_add_simpl_l_r : forall n m p : Z, (n + m) - (p + n) == m - p. Proof. -intros n m p. rewrite (Zplus_comm p n); apply Zplus_plus_simpl_l_l. +intros n m p. rewrite (Zadd_comm p n); apply Zadd_add_simpl_l_l. Qed. -Theorem Zplus_plus_simpl_r_l : forall n m p : Z, (n + m) - (m + p) == n - p. +Theorem Zadd_add_simpl_r_l : forall n m p : Z, (n + m) - (m + p) == n - p. Proof. -intros n m p. rewrite (Zplus_comm n m); apply Zplus_plus_simpl_l_l. +intros n m p. rewrite (Zadd_comm n m); apply Zadd_add_simpl_l_l. Qed. -Theorem Zplus_plus_simpl_r_r : forall n m p : Z, (n + m) - (p + m) == n - p. +Theorem Zadd_add_simpl_r_r : forall n m p : Z, (n + m) - (p + m) == n - p. Proof. -intros n m p. rewrite (Zplus_comm p m); apply Zplus_plus_simpl_r_l. +intros n m p. rewrite (Zadd_comm p m); apply Zadd_add_simpl_r_l. Qed. -Theorem Zminus_plus_simpl_r_l : forall n m p : Z, (n - m) + (m + p) == n + p. +Theorem Zminus_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_plus_distr, Zminus_diag, +intros n m p. now rewrite <- Zminus_minus_distr, Zminus_add_distr, Zminus_diag, Zminus_0_l, Zminus_opp_r. Qed. -Theorem Zminus_plus_simpl_r_r : forall n m p : Z, (n - m) + (p + m) == n + p. +Theorem Zminus_add_simpl_r_r : forall n m p : Z, (n - m) + (p + m) == n + p. Proof. -intros n m p. rewrite (Zplus_comm p m); apply Zminus_plus_simpl_r_l. +intros n m p. rewrite (Zadd_comm p m); apply Zminus_add_simpl_r_l. Qed. (* Of course, there are many other variants *) |