Modularization of BinNat + fixes of stdlib

 A sub-module N in BinNat now contains functions add (ex-Nplus),
 mul (ex-Nmult), ... and properties.

 In particular, this sub-module N directly instantiates NAxiomsSig
  and includes all derived properties NProp.

 Files Ndiv_def and co are now obsolete and kept only for compat

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14100 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 16 insertions, 145 deletions

diff --git a/theories/NArith/Ndiv_def.v b/theories/NArith/Ndiv_def.v
index 0850a631e..559f01f16 100644
--- a/theories/NArith/Ndiv_def.v
+++ b/theories/NArith/Ndiv_def.v
@@ -6,155 +6,26 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-
-Require Import BinPos BinNat.
-
+Require Import BinNat.
 Local Open Scope N_scope.
 
-Definition NPgeb (a:N)(b:positive) :=
-  match a with
-   | 0 => false
-   | Npos na => match Pos.compare na b with Lt => false | _ => true end
-  end.
-
-Local Notation "a >=? b" := (NPgeb a b) (at level 70).
-
-Fixpoint Pdiv_eucl (a b:positive) : N * N :=
-  match a with
-    | xH =>
-       match b with xH => (1, 0) | _ => (0, 1) end
-    | xO a' =>
-       let (q, r) := Pdiv_eucl a' b in
-       let r' := 2 * r in
-        if r' >=? b then (2 * q + 1, r' - Npos b)
-        else (2 * q, r')
-    | xI a' =>
-       let (q, r) := Pdiv_eucl a' b in
-       let r' := 2 * r + 1 in
-        if r' >=? b then (2 * q + 1, r' - Npos b)
-        else  (2 * q, r')
-  end.
-
-Definition Ndiv_eucl (a b:N) : N * N :=
-  match a, b with
-   | 0,  _ => (0, 0)
-   | _, 0  => (0, a)
-   | Npos na, Npos nb => Pdiv_eucl na nb
-  end.
-
-Definition Ndiv a b := fst (Ndiv_eucl a b).
-Definition Nmod a b := snd (Ndiv_eucl a b).
-
-Infix "/" := Ndiv : N_scope.
-Infix "mod" := Nmod (at level 40, no associativity) : N_scope.
-
-(** Auxiliary Results about [NPgeb] *)
+(** Obsolete file, see [BinNat] now,
+    only compatibility notations remain here. *)
 
-Lemma NPgeb_ge : forall a b, NPgeb a b = true -> a >= Npos b.
-Proof.
- destruct a; simpl; intros.
- discriminate.
- unfold Nge, Ncompare. now destruct Pos.compare.
-Qed.
+Definition Pdiv_eucl a b := N.pos_div_eucl a (Npos b).
 
-Lemma NPgeb_lt : forall a b, NPgeb a b = false -> a < Npos b.
-Proof.
- destruct a; simpl; intros. red; auto.
- unfold Nlt, Ncompare. now destruct Pos.compare.
-Qed.
+Definition Pdiv_eucl_correct a b :
+  let (q,r) := Pdiv_eucl a b in Npos a = q * Npos b + r
+ := N.pos_div_eucl_spec a (Npos b).
 
-Theorem NPgeb_correct: forall (a:N)(b:positive),
-  if NPgeb a b then a = a - Npos b + Npos b else True.
-Proof.
-  destruct a as [|a]; simpl; intros b; auto.
-  case Pos.compare_spec; intros; subst; auto.
-  now rewrite Pminus_mask_diag.
-  destruct (Pminus_mask_Gt a b (Pos.lt_gt _ _ H)) as [d [H2 [H3 _]]].
-  rewrite H2. rewrite <- H3.
-  simpl; f_equal; apply Pplus_comm.
-Qed.
-
-Lemma NPgeb_ineq0 : forall a p, a < Npos p -> NPgeb (2*a) p = true ->
- 2*a - Npos p < Npos p.
-Proof.
-intros a p LT GE.
-apply Nplus_lt_cancel_l with (Npos p).
-rewrite Nplus_comm.
-generalize (NPgeb_correct (2*a) p). rewrite GE. intros <-.
-rewrite <- (Nmult_1_l (Npos p)). rewrite <- Nmult_plus_distr_r.
-destruct a; auto.
-Qed.
-
-Lemma NPgeb_ineq1 : forall a p, a < Npos p -> NPgeb (2*a+1) p = true ->
-  (2*a+1) - Npos p < Npos p.
-Proof.
-intros a p LT GE.
-apply Nplus_lt_cancel_l with (Npos p).
-rewrite Nplus_comm.
-generalize (NPgeb_correct (2*a+1) p). rewrite GE. intros <-.
-rewrite <- (Nmult_1_l (Npos p)). rewrite <- Nmult_plus_distr_r.
-destruct a; auto.
-red; simpl. apply Pcompare_Gt_Lt; auto.
-Qed.
-
-(* Proofs of specifications for these euclidean divisions. *)
-
-Theorem Pdiv_eucl_correct: forall a b,
-  let (q,r) := Pdiv_eucl a b in Npos a = q * Npos b + r.
-Proof.
-  induction a; cbv beta iota delta [Pdiv_eucl]; fold Pdiv_eucl; cbv zeta.
-  intros b; generalize (IHa b); case Pdiv_eucl.
-    intros q1 r1 Hq1.
-    assert (Npos a~1 = 2*q1*Npos b + (2*r1+1))
-     by now rewrite Nplus_assoc, <- Nmult_assoc, <- Nmult_plus_distr_l, <- Hq1.
-    generalize (NPgeb_correct (2 * r1 + 1) b); case NPgeb; intros H'; auto.
-    rewrite Nmult_plus_distr_r, Nmult_1_l.
-    rewrite <- Nplus_assoc, (Nplus_comm (Npos b)), <- H'; auto.
-  intros b; generalize (IHa b); case Pdiv_eucl.
-    intros q1 r1 Hq1.
-    assert (Npos a~0 = 2*q1*Npos b + 2*r1)
-     by now rewrite <- Nmult_assoc, <- Nmult_plus_distr_l, <- Hq1.
-    generalize (NPgeb_correct (2 * r1) b); case NPgeb; intros H'; auto.
-    rewrite Nmult_plus_distr_r, Nmult_1_l.
-    rewrite <- Nplus_assoc, (Nplus_comm (Npos b)), <- H'; auto.
-  destruct b; auto.
-Qed.
-
-Theorem Ndiv_eucl_correct: forall a b,
-  let (q,r) := Ndiv_eucl a b in a = b * q + r.
-Proof.
-  destruct a as [|a]; destruct b as [|b]; simpl; auto.
-  generalize (Pdiv_eucl_correct a b); case Pdiv_eucl; intros q r.
-  destruct q. simpl; auto. rewrite Nmult_comm. intro EQ; exact EQ.
-Qed.
-
-Theorem Ndiv_mod_eq : forall a b,
-  a = b * (a/b) + (a mod b).
-Proof.
-  intros; generalize (Ndiv_eucl_correct a b).
-  unfold Ndiv, Nmod; destruct Ndiv_eucl; simpl; auto.
-Qed.
-
-Theorem Pdiv_eucl_remainder : forall a b:positive,
+Lemma Pdiv_eucl_remainder a b :
   snd (Pdiv_eucl a b) < Npos b.
-Proof.
-  induction a; cbv beta iota delta [Pdiv_eucl]; fold Pdiv_eucl; cbv zeta.
-  intros b; generalize (IHa b); case Pdiv_eucl.
-    intros q1 r1 Hr1; simpl in Hr1.
-    case_eq (NPgeb (2*r1+1) b); intros; unfold snd.
-    apply NPgeb_ineq1; auto.
-    apply NPgeb_lt; auto.
-  intros b; generalize (IHa b); case Pdiv_eucl.
-    intros q1 r1 Hr1; simpl in Hr1.
-    case_eq (NPgeb (2*r1) b); intros; unfold snd.
-    apply NPgeb_ineq0; auto.
-    apply NPgeb_lt; auto.
-  destruct b; simpl; reflexivity.
-Qed.
+Proof. now apply (N.pos_div_eucl_remainder a (Npos b)). Qed.
+
+Notation Ndiv_eucl := N.div_eucl (only parsing).
+Notation Ndiv := N.div (only parsing).
+Notation Nmod := N.modulo (only parsing).
 
-Theorem Nmod_lt : forall (a b:N), b<>0 -> a mod b < b.
-Proof.
-  destruct b as [ |b]; intro H; try solve [elim H;auto].
-  destruct a as [ |a]; try solve [compute;auto]; unfold Nmod, Ndiv_eucl.
-  generalize (Pdiv_eucl_remainder a b); destruct Pdiv_eucl; simpl; auto.
-Qed.
+Notation Ndiv_eucl_correct := N.div_eucl_spec (only parsing).
+Notation Ndiv_mod_eq := N.div_mod' (only parsing).
+Notation Nmod_lt := N.mod_lt (only parsing).