Graph.DSep

theorem bbReachable_mono_source {Z : Finset V} {X X' : Finset V} (hXX' : X' ⊆ X) : G.bbReachable Z X' ⊆ G.bbReachable Z X := by simp only [bbReachable] exact bbReachAux_mono_combined G Z (refl _) (Finset.biUnion_subset_biUnion_of_subset_left _ hXX') _

theorem bbReachable_bbStep_subset (Z X : Finset V) {s : BBState V} (hs : s ∈ G.bbReachable Z X) : G.bbStep Z s ⊆ G.bbReachable Z X := by -- Apply `bbReachAux_closed_of_invariant` with the initial setup -- `frontier = visited = bbInit X` and the trivial invariant -- (no element is outside the frontier). The fuel `2 * card V + 1` -- is enough since the state space has size `2 * card V`. unfold bbReachable at hs ⊢ apply bbReachAux_closed_of_invariant G Z (G.bbInit X) (G.bbInit X) (2 * card V + 1) (refl _) · intro s hsv hsf; exact absurd hsv hsf · -- fuel + visited.card = 2|V| + 1 + visited.card ≥ 2|V| + 1 have h := zero_le (G.bbInit X).card omega · exact hs

theorem isActiveWalk_reverse {Z : Finset V} {p : List V} (h : G.IsActiveWalk Z p) : G.IsActiveWalk Z p.reverse := by obtain ⟨hadj, hcoll⟩ := h set n := p.length refine ⟨fun i hi => ?_, fun i hi => ?_⟩ · -- Adjacency: p.reverse[i] and p.reverse[i+1] are UAdj have hn : i + 1 < n := by rw [List.length_reverse] at hi; exact hi rw [get_rev, get_rev] -- p[n-1-i] and p[n-1-(i+1)] = p[n-2-i] are UAdj -- From hadj: p[n-2-i] and p[n-2-i+1] = p[n-1-i] are UAdj have hj : n - 1 - (i + 1) + 1 < n := by omega have := hadj (n - 1 - (i + 1)) hj have heq1 : n - 1 - (i + 1) + 1 = n - 1 - i := by omega rw [show (⟨n - 1 - (i + 1) + 1, hj⟩ : Fin p.length) = ⟨n - 1 - i, by omega⟩ from Fin.ext heq1] at this exact G.UAdj_symm this · -- Collider condition: triple (p.reverse[i], p.reverse[i+1], p.reverse[i+2]) have hn : i + 2 < n := by rw [List.length_reverse] at hi; exact hi rw [get_rev, get_rev, get_rev] -- The triple (i, i+1, i+2) in the reverse corresponds to -- (n-1-i, n-2-i, n-3-i) in the original, which is the reversed triple -- (n-3-i, n-2-i, n-1-i). Use hcoll at index (n-3-i) with And.comm. have hj : p.length - 3 - i + 2 < p.length := by omega have horig := hcoll (p.length - 3 - i) hj simp only [IsCollider] at horig ⊢ -- The indices in horig are (n-3-i, n-3-i+1, n-3-i+2) = (n-3-i, n-2-i, n-1-i) -- The goal indices are (n-1-i, n-2-i, n-3-i) via get_rev -- These are the same vertices but the outer pair is swapped -- First, show the Fin values match: n-3-i+k and n-1-(i+2-k) are the same have heq0 : (⟨p.length - 3 - i, by omega⟩ : Fin p.length) = ⟨p.length - 1 - (i + 2), by omega⟩ := Fin.ext (by simp; omega) have heq1 : (⟨p.length - 3 - i + 1, by omega⟩ : Fin p.length) = ⟨p.length - 1 - (i + 1), by omega⟩ := Fin.ext (by simp; omega) have heq2 : (⟨p.length - 3 - i + 2, hj⟩ : Fin p.length) = ⟨p.length - 1 - i, by omega⟩ := Fin.ext (by simp; omega) simp only [heq0, heq1, heq2] at horig -- horig and goal differ only by And.comm in the if-condition. -- Introduce abbreviations for the three vertices to avoid Fin issues. set a := p.get ⟨p.length - 1 - (i + 2), by omega⟩ set b := p.get ⟨p.length - 1 - (i + 1), by omega⟩ set c := p.get ⟨p.length - 1 - i, by omega⟩ -- horig : if (G.edge a b ∧ G.edge c b) then b ∈ ... else b ∉ ... -- goal : if (G.edge c b ∧ G.edge a b) then b ∈ ... else b ∉ ... -- Split on the condition; And.comm relates the two. by_cases hab : G.edge a b ∧ G.edge c b · simp only [hab] at horig simp only [hab.symm, horig] · simp only [hab, ite_false] at horig have : ¬(G.edge c b ∧ G.edge a b) := fun h => hab h.symm simp only [this, ite_false] exact horig

theorem isActiveWalk_of_reversed_directed {Z : Finset V} {p : List V} (hdir : ∀ (i : ℕ) (hi : i + 1 < p.length), G.edge (p.get ⟨i + 1, hi⟩) (p.get ⟨i, by omega⟩)) (hZ : ∀ (i : ℕ) (hi : i + 2 < p.length), p.get ⟨i + 1, by omega⟩ ∉ Z) : G.IsActiveWalk Z p := by refine ⟨fun i hi => ?_, fun i hi => ?_⟩ · -- Adjacency: hdir says G.edge p[i+1] p[i], so p[i] and p[i+1] are UAdj exact inr (hdir i hi) · -- Collider condition. Let l = p[i], m = p[i+1], r = p[i+2]. -- hdir at index i: G.edge m l (so NOT edge l m, by asymm) -- hdir at index i+1: G.edge r m -- IsCollider l m r requires G.edge l m ∧ G.edge r m; first conjunct fails. simp only have hml : G.edge (p.get ⟨i + 1, by omega⟩) (p.get ⟨i, by omega⟩) := hdir i (by omega) have hlm_false : ¬ G.edge (p.get ⟨i, by omega⟩) (p.get ⟨i + 1, by omega⟩) := G.asymm hml have hnotcoll : ¬ G.IsCollider (p.get ⟨i, by omega⟩) (p.get ⟨i + 1, by omega⟩) (p.get ⟨i + 2, hi⟩) := by intro ⟨h1, _⟩; exact hlm_false h1 rw [if_neg hnotcoll] -- Need p[i+1] ∉ Z, which follows from hZ exact hZ i hi

theorem lastIdxLt_eq_some {n : ℕ} {P : ℕ → Prop} [DecidablePred P] {i : ℕ} (h : lastIdxLt n P = some i) : i < n ∧ P i ∧ ∀ j, i < j → j < n → ¬ P j := by unfold lastIdxLt at h split_ifs at h with hne · injection h with heq subst heq have hi_mem : ((range n).filter P).max' hne ∈ (range n).filter P := Finset.max'_mem _ hne rw [mem_filter, Finset.mem_range] at hi_mem refine ⟨hi_mem.1, hi_mem.2, ?_⟩ intro j hj hjn hPj have hjmem : j ∈ (range n).filter P := by rw [mem_filter, Finset.mem_range]; exact ⟨hjn, hPj⟩ have := Finset.le_max' _ j hjmem omega

theorem lastIdxLt_eq_none {n : ℕ} {P : ℕ → Prop} [DecidablePred P] (h : lastIdxLt n P = none) : ∀ i, i < n → ¬ P i := by intro i hi hPi have hmem : i ∈ (range n).filter P := by rw [mem_filter, Finset.mem_range]; exact ⟨hi, hPi⟩ have hne : ((range n).filter P).Nonempty := ⟨i, hmem⟩ simp [lastIdxLt, hne] at h

theorem take_suffix_at_last_S {X Z S : Finset V} {p : List V} {x w : V} (hxX : x ∈ X) (hlen : p.length ≥ 2) (hact : G.IsActiveWalk (Z ∪ S) p) (hhead : p.head? = some x) (hlast : p.getLast? = some w) : ∃ (x' : V) (q : List V), x' ∈ X ∪ S ∧ q.length ≥ 2 ∧ G.IsActiveWalk (Z ∪ S) q ∧ q.head? = some x' ∧ q.getLast? = some w ∧ (∀ (k : ℕ) (_hk1 : 0 < k) (hk2 : k + 1 < q.length), q.get ⟨k, by omega⟩ ∉ S) := by -- Interior-S-index set: i : Fin p.length with i+1 < p.length and p.get i ∈ S. let IS : Finset (Fin p.length) := Finset.univ.filter (fun i => i.val + 1 < p.length ∧ p.get i ∈ S) by_cases hIS : IS.Nonempty · -- Cut at the maximum. let i₀ : Fin p.length := IS.max' hIS have hi₀_mem : i₀ ∈ IS := Finset.max'_mem _ hIS have hi₀_filt : i₀.val + 1 < p.length ∧ p.get i₀ ∈ S := by have := hi₀_mem simp only [IS, mem_filter, Finset.mem_univ, true_and] at this exact this let q : List V := p.drop i₀.val refine ⟨p.get i₀, q, ?_, ?_, ?_, ?_, ?_, ?_⟩ · exact mem_union_right _ hi₀_filt.2 · show q.length ≥ 2 simp only [q, List.length_drop] omega · -- G.IsActiveWalk (Z ∪ S) q — shift indices obtain ⟨hadj, hcoll⟩ := hact refine ⟨fun i hi => ?_, fun i hi => ?_⟩ · have hq_len : q.length = p.length - i₀.val := by simp only [q, List.length_drop] have hi' : i₀.val + i + 1 < p.length := by rw [hq_len] at hi; omega have hq_i : q.get ⟨i, by omega⟩ = p.get ⟨i₀.val + i, by omega⟩ := by simp [q, List.getElem_drop] have hq_i1 : q.get ⟨i + 1, hi⟩ = p.get ⟨i₀.val + (i + 1), by omega⟩ := by simp [q, List.getElem_drop] rw [hq_i, hq_i1] have hadj' := hadj (i₀.val + i) (by omega) exact hadj' · have hq_len : q.length = p.length - i₀.val := by simp only [q, List.length_drop] have hi' : i₀.val + i + 2 < p.length := by rw [hq_len] at hi; omega have hq_i : q.get ⟨i, by omega⟩ = p.get ⟨i₀.val + i, by omega⟩ := by simp [q, List.getElem_drop] have hq_i1 : q.get ⟨i + 1, by omega⟩ = p.get ⟨i₀.val + (i + 1), by omega⟩ := by simp [q, List.getElem_drop] have hq_i2 : q.get ⟨i + 2, hi⟩ = p.get ⟨i₀.val + (i + 2), by omega⟩ := by simp [q, List.getElem_drop] rw [hq_i, hq_i1, hq_i2] have hcoll' := hcoll (i₀.val + i) (by omega) exact hcoll' · -- q.head? = some (p.get i₀) have hq_ne : q ≠ [] := by simp only [q, ne_eq, List.drop_eq_nil_iff] omega have : q.head? = some (q.head hq_ne) := List.head?_eq_some_head hq_ne rw [this] congr 1 simp only [q] rw [List.head_drop] rfl · -- q.getLast? = p.getLast? = some w have hq_ne : q ≠ [] := by simp only [q, ne_eq, List.drop_eq_nil_iff] omega have hp_ne : p ≠ [] := by intro hnil; rw [hnil] at hlen; simp at hlen rw [getLast?_eq_some_getLast hq_ne] rw [getLast?_eq_some_getLast hp_ne] at hlast simp only [q] rw [List.getLast_drop] exact hlast · -- strict interior q has no S-vertex intro k hk1 hk2 hkS have hq_len : q.length = p.length - i₀.val := by simp only [q, List.length_drop] have hq_k : q.get ⟨k, by omega⟩ = p.get ⟨i₀.val + k, by rw [hq_len] at hk2; omega⟩ := by simp [q, List.getElem_drop] rw [hq_k] at hkS have hidx_lt : i₀.val + k < p.length := by rw [hq_len] at hk2; omega have hmem_IS : (⟨i₀.val + k, hidx_lt⟩ : Fin p.length) ∈ IS := by simp only [IS, mem_filter, Finset.mem_univ, true_and] refine ⟨?_, hkS⟩ rw [hq_len] at hk2; omega have hle := Finset.le_max' _ _ hmem_IS change i₀.val + k ≤ i₀.val at hle omega · -- No interior S-vertex. Take q := p. refine ⟨x, p, mem_union_left _ hxX, hlen, hact, hhead, hlast, ?_⟩ intro k hk1 hk2 hkS apply hIS refine ⟨⟨k, by omega⟩, ?_⟩ simp only [IS, mem_filter, Finset.mem_univ, true_and] exact ⟨hk2, hkS⟩

theorem isActiveWalk_Z_of_no_S_only_collider {Z S : Finset V} {q : List V} (hact : G.IsActiveWalk (Z ∪ S) q) (hNoSOnly : ∀ (i : ℕ) (hi : i + 2 < q.length), G.IsCollider (q.get ⟨i, by omega⟩) (q.get ⟨i + 1, by omega⟩) (q.get ⟨i + 2, hi⟩) → q.get ⟨i + 1, by omega⟩ ∈ G.bbZAncestors Z) : G.IsActiveWalk Z q := by obtain ⟨hadj, hcoll⟩ := hact refine ⟨hadj, fun i hi => ?_⟩ -- Let m := q.get ⟨i+1, _⟩. Two cases: collider or not. simp only by_cases hC : G.IsCollider (q.get ⟨i, by omega⟩) (q.get ⟨i + 1, by omega⟩) (q.get ⟨i + 2, hi⟩) · -- Collider: use hNoSOnly rw [if_pos hC] exact hNoSOnly i hi hC · -- Non-collider: use the (Z ∪ S)-activity to conclude m ∉ Z ∪ S, hence m ∉ Z. rw [if_neg hC] have := hcoll i hi simp only [if_neg hC] at this -- this : q.get ⟨i + 1, _⟩ ∉ Z ∪ S intro hZ exact this (mem_union_left _ hZ)

theorem hasActiveWalk_symm (X Y Z : Finset V) : G.HasActiveWalk X Y Z → G.HasActiveWalk Y X Z := by rintro ⟨p, hlen, hact, hhead, hlast⟩ refine ⟨p.reverse, ?_, G.isActiveWalk_reverse hact, ?_, ?_⟩ · simp only [List.length_reverse]; exact hlen · rwa [List.head?_reverse] · rwa [getLast?_reverse]

theorem isActiveWalk_cons_of_active_triple {Z : Finset V} {z w u : V} {r : List V} (hadj : G.UAdj z w) (htri : if G.IsCollider z w u then w ∈ G.bbZAncestors Z else w ∉ Z) (hact : G.IsActiveWalk Z (w :: u :: r)) : G.IsActiveWalk Z (z :: w :: u :: r) := by obtain ⟨hadj_old, hcoll_old⟩ := hact refine ⟨fun i hi => ?_, fun i hi => ?_⟩ · cases i with | zero => simpa using hadj | succ i => have h := hadj_old i (by simpa [Nat.add_assoc] using hi) simpa using h · cases i with | zero => simpa using htri | succ i => have h := hcoll_old i (by simpa [Nat.add_assoc] using hi) simpa [Nat.add_assoc] using h

theorem active_triple_swap_outer {Z : Finset V} {u w z : V} (h : if G.IsCollider u w z then w ∈ G.bbZAncestors Z else w ∉ Z) : if G.IsCollider z w u then w ∈ G.bbZAncestors Z else w ∉ Z := by simp only [IsCollider] at h ⊢ by_cases hC : G.edge u w ∧ G.edge z w · have hC' : G.edge z w ∧ G.edge u w := hC.symm simpa [hC'] using h · have hC' : ¬(G.edge z w ∧ G.edge u w) := fun h' => hC h'.symm simpa [hC, hC'] using h

theorem isActiveWalk_pair {Z : Finset V} {a b : V} (h : G.UAdj a b) : G.IsActiveWalk Z [a, b] := by refine ⟨fun i hi => ?_, fun i hi => ?_⟩ · match i, hi with | 0, _ => simpa using h · have hlt : i + 2 < 2 := by simpa using hi omega

theorem isActiveWalk_cons_tail {Z : Finset V} {u w : V} {r : List V} (h : G.IsActiveWalk Z (u :: w :: r)) : G.IsActiveWalk Z (w :: r) := by obtain ⟨hadj, hcoll⟩ := h refine ⟨fun i hi => ?_, fun i hi => ?_⟩ · have h' := hadj (i + 1) (by simpa [Nat.add_assoc] using Nat.succ_lt_succ hi) simpa using h' · have h' := hcoll (i + 1) (by simpa [Nat.add_assoc] using Nat.succ_lt_succ hi) simpa [Nat.add_assoc] using h'

theorem dSep_subset_left {X X' Y Z : Finset V} (hXX' : X' ⊆ X) (h : G.dSep X Y Z) : G.dSep X' Y Z := by rcases h with ⟨hXY, hXZ, hYZ, hReach⟩ exact ⟨Disjoint.mono_left hXX' hXY, Disjoint.mono_left hXX' hXZ, hYZ, Disjoint.mono_left (G.bbReachableVertices_mono_source hXX') hReach⟩

theorem dSep_subset_right {X Y Y' Z : Finset V} (hYY' : Y' ⊆ Y) (h : G.dSep X Y Z) : G.dSep X Y' Z := by rcases h with ⟨hXY, hXZ, hYZ, hReach⟩ exact ⟨Disjoint.mono_right hYY' hXY, hXZ, Disjoint.mono_left hYY' hYZ, Disjoint.mono_right hYY' hReach⟩

theorem bbZAncestors_union_eq (Z S : Finset V) : G.bbZAncestors (Z ∪ S) = G.bbZAncestors Z ∪ G.bbZAncestors S := by ext v simp only [bbZAncestors, ancestralSet, ancestorsSet, mem_union, mem_filter, Finset.mem_univ, true_and] constructor · rintro (hZS | ⟨w, hwZS, haw⟩) · rcases hZS with hZ | hS · exact inl (inl hZ) · exact inr (inl hS) · rcases hwZS with hwZ | hwS · exact inl (inr ⟨w, hwZ, haw⟩) · exact inr (inr ⟨w, hwS, haw⟩) · rintro ((hZ | ⟨w, hwZ, haw⟩) | (hS | ⟨w, hwS, haw⟩)) · exact inl (inl hZ) · exact inr ⟨w, inl hwZ, haw⟩ · exact inl (inr hS) · exact inr ⟨w, inr hwS, haw⟩

theorem exists_directedPath_avoiding {u v : V} (huv : G.isAncestor u v) {Z : Finset V} (huZ : u ∉ G.ancestralSet Z) : ∃ (p : List V), p.length ≥ 2 ∧ p.head? = some u ∧ p.getLast? = some v ∧ (∀ (i : ℕ) (hi : i + 1 < p.length), G.edge (p.get ⟨i, by omega⟩) (p.get ⟨i + 1, hi⟩)) ∧ (∀ x ∈ p, x ∉ Z) := by induction huv with | edge he => rename_i u v refine ⟨[u, v], ?_, rfl, rfl, ?_, ?_⟩ · simp · intro i hi -- p.length = 2, so i + 1 < 2 means i = 0 match i, hi with | 0, _ => exact he · intro x hx simp only [List.mem_cons, List.not_mem_nil, or_false] at hx rcases hx with hxu | hxv · -- u ∉ Z because Z ⊆ ancestralSet Z subst hxu intro hxZ exact huZ (mem_union_left _ hxZ) · -- v ∉ Z: else u ∈ ancestorsSet Z ⊆ ancestralSet Z subst hxv intro hvZ apply huZ apply mem_union_right simp only [ancestorsSet, mem_filter, Finset.mem_univ, true_and] exact ⟨_, hvZ, isAncestor.edge he⟩ | trans h₁ he' ih => rename_i u w v obtain ⟨p, hlen, hhead, hlast, hedge, hZ⟩ := ih -- p is a u→w path. Build p ++ [v]. refine ⟨p ++ [v], ?_, ?_, ?_, ?_, ?_⟩ · -- length ≥ 2 rw [List.length_append, List.length_singleton]; omega · -- head? of p ++ [v] = head? of p = some u (p nonempty) have hne : p ≠ [] := by intro hp; rw [hp] at hlen; simp at hlen rw [List.head?_append_of_ne_nil _ hne] exact hhead · -- getLast? of p ++ [v] = some v simp [getLast?_append] · -- edge condition intro i hi have hlen' : (p ++ [v]).length = p.length + 1 := by rw [List.length_append, List.length_singleton] have hi' : i + 1 < p.length + 1 := by rw [← hlen']; exact hi -- Convert .get to [i] change G.edge ((p ++ [v])[i]) ((p ++ [v])[i + 1]) by_cases hlt : i + 1 < p.length · -- both indices in p-part have hi0 : i < p.length := by omega have e1 : (p ++ [v])[i]'(by omega) = p[i]'hi0 := by rw [List.getElem_append]; simp [hi0] have e2 : (p ++ [v])[i + 1]'(by omega) = p[i + 1]'hlt := by rw [List.getElem_append]; simp [hlt] rw [e1, e2] have := hedge i hlt -- convert .get to [i] for hedge simpa [List.get_eq_getElem] using this · -- seam: i + 1 = p.length push_neg at hlt have heq : i + 1 = p.length := by omega have hplen_pos : 0 < p.length := by omega have hi0 : i < p.length := by omega have hne : p ≠ [] := List.ne_nil_of_length_pos hplen_pos -- p[p.length - 1] = w (from hlast) have hlast_w : p[p.length - 1]'(by omega) = w := by have h1 : p.getLast? = some (p.getLast hne) := getLast?_eq_some_getLast hne rw [hlast] at h1 have : p.getLast hne = w := by exact (Option.some_inj.mp h1.symm) rw [← this] exact (List.getLast_eq_getElem hne).symm have hi_eq : i = p.length - 1 := by omega have e1 : (p ++ [v])[i]'(by omega) = p[i]'hi0 := by rw [List.getElem_append]; simp [hi0] have e2 : (p ++ [v])[i + 1]'(by omega) = v := by rw [List.getElem_append] simp [heq] have e3 : p[i]'hi0 = w := by have : p[i]'hi0 = p[p.length - 1]'(by omega) := by congr 1 rw [this, hlast_w] rw [e1, e2, e3] exact he' · -- avoidance intro x hx rw [List.mem_append] at hx rcases hx with hxp | hxv · exact hZ x hxp · rw [List.mem_singleton] at hxv subst hxv intro hvZ apply huZ apply mem_union_right simp only [ancestorsSet, mem_filter, Finset.mem_univ, true_and] refine ⟨x, hvZ, ?_⟩ exact G.isAncestor_trans h₁ (isAncestor.edge he')

theorem activeWalk_transfer_cond_to_source {X Z S : Finset V} {p : List V} {x w : V} (hxX : x ∈ X) (hlen : p.length ≥ 2) (hact : G.IsActiveWalk (Z ∪ S) p) (hhead : p.head? = some x) (hlast : p.getLast? = some w) : ∃ (x' : V) (p' : List V), x' ∈ X ∪ S ∧ p'.length ≥ 2 ∧ G.IsActiveWalk Z p' ∧ p'.head? = some x' ∧ p'.getLast? = some w := by classical -- Step A: Take suffix at last S-vertex. Strict interior of q has no S-vertex. obtain ⟨x₁, q, hx₁XS, hqlen, hqact, hqhead, hqlast, hqInterior⟩ := G.take_suffix_at_last_S hxX hlen hact hhead hlast -- Case split on existence of an S-only-activated collider in q's strict interior. by_cases hExists : ∃ (i : ℕ) (hi : i + 2 < q.length), G.IsCollider (q.get ⟨i, by omega⟩) (q.get ⟨i + 1, by omega⟩) (q.get ⟨i + 2, hi⟩) ∧ q.get ⟨i + 1, by omega⟩ ∉ G.bbZAncestors Z · -- Case B: reroute via directed ancestor path. -- Pick the LARGEST strict-interior index j_star of q at which there is an -- "S-only activated" collider (activated in bbZAncestors (Z ∪ S) via -- bbZAncestors S but NOT already in bbZAncestors Z). Use Finset.max'. let IColl : Finset ℕ := (range q.length).filter (fun i => ∃ (hi : i + 2 < q.length), G.IsCollider (q.get ⟨i, by omega⟩) (q.get ⟨i + 1, by omega⟩) (q.get ⟨i + 2, hi⟩) ∧ q.get ⟨i + 1, by omega⟩ ∉ G.bbZAncestors Z) have hIColl_ne : IColl.Nonempty := by obtain ⟨i, hi, hC, hNotZ⟩ := hExists refine ⟨i, ?_⟩ simp only [IColl, mem_filter, Finset.mem_range] exact ⟨by omega, hi, hC, hNotZ⟩ let j_star : ℕ := IColl.max' hIColl_ne have hj_star_mem : j_star ∈ IColl := Finset.max'_mem _ hIColl_ne have hj_star_spec : j_star < q.length ∧ ∃ (hj : j_star + 2 < q.length), G.IsCollider (q.get ⟨j_star, by omega⟩) (q.get ⟨j_star + 1, by omega⟩) (q.get ⟨j_star + 2, hj⟩) ∧ q.get ⟨j_star + 1, by omega⟩ ∉ G.bbZAncestors Z := by have := hj_star_mem simp only [IColl, mem_filter, Finset.mem_range] at this exact this obtain ⟨_hj_lt_len, hj_lt, hj_coll, hm_notZ⟩ := hj_star_spec set m_star : V := q.get ⟨j_star + 1, by omega⟩ with hm_star_def -- m_star is a strict-interior vertex, so m_star ∉ S (from hqInterior). have hm_notS : m_star ∉ S := hqInterior (j_star + 1) (by omega) (by omega) -- m_star ∈ bbZAncestors (Z ∪ S) comes from the (Z ∪ S)-activity at the collider. have hm_coll_ZUS : m_star ∈ G.bbZAncestors (Z ∪ S) := by obtain ⟨_hqadj, hqcoll⟩ := hqact have hval := hqcoll j_star hj_lt simp only at hval rw [if_pos hj_coll] at hval exact hval -- Since m_star ∉ bbZAncestors Z, by bbZAncestors_union_eq, m_star ∈ bbZAncestors S. have hm_S_anc : m_star ∈ G.bbZAncestors S := by have hsplit : m_star ∈ G.bbZAncestors Z ∪ G.bbZAncestors S := by rw [← G.bbZAncestors_union_eq]; exact hm_coll_ZUS rw [mem_union] at hsplit rcases hsplit with hZ | hS · exact absurd hZ hm_notZ · exact hS -- Unfold bbZAncestors S = S ∪ ancestorsSet S. Since m_star ∉ S, -- m_star is a proper ancestor of some s ∈ S. have hm_ancset_S : ∃ s ∈ S, G.isAncestor m_star s := by have hmem : m_star ∈ G.ancestralSet S := hm_S_anc simp only [ancestralSet, mem_union] at hmem rcases hmem with h | h · exact absurd h hm_notS · simp only [ancestorsSet, mem_filter, Finset.mem_univ, true_and] at h exact h obtain ⟨s, hsS, hmAncs⟩ := hm_ancset_S -- m_star ∉ ancestralSet Z = bbZAncestors Z. have hm_notAncZ : m_star ∉ G.ancestralSet Z := hm_notZ -- Get a directed path m_star → ... → s avoiding Z. obtain ⟨r, hr_len, hr_head, hr_last, hr_edges, hr_avoid⟩ := G.exists_directedPath_avoiding hmAncs hm_notAncZ -- Build q' := r.reverse ++ q.drop (j_star + 2). let qTail : List V := q.drop (j_star + 2) let qPrime : List V := r.reverse ++ qTail have hr_ne : r ≠ [] := by intro h; rw [h] at hr_len; simp at hr_len have hrRev_ne : r.reverse ≠ [] := by simp [hr_ne] have hqTail_ne : qTail ≠ [] := by simp only [qTail, ne_eq, List.drop_eq_nil_iff]; omega -- Head of qPrime = s (head of r.reverse = last of r = s). have hqPrime_head : qPrime.head? = some s := by simp only [qPrime, List.head?_append_of_ne_nil _ hrRev_ne, List.head?_reverse] exact hr_last -- Last of qPrime = last of qTail = w. have hqTail_last : qTail.getLast? = some w := by have hq_ne : q ≠ [] := by intro h; rw [h] at hqlen; simp at hqlen rw [getLast?_eq_some_getLast hqTail_ne] rw [getLast?_eq_some_getLast hq_ne] at hqlast simp only [qTail] rw [List.getLast_drop] exact hqlast have hqPrime_last : qPrime.getLast? = some w := by simp only [qPrime, getLast?_append, hqTail_last] rfl -- Length ≥ 2. have hqPrime_len : qPrime.length ≥ 2 := by have hrl : r.reverse.length ≥ 2 := by rw [List.length_reverse]; exact hr_len have htl : qTail.length ≥ 1 := List.length_pos_iff.mpr hqTail_ne simp only [qPrime, List.length_append] omega -- Head s ∈ X ∪ S. have hs_XS : s ∈ X ∪ S := mem_union_right _ hsS refine ⟨s, qPrime, hs_XS, hqPrime_len, ?_, hqPrime_head, hqPrime_last⟩ -- The remaining goal: G.IsActiveWalk Z qPrime. -- Structure (deferred — indices are finicky): -- (A) inside r.reverse (strict interior): edges are reversed-directed, -- so non-colliders; vertices avoid Z by hr_avoid. -- (B) seam at r.reverse boundary: last vertex of r.reverse = r.head = m_star. -- First vertex of qTail = q.get ⟨j_star + 2, _⟩. -- Adjacency at the seam: q-side is G.UAdj (m_star, q[j_star+2]) from hqact. -- Collider triple at index r.length - 2 (inside r.reverse, ending at m_star): -- m_star = r.head; predecessor in r.reverse = r[1]; successor is -- q[j_star+2]. Asymmetry rules out collider (r.head → r[1] means the -- edge points OUT of m_star; no way to have edge q[j_star+2] → m_star -- AND edge r[1] → m_star both as required, since the former goes out). -- Actually the non-collider guard needs m_star ∉ Z — from hm_notAncZ. -- Collider triple at index r.length - 1 (m_star, q[j_star+2], q[j_star+3]): -- adjacency m_star-q[j_star+2] (UAdj from hqact). For collider status use -- maximality of j_star to show q[j_star+2] (the m of this triple) isn't -- an S-only activated collider in the ORIGINAL q — if it is a collider, -- it must already lie in bbZAncestors Z; otherwise it must ∉ Z ∪ S. -- (C) inside qTail proper (indices ≥ r.length): translated triples from q at -- indices ≥ j_star + 2. By maximality of j_star, any collider there is -- in bbZAncestors Z already; non-colliders avoid Z ∪ S, hence avoid Z. -- ACTIVE-WALK VERIFICATION for qPrime = r.reverse ++ q.drop (j_star + 2). -- Index layout: qPrime[k] = r[R-1-k] for k < R := r.length; qPrime[k] = -- q[j_star + 2 + (k - R)] for k ≥ R. Cases on (i vs R). obtain ⟨hqadj, hqcoll⟩ := hqact have hrrev_len : r.reverse.length = r.length := List.length_reverse have hqTail_len_eq : qTail.length = q.length - (j_star + 2) := by simp only [qTail, List.length_drop] have hqP_len_eq : qPrime.length = r.length + qTail.length := by simp only [qPrime, List.length_append, hrrev_len] have hm_notZ_simple : m_star ∉ Z := fun h => hm_notZ (mem_union_left _ h) -- r.get ⟨0, _⟩ = m_star have hr_get_0 : r.get ⟨0, by omega⟩ = m_star := by have h1 : r.head? = some (r.head hr_ne) := List.head?_eq_some_head hr_ne rw [hr_head] at h1 have hhead_eq : r.head hr_ne = m_star := Option.some_inj.mp h1.symm rw [← hhead_eq] rw [List.get_eq_getElem, List.getElem_zero] -- Maximality of j_star: any j' > j_star with a collider has middle ∈ bbZAncestors Z have hmax : ∀ (j' : ℕ) (hj' : j' + 2 < q.length) (_hlt : j_star < j') (_hcol : G.IsCollider (q.get ⟨j', by omega⟩) (q.get ⟨j' + 1, by omega⟩) (q.get ⟨j' + 2, hj'⟩)), q.get ⟨j' + 1, by omega⟩ ∈ G.bbZAncestors Z := by intro j' hj' hlt hcol by_contra hnotZ have hmem : j' ∈ IColl := by simp only [IColl, mem_filter, Finset.mem_range] exact ⟨by omega, hj', hcol, hnotZ⟩ have hle := Finset.le_max' _ _ hmem change j' ≤ j_star at hle omega -- qPrime on left part (k < r.length): qPrime[k] = r[r.length - 1 - k] have hqP_L : ∀ (k : ℕ) (hkR : k < r.length), qPrime.get ⟨k, by rw [hqP_len_eq]; omega⟩ = r.get ⟨r.length - 1 - k, by omega⟩ := by intro k hkR have hk_rev : k < r.reverse.length := by rw [hrrev_len]; exact hkR simp only [qPrime, List.get_eq_getElem, List.getElem_append_left (h := hk_rev), List.getElem_reverse] -- qPrime on right part (r.length ≤ k): qPrime[k] = q[j_star + 2 + (k - r.length)] have hqP_R : ∀ (k : ℕ) (hkL : r.length ≤ k) (hk : k < qPrime.length), qPrime.get ⟨k, hk⟩ = q.get ⟨j_star + 2 + (k - r.length), by rw [hqP_len_eq, hqTail_len_eq] at hk; omega⟩ := by intro k hkL hk have hk_rev : r.reverse.length ≤ k := by rw [hrrev_len]; exact hkL simp only [qPrime, List.get_eq_getElem, List.getElem_append_right hk_rev, qTail, List.getElem_drop, hrrev_len] -- Main split: adjacency and collider condition refine ⟨?_, ?_⟩ · -- Adjacency: G.UAdj qPrime[i] qPrime[i+1] intro i hi rw [hqP_len_eq] at hi by_cases hA1 : i + 1 < r.length · -- A1: both in r.reverse have hiR : i < r.length := by omega rw [hqP_L i hiR, hqP_L (i + 1) hA1] -- hr_edges at index r.length - 2 - i: G.edge r[r.length-2-i] r[r.length-1-i] have hedge_idx : r.length - 2 - i + 1 < r.length := by omega have hedge := hr_edges (r.length - 2 - i) hedge_idx have heq : r.length - 2 - i + 1 = r.length - 1 - i := by omega rw [show (⟨r.length - 2 - i + 1, hedge_idx⟩ : Fin r.length) = ⟨r.length - 1 - i, by omega⟩ from Fin.ext heq] at hedge have heq2 : r.length - 1 - (i + 1) = r.length - 2 - i := by omega rw [show (⟨r.length - 1 - (i + 1), by omega⟩ : Fin r.length) = ⟨r.length - 2 - i, by omega⟩ from Fin.ext heq2] exact inr hedge · push_neg at hA1 -- r.length ≤ i + 1 by_cases hA2 : i + 1 = r.length · -- A2: seam: i = r.length - 1 have hi_eq : i = r.length - 1 := by omega subst hi_eq have hiR : r.length - 1 < r.length := by omega rw [hqP_L (r.length - 1) hiR] have hi1L : r.length ≤ r.length - 1 + 1 := by omega have hi1_lt : r.length - 1 + 1 < qPrime.length := by -- … truncated; follow the source link for the rest …

theorem isAncestor_mono_edge (G' : DAG V) (hEdge : ∀ u v : V, G'.edge u v → G.edge u v) {u v : V} (h : G'.isAncestor u v) : G.isAncestor u v := by induction h with | edge he => exact isAncestor.edge (hEdge _ _ he) | trans h₁ he ih => exact isAncestor.trans ih (hEdge _ _ he)

theorem bbZAncestors_mono_edge (G' : DAG V) (hEdge : ∀ u v : V, G'.edge u v → G.edge u v) (Z : Finset V) : G'.bbZAncestors Z ⊆ G.bbZAncestors Z := by intro v hv simp only [bbZAncestors, ancestralSet, ancestorsSet, mem_union, mem_filter, Finset.mem_univ, true_and] at hv ⊢ rcases hv with hvZ | ⟨w, hwZ, hvw⟩ · exact inl hvZ · exact inr ⟨w, hwZ, G.isAncestor_mono_edge G' hEdge hvw⟩

theorem uAdj_mono_edge (G' : DAG V) (hEdge : ∀ u v : V, G'.edge u v → G.edge u v) {u v : V} (h : G'.UAdj u v) : G.UAdj u v := by rcases h with huv | hvu · exact inl (hEdge _ _ huv) · exact inr (hEdge _ _ hvu)

theorem isCollider_of_supergraph (G' : DAG V) (hEdge : ∀ u v : V, G'.edge u v → G.edge u v) {l m r : V} (hadj_lm : G'.UAdj l m) (hadj_mr : G'.UAdj m r) (hcoll : G.IsCollider l m r) : G'.IsCollider l m r := by unfold IsCollider at hcoll ⊢ obtain ⟨hlm, hrm⟩ := hcoll constructor · rcases hadj_lm with hlm' | hml' · exact hlm' · exact absurd (hEdge _ _ hml') (G.asymm hlm) · rcases hadj_mr with hmr' | hrm' · exact absurd (hEdge _ _ hmr') (G.asymm hrm) · exact hrm'

theorem isActiveWalk_mono_edge (G' : DAG V) (hEdge : ∀ u v : V, G'.edge u v → G.edge u v) {Z : Finset V} {p : List V} (h : G'.IsActiveWalk Z p) : G.IsActiveWalk Z p := by obtain ⟨hadj, hcoll⟩ := h refine ⟨fun i hi => G.uAdj_mono_edge G' hEdge (hadj i hi), fun i hi => ?_⟩ simp only by_cases hC : G.IsCollider (p.get ⟨i, by omega⟩) (p.get ⟨i + 1, by omega⟩) (p.get ⟨i + 2, hi⟩) · rw [if_pos hC] have hC' : G'.IsCollider (p.get ⟨i, by omega⟩) (p.get ⟨i + 1, by omega⟩) (p.get ⟨i + 2, hi⟩) := G.isCollider_of_supergraph G' hEdge (hadj i (by omega)) (hadj (i + 1) (by omega)) hC have hval := hcoll i hi simp only at hval rw [if_pos hC'] at hval exact G.bbZAncestors_mono_edge G' hEdge Z hval · rw [if_neg hC] have hnotC' : ¬ G'.IsCollider (p.get ⟨i, by omega⟩) (p.get ⟨i + 1, by omega⟩) (p.get ⟨i + 2, hi⟩) := by intro hC' exact hC ⟨hEdge _ _ hC'.1, hEdge _ _ hC'.2⟩ have hval := hcoll i hi simp only at hval rwa [if_neg hnotC'] at hval

lemma ancestralSet_mono {S T : Finset V} (h : S ⊆ T) : G.ancestralSet S ⊆ G.ancestralSet T := by intro v hv rcases Finset.mem_union.mp hv with hvS | hvA · exact mem_union_left _ (h hvS) · simp only [ancestorsSet, mem_filter, Finset.mem_univ, true_and] at hvA obtain ⟨w, hwS, haw⟩ := hvA exact mem_union_right _ (by simp only [ancestorsSet, mem_filter, Finset.mem_univ, true_and] exact ⟨w, h hwS, haw⟩)

lemma mem_ancestralSet_of_isAncestor {u w : V} {S : Finset V} (hwS : w ∈ S) (h : G.isAncestor u w) : u ∈ G.ancestralSet S := by apply mem_union_right simp only [ancestorsSet, mem_filter, Finset.mem_univ, true_and] exact ⟨w, hwS, h⟩

lemma bbZAncestors_subset_ancestralSet_of_subset {Z S : Finset V} (hZS : Z ⊆ S) : G.bbZAncestors Z ⊆ G.ancestralSet S := by unfold bbZAncestors exact G.ancestralSet_mono hZS

lemma nonCollider_has_outgoing {l m r : V} (hadj_lm : G.UAdj l m) (hadj_mr : G.UAdj m r) (hnc : ¬ G.IsCollider l m r) : G.edge m l ∨ G.edge m r := by -- IsCollider l m r := G.edge l m ∧ G.edge r m -- ¬ collider means ¬ edge l m ∨ ¬ edge r m. -- Combined with UAdj giving edge ∨ reverse, deduce one outgoing. unfold IsCollider at hnc push_neg at hnc rcases hadj_lm with hlm | hml · -- edge l m: then ¬ edge r m (else collider). So edge m r (by UAdj m r). have hnr : ¬ G.edge r m := hnc hlm rcases hadj_mr with hmr | hrm · exact inr hmr · exact absurd hrm hnr · -- edge m l: outgoing on the left. exact inl hml

lemma mem_ancestralSet_of_edge_to_mem {u v : V} {S : Finset V} (huv : G.edge u v) (hv : v ∈ G.ancestralSet S) : u ∈ G.ancestralSet S := by rcases Finset.mem_union.mp hv with hvS | hvA · exact G.mem_ancestralSet_of_isAncestor hvS (isAncestor.edge huv) · apply mem_union_right simp only [ancestorsSet, mem_filter, Finset.mem_univ, true_and] at hvA ⊢ obtain ⟨w, hwS, hvw⟩ := hvA exact ⟨w, hwS, G.isAncestor_trans (isAncestor.edge huv) hvw⟩

theorem subset_ancestralSet_of_subset {Y S : Finset V} (hYS : Y ⊆ S) : Y ⊆ G.ancestralSet S := by intro v hvY apply G.subset_ancestralSet exact hYS hvY

theorem activeWalk_witness_subset_ancestralSet {X Y Z : Finset V} {v : V} (hvR : v ∈ G.bbReachableVertices Z X) (hvY : v ∈ Y) : ∃ (p : List V) (x : V), x ∈ X ∧ p.length ≥ 2 ∧ G.IsActiveWalk Z p ∧ p.head? = some x ∧ p.getLast? = some v ∧ ∀ w ∈ p, w ∈ G.ancestralSet (X ∪ Y ∪ Z) := by -- Pull an active walk witness from `bbReachableVertices_iff_activeWalk`, -- then apply `activeWalk_nodes_are_ancestors`. obtain ⟨x, hxX, p, hlen, hact, hhead, hlast⟩ := (G.bbReachableVertices_iff_activeWalk X Z v).mp hvR exact ⟨p, x, hxX, hlen, hact, hhead, hlast, G.activeWalk_nodes_are_ancestors hxX hvY hact hhead hlast⟩

theorem isActiveWalk_of_directed {Z : Finset V} {p : List V} (hdir : ∀ (i : ℕ) (hi : i + 1 < p.length), G.edge (p.get ⟨i, by omega⟩) (p.get ⟨i + 1, hi⟩)) (hZ : ∀ (i : ℕ) (hi : i + 2 < p.length), p.get ⟨i + 1, by omega⟩ ∉ Z) : G.IsActiveWalk Z p := by refine ⟨fun i hi => ?_, fun i hi => ?_⟩ · -- Adjacency: G.edge p[i] p[i+1] gives UAdj. exact inl (hdir i hi) · -- Non-collider: edge from p[i+1] to p[i+2], so ¬ edge p[i+2] p[i+1]. simp only have hmr : G.edge (p.get ⟨i + 1, by omega⟩) (p.get ⟨i + 2, hi⟩) := hdir (i + 1) hi have hrm_false : ¬ G.edge (p.get ⟨i + 2, hi⟩) (p.get ⟨i + 1, by omega⟩) := G.asymm hmr have hnotcoll : ¬ G.IsCollider (p.get ⟨i, by omega⟩) (p.get ⟨i + 1, by omega⟩) (p.get ⟨i + 2, hi⟩) := by intro ⟨_, h2⟩; exact hrm_false h2 rw [if_neg hnotcoll] exact hZ i hi

theorem exists_activeWalk_of_ancestor_avoiding {Z : Finset V} {u v : V} (huv : G.isAncestor u v) (huZ : u ∉ G.ancestralSet Z) : ∃ (p : List V), p.length ≥ 2 ∧ p.head? = some u ∧ p.getLast? = some v ∧ G.IsActiveWalk Z p := by obtain ⟨p, hlen, hhead, hlast, hedge, hZavoid⟩ := G.exists_directedPath_avoiding huv huZ exact ⟨p, hlen, hhead, hlast, G.isActiveWalk_of_directed hedge (fun i hi => hZavoid _ (List.get_mem _ _))⟩

theorem fork_isActiveWalk {Z : Finset V} {u x y : V} {xp yp : List V} (hxp_len : xp.length ≥ 2) (hxp_head : xp.head? = some u) (hxp_last : xp.getLast? = some x) (hxp_edge : ∀ (i : ℕ) (hi : i + 1 < xp.length), G.edge (xp.get ⟨i, by omega⟩) (xp.get ⟨i + 1, hi⟩)) (hxp_Z : ∀ z ∈ xp, z ∉ Z) (hyp_len : yp.length ≥ 2) (hyp_head : yp.head? = some u) (hyp_last : yp.getLast? = some y) (hyp_edge : ∀ (i : ℕ) (hi : i + 1 < yp.length), G.edge (yp.get ⟨i, by omega⟩) (yp.get ⟨i + 1, hi⟩)) (hyp_Z : ∀ z ∈ yp, z ∉ Z) : let p := xp.reverse ++ yp.tail p.length ≥ 2 ∧ p.head? = some x ∧ p.getLast? = some y ∧ G.IsActiveWalk Z p := by -- yp.head = u, yp.tail = yp without u have hyp_ne : yp ≠ [] := by intro h; rw [h] at hyp_len; simp at hyp_len have hxp_ne : xp ≠ [] := by intro h; rw [h] at hxp_len; simp at hxp_len have hxpRev_ne : xp.reverse ≠ [] := by simp [hxp_ne] -- yp.head hyp_ne = u have hyp_head_eq : yp.head hyp_ne = u := by have h := List.head?_eq_some_head hyp_ne rw [hyp_head] at h exact (Option.some_inj.mp h.symm) -- xp.getLast hxp_ne = x have hxp_last_eq : xp.getLast hxp_ne = x := by have h := getLast?_eq_some_getLast hxp_ne rw [hxp_last] at h exact (Option.some_inj.mp h.symm) -- xp.head hxp_ne = u have hxp_head_eq : xp.head hxp_ne = u := by have h := List.head?_eq_some_head hxp_ne rw [hxp_head] at h exact (Option.some_inj.mp h.symm) -- yp.getLast hyp_ne = y have hyp_last_eq : yp.getLast hyp_ne = y := by have h := getLast?_eq_some_getLast hyp_ne rw [hyp_last] at h exact (Option.some_inj.mp h.symm) -- yp = u :: yp.tail have hyp_decomp : yp = u :: yp.tail := by conv_lhs => rw [← List.cons_head_tail hyp_ne] rw [hyp_head_eq] -- yp.tail length = yp.length - 1 have hyp_tail_len : yp.tail.length = yp.length - 1 := List.length_tail -- yp.tail nonempty since yp.length ≥ 2 have hyp_tail_ne : yp.tail ≠ [] := by rw [← List.length_pos_iff, hyp_tail_len]; omega set p := xp.reverse ++ yp.tail with hp_def have hp_len_eq : p.length = xp.length + yp.length - 1 := by simp only [hp_def, List.length_append, List.length_reverse, hyp_tail_len] omega have hp_len : p.length ≥ 2 := by rw [hp_len_eq]; omega -- head p = head xp.reverse = last xp = x have hp_head : p.head? = some x := by simp only [hp_def, List.head?_append_of_ne_nil _ hxpRev_ne, List.head?_reverse] rw [hxp_last] -- last p = last yp.tail = last yp = y have hp_last : p.getLast? = some y := by have hlast_tail : yp.tail.getLast? = some y := by -- yp = [u] ++ yp.tail, so getLast? = yp.tail.getLast? when yp.tail ≠ []. have heq : yp = [u] ++ yp.tail := by simpa using hyp_decomp have := getLast?_append_of_ne_nil [u] hyp_tail_ne rw [← heq] at this rw [← this]; exact hyp_last simp only [hp_def, getLast?_append, hlast_tail] rfl refine ⟨hp_len, hp_head, hp_last, ?_⟩ -- Now show `IsActiveWalk Z p`. -- Layout: p[k] = xp.reverse[k] = xp[xp.length - 1 - k] for k < xp.length. -- p[k] = yp.tail[k - xp.length] = yp[k - xp.length + 1] for k ≥ xp.length. -- The seam is at k = xp.length - 1 (= u, since xp.reverse[xp.length-1] = xp[0] = u), -- and k = xp.length is yp.tail[0] = yp[1]. set R := xp.length with hR_def have hxpRev_len : xp.reverse.length = R := List.length_reverse have hp_len_eq2 : p.length = R + yp.tail.length := by simp only [hp_def, List.length_append, hxpRev_len] have hp_L : ∀ (k : ℕ) (hkR : k < R), p.get ⟨k, by rw [hp_len_eq2]; omega⟩ = xp.get ⟨R - 1 - k, by omega⟩ := by intro k hkR have hk_rev : k < xp.reverse.length := by rw [hxpRev_len]; exact hkR simp only [hp_def, List.get_eq_getElem, List.getElem_append_left (h := hk_rev), List.getElem_reverse] change xp[xp.length - 1 - k] = xp[R - 1 - k] congr 1 have hp_R : ∀ (k : ℕ) (hkL : R ≤ k) (hk : k < p.length), p.get ⟨k, hk⟩ = yp.get ⟨k - R + 1, by rw [hp_len_eq2, hyp_tail_len] at hk; omega⟩ := by intro k hkL hk have hk_rev : xp.reverse.length ≤ k := by rw [hxpRev_len]; exact hkL have htail_idx_lt : k - xp.reverse.length < yp.tail.length := by rw [hxpRev_len, hyp_tail_len] rw [hp_len_eq2, hyp_tail_len] at hk; omega have htail_yp_idx_lt : k - R + 1 < yp.length := by rw [hp_len_eq2, hyp_tail_len] at hk; omega -- yp.tail[j] = yp[j+1] via cons decomposition have hyp_tail_get : ∀ (j : ℕ) (hj1 : j < yp.tail.length) (hj2 : j + 1 < yp.length), yp.tail[j]'hj1 = yp[j + 1]'hj2 := by intro j hj1 hj2 have : yp[j + 1] = (u :: yp.tail)[j + 1]'(by rw [← hyp_decomp]; exact hj2) := by congr 1 rw [this] simp [List.getElem_cons_succ] -- Compute p.get have hpget : p.get ⟨k, hk⟩ = yp.tail[k - xp.reverse.length]'htail_idx_lt := by simp only [hp_def, List.get_eq_getElem, List.getElem_append_right hk_rev] rw [hpget] have hidx_eq : k - xp.reverse.length = k - R := by rw [hxpRev_len] rw [show yp.tail[k - xp.reverse.length]'htail_idx_lt = yp.tail[k - R]'(by rw [← hidx_eq]; exact htail_idx_lt) from by congr 1] rw [hyp_tail_get (k - R) (by rw [hyp_tail_len]; omega) htail_yp_idx_lt] simp [List.get_eq_getElem] -- xp[0] = u have hxp_get_0 : xp.get ⟨0, by omega⟩ = u := by rw [List.get_eq_getElem, List.getElem_zero] exact hxp_head_eq -- u ∉ Z (since u ∈ xp via head) have hu_notZ : u ∉ Z := by apply hxp_Z rw [← hxp_head_eq] exact List.head_mem hxp_ne refine ⟨?_, ?_⟩ · -- Adjacency: G.UAdj p[i] p[i+1] intro i hi rw [hp_len_eq2] at hi by_cases hA1 : i + 1 < R · -- A1: both in xp.reverse. Reversed-directed edge. have hiR : i < R := by omega rw [hp_L i hiR, hp_L (i + 1) hA1] have hedge_idx : R - 2 - i + 1 < R := by omega have hedge := hxp_edge (R - 2 - i) hedge_idx have heq : R - 2 - i + 1 = R - 1 - i := by omega rw [show (⟨R - 2 - i + 1, hedge_idx⟩ : Fin xp.length) = ⟨R - 1 - i, by omega⟩ from Fin.ext heq] at hedge have heq2 : R - 1 - (i + 1) = R - 2 - i := by omega rw [show (⟨R - 1 - (i + 1), by omega⟩ : Fin xp.length) = ⟨R - 2 - i, by omega⟩ from Fin.ext heq2] exact Or.inr hedge · push_neg at hA1 by_cases hA2 : i + 1 = R · -- A2: seam i = R - 1. p[R-1] = xp[0] = u. p[R] = yp.tail[0] = yp[1]. have hi_eq : i = R - 1 := by omega subst hi_eq have hiR : R - 1 < R := by omega rw [hp_L (R - 1) hiR] have hi1L : R ≤ R - 1 + 1 := by omega have hi1_lt : R - 1 + 1 < p.length := by rw [hp_len_eq2]; exact hi rw [hp_R (R - 1 + 1) hi1L hi1_lt] have h_xidx : R - 1 - (R - 1) = 0 := by omega rw [show (⟨R - 1 - (R - 1), by omega⟩ : Fin xp.length) = ⟨0, by omega⟩ from Fin.ext h_xidx] rw [hxp_get_0] have h_yidx : R - 1 + 1 - R + 1 = 1 := by omega rw [show (⟨R - 1 + 1 - R + 1, by rw [hp_len_eq2, hyp_tail_len] at hi1_lt; omega⟩ : Fin yp.length) = ⟨1, by omega⟩ from Fin.ext h_yidx] -- Goal: G.UAdj u yp[1]. Use hyp_edge at 0: G.edge yp[0] yp[1] = G.edge u yp[1]. have hedge0 := hyp_edge 0 (by omega) have hyp0 : yp.get ⟨0, by omega⟩ = u := by rw [List.get_eq_getElem, List.getElem_zero] exact hyp_head_eq rw [hyp0] at hedge0 exact inl hedge0 · -- A3: both in yp.tail. i ≥ R. have hiL : R ≤ i := by omega have hi1L : R ≤ i + 1 := by omega have hi_lt : i < p.length := by rw [hp_len_eq2]; omega have hi1_lt : i + 1 < p.length := by rw [hp_len_eq2]; exact hi rw [hp_R i hiL hi_lt, hp_R (i + 1) hi1L hi1_lt] -- Goal: G.UAdj yp[i-R+1] yp[(i+1)-R+1]. Use hyp_edge at i - R + 1. have hidx : (i - R + 1) + 1 < yp.length := by rw [hyp_tail_len] at hi; omega have hedge := hyp_edge (i - R + 1) hidx have heq : (i - R + 1) + 1 = (i + 1) - R + 1 := by omega rw [show (⟨(i - R + 1) + 1, hidx⟩ : Fin yp.length) = ⟨(i + 1) - R + 1, by omega⟩ from Fin.ext heq] at hedge exact inl hedge · -- Collider condition intro i hi rw [hp_len_eq2] at hi by_cases hC1 : i + 2 < R · -- C1: all three in xp.reverse. Reversed-directed: middle is non-collider. have hiR : i < R := by omega have hi1R : i + 1 < R := by omega rw [hp_L i hiR, hp_L (i + 1) hi1R, hp_L (i + 2) hC1] -- middle: xp[R - 1 - (i+1)] = xp[R - 2 - i]. Edge from middle to left. have h_midx : R - 1 - (i + 1) = R - 2 - i := by omega rw [show (⟨R - 1 - (i + 1), by omega⟩ : Fin xp.length) = ⟨R - 2 - i, by omega⟩ from Fin.ext h_midx] have hedge_idx : R - 2 - i + 1 < R := by omega have hedge := hxp_edge (R - 2 - i) hedge_idx have heq : R - 2 - i + 1 = R - 1 - i := by omega rw [show (⟨R - 2 - i + 1, hedge_idx⟩ : Fin xp.length) = ⟨R - 1 - i, by omega⟩ from Fin.ext heq] at hedge have hnotColl : ¬ G.IsCollider (xp.get ⟨R - 1 - i, by omega⟩) (xp.get ⟨R - 2 - i, by omega⟩) (xp.get ⟨R - 1 - (i + 2), by omega⟩) := by intro ⟨hLM, _⟩ exact G.asymm hedge hLM simp only [hnotColl, if_false] apply hxp_Z exact List.get_mem _ _ · push_neg at hC1 by_cases hC2 : i + 2 = R · -- C2: i = R - 2. Triple straddles seam: left and middle in xp.reverse, right at seam. have hi_eq : i = R - 2 := by omega subst hi_eq have hiR : R - 2 < R := by omega have hi1R : R - 2 + 1 < R := by omega have hi2L : R ≤ R - 2 + 2 := by omega have hi2_lt : R - 2 + 2 < p.length := by rw [hp_len_eq2]; exact hi rw [hp_L (R - 2) hiR, hp_L (R - 2 + 1) hi1R, hp_R (R - 2 + 2) hi2L hi2_lt] -- Middle: xp[R - 1 - (R - 2 + 1)] = xp[0] = u have h_midx : R - 1 - (R - 2 + 1) = 0 := by omega rw [show (⟨R - 1 - (R - 2 + 1), by omega⟩ : Fin xp.length) = ⟨0, by omega⟩ from Fin.ext h_midx] rw [hxp_get_0] -- Non-collider: edge from u to xp[1] (hxp_edge at 0), so ¬ edge xp[1] u. have hedge := hxp_edge 0 (by omega) rw [hxp_get_0] at hedge have h_lidx : R - 1 - (R - 2) = 1 := by omega rw [show (⟨R - 1 - (R - 2), by omega⟩ : Fin xp.length) = ⟨1, by omega⟩ from Fin.ext h_lidx] have hnotColl : ¬ G.IsCollider (xp.get ⟨1, by omega⟩) u (yp.get ⟨R - 2 + 2 - R + 1, by rw [hp_len_eq2, hyp_tail_len] at hi2_lt; omega⟩) := by intro ⟨hLM, _⟩ exact G.asymm hedge hLM simp only [hnotColl, if_false] exact hu_notZ · by_cases hC3 : i + 1 = R · -- C3: seam at middle. i = R - 1. -- Triple: xp.reverse[R-1] = u, yp.tail[0] = yp[1], yp.tail[1] = yp[2]. -- … truncated; follow the source link for the rest …

lemma not_isAncestor_of_root' {r : V} (hr : ∀ u, ¬ G.edge u r) (u : V) : ¬ G.isAncestor u r := by intro h cases h with | edge he => exact hr _ he | trans _ he => exact hr _ he

theorem ancestralSet_idem {V : Type*} [DecidableEq V] [Fintype V] (G : DAG V) (S : Finset V) : G.ancestralSet (G.ancestralSet S) = G.ancestralSet S := by apply Finset.Subset.antisymm · intro u hu rw [ancestralSet, mem_union] at hu rcases hu with hu | hu · exact hu · rw [ancestorsSet, mem_filter] at hu obtain ⟨_, v, hv, huv⟩ := hu rw [ancestralSet, mem_union] at hv rcases hv with hvS | hvAnc · exact G.mem_ancestralSet_of_isAncestor hvS huv · rw [ancestorsSet, mem_filter] at hvAnc obtain ⟨_, w, hwS, hvw⟩ := hvAnc exact G.mem_ancestralSet_of_isAncestor hwS (G.isAncestor_trans huv hvw) · exact G.subset_ancestralSet (G.ancestralSet S)

lemma not_mem_fixed_of_mem_observed {v : SWIGNode N} (hv : v ∈ G.observed) : v ∉ G.fixed := by intro hfix obtain ⟨n, hn⟩ := G.fixed_is_fixed v hfix obtain ⟨m, hm⟩ := G.observed_is_random v hv rw [hn] at hm cases hm

lemma activeWalk_node_not_fixed {R X Y Z : Finset (SWIGNode N)} {x y v : SWIGNode N} {p : List (SWIGNode N)} (hX : X ⊆ R ∩ G.observed) (hY : Y ⊆ R ∩ G.observed) (hxX : x ∈ X) (hyY : y ∈ Y) (hact : G.dag.IsActiveWalk (Z ∪ G.fixed) p) (hhead : p.head? = some x) (hlast : p.getLast? = some y) (hv : v ∈ p) : v ∉ G.fixed := by rw [List.mem_iff_get] at hv obtain ⟨i, rfl⟩ := hv by_cases hi0 : i.val = 0 · have hpne : p ≠ [] := by intro hp simp [hp] at hhead have hhead_get : p.get ⟨0, by omega⟩ = x := by have h := List.head?_eq_some_head hpne rw [h] at hhead have hx_eq : p.head hpne = x := Option.some_inj.mp hhead rw [← hx_eq] simp [List.head_eq_getElem hpne] have hidx : i = ⟨0, by omega⟩ := Fin.ext hi0 rw [hidx, hhead_get] exact G.not_mem_fixed_of_mem_observed (Finset.mem_inter.mp (hX hxX)).2 · by_cases hilast : i.val = p.length - 1 · have hpne : p ≠ [] := by intro hp simp [hp] at hlast have hlast_get : p.get ⟨p.length - 1, by omega⟩ = y := by have h := getLast?_eq_some_getLast hpne rw [h] at hlast have hy_eq : p.getLast hpne = y := Option.some_inj.mp hlast rw [← hy_eq] exact (List.getLast_eq_getElem hpne).symm have hidx : i = ⟨p.length - 1, by omega⟩ := Fin.ext hilast rw [hidx, hlast_get] exact G.not_mem_fixed_of_mem_observed (Finset.mem_inter.mp (hY hyY)).2 · have htri : (i.val - 1) + 2 < p.length := by omega have hclause := hact.2 (i.val - 1) htri have hrew₁ : i.val - 1 + 1 = i.val := by omega simp only [hrew₁] at hclause set l := p.get ⟨i.val - 1, by omega⟩ with hl set m := p.get ⟨i.val, i.isLt⟩ with hm set r := p.get ⟨i.val - 1 + 2, htri⟩ with hr by_cases hcoll : G.dag.IsCollider l m r · rw [if_pos hcoll] at hclause intro hmfix have hpar : l ∈ G.dag.parents m := G.dag.mem_parents.mpr hcoll.1 have hroot := G.fixed_are_roots m hmfix simp [hroot] at hpar · rw [if_neg hcoll] at hclause intro hmfix exact hclause (mem_union_right _ hmfix)