English
Join of a nested join distributes as join of the map-join structure: join (join SS) = join (map join SS).
Русский
Умножение через две операции join распадается на join от отображения и join: join (join SS) = join (map join SS).
LaTeX
$$$\\mathrm{join}(\\mathrm{join}\\; SS) = \\mathrm{join}(\\mathrm{map}\\; \\mathrm{join}\\; SS)$$$
Lean4
@[simp]
theorem join_join (SS : Seq (Seq1 (Seq1 α))) : Seq.join (Seq.join SS) = Seq.join (Seq.map join SS) :=
by
apply
Seq.eq_of_bisim fun s1 s2 =>
∃ s SS, s1 = Seq.append s (Seq.join (Seq.join SS)) ∧ s2 = Seq.append s (Seq.join (Seq.map join SS))
· intro s1 s2 h
exact
match s1, s2, h with
| _, _, ⟨s, SS, rfl, rfl⟩ => by
cases s <;> simp
case nil =>
cases SS <;> simp
case cons S SS =>
obtain ⟨s, S⟩ := S; obtain ⟨x, s⟩ := s
simp only [Seq.join_cons, join_append, destruct_cons]
cases s <;> simp
case nil => exact ⟨_, _, rfl, rfl⟩
case cons x s => refine ⟨Seq.cons x (append s (Seq.join S)), SS, ?_, ?_⟩ <;> simp
case cons _ s => exact ⟨s, SS, rfl, rfl⟩
· refine ⟨nil, SS, ?_, ?_⟩ <;> simp
