diff options
Diffstat (limited to 'theories/Numbers/NatInt/NZDiv.v')
| -rw-r--r-- | theories/Numbers/NatInt/NZDiv.v | 112 |
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. |