Lean4
theorem exists_of_mem_parallel {S : WSeq (Computation α)} {a} (h : a ∈ parallel S) : ∃ c ∈ S, a ∈ c :=
by
suffices ∀ C, a ∈ C → ∀ (l : List (Computation α)) (S), corec parallel.aux1 (l, S) = C → ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c
from
let ⟨c, h1, h2⟩ := this _ h [] S rfl
⟨c, h1.resolve_left <| List.not_mem_nil, h2⟩
let F : List (Computation α) → α ⊕ (List (Computation α)) → Prop :=
by
intro l a
rcases a with a | l'
· exact ∃ c ∈ l, a ∈ c
· exact ∀ a', (∃ c ∈ l', a' ∈ c) → ∃ c ∈ l, a' ∈ c
have lem1 (l) : F l (parallel.aux2 l) :=
by
induction l <;> simp only [parallel.aux2, List.foldr]
case nil =>
intro a h
assumption
case cons c l IH =>
simp only [parallel.aux2] at IH
revert IH
cases
List.foldr
(fun c o =>
match o with
| Sum.inl a => Sum.inl a
| Sum.inr ls => rmap (fun c' => c' :: ls) (destruct c))
(Sum.inr List.nil) l <;>
intro IH <;>
simp only
· rcases IH with ⟨c', cl, ac⟩
exact ⟨c', List.Mem.tail _ cl, ac⟩
· rcases h : destruct c with a | c' <;> simp only [rmap]
· refine ⟨c, List.mem_cons_self, ?_⟩
rw [destruct_eq_pure h]
apply ret_mem
· intro a' h
rcases h with ⟨d, dm, ad⟩
rcases List.mem_cons.mp dm with e | dl
· rw [e] at ad
refine ⟨c, List.mem_cons_self, ?_⟩
rw [destruct_eq_think h]
exact think_mem ad
· obtain ⟨d, dm⟩ := IH a' ⟨d, dl, ad⟩
obtain ⟨dm, ad⟩ := dm
exact ⟨d, List.Mem.tail _ dm, ad⟩
intro C aC
apply memRecOn aC <;> [skip; intro C' IH] <;> intro l S e <;> have e' := congr_arg destruct e <;> have := lem1 l <;>
simp only [parallel.aux1, corec_eq, destruct_pure, destruct_think] at e' <;>
revert this e' <;>
rcases parallel.aux2 l with a' | l' <;>
intro this e' <;>
[injection e' with h'; injection e'; injection e'; injection e' with h']
· rw [h'] at this
rcases this with ⟨c, cl, ac⟩
exact ⟨c, Or.inl cl, ac⟩
· rcases e : Seq.destruct S with - | a <;> rw [e] at h'
·
exact
let ⟨d, o, ad⟩ := IH _ _ h'
let ⟨c, cl, ac⟩ := this a ⟨d, o.resolve_right (WSeq.notMem_nil _), ad⟩
⟨c, Or.inl cl, ac⟩
· obtain ⟨o, S'⟩ := a
obtain - | c := o <;> simp only at h' <;> rcases IH _ _ h' with ⟨d, dl | dS', ad⟩
·
exact
let ⟨c, cl, ac⟩ := this a ⟨d, dl, ad⟩
⟨c, Or.inl cl, ac⟩
· refine ⟨d, Or.inr ?_, ad⟩
rw [Seq.destruct_eq_cons e]
exact Seq.mem_cons_of_mem _ dS'
· simp only [List.mem_cons] at dl
rcases dl with dc | dl
· rw [dc] at ad
refine ⟨c, Or.inr ?_, ad⟩
rw [Seq.destruct_eq_cons e]
apply Seq.mem_cons
·
exact
let ⟨c, cl, ac⟩ := this a ⟨d, dl, ad⟩
⟨c, Or.inl cl, ac⟩
· refine ⟨d, Or.inr ?_, ad⟩
rw [Seq.destruct_eq_cons e]
exact Seq.mem_cons_of_mem _ dS'
