English
If a computation c in a parallel stream S terminates, then the parallel composition parallel S terminates.
Русский
Если вычисление c из параллельной последовательности S прекращает работу, тогда параллельная композиция parallel S прекращает работу.
LaTeX
$$$ \forall S: \mathrm{WSeq}(\mathrm{Computation}(\alpha)), \forall c,\ c \in S \Rightarrow [c\text{ terminates}]\Rightarrow (\mathrm{parallel}\ S)\ \text{terminates}.$$$
Lean4
theorem terminates_parallel {S : WSeq (Computation α)} {c} (h : c ∈ S) [T : Terminates c] : Terminates (parallel S) :=
by
suffices
∀ (n) (l : List (Computation α)) (S c),
c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
from
let ⟨n, h⟩ := h
this n [] S c (Or.inr h) T
intro n; induction n <;> intro l S c o T
case zero =>
rcases o with a | a
· exact terminates_parallel.aux a T
have H : Seq.destruct S = some (some c, Seq.tail S) := by simp [Seq.destruct, (· <$> ·), ← a]
rcases h : parallel.aux2 l with a | l'
· have C : corec parallel.aux1 (l, S) = pure a :=
by
apply destruct_eq_pure
rw [corec_eq, parallel.aux1]
rw [h]
simp only [rmap]
rw [C]
infer_instance
· have C : corec parallel.aux1 (l, S) = _ :=
destruct_eq_think
(by
simp only [corec_eq, rmap, parallel.aux1.eq_1]
rw [h, H])
rw [C]
refine @Computation.think_terminates _ _ ?_
apply terminates_parallel.aux _ T
simp
case succ n IH =>
rcases o with a | a
· exact terminates_parallel.aux a T
rcases h : parallel.aux2 l with a | l'
· have C : corec parallel.aux1 (l, S) = pure a :=
by
apply destruct_eq_pure
rw [corec_eq, parallel.aux1]
rw [h]
simp only [rmap]
rw [C]
infer_instance
· have C : corec parallel.aux1 (l, S) = _ :=
destruct_eq_think
(by
simp only [corec_eq, rmap, parallel.aux1.eq_1]
rw [h])
rw [C]
refine @Computation.think_terminates _ _ ?_
have TT : ∀ l', Terminates (corec parallel.aux1 (l', S.tail)) :=
by
intro
apply IH _ _ _ (Or.inr _) T
rw [a, Seq.get?_tail]
rcases e : Seq.get? S 0 with - | o
· have D : Seq.destruct S = none := by
dsimp [Seq.destruct]
rw [e]
rfl
rw [D]
simp only
have TT := TT l'
rwa [Seq.destruct_eq_none D, Seq.tail_nil] at TT
· have D : Seq.destruct S = some (o, S.tail) :=
by
dsimp [Seq.destruct]
rw [e]
rfl
rw [D]
cases o <;> simp [TT]
