From cd07805915328fd5ee8d41b6cdd4d0340aa156aa Mon Sep 17 00:00:00 2001 From: jadep Date: Thu, 28 Apr 2016 13:13:08 -0400 Subject: Cleanup: mostly moving lemmas to Util files, some moving lemmas to more general contexts. --- src/BaseSystemProofs.v | 13 +++++++++++++ 1 file changed, 13 insertions(+) (limited to 'src/BaseSystemProofs.v') diff --git a/src/BaseSystemProofs.v b/src/BaseSystemProofs.v index 84374fe8f..ab56cb711 100644 --- a/src/BaseSystemProofs.v +++ b/src/BaseSystemProofs.v @@ -17,6 +17,18 @@ Section BaseSystemProofs. unfold decode'; intros; f_equal; apply combine_truncate_l. Qed. + Lemma decode'_splice : forall xs ys bs, + decode' bs (xs ++ ys) = + decode' (firstn (length xs) bs) xs + decode' (skipn (length xs) bs) ys. + Proof. + unfold decode'. + induction xs; destruct ys, bs; boring. + + rewrite combine_truncate_r. + do 2 rewrite Z.add_0_r; auto. + + unfold accumulate. + apply Z.add_assoc. + Qed. + Lemma add_rep : forall bs us vs, decode' bs (add us vs) = decode' bs us + decode' bs vs. Proof. unfold decode', accumulate; induction bs; destruct us, vs; boring; ring. @@ -487,4 +499,5 @@ Section BaseSystemProofs. rewrite rev_length; omega. Qed. + End BaseSystemProofs. -- cgit v1.2.3