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, 11 insertions, 74 deletions

diff --git a/theories/NArith/Ngcd_def.v b/theories/NArith/Ngcd_def.v
index c25af8717..13211f467 100644
--- a/theories/NArith/Ngcd_def.v
+++ b/theories/NArith/Ngcd_def.v
@@ -7,79 +7,16 @@
 (************************************************************************)
 
 Require Import BinPos BinNat.
-
 Local Open Scope N_scope.
 
-(** * Divisibility *)
-
-Definition Ndivide p q := exists r, p*r = q.
-Notation "( p | q )" := (Ndivide p q) (at level 0) : N_scope.
-
-(** * Definition of a Pgcd function for binary natural numbers *)
-
-Definition Ngcd (a b : N) :=
- match a, b with
-  | 0, _ => b
-  | _, 0 => a
-  | Npos p, Npos q => Npos (Pos.gcd p q)
- end.
-
-(** * Generalized Gcd, also computing rests of a and b after
-    division by gcd. *)
-
-Definition Nggcd (a b : N) :=
- match a, b with
-  | 0, _ => (b,(0,1))
-  | _, 0 => (a,(1,0))
-  | Npos p, Npos q =>
-     let '(g,(aa,bb)) := Pos.ggcd p q in
-     (Npos g, (Npos aa, Npos bb))
- end.
-
-(** The first component of Nggcd is Ngcd *)
-
-Lemma Nggcd_gcd : forall  a b, fst (Nggcd a b) = Ngcd a b.
-Proof.
- intros [ |p] [ |q]; simpl; auto.
- generalize (Pos.ggcd_gcd p q). destruct Pos.ggcd as (g,(aa,bb)); simpl; congruence.
-Qed.
-
-(** The other components of Nggcd are indeed the correct factors. *)
-
-Lemma Nggcd_correct_divisors : forall a b,
-  let '(g,(aa,bb)) := Nggcd a b in
-  a=g*aa /\ b=g*bb.
-Proof.
- intros [ |p] [ |q]; simpl; auto.
- now rewrite Pmult_1_r.
- now rewrite Pmult_1_r.
- generalize (Pos.ggcd_correct_divisors p q).
- destruct Pos.ggcd as (g,(aa,bb)); simpl. destruct 1; split; congruence.
-Qed.
-
-(** We can use this fact to prove a part of the gcd correctness *)
-
-Lemma Ngcd_divide_l : forall a b, (Ngcd a b | a).
-Proof.
- intros a b. rewrite <- Nggcd_gcd. generalize (Nggcd_correct_divisors a b).
- destruct Nggcd as (g,(aa,bb)); simpl. intros (H,_). exists aa; auto.
-Qed.
-
-Lemma Ngcd_divide_r : forall a b, (Ngcd a b | b).
-Proof.
- intros a b. rewrite <- Nggcd_gcd. generalize (Nggcd_correct_divisors a b).
- destruct Nggcd as (g,(aa,bb)); simpl. intros (_,H). exists bb; auto.
-Qed.
-
-(** We now prove directly that gcd is the greatest amongst common divisors *)
-
-Lemma Ngcd_greatest : forall a b c, (c|a) -> (c|b) -> (c|Ngcd a b).
-Proof.
- intros [ |p] [ |q]; simpl; auto.
- intros [ |r]. intros (s,H). discriminate.
- intros ([ |s],Hs) ([ |t],Ht); try discriminate; simpl in *.
- destruct (Pos.gcd_greatest p q r) as (u,H).
- exists s. now inversion Hs.
- exists t. now inversion Ht.
- exists (Npos u). simpl; now f_equal.
-Qed.
+(** Obsolete file, see [BinNat] now,
+    only compatibility notations remain here. *)
+
+Notation Ndivide := N.divide (only parsing).
+Notation Ngcd := N.gcd (only parsing).
+Notation Nggcd := N.ggcd (only parsing).
+Notation Nggcd_gcd := N.ggcd_gcd (only parsing).
+Notation Nggcd_correct_divisors := N.ggcd_correct_divisors (only parsing).
+Notation Ngcd_divide_l := N.gcd_divide_l (only parsing).
+Notation Ngcd_divide_r := N.gcd_divide_r (only parsing).
+Notation Ngcd_greatest := N.gcd_greatest (only parsing).