From 0bdfa57b5c24a34f6fafe8a97c1ce6453ce2cd83 Mon Sep 17 00:00:00 2001
From: Jade Philipoom <jadep@google.com>
Date: Wed, 11 Apr 2018 17:48:36 +0200
Subject: add a list lemma

---
 src/Util/ListUtil.v | 9 +++++++++
 1 file changed, 9 insertions(+)

(limited to 'src/Util/ListUtil.v')

diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v
index 2aab77aca..92c648725 100644
--- a/src/Util/ListUtil.v
+++ b/src/Util/ListUtil.v
@@ -966,6 +966,15 @@ Proof.
 Qed.
 Hint Rewrite @combine_nil_r : push_combine.
 
+Lemma combine_snoc {A B} xs : forall ys x y,
+    length xs = length ys ->
+    @combine A B (xs ++ (x :: nil)) (ys ++ (y :: nil)) = combine xs ys ++ ((x, y) :: nil).
+Proof.
+  induction xs; intros; destruct ys; distr_length; cbn;
+    try rewrite IHxs by omega; reflexivity.
+Qed.
+Hint Rewrite @combine_snoc using (solve [distr_length]) : push_combine.
+
 Lemma skipn_combine : forall {A B} n (xs:list A) (ys:list B),
   skipn n (combine xs ys) = combine (skipn n xs) (skipn n ys).
 Proof.
-- 
cgit v1.2.3