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, 69 insertions, 101 deletions

diff --git a/theories/Arith/Lt.v b/theories/Arith/Lt.v
index 8559b782b..5a793ffdd 100644
--- a/theories/Arith/Lt.v
+++ b/theories/Arith/Lt.v
@@ -6,185 +6,149 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(** Theorems about [lt] in nat. [lt] is defined in library [Init/Peano.v] as:
+(** Strict order on natural numbers.
+
+ This file is mostly OBSOLETE now, see module [PeanoNat.Nat] instead.
+
+ [lt] is defined in library [Init/Peano.v] as:
 <<
 Definition lt (n m:nat) := S n <= m.
 Infix "<" := lt : nat_scope.
 >>
 *)
 
-Require Import Le.
-Local Open Scope nat_scope.
+Require Import PeanoNat.
 
-Implicit Types m n p : nat.
+Local Open Scope nat_scope.
 
 (** * Irreflexivity *)
 
-Theorem lt_irrefl : forall n, ~ n < n.
-Proof le_Sn_n.
+Notation lt_irrefl := Nat.lt_irrefl (compat "8.4"). (* ~ x < x *)
+
 Hint Resolve lt_irrefl: arith v62.
 
 (** * Relationship between [le] and [lt] *)
 
-Theorem lt_le_S : forall n m, n < m -> S n <= m.
+Theorem lt_le_S n m : n < m -> S n <= m.
 Proof.
-  auto with arith.
+ apply Nat.le_succ_l.
 Qed.
-Hint Immediate lt_le_S: arith v62.
 
-Theorem lt_n_Sm_le : forall n m, n < S m -> n <= m.
+Theorem lt_n_Sm_le n m : n < S m -> n <= m.
 Proof.
-  auto with arith.
+ apply Nat.lt_succ_r.
 Qed.
-Hint Immediate lt_n_Sm_le: arith v62.
 
-Theorem le_lt_n_Sm : forall n m, n <= m -> n < S m.
+Theorem le_lt_n_Sm n m : n <= m -> n < S m.
 Proof.
-  auto with arith.
+ apply Nat.lt_succ_r.
 Qed.
+
+Hint Immediate lt_le_S: arith v62.
+Hint Immediate lt_n_Sm_le: arith v62.
 Hint Immediate le_lt_n_Sm: arith v62.
 
-Theorem le_not_lt : forall n m, n <= m -> ~ m < n.
+Theorem le_not_lt n m : n <= m -> ~ m < n.
 Proof.
-  induction 1; auto with arith.
+ apply Nat.le_ngt.
 Qed.
 
-Theorem lt_not_le : forall n m, n < m -> ~ m <= n.
+Theorem lt_not_le n m : n < m -> ~ m <= n.
 Proof.
-  red; intros n m Lt Le; exact (le_not_lt m n Le Lt).
+ apply Nat.lt_nge.
 Qed.
+
 Hint Immediate le_not_lt lt_not_le: arith v62.
 
 (** * Asymmetry *)
 
-Theorem lt_asym : forall n m, n < m -> ~ m < n.
-Proof.
-  induction 1; auto with arith.
-Qed.
+Notation lt_asym := Nat.lt_asymm (compat "8.4"). (* n<m -> ~m<n *)
 
-(** * Order and successor *)
+(** * Order and 0 *)
 
-Theorem lt_n_Sn : forall n, n < S n.
-Proof.
-  auto with arith.
-Qed.
-Hint Resolve lt_n_Sn: arith v62.
+Notation lt_0_Sn := Nat.lt_0_succ (compat "8.4"). (* 0 < S n *)
+Notation lt_n_0 := Nat.nlt_0_r (compat "8.4"). (* ~ n < 0 *)
 
-Theorem lt_S : forall n m, n < m -> n < S m.
+Theorem neq_0_lt n : 0 <> n -> 0 < n.
 Proof.
-  auto with arith.
+ intros. now apply Nat.neq_0_lt_0, Nat.neq_sym.
 Qed.
-Hint Resolve lt_S: arith v62.
 
-Theorem lt_n_S : forall n m, n < m -> S n < S m.
+Theorem lt_0_neq n : 0 < n -> 0 <> n.
 Proof.
-  auto with arith.
+ intros. now apply Nat.neq_sym, Nat.neq_0_lt_0.
 Qed.
-Hint Resolve lt_n_S: arith v62.
 
-Theorem lt_S_n : forall n m, S n < S m -> n < m.
+Hint Resolve lt_0_Sn lt_n_0 : arith v62.
+Hint Immediate neq_0_lt lt_0_neq: arith v62.
+
+(** * Order and successor *)
+
+Notation lt_n_Sn := Nat.lt_succ_diag_r (compat "8.4"). (* n < S n *)
+Notation lt_S := Nat.lt_lt_succ_r (compat "8.4"). (* n < m -> n < S m *)
+
+Theorem lt_n_S n m : n < m -> S n < S m.
 Proof.
-  auto with arith.
+ apply Nat.succ_lt_mono.
 Qed.
-Hint Immediate lt_S_n: arith v62.
 
-Theorem lt_0_Sn : forall n, 0 < S n.
+Theorem lt_S_n n m : S n < S m -> n < m.
 Proof.
-  auto with arith.
+ apply Nat.succ_lt_mono.
 Qed.
-Hint Resolve lt_0_Sn: arith v62.
 
-Theorem lt_n_0 : forall n, ~ n < 0.
-Proof le_Sn_0.
-Hint Resolve lt_n_0: arith v62.
+Hint Resolve lt_n_Sn lt_S lt_n_S : arith v62.
+Hint Immediate lt_S_n : arith v62.
 
 (** * Predecessor *)
 
-Lemma S_pred : forall n m, m < n -> n = S (pred n).
+Lemma S_pred n m : m < n -> n = S (pred n).
 Proof.
-induction 1; auto with arith.
+ intros. symmetry. now apply Nat.lt_succ_pred with m.
 Qed.
 
-Lemma lt_pred : forall n m, S n < m -> n < pred m.
+Lemma lt_pred n m : S n < m -> n < pred m.
 Proof.
-induction 1; simpl; auto with arith.
+ apply Nat.lt_succ_lt_pred.
 Qed.
-Hint Immediate lt_pred: arith v62.
 
-Lemma lt_pred_n_n : forall n, 0 < n -> pred n < n.
-destruct 1; simpl; auto with arith.
+Lemma lt_pred_n_n n : 0 < n -> pred n < n.
+Proof.
+ intros. now apply Nat.lt_pred_l, Nat.neq_0_lt_0.
 Qed.
+
+Hint Immediate lt_pred: arith v62.
 Hint Resolve lt_pred_n_n: arith v62.
 
 (** * Transitivity properties *)
 
-Theorem lt_trans : forall n m p, n < m -> m < p -> n < p.
-Proof.
-  induction 2; auto with arith.
-Qed.
-
-Theorem lt_le_trans : forall n m p, n < m -> m <= p -> n < p.
-Proof.
-  induction 2; auto with arith.
-Qed.
-
-Theorem le_lt_trans : forall n m p, n <= m -> m < p -> n < p.
-Proof.
-  induction 2; auto with arith.
-Qed.
+Notation lt_trans := Nat.lt_trans (compat "8.4").
+Notation lt_le_trans := Nat.lt_le_trans (compat "8.4").
+Notation le_lt_trans := Nat.le_lt_trans (compat "8.4").
 
 Hint Resolve lt_trans lt_le_trans le_lt_trans: arith v62.
 
 (** * Large = strict or equal *)
 
-Theorem le_lt_or_eq : forall n m, n <= m -> n < m \/ n = m.
-Proof.
-  induction 1; auto with arith.
-Qed.
+Notation le_lt_or_eq_iff := Nat.lt_eq_cases (compat "8.4").
 
-Theorem le_lt_or_eq_iff : forall n m, n <= m <-> n < m \/ n = m.
+Theorem le_lt_or_eq n m : n <= m -> n < m \/ n = m.
 Proof.
-  split.
-  intros; apply le_lt_or_eq; auto.
-  destruct 1; subst; auto with arith.
+ apply Nat.lt_eq_cases.
 Qed.
 
-Theorem lt_le_weak : forall n m, n < m -> n <= m.
-Proof.
-  auto with arith.
-Qed.
+Notation lt_le_weak := Nat.lt_le_incl (compat "8.4").
+
 Hint Immediate lt_le_weak: arith v62.
 
 (** * Dichotomy *)
 
-Theorem le_or_lt : forall n m, n <= m \/ m < n.
-Proof.
-  intros n m; pattern n, m; apply nat_double_ind; auto with arith.
-  induction 1; auto with arith.
-Qed.
-
-Theorem nat_total_order : forall n m, n <> m -> n < m \/ m < n.
-Proof.
-  intros m n diff.
-  elim (le_or_lt n m); [ intro H'0 | auto with arith ].
-  elim (le_lt_or_eq n m); auto with arith.
-  intro H'; elim diff; auto with arith.
-Qed.
-
-(** * Comparison to 0 *)
+Notation le_or_lt := Nat.le_gt_cases (compat "8.4"). (* n <= m \/ m < n *)
 
-Theorem neq_0_lt : forall n, 0 <> n -> 0 < n.
+Theorem nat_total_order n m : n <> m -> n < m \/ m < n.
 Proof.
-  induction n; auto with arith.
-  intros; absurd (0 = 0); trivial with arith.
+ apply Nat.lt_gt_cases.
 Qed.
-Hint Immediate neq_0_lt: arith v62.
-
-Theorem lt_0_neq : forall n, 0 < n -> 0 <> n.
-Proof.
-  induction 1; auto with arith.
-Qed.
-Hint Immediate lt_0_neq: arith v62.
 
 (* begin hide *)
 Notation lt_O_Sn := lt_0_Sn (only parsing).
@@ -192,3 +156,7 @@ Notation neq_O_lt := neq_0_lt (only parsing).
 Notation lt_O_neq := lt_0_neq (only parsing).
 Notation lt_n_O := lt_n_0 (only parsing).
 (* end hide *)
+
+(** For compatibility, we "Require" the same files as before *)
+
+Require Import Le.