diff options
Diffstat (limited to 'src/ModularArithmetic/Pow2BaseProofs.v')
| -rw-r--r-- | src/ModularArithmetic/Pow2BaseProofs.v | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/src/ModularArithmetic/Pow2BaseProofs.v b/src/ModularArithmetic/Pow2BaseProofs.v index 6d6e3f530..6a8d4a8ff 100644 --- a/src/ModularArithmetic/Pow2BaseProofs.v +++ b/src/ModularArithmetic/Pow2BaseProofs.v @@ -150,6 +150,18 @@ Section Pow2BaseProofs. reflexivity. Qed. + Lemma base_from_limb_widths_app : forall l0 l + (l0_nonneg : forall x, In x l0 -> 0 <= x) + (l_nonneg : forall x, In x l -> 0 <= x), + base_from_limb_widths (l0 ++ l) + = base_from_limb_widths l0 ++ map (Z.mul (two_p (sum_firstn l0 (length l0)))) (base_from_limb_widths l). + Proof. + induction l0 as [|?? IHl0]. + { simpl; intros; rewrite <- map_id at 1; apply map_ext; intros; omega. } + { simpl; intros; rewrite !IHl0, !map_app, map_map, sum_firstn_succ_cons, two_p_is_exp by auto with znonzero. + do 2 f_equal; apply map_ext; intros; lia. } + Qed. + End Pow2BaseProofs. Section BitwiseDecodeEncode. |