Equations
- computation.parallel.aux2 = list.foldr (λ (c : computation α) (o : α ⊕ list (computation α)), computation.parallel.aux2._match_1 c o) (sum.inr list.nil)
- computation.parallel.aux2._match_1 c (sum.inr ls) = computation.rmap (λ (c' : computation α), c' :: ls) c.destruct
- computation.parallel.aux2._match_1 c (sum.inl a) = sum.inl a
def
computation.parallel.aux1
{α : Type u} :
list (computation α) × wseq (computation α) → α ⊕ list (computation α) × wseq (computation α)
Equations
- computation.parallel.aux1 (l, S) = computation.rmap (λ (l' : list (computation α)), computation.parallel.aux1._match_1 l' (seq.destruct S)) (computation.parallel.aux2 l)
- computation.parallel.aux1._match_1 l' (option.some (option.some c, S')) = (c :: l', S')
- computation.parallel.aux1._match_1 l' (option.some (option.none (computation α), S')) = (l', S')
- computation.parallel.aux1._match_1 l' option.none = (l', wseq.nil (computation α))
Parallel computation of an infinite stream of computations, taking the first result
Equations
theorem
computation.terminates_parallel.aux
{α : Type u}
{l : list (computation α)}
{S : wseq (computation α)}
{c : computation α} :
c ∈ l → c.terminates → (computation.corec computation.parallel.aux1 (l, S)).terminates
theorem
computation.terminates_parallel
{α : Type u}
{S : wseq (computation α)}
{c : computation α}
(h : c ∈ S)
[T : c.terminates] :
theorem
computation.exists_of_mem_parallel
{α : Type u}
{S : wseq (computation α)}
{a : α} :
a ∈ computation.parallel S → (∃ (c : computation α) (H : c ∈ S), a ∈ c)
theorem
computation.map_parallel
{α : Type u}
{β : Type v}
(f : α → β)
(S : wseq (computation α)) :
def
computation.parallel_rec
{α : Type u}
{S : wseq (computation α)}
(C : α → Sort v)
(H : Π (s : computation α), s ∈ S → Π (a : α), a ∈ s → C a)
{a : α} :
a ∈ computation.parallel S → C a
Equations
- computation.parallel_rec C H h = let T : wseq (computation (α × computation α)) := wseq.map (λ (c : computation α), computation.map (λ (a : α), (a, c)) c) S in (λ (_x : α × computation α) (e : (computation.parallel T).get = _x), prod.rec (λ (a' : α) (c : computation α) (e : (computation.parallel T).get = (a', c)), and.dcases_on _ (λ (ac : a ∈ c) (cs : c ∈ S), H c cs a ac)) _x e) (computation.parallel T).get _
theorem
computation.parallel_promises
{α : Type u}
{S : wseq (computation α)}
{a : α} :
(∀ (s : computation α), s ∈ S → s ~> a) → computation.parallel S ~> a
theorem
computation.mem_parallel
{α : Type u}
{S : wseq (computation α)}
{a : α}
(H : ∀ (s : computation α), s ∈ S → s ~> a)
{c : computation α} :
c ∈ S → a ∈ c → a ∈ computation.parallel S
theorem
computation.parallel_congr_lem
{α : Type u}
{S T : wseq (computation α)}
{a : α} :
wseq.lift_rel computation.equiv S T → ((∀ (s : computation α), s ∈ S → s ~> a) ↔ ∀ (t : computation α), t ∈ T → t ~> a)
theorem
computation.parallel_congr_left
{α : Type u}
{S T : wseq (computation α)}
{a : α} :
(∀ (s : computation α), s ∈ S → s ~> a) → wseq.lift_rel computation.equiv S T → computation.parallel S ~ computation.parallel T
theorem
computation.parallel_congr_right
{α : Type u}
{S T : wseq (computation α)}
{a : α} :
(∀ (t : computation α), t ∈ T → t ~> a) → wseq.lift_rel computation.equiv S T → computation.parallel S ~ computation.parallel T