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, 81 insertions, 147 deletions

diff --git a/theories/Arith/Compare_dec.v b/theories/Arith/Compare_dec.v
index 76132aed0..bcf409e66 100644
--- a/theories/Arith/Compare_dec.v
+++ b/theories/Arith/Compare_dec.v
@@ -6,10 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Require Import Le.
-Require Import Lt.
-Require Import Gt.
-Require Import Decidable.
+Require Import Le Lt Gt Decidable PeanoNat.
 
 Local Open Scope nat_scope.
 
@@ -29,31 +26,31 @@ Defined.
 
 Definition gt_eq_gt_dec n m : {m > n} + {n = m} + {n > m}.
 Proof.
-  intros; apply lt_eq_lt_dec; assumption.
+  now apply lt_eq_lt_dec.
 Defined.
 
 Definition le_lt_dec n m : {n <= m} + {m < n}.
 Proof.
   induction n in m |- *.
-  auto with arith.
-  destruct m.
-  auto with arith.
-  elim (IHn m); auto with arith.
+  - left; auto with arith.
+  - destruct m.
+    + right; auto with arith.
+    + elim (IHn m); [left|right]; auto with arith.
 Defined.
 
 Definition le_le_S_dec n m : {n <= m} + {S m <= n}.
 Proof.
-  intros; exact (le_lt_dec n m).
+  exact (le_lt_dec n m).
 Defined.
 
 Definition le_ge_dec n m : {n <= m} + {n >= m}.
 Proof.
-  intros; elim (le_lt_dec n m); auto with arith.
+  elim (le_lt_dec n m); auto with arith.
 Defined.
 
 Definition le_gt_dec n m : {n <= m} + {n > m}.
 Proof.
-  intros; exact (le_lt_dec n m).
+  exact (le_lt_dec n m).
 Defined.
 
 Definition le_lt_eq_dec n m : n <= m -> {n < m} + {n = m}.
@@ -62,162 +59,121 @@ Proof.
   intros; absurd (m < n); auto with arith.
 Defined.
 
-Theorem le_dec : forall n m, {n <= m} + {~ n <= m}.
+Theorem le_dec n m : {n <= m} + {~ n <= m}.
 Proof.
-  intros n m. destruct (le_gt_dec n m).
-   auto with arith.
-   right. apply gt_not_le. assumption.
+  destruct (le_gt_dec n m).
+  - now left.
+  - right. now apply gt_not_le.
 Defined.
 
-Theorem lt_dec : forall n m, {n < m} + {~ n < m}.
+Theorem lt_dec n m : {n < m} + {~ n < m}.
 Proof.
-  intros; apply le_dec.
+  apply le_dec.
 Defined.
 
-Theorem gt_dec : forall n m, {n > m} + {~ n > m}.
+Theorem gt_dec n m : {n > m} + {~ n > m}.
 Proof.
-  intros; apply lt_dec.
+  apply lt_dec.
 Defined.
 
-Theorem ge_dec : forall n m, {n >= m} + {~ n >= m}.
+Theorem ge_dec n m : {n >= m} + {~ n >= m}.
 Proof.
-  intros; apply le_dec.
+  apply le_dec.
 Defined.
 
 (** Proofs of decidability *)
 
-Theorem dec_le : forall n m, decidable (n <= m).
+Theorem dec_le n m : decidable (n <= m).
 Proof.
-  intros n m; destruct (le_dec n m); unfold decidable; auto.
+  apply Nat.le_decidable.
 Qed.
 
-Theorem dec_lt : forall n m, decidable (n < m).
+Theorem dec_lt n m : decidable (n < m).
 Proof.
-  intros; apply dec_le.
+  apply Nat.lt_decidable.
 Qed.
 
-Theorem dec_gt : forall n m, decidable (n > m).
+Theorem dec_gt n m : decidable (n > m).
 Proof.
-  intros; apply dec_lt.
+  apply Nat.lt_decidable.
 Qed.
 
-Theorem dec_ge : forall n m, decidable (n >= m).
+Theorem dec_ge n m : decidable (n >= m).
 Proof.
-  intros; apply dec_le.
+  apply Nat.le_decidable.
 Qed.
 
-Theorem not_eq : forall n m, n <> m -> n < m \/ m < n.
+Theorem not_eq n m : n <> m -> n < m \/ m < n.
 Proof.
-  intros x y H; elim (lt_eq_lt_dec x y);
-    [ intros H1; elim H1;
-      [ auto with arith | intros H2; absurd (x = y); assumption ]
-      | auto with arith ].
+  apply Nat.lt_gt_cases.
 Qed.
 
-
-Theorem not_le : forall n m, ~ n <= m -> n > m.
+Theorem not_le n m : ~ n <= m -> n > m.
 Proof.
-  intros x y H; elim (le_gt_dec x y);
-    [ intros H1; absurd (x <= y); assumption | trivial with arith ].
+  apply Nat.nle_gt.
 Qed.
 
-Theorem not_gt : forall n m, ~ n > m -> n <= m.
+Theorem not_gt n m : ~ n > m -> n <= m.
 Proof.
-  intros x y H; elim (le_gt_dec x y);
-    [ trivial with arith | intros H1; absurd (x > y); assumption ].
+  apply Nat.nlt_ge.
 Qed.
 
-Theorem not_ge : forall n m, ~ n >= m -> n < m.
+Theorem not_ge n m : ~ n >= m -> n < m.
 Proof.
-  intros x y H; exact (not_le y x H).
+  apply Nat.nle_gt.
 Qed.
 
-Theorem not_lt : forall n m, ~ n < m -> n >= m.
+Theorem not_lt n m : ~ n < m -> n >= m.
 Proof.
-  intros x y H; exact (not_gt y x H).
+  apply Nat.nlt_ge.
 Qed.
 
 
-(** A ternary comparison function in the spirit of [Z.compare]. *)
+(** A ternary comparison function in the spirit of [Z.compare].
+    See now [Nat.compare] and its properties.
+    In scope [nat_scope], the notation for [Nat.compare] is "?=" *)
 
-Fixpoint nat_compare n m :=
-  match n, m with
-   | O, O => Eq
-   | O, S _ => Lt
-   | S _, O => Gt
-   | S n', S m' => nat_compare n' m'
-  end.
+Notation nat_compare := Nat.compare (compat "8.4").
 
-Lemma nat_compare_S : forall n m, nat_compare (S n) (S m) = nat_compare n m.
-Proof.
- reflexivity.
-Qed.
+Notation nat_compare_spec := Nat.compare_spec (compat "8.4").
+Notation nat_compare_eq_iff := Nat.compare_eq_iff (compat "8.4").
+Notation nat_compare_S := Nat.compare_succ (compat "8.4").
 
-Lemma nat_compare_eq_iff : forall n m, nat_compare n m = Eq <-> n = m.
+Lemma nat_compare_lt n m : n<m <-> (n ?= m) = Lt.
 Proof.
-  induction n; destruct m; simpl; split; auto; try discriminate;
-   destruct (IHn m); auto.
+ symmetry. apply Nat.compare_lt_iff.
 Qed.
 
-Lemma nat_compare_eq : forall n m, nat_compare n m = Eq -> n = m.
+Lemma nat_compare_gt n m : n>m <-> (n ?= m) = Gt.
 Proof.
-  intros; apply -> nat_compare_eq_iff; auto.
+ symmetry. apply Nat.compare_gt_iff.
 Qed.
 
-Lemma nat_compare_lt : forall n m, n<m <-> nat_compare n m = Lt.
+Lemma nat_compare_le n m : n<=m <-> (n ?= m) <> Gt.
 Proof.
-  induction n; destruct m; simpl; split; auto with arith;
-   try solve [inversion 1].
-  destruct (IHn m); auto with arith.
-  destruct (IHn m); auto with arith.
+ symmetry. apply Nat.compare_le_iff.
 Qed.
 
-Lemma nat_compare_gt : forall n m, n>m <-> nat_compare n m = Gt.
+Lemma nat_compare_ge n m : n>=m <-> (n ?= m) <> Lt.
 Proof.
-  induction n; destruct m; simpl; split; auto with arith;
-   try solve [inversion 1].
-  destruct (IHn m); auto with arith.
-  destruct (IHn m); auto with arith.
+ symmetry. apply Nat.compare_ge_iff.
 Qed.
 
-Lemma nat_compare_le : forall n m, n<=m <-> nat_compare n m <> Gt.
-Proof.
-  split.
-  intros LE; contradict LE.
-   apply lt_not_le. apply <- nat_compare_gt; auto.
-  intros NGT. apply not_lt. contradict NGT.
-   apply -> nat_compare_gt; auto.
-Qed.
-
-Lemma nat_compare_ge : forall n m, n>=m <-> nat_compare n m <> Lt.
-Proof.
-  split.
-  intros GE; contradict GE.
-   apply lt_not_le. apply <- nat_compare_lt; auto.
-  intros NLT. apply not_lt. contradict NLT.
-   apply -> nat_compare_lt; auto.
-Qed.
+(** Some projections of the above equivalences. *)
 
-Lemma nat_compare_spec :
-  forall x y, CompareSpec (x=y) (x<y) (y<x) (nat_compare x y).
+Lemma nat_compare_eq n m : (n ?= m) = Eq -> n = m.
 Proof.
- intros. 
- destruct (nat_compare x y) eqn:?; constructor.
- apply nat_compare_eq; auto.
- apply <- nat_compare_lt; auto.
- apply <- nat_compare_gt; auto.
+  apply Nat.compare_eq_iff.
 Qed.
 
-(** Some projections of the above equivalences. *)
-
-Lemma nat_compare_Lt_lt : forall n m, nat_compare n m = Lt -> n<m.
+Lemma nat_compare_Lt_lt n m : (n ?= m) = Lt -> n<m.
 Proof.
-  intros; apply <- nat_compare_lt; auto.
+  apply Nat.compare_lt_iff.
 Qed.
 
-Lemma nat_compare_Gt_gt : forall n m, nat_compare n m = Gt -> n>m.
+Lemma nat_compare_Gt_gt n m : (n ?= m) = Gt -> n>m.
 Proof.
-  intros; apply <- nat_compare_gt; auto.
+  apply Nat.compare_gt_iff.
 Qed.
 
 (** A previous definition of [nat_compare] in terms of [lt_eq_lt_dec].
@@ -230,70 +186,48 @@ Definition nat_compare_alt (n m:nat) :=
     | inright _ => Gt
   end.
 
-Lemma nat_compare_equiv: forall n m,
- nat_compare n m = nat_compare_alt n m.
+Lemma nat_compare_equiv n m : (n ?= m) = nat_compare_alt n m.
 Proof.
-  intros; unfold nat_compare_alt; destruct lt_eq_lt_dec as [[LT|EQ]|GT].
-  apply -> nat_compare_lt; auto.
-  apply <- nat_compare_eq_iff; auto.
-  apply -> nat_compare_gt; auto.
+  unfold nat_compare_alt; destruct lt_eq_lt_dec as [[|]|].
+  - now apply Nat.compare_lt_iff.
+  - now apply Nat.compare_eq_iff.
+  - now apply Nat.compare_gt_iff.
 Qed.
 
+(** A boolean version of [le] over [nat].
+    See now [Nat.leb] and its properties.
+    In scope [nat_scope], the notation for [Nat.leb] is "<=?" *)
 
-(** A boolean version of [le] over [nat]. *)
-
-Fixpoint leb (m:nat) : nat -> bool :=
-  match m with
-    | O => fun _:nat => true
-    | S m' =>
-      fun n:nat => match n with
-                     | O => false
-                     | S n' => leb m' n'
-                   end
-  end.
+Notation leb := Nat.leb (compat "8.4").
 
-Lemma leb_correct : forall m n, m <= n -> leb m n = true.
-Proof.
-  induction m as [| m IHm]. trivial.
-  destruct n. intro H. elim (le_Sn_O _ H).
-  intros. simpl. apply IHm. apply le_S_n. assumption.
-Qed.
+Notation leb_iff := Nat.leb_le (compat "8.4").
 
-Lemma leb_complete : forall m n, leb m n = true -> m <= n.
+Lemma leb_iff_conv m n : (n <=? m) = false <-> m < n.
 Proof.
-  induction m. trivial with arith.
-  destruct n. intro H. discriminate H.
-  auto with arith.
+ rewrite Nat.leb_nle. apply Nat.nle_gt.
 Qed.
 
-Lemma leb_iff : forall m n, leb m n = true <-> m <= n.
+Lemma leb_correct m n : m <= n -> (m <=? n) = true.
 Proof.
-  split; auto using leb_correct, leb_complete.
+ apply Nat.leb_le.
 Qed.
 
-Lemma leb_correct_conv : forall m n, m < n -> leb n m = false.
+Lemma leb_complete m n : (m <=? n) = true -> m <= n.
 Proof.
-  intros.
-  generalize (leb_complete n m).
-  destruct (leb n m); auto.
-  intros; elim (lt_not_le m n); auto.
+ apply Nat.leb_le.
 Qed.
 
-Lemma leb_complete_conv : forall m n, leb n m = false -> m < n.
+Lemma leb_correct_conv m n : m < n -> (n <=? m) = false.
 Proof.
-  intros m n EQ. apply not_le.
-  intro LE. apply leb_correct in LE. rewrite LE in EQ; discriminate.
+ apply leb_iff_conv.
 Qed.
 
-Lemma leb_iff_conv : forall m n, leb n m = false <-> m < n.
+Lemma leb_complete_conv m n : (n <=? m) = false -> m < n.
 Proof.
-  split; auto using leb_complete_conv, leb_correct_conv.
+ apply leb_iff_conv.
 Qed.
 
-Lemma leb_compare : forall n m, leb n m = true <-> nat_compare n m <> Gt.
+Lemma leb_compare n m : (n <=? m) = true <-> (n ?= m) <> Gt.
 Proof.
- split; intros.
- apply -> nat_compare_le. auto using leb_complete.
- apply leb_correct. apply <- nat_compare_le; auto.
+ rewrite Nat.compare_le_iff. apply Nat.leb_le.
 Qed.
-