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, 50 insertions, 87 deletions

diff --git a/theories/Arith/Minus.v b/theories/Arith/Minus.v
index 480243311..cb6cc646f 100644
--- a/theories/Arith/Minus.v
+++ b/theories/Arith/Minus.v
@@ -6,151 +6,114 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(** [minus] (difference between two natural numbers) is defined in [Init/Peano.v] as:
+(** Properties of subtraction between natural numbers.
+
+ This file is mostly OBSOLETE now, see module [PeanoNat.Nat] instead.
+
+ [minus] is now an alias for [Nat.sub], which is defined in [Init/Nat.v] as:
 <<
-Fixpoint minus (n m:nat) : nat :=
+Fixpoint sub (n m:nat) : nat :=
   match n, m with
-  | O, _ => n
-  | S k, O => S k
   | S k, S l => k - l
+  | _, _ => n
   end
-where "n - m" := (minus n m) : nat_scope.
+where "n - m" := (sub n m) : nat_scope.
 >>
 *)
 
-Require Import Lt.
-Require Import Le.
+Require Import PeanoNat Lt Le.
 
 Local Open Scope nat_scope.
 
-Implicit Types m n p : nat.
-
 (** * 0 is right neutral *)
 
-Lemma minus_n_O : forall n, n = n - 0.
+Lemma minus_n_O n : n = n - 0.
 Proof.
-  induction n; simpl; auto with arith.
+ symmetry. apply Nat.sub_0_r.
 Qed.
-Hint Resolve minus_n_O: arith v62.
 
 (** * Permutation with successor *)
 
-Lemma minus_Sn_m : forall n m, m <= n -> S (n - m) = S n - m.
+Lemma minus_Sn_m n m : m <= n -> S (n - m) = S n - m.
 Proof.
-  intros n m Le; pattern m, n; apply le_elim_rel; simpl;
-    auto with arith.
+ intros. symmetry. now apply Nat.sub_succ_l.
 Qed.
-Hint Resolve minus_Sn_m: arith v62.
 
-Theorem pred_of_minus : forall n, pred n = n - 1.
+Theorem pred_of_minus n : pred n = n - 1.
 Proof.
-  intro x; induction x; simpl; auto with arith.
+ symmetry. apply Nat.sub_1_r.
 Qed.
 
 (** * Diagonal *)
 
-Lemma minus_diag : forall n, n - n = 0.
-Proof.
-  induction n; simpl; auto with arith.
-Qed.
+Notation minus_diag := Nat.sub_diag (compat "8.4"). (* n - n = 0 *)
 
-Lemma minus_diag_reverse : forall n, 0 = n - n.
+Lemma minus_diag_reverse n : 0 = n - n.
 Proof.
-  auto using minus_diag.
+ symmetry. apply Nat.sub_diag.
 Qed.
-Hint Resolve minus_diag_reverse: arith v62.
 
 Notation minus_n_n := minus_diag_reverse.
 
 (** * Simplification *)
 
-Lemma minus_plus_simpl_l_reverse : forall n m p, n - m = p + n - (p + m).
+Lemma minus_plus_simpl_l_reverse n m p : n - m = p + n - (p + m).
 Proof.
-  induction p; simpl; auto with arith.
+ now rewrite Nat.sub_add_distr, Nat.add_comm, Nat.add_sub.
 Qed.
-Hint Resolve minus_plus_simpl_l_reverse: arith v62.
 
 (** * Relation with plus *)
 
-Lemma plus_minus : forall n m p, n = m + p -> p = n - m.
+Lemma plus_minus n m p : n = m + p -> p = n - m.
 Proof.
-  intros n m p; pattern m, n; apply nat_double_ind; simpl;
-    intros.
-  replace (n0 - 0) with n0; auto with arith.
-  absurd (0 = S (n0 + p)); auto with arith.
-  auto with arith.
+ symmetry. now apply Nat.add_sub_eq_l.
 Qed.
-Hint Immediate plus_minus: arith v62.
 
-Lemma minus_plus : forall n m, n + m - n = m.
-  symmetry ; auto with arith.
+Lemma minus_plus n m : n + m - n = m.
+Proof.
+ rewrite Nat.add_comm. apply Nat.add_sub.
 Qed.
-Hint Resolve minus_plus: arith v62.
 
-Lemma le_plus_minus : forall n m, n <= m -> m = n + (m - n).
+Lemma le_plus_minus_r n m : n <= m -> n + (m - n) = m.
 Proof.
-  intros n m Le; pattern n, m; apply le_elim_rel; simpl;
-    auto with arith.
+ rewrite Nat.add_comm. apply Nat.sub_add.
 Qed.
-Hint Resolve le_plus_minus: arith v62.
 
-Lemma le_plus_minus_r : forall n m, n <= m -> n + (m - n) = m.
+Lemma le_plus_minus n m : n <= m -> m = n + (m - n).
 Proof.
-  symmetry ; auto with arith.
+ intros. symmetry. rewrite Nat.add_comm. now apply Nat.sub_add.
 Qed.
-Hint Resolve le_plus_minus_r: arith v62.
 
 (** * Relation with order *)
 
-Theorem minus_le_compat_r : forall n m p : nat, n <= m -> n - p <= m - p.
-Proof.
-  intros n m p; generalize n m; clear n m; induction p as [|p HI].
-    intros n m; rewrite <- (minus_n_O n); rewrite <- (minus_n_O m); trivial.
-
-    intros n m Hnm; apply le_elim_rel with (n:=n) (m:=m); auto with arith.
-    intros q r H _. simpl. auto using HI.
-Qed.
-
-Theorem minus_le_compat_l : forall n m p : nat, n <= m -> p - m <= p - n.
-Proof.
-  intros n m p; generalize n m; clear n m; induction p as [|p HI].
-    trivial.
+Notation minus_le_compat_r :=
+  Nat.sub_le_mono_r (compat "8.4"). (* n <= m -> n - p <= m - p. *)
 
-    intros n m Hnm; apply le_elim_rel with (n:=n) (m:=m); trivial.
-      intros q; destruct q; auto with arith.
-        simpl.
-        apply le_trans with (m := p - 0); [apply HI | rewrite <- minus_n_O];
-          auto with arith.
+Notation minus_le_compat_l :=
+  Nat.sub_le_mono_l (compat "8.4"). (* n <= m -> p - m <= p - n. *)
 
-      intros q r Hqr _. simpl. auto using HI.
-Qed.
+Notation le_minus := Nat.le_sub_l (compat "8.4"). (* n - m <= n *)
+Notation lt_minus := Nat.sub_lt (compat "8.4"). (* m <= n -> 0 < m -> n-m < n *)
 
-Corollary le_minus : forall n m, n - m <= n.
+Lemma lt_O_minus_lt n m : 0 < n - m -> m < n.
 Proof.
-  intros n m; rewrite minus_n_O; auto using minus_le_compat_l with arith.
+ apply Nat.lt_add_lt_sub_r.
 Qed.
 
-Lemma lt_minus : forall n m, m <= n -> 0 < m -> n - m < n.
+Theorem not_le_minus_0 n m : ~ m <= n -> n - m = 0.
 Proof.
-  intros n m Le; pattern m, n; apply le_elim_rel; simpl;
-    auto using le_minus with arith.
-    intros; absurd (0 < 0); auto with arith.
+ intros. now apply Nat.sub_0_le, Nat.lt_le_incl, Nat.lt_nge.
 Qed.
-Hint Resolve lt_minus: arith v62.
 
-Lemma lt_O_minus_lt : forall n m, 0 < n - m -> m < n.
-Proof.
-  intros n m; pattern n, m; apply nat_double_ind; simpl;
-    auto with arith.
-  intros; absurd (0 < 0); trivial with arith.
-Qed.
-Hint Immediate lt_O_minus_lt: arith v62.
+(** * Hints *)
 
-Theorem not_le_minus_0 : forall n m, ~ m <= n -> n - m = 0.
-Proof.
-  intros y x; pattern y, x; apply nat_double_ind;
-    [ simpl; trivial with arith
-      | intros n H; absurd (0 <= S n); [ assumption | apply le_O_n ]
-      | simpl; intros n m H1 H2; apply H1; unfold not; intros H3;
-	apply H2; apply le_n_S; assumption ].
-Qed.
+Hint Resolve minus_n_O: arith v62.
+Hint Resolve minus_Sn_m: arith v62.
+Hint Resolve minus_diag_reverse: arith v62.
+Hint Resolve minus_plus_simpl_l_reverse: arith v62.
+Hint Immediate plus_minus: arith v62.
+Hint Resolve minus_plus: arith v62.
+Hint Resolve le_plus_minus: arith v62.
+Hint Resolve le_plus_minus_r: arith v62.
+Hint Resolve lt_minus: arith v62.
+Hint Immediate lt_O_minus_lt: arith v62.