add some zip lemmas

stdpp/list.v

@@ -5043,6 +5043,42 @@ Section zip.
   Lemma elem_of_zip_r x1 x2 l k :
     (x1, x2) ∈ zip l k → x2 ∈ k.
   Proof. intros ?%elem_of_zip_with. naive_solver. Qed.
+
+  Lemma lookup_zip i x1 x2 l k :
+  zip l k !! i = Some(x1, x2)  →
+  l !! i = Some x1 ∧ k !! i = Some x2.
+  Proof.
+    induction l as [ | x xs IH] in k, i |-*; destruct k as [ | y ys]; simpl; [ done.. | ].
+    destruct i as [ | i]; simpl; last by apply IH.
+    injection 1 as [= <-].
+    naive_solver.
+  Qed.
+
+  Lemma zip_length l k :
+    length (zip l k) = min (length l) (length k).
+  Proof. by rewrite length_zip_with. Qed.
+
+  Lemma zip_nil_implies_list_nil l k :
+  zip l k = [] ↔ l = [] ∨ k = [].
+  Proof. by induction l; induction k; naive_solver. Qed.
+
+  Lemma lookup_zip_split l k ind e1 e2 :
+  l !! ind = Some e1 →
+  k !! ind = Some e2 →
+  zip l k !! ind = Some(e1, e2).
+  Proof.
+  induction l as [| hd1 tail1 IH1] in k,ind |-*; destruct k as [ | y ys]; simpl; [ done.. | ].
+  intros ??.
+  case ind as [| ind']; naive_solver.
+  Qed.
+
+  Lemma lookup_zip_None l k ind :
+    length l = length k →
+    zip l k !! ind = None ↔ l !! ind = None ∧ k !! ind = None.
+  Proof.
+    induction l as [| hd1 tail1 IH1] in k,ind |-*; destruct k as [ | y ys]; simpl; [ done.. | ].
+    case ind; naive_solver.
+  Qed.
 End zip.
 
 Lemma zip_diag {A} (l : list A) :