From 9363b21b8cb1669b613b7402de895715d2d9f4d7 Mon Sep 17 00:00:00 2001 From: jadep Date: Thu, 27 Apr 2017 14:30:12 -0400 Subject: stricter divmod proofs --- src/Arithmetic/Core.v | 14 ++++++++++++++ 1 file changed, 14 insertions(+) (limited to 'src/Arithmetic/Core.v') diff --git a/src/Arithmetic/Core.v b/src/Arithmetic/Core.v index 2613765d0..ff1ae67ce 100644 --- a/src/Arithmetic/Core.v +++ b/src/Arithmetic/Core.v @@ -866,6 +866,20 @@ Section DivMod. then let x := Z.log2 b in (a >> x)%RT else Z.div a b. + Lemma div_correct a b : div a b = Z.div a b. + Proof. + cbv [div]; intros. break_match; try reflexivity. + rewrite Z.shiftr_div_pow2 by apply Z.log2_nonneg. + congruence. + Qed. + + Lemma modulo_correct a b : modulo a b = Z.modulo a b. + Proof. + cbv [modulo]; intros. break_match; try reflexivity. + rewrite Z.land_ones by apply Z.log2_nonneg. + congruence. + Qed. + Lemma div_mod a b (H:b <> 0) : a = b * div a b + modulo a b. Proof. cbv [div modulo]; intros. break_match; auto using Z.div_mod. -- cgit v1.2.3