Euclidean division for NArith

 There was already a Ndiv and Nmod, but hiddent in ZOdiv_def. We
 higlight it by putting it in a separate file, prove its specification
 without using Z (but for the moment can't avoid a detour via nat,
 though), and then instantiate general results from Natural/Abstract/NDiv

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

7 files changed, 242 insertions, 140 deletions

diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v
index f0ec2ad64..b289380fd 100644
--- a/theories/NArith/BinNat.v
+++ b/theories/NArith/BinNat.v
@@ -365,6 +365,11 @@ destruct m; destruct p; try reflexivity.
 simpl in |- *; rewrite Pmult_plus_distr_r; reflexivity.
 Qed.
 
+Theorem Nmult_plus_distr_l : forall n m p:N, p * (n + m) = p * n + p * m.
+Proof.
+intros. rewrite ! (Nmult_comm p); apply Nmult_plus_distr_r.
+Qed.
+
 Theorem Nmult_reg_r : forall n m p:N, p <> N0 -> n * p = m * p -> n = m.
 Proof.
 destruct p; intros Hp H.
diff --git a/theories/NArith/NArith.v b/theories/NArith/NArith.v
index 0d936ae83..009e64fd0 100644
--- a/theories/NArith/NArith.v
+++ b/theories/NArith/NArith.v
@@ -13,6 +13,7 @@
 Require Export BinPos.
 Require Export BinNat.
 Require Export Nnat.
+Require Export Ndiv_def.
 Require Export Ndigits.
 Require Export NArithRing.
 Require NBinary.
diff --git a/theories/NArith/Ndiv_def.v b/theories/NArith/Ndiv_def.v
new file mode 100644
index 000000000..17e821da0
--- /dev/null
+++ b/theories/NArith/Ndiv_def.v
@@ -0,0 +1,196 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+
+Require Import BinPos BinNat Pnat Plus Compare_dec.
+
+Local Open Scope N_scope.
+
+Definition NPgeb (a:N)(b:positive) :=
+  match a with
+   | 0 => false
+   | Npos na => match Pcompare na b Eq 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] *)
+
+Lemma NPgeb_ge : forall a b, NPgeb a b = true -> a >= Npos b.
+Proof.
+ destruct a; simpl; intros.
+ discriminate.
+ unfold Nge, Ncompare. now destruct Pcompare.
+Qed.
+
+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 Pcompare.
+Qed.
+
+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.
+  generalize (Pcompare_Eq_eq a b).
+  case_eq (Pcompare a b Eq); intros; auto.
+  rewrite H0; auto.
+  now rewrite Pminus_mask_diag.
+  destruct (Pminus_mask_Gt a b H) as [d [H2 [H3 _]]].
+  rewrite H2. rewrite <- H3.
+  simpl; f_equal; apply Pplus_comm.
+Qed.
+
+Lemma Plt_add_cancel_l : forall n m p, (p+n < p+m -> n<m)%positive.
+Proof.
+ intros n m p H.
+ unfold Plt in *.
+ rewrite nat_of_P_compare_morphism in *.
+ rewrite 2 nat_of_P_plus_morphism in *.
+ apply nat_compare_lt.
+ apply nat_compare_lt in H.
+ eapply plus_lt_reg_l; eauto.
+Qed.
+
+Lemma Plt_add_not_lt : forall n m, ~(n+m < n)%positive.
+Proof.
+ intros n m H.
+ unfold Plt in *.
+ rewrite nat_of_P_compare_morphism in *.
+ rewrite nat_of_P_plus_morphism in *.
+ apply nat_compare_lt in H.
+ absurd (nat_of_P m < 0)%nat.
+ red; inversion 1.
+ apply plus_lt_reg_l with (nat_of_P n). now rewrite plus_0_r.
+Qed.
+
+Lemma Nlt_add_cancel_l : forall n m p, p+n < p+m -> n<m.
+Proof.
+ intros. destruct p. simpl; auto.
+ destruct n; destruct m.
+ elim (Nlt_irrefl _ H).
+ red; auto.
+ rewrite Nplus_0_r in H. simpl in H.
+ elim (Plt_add_not_lt _ _ H).
+ apply Plt_add_cancel_l with p; auto.
+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 Nlt_add_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 Nlt_add_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_eq_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,
+  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.
+
+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.
diff --git a/theories/NArith/vo.itarget b/theories/NArith/vo.itarget
index b80d4d7c8..7692a6368 100644
--- a/theories/NArith/vo.itarget
+++ b/theories/NArith/vo.itarget
@@ -5,6 +5,7 @@ Ndec.vo
 Ndigits.vo
 Ndist.vo
 Nnat.vo
+Ndiv_def.vo
 Pnat.vo
 POrderedType.vo
 Pminmax.vo
diff --git a/theories/Numbers/Natural/Binary/NBinary.v b/theories/Numbers/Natural/Binary/NBinary.v
index d29bb32eb..e8651d47c 100644
--- a/theories/Numbers/Natural/Binary/NBinary.v
+++ b/theories/Numbers/Natural/Binary/NBinary.v
@@ -10,9 +10,9 @@
 
 (*i $Id$ i*)
 
-Require Import BinPos.
+Require Import BinPos Ndiv_def.
 Require Export BinNat.
-Require Import NAxioms NProperties.
+Require Import NAxioms NProperties NDiv.
 
 Local Open Scope N_scope.
 
@@ -138,6 +138,14 @@ clear n; intro n; do 2 rewrite Nrect_step; intro IH. apply f_wd; [reflexivity|].
 now rewrite Nrect_step.
 Qed.
 
+(** Division and modulo *)
+
+Program Instance div_wd : Proper (eq==>eq==>eq) Ndiv.
+Program Instance mod_wd : Proper (eq==>eq==>eq) Nmod.
+
+Definition div_mod := fun x y (_:y<>0) => Ndiv_mod_eq x y.
+Definition mod_upper_bound := Nmod_lt.
+
 (** The instantiation of operations.
     Placing them at the very end avoids having indirections in above lemmas. *)
 
@@ -156,10 +164,16 @@ Definition lt := Nlt.
 Definition le := Nle.
 Definition min := Nmin.
 Definition max := Nmax.
+Definition div := Ndiv.
+Definition modulo := Nmod.
 
 Include NPropFunct
  <+ UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties.
 
+(** Generic properties of [div] and [mod] *)
+
+Include NDivPropFunct.
+
 End N.
 
 (*
diff --git a/theories/ZArith/ZOdiv.v b/theories/ZArith/ZOdiv.v
index 282333c13..7b14d93bb 100644
--- a/theories/ZArith/ZOdiv.v
+++ b/theories/ZArith/ZOdiv.v
@@ -8,7 +8,7 @@
 
 
 Require Import BinPos BinNat Nnat ZArith_base ROmega ZArithRing Morphisms.
-Require Export ZOdiv_def.
+Require Export Ndiv_def ZOdiv_def.
 Require Zdiv ZBinary ZDivTrunc.
 
 Open Scope Z_scope.
@@ -31,9 +31,7 @@ Open Scope Z_scope.
 Infix "/" := ZOdiv : Z_scope.
 Infix "mod" := ZOmod (at level 40, no associativity) : Z_scope.
 
-Infix "/" := Ndiv : N_scope.
-Infix "mod" := Nmod (at level 40, no associativity) : N_scope.
-
+(*
 (** Auxiliary results on the ad-hoc comparison [NPgeb]. *)
 
 Lemma NPgeb_Zge : forall (n:N)(p:positive),
@@ -51,6 +49,7 @@ Proof.
  red; auto.
  red; simpl; destruct Pcompare; now auto.
 Qed.
+*)
 
 (** * Relation between division on N and on Z. *)
 
@@ -76,14 +75,6 @@ Qed.
    has been chosen to be [a], so this equation holds even for [b=0].
 *)
 
-Theorem N_div_mod_eq : forall a b,
-  a = (b * (Ndiv a b) + (Nmod a b))%N.
-Proof.
-  intros; generalize (Ndiv_eucl_correct a b).
-  unfold Ndiv, Nmod; destruct Ndiv_eucl; simpl.
-  intro H; rewrite H; rewrite Nmult_comm; auto.
-Qed.
-
 Theorem ZO_div_mod_eq : forall a b,
   a = b * (ZOdiv a b) + (ZOmod a b).
 Proof.
@@ -92,35 +83,8 @@ Proof.
   intro H; rewrite H; rewrite Zmult_comm; auto.
 Qed.
 
-(** Then, the inequalities constraining the remainder. *)
-
-Theorem Pdiv_eucl_remainder : forall a b:positive,
-  Z_of_N (snd (Pdiv_eucl a b)) < Zpos 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.
-    romega with *.
-    apply NPgeb_Zlt; 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.
-    romega with *.
-    apply NPgeb_Zlt; auto.
-  destruct b; simpl; romega with *.
-Qed.
-
-Theorem Nmod_lt : forall (a b:N), b<>0%N ->
-  (a mod b < b)%N.
-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.
-  romega with *.
-Qed.
-
-(** The remainder is bounded by the divisor, in term of absolute values *)
+(** Then, the inequalities constraining the remainder:
+    The remainder is bounded by the divisor, in term of absolute values *)
 
 Theorem ZOmod_lt : forall a b:Z, b<>0 ->
   Zabs (a mod b) < Zabs b.
@@ -128,7 +92,8 @@ Proof.
   destruct b as [ |b|b]; intro H; try solve [elim H;auto];
   destruct a as [ |a|a]; try solve [compute;auto]; unfold ZOmod, ZOdiv_eucl;
   generalize (Pdiv_eucl_remainder a b); destruct Pdiv_eucl; simpl;
-  try rewrite Zabs_Zopp; rewrite Zabs_eq; auto; apply Z_of_N_le_0.
+  try rewrite Zabs_Zopp; rewrite Zabs_eq; auto using Z_of_N_le_0;
+  intros LT; apply (Z_of_N_lt _ _ LT).
 Qed.
 
 (** The sign of the remainder is the one of [a]. Due to the possible
diff --git a/theories/ZArith/ZOdiv_def.v b/theories/ZArith/ZOdiv_def.v
index 88d573bb0..8e83f344d 100644
--- a/theories/ZArith/ZOdiv_def.v
+++ b/theories/ZArith/ZOdiv_def.v
@@ -7,32 +7,10 @@
 (************************************************************************)
 
 
-Require Import BinPos BinNat Nnat ZArith_base.
+Require Import BinPos BinNat Nnat ZArith_base Ndiv_def.
 
 Open Scope Z_scope.
 
-Definition NPgeb (a:N)(b:positive) :=
-  match a with
-   | N0 => false
-   | Npos na => match Pcompare na b Eq with Lt => false | _ => true end
-  end.
-
-Fixpoint Pdiv_eucl (a b:positive) : N * N :=
-  match a with
-    | xH =>
-       match b with xH => (1, 0)%N | _ => (0, 1)%N end
-    | xO a' =>
-       let (q, r) := Pdiv_eucl a' b in
-       let r' := (2 * r)%N in
-        if (NPgeb r' b) then (2 * q + 1, (Nminus r'  (Npos b)))%N
-        else  (2 * q, r')%N
-    | xI a' =>
-       let (q, r) := Pdiv_eucl a' b in
-       let r' := (2 * r + 1)%N in
-        if (NPgeb r' b) then (2 * q + 1, (Nminus r' (Npos b)))%N
-        else  (2 * q, r')%N
-  end.
-
 Definition ZOdiv_eucl (a b:Z) : Z * Z :=
   match a, b with
    | Z0,  _ => (Z0, Z0)
@@ -54,83 +32,25 @@ Definition ZOdiv_eucl (a b:Z) : Z * Z :=
 Definition ZOdiv a b := fst (ZOdiv_eucl a b).
 Definition ZOmod a b := snd (ZOdiv_eucl a b).
 
-
-Definition Ndiv_eucl (a b:N) : N * N :=
-  match a, b with
-   | N0,  _ => (N0, N0)
-   | _, N0  => (N0, 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).
-
-
-(* Proofs of specifications for these euclidean divisions. *)
-
-Theorem NPgeb_correct: forall (a:N)(b:positive),
-  if NPgeb a b then a = (Nminus a (Npos b) + Npos b)%N else True.
-Proof.
-  destruct a; intros; simpl; auto.
-  generalize (Pcompare_Eq_eq p b).
-  case_eq (Pcompare p b Eq); intros; auto.
-  rewrite H0; auto.
-  now rewrite Pminus_mask_diag.
-  destruct (Pminus_mask_Gt p b H) as [d [H2 [H3 _]]].
-  rewrite H2. rewrite <- H3.
-  simpl; f_equal; apply Pplus_comm.
-Qed.
-
-Hint Rewrite Z_of_N_plus Z_of_N_mult Z_of_N_minus Zmult_1_l Zmult_assoc
- Zmult_plus_distr_l Zmult_plus_distr_r : zdiv.
-Hint Rewrite <- Zplus_assoc : zdiv.
-
-Theorem Pdiv_eucl_correct: forall a b,
-  let (q,r) := Pdiv_eucl a b in
-  Zpos a = Z_of_N q * Zpos b + Z_of_N 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.
-     generalize (NPgeb_correct (2 * r1 + 1) b); case NPgeb; intros H.
-     set (u := Nminus (2 * r1 + 1) (Npos b)) in * |- *.
-     assert (HH: Z_of_N u = (Z_of_N (2 * r1 + 1) - Zpos b)%Z).
-        rewrite H; autorewrite with zdiv; simpl.
-        rewrite Zplus_comm, Zminus_plus; trivial.
-     rewrite HH; autorewrite with zdiv; simpl Z_of_N.
-     rewrite Zpos_xI, Hq1.
-     autorewrite with zdiv; f_equal; rewrite Zplus_minus; trivial.
-     rewrite Zpos_xI, Hq1; autorewrite with zdiv; auto.
-  intros b; generalize (IHa b); case Pdiv_eucl.
-    intros q1 r1 Hq1.
-     generalize (NPgeb_correct (2 * r1) b); case NPgeb; intros H.
-     set (u := Nminus (2 * r1) (Npos b)) in * |- *.
-     assert (HH: Z_of_N u = (Z_of_N (2 * r1) - Zpos b)%Z).
-        rewrite H; autorewrite with zdiv; simpl.
-        rewrite Zplus_comm, Zminus_plus; trivial.
-     rewrite HH; autorewrite with zdiv; simpl Z_of_N.
-     rewrite Zpos_xO, Hq1.
-     autorewrite with zdiv; f_equal; rewrite Zplus_minus; trivial.
-     rewrite Zpos_xO, Hq1; autorewrite with zdiv; auto.
-  destruct b; auto.
-Qed.
+(* Proofs of specifications for this euclidean division. *)
 
 Theorem ZOdiv_eucl_correct: forall a b,
   let (q,r) := ZOdiv_eucl a b in a = q * b + r.
 Proof.
   destruct a; destruct b; simpl; auto;
-  generalize (Pdiv_eucl_correct p p0); case Pdiv_eucl; auto; intros;
-  try change (Zneg p) with (Zopp (Zpos p)); rewrite H.
-    destruct n; auto.
-  repeat (rewrite Zopp_plus_distr || rewrite Zopp_mult_distr_l); trivial.
-  repeat (rewrite Zopp_plus_distr || rewrite Zopp_mult_distr_r); trivial.
-Qed.
+  generalize (Pdiv_eucl_correct p p0); case Pdiv_eucl; auto; intros q r H.
 
-Theorem Ndiv_eucl_correct: forall a b,
-  let (q,r) := Ndiv_eucl a b in a = (q * b + r)%N.
-Proof.
-  destruct a; destruct b; simpl; auto;
-  generalize (Pdiv_eucl_correct p p0); case Pdiv_eucl; auto; intros;
-  destruct n; destruct n0; simpl; simpl in H; try discriminate;
-  injection H; intros; subst; trivial.
+  change (Zpos p) with (Z_of_N (Npos p)). rewrite H.
+   rewrite Z_of_N_plus, Z_of_N_mult. reflexivity.
+
+  change (Zpos p) with (Z_of_N (Npos p)). rewrite H.
+   rewrite Z_of_N_plus, Z_of_N_mult. rewrite Zmult_opp_comm. reflexivity.
+
+  change (Zneg p) with (-(Z_of_N (Npos p))); rewrite H.
+   rewrite Z_of_N_plus, Z_of_N_mult.
+  rewrite Zopp_plus_distr, Zopp_mult_distr_l; trivial.
+
+  change (Zneg p) with (-(Z_of_N (Npos p))); rewrite H.
+   rewrite Z_of_N_plus, Z_of_N_mult.
+  rewrite Zopp_plus_distr, Zopp_mult_distr_r; trivial.
 Qed.