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, 61 insertions, 70 deletions

diff --git a/theories/Arith/Gt.v b/theories/Arith/Gt.v
index 31b155071..d142f3105 100644
--- a/theories/Arith/Gt.v
+++ b/theories/Arith/Gt.v
@@ -6,149 +6,140 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(** Theorems about [gt] in [nat]. [gt] is defined in [Init/Peano.v] as:
+(** Theorems about [gt] in [nat].
+
+ This file is DEPRECATED now, see module [PeanoNat.Nat] instead,
+ which favor [lt] over [gt].
+
+ [gt] is defined in [Init/Peano.v] as:
 <<
 Definition gt (n m:nat) := m < n.
 >>
 *)
 
-Require Import Le.
-Require Import Lt.
-Require Import Plus.
+Require Import PeanoNat Le Lt Plus.
 Local Open Scope nat_scope.
 
-Implicit Types m n p : nat.
-
 (** * Order and successor *)
 
-Theorem gt_Sn_O : forall n, S n > 0.
-Proof.
-  auto with arith.
-Qed.
-Hint Resolve gt_Sn_O: arith v62.
+Theorem gt_Sn_O n : S n > 0.
+Proof Nat.lt_0_succ _.
 
-Theorem gt_Sn_n : forall n, S n > n.
-Proof.
-  auto with arith.
-Qed.
-Hint Resolve gt_Sn_n: arith v62.
+Theorem gt_Sn_n n : S n > n.
+Proof Nat.lt_succ_diag_r _.
 
-Theorem gt_n_S : forall n m, n > m -> S n > S m.
+Theorem gt_n_S n m : n > m -> S n > S m.
 Proof.
-  auto with arith.
+ apply Nat.succ_lt_mono.
 Qed.
-Hint Resolve gt_n_S: arith v62.
 
-Lemma gt_S_n : forall n m, S m > S n -> m > n.
+Lemma gt_S_n n m : S m > S n -> m > n.
 Proof.
-  auto with arith.
+ apply Nat.succ_lt_mono.
 Qed.
-Hint Immediate gt_S_n: arith v62.
 
-Theorem gt_S : forall n m, S n > m -> n > m \/ m = n.
+Theorem gt_S n m : S n > m -> n > m \/ m = n.
 Proof.
-  intros n m H; unfold gt; apply le_lt_or_eq; auto with arith.
+ intro. now apply Nat.lt_eq_cases, Nat.succ_le_mono.
 Qed.
 
-Lemma gt_pred : forall n m, m > S n -> pred m > n.
+Lemma gt_pred n m : m > S n -> pred m > n.
 Proof.
-  auto with arith.
+ apply Nat.lt_succ_lt_pred.
 Qed.
-Hint Immediate gt_pred: arith v62.
 
 (** * Irreflexivity *)
 
-Lemma gt_irrefl : forall n, ~ n > n.
-Proof lt_irrefl.
-Hint Resolve gt_irrefl: arith v62.
+Lemma gt_irrefl n : ~ n > n.
+Proof Nat.lt_irrefl _.
 
 (** * Asymmetry *)
 
-Lemma gt_asym : forall n m, n > m -> ~ m > n.
-Proof fun n m => lt_asym m n.
-
-Hint Resolve gt_asym: arith v62.
+Lemma gt_asym n m : n > m -> ~ m > n.
+Proof Nat.lt_asymm _ _.
 
 (** * Relating strict and large orders *)
 
-Lemma le_not_gt : forall n m, n <= m -> ~ n > m.
-Proof le_not_lt.
-Hint Resolve le_not_gt: arith v62.
-
-Lemma gt_not_le : forall n m, n > m -> ~ n <= m.
+Lemma le_not_gt n m : n <= m -> ~ n > m.
 Proof.
-auto with arith.
+ apply Nat.le_ngt.
 Qed.
 
-Hint Resolve gt_not_le: arith v62.
+Lemma gt_not_le n m : n > m -> ~ n <= m.
+Proof.
+ apply Nat.lt_nge.
+Qed.
 
-Theorem le_S_gt : forall n m, S n <= m -> m > n.
+Theorem le_S_gt n m : S n <= m -> m > n.
 Proof.
-  auto with arith.
+ apply Nat.le_succ_l.
 Qed.
-Hint Immediate le_S_gt: arith v62.
 
-Lemma gt_S_le : forall n m, S m > n -> n <= m.
+Lemma gt_S_le n m : S m > n -> n <= m.
 Proof.
-  intros n p; exact (lt_n_Sm_le n p).
+ apply Nat.succ_le_mono.
 Qed.
-Hint Immediate gt_S_le: arith v62.
 
-Lemma gt_le_S : forall n m, m > n -> S n <= m.
+Lemma gt_le_S n m : m > n -> S n <= m.
 Proof.
-  auto with arith.
+ apply Nat.le_succ_l.
 Qed.
-Hint Resolve gt_le_S: arith v62.
 
-Lemma le_gt_S : forall n m, n <= m -> S m > n.
+Lemma le_gt_S n m : n <= m -> S m > n.
 Proof.
-  auto with arith.
+ apply Nat.succ_le_mono.
 Qed.
-Hint Resolve le_gt_S: arith v62.
 
 (** * Transitivity *)
 
-Theorem le_gt_trans : forall n m p, m <= n -> m > p -> n > p.
+Theorem le_gt_trans n m p : m <= n -> m > p -> n > p.
 Proof.
-  red; intros; apply lt_le_trans with m; auto with arith.
+ intros. now apply Nat.lt_le_trans with m.
 Qed.
 
-Theorem gt_le_trans : forall n m p, n > m -> p <= m -> n > p.
+Theorem gt_le_trans n m p : n > m -> p <= m -> n > p.
 Proof.
-  red; intros; apply le_lt_trans with m; auto with arith.
+ intros. now apply Nat.le_lt_trans with m.
 Qed.
 
-Lemma gt_trans : forall n m p, n > m -> m > p -> n > p.
+Lemma gt_trans n m p : n > m -> m > p -> n > p.
 Proof.
-  red; intros n m p H1 H2.
-  apply lt_trans with m; auto with arith.
+ intros. now apply Nat.lt_trans with m.
 Qed.
 
-Theorem gt_trans_S : forall n m p, S n > m -> m > p -> n > p.
+Theorem gt_trans_S n m p : S n > m -> m > p -> n > p.
 Proof.
-  red; intros; apply lt_le_trans with m; auto with arith.
+ intros. apply Nat.lt_le_trans with m; trivial. now apply Nat.succ_le_mono.
 Qed.
 
-Hint Resolve gt_trans_S le_gt_trans gt_le_trans: arith v62.
-
 (** * Comparison to 0 *)
 
-Theorem gt_0_eq : forall n, n > 0 \/ 0 = n.
+Theorem gt_0_eq n : n > 0 \/ 0 = n.
 Proof.
-  intro n; apply gt_S; auto with arith.
+ destruct n; [now right | left; apply Nat.lt_0_succ].
 Qed.
 
 (** * Simplification and compatibility *)
 
-Lemma plus_gt_reg_l : forall n m p, p + n > p + m -> n > m.
+Lemma plus_gt_reg_l n m p : p + n > p + m -> n > m.
 Proof.
-  red; intros n m p H; apply plus_lt_reg_l with p; auto with arith.
+ apply Nat.add_lt_mono_l.
 Qed.
 
-Lemma plus_gt_compat_l : forall n m p, n > m -> p + n > p + m.
+Lemma plus_gt_compat_l n m p : n > m -> p + n > p + m.
 Proof.
-  auto with arith.
+ apply Nat.add_lt_mono_l.
 Qed.
+
+(** * Hints *)
+
+Hint Resolve gt_Sn_O gt_Sn_n gt_n_S : arith v62.
+Hint Immediate gt_S_n gt_pred : arith v62.
+Hint Resolve gt_irrefl gt_asym : arith v62.
+Hint Resolve le_not_gt gt_not_le : arith v62.
+Hint Immediate le_S_gt gt_S_le : arith v62.
+Hint Resolve gt_le_S le_gt_S : arith v62.
+Hint Resolve gt_trans_S le_gt_trans gt_le_trans: arith v62.
 Hint Resolve plus_gt_compat_l: arith v62.
 
 (* begin hide *)