English
bind (bind s f) g = bind s (\lambda x, bind (f x) g).
Русский
bind (bind s f) g = bind s (λ x, bind (f x) g).
LaTeX
$$$$ \operatorname{bind}(\operatorname{bind} s f) g = \operatorname{bind} s (\lambda x, \operatorname{bind} (f x) g). $$$$
Lean4
@[simp]
theorem bind_assoc (s : Computation α) (f : α → Computation β) (g : β → Computation γ) :
bind (bind s f) g = bind s fun x : α => bind (f x) g :=
by
apply eq_of_bisim fun c₁ c₂ => c₁ = c₂ ∨ ∃ s, c₁ = bind (bind s f) g ∧ c₂ = bind s fun x : α => bind (f x) g
· intro c₁ c₂ h
match c₁, c₂, h with
| _, c₂, Or.inl (Eq.refl _) => rcases destruct c₂ with b | cb <;> simp
| _, _, Or.inr ⟨s, rfl, rfl⟩ =>
induction s using recOn with
| pure s =>
simp only [BisimO, ret_bind]; generalize f s = fs
induction fs using recOn with
| pure t => rw [ret_bind]; rcases destruct (g t) with b | cb <;> simp
| think => simp
| think s => simpa [BisimO] using Or.inr ⟨s, rfl, rfl⟩
· exact Or.inr ⟨s, rfl, rfl⟩
