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

9 files changed, 436 insertions, 7 deletions

diff --git a/theories/Numbers/Natural/Abstract/NBase.v b/theories/Numbers/Natural/Abstract/NBase.v
index 956eca896c..0a3d1a586e 100644
--- a/theories/Numbers/Natural/Abstract/NBase.v
+++ b/theories/Numbers/Natural/Abstract/NBase.v
@@ -141,7 +141,7 @@ 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 N. *)
+from NZ. *)
 
 Ltac induct n := induction_maker n ltac:(apply induction).
 
diff --git a/theories/Numbers/Natural/Abstract/NDefOps.v b/theories/Numbers/Natural/Abstract/NDefOps.v
new file mode 100644
index 0000000000..027bfd3ce6
--- /dev/null
+++ b/theories/Numbers/Natural/Abstract/NDefOps.v
@@ -0,0 +1,286 @@
+Require Import Bool. (* To get the orb and negb function *)
+Require Export NStrongRec.
+
+Module NdefOpsPropFunct (Import NAxiomsMod : NAxiomsSig).
+Module Export NStrongRecPropMod := NStrongRecPropFunct NAxiomsMod.
+Open Local Scope NatScope.
+
+(*****************************************************)
+(**                   Addition                       *)
+
+Definition def_plus (x y : N) := recursion y (fun _ p => S p) x.
+
+Infix Local "++" := def_plus (at level 50, left associativity).
+
+Add Morphism def_plus with signature Neq ==> Neq ==> Neq as def_plus_wd.
+Proof.
+unfold def_plus.
+intros x x' Exx' y y' Eyy'.
+apply recursion_wd with (Aeq := Neq).
+assumption.
+unfold fun2_eq; intros _ _ _ p p' Epp'; now rewrite Epp'.
+assumption.
+Qed.
+
+Theorem def_plus_0_l : forall y : N, 0 ++ y == y.
+Proof.
+intro y. unfold def_plus. now rewrite recursion_0.
+Qed.
+
+Theorem def_plus_succ_l : forall x y : N, S x ++ y == S (x ++ y).
+Proof.
+intros x y; unfold def_plus.
+rewrite (@recursion_succ N Neq); try reflexivity.
+unfold fun2_wd. intros _ _ _ m1 m2 H2. now rewrite H2.
+Qed.
+
+Theorem def_plus_plus : forall n m : N, n ++ m == n + m.
+Proof.
+intros n m; induct n.
+now rewrite def_plus_0_l, plus_0_l.
+intros n H. now rewrite def_plus_succ_l, plus_succ_l, H.
+Qed.
+
+(*****************************************************)
+(**                  Multiplication                  *)
+
+Definition def_times (x y : N) := recursion 0 (fun _ p => p ++ x) y.
+
+Infix Local "**" := def_times (at level 40, left associativity).
+
+Lemma def_times_step_wd : forall x : N, fun2_wd Neq Neq Neq (fun _ p => def_plus p x).
+Proof.
+unfold fun2_wd. intros. now apply def_plus_wd.
+Qed.
+
+Lemma def_times_step_equal :
+  forall x x' : N, x == x' ->
+    fun2_eq Neq Neq Neq (fun _ p => def_plus p x) (fun x p => def_plus p x').
+Proof.
+unfold fun2_eq; intros; apply def_plus_wd; assumption.
+Qed.
+
+Add Morphism def_times with signature Neq ==> Neq ==> Neq as def_times_wd.
+Proof.
+unfold def_times.
+intros x x' Exx' y y' Eyy'.
+apply recursion_wd with (Aeq := Neq).
+reflexivity. apply def_times_step_equal. assumption. assumption.
+Qed.
+
+Theorem def_times_0_r : forall x : N, x ** 0 == 0.
+Proof.
+intro. unfold def_times. now rewrite recursion_0.
+Qed.
+
+Theorem def_times_succ_r : forall x y : N, x ** S y == x ** y ++ x.
+Proof.
+intros x y; unfold def_times.
+now rewrite (@recursion_succ N Neq); [| apply def_times_step_wd |].
+Qed.
+
+Theorem def_times_times : forall n m : N, n ** m == n * m.
+Proof.
+intros n m; induct m.
+now rewrite def_times_0_r, times_0_r.
+intros m IH; now rewrite def_times_succ_r, times_succ_r, def_plus_plus, IH.
+Qed.
+
+(*****************************************************)
+(**                     Order                        *)
+
+Definition def_ltb (m : N) : N -> bool :=
+recursion
+  (if_zero false true)
+  (fun _ f => fun n => recursion false (fun n' _ => f n') n)
+  m.
+
+Infix Local "<<" := def_ltb (at level 70, no associativity).
+
+Lemma lt_base_wd : fun_wd Neq (@eq bool) (if_zero false true).
+unfold fun_wd; intros; now apply if_zero_wd.
+Qed.
+
+Lemma lt_step_wd :
+fun2_wd Neq (fun_eq Neq (@eq bool)) (fun_eq Neq (@eq bool))
+  (fun _ f => fun n => recursion false (fun n' _ => f n') n).
+Proof.
+unfold fun2_wd, fun_eq.
+intros x x' Exx' f f' Eff' y y' Eyy'.
+apply recursion_wd with (Aeq := @eq bool).
+reflexivity.
+unfold fun2_eq; intros; now apply Eff'.
+assumption.
+Qed.
+
+Lemma lt_curry_wd :
+  forall m m' : N, m == m' -> fun_eq Neq (@eq bool) (def_ltb m) (def_ltb m').
+Proof.
+unfold def_ltb.
+intros m m' Emm'.
+apply recursion_wd with (Aeq := fun_eq Neq (@eq bool)).
+apply lt_base_wd.
+apply lt_step_wd.
+assumption.
+Qed.
+
+Add Morphism def_ltb with signature Neq ==> Neq ==> (@eq bool) as def_ltb_wd.
+Proof.
+intros; now apply lt_curry_wd.
+Qed.
+
+Theorem def_ltb_base : forall n : N, 0 << n = if_zero false true n.
+Proof.
+intro n; unfold def_ltb; now rewrite recursion_0.
+Qed.
+
+Theorem def_ltb_step :
+  forall m n : N, S m << n = recursion false (fun n' _ => m << n') n.
+Proof.
+intros m n; unfold def_ltb.
+pose proof
+  (@recursion_succ
+    (N -> bool)
+    (fun_eq Neq (@eq bool))
+    (if_zero false true)
+    (fun _ f => fun n => recursion false (fun n' _ => f n') n)
+    lt_base_wd
+    lt_step_wd
+    m n n) as H.
+now rewrite H.
+Qed.
+
+(* Above, we rewrite applications of function. Is it possible to rewrite
+functions themselves, i.e., rewrite (recursion lt_base lt_step (S n)) to
+lt_step n (recursion lt_base lt_step n)? *)
+
+Theorem def_ltb_0 : forall n : N, n << 0 = false.
+Proof.
+cases n.
+rewrite def_ltb_base; now rewrite if_zero_0.
+intro n; rewrite def_ltb_step. now rewrite recursion_0.
+Qed.
+
+Theorem def_ltb_0_succ : forall n : N, 0 << S n = true.
+Proof.
+intro n; rewrite def_ltb_base; now rewrite if_zero_succ.
+Qed.
+
+Theorem succ_def_ltb_mono : forall n m : N, (S n << S m) = (n << m).
+Proof.
+intros n m.
+rewrite def_ltb_step. rewrite (@recursion_succ bool (@eq bool)); try reflexivity.
+unfold fun2_wd; intros; now apply def_ltb_wd.
+Qed.
+
+Theorem def_ltb_lt : forall n m : N, n << m = true <-> n < m.
+Proof.
+double_induct n m.
+cases m.
+rewrite def_ltb_0. split; intro H; [discriminate H | false_hyp H nlt_0_r].
+intro n. rewrite def_ltb_0_succ. split; intro; [apply lt_0_succ | reflexivity].
+intro n. rewrite def_ltb_0. split; intro H; [discriminate | false_hyp H nlt_0_r].
+intros n m. rewrite succ_def_ltb_mono. now rewrite <- succ_lt_mono.
+Qed.
+
+(*
+(*****************************************************)
+(**                     Even                         *)
+
+Definition even (x : N) := recursion true (fun _ p => negb p) x.
+
+Lemma even_step_wd : fun2_wd Neq (@eq bool) (@eq bool) (fun x p => if p then false else true).
+Proof.
+unfold fun2_wd.
+intros x x' Exx' b b' Ebb'.
+unfold eq_bool; destruct b; destruct b'; now simpl.
+Qed.
+
+Add Morphism even with signature Neq ==> (@eq bool) as even_wd.
+Proof.
+unfold even; intros.
+apply recursion_wd with (A := bool) (Aeq := (@eq bool)).
+now unfold eq_bool.
+unfold fun2_eq. intros _ _ _ b b' Ebb'. unfold eq_bool; destruct b; destruct b'; now simpl.
+assumption.
+Qed.
+
+Theorem even_0 : even 0 = true.
+Proof.
+unfold even.
+now rewrite recursion_0.
+Qed.
+
+Theorem even_succ : forall x : N, even (S x) = negb (even x).
+Proof.
+unfold even.
+intro x; rewrite (recursion_succ (@eq bool)); try reflexivity.
+unfold fun2_wd.
+intros _ _ _ b b' Ebb'. destruct b; destruct b'; now simpl.
+Qed.
+
+(*****************************************************)
+(**                Division by 2                     *)
+
+Definition half_aux (x : N) : N * N :=
+  recursion (0, 0) (fun _ p => let (x1, x2) := p in ((S x2, x1))) x.
+
+Definition half (x : N) := snd (half_aux x).
+
+Definition E2 := prod_rel Neq Neq.
+
+Add Relation (prod N N) E2
+reflexivity proved by (prod_rel_refl N N Neq Neq E_equiv E_equiv)
+symmetry proved by (prod_rel_symm N N Neq Neq E_equiv E_equiv)
+transitivity proved by (prod_rel_trans N N Neq Neq E_equiv E_equiv)
+as E2_rel.
+
+Lemma half_step_wd: fun2_wd Neq E2 E2 (fun _ p => let (x1, x2) := p in ((S x2, x1))).
+Proof.
+unfold fun2_wd, E2, prod_rel.
+intros _ _ _ p1 p2 [H1 H2].
+destruct p1; destruct p2; simpl in *.
+now split; [rewrite H2 |].
+Qed.
+
+Add Morphism half with signature Neq ==> Neq as half_wd.
+Proof.
+unfold half.
+assert (H: forall x y, x == y -> E2 (half_aux x) (half_aux y)).
+intros x y Exy; unfold half_aux; apply recursion_wd with (Aeq := E2); unfold E2.
+unfold E2.
+unfold prod_rel; simpl; now split.
+unfold fun2_eq, prod_rel; simpl.
+intros _ _ _ p1 p2; destruct p1; destruct p2; simpl.
+intros [H1 H2]; split; [rewrite H2 | assumption]. reflexivity. assumption.
+unfold E2, prod_rel in H. intros x y Exy; apply H in Exy.
+exact (proj2 Exy).
+Qed.
+
+(*****************************************************)
+(**            Logarithm for the base 2              *)
+
+Definition log (x : N) : N :=
+strong_rec 0
+           (fun x g =>
+              if (e x 0) then 0
+              else if (e x 1) then 0
+              else S (g (half x)))
+           x.
+
+Add Morphism log with signature Neq ==> Neq as log_wd.
+Proof.
+intros x x' Exx'. unfold log.
+apply strong_rec_wd with (Aeq := Neq); try (reflexivity || assumption).
+unfold fun2_eq. intros y y' Eyy' g g' Egg'.
+assert (H : e y 0 = e y' 0); [now apply e_wd|].
+rewrite <- H; clear H.
+assert (H : e y 1 = e y' 1); [now apply e_wd|].
+rewrite <- H; clear H.
+assert (H : S (g (half y)) == S (g' (half y')));
+[apply succ_wd; apply Egg'; now apply half_wd|].
+now destruct (e y 0); destruct (e y 1).
+Qed.
+*)
+End NdefOpsPropFunct.
+
diff --git a/theories/Numbers/Natural/Abstract/NMinus.v b/theories/Numbers/Natural/Abstract/NMinus.v
index f7c9cf19bb..faf4759bdb 100644
--- a/theories/Numbers/Natural/Abstract/NMinus.v
+++ b/theories/Numbers/Natural/Abstract/NMinus.v
@@ -100,6 +100,7 @@ Qed.
 
 (* This could be proved by adding m to both sides. Then the proof would
 use plus_minus_assoc and minus_0_le, which is proven below. *)
+
 Theorem plus_minus_eq_nz : forall n m p : N, p ~= 0 -> n - m == p -> m + p == n.
 Proof.
 intros n m p H; double_induct n m.
diff --git a/theories/Numbers/Natural/Abstract/NOrder.v b/theories/Numbers/Natural/Abstract/NOrder.v
index c7b7d495f7..9ddaa9a2f0 100644
--- a/theories/Numbers/Natural/Abstract/NOrder.v
+++ b/theories/Numbers/Natural/Abstract/NOrder.v
@@ -317,7 +317,7 @@ rewrite H; apply lt_wf.
 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 *)
+(* Theorems that are true for natural numbers but not for integers *)
 
 (* "le_0_l : forall n : N, 0 <= n" was proved in NBase.v *)
 
diff --git a/theories/Numbers/Natural/Abstract/NPlus.v b/theories/Numbers/Natural/Abstract/NPlus.v
index d1269cf03f..09b5a500b3 100644
--- a/theories/Numbers/Natural/Abstract/NPlus.v
+++ b/theories/Numbers/Natural/Abstract/NPlus.v
@@ -59,7 +59,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 Z *)
+(* Theorems that are valid for natural numbers but cannot be proved for Z *)
 
 Theorem eq_plus_0 : forall n m : N, n + m == 0 <-> n == 0 /\ m == 0.
 Proof.
diff --git a/theories/Numbers/Natural/Abstract/NPlusOrder.v b/theories/Numbers/Natural/Abstract/NPlusOrder.v
index f459e8dd67..265ea81444 100644
--- a/theories/Numbers/Natural/Abstract/NPlusOrder.v
+++ b/theories/Numbers/Natural/Abstract/NPlusOrder.v
@@ -67,7 +67,7 @@ Proof NZplus_le_cases.
 Theorem plus_pos_cases : forall n m : N, 0 < n + m -> 0 < n \/ 0 < m.
 Proof NZplus_pos_cases.
 
-(** Theorems true for natural numbers *)
+(* Theorems true for natural numbers *)
 
 Theorem le_plus_r : forall n m : N, n <= n + m.
 Proof.
@@ -111,4 +111,4 @@ do 2 rewrite <- plus_assoc in H4. do 2 apply <- plus_lt_mono_l in H4.
 now rewrite (plus_comm n' u), (plus_comm m' v).
 Qed.
 
-End NPlusOrderPropFunct.
\ No newline at end of file
+End NPlusOrderPropFunct.
diff --git a/theories/Numbers/Natural/Abstract/NStrongRec.v b/theories/Numbers/Natural/Abstract/NStrongRec.v
new file mode 100644
index 0000000000..ace608dbe0
--- /dev/null
+++ b/theories/Numbers/Natural/Abstract/NStrongRec.v
@@ -0,0 +1,133 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+(*                      Evgeny Makarov, INRIA, 2007                     *)
+(************************************************************************)
+
+(*i i*)
+
+(** This file defined the strong (course-of-value, well-founded) recursion
+and proves its properties *)
+
+Require Export NMinus.
+
+Module NStrongRecPropFunct (Import NAxiomsMod : NAxiomsSig).
+Module Export NMinusPropMod := NMinusPropFunct NAxiomsMod.
+Open Local Scope NatScope.
+
+Section StrongRecursion.
+
+Variable A : Set.
+Variable Aeq : relation A.
+
+Notation Local "x ==A y" := (Aeq x y) (at level 70, no associativity).
+
+Hypothesis Aeq_equiv : equiv A Aeq.
+
+Add Relation A Aeq
+ reflexivity proved by (proj1 Aeq_equiv)
+ symmetry proved by (proj2 (proj2 Aeq_equiv))
+ transitivity proved by (proj1 (proj2 Aeq_equiv))
+as Aeq_rel.
+
+Definition strong_rec (a : A) (f : N -> (N -> A) -> A) (n : N) : A :=
+recursion
+  (fun _ : N => a)
+  (fun (m : N) (p : N -> A) (k : N) => f k p)
+  (S n)
+  n.
+
+Theorem strong_rec_wd :
+forall a a' : A, a ==A a' ->
+  forall f f', fun2_eq Neq (fun_eq Neq Aeq) Aeq f f' ->
+    forall n n', n == n' ->
+      strong_rec a f n ==A strong_rec a' f' n'.
+Proof.
+intros a a' Eaa' f f' Eff' n n' Enn'.
+(* First we prove that recursion (which is on type N -> A) returns
+extensionally equal functions, and then we use the fact that n == n' *)
+assert (H : fun_eq Neq Aeq
+  (recursion
+    (fun _ : N => a)
+    (fun (m : N) (p : N -> A) (k : N) => f k p)
+    (S n))
+  (recursion
+    (fun _ : N => a')
+    (fun (m : N) (p : N -> A) (k : N) => f' k p)
+    (S n'))).
+apply recursion_wd with (Aeq := fun_eq Neq Aeq).
+unfold fun_eq; now intros.
+unfold fun2_eq. intros y y' Eyy' p p' Epp'. unfold fun_eq. auto.
+now rewrite Enn'.
+unfold strong_rec.
+now apply H.
+Qed.
+
+(*Section FixPoint.
+
+Variable a : A.
+Variable f : N -> (N -> A) -> A.
+
+Hypothesis f_wd : fun2_wd Neq (fun_eq Neq Aeq) Aeq f.
+
+Let g (n : N) : A := strong_rec a f n.
+
+Add Morphism g with signature Neq ==> Aeq as g_wd.
+Proof.
+intros n1 n2 H. unfold g. now apply strong_rec_wd.
+Qed.
+
+Theorem NtoA_eq_symm : symmetric (N -> A) (fun_eq Neq Aeq).
+Proof.
+apply fun_eq_symm.
+exact (proj2 (proj2 NZeq_equiv)).
+exact (proj2 (proj2 Aeq_equiv)).
+Qed.
+
+Theorem NtoA_eq_trans : transitive (N -> A) (fun_eq Neq Aeq).
+Proof.
+apply fun_eq_trans.
+exact (proj1 NZeq_equiv).
+exact (proj1 (proj2 NZeq_equiv)).
+exact (proj1 (proj2 Aeq_equiv)).
+Qed.
+
+Add Relation (N -> A) (fun_eq Neq Aeq)
+ symmetry proved by NtoA_eq_symm
+ transitivity proved by NtoA_eq_trans
+as NtoA_eq_rel.
+
+Add Morphism f with signature Neq ==> (fun_eq Neq Aeq) ==> Aeq as f_morph.
+Proof.
+apply f_wd.
+Qed.
+
+(* We need an assumption saying that for every n, the step function (f n h)
+calls h only on the segment [0 ... n - 1]. This means that if h1 and h2
+coincide on values < n, then (f n h1) coincides with (f n h2) *)
+
+Hypothesis step_good :
+  forall (n : N) (h1 h2 : N -> A),
+    (forall m : N, m < n -> Aeq (h1 m) (h2 m)) -> Aeq (f n h1) (f n h2).
+
+(* Todo:
+Theorem strong_rec_fixpoint : forall n : N, Aeq (g n) (f n g).
+Proof.
+apply induction.
+unfold predicate_wd, fun_wd.
+intros x y H. rewrite H. unfold fun_eq; apply g_wd.
+reflexivity.
+unfold g, strong_rec.
+*)
+
+End FixPoint.*)
+End StrongRecursion.
+
+Implicit Arguments strong_rec [A].
+
+End NStrongRecPropFunct.
+
diff --git a/theories/Numbers/Natural/Abstract/NTimes.v b/theories/Numbers/Natural/Abstract/NTimes.v
index e15f02a1ef..7d513dc460 100644
--- a/theories/Numbers/Natural/Abstract/NTimes.v
+++ b/theories/Numbers/Natural/Abstract/NTimes.v
@@ -52,7 +52,7 @@ Proof NZtimes_1_l.
 Theorem times_1_r : forall n : N, n * 1 == n.
 Proof NZtimes_1_r.
 
-(** Theorems that cannot be proved in NZTimes *)
+(* Theorems that cannot be proved in NZTimes *)
 
 (* In proving the correctness of the definition of multiplication on
 integers constructed from pairs of natural numbers, we'll need the
diff --git a/theories/Numbers/Natural/Abstract/NTimesOrder.v b/theories/Numbers/Natural/Abstract/NTimesOrder.v
index 502f994174..259416d468 100644
--- a/theories/Numbers/Natural/Abstract/NTimesOrder.v
+++ b/theories/Numbers/Natural/Abstract/NTimesOrder.v
@@ -32,6 +32,12 @@ Proof NZtimes_cancel_l.
 Theorem times_cancel_r : forall n m p : N, p ~= 0 -> (n * p == m * p <-> n == m).
 Proof NZtimes_cancel_r.
 
+Theorem times_id_l : forall n m : N, m ~= 0 -> (n * m == m <-> n == 1).
+Proof NZtimes_id_l.
+
+Theorem times_id_r : forall n m : N, n ~= 0 -> (n * m == n <-> m == 1).
+Proof NZtimes_id_r.
+
 Theorem times_le_mono_pos_l : forall n m p : N, 0 < p -> (n <= m <-> p * n <= p * m).
 Proof NZtimes_le_mono_pos_l.
 
@@ -50,6 +56,9 @@ Proof NZeq_times_0.
 Theorem neq_times_0 : forall n m : N, n ~= 0 /\ m ~= 0 <-> n * m ~= 0.
 Proof NZneq_times_0.
 
+Theorem eq_square_0 : forall n : N, n * n == 0 <-> n == 0.
+Proof NZeq_square_0.
+
 Theorem eq_times_0_l : forall n m : N, n * m == 0 -> m ~= 0 -> n == 0.
 Proof NZeq_times_0_l.
 
@@ -73,7 +82,7 @@ Qed.
 Theorem times_2_mono_l : forall n m : N, n < m -> 1 + (1 + 1) * n < (1 + 1) * m.
 Proof NZtimes_2_mono_l.
 
-(** Theorems that are either not valid on Z or have different proofs on N and Z *)
+(* Theorems that are either not valid on Z or have different proofs on N and Z *)
 
 Theorem times_le_mono_l : forall n m p : N, n <= m -> p * n <= p * m.
 Proof.