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.

3 files changed, 43 insertions, 38 deletions

diff --git a/plugins/funind/Recdef.v b/plugins/funind/Recdef.v
index e28c845cc..e4671ccd1 100644
--- a/plugins/funind/Recdef.v
+++ b/plugins/funind/Recdef.v
@@ -5,6 +5,9 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
+
+Require Import PeanoNat.
+
 Require Compare_dec.
 Require Wf_nat.
 
@@ -19,32 +22,29 @@ Fixpoint iter (n : nat) : (A -> A) -> A -> A :=
   end.
 End Iter.
 
-Theorem SSplus_lt : forall p p' : nat, p < S (S (p + p')).
-  intro p; intro p'; change (S p <= S (S (p + p')));
-    apply le_S; apply Gt.gt_le_S; change (p < S (p + p'));
-    apply Lt.le_lt_n_Sm; apply Plus.le_plus_l.
+Theorem le_lt_SS x y : x <= y -> x < S (S y).
+Proof.
+ intros. now apply Nat.lt_succ_r, Nat.le_le_succ_r.
 Qed.
 
-
-Theorem Splus_lt : forall p p' : nat, p' < S (p + p').
-  intro p; intro p'; change (S p' <= S (p + p'));
-    apply Gt.gt_le_S; change (p' < S (p + p')); apply Lt.le_lt_n_Sm;
-       apply Plus.le_plus_r.
+Theorem Splus_lt x y : y < S (x + y).
+Proof.
+ apply Nat.lt_succ_r. rewrite Nat.add_comm. apply Nat.le_add_r.
 Qed.
 
-Theorem le_lt_SS : forall x y, x <= y -> x < S (S y).
-intro x; intro y; intro H; change (S x <= S (S y));
-    apply le_S; apply Gt.gt_le_S; change (x < S y);
-    apply Lt.le_lt_n_Sm; exact H.
+Theorem SSplus_lt x y : x < S (S (x + y)).
+Proof.
+ apply le_lt_SS, Nat.le_add_r.
 Qed.
 
 Inductive max_type (m n:nat) : Set :=
   cmt : forall v, m <= v -> n <= v -> max_type m n.
 
-Definition max : forall m n:nat, max_type m n.
-intros m n; case (Compare_dec.le_gt_dec m n).
-intros h; exists n; [exact h | apply le_n].
-intros h; exists m; [apply le_n | apply Lt.lt_le_weak; exact h].
+Definition max m n : max_type m n.
+Proof.
+ destruct (Compare_dec.le_gt_dec m n) as [h|h].
+ - exists n; [exact h | apply le_n].
+ - exists m; [apply le_n | apply Nat.lt_le_incl; exact h].
 Defined.
 
-Definition Acc_intro_generator_function := fun A R => @Acc_intro_generator A R 100.
\ No newline at end of file
+Definition Acc_intro_generator_function := fun A R => @Acc_intro_generator A R 100.
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 38cbd0c53..1fa16a301 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -43,9 +43,14 @@ open Indfun_common
 
 (* Ugly things which should not be here *)
 
-let coq_base_constant s =
-  Coqlib.gen_constant_in_modules "RecursiveDefinition"
-    (Coqlib.init_modules @ [["Coq";"Arith";"Le"];["Coq";"Arith";"Lt"]]) s;;
+let coq_constant m s =
+  Coqlib.coq_constant "RecursiveDefinition" m s
+
+let arith_Nat = ["Arith";"PeanoNat";"Nat"]
+let arith_Lt = ["Arith";"Lt"]
+
+let coq_init_constant s =
+  Coqlib.gen_constant_in_modules "RecursiveDefinition" Coqlib.init_modules s
 
 let find_reference sl s =
   let dp = Names.DirPath.make (List.rev_map Id.of_string sl) in
@@ -120,25 +125,25 @@ let v_id = Id.of_string "v"
 let def_id = Id.of_string "def"
 let p_id = Id.of_string "p"
 let rec_res_id = Id.of_string "rec_res";;
-let lt = function () -> (coq_base_constant "lt")
-let le = function () -> (coq_base_constant "le")
-let ex = function () -> (coq_base_constant "ex")
-let nat = function () -> (coq_base_constant "nat")
+let lt = function () -> (coq_init_constant "lt")
+let le = function () -> (coq_init_constant "le")
+let ex = function () -> (coq_init_constant "ex")
+let nat = function () -> (coq_init_constant "nat")
 let iter_ref () =  
   try find_reference ["Recdef"] "iter" 
   with Not_found -> error "module Recdef not loaded"
 let iter = function () -> (constr_of_global (delayed_force iter_ref))
-let eq = function () -> (coq_base_constant "eq")
+let eq = function () -> (coq_init_constant "eq")
 let le_lt_SS = function () -> (constant ["Recdef"] "le_lt_SS")
-let le_lt_n_Sm = function () -> (coq_base_constant "le_lt_n_Sm")
-let le_trans = function () -> (coq_base_constant "le_trans")
-let le_lt_trans = function () -> (coq_base_constant "le_lt_trans")
-let lt_S_n = function () -> (coq_base_constant "lt_S_n")
-let le_n = function () -> (coq_base_constant "le_n")
+let le_lt_n_Sm = function () -> (coq_constant arith_Lt "le_lt_n_Sm")
+let le_trans = function () -> (coq_constant arith_Nat "le_trans")
+let le_lt_trans = function () -> (coq_constant arith_Nat "le_lt_trans")
+let lt_S_n = function () -> (coq_constant arith_Lt "lt_S_n")
+let le_n = function () -> (coq_init_constant "le_n")
 let coq_sig_ref = function () -> (find_reference ["Coq";"Init";"Specif"] "sig")
-let coq_O = function () -> (coq_base_constant "O")
-let coq_S = function () -> (coq_base_constant "S")
-let lt_n_O = function () -> (coq_base_constant "lt_n_O")
+let coq_O = function () -> (coq_init_constant "O")
+let coq_S = function () -> (coq_init_constant "S")
+let lt_n_O = function () -> (coq_constant arith_Nat "nlt_0_r")
 let max_ref = function () -> (find_reference ["Recdef"] "max")
 let max_constr = function () -> (constr_of_global (delayed_force max_ref))
 let coq_conj = function () -> find_reference Coqlib.logic_module_name "conj"
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 88958d014..83f346242 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -304,10 +304,10 @@ let coq_le = lazy (init_constant "le")
 let coq_lt = lazy (init_constant "lt")
 let coq_ge = lazy (init_constant "ge")
 let coq_gt = lazy (init_constant "gt")
-let coq_minus = lazy (init_constant "minus")
-let coq_plus = lazy (init_constant "plus")
-let coq_mult = lazy (init_constant "mult")
-let coq_pred = lazy (init_constant "pred")
+let coq_minus = lazy (init_constant "Nat.sub")
+let coq_plus = lazy (init_constant "Nat.add")
+let coq_mult = lazy (init_constant "Nat.mul")
+let coq_pred = lazy (init_constant "Nat.pred")
 let coq_nat = lazy (init_constant "nat")
 let coq_S = lazy (init_constant "S")
 let coq_O = lazy (init_constant "O")