flatten_pure — Mathlib

English

Flattening a pure computation yields the original sequence.

Русский

Плоское представление чистого вычисления приводит к исходной последовательности.

LaTeX

$$$$\mathrm{flatten}(\mathrm{pure}\, s)=s.$$$$

Lean4

@[simp]
theorem flatten_pure (s : WSeq α) : flatten (Computation.pure s) = s :=
  by
  refine Seq.eq_of_bisim (fun s1 s2 => flatten (Computation.pure s2) = s1) ?_ rfl
  intro s' s h
  rw [← h]
  simp only [Seq.BisimO, flatten, Seq.omap, pure_def, Seq.corec_eq, destruct_pure]
  cases Seq.destruct s with
  | none => simp
  | some val =>
    obtain ⟨o, s'⟩ := val
    simp

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