From 9764ebbb67edf73a147c536a3c4f4ed0f1a7ce9e Mon Sep 17 00:00:00 2001 From: letouzey Date: Mon, 6 Dec 2010 15:47:32 +0000 Subject: Numbers and bitwise functions. See NatInt/NZBits.v for the common axiomatization of bitwise functions over naturals / integers. Some specs aren't pretty, but easier to prove, see alternate statements in property functors {N,Z}Bits. Negative numbers are considered via the two's complement convention. We provide implementations for N (in Ndigits.v), for nat (quite dummy, just for completeness), for Z (new file Zdigits_def), for BigN (for the moment partly by converting to N, to be improved soon) and for BigZ. NOTA: For BigN.shiftl and BigN.shiftr, the two arguments are now in the reversed order (for consistency with the rest of the world): for instance BigN.shiftl 1 10 is 2^10. NOTA2: Zeven.Zdiv2 is _not_ doing (Zdiv _ 2), but rather (Zquot _ 2) on negative numbers. For the moment I've kept it intact, and have just added a Zdiv2' which is truly equivalent to (Zdiv _ 2). To reorganize someday ? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13689 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Numbers/Integer/Abstract/ZDivEucl.v | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) (limited to 'theories/Numbers/Integer/Abstract/ZDivEucl.v') diff --git a/theories/Numbers/Integer/Abstract/ZDivEucl.v b/theories/Numbers/Integer/Abstract/ZDivEucl.v index 070003972..c8fd29a54 100644 --- a/theories/Numbers/Integer/Abstract/ZDivEucl.v +++ b/theories/Numbers/Integer/Abstract/ZDivEucl.v @@ -575,6 +575,23 @@ Proof. apply div_mod; order. Qed. +(** Similarly, the following result doesn't always hold for negative + [b] and [c]. For instance [3 mod (-2*-2)) = 3] while + [3 mod (-2) + (-2)*((3/-2) mod -2) = -1]. +*) + +Lemma mod_mul_r : forall a b c, 0 0 + a mod (b*c) == a mod b + b*((a/b) mod c). +Proof. + intros a b c 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: -- cgit v1.2.3