An update on Numbers. Added two files dealing with recursion, for information only.

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

5 files changed, 96 insertions, 22 deletions

diff --git a/theories/Numbers/Integer/Abstract/ZLt.v b/theories/Numbers/Integer/Abstract/ZLt.v
index 27cbe085e1..65a938e54d 100644
--- a/theories/Numbers/Integer/Abstract/ZLt.v
+++ b/theories/Numbers/Integer/Abstract/ZLt.v
@@ -338,7 +338,7 @@ 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 *)
+(* 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.
diff --git a/theories/Numbers/Integer/Abstract/ZPlus.v b/theories/Numbers/Integer/Abstract/ZPlus.v
index b0cebd482d..cbe22077e0 100644
--- a/theories/Numbers/Integer/Abstract/ZPlus.v
+++ b/theories/Numbers/Integer/Abstract/ZPlus.v
@@ -38,7 +38,7 @@ 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 *)
+(* Theorems that are valid for both natural numbers and integers *)
 
 Theorem Zplus_0_r : forall n : Z, n + 0 == n.
 Proof NZplus_0_r.
@@ -70,7 +70,7 @@ Proof NZplus_cancel_l.
 Theorem Zplus_cancel_r : forall n m p : Z, n + p == m + p <-> n == m.
 Proof NZplus_cancel_r.
 
-(** Theorems that are either not valid on N or have different proofs on N and Z *)
+(* 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).
 Proof.
@@ -200,6 +200,11 @@ intros n m p; rewrite <- Zplus_opp_r, Zopp_minus_distr, Zplus_assoc.
 now rewrite Zplus_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.
+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.
diff --git a/theories/Numbers/Integer/Abstract/ZPlusOrder.v b/theories/Numbers/Integer/Abstract/ZPlusOrder.v
index c6d0efe451..079fc356d8 100644
--- a/theories/Numbers/Integer/Abstract/ZPlusOrder.v
+++ b/theories/Numbers/Integer/Abstract/ZPlusOrder.v
@@ -16,7 +16,7 @@ Module ZPlusOrderPropFunct (Import ZAxiomsMod : ZAxiomsSig).
 Module Export ZOrderPropMod := ZOrderPropFunct ZAxiomsMod.
 Open Local Scope IntScope.
 
-(** Theorems that are true on both natural numbers and integers *)
+(* Theorems that are true on both natural numbers and integers *)
 
 Theorem Zplus_lt_mono_l : forall n m p : Z, n < m <-> p + n < p + m.
 Proof NZplus_lt_mono_l.
@@ -87,7 +87,7 @@ Proof NZplus_nonpos_cases.
 Theorem Zplus_nonneg_cases : forall n m : Z, 0 <= n + m -> 0 <= n \/ 0 <= m.
 Proof NZplus_nonneg_cases.
 
-(** Theorems that are either not valid on N or have different proofs on N and Z *)
+(* Theorems that are either not valid on N or have different proofs on N and Z *)
 
 Theorem Zplus_neg_neg : forall n m : Z, n < 0 -> m < 0 -> n + m < 0.
 Proof.
@@ -109,31 +109,50 @@ Proof.
 intros n m H1 H2. rewrite <- (Zplus_0_l 0). now apply Zplus_le_mono.
 Qed.
 
-
 (** Minus and order *)
 
-Theorem Zlt_lt_minus : forall n m : Z, n < m <-> 0 < m - n.
+Theorem Zlt_0_minus : forall n m : Z, 0 < m - n <-> n < m.
 Proof.
-intros n m. stepr (0 + n < m - n + n) by symmetry; apply Zplus_lt_mono_r.
+intros n m. stepl (0 + n < m - n + n) by symmetry; apply Zplus_lt_mono_r.
 rewrite Zplus_0_l; now rewrite Zminus_simpl_r.
 Qed.
 
-Theorem Zle_le_minus : forall n m : Z, n <= m <-> 0 <= m - n.
+Notation Zminus_pos := Zlt_0_minus (only parsing).
+
+Theorem Zle_0_minus : forall n m : Z, 0 <= m - n <-> n <= m.
+Proof.
+intros n m; stepl (0 + n <= m - n + n) by symmetry; apply Zplus_le_mono_r.
+rewrite Zplus_0_l; now rewrite Zminus_simpl_r.
+Qed.
+
+Notation Zminus_nonneg := Zle_0_minus (only parsing).
+
+Theorem Zlt_minus_0 : forall n m : Z, n - m < 0 <-> n < m.
 Proof.
-intros n m; stepr (0 + n <= m - n + n) by symmetry; apply Zplus_le_mono_r.
+intros n m. stepl (n - m + m < 0 + m) by symmetry; apply Zplus_lt_mono_r.
 rewrite Zplus_0_l; now rewrite Zminus_simpl_r.
 Qed.
 
+Notation Zminus_neg := Zlt_minus_0 (only parsing).
+
+Theorem Zle_minus_0 : forall n m : Z, n - m <= 0 <-> n <= m.
+Proof.
+intros n m. stepl (n - m + m <= 0 + m) by symmetry; apply Zplus_le_mono_r.
+rewrite Zplus_0_l; now rewrite Zminus_simpl_r.
+Qed.
+
+Notation Zminus_nonpos := Zle_minus_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 Zplus_lt_mono_l.
-do 2 rewrite Zplus_opp_r. rewrite Zminus_diag. apply Zlt_lt_minus.
+do 2 rewrite Zplus_opp_r. rewrite Zminus_diag. symmetry; apply Zlt_0_minus.
 Qed.
 
 Theorem Zopp_le_mono : forall n m : Z, n <= m <-> - m <= - n.
 Proof.
 intros n m. stepr (m + - m <= m + - n) by symmetry; apply Zplus_le_mono_l.
-do 2 rewrite Zplus_opp_r. rewrite Zminus_diag. apply Zle_le_minus.
+do 2 rewrite Zplus_opp_r. rewrite Zminus_diag. symmetry; apply Zle_0_minus.
 Qed.
 
 Theorem Zopp_pos_neg : forall n : Z, 0 < - n <-> n < 0.
diff --git a/theories/Numbers/Integer/Abstract/ZTimes.v b/theories/Numbers/Integer/Abstract/ZTimes.v
index 89249d1ed9..2ff8fd8dae 100644
--- a/theories/Numbers/Integer/Abstract/ZTimes.v
+++ b/theories/Numbers/Integer/Abstract/ZTimes.v
@@ -26,7 +26,7 @@ Proof NZtimes_0_l.
 Theorem Ztimes_succ_l : forall n m : Z, (S n) * m == n * m + m.
 Proof NZtimes_succ_l.
 
-(** Theorems that are valid for both natural numbers and integers *)
+(* Theorems that are valid for both natural numbers and integers *)
 
 Theorem Ztimes_0_r : forall n : Z, n * 0 == 0.
 Proof NZtimes_0_r.
@@ -68,7 +68,7 @@ Proof NZeq_times_0.
 Theorem Zneq_times_0 : forall n m : Z, n ~= 0 /\ m ~= 0 <-> n * m ~= 0.
 Proof NZneq_times_0.
 
-(** Theorems that are either not valid on N or have different proofs on N and Z *)
+(* Theorems that are either not valid on N or have different proofs on N and Z *)
 
 Theorem Ztimes_pred_r : forall n m : Z, n * (P m) == n * m - n.
 Proof.
diff --git a/theories/Numbers/Integer/Abstract/ZTimesOrder.v b/theories/Numbers/Integer/Abstract/ZTimesOrder.v
index a2360dd72e..0f4cb54a8a 100644
--- a/theories/Numbers/Integer/Abstract/ZTimesOrder.v
+++ b/theories/Numbers/Integer/Abstract/ZTimesOrder.v
@@ -16,8 +16,6 @@ Module ZTimesOrderPropFunct (Import ZAxiomsMod : ZAxiomsSig).
 Module Export ZPlusOrderPropMod := ZPlusOrderPropFunct ZAxiomsMod.
 Open Local Scope IntScope.
 
-(** Theorems that are true on both natural numbers and integers *)
-
 Theorem Ztimes_lt_pred :
   forall p q n m : Z, S p == q -> (p * n < p * m <-> q * n + m < q * m + n).
 Proof NZtimes_lt_pred.
@@ -52,6 +50,12 @@ Proof NZtimes_cancel_l.
 Theorem Ztimes_cancel_r : forall n m p : Z, p ~= 0 -> (n * p == m * p <-> n == m).
 Proof NZtimes_cancel_r.
 
+Theorem Ztimes_id_l : forall n m : Z, m ~= 0 -> (n * m == m <-> n == 1).
+Proof NZtimes_id_l.
+
+Theorem Ztimes_id_r : forall n m : Z, n ~= 0 -> (n * m == n <-> m == 1).
+Proof NZtimes_id_r.
+
 Theorem Ztimes_le_mono_pos_l : forall n m p : Z, 0 < p -> (n <= m <-> p * n <= p * m).
 Proof NZtimes_le_mono_pos_l.
 
@@ -134,6 +138,9 @@ Proof NZeq_times_0.
 Theorem Zneq_times_0 : forall n m : Z, n ~= 0 /\ m ~= 0 <-> n * m ~= 0.
 Proof NZneq_times_0.
 
+Theorem Zeq_square_0 : forall n : Z, n * n == 0 <-> n == 0.
+Proof NZeq_square_0.
+
 Theorem Zeq_times_0_l : forall n m : Z, n * m == 0 -> m ~= 0 -> n == 0.
 Proof NZeq_times_0_l.
 
@@ -185,6 +192,20 @@ Qed.
 
 Notation Ztimes_nonpos := Zle_times_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 Ztimes_neg_neg.
+now apply Ztimes_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.
 
@@ -228,8 +249,6 @@ Qed.
 Theorem Ztimes_2_mono_l : forall n m : Z, n < m -> 1 + (1 + 1) * n < (1 + 1) * m.
 Proof NZtimes_2_mono_l.
 
-(** Theorems that are either not valid on N or have different proofs on N and Z *)
-
 Theorem Zlt_1_times_neg : forall n m : Z, n < -1 -> m < 0 -> 1 < n * m.
 Proof.
 intros n m H1 H2. apply -> (NZtimes_lt_mono_neg_r m) in H1.
@@ -253,7 +272,7 @@ apply <- Zopp_neg_pos in H2. now apply Zlt_n1_r with (- m).
 assumption.
 Qed.
 
-Theorem Zlt_1_l_times : forall n m : Z, 1 < n -> n * m < -1 \/ n * m == 0 \/ 1 < n * m.
+Theorem Zlt_1_times_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_times_n1_neg.
@@ -261,7 +280,7 @@ right; left; now rewrite H1, Ztimes_0_r.
 right; right; now apply Zlt_1_times_pos.
 Qed.
 
-Theorem Zlt_n1_r_times : forall n m : Z, n < -1 -> n * m < -1 \/ n * m == 0 \/ 1 < n * m.
+Theorem Zlt_n1_times_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_times_neg.
@@ -278,16 +297,47 @@ assert (H2 : 1 < 0) by now apply Zlt_trans with (-1). false_hyp H2 Znlt_succ_dia
 Z0_pos_neg n.
 intros m H; rewrite Ztimes_0_l in H; false_hyp H Zneq_succ_diag_r.
 intros n H; split; apply <- Zle_succ_l in H; le_elim H.
-intros m H1; apply (Zlt_1_l_times n m) in H.
+intros m H1; apply (Zlt_1_times_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_l_times n m) in H. rewrite Ztimes_opp_l in H1;
+intros m H1; apply (Zlt_1_times_l n m) in H. rewrite Ztimes_opp_l in H1;
 apply -> Zeq_opp_l in H1. rewrite H1 in H; destruct H as [H | [H | H]].
 false_hyp H Zlt_irrefl. apply -> Zeq_opp_l in H. rewrite Zopp_0 in H.
 false_hyp H Zneq_succ_diag_l. false_hyp H F.
 intros; right; symmetry; now apply Zopp_wd.
 Qed.
 
+Theorem Zlt_times_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 Ztimes_1_r.
+now apply Ztimes_lt_mono_neg_l.
+Qed.
+
+Theorem Zlt_times_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 Ztimes_1_r.
+now apply Ztimes_lt_mono_pos_l.
+Qed.
+
+Theorem Zle_times_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 Ztimes_1_r.
+now apply Ztimes_le_mono_neg_l.
+Qed.
+
+Theorem Zle_times_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 Ztimes_1_r.
+now apply Ztimes_le_mono_pos_l.
+Qed.
+
+Theorem Zlt_times_r : forall n m p : Z, 0 < n -> 1 < p -> n < m -> n < m * p.
+Proof.
+intros. stepl (n * 1) by now rewrite Ztimes_1_r.
+apply Ztimes_lt_mono_nonneg.
+now apply Zlt_le_incl. assumption. apply Zle_0_1. assumption.
+Qed.
+
 End ZTimesOrderPropFunct.