From a9a831d988311c25e0d35101f456e3fdd03cbe16 Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Thu, 7 Mar 2019 21:43:45 -0500
Subject: Add some eq lemmas to ListUtil

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

(limited to 'src/Util')

diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v
index 685c132b1..5af914ffe 100644
--- a/src/Util/ListUtil.v
+++ b/src/Util/ListUtil.v
@@ -2405,3 +2405,47 @@ Proof using Type.
   intro H; apply remove_duplicates_eq_NoDupA with (R:=eq); eauto; try exact _.
   now apply NoDupA_eq_NoDup.
 Qed.
+
+Lemma eq_repeat_nat_rect {A} x n
+  : @List.repeat A x n
+    = nat_rect _ nil (fun k repeat_k => x :: repeat_k) n.
+Proof using Type. induction n; cbn; f_equal; assumption. Qed.
+
+Lemma eq_firstn_nat_rect {A} n ls
+  : @List.firstn A n ls
+    = nat_rect
+        _
+        (fun _ => nil)
+        (fun n' firstn_n' ls
+         => match ls with
+            | nil => nil
+            | cons x xs => x :: firstn_n' xs
+            end)
+        n ls.
+Proof using Type. revert ls; induction n, ls; cbn; f_equal; auto. Qed.
+
+Lemma eq_skipn_nat_rect {A} n ls
+  : @List.skipn A n ls
+    = nat_rect
+        _
+        (fun ls => ls)
+        (fun n' skipn_n' ls
+         => match ls with
+            | nil => nil
+            | cons x xs => skipn_n' xs
+            end)
+        n ls.
+Proof using Type. revert ls; induction n, ls; cbn; f_equal; auto. Qed.
+
+Lemma eq_combine_list_rect {A B} xs ys
+  : @List.combine A B xs ys
+    = list_rect
+        _
+        (fun _ => nil)
+        (fun x xs combine_xs ys
+         => match ys with
+            | nil => nil
+            | y :: ys => (x, y) :: combine_xs ys
+            end)
+        xs ys.
+Proof using Type. revert ys; induction xs, ys; cbn; f_equal; auto. Qed.
-- 
cgit v1.2.3