SafeEnding.lean

1 import MachineTheory.FiniteFixedPoints
2 
3 /-! Core 8.3: the two actual finite fixed points and their policy witnesses.
4 The post sets of enabled actions are nonempty. An empty action catalogue is
5 permitted and represents a deadlock, not a vacuous successful transition.
6 The goal is reached at first arrival; no post-goal execution obligation is added.
7 -/
8 namespace Komorebi.MachineTheory.SafeEnding
9 
10 open FiniteFixedPoints
11 
12 universe u v
13 
14 structure Model (Z : Type u) (A : Type v) where
15   safe : Finset Z
16   goal : Finset Z
17   goal_safe : goal ⊆ safe
18   run : Z → Finset A
19   finish : Z → Finset A
20   post : Z → A → Finset Z
21   post_nonempty : ∀ x a, a ∈ run x ∨ a ∈ finish x → (post x a).Nonempty
22 
23 variable {Z : Type u} {A : Type v}
24 noncomputable section
25 
26 /-- An ending predecessor must select its action before its adversarial successor. -/
27 def endStep (M : Model Z A) (U : Finset Z) : Finset Z := by
28   classical
29   exact U ∪ M.safe.filter (fun x => ∃ a ∈ M.finish x, M.post x a ⊆ U)
30 
31 theorem mem_endStep (M : Model Z A) (U : Finset Z) (x : Z) :
32     x ∈ endStep M U ↔ x ∈ U ∨
33       (x ∈ M.safe ∧ ∃ a ∈ M.finish x, M.post x a ⊆ U) := by
34   classical
35   simp only [endStep, Finset.mem_union, Finset.mem_filter]
36 
37 theorem endStep_increasing (M : Model Z A) (U : Finset Z) : U ⊆ endStep M U :=
38   fun x hx => (mem_endStep M U x).mpr (Or.inl hx)
39 
40 def endStage (M : Model Z A) : ℕ → Finset Z := sequence (endStep M) M.goal
41 
42 @[simp] theorem endStage_zero (M : Model Z A) : endStage M 0 = M.goal := rfl
43 @[simp] theorem endStage_succ (M : Model Z A) (n : ℕ) :
44     endStage M (n + 1) = endStep M (endStage M n) := rfl
45 
46 theorem endStage_safe (M : Model Z A) (n : ℕ) : endStage M n ⊆ M.safe := by
47   induction n with
48   | zero => exact M.goal_safe
49   | succ n ih =>
50     intro x hx
51     rcases (mem_endStep M _ x).mp hx with old | new
52     · exact ih old
53     · exact new.1
54 
55 theorem ending_stabilizes [Fintype Z] (M : Model Z A) :
56     ∃ n ≤ Fintype.card Z - M.goal.card,
57       endStep M (endStage M n) = endStage M n :=
58   increasing_stabilization (endStep M) M.goal (endStep_increasing M)
59 
60 def endIndex [Fintype Z] (M : Model Z A) : ℕ := by
61   classical
62   exact Nat.find (ending_stabilizes M)
63 
64 def endingRegion [Fintype Z] (M : Model Z A) : Finset Z := endStage M (endIndex M)
65 
66 theorem endIndex_bound [Fintype Z] (M : Model Z A) :
67     endIndex M ≤ Fintype.card Z - M.goal.card := by
68   classical
69   exact (Nat.find_spec (ending_stabilizes M)).1
70 
71 theorem endingRegion_fixed [Fintype Z] (M : Model Z A) :
72     endStep M (endingRegion M) = endingRegion M := by
73   classical
74   exact (Nat.find_spec (ending_stabilizes M)).2
75 
76 theorem endingRegion_safe [Fintype Z] (M : Model Z A) : endingRegion M ⊆ M.safe :=
77   endStage_safe M (endIndex M)
78 
79 theorem endStage_subset_region [Fintype Z] (M : Model Z A) (n : ℕ) :
80     endStage M n ⊆ endingRegion M := by
81   induction n with
82   | zero =>
83     have hs : ∀ k, M.goal ⊆ endStage M k := by
84       intro k
85       induction k with
86       | zero => exact Finset.Subset.refl _
87       | succ k ih => exact Finset.Subset.trans ih (endStep_increasing M _)
88     exact hs (endIndex M)
89   | succ n ih =>
90     intro x hx
91     rcases (mem_endStep M _ x).mp hx with old | new
92     · exact ih old
93     · have h : x ∈ endStep M (endingRegion M) := by
94         apply (mem_endStep M _ x).mpr
95         right
96         obtain ⟨hs, a, ha, hp⟩ := new
97         exact ⟨hs, a, ha, Finset.Subset.trans hp ih⟩
98       rwa [endingRegion_fixed] at h
99 
100 theorem goal_subset_region [Fintype Z] (M : Model Z A) : M.goal ⊆ endingRegion M :=
101   endStage_subset_region M 0
102 
103 theorem endingRegion_of_pre [Fintype Z] (M : Model Z A) {x : Z} {a : A}
104     (hs : x ∈ M.safe) (ha : a ∈ M.finish x) (hp : M.post x a ⊆ endingRegion M) :
105     x ∈ endingRegion M := by
106   have h := (mem_endStep M (endingRegion M) x).mpr (Or.inr ⟨hs, a, ha, hp⟩)
107   rwa [endingRegion_fixed] at h
108 
109 /-- Every chosen ending action at a safe state outside the attractor has a real
110 successor outside it. No successor is selected before the action is known. -/
111 theorem outside_successor [Fintype Z] (M : Model Z A) {x : Z} {a : A}
112     (hs : x ∈ M.safe) (hx : x ∉ endingRegion M) (ha : a ∈ M.finish x) :
113     ∃ y ∈ M.post x a, y ∉ endingRegion M := by
114   classical
115   by_contra h
116   apply hx
117   apply endingRegion_of_pre M hs ha
118   intro y hy
119   by_contra hn
120   exact h ⟨y, hy, hn⟩
121 
122 /-- First-entry rank is defined on all states, with the unused outside value zero. -/
123 def endRank [Fintype Z] (M : Model Z A) (x : Z) : ℕ := by
124   classical
125   exact if hx : x ∈ endingRegion M then
126     Nat.find (show ∃ n, x ∈ endStage M n from ⟨endIndex M, hx⟩)
127   else 0
128 
129 theorem endRank_spec [Fintype Z] (M : Model Z A) {x : Z} (hx : x ∈ endingRegion M) :
130     x ∈ endStage M (endRank M x) := by
131   classical
132   simp only [endRank, dite_eq_left hx]
133   exact Nat.find_spec (show ∃ n, x ∈ endStage M n from ⟨endIndex M, hx⟩)
134 
135 theorem endRank_min [Fintype Z] (M : Model Z A) {x : Z} {n : ℕ}
136     (hn : x ∈ endStage M n) : endRank M x ≤ n := by
137   classical
138   have hx := endStage_subset_region M n hn
139   simp only [endRank, dite_eq_left hx]
140   exact Nat.find_min' _ hn
141 
142 theorem endRank_bound [Fintype Z] (M : Model Z A) {x : Z} (hx : x ∈ endingRegion M) :
143     endRank M x ≤ Fintype.card Z - M.goal.card :=
144   le_trans (endRank_min M hx) (endIndex_bound M)
145 
146 theorem endRank_zero_iff [Fintype Z] (M : Model Z A) {x : Z}
147     (hx : x ∈ endingRegion M) : endRank M x = 0 ↔ x ∈ M.goal := by
148   constructor
149   · intro hz
150     have hs := endRank_spec M hx
151     rwa [hz, endStage_zero] at hs
152   · intro hg
153     exact Nat.eq_zero_of_le_zero (endRank_min M (n := 0) hg)
154 
155 /-- A single action lowers rank for every successor, not one action per successor. -/
156 theorem rank_action [Fintype Z] (M : Model Z A) {x : Z}
157     (hx : x ∈ endingRegion M) (hg : x ∉ M.goal) :
158     ∃ a ∈ M.finish x, ∀ y ∈ M.post x a,
159       y ∈ endingRegion M ∧ endRank M y < endRank M x := by
160   cases hr : endRank M x with
161   | zero => exact False.elim (hg ((endRank_zero_iff M hx).mp hr))
162   | succ n =>
163     have hm := endRank_spec M hx
164     rw [hr, endStage_succ] at hm
165     rcases (mem_endStep M _ x).mp hm with old | new
166     · have hle := endRank_min M old
167       omega
168     · obtain ⟨_, a, ha, hp⟩ := new
169       refine ⟨a, ha, ?_⟩
170       intro y hy
171       have hs := hp hy
172       refine ⟨endStage_subset_region M n hs, ?_⟩
173       have hle := endRank_min M hs
174       omega
175 
176 def endingAction [Fintype Z] (M : Model Z A) (x : Z) : Option A := by
177   classical
178   exact if hx : x ∈ endingRegion M then
179     if hg : x ∈ M.goal then none else some (Classical.choose (rank_action M hx hg))
180   else none
181 
182 theorem endingAction_spec [Fintype Z] (M : Model Z A) {x : Z}
183     (hx : x ∈ endingRegion M) (hg : x ∉ M.goal) :
184     ∃ a, endingAction M x = some a ∧ a ∈ M.finish x ∧
185       ∀ y ∈ M.post x a, y ∈ endingRegion M ∧ endRank M y < endRank M x := by
186   classical
187   refine ⟨Classical.choose (rank_action M hx hg), ?_, ?_⟩
188   · simp only [endingAction, dite_eq_left hx, dite_eq_right hg]
189   · exact Classical.choose_spec (rank_action M hx hg)
190 
191 /-- Running removes states that cannot keep every successor in the current region. -/
192 def runStep (M : Model Z A) (U : Finset Z) : Finset Z := by
193   classical
194   exact U.filter (fun x => ∃ a ∈ M.run x, M.post x a ⊆ U)
195 
196 theorem mem_runStep (M : Model Z A) (U : Finset Z) (x : Z) :
197     x ∈ runStep M U ↔ x ∈ U ∧ ∃ a ∈ M.run x, M.post x a ⊆ U := by
198   classical
199   simp only [runStep, Finset.mem_filter]
200 
201 theorem runStep_decreasing (M : Model Z A) (U : Finset Z) : runStep M U ⊆ U :=
202   fun x hx => ((mem_runStep M U x).mp hx).1
203 
204 def runStage [Fintype Z] (M : Model Z A) : ℕ → Finset Z :=
205   sequence (runStep M) (endingRegion M)
206 
207 @[simp] theorem runStage_zero [Fintype Z] (M : Model Z A) : runStage M 0 = endingRegion M := rfl
208 @[simp] theorem runStage_succ [Fintype Z] (M : Model Z A) (n : ℕ) :
209     runStage M (n + 1) = runStep M (runStage M n) := rfl
210 
211 theorem running_stabilizes [Fintype Z] (M : Model Z A) :
212     ∃ n ≤ (endingRegion M).card, runStep M (runStage M n) = runStage M n :=
213   decreasing_stabilization (runStep M) (endingRegion M) (runStep_decreasing M)
214 
215 def runIndex [Fintype Z] (M : Model Z A) : ℕ := by
216   classical
217   exact Nat.find (running_stabilizes M)
218 
219 def runningRegion [Fintype Z] (M : Model Z A) : Finset Z := runStage M (runIndex M)
220 
221 theorem runIndex_bound [Fintype Z] (M : Model Z A) :
222     runIndex M ≤ (endingRegion M).card := by
223   classical
224   exact (Nat.find_spec (running_stabilizes M)).1
225 
226 theorem runningRegion_fixed [Fintype Z] (M : Model Z A) :
227     runStep M (runningRegion M) = runningRegion M := by
228   classical
229   exact (Nat.find_spec (running_stabilizes M)).2
230 
231 theorem runStage_subset_ending [Fintype Z] (M : Model Z A) (n : ℕ) :
232     runStage M n ⊆ endingRegion M := by
233   induction n with
234   | zero => exact Finset.Subset.refl _
235   | succ n ih => exact Finset.Subset.trans (runStep_decreasing M _) ih
236 
237 theorem runningRegion_subset_ending [Fintype Z] (M : Model Z A) :
238     runningRegion M ⊆ endingRegion M := runStage_subset_ending M _
239 
240 theorem runningRegion_safe [Fintype Z] (M : Model Z A) :
241     runningRegion M ⊆ M.safe := Finset.Subset.trans (runningRegion_subset_ending M) (endingRegion_safe M)
242 
243 theorem running_action [Fintype Z] (M : Model Z A) {x : Z} (hx : x ∈ runningRegion M) :
244     ∃ a ∈ M.run x, M.post x a ⊆ runningRegion M := by
245   have hh : x ∈ runStep M (runningRegion M) := by rwa [runningRegion_fixed]
246   exact ((mem_runStep M _ x).mp hh).2
247 
248 def runningAction [Fintype Z] (M : Model Z A) (x : Z) : Option A := by
249   classical
250   exact if hx : x ∈ runningRegion M then some (Classical.choose (running_action M hx)) else none
251 
252 theorem runningAction_spec [Fintype Z] (M : Model Z A) {x : Z} (hx : x ∈ runningRegion M) :
253     ∃ a, runningAction M x = some a ∧ a ∈ M.run x ∧ M.post x a ⊆ runningRegion M := by
254   classical
255   refine ⟨Classical.choose (running_action M hx), ?_, ?_⟩
256   · simp only [runningAction, dite_eq_left hx]
257   · exact Classical.choose_spec (running_action M hx)
258 
259 /-- Any set of histories whose current states stay in the ending region and
260 admit safe continuation is contained in the computed running region. -/
261 theorem running_maximal [Fintype Z] (M : Model Z A) (R : Z → Prop)
262     (hEnd : ∀ x, R x → x ∈ endingRegion M)
263     (hRun : ∀ x, R x → ∃ a ∈ M.run x, ∀ y ∈ M.post x a, R y) :
264     ∀ x, R x → x ∈ runningRegion M := by
265   have hstage : ∀ n x, R x → x ∈ runStage M n := by
266     intro n
267     induction n with
268     | zero => exact hEnd
269     | succ n ih =>
270       intro x hx
271       apply (mem_runStep M _ x).mpr
272       obtain ⟨a, ha, hp⟩ := hRun x hx
273       exact ⟨ih x hx, a, ha, fun y hy => ih y (hp y hy)⟩
274   exact hstage (runIndex M)
275 
276 
277 /-- The ending update is monotone in the target set. -/
278 theorem endStep_mono (M : Model Z A) {U V : Finset Z} (h : U ⊆ V) :
279     endStep M U ⊆ endStep M V := by
280   intro x hx
281   rcases (mem_endStep M U x).mp hx with old | new
282   · exact (mem_endStep M V x).mpr (Or.inl (h old))
283   · obtain ⟨hs, a, ha, hp⟩ := new
284     exact (mem_endStep M V x).mpr (Or.inr ⟨hs, a, ha, Finset.Subset.trans hp h⟩)
285 
286 theorem goal_subset_stage (M : Model Z A) (n : ℕ) : M.goal ⊆ endStage M n := by
287   induction n with
288   | zero => exact Finset.Subset.refl _
289   | succ n ih => exact Finset.Subset.trans ih (endStep_increasing M _)
290 
291 /-- An explicit finite fixed-point certificate identifies the actual attractor. -/
292 theorem endingRegion_eq_of_stage_fixed [Fintype Z] (M : Model Z A) (n : ℕ)
293     (hn : endStep M (endStage M n) = endStage M n) : endingRegion M = endStage M n := by
294   apply Finset.Subset.antisymm
295   · have inv : ∀ k, endStage M k ⊆ endStage M n := by
296       intro k
297       induction k with
298       | zero => exact goal_subset_stage M n
299       | succ k ih =>
300         have hs := endStep_mono M ih
301         rwa [hn] at hs
302     exact inv (endIndex M)
303   · exact endStage_subset_region M n
304 
305 theorem runStep_mono (M : Model Z A) {U V : Finset Z} (h : U ⊆ V) :
306     runStep M U ⊆ runStep M V := by
307   intro x hx
308   obtain ⟨hx, a, ha, hp⟩ := (mem_runStep M U x).mp hx
309   exact (mem_runStep M V x).mpr ⟨h hx, a, ha, Finset.Subset.trans hp h⟩
310 
311 theorem runningRegion_subset_stage [Fintype Z] (M : Model Z A) (n : ℕ) :
312     runningRegion M ⊆ runStage M n := by
313   induction n with
314   | zero => exact runningRegion_subset_ending M
315   | succ n ih =>
316     have hs := runStep_mono M ih
317     rwa [runningRegion_fixed] at hs
318 
319 /-- An explicit finite viability fixed point identifies the actual running region. -/
320 theorem runningRegion_eq_of_stage_fixed [Fintype Z] (M : Model Z A) (n : ℕ)
321     (hn : runStep M (runStage M n) = runStage M n) : runningRegion M = runStage M n := by
322   apply Finset.Subset.antisymm (runningRegion_subset_stage M n)
323   apply running_maximal M (fun x => x ∈ runStage M n)
324   · intro x hx
325     exact runStage_subset_ending M n hx
326   · intro x hx
327     have h : x ∈ runStep M (runStage M n) := by rwa [hn]
328     exact ((mem_runStep M _ x).mp h).2
329 
330 end
331 end Komorebi.MachineTheory.SafeEnding

Back to source controls