SynthesisExamples.lean

1 import MachineTheory.SynthesisBudget
2 import Mathlib.Tactic.FinCases
3 import Mathlib.Data.Fintype.Basic
4 import Mathlib.Data.Fintype.Fin
5 import Mathlib.Tactic.NormNum
6 
7 /-!
8 # Checked finite examples and boundary controls
9 
10 An eight-expression grammar is used for the displayed arithmetic synthesis.
11 There are exactly three declared training contexts. This is not a reproduction
12 of the older 3,960-expression experiment, nor a generalization claim from three
13 examples. The normalizer's key soundness is proved for every natural-number
14 prefix independently of the target labels.
15 -/
16 
17 namespace Komorebi.MachineTheory.SynthesisExamples
18 open Synthesis
19 
20 inductive Program where
21   | zero | zeroAlias | bGtA | aLtB | bGtC | cLtB | maxGtC | swappedMax | capped
22   deriving DecidableEq, Repr
23 
24 abbrev Prefix := Nat × Nat × Nat
25 
26 def evaluate : Program → Prefix → Bool
27   | .zero, x => decide (x.1 > x.1)
28   | .zeroAlias, _ => decide ((0 : Nat) = 1)
29   | .bGtA, x => decide (x.2.1 > x.1)
30   | .aLtB, x => decide (x.1 < x.2.1)
31   | .bGtC, x => decide (x.2.1 > x.2.2)
32   | .cLtB, x => decide (x.2.2 < x.2.1)
33   | .maxGtC, x => decide (max x.1 x.2.1 > x.2.2)
34   | .swappedMax, x => decide (max x.2.1 x.1 > x.2.2)
35   | .capped, x => decide (max x.1 x.2.1 > min x.2.2 2)
36 
37 def key : Program → Fin 5
38   | .zero | .zeroAlias => 0
39   | .bGtA | .aLtB => 1
40   | .bGtC | .cLtB => 2
41   | .maxGtC | .swappedMax => 3
42   | .capped => 4
43 
44 /-- These semantic equations hold beyond the three developmental contexts. -/
45 theorem arithmetic_key_sound (p q : Program) (h : key p = key q) (x : Prefix) :
46     evaluate p x = evaluate q x := by
47   cases p <;> cases q <;> simp_all [key, evaluate, max_comm]
48 
49 def context : Fin 3 → Prefix
50   | 0 => (0, 3, 2)
51   | 1 => (0, 1, 2)
52   | 2 => (3, 0, 2)
53 
54 def task : Task Program (Fin 3) Bool where
55   eval p i := evaluate p (context i)
56   target i := evaluate .maxGtC (context i)
57   contexts := [0,1,2]
58   complete := by intro i; fin_cases i <;> decide
59 
60 def grammar : List Program :=
61   [.zero, .zeroAlias, .bGtA, .aLtB, .bGtC, .cLtB, .maxGtC, .swappedMax]
62 
63 def quotientGrammar : List Program := [.zero, .bGtA, .bGtC, .maxGtC]
64 
65 theorem task_key_sound : KeySound task key := by
66   intro p q h i
67   exact arithmetic_key_sound p q h (context i)
68 
69 theorem prepared_grammar : representatives key [] grammar = quotientGrammar := by decide
70 
71 theorem preparation_count : (prepare key [] grammar).1 = quotientGrammar ∧
72     (prepare key [] grammar).2 = 10 := by decide
73 
74 def expectedTrace : List (Program × Option (Fin 3)) :=
75   [(.zero, some 0), (.bGtA, some 1), (.bGtC, some 2), (.maxGtC, none)]
76 
77 /-- The original scan visits seven of eight ASTs and performs nine retained tests. -/
78 theorem original_run : scan task grammar [] =
79     ⟨some .maxGtC, expectedTrace, [2,1,0], 9, 7⟩ := by decide
80 
81 /-- The prepared scan has the identical transcript with six retained tests. -/
82 theorem compressed_run : scan task quotientGrammar [] =
83     ⟨some .maxGtC, expectedTrace, [2,1,0], 6, 4⟩ := by decide
84 
85 theorem arithmetic_trace_from_general_theorem :
86     SameEvidence (scan task quotientGrammar []) (scan task grammar []) ∧
87     (scan task quotientGrammar []).comparisons ≤ (scan task grammar []).comparisons ∧
88     (scan task quotientGrammar []).visits ≤ (scan task grammar []).visits := by
89   simpa [prepared_grammar] using ordered_compression task key task_key_sound grammar []
90 
91 theorem same_teacher_work : teacherComparisons task (scan task grammar []) = 9 ∧
92     teacherComparisons task (scan task quotientGrammar []) = 9 := by decide
93 
94 theorem source_synthesis_contract :
95     Protocol task grammar [] expectedTrace (some .maxGtC) ∧ expectedTrace.length = 4 := by
96   constructor
97   · have h := scan_protocol task grammar []
98     rw [original_run] at h
99     exact h
100   · decide
101 
102 /-- All false alternatives are excluded in this finite grammar, not all programs. -/
103 def failingGrammar : List Program := [.zero, .zeroAlias, .bGtA, .aLtB, .bGtC, .cLtB]
104 
105 theorem failing_run : scan task failingGrammar [] =
106     ⟨none, [(.zero,some 0),(.bGtA,some 1),(.bGtC,some 2)], [2,1,0], 6, 6⟩ := by decide
107 
108 theorem failing_is_complete : ∀ p ∈ failingGrammar, ¬ Correct task p :=
109   (exhaustion_iff task failingGrammar []).mp (by decide)
110 
111 theorem outside_grammar_solution : Correct task .maxGtC ∧ Program.maxGtC ∉ failingGrammar := by
112   constructor
113   · intro i; rfl
114   · decide
115 
116 /-- Agreement on every admitted example does not prove a global arithmetic law. -/
117 theorem finite_fit_not_universal : Correct task .capped ∧
118     evaluate .capped (0,5,8) ≠ evaluate .maxGtC (0,5,8) := by
119   constructor
120   · intro i; fin_cases i <;> decide
121   · decide
122 
123 /-- A collision from one probe erases the only correct Boolean program. -/
124 def probeTask : Task Bool Bool Bool where
125   eval p x := if p then x else false
126   target x := x
127   contexts := [false,true]
128   complete := by intro x; cases x <;> simp
129 
130 def probeKey (p : Bool) : Bool := probeTask.eval p false
131 
132 theorem probe_alias_changes_result :
133     (scan probeTask [false,true] []).answer = some true ∧
134     (scan probeTask (representatives probeKey [] [false,true]) []).answer = none := by decide
135 
136 theorem probe_key_is_unsound : ¬ KeySound probeTask probeKey := by
137   intro h
138   have he := h false true (by decide) true
139   simp [probeTask] at he
140 
141 /-- Selecting the latest rather than the earliest equivalent AST changes the exact answer. -/
142 theorem later_representative_changes_ast :
143     (scan task [.maxGtC,.swappedMax] []).answer = some .maxGtC ∧
144     (scan task [.swappedMax] []).answer = some .swappedMax ∧
145     (scan task [.maxGtC,.swappedMax] []).transcript ≠
146       (scan task [.swappedMax] []).transcript := by decide
147 
148 /-- A changed context order keeps correctness but not the counterexample transcript. -/
149 def reversedTask : Task Program (Fin 3) Bool :=
150   {task with contexts := [2,1,0], complete := by intro i; fin_cases i <;> decide}
151 
152 theorem changed_context_order :
153     (scan reversedTask grammar []).answer = some .maxGtC ∧
154     (scan reversedTask grammar []).transcript ≠ (scan task grammar []).transcript := by decide
155 
156 /-- A deliberately noncompliant alternative that discards all older evidence. -/
157 def forgetfulScan (T : Task Program (Fin 3) Bool) : List Program → List (Fin 3) → Result Program (Fin 3)
158   | [], E => ⟨none, [], E, 0, 0⟩
159   | p :: ps, E =>
160     let c := inspect T p E
161     match c.1 with
162     | some _ =>
163       let r := forgetfulScan T ps E
164       ⟨r.answer, r.transcript, r.retained, c.2 + r.comparisons, 1 + r.visits⟩
165     | none =>
166       match teacher T p with
167       | none => ⟨some p, [(p,none)], E, c.2, 1⟩
168       | some x =>
169         let r := forgetfulScan T ps [x]
170         ⟨r.answer, (p,some x) :: r.transcript, r.retained, c.2 + r.comparisons, 1 + r.visits⟩
171 
172 def repeatGrammar : List Program := [.zero,.bGtA,.zero,.maxGtC]
173 
174 theorem forgetting_repeats_submission :
175     ((forgetfulScan task repeatGrammar []).transcript.map Prod.fst) =
176       [.zero,.bGtA,.zero,.maxGtC] ∧
177     ¬ ((forgetfulScan task repeatGrammar []).transcript.map Prod.fst).Nodup := by decide
178 
179 theorem persistence_prevents_repeat :
180     ((scan task repeatGrammar []).transcript.map Prod.fst) = [.zero,.bGtA,.maxGtC] ∧
181     ((scan task repeatGrammar []).transcript.map Prod.fst).Nodup := by
182   constructor
183   · decide
184   · exact no_repeated_submission task repeatGrammar []
185 
186 /-- With four candidate inspections, one run is suspended and the other is completed. -/
187 theorem finite_budget_boundary :
188     boundedScan task 4 grammar [] =
189       .suspended ⟨[.bGtC,.cLtB,.maxGtC,.swappedMax], [1,0],
190         [(.zero,some 0),(.bGtA,some 1)], 3, 4⟩ ∧
191     boundedScan task 4 quotientGrammar [] = .complete (scan task quotientGrammar []) := by decide
192 
193 theorem resumed_evidence : resume task (boundedScan task 4 grammar []) = scan task grammar [] :=
194   resume_bounded task 4 grammar []
195 
196 theorem suspension_is_not_exhaustion :
197     ¬ ∃ r, boundedScan task 4 grammar [] = .complete r ∧ r.answer = none := by
198   intro ⟨r, hr, _⟩
199   rw [finite_budget_boundary.1] at hr
200   contradiction
201 
202 /-- Preparation has a separate, nonzero event count even when semantic replay is exact. -/
203 theorem preparation_can_outweigh_saved_tests :
204     (prepare key [] grammar).2 + (scan task quotientGrammar []).comparisons >
205       (scan task grammar []).comparisons := by decide
206 
207 /-- Common events on a finite batch: three saved retained tests per run, ten key tests once.
208 This comparison does not charge key computation, index storage or all host instructions. -/
209 theorem illustrative_amortization (n : Nat) :
210     (prepare key [] grammar).2 + n * (scan task quotientGrammar []).comparisons <
211       n * (scan task grammar []).comparisons ↔ 4 ≤ n := by
212   rw [preparation_count.2, original_run, compressed_run]
213   dsimp
214   omega
215 
216 /-- With no contexts every program is vacuously correct; the first is still preserved. -/
217 def emptyContextTask : Task Bool Empty Bool where
218   eval _ x := Empty.elim x
219   target x := Empty.elim x
220   contexts := []
221   complete x := Empty.elim x
222 
223 theorem empty_context_earliest :
224     (scan emptyContextTask [false,true] []).answer = some false ∧
225     (scan emptyContextTask [false,true] []).transcript.length = 1 := by decide
226 
227 theorem empty_grammar_exhausted : (scan task [] []).answer = none ∧
228     (scan task [] []).transcript.length = 0 := by decide
229 
230 /-- A new target defines a different synthesis problem even with unchanged syntax. -/
231 def changedTask : Task Program (Fin 3) Bool :=
232   {task with target := fun i => !(task.target i)}
233 
234 theorem target_change_breaks_old_answer :
235     (scan changedTask grammar []).answer = none ∧
236     (scan task grammar []).answer = some .maxGtC := by decide
237 
238 end Komorebi.MachineTheory.SynthesisExamples

Back to source controls