diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2022-03-04 11:02:35 +0000 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2022-03-04 11:02:35 +0000 |
| commit | 5fe9ec29c08dc2b2e8cedb7b2d63ddca08226199 (patch) | |
| tree | 655baca3781a156c5bfe638c4ed3c84bb9a46d07 | |
| parent | 7548c4c4baffdbb07b1edc59b1df2483506a1476 (diff) | |
| download | biteq-5fe9ec29c08dc2b2e8cedb7b2d63ddca08226199.tar.gz biteq-5fe9ec29c08dc2b2e8cedb7b2d63ddca08226199.zip | |
Clean up the proof further
| -rw-r--r-- | src/BitEQ.v | 7 |
1 files changed, 2 insertions, 5 deletions
diff --git a/src/BitEQ.v b/src/BitEQ.v index 4689b26..72f7d18 100644 --- a/src/BitEQ.v +++ b/src/BitEQ.v @@ -11,10 +11,8 @@ Record bv := Zbv { size: N; val: Z; }. Definition bvZ (b: bv) := (val b) mod (2 ^ (Z.of_N (size b))). -Definition bvadd (sz: N) (a b: bv) := - Zbv sz (bvZ a + bvZ b). - -Compute bvZ (bvadd 4%N (Zbv 3%N 5) (Zbv 3%N 5)). +Definition bvadd (sz: N) (a b: bv) := Zbv sz (bvZ a + bvZ b). +Definition bvmult (sz: N) (a b: bv) := Zbv sz (bvZ a * bvZ b). Lemma pow_2_div : forall p q, 0 <= p <= q -> (2 ^ p | 2 ^ q). Proof. @@ -40,7 +38,6 @@ Lemma bounded_add_assoc : = bvZ (bvadd v (Zbv p a) (bvadd q (Zbv r b) (Zbv s c))). Proof. intros. - (* Zplus_mod *) unfold bvadd, bvZ; simpl in *. rewrite Zplus_mod by eauto. rewrite mod_mod_pow_2 by lia. symmetry. rewrite Zplus_mod by eauto. |