SafeEndingExamples.lean

1 import MachineTheory.SafeEndingPolicies
2 import Mathlib.Tactic.FinCases
3 
4 /-! Exact, kernel-checked examples and boundary controls for Core 8.3. -/
5 namespace Komorebi.MachineTheory.SafeEnding.Examples
6 
7 /-- 0 is a goal, 1 can stop now but loses that option when running,
8 and 2 can run safely forever without an ending. -/
9 def threeState : Model (Fin 3) Bool where
10   safe := Finset.univ
11   goal := {0}
12   goal_safe := Finset.subset_univ _
13   run := fun _ => {false}
14   finish := fun x => if x = 2 then ∅ else {true}
15   post := fun x a => if a then {0} else if x = 0 then {0} else {2}
16   post_nonempty := by
17     intro x a _
18     cases a with
19     | false => by_cases hx : x = 0 <;> simp [hx]
20     | true => simp
21 
22 theorem three_end_stage : endStage threeState 1 = {0, 1} := by
23   ext x
24   fin_cases x <;> simp [endStage_succ, endStage_zero, endStep, threeState]
25 
26 theorem three_end_fixed : endStep threeState (endStage threeState 1) = endStage threeState 1 := by
27   rw [three_end_stage]
28   ext x
29   fin_cases x <;> simp [endStep, threeState]
30 
31 theorem three_ending : endingRegion threeState = {0, 1} :=
32   (endingRegion_eq_of_stage_fixed threeState 1 three_end_fixed).trans three_end_stage
33 
34 theorem three_run_stage : runStage threeState 1 = {0} := by
35   rw [runStage_succ, runStage_zero, three_ending]
36   ext x
37   fin_cases x <;> simp [runStep, threeState]
38 
39 theorem three_run_fixed : runStep threeState (runStage threeState 1) = runStage threeState 1 := by
40   rw [three_run_stage]
41   ext x
42   fin_cases x <;> simp [runStep, threeState]
43 
44 theorem three_running : runningRegion threeState = {0} :=
45   (runningRegion_eq_of_stage_fixed threeState 1 three_run_fixed).trans three_run_stage
46 
47 theorem ready_rank : endRank threeState 1 = 1 := by
48   have hx : (1 : Fin 3) ∈ endingRegion threeState := by simp [three_ending]
49   have hle : endRank threeState 1 ≤ 1 := endRank_min threeState (n := 1) (by rw [three_end_stage]; simp)
50   have hn : endRank threeState 1 ≠ 0 := by
51     intro h
52     have hg := (endRank_zero_iff threeState hx).mp h
53     simp [threeState] at hg
54   omega
55 
56 theorem ready_can_stop : ∃ σ, EndingGuarantee threeState σ 1 :=
57   (ending_region_iff threeState 1).mp (by simp [three_ending])
58 
59 theorem ready_cannot_preserve_ending : ¬ ∃ P, SwitchingGuarantee threeState P 1 := by
60   rw [← safe_continuation_iff, three_running]
61   simp
62 
63 theorem trap_can_run : RunningGuarantee threeState (fun _ => some false) 2 := by
64   intro c _
65   exact ⟨Finset.mem_univ _, false, rfl, by simp [threeState]⟩
66 
67 theorem trap_cannot_end : ¬ ∃ σ, EndingGuarantee threeState σ 2 := by
68   rw [← ending_region_iff, three_ending]
69   simp
70 
71 /-- Empty catalogues are permitted, but are not winning policies. -/
72 def deadlock : Model Unit Unit where
73   safe := Finset.univ
74   goal := ∅
75   goal_safe := Finset.empty_subset _
76   run := fun _ => ∅
77   finish := fun _ => ∅
78   post := fun _ _ => ∅
79   post_nonempty := by simp
80 
81 theorem deadlock_no_running (σ : Strategy Unit Unit) : ¬ RunningGuarantee deadlock σ () := by
82   intro h
83   obtain ⟨a, _, ha⟩ := (h (start ()) Reach.refl).2
84   simp [deadlock] at ha
85 
86 theorem deadlock_no_ending (σ : Strategy Unit Unit) : ¬ EndingGuarantee deadlock σ () := by
87   intro h
88   obtain ⟨a, _, ha⟩ := (h.total (start ()) Reach.refl).2 (by simp [deadlock, start])
89   simp [deadlock] at ha
90 
91 /-- Swapping action and successor quantifiers would allow hindsight. -/
92 theorem hindsight_is_stronger :
93     (∀ y : Bool, ∃ a : Bool, a = y) ∧ ¬ (∃ a : Bool, ∀ y : Bool, a = y) := by decide
94 
95 /-- A winning history-dependent ending may wait longer than the minimal rank.
96 Only the constructed rank strategy receives the first-entry-rank time bound. -/
97 def waitModel : Model Bool Bool where
98   safe := Finset.univ
99   goal := {false}
100   goal_safe := Finset.subset_univ _
101   run := fun _ => {false}
102   finish := fun _ => Finset.univ
103   post := fun x a => {if a then false else x}
104   post_nonempty := by intro x a _; exact Finset.singleton_nonempty _
105 
106 def delayStrategy : Strategy Bool Bool := fun c => some (if c.1 = [] then false else true)
107 
108 theorem wait_end_stage : endStage waitModel 1 = Finset.univ := by
109   ext x
110   cases x <;> simp [endStage_succ, endStage_zero, endStep, waitModel]
111 
112 theorem wait_ending : endingRegion waitModel = Finset.univ := by
113   have hf : endStep waitModel (endStage waitModel 1) = endStage waitModel 1 := by
114     rw [wait_end_stage]
115     ext x
116     simp [endStep]
117   exact (endingRegion_eq_of_stage_fixed waitModel 1 hf).trans wait_end_stage
118 
119 theorem wait_rank : endRank waitModel true = 1 := by
120   have hx : true ∈ endingRegion waitModel := by simp [wait_ending]
121   have hle : endRank waitModel true ≤ 1 := endRank_min waitModel (n := 1) (by rw [wait_end_stage]; simp)
122   have hn : endRank waitModel true ≠ 0 := by
123     intro h
124     have hg := (endRank_zero_iff waitModel hx).mp h
125     simp [waitModel] at hg
126   omega
127 
128 theorem delay_guarantee : EndingGuarantee waitModel delayStrategy true := by
129   refine ⟨?_, ?_⟩
130   · intro c _
131     refine ⟨Finset.mem_univ _, ?_⟩
132     intro _
133     exact ⟨if c.1 = [] then false else true, rfl, Finset.mem_univ _⟩
134   · intro p _ hp
135     obtain ⟨_, a, _, _, hh, _⟩ := hp 0
136     have hn : (p 1).1 ≠ [] := by rw [hh]; simp
137     obtain ⟨_, b, hb, _, _, hy⟩ := hp 1
138     have hb' : b = true := by
139       simpa [delayStrategy, hn] using hb.symm
140     subst b
141     have hgoal : (p 2).2 ∈ waitModel.goal := by simpa [waitModel] using hy
142     exact (hp 2).1 hgoal
143 
144 def delayFirst : Config Bool Bool := ([(true, false)], true)
145 def delayLast : Config Bool Bool := ([(true, true), (true, false)], false)
146 
147 theorem delay_first_step : endEdge waitModel delayStrategy (start true) delayFirst := by
148   exact ⟨by decide, false, rfl, by decide, rfl, by decide⟩
149 
150 theorem delay_second_step : endEdge waitModel delayStrategy delayFirst delayLast := by
151   exact ⟨by decide, true, rfl, by decide, rfl, by decide⟩
152 
153 theorem winning_policy_need_not_take_minimal_time :
154     EndingGuarantee waitModel delayStrategy true ∧
155     endEdge waitModel delayStrategy (start true) delayFirst ∧
156     endEdge waitModel delayStrategy delayFirst delayLast ∧
157     2 > endRank waitModel true := by
158   exact ⟨delay_guarantee, delay_first_step, delay_second_step, by rw [wait_rank]; decide⟩
159 
160 end Komorebi.MachineTheory.SafeEnding.Examples

Back to source controls