English
Destruct on the append of two sequences equals the bind of destruct on the first with the auxiliary function on the second.
Русский
Разложение для конкатенации двух последовательностей равно связыванию первого распознавания с помощью вспомогательной функции уничтожения для второго.
LaTeX
$$$$ \\operatorname{destruct}(\\operatorname{append} s t) = (\\operatorname{destruct} s) \\bind (\\operatorname{destruct\\_append}.aux t) $$$$
Lean4
theorem destruct_append (s t : WSeq α) : destruct (append s t) = (destruct s).bind (destruct_append.aux t) :=
by
apply
Computation.eq_of_bisim
(fun c1 c2 => ∃ s t, c1 = destruct (append s t) ∧ c2 = (destruct s).bind (destruct_append.aux t)) _
⟨s, t, rfl, rfl⟩
intro c1 c2 h; rcases h with ⟨s, t, h⟩; rw [h.left, h.right]
induction s using WSeq.recOn <;> simp
case nil =>
induction t using WSeq.recOn <;> simp
case think t => refine ⟨nil, t, ?_, ?_⟩ <;> simp
case think s => exact ⟨s, t, rfl, rfl⟩
