English
For Dyck words p and q, the firstReturn of p+q is p.firstReturn if p ≠ 0, otherwise it is q.firstReturn.
Русский
Для Dyck-слов p и q firstReturn(p+q) равно p.firstReturn, если p ≠ 0, иначе — q.firstReturn.
LaTeX
$$$$ (p+q).firstReturn = \text{if } p = 0 \text{ then } q.firstReturn \text{ else } p.firstReturn. $$$$
Lean4
@[simp]
theorem firstReturn_add : (p + q).firstReturn = if p = 0 then q.firstReturn else p.firstReturn :=
by
split_ifs with h; · simp [h]
have u : (p + q).toList = p.toList ++ q.toList := rfl
rw [firstReturn, findIdx_eq]
· simp_rw [u, decide_eq_true_eq, getElem_range]
have v := firstReturn_lt_length h
constructor
·
rw [take_append, show p.firstReturn + 1 - p.toList.length = 0 by cutsat, take_zero, append_nil,
count_take_firstReturn_add_one h]
· intro j hj
rw [take_append, show j + 1 - p.toList.length = 0 by cutsat, take_zero, append_nil]
simpa using (count_D_lt_count_U_of_lt_firstReturn hj).ne'
· rw [length_range, u, length_append]
exact Nat.lt_add_right _ (firstReturn_lt_length h)
