Lean4
/-- Induction principle for parallel computations.
The reason this isn't trivial from `exists_of_mem_parallel` is because it eliminates to `Sort`. -/
def parallelRec {S : WSeq (Computation α)} (C : α → Sort v) (H : ∀ s ∈ S, ∀ a ∈ s, C a) {a} (h : a ∈ parallel S) :
C a := by
let T : WSeq (Computation (α × Computation α)) := S.map fun c => c.map fun a => (a, c)
have : S = T.map (map fun c => c.1) := by
rw [← WSeq.map_comp]
refine (WSeq.map_id _).symm.trans (congr_arg (fun f => WSeq.map f S) ?_)
funext c
dsimp [id, Function.comp_def]
rw [← map_comp]
exact (map_id _).symm
have pe := congr_arg parallel this
rw [← map_parallel] at pe
have h' := h
rw [pe] at h'
haveI : Terminates (parallel T) := (terminates_map_iff _ _).1 ⟨⟨_, h'⟩⟩
rcases e : get (parallel T) with ⟨a', c⟩
have : a ∈ c ∧ c ∈ S := by
rcases exists_of_mem_map h' with ⟨d, dT, cd⟩
rw [get_eq_of_mem _ dT] at e
cases e
dsimp at cd
cases cd
rcases exists_of_mem_parallel dT with ⟨d', dT', ad'⟩
rcases WSeq.exists_of_mem_map dT' with ⟨c', cs', e'⟩
rw [← e'] at ad'
rcases exists_of_mem_map ad' with ⟨a', ac', e'⟩
injection e' with i1 i2
constructor
· rwa [i1, i2] at ac'
· rwa [i2] at cs'
obtain ⟨ac, cs⟩ := this
apply H _ cs _ ac
