English
Destruct on flatten(c) corresponds to binding the destruct of c with the flatten operation, i.e., destruct(flatten c) = c >>= destruct.
Русский
Destruct над flatten(c) соответствует связыванию destruct c с flatten, то есть destruct(flatten c) = c >>= destruct.
LaTeX
$$$$\mathrm{destruct}(\mathrm{flatten}(c)) = c \gg= \mathrm{destruct}.$$$$
Lean4
@[simp]
theorem destruct_flatten (c : Computation (WSeq α)) : destruct (flatten c) = c >>= destruct :=
by
refine
Computation.eq_of_bisim (fun c1 c2 => c1 = c2 ∨ ∃ c, c1 = destruct (flatten c) ∧ c2 = Computation.bind c destruct)
?_ (Or.inr ⟨c, rfl, rfl⟩)
intro c1 c2 h
exact
match c1, c2, h with
| c, _, Or.inl rfl => by cases c.destruct <;> simp
| _, _, Or.inr ⟨c, rfl, rfl⟩ => by
induction c using Computation.recOn with
| pure a => simp; cases (destruct a).destruct <;> simp
| think c' => simpa using Or.inr ⟨c', rfl, rfl⟩
