diff options
author | Stephane Glondu <steph@glondu.net> | 2013-05-08 18:03:54 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2013-05-08 18:03:54 +0200 |
commit | db38bb4ad9aff74576d3b7f00028d48f0447d5bd (patch) | |
tree | 09dafc3e5c7361d3a28e93677eadd2b7237d4f9f /theories/ZArith/Zeuclid.v | |
parent | 6e34b272d789455a9be589e27ad3a998cf25496b (diff) | |
parent | 499a11a45b5711d4eaabe84a80f0ad3ae539d500 (diff) |
Merge branch 'experimental/upstream' into upstream
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..1dfe2fb3 --- /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-2012 *) +(* \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. |