From e215871febb7d1294aa5aa13b0c70b2207e745e2 Mon Sep 17 00:00:00 2001 From: jadep Date: Thu, 30 Jun 2016 15:16:50 -0400 Subject: added and proved shift/or decode operation 'decode_bitwise' --- src/Testbit.v | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) (limited to 'src/Testbit.v') diff --git a/src/Testbit.v b/src/Testbit.v index 2bfcc3df6..545c3cbce 100644 --- a/src/Testbit.v +++ b/src/Testbit.v @@ -179,9 +179,10 @@ Proof. - rewrite nth_default_cons_S. erewrite IHus; eauto using no_overflow_tail. remember (i * limb_width)%nat as k. - rewrite Z_shiftr_add_land by omega. - replace (limb_width + k - limb_width)%nat with k by omega. - reflexivity. + rewrite Z_shiftr_add_shiftl_high; rewrite ?Nat2Z.inj_add; + repeat f_equal; try omega. + rewrite Z.land_ones by apply Nat2Z.is_nonneg. + apply Z.mod_pos_bound. zero_bounds. Qed. Lemma unfold_bits_testbit : forall limb_width us n, (0 < limb_width)%nat -> -- cgit v1.2.3