RevisionExamples.lean

1 import MachineTheory.RevisionAdmission
2 import MachineTheory.BinaryExamples
3 
4 /-! # Actual controller-scope revision
5 
6 The artifacts select the inherited eight-case repair language, an installed controller,
7 and the exact expected profile attached to its record. Claim 2 is the general lower
8 bound for the actual model, not a supplied Boolean named "lower bound".
9 -/
10 namespace Komorebi.MachineTheory.RevisionExamples
11 open Dependency HardInquiry BinaryDiagnosis BinaryExamples Finset
12 
13 abbrev Node := Fin 5
14 abbrev Input := Fin 3
15 abbrev Data := Input → Bool
16 
17 /-- 0 equation; 1 counting scope; 2 leaf bound; 3 controller validity; 4 bound profile. -/
18 def graph : Graph Node Input where
19   parents := fun v => if v=2 then {1} else if v=4 then {3} else ∅
20   direct := fun v => if v=1 then {0} else if v=3 then {0,1} else if v=4 then {1,2} else ∅
21 
22 def rank (v : Node) : ℕ := if v=2 ∨ v=4 then 1 else 0
23 
24 theorem rank_checked : graph.Ranked rank := by
25   unfold Graph.Ranked
26   decide
27 
28 /-- Only the success predicate differs between these already formalized models. -/
29 def selectedModel (u : Bool) : Model World Query Bool World Unit :=
30   if u then universalRepair else eight
31 
32 def selectedTree (small : Bool) : Tree Query Bool World 3 :=
33   if small then .inl (false,false,false) else balanced
34 
35 def expectedProfile (small : Bool) : Profile Unit :=
36   if small then (fun _ => 1,1) else (fun _ => 4,15)
37 
38 def actualProfile (small : Bool) : Profile Unit := eight.profile 3 univ (selectedTree small)
39 
40 theorem profile_independent_of_repair_scope (u small : Bool) :
41     (selectedModel u).profile 3 univ (selectedTree small) = actualProfile small := by
42   cases u <;> cases small <;> rfl
43 
44 /-- The actual source bound quantifies over arbitrary supports and finite horizons. -/
45 def Lower (u : Bool) : Prop :=
46   ∀ h V (t : Tree Query Bool World h), (selectedModel u).Valid h V t →
47     lowerProfile V.card ≤ (selectedModel u).profile h V t
48 
49 theorem lower_from_scope (u : Bool) (hs : Scope (selectedModel u)) : Lower u := by
50   intro h V t ht
51   exact lowerProfile_le _ hs h V t ht
52 
53 theorem universal_breaks_old_bound : ¬ Lower true := by
54   intro h
55   have hh := h 0 univ (false,false,false) universal_repair_small.1
56   have no : ¬ lowerProfile (univ : Finset World).card ≤
57       universalRepair.profile 0 univ (false,false,false) := by decide
58   exact no hh
59 
60 theorem lower_iff_scope (u : Bool) : Lower u ↔ Scope (selectedModel u) := by
61   constructor
62   · intro h
63     cases u with
64     | false => exact eight_scope
65     | true => exact False.elim (universal_breaks_old_bound h)
66   · exact lower_from_scope u
67 
68 def meaning (a : Data) (v : Node) : Prop :=
69   if v=0 then (∀ n : ℕ, max n 0 = n)
70   else if v=1 then Scope (selectedModel (a 0))
71   else if v=2 then Lower (a 0)
72   else if v=3 then (selectedModel (a 0)).Valid 3 univ (selectedTree (a 1))
73   else (selectedModel (a 0)).Valid 3 univ (selectedTree (a 1)) ∧
74     (selectedModel (a 0)).profile 3 univ (selectedTree (a 1)) = expectedProfile (a 2)
75 
76 /-- Witness true asks the actual checker to validate this instance; false is malformed. -/
77 def localCheck : (v : Node) → ({i // i ∈ graph.direct v} → Bool) → Bool → Bool
78   | ⟨0,_⟩, _, w => w
79   | ⟨1,_⟩, a, w => w && checkScope (selectedModel (a ⟨0,by simp [graph,Fin.ext_iff]⟩))
80   | ⟨2,_⟩, _, w => w
81   | ⟨3,_⟩, a, w => w && decide ((selectedModel (a ⟨0,by simp [graph,Fin.ext_iff]⟩)).Valid 3 univ
82       (selectedTree (a ⟨1,by simp [graph,Fin.ext_iff]⟩)))
83   | ⟨4,_⟩, a, w => w && decide (actualProfile (a ⟨1,by simp [graph,Fin.ext_iff]⟩) = expectedProfile (a ⟨2,by simp [graph,Fin.ext_iff]⟩))
84   | ⟨n+5,h⟩, _, _ => False.elim (by omega)
85 
86 def system : System graph (fun _ => Bool) (fun _ => Bool) where
87   claim := meaning
88   external := fun _ _ => True
89   check := localCheck
90   sound := by
91     intro a v w hc _ hp
92     fin_cases v
93     · intro n
94       simp
95     · change (w && checkScope (selectedModel (a 0))) = true at hc
96       exact (checkScope_iff _).mp (Bool.and_eq_true_iff.mp hc).2
97     · have hs : Scope (selectedModel (a 0)) := hp 1 (by decide)
98       exact lower_from_scope (a 0) hs
99     · change (w && decide ((selectedModel (a 0)).Valid 3 univ (selectedTree (a 1)))) = true at hc
100       have hv : (selectedModel (a 0)).Valid 3 univ (selectedTree (a 1)) :=
101         of_decide_eq_true (Bool.and_eq_true_iff.mp hc).2
102       exact hv
103     · have hv : (selectedModel (a 0)).Valid 3 univ (selectedTree (a 1)) := hp 3 (by decide)
104       change (w && decide (actualProfile (a 1) = expectedProfile (a 2))) = true at hc
105       exact ⟨hv,(profile_independent_of_repair_scope (a 0) (a 1)).trans
106         (of_decide_eq_true (Bool.and_eq_true_iff.mp hc).2)⟩
107 
108 /-- The supplied registry is proved complete for these actual five claim meanings. -/
109 theorem meanings_complete : system.Complete := by
110   intro a b v hview hp _
111   fin_cases v
112   · rfl
113   · have h0 : a 0=b 0 := congrFun hview ⟨0,by decide⟩
114     change Scope (selectedModel (a 0)) ↔ Scope (selectedModel (b 0))
115     rw [h0]
116   · change Lower (a 0) ↔ Lower (b 0)
117     rw [lower_iff_scope,lower_iff_scope]
118     exact hp 1 (by decide)
119   · have h0 : a 0=b 0 := congrFun hview ⟨0,by decide⟩
120     have h1 : a 1=b 1 := congrFun hview ⟨1,by decide⟩
121     change (selectedModel (a 0)).Valid 3 univ (selectedTree (a 1)) ↔
122       (selectedModel (b 0)).Valid 3 univ (selectedTree (b 1))
123     rw [h0,h1]
124   · have h1 : a 1=b 1 := congrFun hview ⟨1,by decide⟩
125     have h2 : a 2=b 2 := congrFun hview ⟨2,by decide⟩
126     have hvalid := hp 3 (by decide)
127     change (selectedModel (a 0)).Valid 3 univ (selectedTree (a 1)) ↔
128       (selectedModel (b 0)).Valid 3 univ (selectedTree (b 1)) at hvalid
129     change ((selectedModel (a 0)).Valid 3 univ (selectedTree (a 1)) ∧
130         (selectedModel (a 0)).profile 3 univ (selectedTree (a 1)) = expectedProfile (a 2)) ↔
131       ((selectedModel (b 0)).Valid 3 univ (selectedTree (b 1)) ∧
132         (selectedModel (b 0)).profile 3 univ (selectedTree (b 1)) = expectedProfile (b 2))
133     rw [profile_independent_of_repair_scope,profile_independent_of_repair_scope]
134     apply and_congr hvalid
135     rw [h1,h2]
136 
137 def before : Data := fun _ => false
138 
139 def repairAdded : Data := fun i => decide (i=0)
140 
141 def replaced : Data := fun _ => true
142 
143 def oldWitness : Node → Bool := fun _ => true
144 
145 def allFresh : Node → Option Bool := fun _ => some true
146 
147 def missingProfile : Node → Option Bool := fun v => if v=4 then none else some true
148 
149 def externalOK : Node → Bool := fun _ => true
150 
151 set_option maxRecDepth 8192 in
152 set_option maxHeartbeats 2000000 in
153 theorem old_checks : ∀ v, system.check v (graph.view before v) (oldWitness v)=true := by decide
154 
155 /-- The pre-revision claims are established by sound rules, not by a stored PASS flag. -/
156 theorem old_established : ∀ v, system.Established before v (oldWitness v) :=
157   system.established_from_checks rank rank_checked before oldWitness old_checks (fun _ => trivial)
158 
159 theorem exact_changed_roots : graph.changedRoots before repairAdded = {1,3} ∧
160     graph.stale before repairAdded = {1,2,3,4} := by decide
161 
162 theorem exact_replacement_stale : graph.changedRoots before replaced = {1,3,4} ∧
163     graph.stale before replaced = {1,2,3,4} := by decide
164 
165 def afterAddition := system.finish before repairAdded oldWitness missingProfile externalOK rank
166 
167 def afterReplacement := system.finish before replaced oldWitness allFresh externalOK rank
168 
169 set_option maxRecDepth 8192 in
170 set_option maxHeartbeats 2000000 in
171 /-- Stale and false are distinct: the old balanced controller is still valid. -/
172 theorem addition_verdicts : afterAddition 0 = .reused true ∧
173     afterAddition 1 = .rejected ∧ afterAddition 2 = .blockedParents ∧
174     afterAddition 3 = .rechecked true ∧ afterAddition 4 = .missing := by decide
175 
176 set_option maxRecDepth 8192 in
177 set_option maxHeartbeats 2000000 in
178 theorem replacement_verdicts : afterReplacement 0 = .reused true ∧
179     afterReplacement 1 = .rejected ∧ afterReplacement 2 = .blockedParents ∧
180     afterReplacement 3 = .rechecked true ∧ afterReplacement 4 = .rechecked true := by decide
181 
182 theorem addition_sound : system.SoundState repairAdded afterAddition :=
183   system.finish_sound meanings_complete rank rank_checked before repairAdded oldWitness missingProfile
184     externalOK old_established (fun _ _ => trivial) (fun _ _ => trivial)
185 
186 theorem replacement_sound : system.SoundState replaced afterReplacement :=
187   system.finish_sound meanings_complete rank rank_checked before replaced oldWitness allFresh
188     externalOK old_established (fun _ _ => trivial) (fun _ _ => trivial)
189 
190 /-- The still-true profile is missing evidence, not refuted by that procedural outcome. -/
191 theorem missing_is_not_false : afterAddition 4 = .missing ∧ system.claim repairAdded 4 := by
192   refine ⟨addition_verdicts.2.2.2.2,?_⟩
193   change universalRepair.Valid 3 univ balanced ∧ universalRepair.profile 3 univ balanced = (fun _ => 4,15)
194   decide
195 
196 /-- A new valid one-record controller gets a new actual profile, not the old (4,15). -/
197 theorem replacement_actual_controller :
198     (selectedModel (replaced 0)).Valid 3 univ (selectedTree (replaced 1)) ∧
199     (selectedModel (replaced 0)).profile 3 univ (selectedTree (replaced 1)) = (fun _ => 1,1) := by
200   have h := (replacement_sound 4 true (by rw [replacement_verdicts.2.2.2.2]; rfl)).2.2
201   exact h
202 
203 /-- A stored old performance target is not repaired just by installing a valid controller. -/
204 def oldProfileTarget : Data := fun i => decide (i≠2)
205 
206 def afterOldProfile := system.finish before oldProfileTarget oldWitness allFresh externalOK rank
207 
208 set_option maxRecDepth 8192 in
209 set_option maxHeartbeats 2000000 in
210 theorem obsolete_profile_rejected : afterOldProfile 3 = .rechecked true ∧
211     afterOldProfile 4 = .rejected ∧ ¬ system.claim oldProfileTarget 4 := by
212   refine ⟨by decide,by decide,?_⟩
213   intro h
214   have falseProfile := h.2
215   have no : ¬ universalRepair.profile 3 univ (.inl (false,false,false)) =
216       (show Profile Unit from (fun _ => 4,15)) := by decide
217   exact no falseProfile
218 
219 /-- The unchanged equation survives the actual scope change through the generic theorem. -/
220 theorem equation_reused : system.Established replaced 0 true := by
221   exact system.selective_reuse meanings_complete rank rank_checked before replaced oldWitness
222     old_established (fun _ _ => trivial) 0 (by decide)
223 
224 /-- No scope flag licenses the old lower bound after the success predicate changes. -/
225 theorem old_bound_now_false : ¬ system.claim repairAdded 2 := universal_breaks_old_bound
226 
227 end Komorebi.MachineTheory.RevisionExamples

Back to source controls