diff options
| author |  Jason Gross <jagro@google.com> | 2018-08-09 17:33:59 -0400 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2018-08-09 17:33:59 -0400 |
| commit | bf30dc32c108b92f99e9e16c7609f01c2df589c0 (patch) | |
| tree | 86441e7a17685032cbf9defdc9aef62c7e237626 /src/Util/ListUtil.v | |
| parent | e726e52d2fd7cd3a97926613240b4334be717a32 (diff) | |
Add ListUtil.{combine_repeat,combine_rev_rev_samelength}
Diffstat (limited to 'src/Util/ListUtil.v')
| -rw-r--r-- | src/Util/ListUtil.v | 10 |
1 files changed, 10 insertions, 0 deletions
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. |