Move list lemmas to own file

1 files changed, 27 insertions, 0 deletions

diff --git a/src/common/ListExtra.v b/src/common/ListExtra.v
new file mode 100644
index 0000000..6b14a50
--- /dev/null
+++ b/src/common/ListExtra.v
@@ -0,0 +1,27 @@
+Require Export Coq.Lists.List.
+
+Require Import Coq.micromega.Lia.
+Require Import vericert.common.Vericertlib.
+
+From Hammer Require Import Tactics.
+
+Lemma nth_error_length : forall {A} (l : list A) n x,
+    nth_error l n = Some x -> (n < length l)%nat.
+Proof.
+  induction l; intros; simpl in *.
+  - destruct n; crush.
+  - destruct n; crush.
+    edestruct IHl; eauto with arith.
+Qed.
+
+Lemma length_nth_error : forall {A} (l : list A) n,
+    (n < length l)%nat -> exists x, nth_error l n = Some x.
+Proof.
+  induction l; intros; simpl in *.
+  - lia.
+  - destruct n; crush; eauto with arith.
+Qed.
+
+Lemma combine_split : forall {A B} (l : list (A * B)),
+    List.combine (fst (List.split l)) (snd (List.split l)) = l.
+Proof. hfcrush use: split_combine unfold: fst, snd inv: prod. Qed.