diff options
| author |  jadep <jade.philipoom@gmail.com> | 2017-04-27 14:30:12 -0400 |
|---|---|---|
| committer | jadephilipoom <jade.philipoom@gmail.com> | 2017-05-01 14:34:48 -0400 |
| commit | 9363b21b8cb1669b613b7402de895715d2d9f4d7 (patch) | |
| tree | 189d0f1c976d7a42aaef2d54e838fdf704c79d9e /src/Arithmetic/Core.v | |
| parent | f5043a0a3210edf80b266f20998ad5b0f3153c0d (diff) | |
stricter divmod proofs
Diffstat (limited to 'src/Arithmetic/Core.v')
| -rw-r--r-- | src/Arithmetic/Core.v | 14 |
1 files changed, 14 insertions, 0 deletions
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. |