PrefixExamples.lean

1 import MachineTheory.PrefixAdmission
2 import MachineTheory.BinaryExamples
3 import MachineTheory.SynthesisExamples
4 
5 /-! # Concrete compiler instances, sharp boundaries and separately metered work -/
6 namespace Komorebi.MachineTheory.PrefixExamples
7 open OrderedCompiler BinaryDiagnosis HardInquiry Finset
8 
9 /-- A fifth zero closes a capacity-four child; its unread suffix is not inspected. -/
10 theorem first_excess_stops :
11     PrefixScan.stream id 4 0 0 [false,false,false,false,false,true,true,true] = ⟨none,5,6⟩ ∧
12     PrefixScan.full id 4 0 0 [false,false,false,false,false,true,true,true] = ⟨none,8,1⟩ := by decide
13 
14 theorem capacity_equality_survives :
15     (PrefixScan.stream id 4 0 0 [false,false,false,false,true,true,true,true]).branches =
16       some ([false,false,false,false],[true,true,true,true]) ∧
17     (PrefixScan.stream id 4 0 0 [false,false,false,false,true,true,true,true]).reads=8 := by decide
18 
19 /-- Total headroom, not just the two partial counts, is needed for the completion iff. -/
20 theorem missing_total_capacity : max (0:ℕ) 0≤4 ∧ ¬ PrefixScan.Completable 9 4 0 0 := by
21   constructor
22   · decide
23   · rintro ⟨u,v,hs,hu,hv⟩; omega
24 
25 /-- The result acquired in Block09 separately denotes the universally sound predicate. -/
26 theorem acquired_rule_meaning (a b C : ℕ) :
27     SynthesisExamples.evaluate .maxGtC (a,b,C)=true ↔ C<max a b := by
28   simp only [SynthesisExamples.evaluate,decide_eq_true_eq]
29 
30 theorem acquired_rule_completion (m C a b : ℕ) (hr : a+b≤m) (hc : m≤2*C) :
31     SynthesisExamples.evaluate .maxGtC (a,b,C)=false ↔ PrefixScan.Completable m C a b := by
32   rw [PrefixScan.completion_iff m C a b hr hc]
33   simp [SynthesisExamples.evaluate]
34 
35 /-- A training-perfect alternative would reject a legal larger-capacity prefix. -/
36 theorem learned_fit_can_erase_completion :
37     Synthesis.Correct SynthesisExamples.task .capped ∧
38     SynthesisExamples.evaluate .capped (0,5,8)=true ∧
39     PrefixScan.Completable 8 8 0 5 := by
40   refine ⟨SynthesisExamples.finite_fit_not_universal.1,by decide,?_⟩
41   exact (PrefixScan.completion_iff 8 8 0 5 (by decide) (by decide)).mpr (by decide)
42 
43 /-- The artifact acquired earlier receives a separate certificate against actual controller semantics. -/
44 theorem acquired_rule_excludes_actual_root {X E C : Type} [DecidableEq X]
45     (M : Model X E Bool C Unit) (s : Scope M) (h : ℕ) (V P : Finset X) (hPV : P⊆V) (e : E)
46     (hr : SynthesisExamples.evaluate .maxGtC
47       ((P.filter (fun x => M.observe e x=false)).card,
48        (P.filter (fun x => M.observe e x=true)).card,2^h)=true) :
49     ¬ ∃ k : Bool → Option (Tree E Bool C h),M.Valid (h+1) V (.inr (e,k)) := by
50   have ht := (acquired_rule_meaning _ _ _).mp hr
51   rcases lt_max_iff.mp ht with h0 | h1
52   · exact prefix_exclusion M s h V P hPV e false h0
53   · exact prefix_exclusion M s h V P hPV e true h1
54 
55 abbrev World := BinaryExamples.World
56 abbrev Query := BinaryExamples.Query
57 
58 def rows : List World :=
59   [(false,false,false),(false,false,true),(false,true,false),(false,true,true),
60    (true,false,false),(true,false,true),(true,true,false),(true,true,true)]
61 
62 def queries : List Query := rows.map Sum.inr ++ [Sum.inl 0,Sum.inl 1,Sum.inl 2]
63 
64 theorem rows_exact : rows.toFinset=univ ∧ rows.Nodup := by decide
65 
66 theorem complete_repairs : ∀ c : World,c∈rows := by decide
67 
68 theorem complete_queries : ∀ e : Query,e∈queries := by
69   intro e
70   rcases e with i | x
71   · exact List.mem_append_right _ (by fin_cases i <;> simp)
72   · exact List.mem_append_left _ (List.mem_map.mpr ⟨x,complete_repairs x,rfl⟩)
73 
74 def fullEight := search fullScanner BinaryExamples.eight queries rows 3 rows
75 def streamEight := search streamScanner BinaryExamples.eight queries rows 3 rows
76 
77 theorem eight_measured_reads :
78     (fullEight.reads,fullEight.checks,streamEight.reads,streamEight.checks) = (184,45,153,198) := by decide
79 
80 theorem eight_returned_profile :
81     fullEight.answer.map (fun t => ((BinaryExamples.eight.profile 3 univ t).1 (),
82       (BinaryExamples.eight.profile 3 univ t).2))=some (4,15) := by decide
83 
84 /-- Equal event prices do not turn the decrease in reads into a total saving. -/
85 theorem predicate_work_can_cost_more :
86     fullEight.reads+fullEight.checks < streamEight.reads+streamEight.checks := by decide
87 
88 theorem weighted_event_saving (w : ℕ) :
89     w*streamEight.reads+streamEight.checks < w*fullEight.reads+fullEight.checks ↔ 153<31*w := by
90   have hh := eight_measured_reads
91   have h0 : fullEight.reads=184 := by decide
92   have h1 : fullEight.checks=45 := by decide
93   have h2 : streamEight.reads=153 := by decide
94   have h3 : streamEight.checks=198 := by decide
95   rw [h0,h1,h2,h3]
96   omega
97 
98 theorem eight_same_literal_answer : streamEight.answer=fullEight.answer :=
99   same_returned_tree BinaryExamples.eight queries rows 3 rows
100 
101 /-- Not just a matching outcome: the emitted tree is checked under the original semantics. -/
102 theorem eight_returned_valid : ∀ t, streamEight.answer=some t → BinaryExamples.eight.Valid 3 univ t := by
103   intro t ht
104   have h := (streaming_sound_complete BinaryExamples.eight BinaryExamples.eight_scope
105     queries rows complete_queries complete_repairs 3 rows rows_exact.2).1 t ht
106   simpa only [rows_exact.1] using h
107 
108 theorem eight_has_answer : ∃ t, streamEight.answer=some t := by
109   have h := full_search_complete BinaryExamples.eight BinaryExamples.eight_scope queries rows
110     complete_queries complete_repairs 3 rows rows_exact.2 BinaryExamples.balanced
111     (by simpa only [rows_exact.1] using BinaryExamples.balanced_valid)
112   obtain ⟨t,ht⟩ := h
113   refine ⟨t,?_⟩
114   change (search streamScanner _ _ _ _ _).answer=some t
115   rw [same_returned_tree]
116   exact ht
117 
118 /-- In an equality-only model the lower-depth capacity test need not be attainable. -/
119 theorem three_short_horizon_fails :
120     (search streamScanner BinaryExamples.three [0,1,2] [0,1,2] 1 [0,1,2]).answer=none := by decide
121 
122 /-- Capacity survival is not evidence of an informative remaining query. -/
123 theorem silent_capacity_is_not_solution :
124     (streamScanner (BinaryExamples.silent.observe ()) 2 [false,true]).branches ≠ none ∧
125     (search streamScanner BinaryExamples.silent [()] [false,true] 2 [false,true]).answer=none := by decide
126 
127 /-- Duplicated rows falsely enlarge counts, so nodup is an explicit completeness premise. -/
128 def boolModel : Model Bool Unit Bool Bool Unit where
129   permitted := fun _ _ => true
130   next := fun _ x => x
131   observe := fun _ x => x
132   accept := fun x c => decide (x=c)
133   stepCost := fun _ _ => 1
134   terminalCost := fun _ _ _ => 1
135 
136 def boolTree : Tree Unit Bool Bool 2 := .inr ((),fun b => some (.inl b))
137 
138 theorem duplicate_rows_boundary :
139     boolModel.Valid 2 ([false,false,false,true].toFinset) boolTree ∧
140     (streamScanner (boolModel.observe ()) 2 [false,false,false,true]).branches=none := by decide
141 
142 /-- A reset changes what must be repaired; cardinality pruning then loses a valid tree. -/
143 theorem reset_boundary :
144     BinaryExamples.reset.Valid 1 univ BinaryExamples.resetTree ∧
145     (search streamScanner BinaryExamples.reset queries rows 1 rows).answer=none ∧
146     checkScope BinaryExamples.reset=false := by
147   exact ⟨BinaryExamples.reset_valid_and_small.1,by decide,BinaryExamples.reset_guard_rejects⟩
148 
149 /-- One repair per first-bit class violates the singleton leaf premise. -/
150 def classRepair : Model World Unit Bool Bool Unit where
151   permitted := fun _ _ => true
152   next := fun _ x => x
153   observe := fun _ x => x.1
154   accept := fun x c => decide (x.1=c)
155   stepCost := fun _ _ => 1
156   terminalCost := fun _ _ _ => 1
157 
158 def classTree : Tree Unit Bool Bool 1 := .inr ((),fun b => some b)
159 
160 theorem non_singleton_boundary : classRepair.Valid 1 univ classTree ∧
161     (search streamScanner classRepair [()] [false,true] 1 rows).answer=none ∧
162     checkScope classRepair=false := by decide
163 
164 /-- Changing the fixed query order is outside literal-tree preservation. -/
165 def rootLabel (t : Option (Tree (Fin 3) Bool (Fin 3) 2)) : Option (Fin 3) :=
166   t.bind (fun t => match t with | .inl _ => none | .inr (e,_) => some e)
167 
168 theorem query_order_changes_tree :
169     (search streamScanner BinaryExamples.three [0,1,2] [0,1,2] 2 [0,1,2]).answer ≠
170     (search streamScanner BinaryExamples.three [1,0,2] [0,1,2] 2 [0,1,2]).answer := by
171   intro he
172   have h0 : rootLabel (search streamScanner BinaryExamples.three [0,1,2] [0,1,2] 2 [0,1,2]).answer = some 0 := by decide
173   have h1 : rootLabel (search streamScanner BinaryExamples.three [1,0,2] [0,1,2] 2 [0,1,2]).answer = some 1 := by decide
174   have hh := congrArg rootLabel he
175   rw [h0,h1] at hh
176   have hbad : (0 : Fin 3)=1 := Option.some.inj hh
177   exact (by decide : (0:Fin 3)≠1) hbad
178 
179 /-- An incomplete menu cannot certify impossibility in the full model. -/
180 theorem missing_query_boundary :
181     (search streamScanner boolModel [] [false,true] 1 [false,true]).answer=none ∧
182     ∃ t : Tree Unit Bool Bool 1, boolModel.Valid 1 univ t := by
183   refine ⟨by decide,⟨(show Tree Unit Bool Bool 1 from .inr ((),fun b => some b)),by decide⟩⟩
184 
185 /-- The theorem never permits a terminal whose installed permission was removed. -/
186 def forbidden : Model Bool Unit Bool Bool Unit :=
187   {boolModel with permitted := fun _ _ => false}
188 
189 theorem permission_boundary :
190     (search streamScanner forbidden [()] [false,true] 1 [false,true]).answer=none ∧
191     (search streamScanner boolModel [()] [false,true] 1 [false,true]).answer ≠ none := by decide
192 
193 
194 /-- Checked completion is available for the actual source-shaped finite example. -/
195 theorem eight_guarded_completion :
196     ∃ r, checkedSearch BinaryExamples.eight queries rows 3 rows=some r ∧
197       r.answer=fullEight.answer := by
198   classical
199   have hg : guard BinaryExamples.eight queries rows rows=true :=
200     (guard_iff _ _ _ _).mpr ⟨BinaryExamples.eight_scope,rows_exact.2,complete_queries,complete_repairs⟩
201   refine ⟨streamEight,?_,eight_same_literal_answer⟩
202   simp only [checkedSearch,hg,ite_true]
203   rfl
204 
205 /-- Rejection of the optimization's scope is not a proof of an unsolvable task. -/
206 theorem scope_rejection_not_infeasible :
207     checkedSearch BinaryExamples.reset queries rows 1 rows=none ∧
208     BinaryExamples.reset.Valid 1 univ BinaryExamples.resetTree := by
209   classical
210   constructor
211   · simp only [checkedSearch,OrderedCompiler.guard,BinaryExamples.reset_guard_rejects,Bool.false_and,
212       Bool.false_eq_true,ite_false]
213   · exact BinaryExamples.reset_valid_and_small.1
214 
215 end Komorebi.MachineTheory.PrefixExamples
216 

Back to source controls