Imported Upstream version 8.4~betaupstream/8.4_beta

1 files changed, 58 insertions, 54 deletions

diff --git a/theories/Numbers/NatInt/NZDiv.v b/theories/Numbers/NatInt/NZDiv.v
index ba1c171e..bc109ace 100644
--- a/theories/Numbers/NatInt/NZDiv.v
+++ b/theories/Numbers/NatInt/NZDiv.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -12,44 +12,36 @@ Require Import NZAxioms NZMulOrder.
 
 (** The first signatures will be common to all divisions over NZ, N and Z *)
 
-Module Type DivMod (Import T:Typ).
+Module Type DivMod (Import A : Typ).
  Parameters Inline div modulo : t -> t -> t.
 End DivMod.
 
-Module Type DivModNotation (T:Typ)(Import NZ:DivMod T).
+Module Type DivModNotation (A : Typ)(Import B : DivMod A).
  Infix "/" := div.
  Infix "mod" := modulo (at level 40, no associativity).
 End DivModNotation.
 
-Module Type DivMod' (T:Typ) := DivMod T <+ DivModNotation T.
+Module Type DivMod' (A : Typ) := DivMod A <+ DivModNotation A.
 
-Module Type NZDivCommon (Import NZ : NZAxiomsSig')(Import DM : DivMod' NZ).
+Module Type NZDivSpec (Import A : NZOrdAxiomsSig')(Import B : DivMod' A).
  Declare Instance div_wd : Proper (eq==>eq==>eq) div.
  Declare Instance mod_wd : Proper (eq==>eq==>eq) modulo.
  Axiom div_mod : forall a b, b ~= 0 -> a == b*(a/b) + (a mod b).
-End NZDivCommon.
+ Axiom mod_bound_pos : forall a b, 0<=a -> 0<b -> 0 <= a mod b < b.
+End NZDivSpec.
 
 (** The different divisions will only differ in the conditions
-    they impose on [modulo]. For NZ, we only describe behavior
-    on positive numbers.
-
-    NB: This axiom would also be true for N and Z, but redundant.
+    they impose on [modulo]. For NZ, we have only described the
+    behavior on positive numbers.
 *)
 
-Module Type NZDivSpecific (Import NZ : NZOrdAxiomsSig')(Import DM : DivMod' NZ).
- Axiom mod_bound : forall a b, 0<=a -> 0<b -> 0 <= a mod b < b.
-End NZDivSpecific.
-
-Module Type NZDiv (NZ:NZOrdAxiomsSig)
- := DivMod NZ <+ NZDivCommon NZ <+ NZDivSpecific NZ.
+Module Type NZDiv (A : NZOrdAxiomsSig) := DivMod A <+ NZDivSpec A.
+Module Type NZDiv' (A : NZOrdAxiomsSig) := NZDiv A <+ DivModNotation A.
 
-Module Type NZDiv' (NZ:NZOrdAxiomsSig) := NZDiv NZ <+ DivModNotation NZ.
-
-Module NZDivPropFunct
- (Import NZ : NZOrdAxiomsSig')
- (Import NZP : NZMulOrderPropSig NZ)
- (Import NZD : NZDiv' NZ)
-.
+Module Type NZDivProp
+ (Import A : NZOrdAxiomsSig')
+ (Import B : NZDiv' A)
+ (Import C : NZMulOrderProp A).
 
 (** Uniqueness theorems *)
 
@@ -84,7 +76,7 @@ Theorem div_unique:
 Proof.
 intros a b q r Ha (Hb,Hr) EQ.
 destruct (div_mod_unique b q (a/b) r (a mod b)); auto.
-apply mod_bound; order.
+apply mod_bound_pos; order.
 rewrite <- div_mod; order.
 Qed.
 
@@ -94,18 +86,21 @@ Theorem mod_unique:
 Proof.
 intros a b q r Ha (Hb,Hr) EQ.
 destruct (div_mod_unique b q (a/b) r (a mod b)); auto.
-apply mod_bound; order.
+apply mod_bound_pos; order.
 rewrite <- div_mod; order.
 Qed.
 
+Theorem div_unique_exact a b q:
+ 0<=a -> 0<b -> a == b*q -> q == a/b.
+Proof.
+ intros Ha Hb H. apply div_unique with 0; nzsimpl; now try split.
+Qed.
 
 (** A division by itself returns 1 *)
 
 Lemma div_same : forall a, 0<a -> a/a == 1.
 Proof.
-intros. symmetry.
-apply div_unique with 0; intuition; try order.
-now nzsimpl.
+intros. symmetry. apply div_unique_exact; nzsimpl; order.
 Qed.
 
 Lemma mod_same : forall a, 0<a -> a mod a == 0.
@@ -147,9 +142,7 @@ Qed.
 
 Lemma div_1_r: forall a, 0<=a -> a/1 == a.
 Proof.
-intros. symmetry.
-apply div_unique with 0; try split; try order; try apply lt_0_1.
-now nzsimpl.
+intros. symmetry. apply div_unique_exact; nzsimpl; order'.
 Qed.
 
 Lemma mod_1_r: forall a, 0<=a -> a mod 1 == 0.
@@ -161,20 +154,19 @@ Qed.
 
 Lemma div_1_l: forall a, 1<a -> 1/a == 0.
 Proof.
-intros; apply div_small; split; auto. apply le_succ_diag_r.
+intros; apply div_small; split; auto. apply le_0_1.
 Qed.
 
 Lemma mod_1_l: forall a, 1<a -> 1 mod a == 1.
 Proof.
-intros; apply mod_small; split; auto. apply le_succ_diag_r.
+intros; apply mod_small; split; auto. apply le_0_1.
 Qed.
 
 Lemma div_mul : forall a b, 0<=a -> 0<b -> (a*b)/b == a.
 Proof.
-intros; symmetry.
-apply div_unique with 0; try split; try order.
+intros; symmetry. apply div_unique_exact; trivial.
 apply mul_nonneg_nonneg; order.
-nzsimpl; apply mul_comm.
+apply mul_comm.
 Qed.
 
 Lemma mod_mul : forall a b, 0<=a -> 0<b -> (a*b) mod b == 0.
@@ -194,7 +186,7 @@ Theorem mod_le: forall a b, 0<=a -> 0<b -> a mod b <= a.
 Proof.
 intros. destruct (le_gt_cases b a).
 apply le_trans with b; auto.
-apply lt_le_incl. destruct (mod_bound a b); auto.
+apply lt_le_incl. destruct (mod_bound_pos a b); auto.
 rewrite lt_eq_cases; right.
 apply mod_small; auto.
 Qed.
@@ -216,7 +208,7 @@ Lemma div_str_pos : forall a b, 0<b<=a -> 0 < a/b.
 Proof.
 intros a b (Hb,Hab).
 assert (LE : 0 <= a/b) by (apply div_pos; order).
-assert (MOD : a mod b < b) by (destruct (mod_bound a b); order).
+assert (MOD : a mod b < b) by (destruct (mod_bound_pos a b); order).
 rewrite lt_eq_cases in LE; destruct LE as [LT|EQ]; auto.
 exfalso; revert Hab.
 rewrite (div_mod a b), <-EQ; nzsimpl; order.
@@ -263,7 +255,7 @@ rewrite <- (mul_1_l (a/b)) at 1.
 rewrite <- mul_lt_mono_pos_r; auto.
 apply div_str_pos; auto.
 rewrite <- (add_0_r (b*(a/b))) at 1.
-rewrite <- add_le_mono_l. destruct (mod_bound a b); order.
+rewrite <- add_le_mono_l. destruct (mod_bound_pos a b); order.
 Qed.
 
 (** [le] is compatible with a positive division. *)
@@ -282,8 +274,8 @@ apply lt_le_trans with b; auto.
 rewrite (div_mod b c) at 1 by order.
 rewrite <- add_assoc, <- add_le_mono_l.
 apply le_trans with (c+0).
-nzsimpl; destruct (mod_bound b c); order.
-rewrite <- add_le_mono_l. destruct (mod_bound a c); order.
+nzsimpl; destruct (mod_bound_pos b c); order.
+rewrite <- add_le_mono_l. destruct (mod_bound_pos a c); order.
 Qed.
 
 (** The following two properties could be used as specification of div *)
@@ -293,7 +285,7 @@ Proof.
 intros.
 rewrite (add_le_mono_r _ _ (a mod b)), <- div_mod by order.
 rewrite <- (add_0_r a) at 1.
-rewrite <- add_le_mono_l. destruct (mod_bound a b); order.
+rewrite <- add_le_mono_l. destruct (mod_bound_pos a b); order.
 Qed.
 
 Lemma mul_succ_div_gt : forall a b, 0<=a -> 0<b -> a < b*(S (a/b)).
@@ -302,7 +294,7 @@ intros.
 rewrite (div_mod a b) at 1 by order.
 rewrite (mul_succ_r).
 rewrite <- add_lt_mono_l.
-destruct (mod_bound a b); auto.
+destruct (mod_bound_pos a b); auto.
 Qed.
 
 
@@ -359,7 +351,7 @@ Proof.
  apply mul_le_mono_nonneg_r; try order.
  apply div_pos; order.
  rewrite <- (add_0_r (r*(p/r))) at 1.
- rewrite <- add_le_mono_l. destruct (mod_bound p r); order.
+ rewrite <- add_le_mono_l. destruct (mod_bound_pos p r); order.
 Qed.
 
 
@@ -371,7 +363,7 @@ Proof.
  intros.
  symmetry.
  apply mod_unique with (a/c+b); auto.
- apply mod_bound; auto.
+ apply mod_bound_pos; auto.
  rewrite mul_add_distr_l, add_shuffle0, <- div_mod by order.
  now rewrite mul_comm.
 Qed.
@@ -404,8 +396,8 @@ Proof.
  apply div_unique with ((a mod b)*c).
  apply mul_nonneg_nonneg; order.
  split.
- apply mul_nonneg_nonneg; destruct (mod_bound a b); order.
- rewrite <- mul_lt_mono_pos_r; auto. destruct (mod_bound a b); auto.
+ apply mul_nonneg_nonneg; destruct (mod_bound_pos a b); order.
+ rewrite <- mul_lt_mono_pos_r; auto. destruct (mod_bound_pos a b); auto.
  rewrite (div_mod a b) at 1 by order.
  rewrite mul_add_distr_r.
  rewrite add_cancel_r.
@@ -441,7 +433,7 @@ Qed.
 Theorem mod_mod: forall a n, 0<=a -> 0<n ->
  (a mod n) mod n == a mod n.
 Proof.
- intros. destruct (mod_bound a n); auto. now rewrite mod_small_iff.
+ intros. destruct (mod_bound_pos a n); auto. now rewrite mod_small_iff.
 Qed.
 
 Lemma mul_mod_idemp_l : forall a b n, 0<=a -> 0<=b -> 0<n ->
@@ -454,7 +446,7 @@ Proof.
  rewrite mul_add_distr_l, mul_assoc.
  intros. rewrite mod_add; auto.
  now rewrite mul_comm.
- apply mul_nonneg_nonneg; destruct (mod_bound a n); auto.
+ apply mul_nonneg_nonneg; destruct (mod_bound_pos a n); auto.
 Qed.
 
 Lemma mul_mod_idemp_r : forall a b n, 0<=a -> 0<=b -> 0<n ->
@@ -467,7 +459,7 @@ Theorem mul_mod: forall a b n, 0<=a -> 0<=b -> 0<n ->
  (a * b) mod n == ((a mod n) * (b mod n)) mod n.
 Proof.
  intros. rewrite mul_mod_idemp_l, mul_mod_idemp_r; trivial. reflexivity.
- now destruct (mod_bound b n).
+ now destruct (mod_bound_pos b n).
 Qed.
 
 Lemma add_mod_idemp_l : forall a b n, 0<=a -> 0<=b -> 0<n ->
@@ -478,7 +470,7 @@ Proof.
  rewrite (div_mod a n) at 1 2 by order.
  rewrite <- add_assoc, add_comm, mul_comm.
  intros. rewrite mod_add; trivial. reflexivity.
- apply add_nonneg_nonneg; auto. destruct (mod_bound a n); auto.
+ apply add_nonneg_nonneg; auto. destruct (mod_bound_pos a n); auto.
 Qed.
 
 Lemma add_mod_idemp_r : forall a b n, 0<=a -> 0<=b -> 0<n ->
@@ -491,7 +483,7 @@ Theorem add_mod: forall a b n, 0<=a -> 0<=b -> 0<n ->
  (a+b) mod n == (a mod n + b mod n) mod n.
 Proof.
  intros. rewrite add_mod_idemp_l, add_mod_idemp_r; trivial. reflexivity.
- now destruct (mod_bound b n).
+ now destruct (mod_bound_pos b n).
 Qed.
 
 Lemma div_div : forall a b c, 0<=a -> 0<b -> 0<c ->
@@ -500,7 +492,7 @@ Proof.
  intros a b c Ha Hb Hc.
  apply div_unique with (b*((a/b) mod c) + a mod b); trivial.
  (* begin 0<= ... <b*c *)
- destruct (mod_bound (a/b) c), (mod_bound a b); auto using div_pos.
+ destruct (mod_bound_pos (a/b) c), (mod_bound_pos a b); auto using div_pos.
  split.
  apply add_nonneg_nonneg; auto.
  apply mul_nonneg_nonneg; order.
@@ -514,6 +506,18 @@ Proof.
  apply div_mod; order.
 Qed.
 
+Lemma mod_mul_r : forall a b c, 0<=a -> 0<b -> 0<c ->
+ a mod (b*c) == a mod b + b*((a/b) mod c).
+Proof.
+ intros a b c Ha Hb Hc.
+ apply add_cancel_l with (b*c*(a/(b*c))).
+ rewrite <- div_mod by (apply neq_mul_0; split; order).
+ rewrite <- div_div by trivial.
+ rewrite add_assoc, add_shuffle0, <- mul_assoc, <- mul_add_distr_l.
+ rewrite <- div_mod by order.
+ apply div_mod; order.
+Qed.
+
 (** A last inequality: *)
 
 Theorem div_mul_le:
@@ -538,5 +542,5 @@ Proof.
  rewrite (mul_le_mono_pos_l _ _ b); auto. nzsimpl. order.
 Qed.
 
-End NZDivPropFunct.
+End NZDivProp.