DependencyGraph.lean

1 import Mathlib.Data.Finset.Card
2 import Mathlib.Data.Fintype.Powerset
3 import Mathlib.Data.Int.Basic
4 
5 /-! # A finite, declared dependency graph and its exact forward invalidation
6 
7 Artifact values are heterogeneous and compared on the actual direct-input restriction.
8 The closure algorithm does not assume acyclicity. A rank certificate is used separately
9 for sound reuse and topological restoration, not as a substitute for declared inputs.
10 -/
11 namespace Komorebi.MachineTheory.Dependency
12 open Finset
13 
14 variable {V I : Type*} [Fintype V] [DecidableEq V]
15 
16 structure Graph (V I : Type*) where
17   parents : V → Finset V
18   direct : V → Finset I
19 
20 /-- An explicitly checkable topological rank is a certificate of acyclicity. -/
21 def Graph.Ranked (G : Graph V I) (rank : V → ℕ) : Prop :=
22   ∀ v u, u ∈ G.parents v → rank u < rank v
23 
24 /-- One synchronous forward propagation, including the old affected set. -/
25 def expand (parents : V → Finset V) (S : Finset V) : Finset V :=
26   S ∪ univ.filter (fun v => ∃ u ∈ parents v, u ∈ S)
27 
28 def stages (parents : V → Finset V) (seed : Finset V) : ℕ → Finset V
29   | 0 => seed
30   | n+1 => expand parents (stages parents seed n)
31 
32 @[simp] theorem mem_expand (parents : V → Finset V) (S : Finset V) (v : V) :
33     v ∈ expand parents S ↔ v ∈ S ∨ ∃ u ∈ parents v, u ∈ S := by
34   simp [expand]
35 
36 theorem subset_expand (parents : V → Finset V) (S : Finset V) : S ⊆ expand parents S := by
37   intro v hv
38   exact (mem_expand parents S v).mpr (Or.inl hv)
39 
40 theorem expand_mono (parents : V → Finset V) {S T : Finset V} (h : S ⊆ T) :
41     expand parents S ⊆ expand parents T := by
42   intro v hv
43   rcases (mem_expand parents S v).mp hv with hv | ⟨u,hu,hs⟩
44   · exact (mem_expand parents T v).mpr (Or.inl (h hv))
45   · exact (mem_expand parents T v).mpr (Or.inr ⟨u,hu,h hs⟩)
46 
47 theorem stages_step (parents : V → Finset V) (seed : Finset V) (n : ℕ) :
48     stages parents seed n ⊆ stages parents seed (n+1) := subset_expand parents _
49 
50 theorem seed_subset_stages (parents : V → Finset V) (seed : Finset V) (n : ℕ) :
51     seed ⊆ stages parents seed n := by
52   induction n with
53   | zero => exact Subset.refl _
54   | succ n ih => exact Subset.trans ih (stages_step parents seed n)
55 
56 theorem bounded_stabilization (parents : V → Finset V) (seed : Finset V) :
57     ∃ n ≤ Fintype.card V - seed.card,
58       expand parents (stages parents seed n) = stages parents seed n := by
59   by_contra h
60   push Not at h
61   let b := Fintype.card V - seed.card
62   have growth : ∀ n, n ≤ b+1 → seed.card+n ≤ (stages parents seed n).card := by
63     intro n
64     induction n with
65     | zero => intro _; simp [stages]
66     | succ n ih =>
67       intro hn
68       have hn' : n ≤ b := by omega
69       have hh := h n hn'
70       have sub := stages_step parents seed n
71       have strict : (stages parents seed n).card < (stages parents seed (n+1)).card := by
72         by_contra hc
73         have eq := Finset.eq_of_subset_of_card_le sub (by omega)
74         exact hh eq.symm
75       have previous := ih (by omega)
76       omega
77   have impossible := growth (b+1) le_rfl
78   have top := Finset.card_le_univ (stages parents seed (b+1))
79   have start := Finset.card_le_univ seed
80   dsimp [b] at impossible top
81   omega
82 
83 theorem stable_tail (parents : V → Finset V) (seed : Finset V) (n : ℕ)
84     (hs : expand parents (stages parents seed n) = stages parents seed n) :
85     ∀ k, stages parents seed (n+k) = stages parents seed n := by
86   intro k
87   induction k with
88   | zero => simp
89   | succ k ih =>
90     change expand parents (stages parents seed (n+k)) = _
91     rw [ih,hs]
92 
93 /-- A fixed number of rounds, with no chosen stopping index or reachability oracle. -/
94 def closure (parents : V → Finset V) (seed : Finset V) : Finset V :=
95   stages parents seed (Fintype.card V)
96 
97 theorem closure_stable (parents : V → Finset V) (seed : Finset V) :
98     expand parents (closure parents seed) = closure parents seed := by
99   obtain ⟨n,hn,hs⟩ := bounded_stabilization parents seed
100   have hn' : n ≤ Fintype.card V := le_trans hn (Nat.sub_le _ _)
101   have eq : closure parents seed = stages parents seed n := by
102     simpa [closure,Nat.add_sub_of_le hn'] using stable_tail parents seed n hs (Fintype.card V-n)
103   rw [eq,hs]
104 
105 theorem seed_subset_closure (parents : V → Finset V) (seed : Finset V) :
106     seed ⊆ closure parents seed := seed_subset_stages parents seed _
107 
108 theorem closure_parent (parents : V → Finset V) (seed : Finset V) {u v : V}
109     (hu : u ∈ closure parents seed) (hp : u ∈ parents v) : v ∈ closure parents seed := by
110   rw [← closure_stable parents seed]
111   exact (mem_expand parents _ v).mpr (Or.inr ⟨u,hp,hu⟩)
112 
113 theorem closure_least (parents : V → Finset V) (seed T : Finset V)
114     (hseed : seed ⊆ T) (hclosed : ∀ v u, u ∈ parents v → u ∈ T → v ∈ T) :
115     closure parents seed ⊆ T := by
116   have step : ∀ n, stages parents seed n ⊆ T := by
117     intro n
118     induction n with
119     | zero => exact hseed
120     | succ n ih =>
121       intro v hv
122       rcases (mem_expand parents _ v).mp hv with hv | ⟨u,hp,hu⟩
123       · exact ih hv
124       · exact hclosed v u hp (ih hu)
125   exact step _
126 
127 /-- Semantic forward paths from a changed direct-input vertex. -/
128 inductive Reach (parents : V → Finset V) (seed : Finset V) : V → Prop
129   | root (v) : v ∈ seed → Reach parents seed v
130   | edge {u v} : Reach parents seed u → u ∈ parents v → Reach parents seed v
131 
132 theorem closure_iff_reach (parents : V → Finset V) (seed : Finset V) (v : V) :
133     v ∈ closure parents seed ↔ Reach parents seed v := by
134   constructor
135   · have all : ∀ n v, v ∈ stages parents seed n → Reach parents seed v := by
136       intro n
137       induction n with
138       | zero => intro v hv; exact Reach.root v hv
139       | succ n ih =>
140         intro v hv
141         rcases (mem_expand parents _ v).mp hv with hv | ⟨u,hp,hu⟩
142         · exact ih v hv
143         · exact Reach.edge (ih u hu) hp
144     exact all _ v
145   · intro h
146     induction h with
147     | root v hv => exact seed_subset_closure parents seed hv
148     | edge _ hp ih => exact closure_parent parents seed ih hp
149 
150 theorem closure_mono (parents : V → Finset V) {S T : Finset V} (h : S ⊆ T) :
151     closure parents S ⊆ closure parents T :=
152   closure_least parents S _ (Subset.trans h (seed_subset_closure parents T))
153     (fun _ _ hp hu => closure_parent parents T hu hp)
154 
155 theorem no_stale_parent (parents : V → Finset V) (seed : Finset V) {v : V}
156     (hv : v ∉ closure parents seed) {u : V} (hu : u ∈ parents v) :
157     u ∉ closure parents seed := fun hs => hv (closure_parent parents seed hs hu)
158 
159 variable {A : I → Type*} [∀ i, DecidableEq (A i)]
160 
161 /-- The actual values visible to this local witness checker. -/
162 def Graph.view (G : Graph V I) (a : ∀ i, A i) (v : V) :
163     (i : {i // i ∈ G.direct v}) → A i.val := fun i => a i.val
164 
165 def Graph.changedRoots (G : Graph V I) (a b : ∀ i, A i) : Finset V :=
166   univ.filter (fun v => ∃ i ∈ G.direct v, a i ≠ b i)
167 
168 def Graph.stale (G : Graph V I) (a b : ∀ i, A i) : Finset V :=
169   closure G.parents (G.changedRoots a b)
170 
171 omit [DecidableEq V] in
172 @[simp] theorem Graph.mem_changedRoots (G : Graph V I) (a b : ∀ i, A i) (v : V) :
173     v ∈ G.changedRoots a b ↔ ∃ i ∈ G.direct v, a i ≠ b i := by simp [changedRoots]
174 
175 theorem Graph.nonstale_view (G : Graph V I) (a b : ∀ i, A i) {v : V}
176     (hv : v ∉ G.stale a b) : G.view a v = G.view b v := by
177   funext i
178   by_contra he
179   apply hv
180   apply seed_subset_closure G.parents (G.changedRoots a b)
181   exact (G.mem_changedRoots a b v).mpr ⟨i.val,i.property,he⟩
182 
183 theorem Graph.nonstale_parents (G : Graph V I) (a b : ∀ i, A i) {v : V}
184     (hv : v ∉ G.stale a b) {u : V} (hu : u ∈ G.parents v) : u ∉ G.stale a b :=
185   no_stale_parent G.parents (G.changedRoots a b) hv hu
186 
187 theorem Graph.stale_iff (G : Graph V I) (a b : ∀ i, A i) (v : V) :
188     v ∈ G.stale a b ↔ Reach G.parents (G.changedRoots a b) v :=
189   closure_iff_reach _ _ _
190 
191 theorem Graph.same_state_not_stale (G : Graph V I) (a : ∀ i, A i) : G.stale a a = ∅ := by
192   apply Finset.Subset.antisymm ?_ (Finset.empty_subset _)
193   exact closure_least G.parents (G.changedRoots a a) ∅
194     (by simp [changedRoots]) (by simp)
195 
196 end Komorebi.MachineTheory.Dependency

Back to source controls