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

4 files changed, 22 insertions, 0 deletions

diff --git a/theories/Numbers/NatInt/NZAxioms.v b/theories/Numbers/NatInt/NZAxioms.v
index f218ed6a64..6bdfe56426 100644
--- a/theories/Numbers/NatInt/NZAxioms.v
+++ b/theories/Numbers/NatInt/NZAxioms.v
@@ -23,6 +23,9 @@ Parameter Inline NZplus : NZ -> NZ -> NZ.
 Parameter Inline NZminus : NZ -> NZ -> NZ.
 Parameter Inline NZtimes : NZ -> NZ -> NZ.
 
+(* Unary minus (opp) is not defined on natural numbers, so we have it for
+integers only *)
+
 Axiom NZeq_equiv : equiv NZ NZeq.
 Add Relation NZ NZeq
  reflexivity proved by (proj1 NZeq_equiv)
diff --git a/theories/Numbers/NatInt/NZBase.v b/theories/Numbers/NatInt/NZBase.v
index d8a9f06871..730d8a00fd 100644
--- a/theories/Numbers/NatInt/NZBase.v
+++ b/theories/Numbers/NatInt/NZBase.v
@@ -55,6 +55,7 @@ left-inverse to the successor at this point *)
 Section CentralInduction.
 
 Variable A : NZ -> Prop.
+
 (* FIXME: declaring "A : predicate NZ" leads to the error during the
 declaration of the morphism below because the "predicate NZ" is not
 recognized as a type of function. Maybe it should do "eval hnf" or
diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v
index 95df8e7473..0708e060a2 100644
--- a/theories/Numbers/NatInt/NZOrder.v
+++ b/theories/Numbers/NatInt/NZOrder.v
@@ -243,6 +243,8 @@ now left.
 right; intro H1; rewrite H1 in H; false_hyp H NZlt_irrefl.
 Qed.
 
+(* DNE stands for double-negation elimination *)
+
 Theorem NZeq_dne : forall n m, ~ ~ n == m <-> n == m.
 Proof.
 intros n m; split; intro H.
diff --git a/theories/Numbers/NatInt/NZTimesOrder.v b/theories/Numbers/NatInt/NZTimesOrder.v
index aac823dc40..51d2172dec 100644
--- a/theories/Numbers/NatInt/NZTimesOrder.v
+++ b/theories/Numbers/NatInt/NZTimesOrder.v
@@ -121,6 +121,17 @@ Proof.
 intros n m p. rewrite (NZtimes_comm n p), (NZtimes_comm m p); apply NZtimes_cancel_l.
 Qed.
 
+Theorem NZtimes_id_l : forall n m : NZ, m ~= 0 -> (n * m == m <-> n == 1).
+Proof.
+intros n m H.
+stepl (n * m == 1 * m) by now rewrite NZtimes_1_l. now apply NZtimes_cancel_r.
+Qed.
+
+Theorem NZtimes_id_r : forall n m : NZ, n ~= 0 -> (n * m == n <-> m == 1).
+Proof.
+intros n m; rewrite NZtimes_comm; apply NZtimes_id_l.
+Qed.
+
 Theorem NZtimes_le_mono_pos_l : forall n m p : NZ, 0 < p -> (n <= m <-> p * n <= p * m).
 Proof.
 intros n m p H; do 2 rewrite NZlt_eq_cases.
@@ -224,6 +235,11 @@ split; intro H1; rewrite H1 in H;
 (rewrite NZtimes_0_l in H || rewrite NZtimes_0_r in H); now apply H.
 Qed.
 
+Theorem NZeq_square_0 : forall n : NZ, n * n == 0 <-> n == 0.
+Proof.
+intro n; rewrite NZeq_times_0; tauto.
+Qed.
+
 Theorem NZeq_times_0_l : forall n m : NZ, n * m == 0 -> m ~= 0 -> n == 0.
 Proof.
 intros n m H1 H2. apply -> NZeq_times_0 in H1. destruct H1 as [H1 | H1].