Update on Numbers; renamed ZOrder.v to ZLt to remove clash with ZArith/Zorder on MacOS.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10323 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 138 insertions, 32 deletions

diff --git a/theories/Numbers/Integer/Abstract/ZPlus.v b/theories/Numbers/Integer/Abstract/ZPlus.v
index 16fe114313..b0cebd482d 100644
--- a/theories/Numbers/Integer/Abstract/ZPlus.v
+++ b/theories/Numbers/Integer/Abstract/ZPlus.v
@@ -85,7 +85,7 @@ intros n m; rewrite (Zplus_comm n (P m)), (Zplus_comm n m);
 apply Zplus_pred_l.
 Qed.
 
-Theorem Zplus_opp_minus : forall n m : Z, n + (- m) == n - m.
+Theorem Zplus_opp_r : forall n m : Z, n + (- m) == n - m.
 Proof.
 NZinduct m.
 rewrite Zopp_0; rewrite Zminus_0_r; now rewrite Zplus_0_r.
@@ -94,12 +94,12 @@ Qed.
 
 Theorem Zminus_0_l : forall n : Z, 0 - n == - n.
 Proof.
-intro n; rewrite <- Zplus_opp_minus; now rewrite Zplus_0_l.
+intro n; rewrite <- Zplus_opp_r; now rewrite Zplus_0_l.
 Qed.
 
 Theorem Zminus_succ_l : forall n m : Z, S n - m == S (n - m).
 Proof.
-intros n m; do 2 rewrite <- Zplus_opp_minus; now rewrite Zplus_succ_l.
+intros n m; do 2 rewrite <- Zplus_opp_r; now rewrite Zplus_succ_l.
 Qed.
 
 Theorem Zminus_pred_l : forall n m : Z, P n - m == P (n - m).
@@ -127,24 +127,24 @@ now rewrite Zminus_0_r.
 intro n. rewrite Zminus_succ_r, Zminus_succ_l; now rewrite Zpred_succ.
 Qed.
 
-Theorem Zplus_opp_r : forall n : Z, n + (- n) == 0.
+Theorem Zplus_opp_diag_l : forall n : Z, - n + n == 0.
 Proof.
-intro n; rewrite Zplus_opp_minus; now rewrite Zminus_diag.
+intro n; now rewrite Zplus_comm, Zplus_opp_r, Zminus_diag.
 Qed.
 
-Theorem Zplus_opp_l : forall n : Z, - n + n == 0.
+Theorem Zplus_opp_diag_r : forall n : Z, n + (- n) == 0.
 Proof.
-intro n; rewrite Zplus_comm; apply Zplus_opp_r.
+intro n; rewrite Zplus_comm; apply Zplus_opp_diag_l.
 Qed.
 
-Theorem Zminus_swap : forall n m : Z, - m + n == n - m.
+Theorem Zplus_opp_l : forall n m : Z, - m + n == n - m.
 Proof.
-intros n m; rewrite <- Zplus_opp_minus; now rewrite Zplus_comm.
+intros n m; rewrite <- Zplus_opp_r; now rewrite Zplus_comm.
 Qed.
 
 Theorem Zplus_minus_assoc : forall n m p : Z, n + (m - p) == (n + m) - p.
 Proof.
-intros n m p; do 2 rewrite <- Zplus_opp_minus; now rewrite Zplus_assoc.
+intros n m p; do 2 rewrite <- Zplus_opp_r; now rewrite Zplus_assoc.
 Qed.
 
 Theorem Zopp_involutive : forall n : Z, - (- n) == n.
@@ -164,7 +164,7 @@ Qed.
 
 Theorem Zopp_minus_distr : forall n m : Z, - (n - m) == - n + m.
 Proof.
-intros n m; rewrite <- Zplus_opp_minus, Zopp_plus_distr.
+intros n m; rewrite <- Zplus_opp_r, Zopp_plus_distr.
 now rewrite Zopp_involutive.
 Qed.
 
@@ -178,57 +178,163 @@ Proof.
 intros n m; split; [apply Zopp_inj | apply Zopp_wd].
 Qed.
 
+Theorem Zeq_opp_l : forall n m : Z, - n == m <-> n == - m.
+Proof.
+intros n m. now rewrite <- (Zopp_inj_wd (- n) m), Zopp_involutive.
+Qed.
+
+Theorem Zeq_opp_r : forall n m : Z, n == - m <-> - n == m.
+Proof.
+symmetry; apply Zeq_opp_l.
+Qed.
+
 Theorem Zminus_plus_distr : forall n m p : Z, n - (m + p) == (n - m) - p.
 Proof.
-intros n m p; rewrite <- Zplus_opp_minus, Zopp_plus_distr, Zplus_assoc.
-now do 2 rewrite Zplus_opp_minus.
+intros n m p; rewrite <- Zplus_opp_r, Zopp_plus_distr, Zplus_assoc.
+now do 2 rewrite Zplus_opp_r.
 Qed.
 
 Theorem Zminus_minus_distr : forall n m p : Z, n - (m - p) == (n - m) + p.
 Proof.
-intros n m p; rewrite <- Zplus_opp_minus, Zopp_minus_distr, Zplus_assoc.
-now rewrite Zplus_opp_minus.
+intros n m p; rewrite <- Zplus_opp_r, Zopp_minus_distr, Zplus_assoc.
+now rewrite Zplus_opp_r.
 Qed.
 
-Theorem Zminus_opp : forall n m : Z, n - (- m) == n + m.
+Theorem Zminus_opp_r : forall n m : Z, n - (- m) == n + m.
 Proof.
-intros n m; rewrite <- Zplus_opp_minus; now rewrite Zopp_involutive.
+intros n m; rewrite <- Zplus_opp_r; now rewrite Zopp_involutive.
 Qed.
 
 Theorem Zplus_minus_swap : forall n m p : Z, n + m - p == n - p + m.
 Proof.
-intros n m p. rewrite <- Zplus_minus_assoc, <- (Zplus_opp_minus n p), <- Zplus_assoc.
-now rewrite Zminus_swap.
+intros n m p. rewrite <- Zplus_minus_assoc, <- (Zplus_opp_r n p), <- Zplus_assoc.
+now rewrite Zplus_opp_l.
 Qed.
 
-Theorem Zminus_plus_diag : forall n m : Z, n - m + m == n.
+Theorem Zminus_cancel_l : forall n m p : Z, n - m == n - p <-> m == p.
 Proof.
-intros; rewrite <- Zplus_minus_swap; rewrite <- Zplus_minus_assoc;
-rewrite Zminus_diag; now rewrite Zplus_0_r.
+intros n m p. rewrite <- (Zplus_cancel_l (n - m) (n - p) (- n)).
+do 2 rewrite Zplus_minus_assoc. rewrite Zplus_opp_diag_l; do 2 rewrite Zminus_0_l.
+apply Zopp_inj_wd.
 Qed.
 
-Theorem Zplus_minus_diag : forall n m : Z, n + m - m == n.
+Theorem Zminus_cancel_r : forall n m p : Z, n - p == m - p <-> n == m.
 Proof.
-intros; rewrite <- Zplus_minus_assoc; rewrite Zminus_diag; now rewrite Zplus_0_r.
+intros n m p.
+stepl (n - p + p == m - p + p) by apply Zplus_cancel_r.
+now do 2 rewrite <- Zminus_minus_distr, Zminus_diag, Zminus_0_r.
 Qed.
 
-Theorem Zplus_minus_eq_l : forall n m p : Z, m + p == n <-> n - m == p.
+(* The next several theorems are devoted to moving terms from one side of
+an equation to the other. The name contains the operation in the original
+equation (plus or minus) and the indication whether the left or right term
+is moved. *)
+
+Theorem Zplus_move_l : forall n m p : Z, n + m == p <-> m == p - n.
 Proof.
 intros n m p.
-stepl (-m + (m + p) == -m + n) by apply Zplus_cancel_l.
-stepr (p == n - m) by now split.
-rewrite Zplus_assoc, Zplus_opp_l, Zplus_0_l. now rewrite Zminus_swap.
+stepl (n + m - n == p - n) by apply Zminus_cancel_r.
+now rewrite Zplus_comm, <- Zplus_minus_assoc, Zminus_diag, Zplus_0_r.
+Qed.
+
+Theorem Zplus_move_r : forall n m p : Z, n + m == p <-> n == p - m.
+Proof.
+intros n m p; rewrite Zplus_comm; now apply Zplus_move_l.
+Qed.
+
+(* The two theorems above do not allow rewriting subformulas of the form
+n - m == p to n == p + m since subtraction is in the right-hand side of
+the equation. Hence the following two theorems. *)
+
+Theorem Zminus_move_l : forall n m p : Z, n - m == p <-> - m == p - n.
+Proof.
+intros n m p; rewrite <- (Zplus_opp_r n m); apply Zplus_move_l.
 Qed.
 
-Theorem Zplus_minus_eq_r : forall n m p : Z, m + p == n <-> n - p == m.
+Theorem Zminus_move_r : forall n m p : Z, n - m == p <-> n == p + m.
 Proof.
-intros n m p; rewrite Zplus_comm; now apply Zplus_minus_eq_l.
+intros n m p; rewrite <- (Zplus_opp_r n m). now rewrite Zplus_move_r, Zminus_opp_r.
 Qed.
 
-Theorem Zminus_eq : forall n m : Z, n - m == 0 <-> n == m.
+Theorem Zplus_move_0_l : forall n m : Z, n + m == 0 <-> m == - n.
 Proof.
-intros n m. rewrite <- Zplus_minus_eq_l, Zplus_0_r; now split.
+intros n m; now rewrite Zplus_move_l, Zminus_0_l.
 Qed.
 
+Theorem Zplus_move_0_r : forall n m : Z, n + m == 0 <-> n == - m.
+Proof.
+intros n m; now rewrite Zplus_move_r, Zminus_0_l.
+Qed.
+
+Theorem Zminus_move_0_l : forall n m : Z, n - m == 0 <-> - m == - n.
+Proof.
+intros n m. now rewrite Zminus_move_l, Zminus_0_l.
+Qed.
+
+Theorem Zminus_move_0_r : forall n m : Z, n - m == 0 <-> n == m.
+Proof.
+intros n m. now rewrite Zminus_move_r, Zplus_0_l.
+Qed.
+
+(* The following section is devoted to cancellation of like terms. The name
+includes the first operator and the position of the term being canceled. *)
+
+Theorem Zplus_simpl_l : forall n m : Z, n + m - n == m.
+Proof.
+intros; now rewrite Zplus_minus_swap, Zminus_diag, Zplus_0_l.
+Qed.
+
+Theorem Zplus_simpl_r : forall n m : Z, n + m - m == n.
+Proof.
+intros; now rewrite <- Zplus_minus_assoc, Zminus_diag, Zplus_0_r.
+Qed.
+
+Theorem Zminus_simpl_l : forall n m : Z, - n - m + n == - m.
+Proof.
+intros; now rewrite <- Zplus_minus_swap, Zplus_opp_diag_l, Zminus_0_l.
+Qed.
+
+Theorem Zminus_simpl_r : forall n m : Z, n - m + m == n.
+Proof.
+intros; now rewrite <- Zminus_minus_distr, Zminus_diag, Zminus_0_r.
+Qed.
+
+(* Now we have two sums or differences; the name includes the two operators
+and the position of the terms being canceled *)
+
+Theorem Zplus_plus_simpl_l_l : forall n m p : Z, (n + m) - (n + p) == m - p.
+Proof.
+intros n m p. now rewrite (Zplus_comm n m), <- Zplus_minus_assoc,
+Zminus_plus_distr, Zminus_diag, Zminus_0_l, Zplus_opp_r.
+Qed.
+
+Theorem Zplus_plus_simpl_l_r : forall n m p : Z, (n + m) - (p + n) == m - p.
+Proof.
+intros n m p. rewrite (Zplus_comm p n); apply Zplus_plus_simpl_l_l.
+Qed.
+
+Theorem Zplus_plus_simpl_r_l : forall n m p : Z, (n + m) - (m + p) == n - p.
+Proof.
+intros n m p. rewrite (Zplus_comm n m); apply Zplus_plus_simpl_l_l.
+Qed.
+
+Theorem Zplus_plus_simpl_r_r : forall n m p : Z, (n + m) - (p + m) == n - p.
+Proof.
+intros n m p. rewrite (Zplus_comm p m); apply Zplus_plus_simpl_r_l.
+Qed.
+
+Theorem Zminus_plus_simpl_r_l : forall n m p : Z, (n - m) + (m + p) == n + p.
+Proof.
+intros n m p. now rewrite <- Zminus_minus_distr, Zminus_plus_distr, Zminus_diag,
+Zminus_0_l, Zminus_opp_r.
+Qed.
+
+Theorem Zminus_plus_simpl_r_r : forall n m p : Z, (n - m) + (p + m) == n + p.
+Proof.
+intros n m p. rewrite (Zplus_comm p m); apply Zminus_plus_simpl_r_l.
+Qed.
+
+(* Of course, there are many other variants *)
+
 End ZPlusPropFunct.