Graph.DSep
d-separation on directed acyclic graphs: the Bayes-Ball characterization, ancestral closures, moralization bridges, and equivalences between the criteria.
BayesBall 8 core · 7 supporting This file implements the Bayes Ball reachability computation for finite directed acyclic graphs. ★ bbReachable_minimal
Bayes Ball Reachability
This file implements the Bayes Ball reachability computation for finite directed acyclic graphs. Given source and conditioning sets, it tracks directed arrival states and returns the vertices reachable along paths that remain active under the conditioning information.
The core definitions are BBDir, BBState, bbZAncestors, one-step transition
bbStep, initial frontier bbInit, reachable state set bbReachable, and
vertex projection bbReachableVertices. The exposed invariants include source
monotonicity (bbReachable_mono_source,
bbReachableVertices_mono_source), minimality of the fixed point, and closure of
reachable states under bbStep.
inductive BBDir reviewed
⚑ flagged
Causalean.DAG
Direction from which a node is visited in the Bayes Ball algorithm: arrival from a parent (fromParent) or arrival from a child (fromChild).
Definition (Lean source)
abbrev BBState reviewed
⚑ flagged
Causalean.DAG
A Bayes Ball state: a vertex paired with arrival direction.
def bbZAncestors reviewed
⚑ flagged
Causalean.DAG
The set of vertices in Z together with all ancestors of Z. A collider is "activated" iff it or a descendant is in Z.
Definition (Lean source)
def bbStep reviewed
⚑ flagged
Causalean.DAG
One step of the Bayes Ball algorithm from state (w, dir).
Definition (Lean source)
def bbStep (Z : Finset V) (s : BBState V) : Finset (BBState V) :=
let (w, dir) := s
match dir with
| BBDir.fromChild =>
if w ∈ Z then
∅
else
(G.parents w).map
⟨(·, BBDir.fromChild), fun _ _ h => by simpa using h⟩ ∪
(G.children w).map
⟨(·, BBDir.fromParent), fun _ _ h => by simpa using h⟩
| BBDir.fromParent =>
if w ∉ Z then
(G.children w).map
⟨(·, BBDir.fromParent), fun _ _ h => by simpa using h⟩ ∪
if w ∈ G.bbZAncestors Z then
(G.parents w).map
⟨(·, BBDir.fromChild), fun _ _ h => by simpa using h⟩
else ∅
else
(G.parents w).map
⟨(·, BBDir.fromChild), fun _ _ h => by simpa using h⟩
def bbInit reviewed
⚑ flagged
Causalean.DAG
Initial BFS frontier from a source set X: for each x ∈ X, include all children of x in direction fromParent and all parents of x in direction fromChild. These are the states a "ball" passing through x can occupy.
def bbReachable reviewed
⚑ flagged
Causalean.DAG
The set of Bayes Ball states reachable from source vertices X given conditioning set Z.
Definition (Lean source)
def bbReachable (Z X : Finset V) : Finset (BBState V) :=
bbReachAux G Z (G.bbInit X) (G.bbInit X) (2 * card V + 1)
def bbReachableVertices reviewed
⚑ flagged
Causalean.DAG
Vertices reachable from X via Bayes Ball (ignoring direction).
Definition (Lean source)
theorem bbReachable_minimal reviewed
⚑ flagged
Causalean.DAG
bbReachable Z X is the least superset of bbInit X closed under bbStep Z: for a conditioning set Z and source set X, if a candidate set S of Bayes-Ball states contains the initial frontier bbInit X and S is closed under the Bayes-Ball step relation bbStep Z, then S contains every state reachable via bbReachable Z X.
Formal statement
Proof (Lean source)
theorem bbReachable_minimal (Z X : Finset V) (S : Finset (BBState V))
(hinit : G.bbInit X ⊆ S)
(hstep : ∀ s ∈ S, G.bbStep Z s ⊆ S) :
G.bbReachable Z X ⊆ S := by
unfold bbReachable
refine bbReachAux_closed G Z _ hinit hinit ?_
intro x hx
rw [Finset.mem_biUnion] at hx
obtain ⟨s, hs, hxs⟩ := hx
exact hstep s hs hxs
7 supporting declarations (lemmas, instances)
-
instDecidableEqBBDirinstancederiving DecidableEq, Repr -
instReprBBDirinstancederiving DecidableEq, Repr -
bbReachable_mono_sourcetheorem — Bayes Ball reachability is monotone in the source set.hypothesesconclusionG.bbReachable Z X' ⊆ G.bbReachable Z XProof (Lean source)
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') _ -
bbReachableVertices_mono_sourcetheorem — Bayes Ball reachable vertices are monotone in the source set.hypothesesconclusionG.bbReachableVertices Z X' ⊆ G.bbReachableVertices Z XProof (Lean source)
theorem bbReachableVertices_mono_source {Z : Finset V} {X X' : Finset V} (hXX' : X' ⊆ X) : G.bbReachableVertices Z X' ⊆ G.bbReachableVertices Z X := Finset.image_subset_image (G.bbReachable_mono_source hXX') -
bbReachable_init_subsettheorem — The initial BFS frontier bbInit X is contained in bbReachable Z X.Proof (Lean source)
theorem bbReachable_init_subset (Z X : Finset V) : G.bbInit X ⊆ G.bbReachable Z X := by unfold bbReachable exact visited_sub_bbReachAux G Z (G.bbInit X) (G.bbInit X) _ -
bbReachable_bbStep_subsettheorem — bbReachable Z X is closed under bbStep Z. If s ∈ bbReachable Z X, then every state produced by bbStep Z s is also in bbReachable Z X.hypothesesconclusionG.bbStep Z s ⊆ G.bbReachable Z XProof (Lean source)
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
ActivePath 6 core · 14 supporting This file defines active paths in directed acyclic graphs relative to a conditioning set. ★ IsActivePath★ bbReachableVertices_iff_activePath
Active Paths
This file defines active paths in directed acyclic graphs relative to a
conditioning set. It records undirected adjacency (UAdj), collider triples
(IsCollider), path activity (IsActivePath), and active-path existence between
sets (HasActivePath).
The main path lemmas prove reversal symmetry (isActivePath_reverse,
hasActivePath_symm), directed-path activity helpers, suffix extraction for
source-to-conditioning transfer, and the Bayes Ball correctness theorem
bbReachableVertices_iff_activePath, which identifies computed reachability
with existence of an active path.
def UAdj reviewed
⚑ flagged
Causalean.DAG
An undirected edge in the DAG: either G.edge u v or G.edge v u.
Definition (Lean source)
def UAdj (u v : V) : Prop := G.edge u v ∨ G.edge v u
def IsCollider reviewed
⚑ flagged
Causalean.DAG
Whether vertex m is a collider on the triple (l, m, r): both edges point toward m, i.e., G.edge l m ∧ G.edge r m.
Definition (Lean source)
def IsCollider (l m r : V) : Prop := G.edge l m ∧ G.edge r m
def IsActivePath reviewed
⚑ flagged
Causalean.DAG
A path (list of vertices) is active (unblocked) given conditioning set Z if: - consecutive vertices are undirected-adjacent - for every intermediate triple (pᵢ, pᵢ₊₁, pᵢ₊₂): - if pᵢ₊₁ is a collider: pᵢ₊₁ ∈ G.bbZAncestors Z - if pᵢ₊₁ is not a collider: pᵢ₊₁ ∉ Z
Definition (Lean source)
def IsActivePath (Z : Finset V) (p : List V) : Prop :=
-- All consecutive pairs are adjacent
(∀ (i : ℕ) (hi : i + 1 < p.length),
G.UAdj (p.get ⟨i, by omega⟩) (p.get ⟨i + 1, hi⟩)) ∧
-- All intermediate vertices satisfy the collider/non-collider condition
(∀ (i : ℕ) (hi : i + 2 < p.length),
let l := p.get ⟨i, by omega⟩
let m := p.get ⟨i + 1, by omega⟩
let r := p.get ⟨i + 2, hi⟩
if G.IsCollider l m r then m ∈ G.bbZAncestors Z else m ∉ Z)
def HasActivePath reviewed
⚑ flagged
Causalean.DAG
There exists an active path from some vertex in X to some vertex in Y.
Definition (Lean source)
def HasActivePath (X Y Z : Finset V) : Prop :=
∃ (p : List V), p.length ≥ 2 ∧
G.IsActivePath Z p ∧
p.head? ∈ (X.image some) ∧
p.getLast? ∈ (Y.image some)
def lastIdxLt reviewed
⚑ flagged
Causalean.DAG
Largest i < n satisfying a decidable predicate P, if any.
theorem bbReachableVertices_iff_activePath reviewed
⚑ flagged
Causalean.DAG
Bayes Ball correctness. For a source vertex set X and a conditioning vertex set Z and a vertex v, v lies in the breadth-first-search reachable set bbReachableVertices Z X if and only if there is an active path, given Z, from some vertex of X to v.
Formal statement
Proof (Lean source)
theorem bbReachableVertices_iff_activePath (X Z : Finset V) (v : V) :
v ∈ G.bbReachableVertices Z X ↔
∃ (x : V), x ∈ X ∧ ∃ (p : List V), p.length ≥ 2 ∧
G.IsActivePath Z p ∧ p.head? = some x ∧ p.getLast? = some v := by
constructor
· intro hv
rw [bbReachableVertices] at hv
obtain ⟨s, hs, hsv⟩ := Finset.mem_image.mp hv
rcases s with ⟨w, d⟩
change w = v at hsv
subst w
obtain ⟨x, hxX, u, r, _hdir, hact, hlast⟩ :=
G.bbReachable_state_has_reverse_activePath X Z hs
refine ⟨x, hxX, (v :: u :: r).reverse, ?_, ?_, ?_, ?_⟩
· simp
· exact G.isActivePath_reverse hact
· rwa [List.head?_reverse]
· rw [getLast?_reverse]
rfl
· rintro ⟨x, hxX, p, hlen, hact, hhead, hlast⟩
cases p with
| nil =>
simp at hlen
| cons a p' =>
cases p' with
| nil =>
simp at hlen
| cons b r =>
simp only [List.head?_cons] at hhead
injection hhead with ha
subst a
exact G.bbReachableVertices_of_activePath_cons hxX hact hlast
14 supporting declarations (lemmas, instances)
-
decIsColliderinstance — Collider status of a triple is decidable whenever the directed edge relation is decidable.instance decIsCollider (l m r : V) : Decidable (G.IsCollider l m r) := inferInstanceAs (Decidable (_ ∧ _)) -
UAdj_symmtheorem — Undirected adjacency is symmetric: if two vertices are adjacent, they remain adjacent in the opposite order.hypothesesu v :Vh :G.UAdj u vconclusionG.UAdj v uProof (Lean source)
theorem UAdj_symm {u v : V} (h : G.UAdj u v) : G.UAdj v u := Or.comm.mp h -
isActivePath_reversetheorem — Active paths are symmetric: reversing an active path is also active.Proof (Lean source)
theorem isActivePath_reverse {Z : Finset V} {p : List V} (h : G.IsActivePath Z p) : G.IsActivePath 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 -
isActivePath_of_reversed_directedtheorem — A backward-directed path whose interior vertices avoid the conditioning set is active.hypothesesZ :Finset Vp :List Vhdir :∀ (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⟩ ∉ ZconclusionG.IsActivePath Z pProof (Lean source)
theorem isActivePath_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.IsActivePath 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 -
lastIdxLt_eq_sometheorem — If the last index below a bound exists, it is below the bound, satisfies the predicate, and no larger index below the bound satisfies it.hypothesesconclusioni < n ∧ P i ∧ ∀ j, i < j → j < n → ¬ P jProof (Lean source)
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 -
lastIdxLt_eq_nonetheorem — If there is no last index below a bound satisfying a predicate, then no index below the bound satisfies the predicate.hypothesesconclusion∀ iifi < nthen¬ P iProof (Lean source)
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 -
take_suffix_at_last_Stheorem — Suffix-step for source-to-cond transfer.hypothesesX Z S :Finset Vp :List Vx w :VhxX :x ∈ Xhlen :p.length ≥ 2hact :G.IsActivePath (Z ∪ S) phhead :p.head? = some xhlast :p.getLast? = some wconclusion∃ (x' : V) (q : List V),x' ∈ X ∪ S ∧q.length ≥ 2 ∧G.IsActivePath (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)Proof (Lean source)
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.IsActivePath (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.IsActivePath (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.IsActivePath (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⟩ -
isActivePath_Z_of_no_S_only_collidertheorem — If q is active given Z ∪ S and every interior collider of q is Z-activated (not merely S-activated), then q is active given Z alone.hypothesesZ S :Finset Vq :List Vhact :G.IsActivePath (Z ∪ S) qhNoSOnly :∀ (i : ℕ) (hi : i + 2 < q.length)ifG.IsCollider (q.get ⟨i, by omega⟩) (q.get ⟨i + 1, by omega⟩) (q.get ⟨i + 2, hi⟩)thenq.get ⟨i + 1, by omega⟩ ∈ G.bbZAncestors ZconclusionG.IsActivePath Z qProof (Lean source)
theorem isActivePath_Z_of_no_S_only_collider {Z S : Finset V} {q : List V} (hact : G.IsActivePath (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.IsActivePath 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) -
hasActivePath_symmtheorem — HasActivePath is symmetric in X and Y.Proof (Lean source)
theorem hasActivePath_symm (X Y Z : Finset V) : G.HasActivePath X Y Z → G.HasActivePath Y X Z := by rintro ⟨p, hlen, hact, hhead, hlast⟩ refine ⟨p.reverse, ?_, G.isActivePath_reverse hact, ?_, ?_⟩ · simp only [List.length_reverse]; exact hlen · rwa [List.head?_reverse] · rwa [getLast?_reverse] -
isActivePath_cons_of_active_tripletheorem — Prepending an active triple to an active path keeps the path active.hypothesesZ :Finset Vz w u :Vr :List Vhadj :G.UAdj z whtri :if G.IsCollider z w u then w ∈ G.bbZAncestors Z else w ∉ Zhact :G.IsActivePath Z (w :: u :: r)conclusionG.IsActivePath Z (z :: w :: u :: r)Proof (Lean source)
theorem isActivePath_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.IsActivePath Z (w :: u :: r)) : G.IsActivePath 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 -
active_triple_swap_outertheorem — The active-path condition at a three-vertex segment is unchanged when its two outer vertices are swapped.hypothesesconclusionif G.IsCollider z w u then w ∈ G.bbZAncestors Z else w ∉ ZProof (Lean source)
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 -
isActivePath_pairtheorem — Any two adjacent vertices form an active path of length one for every conditioning set.Proof (Lean source)
theorem isActivePath_pair {Z : Finset V} {a b : V} (h : G.UAdj a b) : G.IsActivePath 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 -
isActivePath_cons_tailtheorem — Removing the first vertex from an active path leaves an active path.hypothesesconclusionG.IsActivePath Z (w :: r)Proof (Lean source)
theorem isActivePath_cons_tail {Z : Finset V} {u w : V} {r : List V} (h : G.IsActivePath Z (u :: w :: r)) : G.IsActivePath 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'
Separation 4 core · 11 supporting This file defines d-separation in a finite directed acyclic graph as pairwise disjointness of the query sets together with absence of Bayes Ball reachability from the source set to the target set given a conditioning set ★ dSep★ dSep_source_to_cond★ dSep_mono_conditioningSet★ dSep_symm
d-Separation
This file defines d-separation in a finite directed acyclic graph as pairwise
disjointness of the query sets together with absence of Bayes Ball reachability
from the source set to the target set given a conditioning set. It proves
structural properties used by the global Markov and identification layers:
monotonicity in source and target sets, the union rule for collider-activation
ancestors (bbZAncestors_union_eq), directed-path extraction avoiding a
conditioning set, source-to-conditioning transfer (dSep_source_to_cond),
transfer to edge subgraphs (dSep_mono_conditioningSet), and symmetry.
def dSep reviewed
⚑ flagged
Causalean.DAG
The source, target, and conditioning sets are d-separated when they are pairwise disjoint and no target vertex is Bayes-Ball-reachable from the source set after conditioning.
theorem dSep_source_to_cond reviewed
⚑ flagged
Causalean.DAG
Source-to-conditioning transfer for d-separation. If X and S are disjoint and X ∪ S and Y are d-separated by Z, then X and Y remain d-separated once S is moved into the conditioning set: G.dSep X Y (Z ∪ S). Equivalently: bbReachableVertices (Z ∪ S) X is a subset of bbReachableVertices Z (X ∪ S).
Formal statement
Proof (Lean source)
theorem dSep_source_to_cond {X Y Z S : Finset V}
(hXS : Disjoint X S) (h : G.dSep (X ∪ S) Y Z) : G.dSep X Y (Z ∪ S) := by
rcases h with ⟨hXUSY, hXUSZ, hYZ, hReach⟩
refine ⟨?_, ?_, ?_, ?_⟩
· exact Disjoint.mono_left (subset_union_left (s₁ := X) (s₂ := S)) hXUSY
· rw [Finset.disjoint_left]
intro v hvX hvZS
rcases Finset.mem_union.mp hvZS with hvZ | hvS
· exact Finset.disjoint_left.mp hXUSZ (mem_union_left S hvX) hvZ
· exact Finset.disjoint_left.mp hXS hvX hvS
· rw [Finset.disjoint_left]
intro v hvY hvZS
rcases Finset.mem_union.mp hvZS with hvZ | hvS
· exact Finset.disjoint_left.mp hYZ hvY hvZ
· exact Finset.disjoint_left.mp hXUSY (mem_union_right X hvS) hvY
· refine Disjoint.mono_left ?_ hReach
intro w hw
rw [G.bbReachableVertices_iff_activePath] at hw ⊢
obtain ⟨x, hxX, p, hlen, hact, hhead, hlast⟩ := hw
obtain ⟨x', p', hx'XS, hlen', hact', hhead', hlast'⟩ :=
G.activePath_transfer_cond_to_source (X := X) (S := S)
hxX hlen hact hhead hlast
exact ⟨x', hx'XS, p', hlen', hact', hhead', hlast'⟩
theorem dSep_mono_conditioningSet reviewed
⚑ flagged
Causalean.DAG
d-separation transfers from a supergraph to a subgraph. For DAGs G and G' on the same vertex set, if every edge of G' is also an edge of G — G' is obtained from G by removing edges — and X and Y are d-separated by Z in G, then X and Y are also d-separated by Z in G'.
Formal statement
Proof (Lean source)
theorem dSep_mono_conditioningSet {X Y Z : Finset V}
(G' : DAG V)
(hEdge : ∀ u v : V, G'.edge u v → G.edge u v)
(h : G.dSep X Y Z) : G'.dSep X Y Z := by
rcases h with ⟨hXY, hXZ, hYZ, hReach⟩
refine ⟨hXY, hXZ, hYZ, ?_⟩
refine Disjoint.mono_left ?_ hReach
intro v hv
rw [G'.bbReachableVertices_iff_activePath] at hv
rw [G.bbReachableVertices_iff_activePath]
obtain ⟨x, hxX, p, hlen, hact, hhead, hlast⟩ := hv
exact ⟨x, hxX, p, hlen, G.isActivePath_mono_edge G' hEdge hact, hhead, hlast⟩
theorem dSep_symm reviewed
⚑ flagged
Causalean.DAG
d-separation is symmetric. For three finite vertex sets X, Y, Z, if X is d-separated from Y given Z then Y is d-separated from X given Z.
Formal statement
Proof (Lean source)
theorem dSep_symm (X Y Z : Finset V) (h : G.dSep X Y Z) :
G.dSep Y X Z := by
rcases h with ⟨hXY, hXZ, hYZ, hReach⟩
refine ⟨hXY.symm, hYZ, hXZ, ?_⟩
rw [Finset.disjoint_left] at hReach ⊢
intro v hv hX
-- v ∈ bbReachableVertices Z Y and v ∈ X
-- By BFS correctness, there is an active path from some y ∈ Y to v
rw [bbReachableVertices_iff_activePath] at hv
obtain ⟨y, hy, p, hlen, hact, hhead, hlast⟩ := hv
-- Reverse the path: active path from v to y
have hact' := G.isActivePath_reverse hact
-- y is reachable from v ∈ X via the reversed active path, so y ∈ bbReachableVertices Z X
have hyReach : y ∈ G.bbReachableVertices Z X := by
rw [bbReachableVertices_iff_activePath]
exact ⟨v, hX, p.reverse, by simp only [List.length_reverse]; exact hlen,
hact', by rwa [List.head?_reverse], by rwa [getLast?_reverse]⟩
-- But h says nothing in bbReachableVertices Z X is in Y, contradicting y ∈ Y
exact hReach hyReach hy
11 supporting declarations (lemmas, instances)
-
dSep_subset_lefttheorem — d-separation is monotone in X: smaller source sets preserve d-separation.Proof (Lean source)
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⟩ -
dSep_subset_righttheorem — d-separation is monotone in Y: shrinking the target set preserves d-separation.Proof (Lean source)
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⟩ -
bbZAncestors_union_eqtheorem — Ancestral-set distributes over union.Proof (Lean source)
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⟩ -
exists_directedPath_avoidingtheorem — If u is an ancestor of v and u ∉ ancestralSet Z, there is a list u = p₀, p₁, …, pₖ = v (k ≥ 1) of directed edges all avoiding Z.hypothesesconclusion∃ (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)Proof (Lean source)
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 [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 [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') -
activePath_transfer_cond_to_sourcetheorem — An active path under an enlarged conditioning set can be replaced by an active path whose source may additionally come from the newly conditioned vertices.hypothesesX Z S :Finset Vp :List Vx w :VhxX :x ∈ Xhlen :p.length ≥ 2hact :G.IsActivePath (Z ∪ S) phhead :p.head? = some xhlast :p.getLast? = some wconclusion∃ (x' : V) (p' : List V),x' ∈ X ∪ S ∧p'.length ≥ 2 ∧G.IsActivePath Z p' ∧p'.head? = some x' ∧p'.getLast? = some wProof (Lean source)
theorem activePath_transfer_cond_to_source {X Z S : Finset V} {p : List V} {x w : V} (hxX : x ∈ X) (hlen : p.length ≥ 2) (hact : G.IsActivePath (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.IsActivePath 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, 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.IsActivePath 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-PATH 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, 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 rw [hqP_len_eq]; exact hi rw [hqP_R (r.length - 1 + 1) hi1L hi1_lt] -- Goal: G.UAdj r[R-1-(R-1)] q[j_star+2+((R-1+1)-R)] after simplification. -- Simplify indices -- … truncated; follow the source link for the rest … -
isAncestor_mono_edgetheorem — If every directed edge of one graph is also an edge of another graph, every ancestor relation in the first graph also holds in the second graph.hypothesesconclusionG.isAncestor u vProof (Lean source)
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) -
bbZAncestors_mono_edgetheorem — Adding directed edges can only enlarge the set of vertices that are ancestors of the conditioning set and can activate colliders.hypothesesconclusionG'.bbZAncestors Z ⊆ G.bbZAncestors ZProof (Lean source)
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⟩ -
uAdj_mono_edgetheorem — If every directed edge of one graph is also an edge of another graph, vertices adjacent in the first graph are also adjacent in the second graph.hypothesesconclusionG.UAdj u vProof (Lean source)
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) -
isCollider_of_supergraphtheorem — If every edge of one graph is also an edge of another, a collider in the larger graph remains a collider in the smaller graph whenever its two adjacent pairs are present there.hypothesesG' :DAG VhEdge :∀ u v : VifG'.edge u vthenG.edge u vl m r :Vhadj_lm :G'.UAdj l mhadj_mr :G'.UAdj m rhcoll :G.IsCollider l m rconclusionG'.IsCollider l m rProof (Lean source)
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' -
isActivePath_mono_edgetheorem — An active path in a graph with fewer edges remains active when those edges are restored, so path witnesses transfer across graph transformations.hypothesesG' :DAG VhEdge :∀ u v : VifG'.edge u vthenG.edge u vZ :Finset Vp :List Vh :G'.IsActivePath Z pconclusionG.IsActivePath Z pProof (Lean source)
theorem isActivePath_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'.IsActivePath Z p) : G.IsActivePath 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
Ancestral 2 core · 11 supporting This file proves that active paths relevant to a d-separation query can be restricted to the ancestral set of the source, target, and conditioning vertices. ★ activePath_nodes_are_ancestors★ ancestralSet_inter_subset_ancestralSet_of_dSep
Ancestral Reduction for d-Separation
This file proves that active paths relevant to a d-separation query can be restricted to the ancestral set of the source, target, and conditioning vertices. The resulting finset lemmas distinguish the trivial reachable-target endpoint inclusion from the stronger statement about all nodes on a witnessing active path.
theorem activePath_nodes_are_ancestors reviewed
⚑ flagged
Causalean.DAG
Active-path nodes lie in the ancestral set. For finite vertex sets X, Y, Z, consider a path p that is active given Z running from a node x in X to a node y in Y. Then every vertex on p lies in the ancestral set of X ∪ Y ∪ Z. This is the main classical lemma used to justify ancestral reduction of d-separation.
Formal statement
Proof (Lean source)
theorem activePath_nodes_are_ancestors
{X Y Z : Finset V} {x y : V} {p : List V}
(hxX : x ∈ X) (hyY : y ∈ Y)
(hp : G.IsActivePath Z p)
(hhead : p.head? = some x) (hlast : p.getLast? = some y) :
∀ v ∈ p, v ∈ G.ancestralSet (X ∪ Y ∪ Z) := by
intro v hv
-- Convert `v ∈ p` to an index witness, then invoke `walk_forward_witness`.
rw [List.mem_iff_get] at hv
obtain ⟨i, hieq⟩ := hv
rw [← hieq]
exact G.walk_forward_witness hxX hyY hp hhead hlast i.val i.isLt
theorem ancestralSet_inter_subset_ancestralSet_of_dSep reviewed
⚑ flagged
Causalean.DAG
Ancestral intersection from reachability separation. If X and Y are disjoint and no vertex of Y is Bayes-Ball-reachable from X given Z, then any vertex lying in both the ancestral closure of X and the ancestral closure of Y also lies in the ancestral closure of Z.
Formal statement
Proof (Lean source)
theorem ancestralSet_inter_subset_ancestralSet_of_dSep
{X Y Z : Finset V} (hXY : Disjoint X Y)
(hReach : Disjoint (G.bbReachableVertices Z X) Y) :
G.ancestralSet X ∩ G.ancestralSet Y ⊆ G.ancestralSet Z := by
intro u hu
rw [mem_inter] at hu
obtain ⟨huX, huY⟩ := hu
-- Proceed by contradiction.
by_contra huZ
-- Unfold membership in ancestralSet for each side.
have huX' : u ∈ X ∨ ∃ x ∈ X, G.isAncestor u x := by
simp only [ancestralSet, mem_union, ancestorsSet,
mem_filter, Finset.mem_univ, true_and] at huX
rcases huX with h | ⟨x, hxX, hax⟩
· exact inl h
· exact inr ⟨x, hxX, hax⟩
have huY' : u ∈ Y ∨ ∃ y ∈ Y, G.isAncestor u y := by
simp only [ancestralSet, mem_union, ancestorsSet,
mem_filter, Finset.mem_univ, true_and] at huY
rcases huY with h | ⟨y, hyY, hay⟩
· exact inl h
· exact inr ⟨y, hyY, hay⟩
-- Convert dSep to: no active path from X to Y given Z.
have hNoPath : ∀ (x y : V), x ∈ X → y ∈ Y →
¬ ∃ (p : List V), p.length ≥ 2 ∧ G.IsActivePath Z p ∧
p.head? = some x ∧ p.getLast? = some y := by
intro x y hxX hyY ⟨p, hlen, hact, hhead, hlast⟩
-- y ∈ bbReachableVertices Z X, but dSep says it's disjoint from Y.
have hyR : y ∈ G.bbReachableVertices Z X := by
rw [G.bbReachableVertices_iff_activePath]
exact ⟨x, hxX, p, hlen, hact, hhead, hlast⟩
exact (Finset.disjoint_left.mp hReach) hyR hyY
-- Build the active path. Three cases on (huX', huY').
rcases huX' with hxIs | ⟨x, hxX, hax⟩
· -- u ∈ X. Use directed path u → ... → y for some y ∈ Y.
rcases huY' with hyIs | ⟨y, hyY, hay⟩
· -- u ∈ X ∩ Y, contradicting disjointness.
exact absurd hyIs ((Finset.disjoint_left.mp hXY) hxIs)
· obtain ⟨p, hplen, hphead, hplast, hpact⟩ :=
G.exists_activePath_of_ancestor_avoiding hay huZ
exact hNoPath u y hxIs hyY ⟨p, hplen, hpact, hphead, hplast⟩
· -- u is a strict ancestor of x ∈ X.
obtain ⟨xp, hxp_len, hxp_head, hxp_last, hxp_edge, hxp_Z⟩ :=
G.exists_directedPath_avoiding hax huZ
rcases huY' with hyIs | ⟨y, hyY, hay⟩
· -- u ∈ Y. The directed path xp (u → ... → x) is itself an active path
-- from u to x; reverse it via the public `isActivePath_reverse`.
have hxp_act_fwd : G.IsActivePath Z xp :=
G.isActivePath_of_directed hxp_edge (fun i hi => hxp_Z _ (List.get_mem _ _))
have hxp_act : G.IsActivePath Z xp.reverse := G.isActivePath_reverse hxp_act_fwd
have hxp_rev_len : xp.reverse.length ≥ 2 := by
rw [List.length_reverse]; exact hxp_len
have hxp_rev_head : xp.reverse.head? = some x := by
rw [List.head?_reverse]; exact hxp_last
have hxp_rev_last : xp.reverse.getLast? = some u := by
rw [getLast?_reverse]; exact hxp_head
exact hNoPath x u hxX hyIs ⟨xp.reverse, hxp_rev_len, hxp_act, hxp_rev_head, hxp_rev_last⟩
· -- u is a strict ancestor of both x ∈ X and y ∈ Y. Build the fork.
obtain ⟨yp, hyp_len, hyp_head, hyp_last, hyp_edge, hyp_Z⟩ :=
G.exists_directedPath_avoiding hay huZ
obtain ⟨hp_len, hp_head, hp_last, hp_act⟩ :=
G.fork_isActivePath hxp_len hxp_head hxp_last hxp_edge hxp_Z
hyp_len hyp_head hyp_last hyp_edge hyp_Z
exact hNoPath x y hxX hyY ⟨_, hp_len, hp_act, hp_head, hp_last⟩
11 supporting declarations (lemmas, instances)
-
subset_ancestralSetlemma — S ⊆ ancestralSet S: every member is in its own ancestral set.Proof (Lean source)
lemma subset_ancestralSet (S : Finset V) : S ⊆ G.ancestralSet S := by intro v hv exact mem_union_left _ hv -
ancestralSet_monolemma — ancestralSet is monotone in its argument.Proof (Lean source)
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⟩) -
mem_ancestralSet_of_isAncestorlemma — If u is an ancestor of some vertex w ∈ S, then u ∈ ancestralSet S.Proof (Lean source)
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⟩ -
bbZAncestors_subset_ancestralSet_of_subsetlemma — bbZAncestors Z ⊆ ancestralSet S whenever Z ⊆ S. Used to lift a collider-activation witness m ∈ bbZAncestors Z into the larger ancestralSet (X ∪ Y ∪ Z).Proof (Lean source)
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 -
nonCollider_has_outgoinglemma — A non-collider triple (l, m, r) has at least one outgoing edge from m.hypothesesl m r :Vhadj_lm :G.UAdj l mhadj_mr :G.UAdj m rhnc :¬ G.IsCollider l m rconclusionG.edge m l ∨ G.edge m rProof (Lean source)
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 -
mem_ancestralSet_of_edge_to_memlemma — When a directed edge points to a vertex in the ancestral closure of a set, its source vertex is also in that ancestral closure.hypothesesconclusionu ∈ G.ancestralSet SProof (Lean source)
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⟩ -
subset_ancestralSet_of_subsettheorem — Every element of a subset belongs to the ancestral closure of its ambient set.Proof (Lean source)
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 -
activePath_witness_subset_ancestralSettheorem — Active-path inner nodes lie in the ancestral set (informative form).hypothesesconclusion∃ (p : List V) (x : V),x ∈ X ∧p.length ≥ 2 ∧G.IsActivePath Z p ∧p.head? = some x ∧p.getLast? = some v ∧∀ w ∈ p, w ∈ G.ancestralSet (X ∪ Y ∪ Z)Proof (Lean source)
theorem activePath_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.IsActivePath Z p ∧ p.head? = some x ∧ p.getLast? = some v ∧ ∀ w ∈ p, w ∈ G.ancestralSet (X ∪ Y ∪ Z) := by -- Pull an active path witness from `bbReachableVertices_iff_activePath`, -- then apply `activePath_nodes_are_ancestors`. obtain ⟨x, hxX, p, hlen, hact, hhead, hlast⟩ := (G.bbReachableVertices_iff_activePath X Z v).mp hvR exact ⟨p, x, hxX, hlen, hact, hhead, hlast, G.activePath_nodes_are_ancestors hxX hvY hact hhead hlast⟩ -
isActivePath_of_directedtheorem — A *forward*-directed path whose interior vertices avoid Z is an active path given Z. "Forward-directed" means each edge points from the *earlier* index to the *later* index. Every interior vertex is then a non-collider (incoming + outgoing), and by the avoidance hypothesis none is in Z; endpoints may lie in Z.hypothesesZ :Finset Vp :List Vhdir :∀ (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⟩ ∉ ZconclusionG.IsActivePath Z pProof (Lean source)
theorem isActivePath_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.IsActivePath 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 -
exists_activePath_of_ancestor_avoidingtheorem — An ancestor outside the conditioning set's ancestral closure has an active path to its descendant.hypothesesconclusion∃ (p : List V), p.length ≥ 2 ∧ p.head? = some u ∧ p.getLast? = some v ∧ G.IsActivePath Z pProof (Lean source)
theorem exists_activePath_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.IsActivePath Z p := by obtain ⟨p, hlen, hhead, hlast, hedge, hZavoid⟩ := G.exists_directedPath_avoiding huv huZ exact ⟨p, hlen, hhead, hlast, G.isActivePath_of_directed hedge (fun i hi => hZavoid _ (List.get_mem _ _))⟩ -
fork_isActivePaththeorem — Two directed paths from one unconditioned vertex can be joined through that fork.hypothesesZ :Finset Vu x y :Vxp yp :List Vhxp_len :xp.length ≥ 2hxp_head :xp.head? = some uhxp_last :xp.getLast? = some xhxp_edge :∀ (i : ℕ) (hi : i + 1 < xp.length), G.edge (xp.get ⟨i, by omega⟩) (xp.get ⟨i + 1, hi⟩)hxp_Z :∀ z ∈ xp, z ∉ Zhyp_len :yp.length ≥ 2hyp_head :yp.head? = some uhyp_last :yp.getLast? = some yhyp_edge :∀ (i : ℕ) (hi : i + 1 < yp.length), G.edge (yp.get ⟨i, by omega⟩) (yp.get ⟨i + 1, hi⟩)hyp_Z :∀ z ∈ yp, z ∉ Zconclusionlet p := xp.reverse ++ yp.tail p.length ≥ 2 ∧p.head? = some x ∧p.getLast? = some y ∧G.IsActivePath Z pProof (Lean source)
theorem fork_isActivePath {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.IsActivePath 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 := length_tail -- yp.tail nonempty since yp.length ≥ 2 have hyp_tail_ne : yp.tail ≠ [] := by rw [← 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, 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 `IsActivePath 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, 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]. have hi_eq : i = R - 1 := by omega subst hi_eq have hiR : R - 1 < R := by omega have hi1L : R ≤ R - 1 + 1 := by omega have hi2L : R ≤ R - 1 + 2 := by omega -- … truncated; follow the source link for the rest …
BackdoorBridges 1 core · 1 supporting This file contains graph-level lemmas for backdoor identification arguments. ★ dSep_union_roots_right
Backdoor Graph Bridges
This file contains graph-level lemmas for backdoor identification arguments. The
main theorem DAG.dSep_union_roots_right shows that adding root vertices
disjoint from the query variables to the conditioning set preserves
d-separation. The proof uses active-path semantics: a conditioned root can only
appear as a non-collider fork on an interior path, so it blocks rather than opens
paths.
theorem dSep_union_roots_right reviewed
⚑ flagged
Causalean.DAG
Adding root nodes (no incoming edges) to the conditioning set preserves d-separation. In a DAG G, suppose X and Y are d-separated by Z, every vertex of R has no incoming edge in G, i.e. R consists of root vertices, and R is disjoint from X and from Y. Then X and Y remain d-separated once the root vertices R are added to the conditioning set: G.dSep X Y (Z ∪ R).
Formal statement
Proof (Lean source)
theorem dSep_union_roots_right {X Y Z R : Finset V}
(hXY_sep : G.dSep X Y Z)
(hRoots : ∀ r ∈ R, ∀ u, ¬ G.edge u r)
(hRX : Disjoint R X) (hRY : Disjoint R Y) :
G.dSep X Y (Z ∪ R) := by
rcases hXY_sep with ⟨hXY, hXZ, hYZ, hReach⟩
refine ⟨hXY, ?_, ?_, ?_⟩
· rw [Finset.disjoint_left]
intro v hvX hvZR
rcases Finset.mem_union.mp hvZR with hvZ | hvR
· exact Finset.disjoint_left.mp hXZ hvX hvZ
· exact Finset.disjoint_left.mp hRX hvR hvX
· rw [Finset.disjoint_left]
intro v hvY hvZR
rcases Finset.mem_union.mp hvZR with hvZ | hvR
· exact Finset.disjoint_left.mp hYZ hvY hvZ
· exact Finset.disjoint_left.mp hRY hvR hvY
rw [Finset.disjoint_left] at hReach ⊢
intro v hv_ZR hvY
rw [G.bbReachableVertices_iff_activePath] at hv_ZR
obtain ⟨x, hxX, p, hlen, hact, hhead, hlast⟩ := hv_ZR
obtain ⟨hadj, hcoll⟩ := hact
-- Helper: the interior vertex condition, parametrized by the triple's left index.
-- For a triple (i, i+1, i+2), middle `p[i+1]` is not a collider and not in Z ∪ R.
-- If `p[i+1] ∈ R`, the "not in Z ∪ R" fails, contradiction.
have hNoR_interior : ∀ (i : ℕ) (hi : i + 2 < p.length),
p.get ⟨i + 1, by omega⟩ ∉ R := by
intro i hi hmem
have hc := hcoll i hi
set l := p.get ⟨i, by omega⟩
set m := p.get ⟨i + 1, by omega⟩
set r := p.get ⟨i + 2, hi⟩
have hnoInL : ¬ G.edge l m := hRoots _ hmem l
have hnc : ¬ G.IsCollider l m r := fun h => hnoInL h.1
simp only [hnc, if_false] at hc
exact hc (mem_union_right _ hmem)
-- Rebuild active path given Z.
have hact_Z : G.IsActivePath Z p := by
refine ⟨hadj, ?_⟩
intro i hi
have hc := hcoll i hi
set l := p.get ⟨i, by omega⟩
set m := p.get ⟨i + 1, by omega⟩
set r := p.get ⟨i + 2, hi⟩
have hm_notR : m ∉ R := hNoR_interior i hi
by_cases hColl : G.IsCollider l m r
· -- Collider case.
simp only [hColl, if_true] at hc
simp only [hColl, if_true]
-- `hc : m ∈ bbZAncestors (Z ∪ R)`. Want `m ∈ bbZAncestors Z`.
-- bbZAncestors = ancestralSet = S ∪ ancestorsSet S
simp only [bbZAncestors, ancestralSet] at hc ⊢
rcases Finset.mem_union.mp hc with hZR | hmAnc
· rcases Finset.mem_union.mp hZR with hZ | hR
· exact mem_union_left _ hZ
· exact absurd hR hm_notR
· simp only [ancestorsSet, mem_filter, Finset.mem_univ,
true_and] at hmAnc
obtain ⟨w, hwZR, hma⟩ := hmAnc
rcases Finset.mem_union.mp hwZR with hwZ | hwR
· refine mem_union_right _ ?_
simp only [ancestorsSet, mem_filter, Finset.mem_univ, true_and]
exact ⟨w, hwZ, hma⟩
· exact absurd hma (G.not_isAncestor_of_root' (hRoots w hwR) m)
· -- Non-collider case.
simp only [hColl, if_false] at hc
simp only [hColl, if_false]
exact fun hmZ => hc (mem_union_left _ hmZ)
-- Close: active path given Z witnesses bbReachable Z X, contradicting hXY_sep.
have hvReachZ : v ∈ G.bbReachableVertices Z X := by
rw [G.bbReachableVertices_iff_activePath]
exact ⟨x, hxX, p, hlen, hact_Z, hhead, hlast⟩
exact hReach hvReachZ hvY
1 supporting declaration (lemmas, instances)
-
not_isAncestor_of_root'lemma — A vertex with no incoming edges has no proper ancestors.hypothesesr :Vhr :∀ u, ¬ G.edge u ru :Vconclusion¬ G.isAncestor u rProof (Lean source)
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
InduceTransport 1 core · 3 supporting This file collects graph-only bridges that compare d-separation in an induced SWIG with d-separation in the ambient SWIG. ★ dSep_union_fixed_of_induce_dSep
d-Separation Transport for Induced SWIGs
This file collects graph-only bridges that compare d-separation in an induced SWIG with d-separation in the ambient SWIG. The main bridge is tailored to ancestral induced graphs: active paths between observed vertices cannot use vertices outside the ancestral support, except for fixed nodes, which are handled by placing all fixed nodes in the conditioning set.
The support lemmas prove idempotence of ancestral closure, preservation of
ancestor paths and collider activations inside an ancestral induced SWIG, and
non-membership of fixed nodes on relevant observed-endpoint active paths. The
main theorem SWIGGraph.dSep_union_fixed_of_induce_dSep lifts d-separation from
(G.induce R).dag to the ambient G.dag after adjoining all fixed nodes to the
conditioning set.
theorem dSep_union_fixed_of_induce_dSep reviewed
⚑ flagged
Causalean.SWIGGraph
D-separation in an ancestral induced SWIG lifts to the ambient SWIG once fixed intervention nodes are included in the conditioning set. Fix a SWIG G and a node set R that is closed under G's ancestral relation, with X, Y, and Z each contained in the observed nodes of R. If X and Y are d-separated by Z in the graph induced on R, then X and Y are d-separated by Z together with G's fixed intervention nodes, in the ambient graph.
Formal statement
Proof (Lean source)
theorem dSep_union_fixed_of_induce_dSep
(R X Y Z : Finset (SWIGNode N))
(hX : X ⊆ R ∩ G.observed) (hY : Y ⊆ R ∩ G.observed)
(hZ : Z ⊆ R ∩ G.observed)
(hR : G.dag.ancestralSet R ⊆ R)
(h : (G.induce R).dag.dSep X Y Z) :
G.dag.dSep X Y (Z ∪ G.fixed) := by
rcases h with ⟨hXY, hXZ, hYZ, hReach⟩
refine ⟨hXY, ?_, ?_, ?_⟩
· rw [Finset.disjoint_left]
intro x hxX hxZf
rcases Finset.mem_union.mp hxZf with hxZ | hxF
· exact Finset.disjoint_left.mp hXZ hxX hxZ
· exact G.not_mem_fixed_of_mem_observed ((Finset.mem_inter.mp (hX hxX)).2) hxF
· rw [Finset.disjoint_left]
intro y hyY hyZf
rcases Finset.mem_union.mp hyZf with hyZ | hyF
· exact Finset.disjoint_left.mp hYZ hyY hyZ
· exact G.not_mem_fixed_of_mem_observed ((Finset.mem_inter.mp (hY hyY)).2) hyF
rw [Finset.disjoint_left]
intro y hyReach hyY
rw [G.dag.bbReachableVertices_iff_activePath] at hyReach
obtain ⟨x, hxX, p, hlen, hact, hhead, hlast⟩ := hyReach
have hnotFixed : ∀ v ∈ p, v ∉ G.fixed := by
intro v hv
exact G.activePath_node_not_fixed hX hY hxX hyY hact hhead hlast hv
have hnodeR : ∀ v ∈ p, v ∈ R := by
intro v hv
have hvAnc : v ∈ G.dag.ancestralSet (X ∪ Y ∪ (Z ∪ G.fixed)) :=
G.dag.activePath_nodes_are_ancestors hxX hyY hact hhead hlast v hv
exact G.mem_R_of_ancestor_union_not_fixed hX hY hZ hR hvAnc (hnotFixed v hv)
let active : Finset (SWIGNode N) :=
(G.fixed.filter (fun s => iotaMap s ∈ R ∩ G.observed)) ∪
(R ∩ G.observed) ∪
(G.unobserved.filter (fun u => ∃ z ∈ R ∩ G.observed, G.dag.edge u z))
have hactive_of_incident :
∀ {v : SWIGNode N}, v ∈ p →
(∃ w ∈ R, G.dag.edge v w ∨ G.dag.edge w v) → v ∈ active := by
intro v hv hinc
exact G.mem_induce_active_of_mem_R_of_not_fixed_of_incident
(hnodeR v hv) (hnotFixed v hv) hinc
have hIndEdge :
∀ {u v : SWIGNode N}, G.dag.edge u v → u ∈ active → v ∈ active →
(G.induce R).dag.edge u v := by
intro u v huv hu hv
exact G.induced_edge_of_edge_of_active huv hu hv
have hactInd : (G.induce R).dag.IsActivePath Z p := by
refine ⟨?_, ?_⟩
· intro i hi
let u := p.get ⟨i, by omega⟩
let v := p.get ⟨i + 1, hi⟩
have huMem : u ∈ p := List.get_mem _ _
have hvMem : v ∈ p := List.get_mem _ _
rcases hact.1 i hi with huv | hvu
· have huAct : u ∈ active := hactive_of_incident huMem
⟨v, hnodeR v hvMem, Or.inl huv⟩
have hvAct : v ∈ active := hactive_of_incident hvMem
⟨u, hnodeR u huMem, Or.inr huv⟩
exact Or.inl (hIndEdge huv huAct hvAct)
· have huAct : u ∈ active := hactive_of_incident huMem
⟨v, hnodeR v hvMem, Or.inr hvu⟩
have hvAct : v ∈ active := hactive_of_incident hvMem
⟨u, hnodeR u huMem, Or.inl hvu⟩
exact Or.inr (hIndEdge hvu hvAct huAct)
· intro i hi
let l := p.get ⟨i, by omega⟩
let m := p.get ⟨i + 1, by omega⟩
let r := p.get ⟨i + 2, hi⟩
have hlMem : l ∈ p := List.get_mem _ _
have hmMem : m ∈ p := List.get_mem _ _
have hrMem : r ∈ p := List.get_mem _ _
have hambClause := hact.2 i hi
by_cases hcollInd : (G.induce R).dag.IsCollider l m r
· rw [if_pos hcollInd]
have hlmAmb : G.dag.edge l m := by
change (G.inducedDag active).edge l m ∧
(G.inducedDag active).edge r m at hcollInd
exact ((G.inducedDag_edge_iff active l m).mp hcollInd.1).1
have hrmAmb : G.dag.edge r m := by
change (G.inducedDag active).edge l m ∧
(G.inducedDag active).edge r m at hcollInd
exact ((G.inducedDag_edge_iff active r m).mp hcollInd.2).1
have hcollAmb : G.dag.IsCollider l m r := ⟨hlmAmb, hrmAmb⟩
rw [if_pos hcollAmb] at hambClause
have hmpar : G.dag.parents m ≠ ∅ := by
intro hempty
have : l ∈ G.dag.parents m := G.dag.mem_parents.mpr hlmAmb
simp [hempty] at this
exact G.induced_bbZAncestors_of_ambient_union_fixed hZ hR hmpar hambClause
· rw [if_neg hcollInd]
intro hmZ
by_cases hcollAmb : G.dag.IsCollider l m r
· have hlAct : l ∈ active := hactive_of_incident hlMem
⟨m, hnodeR m hmMem, Or.inl hcollAmb.1⟩
have hmAct : m ∈ active := hactive_of_incident hmMem
⟨l, hnodeR l hlMem, Or.inr hcollAmb.1⟩
have hrAct : r ∈ active := hactive_of_incident hrMem
⟨m, hnodeR m hmMem, Or.inl hcollAmb.2⟩
have hcollInd' : (G.induce R).dag.IsCollider l m r :=
⟨hIndEdge hcollAmb.1 hlAct hmAct,
hIndEdge hcollAmb.2 hrAct hmAct⟩
exact hcollInd hcollInd'
· rw [if_neg hcollAmb] at hambClause
exact hambClause (mem_union_left _ hmZ)
have hyReachInd : y ∈ (G.induce R).dag.bbReachableVertices Z X := by
rw [(G.induce R).dag.bbReachableVertices_iff_activePath]
exact ⟨x, hxX, p, hlen, hactInd, hhead, hlast⟩
exact Finset.disjoint_left.mp hReach hyReachInd hyY
3 supporting declarations (lemmas, instances)
-
ancestralSet_idemtheorem — Taking the ancestors of an ancestral set gives back the same set.hypothesesconclusionG.ancestralSet (G.ancestralSet S) = G.ancestralSet SProof (Lean source)
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) -
not_mem_fixed_of_mem_observedlemma — Observed SWIG vertices are not members of the fixed intervention set.Proof (Lean source)
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 -
activePath_node_not_fixedlemma — Every node on an active path conditioned on the union of a conditioning set and the fixed intervention nodes, with observed endpoints, is not fixed.hypothesesx y v :SWIGNode NhX :X ⊆ R ∩ G.observedhY :Y ⊆ R ∩ G.observedhxX :x ∈ XhyY :y ∈ Yhact :G.dag.IsActivePath (Z ∪ G.fixed) phhead :p.head? = some xhlast :p.getLast? = some yhv :v ∈ pconclusionv ∉ G.fixedProof (Lean source)
lemma activePath_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.IsActivePath (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)
OrderedLocalSG 2 core · 11 supporting This file introduces a purely combinatorial inductive predicate DAG.OrderedLocalSG on a DAG, recording which conditional-independence triples are derivable from the *ordered-local basis* (each node is independent of its ★ OrderedLocalSG★ orderedLocalSG_of_dSep_with_fixed
Ordered-local semi-graphoid closure of a DAG
This file introduces a purely combinatorial inductive predicate DAG.OrderedLocalSG
on a DAG, recording which conditional-independence triples are derivable from the
ordered-local basis (each node is independent of its non-parent predecessors given
its parents) using only the semi-graphoid axioms (symmetry, decomposition, weak
union, contraction — no graphoid intersection). It then proves the graph theorem
orderedLocalSG_of_dSep_with_fixed: every d-separation is such a derivation.
This is the graph-level heart of the global Markov property. The probabilistic
content is added separately by interpreting a derivation as a conditional
independence under the joint distribution (fullCondIndep_of_orderedLocalSG), which
maps each constructor to the matching FullCondIndep semi-graphoid lemma. Splitting
the proof this way keeps all measure theory out of the graph induction.
inductive OrderedLocalSG reviewed
⚑ flagged
Causalean.DAG
Ordered-local semi-graphoid closure. A conditional-independence claim between two random-node blocks, given a third block, belongs to this closure when it can be derived from the DAG's ordered-local Markov basis using only the semi-graphoid rules.
Definition (Lean source)
inductive OrderedLocalSG (G : DAG V) (R : Finset V) :
Finset V → Finset V → Finset V → Prop
| nil (Y Z : Finset V) (hY : Y ⊆ R) (hZ : Z ⊆ R) : OrderedLocalSG G R ∅ Y Z
| basis (v : V) (hv : v ∈ R) (P : Finset V)
(hP : P ⊆ R) (hND : P ⊆ G.nonDescendants v) (hPa : G.parents v ∩ R ⊆ P) :
OrderedLocalSG G R {v} (P \ (G.parents v ∩ R)) (G.parents v ∩ R)
| symm {X Y Z : Finset V} : OrderedLocalSG G R X Y Z → OrderedLocalSG G R Y X Z
| decomp {X Y W Z : Finset V} :
OrderedLocalSG G R X (Y ∪ W) Z → OrderedLocalSG G R X Y Z
| weakUnion {X Y W Z : Finset V} :
OrderedLocalSG G R X (Y ∪ W) Z → OrderedLocalSG G R X Y (Z ∪ W)
| contract {X Y W Z : Finset V} :
OrderedLocalSG G R X Y (Z ∪ W) → OrderedLocalSG G R X W Z →
OrderedLocalSG G R X (Y ∪ W) Z
theorem orderedLocalSG_of_dSep_with_fixed reviewed
⚑ flagged
Causalean.DAG
d-separation yields an ordered-local derivation. In a DAG G, suppose every vertex of Zf has no parents, i.e. Zf consists of fixed roots, Zf is disjoint from R, and X, Y, and Zr are each contained in R. If X and Y are d-separated by Zr ∪ Zf, then the conditional-independence triple "X ⊥ Y given Zr" is derivable from the ordered-local basis on R via the semi-graphoid axioms.
Formal statement
Proof (Lean source)
theorem orderedLocalSG_of_dSep_with_fixed
(R X Y Zr Zf : Finset V)
(hFixedRoots : ∀ f ∈ Zf, G.parents f = ∅)
(hFR : Disjoint Zf R)
(hX : X ⊆ R) (hY : Y ⊆ R) (hZr : Zr ⊆ R)
(hdSep : G.dSep X Y (Zr ∪ Zf)) :
G.OrderedLocalSG R X Y Zr := by
have hXY : Disjoint X Y := hdSep.1
have hXZ : Disjoint X Zr := hdSep.2.1.mono_right Finset.subset_union_left
have hYZ : Disjoint Y Zr := hdSep.2.2.1.mono_right Finset.subset_union_left
-- Trivial base case: an empty source set.
rcases Finset.eq_empty_or_nonempty X with hXe | hXne
· subst hXe; exact OrderedLocalSG.nil Y Zr hY hZr
-- Abbreviate the query set and select a topological maximum of its ancestral set.
set Q : Finset V := X ∪ Y ∪ Zr ∪ Zf with hQ_def
have hQne : (G.ancestralSet Q).Nonempty := by
obtain ⟨x, hx⟩ := hXne
exact ⟨x, G.subset_ancestralSet Q (by
simp only [hQ_def, mem_union]; exact inl (inl (inl hx)))⟩
obtain ⟨n, hnAnc, hmax⟩ := Finset.exists_max_image (G.ancestralSet Q) G.topoOrder hQne
have hnQ : n ∈ Q := G.topoMax_mem_seed hnAnc hmax
-- Membership facts used across the cases.
have hnR_of_mem : ∀ {S : Finset V}, S ⊆ R → n ∈ S → n ∉ Zf := by
intro S hSR hnS hnF
exact (Finset.disjoint_left.mp hFR hnF) (hSR hnS)
-- Reusable inclusions for the termination (card-drop) arguments.
have hQanc : Q ⊆ G.ancestralSet Q := G.subset_ancestralSet Q
have hParAnc : G.parents n ⊆ G.ancestralSet Q := by
intro a ha
exact G.mem_ancestralSet_of_isAncestor hnQ (isAncestor.edge (G.mem_parents.mp ha))
have hXsubQ : X ⊆ Q := by rw [hQ_def]; intro x hx; simp only [mem_union]; tauto
have hYsubQ : Y ⊆ Q := by rw [hQ_def]; intro x hx; simp only [mem_union]; tauto
have hZrsubQ : Zr ⊆ Q := by rw [hQ_def]; intro x hx; simp only [mem_union]; tauto
have hZfsubQ : Zf ⊆ Q := by rw [hQ_def]; intro x hx; simp only [mem_union]; tauto
have hXQ : X ⊆ G.ancestralSet Q := hXsubQ.trans hQanc
have hYQ : Y ⊆ G.ancestralSet Q := hYsubQ.trans hQanc
have hZrQ : Zr ⊆ G.ancestralSet Q := hZrsubQ.trans hQanc
have hZfQ : Zf ⊆ G.ancestralSet Q := hZfsubQ.trans hQanc
rw [hQ_def] at hnQ
simp only [mem_union] at hnQ
-- Case analysis on where the maximal node `n` sits.
rcases hnQ with ((hnX | hnY) | hnZr) | hnZf
· -- ===== Case n ∈ X =====
set X' : Finset V := X.erase n with hX'_def
set A : Finset V := G.parents n ∩ R with hA_def
set C : Finset V := Zr ∪ X' with hC_def
set A0 : Finset V := A \ C with hA0_def
have hnX' : n ∉ X' := Finset.notMem_erase n X
have hnZf : n ∉ Zf := fun h => (hnR_of_mem hX hnX) h
have hXins : X = insert n X' := (Finset.insert_erase hnX).symm
have hX'R : X' ⊆ R := (Finset.erase_subset _ _).trans hX
have hX'X : X' ⊆ X := Finset.erase_subset _ _
have hnY : n ∉ Y := fun h => (Finset.disjoint_left.mp hXY hnX) h
have hnZr : n ∉ Zr := fun h => (Finset.disjoint_left.mp hXZ hnX) h
have hCR : C ⊆ R := Finset.union_subset hZr hX'R
have hAR : A ⊆ R := Finset.inter_subset_right
have hA0R : A0 ⊆ R := (sdiff_subset).trans hAR
-- `n` is not an ancestor of any query node (topological maximality).
have hND_Q : ∀ w ∈ Q, ¬ G.isAncestor n w := by
intro w hwQ hanc
have h1 : G.topoOrder w ≤ G.topoOrder n := hmax w (G.subset_ancestralSet Q hwQ)
have h2 : G.topoOrder n < G.topoOrder w := G.isAncestor_topoOrder_lt hanc
omega
-- ihX': drop `n` from the source.
have ihX' : G.OrderedLocalSG R X' Y Zr :=
orderedLocalSG_of_dSep_with_fixed R X' Y Zr Zf hFixedRoots hFR hX'R hY hZr
(G.dSep_subset_left hX'X hdSep)
-- `dSep {n} Y (C ∪ Zf)`.
have hCZf_eq : C ∪ Zf = (Zr ∪ Zf) ∪ X' := by
rw [hC_def]; ext x; simp only [mem_union]; tauto
have hdSepN : G.dSep {n} Y (C ∪ Zf) := by
rw [hCZf_eq]
apply G.dSep_source_to_cond (X := {n}) (S := X')
· exact Finset.disjoint_singleton_left.mpr hnX'
· rw [show ({n} : Finset V) ∪ X' = X by rw [hXins, Finset.insert_eq]]
exact hdSep
-- Parents disjoint from `Y`; hence `A0` (⊆ parents) too.
have hParY : Disjoint (G.parents n) Y := G.parents_disjoint_of_dSep_singleton hdSepN
have hAY : Disjoint A Y := hParY.mono_left Finset.inter_subset_left
-- A2f: parents inherit the separation.
have hA0_par : ∀ a ∈ A0, G.edge a n := by
intro a ha
have : a ∈ A := (Finset.mem_sdiff.mp ha).1
exact G.mem_parents.mp (Finset.mem_inter.mp this).1
have hA0_D : ∀ a ∈ A0, a ∉ C ∪ Zf := by
intro a ha haCZf
rw [mem_union] at haCZf
rcases haCZf with haC | haZf
· exact (Finset.mem_sdiff.mp ha).2 haC
· exact (Finset.disjoint_left.mp hFR haZf) (hA0R ha)
have hdSepA0 : G.dSep A0 Y (C ∪ Zf) :=
G.dSep_parents_of_maximal_source hdSepN hA0_par hA0_D
-- ihA0.
have ihA0 : G.OrderedLocalSG R A0 Y C :=
orderedLocalSG_of_dSep_with_fixed R A0 Y C Zf hFixedRoots hFR hA0R hY hCR
hdSepA0
-- Basis at `n` with block `P = Y ∪ C ∪ A`.
have hPR : Y ∪ C ∪ A ⊆ R := Finset.union_subset (Finset.union_subset hY hCR) hAR
-- `Y ∪ C ⊆ Q` (used to inherit `¬ isAncestor n ·` from topo-maximality).
have hYC_subQ : Y ∪ C ⊆ Q := by
rw [hQ_def, hC_def]
intro w hw
simp only [mem_union] at hw ⊢
rcases hw with hY' | hZr' | hX''
· exact inl (inl (inr hY'))
· exact inl (inr hZr')
· exact inl (inl (inl (hX'X hX'')))
have hPND : Y ∪ C ∪ A ⊆ G.nonDescendants n := by
intro w hw
rw [mem_union] at hw
simp only [nonDescendants, mem_filter, Finset.mem_univ, true_and]
rcases hw with hwYC | hwA
· -- w ∈ Y ∪ C ⊆ Q: topo-maximal `n` is no ancestor of `w`, and `w ≠ n`.
have hwQ : w ∈ Q := hYC_subQ hwYC
refine ⟨hND_Q w hwQ, ?_⟩
rintro rfl
rw [mem_union, hC_def, mem_union] at hwYC
rcases hwYC with h | h | h
exacts [hnY h, hnZr h, hnX' h]
· -- w ∈ A = parents n ∩ R: `n` cannot be an ancestor of its own parent.
have hwPar : w ∈ G.parents n := (Finset.mem_inter.mp hwA).1
have hedge : G.edge w n := G.mem_parents.mp hwPar
refine ⟨fun hanc => ?_, fun hwn => G.irrefl n (hwn ▸ hedge)⟩
exact G.isAncestor_irrefl n (G.isAncestor_trans hanc (isAncestor.edge hedge))
have hAsubP : A ⊆ Y ∪ C ∪ A := Finset.subset_union_right
have hPaR_sub : G.parents n ∩ R ⊆ Y ∪ C ∪ A := by rw [← hA_def]; exact hAsubP
have hbasis := OrderedLocalSG.basis (G := G) (R := R) n (hX hnX) (Y ∪ C ∪ A) hPR hPND hPaR_sub
-- `(Y ∪ C ∪ A) \ (parents n ∩ R) = Y ∪ (C \ A)`.
have hsdiff_eq : (Y ∪ C ∪ A) \ (G.parents n ∩ R) = Y ∪ (C \ A) := by
rw [← hA_def]; ext x
simp only [mem_sdiff, mem_union]
constructor
· rintro ⟨(hY' | hC') | hA', hnA⟩
· exact inl hY'
· exact inr ⟨hC', hnA⟩
· exact absurd hA' hnA
· rintro (hY' | ⟨hC', hnA⟩)
· exact ⟨Or.inl (inl hY'), fun hA' => (Finset.disjoint_left.mp hAY hA') hY'⟩
· exact ⟨Or.inl (inr hC'), hnA⟩
rw [hsdiff_eq, ← hA_def] at hbasis
-- weakUnion: move `C \ A` into the condition; `A ∪ (C \ A) = C ∪ A0`.
have hweak := OrderedLocalSG.weakUnion (W := C \ A) (Z := A) hbasis
have hAC_eq : A ∪ (C \ A) = C ∪ A0 := by
rw [hA0_def]; ext x
simp only [mem_union, mem_sdiff]; tauto
rw [hAC_eq] at hweak
-- hweak : {n} ⊥ Y | (C ∪ A0). Fold with ihA0 to drop `A0`.
have hstep2 : G.OrderedLocalSG R {n} Y C := by
have h1 : G.OrderedLocalSG R Y {n} (C ∪ A0) := hweak.symm
have h2 : G.OrderedLocalSG R Y A0 C := ihA0.symm
have hc : G.OrderedLocalSG R Y ({n} ∪ A0) C := OrderedLocalSG.contract h1 h2
exact (OrderedLocalSG.decomp (W := A0) hc).symm
-- Final fold with ihX': `{n}∪X' = X`.
have h1 : G.OrderedLocalSG R Y {n} (Zr ∪ X') := by rw [← hC_def]; exact hstep2.symm
have h2 : G.OrderedLocalSG R Y X' Zr := ihX'.symm
have hc : G.OrderedLocalSG R Y ({n} ∪ X') Zr := OrderedLocalSG.contract h1 h2
rw [show ({n} : Finset V) ∪ X' = X by rw [hXins, Finset.insert_eq]] at hc
exact hc.symm
· -- ===== Case n ∈ Y ===== (mirror of the n ∈ X case with X ↔ Y)
refine OrderedLocalSG.symm ?_
have hdSepYX : G.dSep Y X (Zr ∪ Zf) := G.dSep_symm _ _ _ hdSep
set Y' : Finset V := Y.erase n with hY'_def
set A : Finset V := G.parents n ∩ R with hA_def
set C : Finset V := Zr ∪ Y' with hC_def
set A0 : Finset V := A \ C with hA0_def
have hnY' : n ∉ Y' := Finset.notMem_erase n Y
have hnZf : n ∉ Zf := fun h => (hnR_of_mem hY hnY) h
have hYins : Y = insert n Y' := (Finset.insert_erase hnY).symm
have hY'R : Y' ⊆ R := (Finset.erase_subset _ _).trans hY
have hY'Y : Y' ⊆ Y := Finset.erase_subset _ _
have hnX : n ∉ X := fun h => (Finset.disjoint_left.mp hXY h) hnY
have hnZr : n ∉ Zr := fun h => (Finset.disjoint_left.mp hYZ hnY) h
have hCR : C ⊆ R := Finset.union_subset hZr hY'R
have hAR : A ⊆ R := Finset.inter_subset_right
have hA0R : A0 ⊆ R := (sdiff_subset).trans hAR
have hND_Q : ∀ w ∈ Q, ¬ G.isAncestor n w := by
intro w hwQ hanc
have h1 : G.topoOrder w ≤ G.topoOrder n := hmax w (G.subset_ancestralSet Q hwQ)
have h2 : G.topoOrder n < G.topoOrder w := G.isAncestor_topoOrder_lt hanc
omega
have ihY' : G.OrderedLocalSG R Y' X Zr :=
orderedLocalSG_of_dSep_with_fixed R Y' X Zr Zf hFixedRoots hFR hY'R hX hZr
(G.dSep_subset_left hY'Y hdSepYX)
have hCZf_eq : C ∪ Zf = (Zr ∪ Zf) ∪ Y' := by
rw [hC_def]; ext x; simp only [mem_union]; tauto
have hdSepN : G.dSep {n} X (C ∪ Zf) := by
rw [hCZf_eq]
apply G.dSep_source_to_cond (X := {n}) (S := Y')
· exact Finset.disjoint_singleton_left.mpr hnY'
· rw [show ({n} : Finset V) ∪ Y' = Y by rw [hYins, Finset.insert_eq]]
exact hdSepYX
have hParX : Disjoint (G.parents n) X := G.parents_disjoint_of_dSep_singleton hdSepN
have hAX : Disjoint A X := hParX.mono_left Finset.inter_subset_left
have hA0_par : ∀ a ∈ A0, G.edge a n := by
intro a ha
have : a ∈ A := (Finset.mem_sdiff.mp ha).1
exact G.mem_parents.mp (Finset.mem_inter.mp this).1
have hA0_D : ∀ a ∈ A0, a ∉ C ∪ Zf := by
intro a ha haCZf
rw [mem_union] at haCZf
rcases haCZf with haC | haZf
· exact (Finset.mem_sdiff.mp ha).2 haC
· exact (Finset.disjoint_left.mp hFR haZf) (hA0R ha)
have hdSepA0 : G.dSep A0 X (C ∪ Zf) :=
G.dSep_parents_of_maximal_source hdSepN hA0_par hA0_D
have ihA0 : G.OrderedLocalSG R A0 X C :=
orderedLocalSG_of_dSep_with_fixed R A0 X C Zf hFixedRoots hFR hA0R hX hCR
hdSepA0
have hPR : X ∪ C ∪ A ⊆ R := Finset.union_subset (Finset.union_subset hX hCR) hAR
have hXC_subQ : X ∪ C ⊆ Q := by
rw [hQ_def, hC_def]
intro w hw
simp only [mem_union] at hw ⊢
rcases hw with hX' | hZr' | hY''
· exact inl (inl (inl hX'))
· exact inl (inr hZr')
· exact inl (inl (inr (hY'Y hY'')))
have hPND : X ∪ C ∪ A ⊆ G.nonDescendants n := by
intro w hw
rw [mem_union] at hw
simp only [nonDescendants, mem_filter, Finset.mem_univ, true_and]
rcases hw with hwXC | hwA
· have hwQ : w ∈ Q := hXC_subQ hwXC
refine ⟨hND_Q w hwQ, ?_⟩
rintro rfl
rw [mem_union, hC_def, mem_union] at hwXC
rcases hwXC with h | h | h
exacts [hnX h, hnZr h, hnY' h]
· have hwPar : w ∈ G.parents n := (Finset.mem_inter.mp hwA).1
have hedge : G.edge w n := G.mem_parents.mp hwPar
refine ⟨fun hanc => ?_, fun hwn => G.irrefl n (hwn ▸ hedge)⟩
exact G.isAncestor_irrefl n (G.isAncestor_trans hanc (isAncestor.edge hedge))
have hPaR_sub : G.parents n ∩ R ⊆ X ∪ C ∪ A := by rw [← hA_def]; exact Finset.subset_union_right
-- … truncated; follow the source link for the rest …
11 supporting declarations (lemmas, instances)
-
subset_randomtheorem — Every triple appearing in an ordered-local derivation has all three sets contained in the ambient random set R. Used by the SCM interpretation to recover the ⊆ randomVars side-conditions of FullCondIndep.hypothesesconclusionX ⊆ R ∧ Y ⊆ R ∧ Z ⊆ RProof (Lean source)
theorem OrderedLocalSG.subset_random {G : DAG V} {R X Y Z : Finset V} (h : G.OrderedLocalSG R X Y Z) : X ⊆ R ∧ Y ⊆ R ∧ Z ⊆ R := by induction h with | nil Y Z hY hZ => exact ⟨Finset.empty_subset _, hY, hZ⟩ | basis v hv P hP hND hPa => refine ⟨Finset.singleton_subset_iff.mpr hv, ?_, Finset.inter_subset_right⟩ exact (sdiff_subset).trans hP | symm _ ih => exact ⟨ih.2.1, ih.1, ih.2.2⟩ | decomp _ ih => exact ⟨ih.1, (subset_union_left).trans ih.2.1, ih.2.2⟩ | weakUnion _ ih => refine ⟨ih.1, (subset_union_left).trans ih.2.1, ?_⟩ exact union_subset ih.2.2 ((subset_union_right).trans ih.2.1) | contract _ _ ih1 ih2 => exact ⟨ih1.1, union_subset ih1.2.1 ih2.2.1, ih2.2.2⟩ -
topoMax_mem_seedtheorem — A vertex with maximal topological order in the ancestral closure of a seed set must itself belong to that seed set.hypothesesQ :Finset Vn :Vhn :n ∈ G.ancestralSet Qhmax :∀ m ∈ G.ancestralSet Q, G.topoOrder m ≤ G.topoOrder nconclusionn ∈ QProof (Lean source)
theorem topoMax_mem_seed {Q : Finset V} {n : V} (hn : n ∈ G.ancestralSet Q) (hmax : ∀ m ∈ G.ancestralSet Q, G.topoOrder m ≤ G.topoOrder n) : n ∈ Q := by simp only [ancestralSet, mem_union, ancestorsSet, mem_filter, Finset.mem_univ, true_and] at hn rcases hn with hnQ | ⟨w, hwQ, haw⟩ · exact hnQ · -- `n` is a strict ancestor of `w ∈ Q`; but `w ∈ ancestralSet Q`, so -- `topoOrder w ≤ topoOrder n < topoOrder w`, contradiction. exfalso have hwAnc : w ∈ G.ancestralSet Q := G.subset_ancestralSet Q (by exact hwQ) have h1 : G.topoOrder w ≤ G.topoOrder n := hmax w hwAnc have h2 : G.topoOrder n < G.topoOrder w := G.isAncestor_topoOrder_lt haw omega -
ancestralSet_subset_of_subset_ancestralSettheorem — The ancestral closure of a subset of an ancestral closure remains inside the original ancestral closure.hypothesesQ Q' :Finset Vh :Q' ⊆ G.ancestralSet QconclusionG.ancestralSet Q' ⊆ G.ancestralSet QProof (Lean source)
theorem ancestralSet_subset_of_subset_ancestralSet {Q Q' : Finset V} (h : Q' ⊆ G.ancestralSet Q) : G.ancestralSet Q' ⊆ G.ancestralSet Q := by intro u hu simp only [ancestralSet, mem_union, ancestorsSet, mem_filter, Finset.mem_univ, true_and] at hu ⊢ rcases hu with huQ' | ⟨q', hq'Q', haq'⟩ · have := h huQ' simpa only [ancestralSet, mem_union, ancestorsSet, mem_filter, Finset.mem_univ, true_and] using this · have hq' := h hq'Q' simp only [ancestralSet, mem_union, ancestorsSet, mem_filter, Finset.mem_univ, true_and] at hq' rcases hq' with hq'Q | ⟨q, hqQ, haq'q⟩ · exact inr ⟨q', hq'Q, haq'⟩ · exact inr ⟨q, hqQ, G.isAncestor_trans haq' haq'q⟩ -
isActivePath_insert_condtheorem — Adding a conditioning vertex preserves activity when that vertex appears internally only as a collider.hypothesesD :Finset Vp :List Vn :Vhact :G.IsActivePath D phno :∀ (i : ℕ) (hi : i + 2 < p.length)ifp.get ⟨i + 1, by omega⟩ = nthenG.IsCollider (p.get ⟨i, by omega⟩) (p.get ⟨i + 1, by omega⟩) (p.get ⟨i + 2, hi⟩)conclusionG.IsActivePath (insert n D) pProof (Lean source)
theorem isActivePath_insert_cond {D : Finset V} {p : List V} {n : V} (hact : G.IsActivePath D p) (hno : ∀ (i : ℕ) (hi : i + 2 < p.length), p.get ⟨i + 1, by omega⟩ = n → G.IsCollider (p.get ⟨i, by omega⟩) (p.get ⟨i + 1, by omega⟩) (p.get ⟨i + 2, hi⟩)) : G.IsActivePath (insert n D) p := by obtain ⟨hadj, hcoll⟩ := hact refine ⟨hadj, fun i hi => ?_⟩ have hval := hcoll i hi simp only at hval ⊢ set l := p.get ⟨i, by omega⟩ set m := p.get ⟨i + 1, by omega⟩ set r := p.get ⟨i + 2, hi⟩ by_cases hC : G.IsCollider l m r · rw [if_pos hC] at hval ⊢ exact (G.ancestralSet_mono (Finset.subset_insert n D)) hval · rw [if_neg hC] at hval ⊢ rw [Finset.mem_insert, not_or] refine ⟨fun hmn => hC (hno i hi hmn), hval⟩ -
last_edge_into_maxtheorem — The final edge of a path to a topological maximum points into it. On an active path whose nodes all lie in an ancestral set with topological maximum n, if the path ends at n then its last edge points into n: a child of n on the path would be a strict descendant, hence a strictly larger node.hypothesesD bigQ :Finset Vp :List Vn :Vhp_len :p.length ≥ 2hact :G.IsActivePath D phlast :p.getLast? = some nhpAnc :∀ v ∈ p, v ∈ G.ancestralSet bigQhmax :∀ m ∈ G.ancestralSet bigQ, G.topoOrder m ≤ G.topoOrder nconclusionG.edge (p.get ⟨p.length - 2, by omega⟩) nProof (Lean source)
theorem last_edge_into_max {D bigQ : Finset V} {p : List V} {n : V} (hp_len : p.length ≥ 2) (hact : G.IsActivePath D p) (hlast : p.getLast? = some n) (hpAnc : ∀ v ∈ p, v ∈ G.ancestralSet bigQ) (hmax : ∀ m ∈ G.ancestralSet bigQ, G.topoOrder m ≤ G.topoOrder n) : G.edge (p.get ⟨p.length - 2, by omega⟩) n := by -- The last adjacency is between `p[len-2]` and `p[len-1] = n`. have hadj := hact.1 (p.length - 2) (by omega) have hlast_get : p.get ⟨p.length - 2 + 1, by omega⟩ = n := by have hpne : p ≠ [] := by intro h; rw [h] at hp_len; simp at hp_len have h := getLast?_eq_some_getLast hpne rw [hlast] at h have hn_eq : p.getLast hpne = n := Option.some_inj.mp h.symm have hidx : (⟨p.length - 2 + 1, by omega⟩ : Fin p.length) = ⟨p.length - 1, by omega⟩ := Fin.ext (show p.length - 2 + 1 = p.length - 1 by omega) rw [hidx, List.get_eq_getElem, ← hn_eq, List.getLast_eq_getElem] rw [hlast_get] at hadj -- `hadj : UAdj p[len-2] n`. Rule out `edge n p[len-2]` by topo-maximality. rcases hadj with hin | hout · exact hin · exfalso have hAnc := hpAnc _ (List.get_mem p ⟨p.length - 2, by omega⟩) have h1 : G.topoOrder (p.get ⟨p.length - 2, by omega⟩) ≤ G.topoOrder n := hmax _ hAnc have h2 := G.isAncestor_topoOrder_lt (isAncestor.edge hout) omega -
activePath_join_at_collidertheorem — Two active paths that meet at a conditioned collider can be joined into an active path when both incident edges point into the joining vertex.hypothesesZ :Finset Vn x y :Vpa pb :List Vhpa_len :pa.length ≥ 2hpa_head :pa.head? = some xhpa_last :pa.getLast? = some nhpa_act :G.IsActivePath Z pahpb_len :pb.length ≥ 2hpb_head :pb.head? = some nhpb_last :pb.getLast? = some yhpb_act :G.IsActivePath Z pbhpa_in :G.edge (pa.get ⟨pa.length - 2, by omega⟩) nhpb_in :G.edge (pb.get ⟨1, by omega⟩) nhnZ :n ∈ Zconclusionlet p := pa ++ pb.tail p.length ≥ 2 ∧p.head? = some x ∧p.getLast? = some y ∧G.IsActivePath Z pProof (Lean source)
theorem activePath_join_at_collider {Z : Finset V} {n x y : V} {pa pb : List V} (hpa_len : pa.length ≥ 2) (hpa_head : pa.head? = some x) (hpa_last : pa.getLast? = some n) (hpa_act : G.IsActivePath Z pa) (hpb_len : pb.length ≥ 2) (hpb_head : pb.head? = some n) (hpb_last : pb.getLast? = some y) (hpb_act : G.IsActivePath Z pb) (hpa_in : G.edge (pa.get ⟨pa.length - 2, by omega⟩) n) (hpb_in : G.edge (pb.get ⟨1, by omega⟩) n) (hnZ : n ∈ Z) : let p := pa ++ pb.tail p.length ≥ 2 ∧ p.head? = some x ∧ p.getLast? = some y ∧ G.IsActivePath Z p := by have hpa_ne : pa ≠ [] := by intro h; rw [h] at hpa_len; simp at hpa_len have hpb_ne : pb ≠ [] := by intro h; rw [h] at hpb_len; simp at hpb_len -- pb.head = n have hpb_head_eq : pb.head hpb_ne = n := by have h := List.head?_eq_some_head hpb_ne; rw [hpb_head] at h exact (Option.some_inj.mp h.symm) -- pa.getLast = n have hpa_last_eq : pa.getLast hpa_ne = n := by have h := getLast?_eq_some_getLast hpa_ne; rw [hpa_last] at h exact (Option.some_inj.mp h.symm) -- pa.head = x have hpa_head_eq : pa.head hpa_ne = x := by have h := List.head?_eq_some_head hpa_ne; rw [hpa_head] at h exact (Option.some_inj.mp h.symm) -- pb.getLast = y have hpb_last_eq : pb.getLast hpb_ne = y := by have h := getLast?_eq_some_getLast hpb_ne; rw [hpb_last] at h exact (Option.some_inj.mp h.symm) -- pb = n :: pb.tail have hpb_decomp : pb = n :: pb.tail := by conv_lhs => rw [← List.cons_head_tail hpb_ne]; rw [hpb_head_eq] have hpb_tail_len : pb.tail.length = pb.length - 1 := List.length_tail have hpb_tail_ne : pb.tail ≠ [] := by rw [← length_pos_iff, hpb_tail_len]; omega set p := pa ++ pb.tail with hp_def set R := pa.length with hR_def have hp_len_eq : p.length = R + pb.tail.length := by simp only [hp_def, length_append, ← hR_def] have hp_len : p.length ≥ 2 := by rw [hp_len_eq]; omega have hp_head : p.head? = some x := by have : p.head? = pa.head? := List.head?_append_of_ne_nil _ hpa_ne rw [this, hpa_head] have hp_last : p.getLast? = some y := by have hlast_tail : pb.tail.getLast? = some y := by have heq : pb = [n] ++ pb.tail := by simpa using hpb_decomp have := getLast?_append_of_ne_nil [n] hpb_tail_ne rw [← heq] at this; rw [← this]; exact hpb_last simp only [hp_def, getLast?_append, hlast_tail]; rfl refine ⟨hp_len, hp_head, hp_last, ?_⟩ -- Index translation: p[k] = pa[k] for k < R; p[k] = pb[k-R+1] for k ≥ R. have hp_L : ∀ (k : ℕ) (hkR : k < R), p.get ⟨k, by rw [hp_len_eq]; omega⟩ = pa.get ⟨k, hkR⟩ := by intro k hkR simp only [hp_def, List.get_eq_getElem, List.getElem_append_left (h := hkR)] have hpb_tail_get : ∀ (j : ℕ) (hj1 : j < pb.tail.length) (hj2 : j + 1 < pb.length), pb.tail[j]'hj1 = pb[j + 1]'hj2 := by intro j hj1 hj2 have : pb[j + 1] = (n :: pb.tail)[j + 1]'(by rw [← hpb_decomp]; exact hj2) := by congr 1 rw [this]; simp [List.getElem_cons_succ] have hp_R : ∀ (k : ℕ) (hkL : R ≤ k) (hk : k < p.length), p.get ⟨k, hk⟩ = pb.get ⟨k - R + 1, by rw [hp_len_eq, hpb_tail_len] at hk; omega⟩ := by intro k hkL hk have hk_app : R ≤ k := hkL have htail_idx_lt : k - R < pb.tail.length := by rw [hp_len_eq] at hk; omega have hpget : p.get ⟨k, hk⟩ = pb.tail[k - R]'htail_idx_lt := by simp only [hp_def, List.get_eq_getElem] rw [List.getElem_append_right (by rw [← hR_def]; exact hk_app)] rw [hpget] rw [hpb_tail_get (k - R) htail_idx_lt (by rw [hpb_tail_len] at htail_idx_lt; omega)] simp [List.get_eq_getElem] -- pb[0] = n, pa[R-1] = n. have hpb_get_0 : pb.get ⟨0, by omega⟩ = n := by rw [List.get_eq_getElem, List.getElem_zero]; exact hpb_head_eq have hpa_get_last : pa.get ⟨R - 1, by omega⟩ = n := by rw [List.get_eq_getElem] have := List.getLast_eq_getElem hpa_ne rw [hpa_last_eq] at this rw [← this] refine ⟨?_, ?_⟩ · -- Adjacency. intro i hi rw [hp_len_eq] at hi by_cases hA1 : i + 1 < R · -- Both in pa. have hiR : i < R := by omega rw [hp_L i hiR, hp_L (i + 1) hA1] exact hpa_act.1 i hA1 · push_neg at hA1 by_cases hA2 : i + 1 = R · -- Seam at i = R-1: UAdj(pa[R-1]=n, pb.tail[0]=pb[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_eq]; exact hi rw [hp_R (R - 1 + 1) hi1L hi1_lt] rw [hpa_get_last] have h_yidx : R - 1 + 1 - R + 1 = 1 := by omega rw [show (⟨R - 1 + 1 - R + 1, by rw [hp_len_eq, hpb_tail_len] at hi1_lt; omega⟩ : Fin pb.length) = ⟨1, by omega⟩ from Fin.ext h_yidx] -- UAdj n pb[1] from edge pb[1] → n. exact inr hpb_in · -- Both in pb.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_eq]; omega have hi1_lt : i + 1 < p.length := by rw [hp_len_eq]; exact hi rw [hp_R i hiL hi_lt, hp_R (i + 1) hi1L hi1_lt] have hidx : (i - R + 1) + 1 < pb.length := by omega have hadj := hpb_act.1 (i - R + 1) hidx have he : (i - R + 1) + 1 = (i + 1) - R + 1 := by omega rw [show (⟨(i - R + 1) + 1, hidx⟩ : Fin pb.length) = ⟨(i + 1) - R + 1, by omega⟩ from Fin.ext he] at hadj exact hadj · -- Collider condition. intro i hi rw [hp_len_eq] at hi by_cases hC1 : i + 2 < R · -- All three in pa. 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] exact hpa_act.2 i hC1 · push_neg at hC1 by_cases hC2 : i + 2 = R · -- Seam collider: middle = pa[R-1] = n. Triple (pa[R-2], n, pb[1]). 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_eq]; exact hi rw [hp_L (R - 2) hiR, hp_L (R - 2 + 1) hi1R, hp_R (R - 2 + 2) hi2L hi2_lt] rw [show (⟨R - 2 + 1, by omega⟩ : Fin pa.length) = ⟨R - 1, by omega⟩ from Fin.ext (show R - 2 + 1 = R - 1 by omega)] rw [hpa_get_last] have h_ridx : R - 2 + 2 - R + 1 = 1 := by omega rw [show (⟨R - 2 + 2 - R + 1, by rw [hp_len_eq, hpb_tail_len] at hi2_lt; omega⟩ : Fin pb.length) = ⟨1, by omega⟩ from Fin.ext h_ridx] -- left = pa[R-2]; edge into n is hpa_in (pa[R-2]→n); right = pb[1], edge pb[1]→n. have hLeq : pa.get ⟨R - 2, by omega⟩ = pa.get ⟨pa.length - 2, by omega⟩ := by congr 1 have hColl : G.IsCollider (pa.get ⟨R - 2, by omega⟩) n (pb.get ⟨1, by omega⟩) := by refine ⟨?_, hpb_in⟩ rw [hLeq]; exact hpa_in rw [if_pos hColl] -- n ∈ bbZAncestors Z since n ∈ Z. show n ∈ G.bbZAncestors Z exact G.subset_ancestralSet Z hnZ · by_cases hC3 : i + 1 = R · -- Straddle: middle = pb.tail[0] = pb[1]. Triple (pa[R-1]=n, pb[1], pb[2]) = pb's index 0. have hi_eq : i = R - 1 := by omega subst hi_eq have hiR : R - 1 < R := by omega have hi1L : R ≤ R - 1 + 1 := by omega have hi2L : R ≤ R - 1 + 2 := by omega have hi1_lt : R - 1 + 1 < p.length := by rw [hp_len_eq]; omega have hi2_lt : R - 1 + 2 < p.length := by rw [hp_len_eq]; exact hi rw [hp_L (R - 1) hiR, hp_R (R - 1 + 1) hi1L hi1_lt, hp_R (R - 1 + 2) hi2L hi2_lt] rw [hpa_get_last] rw [show (⟨R - 1 + 1 - R + 1, by omega⟩ : Fin pb.length) = ⟨1, by omega⟩ from Fin.ext (show R - 1 + 1 - R + 1 = 1 by omega)] rw [show (⟨R - 1 + 2 - R + 1, by omega⟩ : Fin pb.length) = ⟨2, by omega⟩ from Fin.ext (show R - 1 + 2 - R + 1 = 2 by omega)] -- This matches pb's collider clause at index 0 (triple pb[0]=n, pb[1], pb[2]). have hpb0 := hpb_act.2 0 (by omega) rw [show (⟨0 + 1, by omega⟩ : Fin pb.length) = ⟨1, by omega⟩ from rfl, show (⟨0 + 2, by omega⟩ : Fin pb.length) = ⟨2, by omega⟩ from rfl] at hpb0 rw [hpb_get_0] at hpb0 exact hpb0 · -- All three in pb.tail. i ≥ R. have hiL : R ≤ i := by omega have hi1L : R ≤ i + 1 := by omega have hi2L : R ≤ i + 2 := by omega have hi_lt : i < p.length := by rw [hp_len_eq]; omega have hi1_lt : i + 1 < p.length := by rw [hp_len_eq]; omega have hi2_lt : i + 2 < p.length := by rw [hp_len_eq]; exact hi rw [hp_R i hiL hi_lt, hp_R (i + 1) hi1L hi1_lt, hp_R (i + 2) hi2L hi2_lt] have hjlen : (i - R + 1) + 2 < pb.length := by omega have hpbcoll := hpb_act.2 (i - R + 1) hjlen rw [show (⟨(i - R + 1) + 1, by omega⟩ : Fin pb.length) = ⟨(i + 1) - R + 1, by omega⟩ from Fin.ext (show (i-R+1)+1 = (i+1)-R+1 by omega), show (⟨(i - R + 1) + 2, hjlen⟩ : Fin pb.length) = ⟨(i + 2) - R + 1, by omega⟩ from Fin.ext (show (i-R+1)+2 = (i+2)-R+1 by omega)] at hpbcoll exact hpbcoll -
chain_join_activetheorem — Concatenating two active paths at a non-collider. If pa is active given Z ending at m, pb is active given Z starting at m, the first edge of pb points *out of* m (so m is a chain/fork point, not a collider), and m ∉ Z, then the glued path pa ++ pb.tail is active given Z.hypothesesZ :Finset Vm x y :Vpa pb :List Vhpa_len :pa.length ≥ 2hpa_head :pa.head? = some xhpa_last :pa.getLast? = some mhpa_act :G.IsActivePath Z pahpb_len :pb.length ≥ 2hpb_head :pb.head? = some mhpb_last :pb.getLast? = some yhpb_act :G.IsActivePath Z pbhseam_out :G.edge m (pb.get ⟨1, by omega⟩)hmZ :m ∉ Zconclusionlet p := pa ++ pb.tail p.length ≥ 2 ∧p.head? = some x ∧p.getLast? = some y ∧G.IsActivePath Z pProof (Lean source)
theorem chain_join_active {Z : Finset V} {m x y : V} {pa pb : List V} (hpa_len : pa.length ≥ 2) (hpa_head : pa.head? = some x) (hpa_last : pa.getLast? = some m) (hpa_act : G.IsActivePath Z pa) (hpb_len : pb.length ≥ 2) (hpb_head : pb.head? = some m) (hpb_last : pb.getLast? = some y) (hpb_act : G.IsActivePath Z pb) (hseam_out : G.edge m (pb.get ⟨1, by omega⟩)) (hmZ : m ∉ Z) : let p := pa ++ pb.tail p.length ≥ 2 ∧ p.head? = some x ∧ p.getLast? = some y ∧ G.IsActivePath Z p := by have hpa_ne : pa ≠ [] := by intro h; rw [h] at hpa_len; simp at hpa_len have hpb_ne : pb ≠ [] := by intro h; rw [h] at hpb_len; simp at hpb_len -- pb.head = m have hpb_head_eq : pb.head hpb_ne = m := by have h := List.head?_eq_some_head hpb_ne; rw [hpb_head] at h exact (Option.some_inj.mp h.symm) -- pa.getLast = m have hpa_last_eq : pa.getLast hpa_ne = m := by have h := getLast?_eq_some_getLast hpa_ne; rw [hpa_last] at h exact (Option.some_inj.mp h.symm) -- pa.head = x have hpa_head_eq : pa.head hpa_ne = x := by have h := List.head?_eq_some_head hpa_ne; rw [hpa_head] at h exact (Option.some_inj.mp h.symm) -- pb.getLast = y have hpb_last_eq : pb.getLast hpb_ne = y := by have h := getLast?_eq_some_getLast hpb_ne; rw [hpb_last] at h exact (Option.some_inj.mp h.symm) -- pb = m :: pb.tail have hpb_decomp : pb = m :: pb.tail := by conv_lhs => rw [← List.cons_head_tail hpb_ne]; rw [hpb_head_eq] have hpb_tail_len : pb.tail.length = pb.length - 1 := List.length_tail have hpb_tail_ne : pb.tail ≠ [] := by rw [← length_pos_iff, hpb_tail_len]; omega set p := pa ++ pb.tail with hp_def set R := pa.length with hR_def have hp_len_eq : p.length = R + pb.tail.length := by simp only [hp_def, length_append, ← hR_def] have hp_len : p.length ≥ 2 := by rw [hp_len_eq]; omega have hp_head : p.head? = some x := by have : p.head? = pa.head? := List.head?_append_of_ne_nil _ hpa_ne rw [this, hpa_head] have hp_last : p.getLast? = some y := by have hlast_tail : pb.tail.getLast? = some y := by have heq : pb = [m] ++ pb.tail := by simpa using hpb_decomp have := getLast?_append_of_ne_nil [m] hpb_tail_ne rw [← heq] at this; rw [← this]; exact hpb_last simp only [hp_def, getLast?_append, hlast_tail]; rfl refine ⟨hp_len, hp_head, hp_last, ?_⟩ -- Index translation: p[k] = pa[k] for k < R; p[k] = pb[k-R+1] for k ≥ R. have hp_L : ∀ (k : ℕ) (hkR : k < R), p.get ⟨k, by rw [hp_len_eq]; omega⟩ = pa.get ⟨k, hkR⟩ := by intro k hkR simp only [hp_def, List.get_eq_getElem, List.getElem_append_left (h := hkR)] have hpb_tail_get : ∀ (j : ℕ) (hj1 : j < pb.tail.length) (hj2 : j + 1 < pb.length), pb.tail[j]'hj1 = pb[j + 1]'hj2 := by intro j hj1 hj2 have : pb[j + 1] = (m :: pb.tail)[j + 1]'(by rw [← hpb_decomp]; exact hj2) := by congr 1 rw [this]; simp [List.getElem_cons_succ] have hp_R : ∀ (k : ℕ) (hkL : R ≤ k) (hk : k < p.length), p.get ⟨k, hk⟩ = pb.get ⟨k - R + 1, by rw [hp_len_eq, hpb_tail_len] at hk; omega⟩ := by intro k hkL hk have hk_app : R ≤ k := hkL have htail_idx_lt : k - R < pb.tail.length := by rw [hp_len_eq] at hk; omega have hpget : p.get ⟨k, hk⟩ = pb.tail[k - R]'htail_idx_lt := by simp only [hp_def, List.get_eq_getElem] rw [List.getElem_append_right (by rw [← hR_def]; exact hk_app)] rw [hpget] rw [hpb_tail_get (k - R) htail_idx_lt (by rw [hpb_tail_len] at htail_idx_lt; omega)] simp [List.get_eq_getElem] -- pb[0] = m, pa[R-1] = m. have hpb_get_0 : pb.get ⟨0, by omega⟩ = m := by rw [List.get_eq_getElem, List.getElem_zero]; exact hpb_head_eq have hpa_get_last : pa.get ⟨R - 1, by omega⟩ = m := by rw [List.get_eq_getElem] have := List.getLast_eq_getElem hpa_ne rw [hpa_last_eq] at this rw [← this] refine ⟨?_, ?_⟩ · -- Adjacency. intro i hi rw [hp_len_eq] at hi by_cases hA1 : i + 1 < R · have hiR : i < R := by omega rw [hp_L i hiR, hp_L (i + 1) hA1] exact hpa_act.1 i hA1 · push_neg at hA1 by_cases hA2 : i + 1 = R · 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_eq]; exact hi rw [hp_R (R - 1 + 1) hi1L hi1_lt] rw [hpa_get_last] have h_yidx : R - 1 + 1 - R + 1 = 1 := by omega rw [show (⟨R - 1 + 1 - R + 1, by rw [hp_len_eq, hpb_tail_len] at hi1_lt; omega⟩ : Fin pb.length) = ⟨1, by omega⟩ from Fin.ext h_yidx] exact Or.inl hseam_out · have hiL : R ≤ i := by omega have hi1L : R ≤ i + 1 := by omega have hi_lt : i < p.length := by rw [hp_len_eq]; omega have hi1_lt : i + 1 < p.length := by rw [hp_len_eq]; exact hi rw [hp_R i hiL hi_lt, hp_R (i + 1) hi1L hi1_lt] have hidx : (i - R + 1) + 1 < pb.length := by omega have hadj := hpb_act.1 (i - R + 1) hidx have he : (i - R + 1) + 1 = (i + 1) - R + 1 := by omega rw [show (⟨(i - R + 1) + 1, hidx⟩ : Fin pb.length) = ⟨(i + 1) - R + 1, by omega⟩ from Fin.ext he] at hadj exact hadj · -- Collider condition. intro i hi rw [hp_len_eq] at hi by_cases hC1 : i + 2 < R · 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] exact hpa_act.2 i hC1 · push_neg at hC1 by_cases hC2 : i + 2 = R · 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_eq]; exact hi rw [hp_L (R - 2) hiR, hp_L (R - 2 + 1) hi1R, hp_R (R - 2 + 2) hi2L hi2_lt] rw [show (⟨R - 2 + 1, by omega⟩ : Fin pa.length) = ⟨R - 1, by omega⟩ from Fin.ext (show R - 2 + 1 = R - 1 by omega)] rw [hpa_get_last] have h_ridx : R - 2 + 2 - R + 1 = 1 := by omega rw [show (⟨R - 2 + 2 - R + 1, by rw [hp_len_eq, hpb_tail_len] at hi2_lt; omega⟩ : Fin pb.length) = ⟨1, by omega⟩ from Fin.ext h_ridx] have hNotColl : ¬ G.IsCollider (pa.get ⟨R - 2, by omega⟩) m (pb.get ⟨1, by omega⟩) := by intro hColl exact (G.asymm hseam_out) hColl.2 rw [if_neg hNotColl] exact hmZ · by_cases hC3 : i + 1 = R · have hi_eq : i = R - 1 := by omega subst hi_eq have hiR : R - 1 < R := by omega have hi1L : R ≤ R - 1 + 1 := by omega have hi2L : R ≤ R - 1 + 2 := by omega have hi1_lt : R - 1 + 1 < p.length := by rw [hp_len_eq]; omega have hi2_lt : R - 1 + 2 < p.length := by rw [hp_len_eq]; exact hi rw [hp_L (R - 1) hiR, hp_R (R - 1 + 1) hi1L hi1_lt, hp_R (R - 1 + 2) hi2L hi2_lt] rw [hpa_get_last] rw [show (⟨R - 1 + 1 - R + 1, by omega⟩ : Fin pb.length) = ⟨1, by omega⟩ from Fin.ext (show R - 1 + 1 - R + 1 = 1 by omega)] rw [show (⟨R - 1 + 2 - R + 1, by omega⟩ : Fin pb.length) = ⟨2, by omega⟩ from Fin.ext (show R - 1 + 2 - R + 1 = 2 by omega)] have hpb0 := hpb_act.2 0 (by omega) rw [show (⟨0 + 1, by omega⟩ : Fin pb.length) = ⟨1, by omega⟩ from rfl, show (⟨0 + 2, by omega⟩ : Fin pb.length) = ⟨2, by omega⟩ from rfl] at hpb0 rw [hpb_get_0] at hpb0 exact hpb0 · have hiL : R ≤ i := by omega have hi1L : R ≤ i + 1 := by omega have hi2L : R ≤ i + 2 := by omega have hi_lt : i < p.length := by rw [hp_len_eq]; omega have hi1_lt : i + 1 < p.length := by rw [hp_len_eq]; omega have hi2_lt : i + 2 < p.length := by rw [hp_len_eq]; exact hi rw [hp_R i hiL hi_lt, hp_R (i + 1) hi1L hi1_lt, hp_R (i + 2) hi2L hi2_lt] have hjlen : (i - R + 1) + 2 < pb.length := by omega have hpbcoll := hpb_act.2 (i - R + 1) hjlen rw [show (⟨(i - R + 1) + 1, by omega⟩ : Fin pb.length) = ⟨(i + 1) - R + 1, by omega⟩ from Fin.ext (show (i-R+1)+1 = (i+1)-R+1 by omega), show (⟨(i - R + 1) + 2, hjlen⟩ : Fin pb.length) = ⟨(i + 2) - R + 1, by omega⟩ from Fin.ext (show (i-R+1)+2 = (i+2)-R+1 by omega)] at hpbcoll exact hpbcoll -
node_isAncestor_last_of_directedtheorem — Every vertex on a forward directed path is either the path's endpoint or a strict ancestor of that endpoint.hypothesesq :List Vw :Vhlen :q.length ≥ 2hlast :q.getLast? = some whedge :∀ (i : ℕ) (hi : i + 1 < q.length), G.edge (q.get ⟨i, by omega⟩) (q.get ⟨i + 1, hi⟩)j :ℕhj :j < q.lengthconclusionG.isAncestor (q.get ⟨j, hj⟩) w ∨ q.get ⟨j, hj⟩ = wProof (Lean source)
theorem node_isAncestor_last_of_directed {q : List V} {w : V} (hlen : q.length ≥ 2) (hlast : q.getLast? = some w) (hedge : ∀ (i : ℕ) (hi : i + 1 < q.length), G.edge (q.get ⟨i, by omega⟩) (q.get ⟨i + 1, hi⟩)) (j : ℕ) (hj : j < q.length) : G.isAncestor (q.get ⟨j, hj⟩) w ∨ q.get ⟨j, hj⟩ = w := by by_cases hjlast : j = q.length - 1 · right have hqne : q ≠ [] := by intro h; rw [h] at hlen; simp at hlen have hh := getLast?_eq_some_getLast hqne rw [hlast] at hh have hw_eq : q.getLast hqne = w := Option.some_inj.mp hh.symm have hidx : (⟨j, hj⟩ : Fin q.length) = ⟨q.length - 1, by omega⟩ := Fin.ext (by omega) rw [hidx, List.get_eq_getElem, ← hw_eq, List.getLast_eq_getElem] · have hj1 : j + 1 < q.length := by omega have he := hedge j hj1 rcases node_isAncestor_last_of_directed hlen hlast hedge (j + 1) hj1 with h | h · exact inl (G.isAncestor_trans (isAncestor.edge he) h) · exact inl (h ▸ isAncestor.edge he) termination_by q.length - j decreasing_by omega -
isActivePath_taketheorem — Every prefix of an active path is active.hypothesesconclusionG.IsActivePath Z (p.take k)Proof (Lean source)
theorem isActivePath_take {Z : Finset V} {p : List V} {k : ℕ} (hact : G.IsActivePath Z p) : G.IsActivePath Z (p.take k) := by obtain ⟨hadj, hcoll⟩ := hact have hle : (p.take k).length ≤ p.length := by rw [List.length_take]; exact min_le_right k p.length have hget : ∀ (j : ℕ) (hj : j < (p.take k).length), (p.take k).get ⟨j, hj⟩ = p.get ⟨j, by omega⟩ := by intro j hj simp only [List.get_eq_getElem, List.getElem_take] refine ⟨fun i hi => ?_, fun i hi => ?_⟩ · rw [hget i (by omega), hget (i + 1) hi] exact hadj i (by omega) · rw [hget i (by omega), hget (i + 1) (by omega), hget (i + 2) hi] exact hcoll i (by omega) -
branch_seed_eqtheorem — If a finite set contains a node, removing and then reinserting that node while taking unions recovers the same union as using the original set.hypothesesconclusiona ∪ {n} ∪ (Zr.erase n ∪ b) ∪ c = a ∪ b ∪ Zr ∪ cProof (Lean source)
theorem branch_seed_eq {a b Zr c : Finset V} {n : V} (hn : n ∈ Zr) : a ∪ {n} ∪ (Zr.erase n ∪ b) ∪ c = a ∪ b ∪ Zr ∪ c := by ext x; simp only [mem_union, mem_singleton, Finset.mem_erase] constructor · rintro (((h | h) | (h | h)) | h) · exact inl (inl (inl h)) · exact inl (inr (h ▸ hn)) · exact inl (inr h.2) · exact inl (inl (inr h)) · exact inr h · rintro (((h | h) | h) | h) · exact inl (inl (inl h)) · exact inl (inr (inr h)) · by_cases hx : x = n · exact inl (inl (inr hx)) · exact inl (inr (inl ⟨hx, h⟩)) · exact inr h -
bbReachable_extend_directed_armtheorem — Extending an active path by a directed arm at a non-collider seam.hypothesesZ :Finset Va c b :Vpa q :List Vhpa_len :pa.length ≥ 2hpa_head :pa.head? = some ahpa_last :pa.getLast? = some chpa_act :G.IsActivePath Z pahq_len :q.length ≥ 2hq_head :q.head? = some chq_last :q.getLast? = some bhq_edge :∀ (i : ℕ) (hi : i + 1 < q.length), G.edge (q.get ⟨i, by omega⟩) (q.get ⟨i + 1, hi⟩)hq_int :∀ (i : ℕ) (hi : i + 2 < q.length), q.get ⟨i + 1, by omega⟩ ∉ ZhcZ :c ∉ Zconclusionb ∈ G.bbReachableVertices Z ({a} : Finset V)Proof (Lean source)
theorem bbReachable_extend_directed_arm {Z : Finset V} {a c b : V} {pa q : List V} (hpa_len : pa.length ≥ 2) (hpa_head : pa.head? = some a) (hpa_last : pa.getLast? = some c) (hpa_act : G.IsActivePath Z pa) (hq_len : q.length ≥ 2) (hq_head : q.head? = some c) (hq_last : q.getLast? = some b) (hq_edge : ∀ (i : ℕ) (hi : i + 1 < q.length), G.edge (q.get ⟨i, by omega⟩) (q.get ⟨i + 1, hi⟩)) (hq_int : ∀ (i : ℕ) (hi : i + 2 < q.length), q.get ⟨i + 1, by omega⟩ ∉ Z) (hcZ : c ∉ Z) : b ∈ G.bbReachableVertices Z ({a} : Finset V) := by have hq_act : G.IsActivePath Z q := G.isActivePath_of_directed hq_edge hq_int have hqne : q ≠ [] := by intro h; rw [h] at hq_len; simp at hq_len -- First edge of `q` points out of `c`. have hq_head_eq : q.get ⟨0, by omega⟩ = c := by have h := List.head?_eq_some_head hqne rw [hq_head] at h rw [List.get_eq_getElem, List.getElem_zero] exact Option.some_inj.mp h.symm have hseam_out : G.edge c (q.get ⟨1, by omega⟩) := by have he := hq_edge 0 (by omega) rwa [hq_head_eq] at he obtain ⟨_, hjhead, hjlast, hjact⟩ := G.chain_join_active hpa_len hpa_head hpa_last hpa_act hq_len hq_head hq_last hq_act hseam_out hcZ rw [G.bbReachableVertices_iff_activePath] exact ⟨a, mem_singleton_self a, pa ++ q.tail, by rw [length_append]; have := length_tail (l := q); omega, hjact, hjhead, hjlast⟩