English
A walk p1 is a subwalk of p2 iff the list of vertices of p1 is an infix of the list of vertices of p2.
Русский
Обход p1 является подпрохождением к p2 тогда и только тогда, когда список вершин p1 является инфиксом списка вершин p2.
LaTeX
$$$\forall v,w,v',w': V\;{p_1:G.Walk\,v\,w}\;{p_2:G.Walk\,v'\,w'}:\ IsSubwalk(p_1,p_2) \iff p_1.support \;IsInfix\; p_2.support.$$$
Lean4
theorem isSubwalk_iff_support_isInfix {v w v' w' : V} {p₁ : G.Walk v w} {p₂ : G.Walk v' w'} :
p₁.IsSubwalk p₂ ↔ p₁.support <:+: p₂.support :=
by
refine ⟨fun ⟨ru, rv, h⟩ ↦ ?_, fun ⟨s, t, h⟩ ↦ ?_⟩
· grind [support_append, support_append_eq_support_dropLast_append]
· have : (s.length + p₁.length) ≤ p₂.length := by grind [_=_ length_support]
have h₁ : p₂.getVert s.length = v := by
simp [p₂.getVert_eq_support_getElem (by cutsat : s.length ≤ p₂.length), ← h, List.getElem_zero]
have h₂ : p₂.getVert (s.length + p₁.length) = w := by
simp [p₂.getVert_eq_support_getElem (by omega), ← h, ← p₁.getVert_eq_support_getElem (Nat.le_refl _)]
refine ⟨p₂.take s.length |>.copy rfl h₁, p₂.drop (s.length + p₁.length) |>.copy h₂ rfl, ?_⟩
apply ext_support
simp only [← h, support_append, support_copy, take_support_eq_support_take_succ, List.take_append,
drop_support_eq_support_drop_min, List.tail_drop]
rw [Nat.min_eq_left (by grind [length_support]), List.drop_append, List.drop_append,
List.drop_eq_nil_of_le (by cutsat), List.drop_eq_nil_of_le (by grind [length_support]), p₁.support_eq_cons]
simp +arith
