English
A second formulation of the coinductive length bound: under suitable motive and step, b.length' ≤ a.length'.
Русский
Вторая формулировка коиндуктивного ограничения длин: при надлежащем мотиве и шаге выполняется b.length' ≤ a.length'.
LaTeX
$$$\\text{at\_least\_as\_long\_as\_coind}(\\cdot) \Rightarrow b.length' \\le a.length'$$$
Lean4
@[simp]
theorem bind_assoc (s : Seq1 α) (f : α → Seq1 β) (g : β → Seq1 γ) :
bind (bind s f) g = bind s fun x : α => bind (f x) g :=
by
obtain ⟨a, s⟩ := s
simp only [bind, map_pair, map_join]
rw [← map_comp]
simp only [show (fun x => join (map g (f x))) = join ∘ (map g ∘ f) from rfl]
rw [map_comp _ join]
generalize Seq.map (map g ∘ f) s = SS
rcases map g (f a) with ⟨⟨a, s⟩, S⟩
induction s using recOn with
| nil => ?_
| cons x s_1 => ?_ <;>
induction S using recOn with
| nil => simp
| cons x_1 s_2 => ?_
· obtain ⟨x, t⟩ := x_1
cases t <;> simp
· obtain ⟨y, t⟩ := x_1; simp
