From 9b6a08343fd418296b069ead6fc4e879f8af0e7c Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 18 Jul 2016 16:35:51 -0700 Subject: Add a lemma about base_from_limb_widths and app --- src/ModularArithmetic/Pow2BaseProofs.v | 12 ++++++++++++ 1 file changed, 12 insertions(+) (limited to 'src/ModularArithmetic') 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. -- cgit v1.2.3