diff options
author | Stephane Glondu <steph@glondu.net> | 2012-01-12 16:02:20 +0100 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2012-01-12 16:02:20 +0100 |
commit | 97fefe1fcca363a1317e066e7f4b99b9c1e9987b (patch) | |
tree | 97ec6b7d831cc5fb66328b0c63a11db1cbb2f158 /theories/ZArith/Zeuclid.v | |
parent | 300293c119981054c95182a90c829058530a6b6f (diff) |
Imported Upstream version 8.4~betaupstream/8.4_beta
Diffstat (limited to 'theories/ZArith/Zeuclid.v')
-rw-r--r-- | theories/ZArith/Zeuclid.v | 52 |
1 files changed, 52 insertions, 0 deletions
diff --git a/theories/ZArith/Zeuclid.v b/theories/ZArith/Zeuclid.v new file mode 100644 index 00000000..f1b59749 --- /dev/null +++ b/theories/ZArith/Zeuclid.v @@ -0,0 +1,52 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <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 *) +(************************************************************************) + +Require Import Morphisms BinInt ZDivEucl. +Local Open Scope Z_scope. + +(** * Definitions of division for binary integers, Euclid convention. *) + +(** In this convention, the remainder is always positive. + For other conventions, see [Z.div] and [Z.quot] in file [BinIntDef]. + To avoid collision with the other divisions, we place this one + under a module. +*) + +Module ZEuclid. + + Definition modulo a b := Z.modulo a (Z.abs b). + Definition div a b := (Z.sgn b) * (Z.div a (Z.abs b)). + + Instance mod_wd : Proper (eq==>eq==>eq) modulo. + Proof. congruence. Qed. + Instance div_wd : Proper (eq==>eq==>eq) div. + Proof. congruence. Qed. + + Theorem div_mod a b : b<>0 -> a = b*(div a b) + modulo a b. + Proof. + intros Hb. unfold div, modulo. + rewrite Z.mul_assoc. rewrite Z.sgn_abs. apply Z.div_mod. + now destruct b. + Qed. + + Lemma mod_always_pos a b : b<>0 -> 0 <= modulo a b < Z.abs b. + Proof. + intros Hb. unfold modulo. + apply Z.mod_pos_bound. + destruct b; compute; trivial. now destruct Hb. + Qed. + + Lemma mod_bound_pos a b : 0<=a -> 0<b -> 0 <= modulo a b < b. + Proof. + intros _ Hb. rewrite <- (Z.abs_eq b) at 3 by Z.order. + apply mod_always_pos. Z.order. + Qed. + + Include ZEuclidProp Z Z Z. + +End ZEuclid. |