English
Joining the concatenation of two streams equals the concatenation of their joins: join (append S T) ~ʷ append (join S) (join T).
Русский
Слияние конкатенации двух потоков равно конкатенации их слияний: join (append S T) ~ʷ append (join S) (join T).
LaTeX
$$$ \forall S,T : \mathrm{WSeq}(\mathrm{WSeq}\,\alpha),\; \mathrm{join}(\mathrm{append}\ S\ T) ~ʷ \mathrm{append}(\mathrm{join}\ S)(\mathrm{join}\ T)$$$
Lean4
@[simp]
theorem join_append (S T : WSeq (WSeq α)) : join (append S T) ~ʷ append (join S) (join T) :=
by
refine
⟨fun s1 s2 => ∃ s S T, s1 = append s (join (append S T)) ∧ s2 = append s (append (join S) (join T)),
⟨nil, S, T, by simp, by simp⟩, ?_⟩
intro s1 s2 h
apply
liftRel_rec
(fun c1 c2 =>
∃ (s : WSeq α) (S T : _),
c1 = destruct (append s (join (append S T))) ∧ c2 = destruct (append s (append (join S) (join T))))
_ _ _
(let ⟨s, S, T, h1, h2⟩ := h
⟨s, S, T, congr_arg destruct h1, congr_arg destruct h2⟩)
rintro c1 c2 ⟨s, S, T, rfl, rfl⟩
induction s using WSeq.recOn with
| nil =>
induction S using WSeq.recOn with
| nil =>
simp only [nil_append, join_nil]
induction T using WSeq.recOn with
| nil => simp
| cons s T =>
simp only [join_cons, destruct_think, Computation.destruct_think, liftRelAux_inr_inr]
refine ⟨s, nil, T, ?_, ?_⟩ <;> simp
| think T =>
simp only [join_think, destruct_think, Computation.destruct_think, liftRelAux_inr_inr]
refine ⟨nil, nil, T, ?_, ?_⟩ <;> simp
| cons s S => simpa using ⟨s, S, T, rfl, rfl⟩
| think S => refine ⟨nil, S, T, ?_, ?_⟩ <;> simp
| cons a s => simpa using ⟨s, S, T, rfl, rfl⟩
| think s => simpa using ⟨s, S, T, rfl, rfl⟩
