Parallel computation

Parallel computation of a computable sequence of computations by a diagonal enumeration. The important theorems of this operation are proven as terminates_parallel and exists_of_mem_parallel. (This operation is nondeterministic in the sense that it does not honor sequence equivalence (irrelevance of computation time).)

def Computation.parallel {α : Type u} (S : Stream'.WSeq (Computation α)) : Computation α

Parallel computation of an infinite stream of computations, taking the first result

theorem Computation.terminates_parallel.aux {α : Type u} {l : List (Computation α)} {S : Stream'.WSeq (Computation α)} {c : Computation α} : c ∈ l → c.Terminates → (corec Computation.parallel.aux1✝ (l, S)).Terminates

theorem Computation.terminates_parallel {α : Type u} {S : Stream'.WSeq (Computation α)} {c : Computation α} (h : c ∈ S) [T : c.Terminates] : (parallel S).Terminates

theorem Computation.exists_of_mem_parallel {α : Type u} {S : Stream'.WSeq (Computation α)} {a : α} (h : a ∈ parallel S) : ∃ (c : Computation α), c ∈ S ∧ a ∈ c

theorem Computation.map_parallel {α : Type u} {β : Type v} (f : α → β) (S : Stream'.WSeq (Computation α)) : map f (parallel S) = parallel (Stream'.WSeq.map (map f) S)

theorem Computation.parallel_empty {α : Type u} (S : Stream'.WSeq (Computation α)) (h : S.head.Promises none) : parallel S = empty α

def Computation.parallelRec {α : Type u} {S : Stream'.WSeq (Computation α)} (C : α → Sort v) (H : (s : Computation α) → s ∈ S → (a : α) → a ∈ s → C a) {a : α} (h : a ∈ parallel S) : C a

Induction principle for parallel computations. The reason this isn't trivial from exists_of_mem_parallel is because it eliminates to Sort.

theorem Computation.parallel_promises {α : Type u} {S : Stream'.WSeq (Computation α)} {a : α} (H : ∀ (s : Computation α), s ∈ S → s.Promises a) : (parallel S).Promises a

theorem Computation.mem_parallel {α : Type u} {S : Stream'.WSeq (Computation α)} {a : α} (H : ∀ (s : Computation α), s ∈ S → s.Promises a) {c : Computation α} (cs : c ∈ S) (ac : a ∈ c) : a ∈ parallel S

theorem Computation.parallel_congr_lem {α : Type u} {S T : Stream'.WSeq (Computation α)} {a : α} (H : Stream'.WSeq.LiftRel Equiv S T) : (∀ (s : Computation α), s ∈ S → s.Promises a) ↔ ∀ (t : Computation α), t ∈ T → t.Promises a

theorem Computation.parallel_congr_left {α : Type u} {S T : Stream'.WSeq (Computation α)} {a : α} (h1 : ∀ (s : Computation α), s ∈ S → s.Promises a) (H : Stream'.WSeq.LiftRel Equiv S T) : (parallel S).Equiv (parallel T)

theorem Computation.parallel_congr_right {α : Type u} {S T : Stream'.WSeq (Computation α)} {a : α} (h2 : ∀ (t : Computation α), t ∈ T → t.Promises a) (H : Stream'.WSeq.LiftRel Equiv S T) : (parallel S).Equiv (parallel T)