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.

1 files changed, 36 insertions, 84 deletions

diff --git a/theories/Arith/Le.v b/theories/Arith/Le.v
index c3386787d..53bb5cde2 100644
--- a/theories/Arith/Le.v
+++ b/theories/Arith/Le.v
@@ -6,7 +6,11 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(** Order on natural numbers. [le] is defined in [Init/Peano.v] as:
+(** Order on natural numbers.
+
+ This file is mostly OBSOLETE now, see module [PeanoNat.Nat] instead.
+
+ [le] is defined in [Init/Peano.v] as:
 <<
 Inductive le (n:nat) : nat -> Prop :=
   | le_n : n <= n
@@ -14,110 +18,58 @@ Inductive le (n:nat) : nat -> Prop :=
 
 where "n <= m" := (le n m) : nat_scope.
 >>
- *)
+*)
 
-Local Open Scope nat_scope.
+Require Import PeanoNat.
 
-Implicit Types m n p : nat.
+Local Open Scope nat_scope.
 
-(** * [le] is a pre-order *)
+(** * [le] is an order on [nat] *)
 
-(** Reflexivity *)
-Theorem le_refl : forall n, n <= n.
-Proof.
-  exact le_n.
-Qed.
+Notation le_refl := Nat.le_refl (compat "8.4").
+Notation le_trans := Nat.le_trans (compat "8.4").
+Notation le_antisym := Nat.le_antisymm (compat "8.4").
 
-(** Transitivity *)
-Theorem le_trans : forall n m p, n <= m -> m <= p -> n <= p.
-Proof.
-  induction 2; auto.
-Qed.
 Hint Resolve le_trans: arith v62.
+Hint Immediate le_antisym: arith v62.
 
-(** * Properties of [le] w.r.t. successor, predecessor and 0 *)
-
-(** Comparison to 0 *)
-
-Theorem le_0_n : forall n, 0 <= n.
-Proof.
-  induction n; auto.
-Qed.
-
-Theorem le_Sn_0 : forall n, ~ S n <= 0.
-Proof.
-  red; intros n H.
-  change (IsSucc 0); elim H; simpl; auto with arith.
-Qed.
+(** * Properties of [le] w.r.t 0 *)
 
-Hint Resolve le_0_n le_Sn_0: arith v62.
+Notation le_0_n := Nat.le_0_l (compat "8.4").  (* 0 <= n *)
+Notation le_Sn_0 := Nat.nle_succ_0 (compat "8.4").  (* ~ S n <= 0 *)
 
-Theorem le_n_0_eq : forall n, n <= 0 -> 0 = n.
+Lemma le_n_0_eq n : n <= 0 -> 0 = n.
 Proof.
-  induction n. auto with arith.  idtac. auto with arith.
-  intro; contradiction le_Sn_0 with n.
+ intros. symmetry. now apply Nat.le_0_r.
 Qed.
-Hint Immediate le_n_0_eq: arith v62.
 
+(** * Properties of [le] w.r.t successor *)
 
-(** [le] and successor *)
+(** See also [Nat.succ_le_mono]. *)
 
 Theorem le_n_S : forall n m, n <= m -> S n <= S m.
-Proof.
-  induction 1; auto.
-Qed.
+Proof Peano.le_n_S.
 
-Theorem le_n_Sn : forall n, n <= S n.
-Proof.
-  auto.
-Qed.
+Theorem le_S_n : forall n m, S n <= S m -> n <= m.
+Proof Peano.le_S_n.
 
-Hint Resolve le_n_S le_n_Sn : arith v62.
+Notation le_n_Sn := Nat.le_succ_diag_r (compat "8.4"). (* n <= S n *)
+Notation le_Sn_n := Nat.nle_succ_diag_l (compat "8.4"). (* ~ S n <= n *)
 
 Theorem le_Sn_le : forall n m, S n <= m -> n <= m.
-Proof.
-  intros n m H; apply le_trans with (S n); auto with arith.
-Qed.
-Hint Immediate le_Sn_le: arith v62.
+Proof Nat.lt_le_incl.
 
-Theorem le_S_n : forall n m, S n <= S m -> n <= m.
-Proof.
-  exact Peano.le_S_n.
-Qed.
-Hint Immediate le_S_n: arith v62.
+Hint Resolve le_0_n le_Sn_0: arith v62.
+Hint Resolve le_n_S le_n_Sn le_Sn_n : arith v62.
+Hint Immediate le_n_0_eq le_Sn_le le_S_n : arith v62.
 
-Theorem le_Sn_n : forall n, ~ S n <= n.
-Proof.
-  induction n; auto with arith.
-Qed.
-Hint Resolve le_Sn_n: arith v62.
+(** * Properties of [le] w.r.t predecessor *)
 
-(** [le] and predecessor *)
+Notation le_pred_n := Nat.le_pred_l (compat "8.4"). (* pred n <= n *)
+Notation le_pred := Nat.pred_le_mono (compat "8.4"). (* n<=m -> pred n <= pred m *)
 
-Theorem le_pred_n : forall n, pred n <= n.
-Proof.
-  induction n; auto with arith.
-Qed.
 Hint Resolve le_pred_n: arith v62.
 
-Theorem le_pred : forall n m, n <= m -> pred n <= pred m.
-Proof.
-  exact Peano.le_pred.
-Qed.
-
-(** * [le] is a order on [nat] *)
-(** Antisymmetry *)
-
-Theorem le_antisym : forall n m, n <= m -> m <= n -> n = m.
-Proof.
-  intros n m H; destruct H as [|m' H]; auto with arith.
-  intros H1.
-  absurd (S m' <= m'); auto with arith.
-  apply le_trans with n; auto with arith.
-Qed.
-Hint Immediate le_antisym: arith v62.
-
-
 (** * A different elimination principle for the order on natural numbers *)
 
 Lemma le_elim_rel :
@@ -126,10 +78,10 @@ Lemma le_elim_rel :
    (forall p (q:nat), p <= q -> P p q -> P (S p) (S q)) ->
    forall n m, n <= m -> P n m.
 Proof.
-  induction n; auto with arith.
-  intros m Le.
-  elim Le; auto with arith.
-Qed.
+  intros P H0 HS.
+  induction n; trivial.
+  intros m Le. elim Le; auto with arith.
+ Qed.
 
 (* begin hide *)
 Notation le_O_n := le_0_n (only parsing).