map_parallel — Mathlib

English

Mapping f over a parallel composition commutes with forming a parallel composition of mapped elements: map f (parallel S) = parallel (S.map (map f)).

Русский

Отображение f над параллельной композицией коммутирует с построением параллельной композиции отображённых элементов.

LaTeX

$$$ \mathrm{map\ }f\ (\mathrm{parallel}\ S) = \mathrm{parallel}\ (S.map(\mathrm{map}\ f)).$$$

Lean4

theorem map_parallel (f : α → β) (S) : map f (parallel S) = parallel (S.map (map f)) :=
  by
  refine
    eq_of_bisim
      (fun c1 c2 =>
        ∃ l S, c1 = map f (corec parallel.aux1 (l, S)) ∧ c2 = corec parallel.aux1 (l.map (map f), S.map (map f)))
      ?_ ⟨[], S, rfl, rfl⟩
  intro c1 c2 h
  exact
    match c1, c2, h with
    | _, _, ⟨l, S, rfl, rfl⟩ =>
      by
      have : parallel.aux2 (l.map (map f)) = lmap f (rmap (List.map (map f)) (parallel.aux2 l)) :=
        by
        simp only [parallel.aux2, rmap, lmap]
        induction l with
        | nil => simp
        | cons c l IH =>
          simp only [List.map_cons, List.foldr_cons, destruct_map, lmap, rmap]
          rw [IH]
          cases List.foldr _ _ _
          · simp
          · cases destruct c <;> simp
      simp only [BisimO, destruct_map, lmap, rmap, corec_eq, parallel.aux1.eq_1]
      rw [this]
      rcases parallel.aux2 l with a | l'
      · simp
      simp only [lmap, rmap]
      induction S using WSeq.recOn <;> simpa using ⟨_, _, rfl, rfl⟩

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