feat(data/list): add a few lemmas (#14047)

* add `list.reverse_surjective` and `list.reverse_bijective`;
* add `list.chain_iff_forall₂`,
  `list.chain_append_singleton_iff_forall₂`, and `list.all₂_zip_with`.

src/data/list/basic.lean

@@ -630,11 +630,10 @@ by rw [concat_eq_append, reverse_append, reverse_singleton, singleton_append]
 @[simp] theorem reverse_reverse (l : list α) : reverse (reverse l) = l :=
 by induction l; [refl, simp only [*, reverse_cons, reverse_append]]; refl
 
-@[simp] theorem reverse_involutive : involutive (@reverse α) :=
-λ l, reverse_reverse l
-
-@[simp] theorem reverse_injective : injective (@reverse α) :=
-reverse_involutive.injective
+@[simp] theorem reverse_involutive : involutive (@reverse α) := reverse_reverse
+@[simp] theorem reverse_injective : injective (@reverse α) := reverse_involutive.injective
+theorem reverse_surjective : surjective (@reverse α) := reverse_involutive.surjective
+theorem reverse_bijective : bijective (@reverse α) := reverse_involutive.bijective
 
 @[simp] theorem reverse_inj {l₁ l₂ : list α} : reverse l₁ = reverse l₂ ↔ l₁ = l₂ :=
 reverse_injective.eq_iff

src/data/list/chain.lean

@@ -68,6 +68,16 @@ simp only [*, nil_append, cons_append, chain.nil, chain_cons, and_true, and_asso
   chain R a (l₁ ++ b :: c :: l₂) ↔ chain R a (l₁ ++ [b]) ∧ R b c ∧ chain R c l₂ :=
 by rw [chain_split, chain_cons]
 
+theorem chain_iff_forall₂ :
+  ∀ {a : α} {l : list α}, chain R a l ↔ l = [] ∨ forall₂ R (a :: init l) l
+| a [] := by simp
+| a [b] := by simp [init]
+| a (b :: c :: l) := by simp [@chain_iff_forall₂ b]
+
+theorem chain_append_singleton_iff_forall₂ :
+  chain R a (l ++ [b]) ↔ forall₂ R (a :: l) (l ++ [b]) :=
+by simp [chain_iff_forall₂, init]
+
 theorem chain_map (f : β → α) {b : β} {l : list β} :
   chain R (f b) (map f l) ↔ chain (λ a b : β, R (f a) (f b)) b l :=
 by induction l generalizing b; simp only [map, chain.nil, chain_cons, *]

src/data/list/zip.lean

@@ -62,6 +62,13 @@ zip_with_nil_right _ l
    length (zip l₁ l₂) = min (length l₁) (length l₂) :=
 length_zip_with _
 
+theorem all₂_zip_with {f : α → β → γ} {p : γ → Prop} :
+  ∀ {l₁ : list α} {l₂ : list β} (h : length l₁ = length l₂),
+  all₂ p (zip_with f l₁ l₂) ↔ forall₂ (λ x y, p (f x y)) l₁ l₂
+| [] [] _ := by simp
+| (a :: l₁) (b :: l₂) h :=
+  by { simp only [length_cons, add_left_inj] at h, simp [all₂_zip_with h] }
+
 lemma lt_length_left_of_zip_with {f : α → β → γ} {i : ℕ} {l : list α} {l' : list β}
   (h : i < (zip_with f l l').length) :
   i < l.length :=