An update of theories/Numbers

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

5 files changed, 79 insertions, 30 deletions

diff --git a/theories/Numbers/Natural/Abstract/NAxioms.v b/theories/Numbers/Natural/Abstract/NAxioms.v
index 2a17754d5a..052a18c3ec 100644
--- a/theories/Numbers/Natural/Abstract/NAxioms.v
+++ b/theories/Numbers/Natural/Abstract/NAxioms.v
@@ -15,6 +15,8 @@ Notation P := NZpred.
 Notation plus := NZplus.
 Notation times := NZtimes.
 Notation minus := NZminus.
+Notation lt := NZlt.
+Notation le := NZle.
 Notation "x == y"  := (NZeq x y) (at level 70) : NatScope.
 Notation "x ~= y" := (~ NZeq x y) (at level 70) : NatScope.
 Notation "0" := NZ0 : NatScope.
@@ -36,7 +38,7 @@ Axiom pred_0 : P 0 == 0.
 
 Axiom recursion_wd : forall (A : Set) (Aeq : relation A),
   forall a a' : A, Aeq a a' ->
-    forall f f' : N -> A -> A, eq_fun2 Neq Aeq Aeq f f' ->
+    forall f f' : N -> A -> A, fun2_eq Neq Aeq Aeq f f' ->
       forall x x' : N, x == x' ->
         Aeq (recursion a f x) (recursion a' f' x').
 
diff --git a/theories/Numbers/Natural/Abstract/NBase.v b/theories/Numbers/Natural/Abstract/NBase.v
index c0c479dc84..7c44646320 100644
--- a/theories/Numbers/Natural/Abstract/NBase.v
+++ b/theories/Numbers/Natural/Abstract/NBase.v
@@ -59,7 +59,7 @@ Definition if_zero (A : Set) (a b : A) (n : N) : A :=
 Add Morphism if_zero with signature @eq ==> @eq ==> Neq ==> @eq as if_zero_wd.
 Proof.
 intros; unfold if_zero. apply recursion_wd with (Aeq := (@eq A)).
-reflexivity. unfold eq_fun2; now intros. assumption.
+reflexivity. unfold fun2_eq; now intros. assumption.
 Qed.
 
 Theorem if_zero_0 : forall (A : Set) (a b : A), if_zero A a b 0 = a.
@@ -198,7 +198,7 @@ End PairInduction.
 Section TwoDimensionalInduction.
 
 Variable R : N -> N -> Prop.
-Hypothesis R_wd : rel_wd Neq Neq R.
+Hypothesis R_wd : relation_wd Neq Neq R.
 
 Add Morphism R with signature Neq ==> Neq ==> iff as R_morph.
 Proof.
@@ -223,12 +223,12 @@ End TwoDimensionalInduction.
   try intros until n;
   try intros until m;
   pattern n, m; apply two_dim_induction; clear n m;
-  [solve_rel_wd | | | ].*)
+  [solve_relation_wd | | | ].*)
 
 Section DoubleInduction.
 
 Variable R : N -> N -> Prop.
-Hypothesis R_wd : rel_wd Neq Neq R.
+Hypothesis R_wd : relation_wd Neq Neq R.
 
 Add Morphism R with signature Neq ==> Neq ==> iff as R_morph1.
 Proof.
@@ -250,7 +250,7 @@ Ltac double_induct n m :=
   try intros until n;
   try intros until m;
   pattern n, m; apply double_induction; clear n m;
-  [solve_rel_wd | | | ].
+  [solve_relation_wd | | | ].
 
 End NBasePropFunct.
 
diff --git a/theories/Numbers/Natural/Abstract/NIso.v b/theories/Numbers/Natural/Abstract/NIso.v
index b792beefe6..35e93bbc7f 100644
--- a/theories/Numbers/Natural/Abstract/NIso.v
+++ b/theories/Numbers/Natural/Abstract/NIso.v
@@ -26,7 +26,7 @@ unfold natural_isomorphism.
 intros n m Eqxy.
 apply NAxiomsMod1.recursion_wd with (Aeq := Eq2).
 reflexivity.
-unfold eq_fun2. intros _ _ _ y' y'' H. now apply NBasePropMod2.succ_wd.
+unfold fun2_eq. intros _ _ _ y' y'' H. now apply NBasePropMod2.succ_wd.
 assumption.
 Qed.
 
diff --git a/theories/Numbers/Natural/Abstract/NMinus.v b/theories/Numbers/Natural/Abstract/NMinus.v
index 5ac1f70fbf..fe0ec4e627 100644
--- a/theories/Numbers/Natural/Abstract/NMinus.v
+++ b/theories/Numbers/Natural/Abstract/NMinus.v
@@ -41,7 +41,7 @@ Qed.
 Theorem minus_gt : forall n m : N, n > m -> n - m ~= 0.
 Proof.
 intros n m H; elim H using lt_ind_rel; clear n m H.
-solve_rel_wd.
+solve_relation_wd.
 intro; rewrite minus_0_r; apply neq_succ_0.
 intros; now rewrite minus_succ.
 Qed.
diff --git a/theories/Numbers/Natural/Abstract/NOrder.v b/theories/Numbers/Natural/Abstract/NOrder.v
index 3e338825e6..8f68716bbb 100644
--- a/theories/Numbers/Natural/Abstract/NOrder.v
+++ b/theories/Numbers/Natural/Abstract/NOrder.v
@@ -163,14 +163,6 @@ Theorem left_induction :
         forall n : N, n <= z -> A n.
 Proof NZleft_induction.
 
-Theorem order_induction :
-  forall A : N -> Prop, predicate_wd Neq A ->
-    forall z : N, A z ->
-      (forall n : N, z <= n -> A n -> A (S n)) ->
-      (forall n : N, n < z  -> A (S n) -> A n) ->
-        forall n : N, A n.
-Proof NZorder_induction.
-
 Theorem right_induction' :
   forall A : N -> Prop, predicate_wd Neq A ->
     forall z : N,
@@ -179,6 +171,28 @@ Theorem right_induction' :
         forall n : N, A n.
 Proof NZright_induction'.
 
+Theorem left_induction' :
+  forall A : N -> Prop, predicate_wd Neq A ->
+    forall z : N,
+    (forall n : NZ, z <= n -> A n) ->
+    (forall n : N, n < z -> A (S n) -> A n) ->
+      forall n : NZ, A n.
+Proof NZleft_induction'.
+
+Theorem strong_right_induction :
+  forall A : N -> Prop, predicate_wd Neq A ->
+    forall z : N,
+    (forall n : N, z <= n -> (forall m : N, z <= m -> m < n -> A m) -> A n) ->
+       forall n : N, z <= n -> A n.
+Proof NZstrong_right_induction.
+
+Theorem strong_left_induction :
+  forall A : N -> Prop, predicate_wd Neq A ->
+    forall z : N,
+      (forall n : N, n <= z -> (forall m : N, m <= z -> S n <= m -> A m) -> A n) ->
+        forall n : N, n <= z -> A n.
+Proof NZstrong_left_induction.
+
 Theorem strong_right_induction' :
   forall A : N -> Prop, predicate_wd Neq A ->
     forall z : N,
@@ -187,6 +201,33 @@ Theorem strong_right_induction' :
         forall n : N, A n.
 Proof NZstrong_right_induction'.
 
+Theorem strong_left_induction' :
+  forall A : N -> Prop, predicate_wd Neq A ->
+    forall z : N,
+    (forall n : N, z <= n -> A n) ->
+    (forall n : N, n <= z -> (forall m : N, m <= z -> S n <= m -> A m) -> A n) ->
+      forall n : N, A n.
+Proof NZstrong_left_induction'.
+
+Theorem order_induction :
+  forall A : N -> Prop, predicate_wd Neq A ->
+    forall z : N, A z ->
+      (forall n : N, z <= n -> A n -> A (S n)) ->
+      (forall n : N, n < z  -> A (S n) -> A n) ->
+        forall n : N, A n.
+Proof NZorder_induction.
+
+Theorem order_induction' :
+  forall A : N -> Prop, predicate_wd Neq A ->
+    forall z : N, A z ->
+      (forall n : N, z <= n -> A n -> A (S n)) ->
+      (forall n : N, n <= z -> A n -> A (P n)) ->
+        forall n : N, A n.
+Proof NZorder_induction'.
+
+(* We don't need order_induction_0 and order_induction'_0 (see NZOrder and
+ZOrder) since they boil down to regular induction *)
+
 (** Elimintation principle for < *)
 
 Theorem lt_ind :
@@ -207,6 +248,24 @@ Theorem le_ind :
         forall m : N, n <= m -> A m.
 Proof NZle_ind.
 
+(** Well-founded relations *)
+
+Theorem lt_wf : forall z : N, well_founded (fun n m : N => z <= n /\ n < m).
+Proof NZlt_wf.
+
+Theorem gt_wf : forall z : N, well_founded (fun n m : N => m < n /\ n <= z).
+Proof NZgt_wf.
+
+Theorem lt_wf_0 : well_founded lt.
+Proof.
+assert (H : relations_eq lt (fun n m : N => 0 <= n /\ n < m)).
+intros x y; split.
+intro H; split; [apply le_0_l | assumption]. now intros [_ H].
+rewrite H; apply lt_wf.
+(* does not work:
+setoid_replace lt with (fun n m : N => 0 <= n /\ n < m) using relation relations_eq.*)
+Qed.
+
 (** Theorems that are true for natural numbers but not for integers *)
 
 (* "le_0_l : forall n : N, 0 <= n" was proved in NBase.v *)
@@ -247,18 +306,6 @@ 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 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 NZlt.
-Proof.
-unfold well_founded; intro n; apply Acc_nonneg_lt. apply NZlt_wf.
-Qed.
-
 (** Elimination principlies for < and <= for relations *)
 
 Section RelElim.
@@ -266,7 +313,7 @@ Section RelElim.
 (* FIXME: Variable R : relation N. -- does not work *)
 
 Variable R : N -> N -> Prop.
-Hypothesis R_wd : rel_wd Neq Neq R.
+Hypothesis R_wd : relation_wd Neq Neq R.
 
 Add Morphism R with signature Neq ==> Neq ==> iff as R_morph2.
 Proof R_wd.
@@ -359,7 +406,7 @@ Qed.
 Theorem pred_le_mono : forall n m : N, n <= m -> P n <= P m. (* Converse is false for n == 1, m == 0 *)
 Proof.
 intros n m H; elim H using le_ind_rel.
-solve_rel_wd.
+solve_relation_wd.
 intro; rewrite pred_0; apply le_0_l.
 intros p q H1 _; now do 2 rewrite pred_succ.
 Qed.