feat(data/list/forall2): defines sublist_forall2 relation (#7165)

Defines the `sublist_forall₂` relation, indicating that one list is related by `forall₂` to a sublist of another.
Provides two lemmas, `head_mem_self` and `mem_of_mem_tail`, which will be useful when proving Higman's Lemma about the `sublist_forall₂` relation.



Co-authored-by: Aaron Anderson <65780815+awainverse@users.noreply.github.com>

Author: awainverse

src/data/list/basic.lean

@@ -763,6 +763,12 @@ theorem head_mem_head' [inhabited α] : ∀ {l : list α} (h : l ≠ []), head l
 theorem cons_head_tail [inhabited α] {l : list α} (h : l ≠ []) : (head l)::(tail l) = l :=
 cons_head'_tail (head_mem_head' h)
 
+lemma head_mem_self [inhabited α] {l : list α} (h : l ≠ nil) : l.head ∈ l :=
+begin
+  have h' := mem_cons_self l.head l.tail,
+  rwa cons_head_tail h at h',
+end
+
 @[simp] theorem head'_map (f : α → β) (l) : head' (map f l) = (head' l).map f := by cases l; refl
 
 /-! ### Induction from the right -/
@@ -3529,7 +3535,9 @@ theorem drop_suffix (n) (l : list α) : drop n l <:+ l := ⟨_, take_append_drop
 
 theorem tail_suffix (l : list α) : tail l <:+ l := by rw ← drop_one; apply drop_suffix
 
-theorem tail_subset (l : list α) : tail l ⊆ l := (sublist_of_suffix (tail_suffix l)).subset
+lemma tail_sublist (l : list α) : l.tail <+ l := sublist_of_suffix (tail_suffix l)
+
+theorem tail_subset (l : list α) : tail l ⊆ l := (tail_sublist l).subset
 
 theorem prefix_iff_eq_append {l₁ l₂ : list α} : l₁ <+: l₂ ↔ l₁ ++ drop (length l₁) l₂ = l₂ :=
 ⟨by rintros ⟨r, rfl⟩; rw drop_left, λ e, ⟨_, e⟩⟩

src/data/list/forall2.lean

@@ -219,4 +219,64 @@ lemma rel_prod [monoid α] [monoid β]
   (h : r 1 1) (hf : (r ⇒ r ⇒ r) (*) (*)) : (forall₂ r ⇒ r) prod prod :=
 rel_foldl hf h
 
+/-- Given a relation `r`, `sublist_forall₂ r l₁ l₂` indicates that there is a sublist of `l₂` such
+  that `forall₂ r l₁ l₂`. -/
+inductive sublist_forall₂ (r : α → β → Prop) : list α → list β → Prop
+| nil {l} : sublist_forall₂ [] l
+| cons {a₁ a₂ l₁ l₂} : r a₁ a₂ → sublist_forall₂ l₁ l₂ →
+  sublist_forall₂ (a₁ :: l₁) (a₂ :: l₂)
+| cons_right {a l₁ l₂} : sublist_forall₂ l₁ l₂ → sublist_forall₂ l₁ (a :: l₂)
+
+lemma sublist_forall₂_iff {l₁ : list α} {l₂ : list β} :
+  sublist_forall₂ r l₁ l₂ ↔ ∃ l, forall₂ r l₁ l ∧ l <+ l₂ :=
+begin
+  split; intro h,
+  { induction h with _ a b l1 l2 rab rll ih b l1 l2 hl ih,
+    { exact ⟨nil, forall₂.nil, nil_sublist _⟩ },
+    { obtain ⟨l, hl1, hl2⟩ := ih,
+      refine ⟨b :: l, forall₂.cons rab hl1, cons_sublist_cons b hl2⟩ },
+    { obtain ⟨l, hl1, hl2⟩ := ih,
+      exact ⟨l, hl1, hl2.trans (sublist.cons _ _ _ (sublist.refl _))⟩ } },
+  { obtain ⟨l, hl1, hl2⟩ := h,
+    revert l₁,
+    induction hl2 with _ _ _ _ ih _ _ _ _ ih; intros l₁ hl1,
+    { rw [forall₂_nil_right_iff.1 hl1],
+      exact sublist_forall₂.nil },
+    { exact sublist_forall₂.cons_right (ih hl1) },
+    { cases hl1 with _ _ _ _ hr hl _,
+      exact sublist_forall₂.cons hr (ih hl) } }
+end
+
+variable {ra : α → α → Prop}
+
+instance sublist_forall₂.is_refl [is_refl α ra] :
+  is_refl (list α) (sublist_forall₂ ra) :=
+⟨λ l, sublist_forall₂_iff.2 ⟨l, forall₂_refl l, sublist.refl l⟩⟩
+
+instance sublist_forall₂.is_trans [is_trans α ra] :
+  is_trans (list α) (sublist_forall₂ ra) :=
+⟨λ a b c, begin
+  revert a b,
+  induction c with _ _ ih,
+  { rintros _ _ h1 (_ | _ | _),
+    exact h1 },
+  { rintros a b h1 h2,
+    cases h2 with _ _ _ _ _ hbc tbc _ _ y1 btc,
+    { cases h1,
+      exact sublist_forall₂.nil },
+    { cases h1 with _ _ _ _ _ hab tab _ _ _ atb,
+      { exact sublist_forall₂.nil },
+      { exact sublist_forall₂.cons (trans hab hbc) (ih _ _ tab tbc) },
+      { exact sublist_forall₂.cons_right (ih _ _ atb tbc) } },
+    { exact sublist_forall₂.cons_right (ih _ _ h1 btc), } }
+end⟩
+
+lemma sublist.sublist_forall₂ {l₁ l₂ : list α} (h : l₁ <+ l₂) (r : α → α → Prop) [is_refl α r] :
+  sublist_forall₂ r l₁ l₂ :=
+sublist_forall₂_iff.2 ⟨l₁, forall₂_refl l₁, h⟩
+
+lemma tail_sublist_forall₂_self [is_refl α ra] (l : list α) :
+  sublist_forall₂ ra l.tail l :=
+l.tail_sublist.sublist_forall₂ ra
+
 end list