bind_pure — Mathlib

English

bind s (pure ∘ f) = map f s.

Русский

bind s (pure ∘ f) = map f s.

LaTeX

$$$$ \operatorname{bind} s (\mathrm{pure}\circ f) = \operatorname{map} f s. $$$$

Lean4

@[simp]
theorem bind_pure (f : α → β) (s) : bind s (pure ∘ f) = map f s :=
  by
  apply eq_of_bisim fun c₁ c₂ => c₁ = c₂ ∨ ∃ s, c₁ = bind s (pure ∘ f) ∧ c₂ = map f s
  · 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
      | think s => simpa using Or.inr ⟨s, rfl, rfl⟩
  · exact Or.inr ⟨s, rfl, rfl⟩

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