From 70eb4b8dd94ef17cb246a25eb7525626e0f30296 Mon Sep 17 00:00:00 2001 From: letouzey Date: Tue, 5 Jan 2010 18:39:14 +0000 Subject: Numbers abstract layer: more Module Type, used especially for divisions. Properties are now rather passed as functor arg instead of via Include or some inner modules. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12629 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/ZArith/ZOdiv.v | 17 ++++++++--------- theories/ZArith/Zdiv.v | 2 +- 2 files changed, 9 insertions(+), 10 deletions(-) (limited to 'theories/ZArith') diff --git a/theories/ZArith/ZOdiv.v b/theories/ZArith/ZOdiv.v index 473e25ffb..a7dcb63de 100644 --- a/theories/ZArith/ZOdiv.v +++ b/theories/ZArith/ZOdiv.v @@ -7,10 +7,9 @@ (************************************************************************) -Require Import BinPos BinNat Nnat ZArith_base ROmega ZArithRing - ZBinary ZDivTrunc Morphisms. +Require Import BinPos BinNat Nnat ZArith_base ROmega ZArithRing Morphisms. Require Export ZOdiv_def. -Require Zdiv. +Require Zdiv ZBinary ZDivTrunc. Open Scope Z_scope. @@ -247,7 +246,7 @@ Qed. (** We know enough to prove that [ZOdiv] and [ZOmod] are instances of one of the abstract Euclidean divisions of Numbers. *) -Module ZODiv <: ZDiv ZBinAxiomsMod. +Module ZODiv <: ZDivTrunc.ZDiv ZBinary.ZBinAxiomsMod. Definition div := ZOdiv. Definition modulo := ZOmod. Program Instance div_wd : Proper (eq==>eq==>eq) div. @@ -259,12 +258,12 @@ Module ZODiv <: ZDiv ZBinAxiomsMod. Definition mod_opp_r := fun a b (_:b<>0) => ZOmod_opp_r a b. End ZODiv. -Module ZODivMod := ZBinAxiomsMod <+ ZODiv. +Module ZODivMod := ZBinary.ZBinAxiomsMod <+ ZODiv. (** We hence benefit from generic results about this abstract division. *) Module Z. - Include ZDivPropFunct ZODivMod. + Include ZDivTrunc.ZDivPropFunct ZODivMod ZBinary.ZBinPropMod. End Z. (** * Unicity results *) @@ -434,15 +433,15 @@ Proof. intros. zero_or_not b. apply Z.mod_le; auto with zarith. Qed. Theorem ZOdiv_le_upper_bound: forall a b q, 0 < b -> a <= q*b -> a/b <= q. -Proof. intros a b q; rewrite mul_comm; apply Z.div_le_upper_bound. Qed. +Proof. intros a b q; rewrite Zmult_comm; apply Z.div_le_upper_bound. Qed. Theorem ZOdiv_lt_upper_bound: forall a b q, 0 <= a -> 0 < b -> a < q*b -> a/b < q. -Proof. intros a b q; rewrite mul_comm; apply Z.div_lt_upper_bound. Qed. +Proof. intros a b q; rewrite Zmult_comm; apply Z.div_lt_upper_bound. Qed. Theorem ZOdiv_le_lower_bound: forall a b q, 0 < b -> q*b <= a -> q <= a/b. -Proof. intros a b q; rewrite mul_comm; apply Z.div_le_lower_bound. Qed. +Proof. intros a b q; rewrite Zmult_comm; apply Z.div_le_lower_bound. Qed. Theorem ZOdiv_sgn: forall a b, 0 <= Zsgn (a/b) * Zsgn a * Zsgn b. diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v index 06aa2b660..a07b6d038 100644 --- a/theories/ZArith/Zdiv.v +++ b/theories/ZArith/Zdiv.v @@ -319,7 +319,7 @@ Module ZDivMod := ZBinary.ZBinAxiomsMod <+ ZDiv. (** We hence benefit from generic results about this abstract division. *) -Module Z := ZDivFloor.ZDivPropFunct ZDivMod. +Module Z := ZDivFloor.ZDivPropFunct ZDivMod ZBinary.ZBinPropMod. (** Existence theorem *) -- cgit v1.2.3