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, 80 insertions, 111 deletions

diff --git a/theories/Arith/Plus.v b/theories/Arith/Plus.v
index 5428ada32..3b823da6f 100644
--- a/theories/Arith/Plus.v
+++ b/theories/Arith/Plus.v
@@ -6,176 +6,139 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(** Properties of addition. [add] is defined in [Init/Peano.v] as:
+(** Properties of addition.
+
+ This file is mostly OBSOLETE now, see module [PeanoNat.Nat] instead.
+
+ [Nat.add] is defined in [Init/Nat.v] as:
 <<
-Fixpoint plus (n m:nat) : nat :=
+Fixpoint add (n m:nat) : nat :=
   match n with
   | O => m
   | S p => S (p + m)
   end
-where "n + m" := (plus n m) : nat_scope.
+where "n + m" := (add n m) : nat_scope.
 >>
- *)
+*)
 
-Require Import Le.
-Require Import Lt.
+Require Import PeanoNat.
 
 Local Open Scope nat_scope.
 
-Implicit Types m n p q : nat.
-
-(** * Zero is neutral 
-Deprecated : Already in Init/Peano.v *)
-Notation plus_0_l := plus_O_n (only parsing).
-Definition plus_0_r n := eq_sym (plus_n_O n).
-
-(** * Commutativity *)
-
-Lemma plus_comm : forall n m, n + m = m + n.
-Proof.
-  intros n m; elim n; simpl; auto with arith.
-  intros y H; elim (plus_n_Sm m y); auto with arith.
-Qed.
-Hint Immediate plus_comm: arith v62.
-
-(** * Associativity *)
+(** * Neutrality of 0, commutativity, associativity *)
 
-Definition plus_Snm_nSm : forall n m, S n + m = n + S m:=
- plus_n_Sm.
+Notation plus_0_l := Nat.add_0_l (compat "8.4").
+Notation plus_0_r := Nat.add_0_r (compat "8.4").
+Notation plus_comm := Nat.add_comm (compat "8.4").
+Notation plus_assoc := Nat.add_assoc (compat "8.4").
 
-Lemma plus_assoc : forall n m p, n + (m + p) = n + m + p.
-Proof.
-  intros n m p; elim n; simpl; auto with arith.
-Qed.
-Hint Resolve plus_assoc: arith v62.
+Notation plus_permute := Nat.add_shuffle3 (compat "8.4").
 
-Lemma plus_permute : forall n m p, n + (m + p) = m + (n + p).
-Proof.
-  intros; rewrite (plus_assoc m n p); rewrite (plus_comm m n); auto with arith.
-Qed.
+Definition plus_Snm_nSm : forall n m, S n + m = n + S m :=
+ Peano.plus_n_Sm.
 
-Lemma plus_assoc_reverse : forall n m p, n + m + p = n + (m + p).
+Lemma plus_assoc_reverse n m p : n + m + p = n + (m + p).
 Proof.
-  auto with arith.
+  symmetry. apply Nat.add_assoc.
 Qed.
-Hint Resolve plus_assoc_reverse: arith v62.
 
 (** * Simplification *)
 
-Lemma plus_reg_l : forall n m p, p + n = p + m -> n = m.
+Lemma plus_reg_l n m p : p + n = p + m -> n = m.
 Proof.
-  intros m p n; induction n; simpl; auto with arith.
+ apply Nat.add_cancel_l.
 Qed.
 
-Lemma plus_le_reg_l : forall n m p, p + n <= p + m -> n <= m.
+Lemma plus_le_reg_l n m p : p + n <= p + m -> n <= m.
 Proof.
-  induction p; simpl; auto with arith.
+ apply Nat.add_le_mono_l.
 Qed.
 
-Lemma plus_lt_reg_l : forall n m p, p + n < p + m -> n < m.
+Lemma plus_lt_reg_l n m p : p + n < p + m -> n < m.
 Proof.
-  induction p; simpl; auto with arith.
+ apply Nat.add_lt_mono_l.
 Qed.
 
 (** * Compatibility with order *)
 
-Lemma plus_le_compat_l : forall n m p, n <= m -> p + n <= p + m.
+Lemma plus_le_compat_l n m p : n <= m -> p + n <= p + m.
 Proof.
-  induction p; simpl; auto with arith.
+ apply Nat.add_le_mono_l.
 Qed.
-Hint Resolve plus_le_compat_l: arith v62.
 
-Lemma plus_le_compat_r : forall n m p, n <= m -> n + p <= m + p.
+Lemma plus_le_compat_r n m p : n <= m -> n + p <= m + p.
 Proof.
-  induction 1; simpl; auto with arith.
+ apply Nat.add_le_mono_r.
 Qed.
-Hint Resolve plus_le_compat_r: arith v62.
 
-Lemma le_plus_l : forall n m, n <= n + m.
+Lemma plus_lt_compat_l n m p : n < m -> p + n < p + m.
 Proof.
-  induction n; simpl; auto with arith.
+ apply Nat.add_lt_mono_l.
 Qed.
-Hint Resolve le_plus_l: arith v62.
 
-Lemma le_plus_r : forall n m, m <= n + m.
+Lemma plus_lt_compat_r n m p : n < m -> n + p < m + p.
 Proof.
-  intros n m; elim n; simpl; auto with arith.
+ apply Nat.add_lt_mono_r.
 Qed.
-Hint Resolve le_plus_r: arith v62.
 
-Theorem le_plus_trans : forall n m p, n <= m -> n <= m + p.
+Lemma plus_le_compat n m p q : n <= m -> p <= q -> n + p <= m + q.
 Proof.
-  intros; apply le_trans with (m := m); auto with arith.
+ apply Nat.add_le_mono.
 Qed.
-Hint Resolve le_plus_trans: arith v62.
 
-Theorem lt_plus_trans : forall n m p, n < m -> n < m + p.
+Lemma plus_le_lt_compat n m p q : n <= m -> p < q -> n + p < m + q.
 Proof.
-  intros; apply lt_le_trans with (m := m); auto with arith.
+ apply Nat.add_le_lt_mono.
 Qed.
-Hint Immediate lt_plus_trans: arith v62.
 
-Lemma plus_lt_compat_l : forall n m p, n < m -> p + n < p + m.
+Lemma plus_lt_le_compat n m p q : n < m -> p <= q -> n + p < m + q.
 Proof.
-  induction p; simpl; auto with arith.
+ apply Nat.add_lt_le_mono.
 Qed.
-Hint Resolve plus_lt_compat_l: arith v62.
 
-Lemma plus_lt_compat_r : forall n m p, n < m -> n + p < m + p.
+Lemma plus_lt_compat n m p q : n < m -> p < q -> n + p < m + q.
 Proof.
-  intros n m p H; rewrite (plus_comm n p); rewrite (plus_comm m p).
-  elim p; auto with arith.
+ apply Nat.add_lt_mono.
 Qed.
-Hint Resolve plus_lt_compat_r: arith v62.
 
-Lemma plus_le_compat : forall n m p q, n <= m -> p <= q -> n + p <= m + q.
+Lemma le_plus_l n m : n <= n + m.
 Proof.
-  intros n m p q H H0.
-  elim H; simpl; auto with arith.
+ apply Nat.le_add_r.
 Qed.
 
-Lemma plus_le_lt_compat : forall n m p q, n <= m -> p < q -> n + p < m + q.
+Lemma le_plus_r n m : m <= n + m.
 Proof.
-  unfold lt. intros. change (S n + p <= m + q). rewrite plus_Snm_nSm.
-  apply plus_le_compat; assumption.
+ rewrite Nat.add_comm. apply Nat.le_add_r.
 Qed.
 
-Lemma plus_lt_le_compat : forall n m p q, n < m -> p <= q -> n + p < m + q.
+Theorem le_plus_trans n m p : n <= m -> n <= m + p.
 Proof.
-  unfold lt. intros. change (S n + p <= m + q). apply plus_le_compat; assumption.
+  intros. now rewrite <- Nat.le_add_r.
 Qed.
 
-Lemma plus_lt_compat : forall n m p q, n < m -> p < q -> n + p < m + q.
+Theorem lt_plus_trans n m p : n < m -> n < m + p.
 Proof.
-  intros. apply plus_lt_le_compat. assumption.
-  apply lt_le_weak. assumption.
+  intros. apply Nat.lt_le_trans with m. trivial. apply Nat.le_add_r.
 Qed.
 
 (** * Inversion lemmas *)
 
-Lemma plus_is_O : forall n m, n + m = 0 -> n = 0 /\ m = 0.
+Lemma plus_is_O n m : n + m = 0 -> n = 0 /\ m = 0.
 Proof.
-  intro m; destruct m as [| n]; auto.
-  intros. discriminate H.
+  destruct n; now split.
 Qed.
 
-Definition plus_is_one :
-  forall m n, m + n = 1 -> {m = 0 /\ n = 1} + {m = 1 /\ n = 0}.
+Definition plus_is_one m n :
+  m + n = 1 -> {m = 0 /\ n = 1} + {m = 1 /\ n = 0}.
 Proof.
-  intro m; destruct m as [| n]; auto.
-  destruct n; auto.
-  intros.
-  simpl in H. discriminate H.
+  destruct m as [| m]; auto.
+  destruct m; auto.
+  discriminate.
 Defined.
 
 (** * Derived properties *)
 
-Lemma plus_permute_2_in_4 : forall n m p q, n + m + (p + q) = n + p + (m + q).
-Proof.
-  intros m n p q.
-  rewrite <- (plus_assoc m n (p + q)). rewrite (plus_assoc n p q).
-  rewrite (plus_comm n p). rewrite <- (plus_assoc p n q). apply plus_assoc.
-Qed.
+Notation plus_permute_2_in_4 := Nat.add_shuffle1 (compat "8.4").
 
 (** * Tail-recursive plus *)
 
@@ -190,31 +153,37 @@ Fixpoint tail_plus n m : nat :=
   end.
 
 Lemma plus_tail_plus : forall n m, n + m = tail_plus n m.
+Proof.
 induction n as [| n IHn]; simpl; auto.
 intro m; rewrite <- IHn; simpl; auto.
 Qed.
 
 (** * Discrimination *)
 
-Lemma succ_plus_discr : forall n m, n <> S (plus m n).
+Lemma succ_plus_discr n m : n <> S (m+n).
 Proof.
-  intros n m; induction n as [|n IHn].
-  discriminate.
-  intro H; apply IHn; apply eq_add_S; rewrite H; rewrite <- plus_n_Sm;
-    reflexivity.
+ apply Nat.succ_add_discr.
 Qed.
 
-Lemma n_SSn : forall n, n <> S (S n).
-Proof.
-  intro n; exact (succ_plus_discr n 1).
-Qed.
+Lemma n_SSn n : n <> S (S n).
+Proof (succ_plus_discr n 1).
 
-Lemma n_SSSn : forall n, n <> S (S (S n)).
-Proof.
-  intro n; exact (succ_plus_discr n 2).
-Qed.
+Lemma n_SSSn n : n <> S (S (S n)).
+Proof (succ_plus_discr n 2).
 
-Lemma n_SSSSn : forall n, n <> S (S (S (S n))).
-Proof.
-  intro n; exact (succ_plus_discr n 3).
-Qed.
+Lemma n_SSSSn n : n <> S (S (S (S n))).
+Proof (succ_plus_discr n 3).
+
+
+(** * Compatibility Hints *)
+
+Hint Immediate plus_comm : arith v62.
+Hint Resolve plus_assoc plus_assoc_reverse : arith v62.
+Hint Resolve plus_le_compat_l plus_le_compat_r : arith v62.
+Hint Resolve le_plus_l le_plus_r le_plus_trans : arith v62.
+Hint Immediate lt_plus_trans : arith v62.
+Hint Resolve plus_lt_compat_l plus_lt_compat_r : arith v62.
+
+(** For compatibility, we "Require" the same files as before *)
+
+Require Import Le Lt.