English
For a relation r and list l with starting option o, the folded value l.foldl(argAux r) o equals none if and only if l is empty and o is none.
Русский
Для отношения r и списка l с начальным значением o, свёртка l.foldl(argAux r) o равна none тогда и только тогда, когда l пуст и o = none.
LaTeX
$$$ \operatorname{foldl}(\operatorname{argAux}(r), o, l) = \mathrm{none} \iff l = \varnothing \land o = \mathrm{none}$$$
Lean4
@[simp]
theorem foldl_argAux_eq_none : l.foldl (argAux r) o = none ↔ l = [] ∧ o = none :=
List.reverseRecOn l (by simp) fun tl hd =>
by
simp only [foldl_append, foldl_cons, argAux, foldl_nil, append_eq_nil_iff]
cases foldl (argAux r) o tl
· simp
· simp only
split_ifs <;> simp
