An update on theories/Numbers.

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

8 files changed, 156 insertions, 84 deletions

diff --git a/theories/Numbers/Natural/Abstract/NAxioms.v b/theories/Numbers/Natural/Abstract/NAxioms.v
new file mode 100644
index 0000000000..a30c816822
--- /dev/null
+++ b/theories/Numbers/Natural/Abstract/NAxioms.v
@@ -0,0 +1,39 @@
+Require Export NumPrelude.
+Require Export NZAxioms.
+
+Set Implicit Arguments.
+
+Module Type NAxiomsSig.
+Declare Module Export NZOrdAxiomsMod : NZOrdAxiomsSig.
+Open Local Scope NatIntScope.
+
+Notation N := NZ (only parsing).
+Notation E := NZE (only parsing).
+
+Parameter Inline recursion : forall A : Set, A -> (N -> A -> A) -> N -> A.
+Implicit Arguments recursion [A].
+
+Axiom pred_0 : P 0 == 0.
+
+Axiom recursion_wd : forall (A : Set) (EA : relation A),
+  forall a a' : A, EA a a' ->
+    forall f f' : N -> A -> A, eq_fun2 E EA EA f f' ->
+      forall x x' : N, x == x' ->
+        EA (recursion a f x) (recursion a' f' x').
+
+Axiom recursion_0 :
+  forall (A : Set) (a : A) (f : N -> A -> A), recursion a f 0 = a.
+
+Axiom recursion_succ :
+  forall (A : Set) (EA : relation A) (a : A) (f : N -> A -> A),
+    EA a a -> fun2_wd E EA EA f ->
+      forall n : N, EA (recursion a f (S n)) (f n (recursion a f n)).
+
+End NAxiomsSig.
+
+
+(*
+ Local Variables:
+ tags-file-name: "~/coq/trunk/theories/Numbers/TAGS"
+ End:
+*)
diff --git a/theories/Numbers/Natural/Abstract/NBase.v b/theories/Numbers/Natural/Abstract/NBase.v
index b8940027c0..b999240fb8 100644
--- a/theories/Numbers/Natural/Abstract/NBase.v
+++ b/theories/Numbers/Natural/Abstract/NBase.v
@@ -2,13 +2,12 @@ Require Export NAxioms.
 Require Import NZTimesOrder. (* The last property functor on NZ, which subsumes all others *)
 
 Module NBasePropFunct (Import NAxiomsMod : NAxiomsSig).
-Open Local Scope NatScope.
+Open Local Scope NatIntScope.
 
 (* We call the last property functor on NZ, which includes all the previous
 ones, to get all properties of NZ at once. This way we will include them
 only one time. *)
 
-Module NZOrdAxiomsMod := NNZFunct NAxiomsMod.
 Module Export NZTimesOrderMod := NZTimesOrderPropFunct NZOrdAxiomsMod.
 
 (* Here we probably need to re-prove all axioms declared in NAxioms.v to
@@ -20,20 +19,12 @@ this way, one only has to consult, for example, NPlus.v to see all
 available properties for plus (i.e., one does not have to go to NAxioms.v
 and NZPlus.v). *)
 
-Theorem E_equiv : equiv N E.
-Proof E_equiv.
-
-Theorem induction :
-  forall A : N -> Prop, predicate_wd E A ->
-    A 0 -> (forall n : N, A n -> A (S n)) -> forall n : N, A n.
-Proof induction.
+Theorem pred_succ : forall n : N, P (S n) == n.
+Proof NZpred_succ.
 
 Theorem pred_0 : P 0 == 0.
 Proof pred_0.
 
-Theorem pred_succ : forall n : N, P (S n) == n.
-Proof pred_succ.
-
 Theorem neq_symm : forall n m : N, n ~= m -> m ~= n.
 Proof NZneq_symm.
 
@@ -46,37 +37,79 @@ Proof NZsucc_inj_wd.
 Theorem succ_inj_wd_neg : forall n m : N, S n ~= S m <-> n ~= m.
 Proof NZsucc_inj_wd_neg.
 
+(* Now we prove that the successor of a number is not zero by defining a
+function (by recursion) that maps 0 to false and the successor to true *)
+
+Definition if_zero (A : Set) (a b : A) (n : N) : A :=
+  recursion a (fun _ _ => b) n.
+
+Add Morphism if_zero with signature @eq ==> @eq ==> E ==> @eq as if_zero_wd.
+Proof.
+intros; unfold if_zero. apply recursion_wd with (EA := (@eq A)).
+reflexivity. unfold eq_fun2; now intros. assumption.
+Qed.
+
+Theorem if_zero_0 : forall (A : Set) (a b : A), if_zero A a b 0 = a.
+Proof.
+unfold if_zero; intros; now rewrite recursion_0.
+Qed.
+
+Theorem if_zero_succ : forall (A : Set) (a b : A) (n : N), if_zero A a b (S n) = b.
+Proof.
+intros; unfold if_zero.
+now rewrite (@recursion_succ A (@eq A)); [| | unfold fun2_wd; now intros].
+Qed.
+
+Implicit Arguments if_zero [A].
+
+Theorem neq_succ_0 : forall n : N, ~ S n == 0.
+Proof.
+intros n H.
+assert (true = false); [| discriminate].
+replace true with (if_zero false true (S n)) by apply if_zero_succ.
+pattern false at 2; replace false with (if_zero false true 0) by apply if_zero_0.
+now rewrite H.
+Qed.
+
+(* Next, we show that all numbers are nonnegative and recover regular induction
+from the bidirectional induction on NZ *)
+
+Theorem le_0_l : forall n : N, 0 <= n.
+Proof.
+NZinduct n.
+le_equal.
+intro n; split.
+apply NZle_le_succ.
+intro H; apply -> NZle_succ_le_or_eq_succ in H; destruct H as [H | H].
+assumption.
+symmetry in H; false_hyp H neq_succ_0.
+Qed.
+
+Theorem induction :
+  forall A : N -> Prop, predicate_wd E A ->
+    A 0 -> (forall n : N, A n -> A (S n)) -> forall n : N, A n.
+Proof.
+intros A A_wd A0 AS n; apply NZright_induction with 0; try assumption.
+intros; auto; apply le_0_l. apply le_0_l.
+Qed.
+
 (* The theorems NZinduction, NZcentral_induction and the tactic NZinduct
-refer to bidirectional induction, which is not so useful on natural
+refer to bidirectional induction, which is not useful on natural
 numbers. Therefore, we define a new induction tactic for natural numbers.
 We do not have to call "Declare Left Step" and "Declare Right Step"
 commands again, since the data for stepl and stepr tactics is inherited
-from NZ. *)
+from N. *)
 
-Tactic Notation "induct" ident(n) := induction_maker n ltac:(apply induction).
-(* FIXME: "Ltac induct n := induction_maker n ltac:(apply induction)" does not work (bug 1703) *)
+Ltac induct n := induction_maker n ltac:(apply induction).
 
-(* Now we add properties peculiar to natural numbers *)
-
-Theorem nondep_induction :
+Theorem case_analysis :
   forall A : N -> Prop, predicate_wd E A ->
     A 0 -> (forall n : N, A (S n)) -> forall n : N, A n.
 Proof.
 intros; apply induction; auto.
 Qed.
 
-Tactic Notation "nondep_induct" ident(n) :=
-  induction_maker n ltac:(apply nondep_induction).
-
-(* The fact "forall n : N, S n ~= 0" can be proved either by building a
-function (using recursion) that maps 0 ans S n to two provably different
-terms, or from the axioms of order *)
-
-Theorem neq_succ_0 : forall n : N, S n ~= 0.
-Proof.
-intros n H. apply nlt_0_r with n. rewrite <- H.
-apply <- lt_succ_le. apply <- le_lt_or_eq. now right.
-Qed.
+Ltac cases n := induction_maker n ltac:(apply case_analysis).
 
 Theorem neq_0 : ~ forall n, n == 0.
 Proof.
@@ -85,19 +118,21 @@ Qed.
 
 Theorem neq_0_succ : forall n, n ~= 0 <-> exists m, n == S m.
 Proof.
-nondep_induct n. split; intro H;
+cases n. split; intro H;
 [now elim H | destruct H as [m H]; symmetry in H; false_hyp H neq_succ_0].
 intro n; split; intro H; [now exists n | apply neq_succ_0].
 Qed.
 
 Theorem zero_or_succ : forall n, n == 0 \/ exists m, n == S m.
 Proof.
-nondep_induct n; [now left | intros n; right; now exists n].
+cases n.
+now left.
+intro n; right; now exists n.
 Qed.
 
 Theorem eq_pred_0 : forall n : N, P n == 0 <-> n == 0 \/ n == 1.
 Proof.
-nondep_induct n.
+cases n.
 rewrite pred_0. setoid_replace (0 == 1) with False using relation iff. tauto.
 split; intro H; [symmetry in H; false_hyp H neq_succ_0 | elim H].
 intro n. rewrite pred_succ. rewrite_false (S n == 0) neq_succ_0.
@@ -106,18 +141,18 @@ Qed.
 
 Theorem succ_pred : forall n : N, n ~= 0 -> S (P n) == n.
 Proof.
-nondep_induct n.
+cases n.
 intro H; elimtype False; now apply H.
 intros; now rewrite pred_succ.
 Qed.
 
 Theorem pred_inj : forall n m : N, n ~= 0 -> m ~= 0 -> P n == P m -> n == m.
 Proof.
-intros n m; nondep_induct n.
+intros n m; cases n.
 intros H; elimtype False; now apply H.
-intros n H1; nondep_induct m.
+intros n _; cases m.
 intros H; elimtype False; now apply H.
-intros m H2 H3. do 2 rewrite pred_succ in H3. now apply succ_wd.
+intros m H2 H3. do 2 rewrite pred_succ in H3. now rewrite H3.
 Qed.
 
 (* The following induction principle is useful for reasoning about, e.g.,
@@ -144,7 +179,7 @@ Qed.
 
 End PairInduction.
 
-Tactic Notation "pair_induct" ident(n) := induction_maker n ltac:(apply pair_induction).
+(*Ltac pair_induct n := induction_maker n ltac:(apply pair_induction).*)
 
 (* The following is useful for reasoning about, e.g., Ackermann function *)
 Section TwoDimensionalInduction.
@@ -171,11 +206,11 @@ Qed.
 
 End TwoDimensionalInduction.
 
-Tactic Notation "two_dim_induct" ident(n) ident(m) :=
+(*Ltac two_dim_induct n m :=
   try intros until n;
   try intros until m;
   pattern n, m; apply two_dim_induction; clear n m;
-  [solve_rel_wd | | | ].
+  [solve_rel_wd | | | ].*)
 
 Section DoubleInduction.
 
@@ -193,12 +228,12 @@ Theorem double_induction :
    (forall n m : N, R n m -> R (S n) (S m)) -> forall n m : N, R n m.
 Proof.
 intros H1 H2 H3; induct n; auto.
-intros n IH; nondep_induct m; auto.
+intros n H; cases m; auto.
 Qed.
 
 End DoubleInduction.
 
-Tactic Notation "double_induct" ident(n) ident(m) :=
+Ltac double_induct n m :=
   try intros until n;
   try intros until m;
   pattern n, m; apply double_induction; clear n m;
diff --git a/theories/Numbers/Natural/Abstract/NMinus.v b/theories/Numbers/Natural/Abstract/NMinus.v
index 0af5c22fd2..8111261239 100644
--- a/theories/Numbers/Natural/Abstract/NMinus.v
+++ b/theories/Numbers/Natural/Abstract/NMinus.v
@@ -2,13 +2,13 @@ Require Export NTimesOrder.
 
 Module NMinusPropFunct (Import NAxiomsMod : NAxiomsSig).
 Module Export NTimesOrderPropMod := NTimesOrderPropFunct NAxiomsMod.
-Open Local Scope NatScope.
+Open Local Scope NatIntScope.
 
 Theorem minus_0_r : forall n : N, n - 0 == n.
-Proof minus_0_r.
+Proof NZminus_0_r.
 
 Theorem minus_succ_r : forall n m : N, n - (S m) == P (n - m).
-Proof minus_succ_r.
+Proof NZminus_succ_r.
 
 Theorem minus_1_r : forall n : N, n - 1 == P n.
 Proof.
@@ -85,7 +85,7 @@ 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 plus_0_l.
 intros n m IH H1. rewrite minus_succ in H1. apply IH in H1.
-rewrite plus_succ_l; now apply succ_wd.
+rewrite plus_succ_l; now rewrite H1.
 Qed.
 
 Theorem minus_plus_distr : forall n m p : N, n - (m + p) == (n - m) - p.
@@ -126,7 +126,7 @@ Qed.
 
 Theorem times_pred_r : forall n m : N, n * (P m) == n * m - n.
 Proof.
-intro n; nondep_induct m.
+intros n m; cases m.
 now rewrite pred_0, times_0_r, minus_0_l.
 intro m; rewrite pred_succ, times_succ_r, <- plus_minus_assoc.
 le_equal.
diff --git a/theories/Numbers/Natural/Abstract/NMiscFunct.v b/theories/Numbers/Natural/Abstract/NMiscFunct.v
index 82a9224533..362dc05164 100644
--- a/theories/Numbers/Natural/Abstract/NMiscFunct.v
+++ b/theories/Numbers/Natural/Abstract/NMiscFunct.v
@@ -164,7 +164,7 @@ Qed.
 
 Theorem lt_0 : forall n, ~ lt n 0.
 Proof.
-nondep_induct n.
+ases/g
 rewrite lt_base_eq; rewrite if_zero_0; now intro.
 intros n; rewrite lt_step_eq. rewrite recursion_0. now intro.
 Qed.
@@ -196,10 +196,10 @@ Theorem lt_succ : forall m n, lt m (S n) <-> le m n.
 Proof.
 assert (A : forall m n, lt m (S n) <-> lt m n \/ m == n).
 induct m.
-nondep_induct n;
+ases/g
 [split; intro; [now right | apply lt_0_1] |
 intro n; split; intro; [left |]; apply lt_0_succn].
-intros n IH. nondep_induct n0.
+ases/g
 split.
 intro. assert (H1 : lt n 0); [now apply -> lt_succn_succm | false_hyp H1 lt_0].
 intro H; destruct H as [H | H].
diff --git a/theories/Numbers/Natural/Abstract/NOrder.v b/theories/Numbers/Natural/Abstract/NOrder.v
index 773f5d97ee..e8311c63c4 100644
--- a/theories/Numbers/Natural/Abstract/NOrder.v
+++ b/theories/Numbers/Natural/Abstract/NOrder.v
@@ -2,20 +2,17 @@ Require Export NTimes.
 
 Module NOrderPropFunct (Import NAxiomsMod : NAxiomsSig).
 Module Export NTimesPropMod := NTimesPropFunct NAxiomsMod.
-Open Local Scope NatScope.
+Open Local Scope NatIntScope.
 
 (* The tactics le_less, le_equal and le_elim are inherited from NZOrder.v *)
 
 (* Axioms *)
 
 Theorem le_lt_or_eq : forall x y, x <= y <-> x < y \/ x == y.
-Proof le_lt_or_eq.
-
-Theorem nlt_0_r : forall x, ~ (x < 0).
-Proof nlt_0_r.
+Proof NZle_lt_or_eq.
 
 Theorem lt_succ_le : forall x y, x < S y <-> x <= y.
-Proof lt_succ_le.
+Proof NZlt_succ_le.
 
 (* Renaming theorems from NZOrder.v *)
 
@@ -195,11 +192,11 @@ Proof NZle_ind.
 
 (** Theorems that are true for natural numbers but not for integers *)
 
-Theorem le_0_l : forall n : N, 0 <= n.
+(* "le_0_l : forall n : N, 0 <= n" was proved in NBase.v *)
+
+Theorem nlt_0_r : forall n : N, ~ n < 0.
 Proof.
-induct n.
-now le_equal.
-intros; now apply le_le_succ.
+intro n; apply -> le_nlt. apply le_0_l.
 Qed.
 
 Theorem nle_succ_0 : forall n, ~ (S n <= 0).
@@ -228,19 +225,19 @@ Qed.
 
 Theorem neq_0_lt_0 : forall n, n ~= 0 <-> 0 < n.
 Proof.
-nondep_induct n.
+cases n.
 split; intro H; [now elim H | intro; now apply lt_irrefl with 0].
 intro n; split; intro H; [apply lt_0_succ | apply neq_succ_0].
 Qed.
 
 Lemma Acc_nonneg_lt : forall n : N,
-  Acc (fun n m => 0 <= n /\ n < m) n -> Acc lt n.
+  Acc (fun n m => 0 <= n /\ n < m) n -> Acc NZlt n.
 Proof.
 intros n H; induction H as [n _ H2];
 constructor; intros y H; apply H2; split; [apply le_0_l | assumption].
 Qed.
 
-Theorem lt_wf : well_founded lt.
+Theorem lt_wf : well_founded NZlt.
 Proof.
 unfold well_founded; intro n; apply Acc_nonneg_lt. apply NZlt_wf.
 Qed.
@@ -296,14 +293,14 @@ Qed.
 
 Theorem le_pred_l : forall n : N, P n <= n.
 Proof.
-nondep_induct n.
+cases n.
 rewrite pred_0; le_equal.
 intros; rewrite pred_succ;  apply le_succ_r.
 Qed.
 
 Theorem lt_pred_l : forall n : N, n ~= 0 -> P n < n.
 Proof.
-nondep_induct n.
+cases n.
 intro H; elimtype False; now apply H.
 intros; rewrite pred_succ;  apply lt_succ_r.
 Qed.
@@ -320,14 +317,14 @@ Qed.
 
 Theorem lt_le_pred : forall n m : N, n < m -> n <= P m. (* Converse is false for n == m == 0 *)
 Proof.
-intro n; nondep_induct m.
+intro n; cases m.
 intro H; false_hyp H nlt_0_r.
 intros m IH. rewrite pred_succ; now apply -> lt_succ_le.
 Qed.
 
 Theorem lt_pred_le : forall n m : N, P n < m -> n <= m. (* Converse is false for n == m == 0 *)
 Proof.
-intros n m; nondep_induct n.
+intros n m; cases n.
 rewrite pred_0; intro H; le_less.
 intros n IH. rewrite pred_succ in IH. now apply -> lt_le_succ.
 Qed.
@@ -378,7 +375,7 @@ Qed.
 
 Theorem le_pred_le_succ : forall n m : N, P n <= m <-> n <= S m.
 Proof.
-intros n m; nondep_induct n.
+intros n m; cases n.
 rewrite pred_0. split; intro H; apply le_0_l.
 intro n. rewrite pred_succ. apply succ_le_mono.
 Qed.
diff --git a/theories/Numbers/Natural/Abstract/NPlus.v b/theories/Numbers/Natural/Abstract/NPlus.v
index 67a2766ba4..f1e0e6ace9 100644
--- a/theories/Numbers/Natural/Abstract/NPlus.v
+++ b/theories/Numbers/Natural/Abstract/NPlus.v
@@ -2,13 +2,13 @@ Require Export NBase.
 
 Module NPlusPropFunct (Import NAxiomsMod : NAxiomsSig).
 Module Export NBasePropMod := NBasePropFunct NAxiomsMod.
-Open Local Scope NatScope.
+Open Local Scope NatIntScope.
 
 Theorem plus_0_l : forall n : N, 0 + n == n.
-Proof plus_0_l.
+Proof NZplus_0_l.
 
 Theorem plus_succ_l : forall n m : N, (S n) + m == S (n + m).
-Proof plus_succ_l.
+Proof NZplus_succ_l.
 
 (** Theorems that are valid for both natural numbers and integers *)
 
@@ -42,7 +42,7 @@ Proof NZplus_cancel_l.
 Theorem plus_cancel_r : forall n m p : N, n + p == m + p <-> n == m.
 Proof NZplus_cancel_r.
 
-(** Theorems that are valid for natural numbers but cannot be proved for NZ *)
+(** Theorems that are valid for natural numbers but cannot be proved for N *)
 
 Theorem plus_eq_0 : forall n m : N, n + m == 0 <-> n == 0 /\ m == 0.
 Proof.
@@ -58,7 +58,7 @@ Theorem plus_eq_succ :
   forall n m : N, (exists p : N, n + m == S p) <->
                     (exists n' : N, n == S n') \/ (exists m' : N, m == S m').
 Proof.
-intros n m; nondep_induct n.
+intros n m; cases n.
 split; intro H.
 destruct H as [p H]. rewrite plus_0_l in H; right; now exists p.
 destruct H as [[n' H] | [m' H]].
@@ -91,7 +91,7 @@ Qed.
 
 Theorem plus_pred_l : forall n m : N, n ~= 0 -> P n + m == P (n + m).
 Proof.
-intros n m; nondep_induct n.
+intros n m; cases n.
 intro H; now elim H.
 intros n IH; rewrite plus_succ_l; now do 2 rewrite pred_succ.
 Qed.
diff --git a/theories/Numbers/Natural/Abstract/NTimes.v b/theories/Numbers/Natural/Abstract/NTimes.v
index 7d42a812ce..a0d255892b 100644
--- a/theories/Numbers/Natural/Abstract/NTimes.v
+++ b/theories/Numbers/Natural/Abstract/NTimes.v
@@ -5,13 +5,13 @@ Require Export NPlus.
 
 Module NTimesPropFunct (Import NAxiomsMod : NAxiomsSig).
 Module Export NPlusPropMod := NPlusPropFunct NAxiomsMod.
-Open Local Scope NatScope.
+Open Local Scope NatIntScope.
 
 Theorem times_0_r : forall n, n * 0 == 0.
-Proof times_0_r.
+Proof NZtimes_0_r.
 
 Theorem times_succ_r : forall n m, n * (S m) == n * m + n.
-Proof times_succ_r.
+Proof NZtimes_succ_r.
 
 (** Theorems that are valid for both natural numbers and integers *)
 
@@ -39,7 +39,7 @@ Proof NZtimes_1_l.
 Theorem times_1_r : forall n : N, n * 1 == n.
 Proof NZtimes_1_r.
 
-Lemma semi_ring : semi_ring_theory 0 1 plus times E.
+Lemma semi_ring : semi_ring_theory 0 1 NZplus NZtimes E.
 Proof.
 constructor.
 exact plus_0_l.
@@ -97,9 +97,10 @@ Theorem plus_times_repl_pair : forall a n m n' m' u v,
   a * n + u == a * m + v -> n + m' == n' + m -> a * n' + u == a * m' + v.
 Proof.
 intros a n m n' m' u v H1 H2.
-apply (@times_wd a a) in H2; [| reflexivity].
-do 2 rewrite times_plus_distr_l in H2.
-symmetry in H2; add_equations H1 H2 as H3.
+apply (@NZtimes_wd a a) in H2; [| reflexivity].
+do 2 rewrite times_plus_distr_l in H2. symmetry in H2.
+assert (H3 : (a * n + u) + (a * n' + a * m) == (a * m + v) + (a * n + a * m'))
+  by now apply NZplus_wd.
 stepl (a * n + (u + a * n' + a * m)) in H3 by ring.
 stepr (a * n + (a * m + v + a * m')) in H3 by ring.
 apply -> plus_cancel_l in H3.
diff --git a/theories/Numbers/Natural/Abstract/NTimesOrder.v b/theories/Numbers/Natural/Abstract/NTimesOrder.v
index 19b9e0ae42..68c6c4494f 100644
--- a/theories/Numbers/Natural/Abstract/NTimesOrder.v
+++ b/theories/Numbers/Natural/Abstract/NTimesOrder.v
@@ -2,7 +2,7 @@ Require Export NOrder.
 
 Module NTimesOrderPropFunct (Import NAxiomsMod : NAxiomsSig).
 Module Export NOrderPropMod := NOrderPropFunct NAxiomsMod.
-Open Local Scope NatScope.
+Open Local Scope NatIntScope.
 
 Theorem plus_lt_mono_l : forall n m p : N, n < m <-> p + n < p + m.
 Proof NZplus_lt_mono_l.
@@ -48,7 +48,7 @@ Qed.
 
 Theorem lt_plus_r : forall n m : N, m ~= 0 -> n < n + m.
 Proof.
-intro n; nondep_induct m.
+intros n m; cases m.
 intro H; elimtype False; now apply H.
 intros. rewrite plus_succ_r. apply <- lt_succ_le. apply le_plus_r.
 Qed.