ret_bind — Mathlib

English

bind (pure a) f = f a.

Русский

bind (pure a) f = f a.

LaTeX

$$$$ \operatorname{bind}(\mathrm{pure}\ a)\ f = f\ a. $$$$

Lean4

@[simp]
theorem ret_bind (a) (f : α → Computation β) : bind (pure a) f = f a :=
  by
  apply eq_of_bisim fun c₁ c₂ => c₁ = bind (pure a) f ∧ c₂ = f a ∨ c₁ = corec (Bind.f f) (Sum.inr c₂)
  · intro c₁ c₂ h
    match c₁, c₂, h with
    | _, _, Or.inl ⟨rfl, rfl⟩ =>
      simp only [BisimO, bind, Bind.f, corec_eq, rmap, destruct_pure]
      rcases destruct (f a) with b | cb <;> simp [Bind.g]
    | _, c, Or.inr rfl =>
      simp only [BisimO, Bind.f, corec_eq, rmap]
      rcases destruct c with b | cb <;> simp [Bind.g]
  · simp

Похожие утверждения