English
For nonempty p, the firstReturn of p.nest equals the length of p.toList plus 1.
Русский
Для непустого p первый возврат p.nest равен длине p.toList плюс 1.
LaTeX
$$$$ p \neq 0 \implies p.nest.firstReturn = p.toList.length + 1. $$$$
Lean4
@[simp]
theorem firstReturn_nest : p.nest.firstReturn = p.toList.length + 1 :=
by
have u : p.nest.toList = U :: p.toList ++ [D] := rfl
rw [firstReturn, findIdx_eq]
· simp_rw [u, decide_eq_true_eq, getElem_range]
constructor
· rw [take_of_length_le (by simp), ← u, p.nest.count_U_eq_count_D]
· intro j hj
simp_rw [cons_append, take_succ_cons, count_cons, beq_self_eq_true, ite_true, beq_iff_eq, reduceCtorEq, ite_false,
take_append, show j - p.toList.length = 0 by cutsat, take_zero, append_nil]
have := p.count_D_le_count_U j
simp only [add_zero, decide_eq_false_iff_not, ne_eq]
cutsat
· simp_rw [length_range, u, length_append, length_cons]
exact Nat.lt_add_one _
