From bf30dc32c108b92f99e9e16c7609f01c2df589c0 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 9 Aug 2018 17:33:59 -0400 Subject: Add ListUtil.{combine_repeat,combine_rev_rev_samelength} --- src/Util/ListUtil.v | 10 ++++++++++ 1 file changed, 10 insertions(+) (limited to 'src/Util/ListUtil.v') diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v index 22b90cdc7..797796322 100644 --- a/src/Util/ListUtil.v +++ b/src/Util/ListUtil.v @@ -2112,3 +2112,13 @@ Proof. revert ls2 n; induction ls1 as [|l1 ls1 IHls1], ls2, n; cbn [combine nth_error]; try reflexivity; auto. edestruct nth_error; reflexivity. Qed. + +Lemma combine_repeat {A B} (a : A) (b : B) n : combine (repeat a n) (repeat b n) = repeat (a, b) n. +Proof. induction n; cbn; congruence. Qed. + +Lemma combine_rev_rev_samelength {A B} ls1 ls2 : length ls1 = length ls2 -> @combine A B (rev ls1) (rev ls2) = rev (combine ls1 ls2). +Proof. + revert ls2; induction ls1 as [|? ? IHls1], ls2; cbn in *; try congruence; intros. + rewrite combine_app_samelength, IHls1 by (rewrite ?rev_length; congruence); cbn [combine]. + reflexivity. +Qed. -- cgit v1.2.3