English
Concat of two option-lists followed by reduction equals concatenation of their reduced parts.
Русский
Слияние двух списков опций с последующим снижением эквивалентно конкатенации их упрощённых частей.
LaTeX
$$$\mathrm{reduceOption}(l \append \mathrm{some}(a) :: l_2) = \mathrm{reduceOption}(l) \append a$$$
Lean4
theorem reduceOption_eq_concat_iff (l : List (Option α)) (l' : List α) (a : α) :
l.reduceOption = l'.concat a ↔ ∃ l₁ l₂, l = l₁ ++ some a :: l₂ ∧ l₁.reduceOption = l' ∧ l₂.reduceOption = [] :=
by
rw [concat_eq_append]
constructor
· intro h
rw [reduceOption_eq_append_iff] at h
obtain ⟨l₁, _, h, hl₁, hl₂⟩ := h
rw [reduceOption_eq_singleton_iff] at hl₂
obtain ⟨m, n, hl₂⟩ := hl₂
use l₁ ++ replicate m none, replicate n none
simp_rw [h, reduceOption_append, reduceOption_replicate_none, append_assoc, append_nil, hl₁, hl₂, and_self]
· intro ⟨_, _, h, hl₁, hl₂⟩
rw [h, reduceOption_append, reduceOption_cons_of_some, hl₁, hl₂]
