Arith: full integration of the "Numbers" modular framework

 - The earlier proof-of-concept file NPeano (which instantiates
   the "Numbers" framework for nat) becomes now the entry point
   in the Arith lib, and gets renamed PeanoNat. It still provides
   an inner module "Nat" which sums up everything about type nat
   (functions, predicates and properties of them).
   This inner module Nat is usable as soon as you Require Import Arith,
   or just Arith_base, or simply PeanoNat.

 - Definitions of operations over type nat are now grouped in a new
   file Init/Nat.v. This file is meant to be used without "Import",
   hence providing for instance Nat.add or Nat.sqrt as soon as coqtop
   starts (but no proofs about them).

 - The definitions that used to be in Init/Peano.v (pred, plus, minus, mult)
   are now compatibility notations (for Nat.pred, Nat.add, Nat.sub, Nat.mul
   where here Nat is Init/Nat.v).

 - This Coq.Init.Nat module (with only pure definitions) is Include'd
   in the aforementioned Coq.Arith.PeanoNat.Nat. You might see Init.Nat
   sometimes instead of just Nat (for instance when doing "Print plus").
   Normally it should be ok to just ignore these "Init" since
   Init.Nat is included in the full PeanoNat.Nat. I'm investigating if
   it's possible to get rid of these "Init" prefixes.

 - Concerning predicates, orders le and lt are still defined in Init/Peano.v,
   with their notations "<=" and "<". Properties in PeanoNat.Nat directly
   refer to these predicates in Peano. For instantation reasons, PeanoNat.Nat
   also contains a Nat.le and Nat.lt (defined via "Definition le := Peano.le",
   we cannot yet include an Inductive to implement a Parameter), but these
   aliased predicates won't probably be very convenient to use.

 - Technical remark: I've split the previous property functor NProp in
   two parts (NBasicProp and NExtraProp), it helps a lot for building
   PeanoNat.Nat incrementally. Roughly speaking, we have the following schema:

   Module Nat.
     Include Coq.Init.Nat. (* definition of operations : add ... sqrt ... *)
     ... (** proofs of specifications for basic ops such as + * - *)
     Include NBasicProp. (** generic properties of these basic ops *)
     ... (** proofs of specifications for advanced ops (pow sqrt log2...)
             that may rely on proofs for + * - *)
     Include NExtraProp. (** all remaining properties *)
   End Nat.

- All other files in directory Arith are now taking advantage of PeanoNat :
  they are now filled with compatibility notations (when earlier lemmas
  have exact counterpart in the Nat module) or lemmas with one-line proofs
  based on the Nat module. All hints for database "arith" remain declared
  in these old-style file (such as Plus.v, Lt.v, etc). All the old-style
  files are still Require'd (or not) by Arith.v, just as before.

- Compatibility should be almost complete. For instance in the stdlib,
  the only adaptations were due to .ml code referring to some Coq constant
  name such as Coq.Init.Peano.pred, which doesn't live well with the
  new compatibility notations.

4 files changed, 339 insertions, 52 deletions

diff --git a/theories/Init/Nat.v b/theories/Init/Nat.v
new file mode 100644
index 0000000000..5764b349b6
--- /dev/null
+++ b/theories/Init/Nat.v
@@ -0,0 +1,297 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+Require Import Notations Logic Datatypes.
+
+Local Open Scope nat_scope.
+
+(**********************************************************************)
+(** * Peano natural numbers, definitions of operations *)
+(**********************************************************************)
+
+(** This file is meant to be used as a whole module,
+    without importing it, leading to qualified definitions
+    (e.g. Nat.pred) *)
+
+Definition t := nat.
+
+(** ** Constants *)
+
+Definition zero := 0.
+Definition one := 1.
+Definition two := 2.
+
+(** ** Basic operations *)
+
+Definition succ := S.
+
+Definition pred n :=
+  match n with
+    | 0 => n
+    | S u => u
+  end.
+
+Fixpoint add n m :=
+  match n with
+  | 0 => m
+  | S p => S (p + m)
+  end
+
+where "n + m" := (add n m) : nat_scope.
+
+Definition double n := n + n.
+
+Fixpoint mul n m :=
+  match n with
+  | 0 => 0
+  | S p => m + p * m
+  end
+
+where "n * m" := (mul n m) : nat_scope.
+
+(** Truncated subtraction: [n-m] is [0] if [n<=m] *)
+
+Fixpoint sub n m :=
+  match n, m with
+  | S k, S l => k - l
+  | _, _ => n
+  end
+
+where "n - m" := (sub n m) : nat_scope.
+
+(** ** Comparisons *)
+
+Fixpoint eqb n m : bool :=
+  match n, m with
+    | 0, 0 => true
+    | 0, S _ => false
+    | S _, 0 => false
+    | S n', S m' => eqb n' m'
+  end.
+
+Fixpoint leb n m : bool :=
+  match n, m with
+    | 0, _ => true
+    | _, 0 => false
+    | S n', S m' => leb n' m'
+  end.
+
+Definition ltb n m := leb (S n) m.
+
+Infix "=?" := eqb (at level 70) : nat_scope.
+Infix "<=?" := leb (at level 70) : nat_scope.
+Infix "<?" := ltb (at level 70) : nat_scope.
+
+Fixpoint compare n m : comparison :=
+  match n, m with
+   | 0, 0 => Eq
+   | 0, S _ => Lt
+   | S _, 0 => Gt
+   | S n', S m' => compare n' m'
+  end.
+
+Infix "?=" := compare (at level 70) : nat_scope.
+
+(** ** Minimum, maximum *)
+
+Fixpoint max n m :=
+  match n, m with
+    | 0, _ => m
+    | S n', 0 => n
+    | S n', S m' => S (max n' m')
+  end.
+
+Fixpoint min n m :=
+  match n, m with
+    | 0, _ => 0
+    | S n', 0 => 0
+    | S n', S m' => S (min n' m')
+  end.
+
+(** ** Parity tests *)
+
+Fixpoint even n : bool :=
+  match n with
+    | 0 => true
+    | 1 => false
+    | S (S n') => even n'
+  end.
+
+Definition odd n := negb (even n).
+
+(** ** Power *)
+
+Fixpoint pow n m :=
+  match m with
+    | 0 => 1
+    | S m => n * (n^m)
+  end
+
+where "n ^ m" := (pow n m) : nat_scope.
+
+(** ** Euclidean division *)
+
+(** This division is linear and tail-recursive.
+    In [divmod], [y] is the predecessor of the actual divisor,
+    and [u] is [y] minus the real remainder
+*)
+
+Fixpoint divmod x y q u :=
+  match x with
+    | 0 => (q,u)
+    | S x' => match u with
+                | 0 => divmod x' y (S q) y
+                | S u' => divmod x' y q u'
+              end
+  end.
+
+Definition div x y :=
+  match y with
+    | 0 => y
+    | S y' => fst (divmod x y' 0 y')
+  end.
+
+Definition modulo x y :=
+  match y with
+    | 0 => y
+    | S y' => y' - snd (divmod x y' 0 y')
+  end.
+
+Infix "/" := div : nat_scope.
+Infix "mod" := modulo (at level 40, no associativity) : nat_scope.
+
+
+(** ** Greatest common divisor *)
+
+(** We use Euclid algorithm, which is normally not structural,
+    but Coq is now clever enough to accept this (behind modulo
+    there is a subtraction, which now preserves being a subterm)
+*)
+
+Fixpoint gcd a b :=
+  match a with
+   | O => b
+   | S a' => gcd (b mod (S a')) (S a')
+  end.
+
+(** ** Square *)
+
+Definition square n := n * n.
+
+(** ** Square root *)
+
+(** The following square root function is linear (and tail-recursive).
+  With Peano representation, we can't do better. For faster algorithm,
+  see Psqrt/Zsqrt/Nsqrt...
+
+  We search the square root of n = k + p^2 + (q - r)
+  with q = 2p and 0<=r<=q. We start with p=q=r=0, hence
+  looking for the square root of n = k. Then we progressively
+  decrease k and r. When k = S k' and r=0, it means we can use (S p)
+  as new sqrt candidate, since (S k')+p^2+2p = k'+(S p)^2.
+  When k reaches 0, we have found the biggest p^2 square contained
+  in n, hence the square root of n is p.
+*)
+
+Fixpoint sqrt_iter k p q r :=
+  match k with
+    | O => p
+    | S k' => match r with
+                | O => sqrt_iter k' (S p) (S (S q)) (S (S q))
+                | S r' => sqrt_iter k' p q r'
+              end
+  end.
+
+Definition sqrt n := sqrt_iter n 0 0 0.
+
+(** ** Log2 *)
+
+(** This base-2 logarithm is linear and tail-recursive.
+
+  In [log2_iter], we maintain the logarithm [p] of the counter [q],
+  while [r] is the distance between [q] and the next power of 2,
+  more precisely [q + S r = 2^(S p)] and [r<2^p]. At each
+  recursive call, [q] goes up while [r] goes down. When [r]
+  is 0, we know that [q] has almost reached a power of 2,
+  and we increase [p] at the next call, while resetting [r]
+  to [q].
+
+  Graphically (numbers are [q], stars are [r]) :
+
+<<
+                    10
+                  9
+                8
+              7   *
+            6       *
+          5           ...
+        4
+      3   *
+    2       *
+  1   *       *
+0   *   *       *
+>>
+
+  We stop when [k], the global downward counter reaches 0.
+  At that moment, [q] is the number we're considering (since
+  [k+q] is invariant), and [p] its logarithm.
+*)
+
+Fixpoint log2_iter k p q r :=
+  match k with
+    | O => p
+    | S k' => match r with
+                | O => log2_iter k' (S p) (S q) q
+                | S r' => log2_iter k' p (S q) r'
+              end
+  end.
+
+Definition log2 n := log2_iter (pred n) 0 1 0.
+
+(** Iterator on natural numbers *)
+
+Definition iter (n:nat) {A} (f:A->A) (x:A) : A :=
+ nat_rect (fun _ => A) x (fun _ => f) n.
+
+(** Bitwise operations *)
+
+(** We provide here some bitwise operations for unary numbers.
+  Some might be really naive, they are just there for fullfiling
+  the same interface as other for natural representations. As
+  soon as binary representations such as NArith are available,
+  it is clearly better to convert to/from them and use their ops.
+*)
+
+Fixpoint div2 n :=
+  match n with
+  | 0 => 0
+  | S 0 => 0
+  | S (S n') => S (div2 n')
+  end.
+
+Fixpoint testbit a n : bool :=
+ match n with
+   | 0 => odd a
+   | S n => testbit (div2 a) n
+ end.
+
+Definition shiftl a n := iter n double a.
+Definition shiftr a n := iter n div2 a.
+
+Fixpoint bitwise (op:bool->bool->bool) n a b :=
+ match n with
+  | 0 => 0
+  | S n' =>
+    (if op (odd a) (odd b) then 1 else 0) +
+    2*(bitwise op n' (div2 a) (div2 b))
+ end.
+
+Definition land a b := bitwise andb a a b.
+Definition lor a b := bitwise orb (max a b) a b.
+Definition ldiff a b := bitwise (fun b b' => andb b (negb b')) a a b.
+Definition lxor a b := bitwise xorb (max a b) a b.
diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v
index 6b0db724dc..0de06c95d8 100644
--- a/theories/Init/Peano.v
+++ b/theories/Init/Peano.v
@@ -26,6 +26,7 @@
 Require Import Notations.
 Require Import Datatypes.
 Require Import Logic.
+Require Coq.Init.Nat.
 
 Open Scope nat_scope.
 
@@ -37,10 +38,8 @@ Hint Resolve f_equal_nat: core.
 
 (** The predecessor function *)
 
-Definition pred (n:nat) : nat := match n with
-                                 | O => n
-                                 | S u => u
-                                 end.
+Notation pred := Nat.pred (compat "8.4").
+
 Definition f_equal_pred := f_equal pred.
 Hint Resolve f_equal_pred: v62.
 
@@ -82,13 +81,8 @@ Hint Resolve n_Sn: core.
 
 (** Addition *)
 
-Fixpoint plus (n m:nat) : nat :=
-  match n with
-  | O => m
-  | S p => S (p + m)
-  end
-
-where "n + m" := (plus n m) : nat_scope.
+Notation plus := Nat.add (compat "8.4").
+Infix "+" := Nat.add : nat_scope.
 
 Definition f_equal2_plus := f_equal2 plus.
 Hint Resolve f_equal2_plus: v62.
@@ -103,7 +97,7 @@ Hint Resolve plus_n_O: core.
 
 Lemma plus_O_n : forall n:nat, 0 + n = n.
 Proof.
-  auto.
+  reflexivity.
 Qed.
 
 Lemma plus_n_Sm : forall n m:nat, S (n + m) = n + S m.
@@ -114,7 +108,7 @@ Hint Resolve plus_n_Sm: core.
 
 Lemma plus_Sn_m : forall n m:nat, S n + m = S (n + m).
 Proof.
-  auto.
+  reflexivity.
 Qed.
 
 (** Standard associated names *)
@@ -124,13 +118,9 @@ Notation plus_succ_r_reverse := plus_n_Sm (compat "8.2").
 
 (** Multiplication *)
 
-Fixpoint mult (n m:nat) : nat :=
-  match n with
-  | O => 0
-  | S p => m + p * m
-  end
+Notation mult := Nat.mul (compat "8.4").
+Infix "*" := Nat.mul : nat_scope.
 
-where "n * m" := (mult n m) : nat_scope.
 Definition f_equal2_mult := f_equal2 mult.
 Hint Resolve f_equal2_mult: core.
 
@@ -155,14 +145,8 @@ Notation mult_succ_r_reverse := mult_n_Sm (compat "8.2").
 
 (** Truncated subtraction: [m-n] is [0] if [n>=m] *)
 
-Fixpoint minus (n m:nat) : nat :=
-  match n, m with
-  | O, _ => n
-  | S k, O => n
-  | S k, S l => k - l
-  end
-
-where "n - m" := (minus n m) : nat_scope.
+Notation minus := Nat.sub (compat "8.4").
+Infix "-" := Nat.sub : nat_scope.
 
 (** Definition of the usual orders, the basic properties of [le] and [lt]
     can be found in files Le and Lt *)
@@ -206,6 +190,16 @@ Proof.
 intros n m. exact (le_pred (S n) (S m)).
 Qed.
 
+Theorem le_0_n : forall n, 0 <= n.
+Proof.
+ induction n; constructor; trivial.
+Qed.
+
+Theorem le_n_S : forall n m, n <= m -> S n <= S m.
+Proof.
+ induction 1; constructor; trivial.
+Qed.
+
 (** Case analysis *)
 
 Theorem nat_case :
@@ -228,44 +222,38 @@ Qed.
 
 (** Maximum and minimum : definitions and specifications *)
 
-Fixpoint max n m : nat :=
-  match n, m with
-    | O, _ => m
-    | S n', O => n
-    | S n', S m' => S (max n' m')
-  end.
+Notation max := Nat.max (compat "8.4").
+Notation min := Nat.min (compat "8.4").
 
-Fixpoint min n m : nat :=
-  match n, m with
-    | O, _ => 0
-    | S n', O => 0
-    | S n', S m' => S (min n' m')
-  end.
-
-Theorem max_l : forall n m : nat, m <= n -> max n m = n.
+Lemma max_l n m : m <= n -> Nat.max n m = n.
 Proof.
-induction n; destruct m; simpl; auto. inversion 1.
-intros. apply f_equal. apply IHn. apply le_S_n. trivial.
+ revert m; induction n; destruct m; simpl; trivial.
+ - inversion 1.
+ - intros. apply f_equal, IHn, le_S_n; trivial.
 Qed.
 
-Theorem max_r : forall n m : nat, n <= m -> max n m = m.
+Lemma max_r n m : n <= m -> Nat.max n m = m.
 Proof.
-induction n; destruct m; simpl; auto. inversion 1.
-intros. apply f_equal. apply IHn. apply le_S_n. trivial.
+ revert m; induction n; destruct m; simpl; trivial.
+ - inversion 1.
+ - intros. apply f_equal, IHn, le_S_n; trivial.
 Qed.
 
-Theorem min_l : forall n m : nat, n <= m -> min n m = n.
+Lemma min_l n m : n <= m -> Nat.min n m = n.
 Proof.
-induction n; destruct m; simpl; auto. inversion 1.
-intros. apply f_equal. apply IHn. apply le_S_n. trivial.
+ revert m; induction n; destruct m; simpl; trivial.
+ - inversion 1.
+ - intros. apply f_equal, IHn, le_S_n; trivial.
 Qed.
 
-Theorem min_r : forall n m : nat, m <= n -> min n m = m.
+Lemma min_r n m : m <= n -> Nat.min n m = m.
 Proof.
-induction n; destruct m; simpl; auto. inversion 1.
-intros. apply f_equal. apply IHn. apply le_S_n. trivial.
+ revert m; induction n; destruct m; simpl; trivial.
+ - inversion 1.
+ - intros. apply f_equal, IHn, le_S_n; trivial.
 Qed.
 
+
 Lemma nat_rect_succ_r {A} (f: A -> A) (x:A) n :
   nat_rect (fun _ => A) x (fun _ => f) (S n) = nat_rect (fun _ => A) (f x) (fun _ => f) n.
 Proof.
diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v
index 3fa62e0a4f..01383365e7 100644
--- a/theories/Init/Prelude.v
+++ b/theories/Init/Prelude.v
@@ -11,6 +11,7 @@ Require Export Logic.
 Require Export Logic_Type.
 Require Export Datatypes.
 Require Export Specif.
+Require Coq.Init.Nat.
 Require Export Peano.
 Require Export Coq.Init.Wf.
 Require Export Coq.Init.Tactics.
diff --git a/theories/Init/vo.itarget b/theories/Init/vo.itarget
index f53d55e718..cc62e66cce 100644
--- a/theories/Init/vo.itarget
+++ b/theories/Init/vo.itarget
@@ -7,3 +7,4 @@ Prelude.vo
 Specif.vo
 Tactics.vo
 Wf.vo
+Nat.vo
\ No newline at end of file