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, 138 deletions

diff --git a/theories/Arith/Mult.v b/theories/Arith/Mult.v
index cbb9b376b..d53a1646a 100644
--- a/theories/Arith/Mult.v
+++ b/theories/Arith/Mult.v
@@ -6,215 +6,139 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Require Export Plus.
-Require Export Minus.
-Require Export Lt.
-Require Export Le.
+(** * Properties of multiplication.
 
-Local Open Scope nat_scope.
+ This file is mostly OBSOLETE now, see module [PeanoNat.Nat] instead.
+
+ [Nat.mul] is defined in [Init/Nat.v].
+*)
 
-Implicit Types m n p : nat.
+Require Import PeanoNat.
+(** For Compatibility: *)
+Require Export Plus Minus Le Lt.
 
-(** Theorems about multiplication in [nat]. [mult] is defined in module [Init/Peano.v]. *)
+Local Open Scope nat_scope.
 
 (** * [nat] is a semi-ring *)
 
 (** ** Zero property *)
 
-Lemma mult_0_r : forall n, n * 0 = 0.
-Proof.
-  intro; symmetry ; apply mult_n_O.
-Qed.
-
-Lemma mult_0_l : forall n, 0 * n = 0.
-Proof.
-  reflexivity.
-Qed.
+Notation mult_0_l := Nat.mul_0_l (compat "8.4"). (* 0 * n = 0 *)
+Notation mult_0_r := Nat.mul_0_r (compat "8.4"). (* n * 0 = 0 *)
 
 (** ** 1 is neutral *)
 
-Lemma mult_1_l : forall n, 1 * n = n.
-Proof.
-  simpl; auto with arith.
-Qed.
-Hint Resolve mult_1_l: arith v62.
+Notation mult_1_l := Nat.mul_1_l (compat "8.4"). (* 1 * n = n *)
+Notation mult_1_r := Nat.mul_1_r (compat "8.4"). (* n * 1 = n *)
 
-Lemma mult_1_r : forall n, n * 1 = n.
-Proof.
-  induction n; [ trivial |
-    simpl; rewrite IHn; reflexivity].
-Qed.
-Hint Resolve mult_1_r: arith v62.
+Hint Resolve mult_1_l mult_1_r: arith v62.
 
 (** ** Commutativity *)
 
-Lemma mult_comm : forall n m, n * m = m * n.
-Proof.
-intros; induction n; simpl; auto with arith.
-rewrite <- mult_n_Sm.
-rewrite IHn; apply plus_comm.
-Qed.
+Notation mult_comm := Nat.mul_comm (compat "8.4"). (* n * m = m * n *)
+
 Hint Resolve mult_comm: arith v62.
 
 (** ** Distributivity *)
 
-Lemma mult_plus_distr_r : forall n m p, (n + m) * p = n * p + m * p.
-Proof.
-  intros; induction n; simpl; auto with arith.
-  rewrite <- plus_assoc, IHn; auto with arith.
-Qed.
-Hint Resolve mult_plus_distr_r: arith v62.
+Notation mult_plus_distr_r :=
+  Nat.mul_add_distr_r (compat "8.4"). (* (n+m)*p = n*p + m*p *)
 
-Lemma mult_plus_distr_l : forall n m p, n * (m + p) = n * m + n * p.
-Proof.
-  induction n. trivial.
-  intros. simpl. rewrite IHn. symmetry. apply plus_permute_2_in_4.
-Qed.
+Notation mult_plus_distr_l :=
+  Nat.mul_add_distr_l (compat "8.4"). (* n*(m+p) = n*m + n*p *)
 
-Lemma mult_minus_distr_r : forall n m p, (n - m) * p = n * p - m * p.
-Proof.
-  intros; induction n, m using nat_double_ind; simpl; auto with arith.
-  rewrite <- minus_plus_simpl_l_reverse; auto with arith.
-Qed.
-Hint Resolve mult_minus_distr_r: arith v62.
+Notation mult_minus_distr_r :=
+  Nat.mul_sub_distr_r (compat "8.4"). (* (n-m)*p = n*p - m*p *)
 
-Lemma mult_minus_distr_l : forall n m p, n * (m - p) = n * m - n * p.
-Proof.
-  intros n m p.
-  rewrite mult_comm, mult_minus_distr_r, (mult_comm m n), (mult_comm p n); reflexivity.
-Qed.
+Notation mult_minus_distr_l :=
+  Nat.mul_sub_distr_l (compat "8.4"). (* n*(m-p) = n*m - n*p *)
+
+Hint Resolve mult_plus_distr_r: arith v62.
+Hint Resolve mult_minus_distr_r: arith v62.
 Hint Resolve mult_minus_distr_l: arith v62.
 
 (** ** Associativity *)
 
-Lemma mult_assoc_reverse : forall n m p, n * m * p = n * (m * p).
-Proof.
-  intros; induction n; simpl; auto with arith.
-  rewrite mult_plus_distr_r.
-  induction IHn; auto with arith.
-Qed.
-Hint Resolve mult_assoc_reverse: arith v62.
+Notation mult_assoc := Nat.mul_assoc (compat "8.4"). (* n*(m*p)=n*m*p *)
 
-Lemma mult_assoc : forall n m p, n * (m * p) = n * m * p.
+Lemma mult_assoc_reverse n m p : n * m * p = n * (m * p).
 Proof.
-  auto with arith.
+ symmetry. apply Nat.mul_assoc.
 Qed.
+
+Hint Resolve mult_assoc_reverse: arith v62.
 Hint Resolve mult_assoc: arith v62.
 
 (** ** Inversion lemmas *)
 
-Lemma mult_is_O : forall n m, n * m = 0 -> n = 0 \/ m = 0.
+Lemma mult_is_O n m : n * m = 0 -> n = 0 \/ m = 0.
 Proof.
-  destruct n as [| n]; simpl; intros m H.
-    left; trivial.
-    right; apply plus_is_O in H; destruct H; trivial.
+ apply Nat.eq_mul_0.
 Qed.
 
-Lemma mult_is_one : forall n m, n * m = 1 -> n = 1 /\ m = 1.
+Lemma mult_is_one n m : n * m = 1 -> n = 1 /\ m = 1.
 Proof.
-  destruct n as [|n]; simpl; intros m H.
-    edestruct O_S; eauto.
-    destruct plus_is_one with (1:=H) as [[-> Hnm] | [-> Hnm]].
-      simpl in H; rewrite mult_0_r in H; elim (O_S _ H).
-      rewrite mult_1_r in Hnm; auto.
+ apply Nat.eq_mul_1.
 Qed.
 
 (** ** Multiplication and successor *)
 
-Lemma mult_succ_l : forall n m:nat, S n * m = n * m + m.
-Proof.
-  intros; simpl. rewrite plus_comm. reflexivity.
-Qed.
-
-Lemma mult_succ_r : forall n m:nat, n * S m = n * m + n.
-Proof.
-  induction n as [| p H]; intro m; simpl.
-  reflexivity.
-  rewrite H, <- plus_n_Sm; apply f_equal; rewrite plus_assoc; reflexivity.
-Qed.
+Notation mult_succ_l := Nat.mul_succ_l (compat "8.4"). (* S n * m = n * m + m *)
+Notation mult_succ_r := Nat.mul_succ_r (compat "8.4"). (* n * S m = n * m + n *)
 
 (** * Compatibility with orders *)
 
-Lemma mult_O_le : forall n m, m = 0 \/ n <= m * n.
+Lemma mult_O_le n m : m = 0 \/ n <= m * n.
 Proof.
-  induction m; simpl; auto with arith.
+ destruct m; [left|right]; simpl; trivial using Nat.le_add_r.
 Qed.
 Hint Resolve mult_O_le: arith v62.
 
-Lemma mult_le_compat_l : forall n m p, n <= m -> p * n <= p * m.
+Lemma mult_le_compat_l n m p : n <= m -> p * n <= p * m.
 Proof.
-  induction p as [| p IHp]; intros; simpl.
-  apply le_n.
-  auto using plus_le_compat.
+ apply Nat.mul_le_mono_nonneg_l, Nat.le_0_l. (* TODO : get rid of 0<=n hyp *)
 Qed.
 Hint Resolve mult_le_compat_l: arith.
 
-
-Lemma mult_le_compat_r : forall n m p, n <= m -> n * p <= m * p.
+Lemma mult_le_compat_r n m p : n <= m -> n * p <= m * p.
 Proof.
-  intros m n p H; rewrite mult_comm, (mult_comm n); auto with arith.
+ apply Nat.mul_le_mono_nonneg_r, Nat.le_0_l.
 Qed.
 
-Lemma mult_le_compat :
-  forall n m p (q:nat), n <= m -> p <= q -> n * p <= m * q.
+Lemma mult_le_compat n m p q : n <= m -> p <= q -> n * p <= m * q.
 Proof.
-  intros m n p q Hmn Hpq; induction Hmn.
-  induction Hpq.
-  (* m*p<=m*p *)
-  apply le_n.
-  (* m*p<=m*m0 -> m*p<=m*(S m0) *)
-  rewrite <- mult_n_Sm; apply le_trans with (m * m0).
-  assumption.
-  apply le_plus_l.
-  (* m*p<=m0*q -> m*p<=(S m0)*q *)
-  simpl; apply le_trans with (m0 * q).
-  assumption.
-  apply le_plus_r.
+  intros. apply Nat.mul_le_mono_nonneg; trivial; apply Nat.le_0_l.
 Qed.
 
-Lemma mult_S_lt_compat_l : forall n m p, m < p -> S n * m < S n * p.
+Lemma mult_S_lt_compat_l n m p : m < p -> S n * m < S n * p.
 Proof.
-  induction n; intros; simpl in *.
-    rewrite <- 2 plus_n_O; assumption.
-    auto using plus_lt_compat.
+  apply Nat.mul_lt_mono_pos_l, Nat.lt_0_succ.
 Qed.
 
 Hint Resolve mult_S_lt_compat_l: arith.
 
-Lemma mult_lt_compat_l : forall n m p, n < m -> 0 < p -> p * n < p * m.
+Lemma mult_lt_compat_l n m p : n < m -> 0 < p -> p * n < p * m.
 Proof.
- intros m n p H Hp. destruct p. elim (lt_irrefl _ Hp).
- now apply mult_S_lt_compat_l.
+ intros. now apply Nat.mul_lt_mono_pos_l.
 Qed.
 
-Lemma mult_lt_compat_r : forall n m p, n < m -> 0 < p -> n * p < m * p.
+Lemma mult_lt_compat_r n m p : n < m -> 0 < p -> n * p < m * p.
 Proof.
-  intros m n p H Hp. destruct p. elim (lt_irrefl _ Hp).
-  rewrite (mult_comm m), (mult_comm n). now apply mult_S_lt_compat_l.
+ intros. now apply Nat.mul_lt_mono_pos_r.
 Qed.
 
-Lemma mult_S_le_reg_l : forall n m p, S n * m <= S n * p -> m <= p.
+Lemma mult_S_le_reg_l n m p : S n * m <= S n * p -> m <= p.
 Proof.
-  intros m n p H; destruct (le_or_lt n p). trivial.
-  assert (H1:S m * n < S m * n).
-    apply le_lt_trans with (m := S m * p). assumption.
-    apply mult_S_lt_compat_l. assumption.
-  elim (lt_irrefl _ H1).
+ apply Nat.mul_le_mono_pos_l, Nat.lt_0_succ.
 Qed.
 
 (** * n|->2*n and n|->2n+1 have disjoint image *)
 
-Theorem odd_even_lem : forall p q, 2 * p + 1 <> 2 * q.
+Theorem odd_even_lem p q : 2 * p + 1 <> 2 * q.
 Proof.
-  induction p; destruct q.
-    discriminate.
-    simpl; rewrite plus_comm. discriminate.
-    discriminate.
-    intro H0; destruct (IHp q).
-    replace (2 * q) with (2 * S q - 2).
-      rewrite <- H0; simpl.
-      repeat rewrite (fun x y => plus_comm x (S y)); simpl;  auto.
-    simpl; rewrite (fun y => plus_comm q (S y)); destruct q; simpl; auto.
+ intro. apply (Nat.Even_Odd_False (2*q)).
+ - now exists q.
+ - now exists p.
 Qed.
 
 
@@ -232,10 +156,9 @@ Fixpoint mult_acc (s:nat) m n : nat :=
 
 Lemma mult_acc_aux : forall n m p, m + n * p = mult_acc m p n.
 Proof.
-  induction n as [| p IHp]; simpl; auto.
-  intros s m; rewrite <- plus_tail_plus; rewrite <- IHp.
-  rewrite <- plus_assoc_reverse; apply f_equal2; auto.
-  rewrite plus_comm; auto.
+  induction n as [| n IHn]; simpl; auto.
+  intros. rewrite Nat.add_assoc, IHn. f_equal.
+  rewrite Nat.add_comm. apply plus_tail_plus.
 Qed.
 
 Definition tail_mult n m := mult_acc 0 m n.