destruct_tail — Mathlib

English

destruct(tail s) = destruct s >>= tail.aux.

Русский

destruct(tail(s)) = destruct(s)bind tail.aux.

LaTeX

$$$$\operatorname{destruct}(\operatorname{tail}(s)) = \operatorname{destruct}(s) \bind \operatorname{tail.aux}.$$$$

Lean4

theorem destruct_tail (s : WSeq α) : destruct (tail s) = destruct s >>= tail.aux :=
  by
  simp only [tail, destruct_flatten]; rw [← bind_pure_comp, LawfulMonad.bind_assoc]
  apply congr_arg; ext1 (_ | ⟨a, s⟩) <;> apply (@pure_bind Computation _ _ _ _ _ _).trans _ <;> simp

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