Synthesis.lean

1 import Mathlib.Data.List.Basic
2 import Mathlib.Data.List.Nodup
3 
4 /-!
5 # Finite counterexample-guided synthesis
6 
7 Reviewed Core 6.1. Programs remain their original syntax values. The teacher checks
8 one fixed complete ordered context list. Retained counterexamples are persistent.
9 The implementation scans candidates once; a prefix invariant below justifies that
10 this is the earliest-consistent learner, not a different search convention.
11 No returned result represents interruption of host execution.
12 -/
13 
14 namespace Komorebi.MachineTheory.Synthesis
15 
16 universe u v w
17 
18 structure Task (P : Type u) (D : Type v) (Y : Type w) where
19   eval : P → D → Y
20   target : D → Y
21   contexts : List D
22   complete : ∀ x, x ∈ contexts
23 
24 variable {P : Type u} {D : Type v} {Y : Type w} [DecidableEq Y]
25 
26 /-- A literal short-circuit scan: first disagreement and number of comparisons. -/
27 def inspect (T : Task P D Y) (p : P) : List D → Option D × Nat
28   | [] => (none, 0)
29   | x :: xs =>
30     if T.eval p x = T.target x then
31       let r := inspect T p xs
32       (r.1, r.2 + 1)
33     else (some x, 1)
34 
35 def Correct (T : Task P D Y) (p : P) : Prop := ∀ x, T.eval p x = T.target x
36 
37 def Refuted (T : Task P D Y) (E : List D) (p : P) : Prop :=
38   ∃ x ∈ E, T.eval p x ≠ T.target x
39 
40 def Consistent (T : Task P D Y) (E : List D) (p : P) : Prop :=
41   ∀ x ∈ E, T.eval p x = T.target x
42 
43 @[simp] theorem inspect_none_iff (T : Task P D Y) (p : P) (E : List D) :
44     (inspect T p E).1 = none ↔ Consistent T E p := by
45   induction E with
46   | nil => simp [inspect, Consistent]
47   | cons x xs ih =>
48     by_cases hx : T.eval p x = T.target x
49     · simp [inspect, hx, Consistent, ih, Consistent] at *
50     · simp [inspect, hx, Consistent]
51 
52 theorem inspect_some (T : Task P D Y) (p : P) (E : List D) (x : D)
53     (h : (inspect T p E).1 = some x) : x ∈ E ∧ T.eval p x ≠ T.target x := by
54   induction E with
55   | nil => simp [inspect] at h
56   | cons y ys ih =>
57     by_cases hy : T.eval p y = T.target y
58     · simp only [inspect, hy, ↓reduceIte] at h
59       exact ⟨List.mem_cons_of_mem y (ih h).1, (ih h).2⟩
60     · simp only [inspect, hy, ↓reduceIte, Option.some.injEq] at h
61       subst x
62       exact ⟨List.mem_cons_self, hy⟩
63 
64 theorem inspect_none_of_correct (T : Task P D Y) {p : P} (h : Correct T p)
65     (E : List D) : (inspect T p E).1 = none := by
66   apply (inspect_none_iff T p E).2
67   intro x _
68   exact h x
69 
70 theorem refuted_iff_inspect_ne_none (T : Task P D Y) (E : List D) (p : P) :
71     Refuted T E p ↔ (inspect T p E).1 ≠ none := by
72   classical
73   simp only [ne_eq, inspect_none_iff, Consistent, Refuted]
74   push Not
75   rfl
76 
77 /-- The actual deterministic, extensional, complete finite teacher. -/
78 def teacher (T : Task P D Y) (p : P) : Option D := (inspect T p T.contexts).1
79 
80 @[simp] theorem teacher_accepts_iff (T : Task P D Y) (p : P) :
81     teacher T p = none ↔ Correct T p := by
82   rw [teacher, inspect_none_iff]
83   exact ⟨fun h x => h x (T.complete x), fun h x _ => h x⟩
84 
85 theorem teacher_refutes (T : Task P D Y) {p : P} {x : D}
86     (h : teacher T p = some x) : T.eval p x ≠ T.target x :=
87   (inspect_some T p T.contexts x h).2
88 
89 /-- The fixed teacher's rejection is the first disagreement in its context order. -/
90 theorem inspect_first (T : Task P D Y) (p : P) (E : List D) :
91     (inspect T p E).1 = E.find? (fun x => decide (T.eval p x ≠ T.target x)) := by
92   induction E with
93   | nil => rfl
94   | cons x xs ih =>
95     by_cases hx : T.eval p x = T.target x
96     · simp [inspect, hx, ih]
97     · simp [inspect, hx]
98 
99 theorem inspect_comparisons_le (T : Task P D Y) (p : P) (E : List D) :
100     (inspect T p E).2 ≤ E.length := by
101   induction E with
102   | nil => simp [inspect]
103   | cons x xs ih =>
104     by_cases hx : T.eval p x = T.target x
105     · simp only [inspect, hx, ↓reduceIte, List.length_cons]
106       omega
107     · simp [inspect, hx]
108 
109 structure Result (P : Type u) (D : Type v) where
110   answer : Option P
111   transcript : List (P × Option D)
112   retained : List D
113   comparisons : Nat
114   visits : Nat
115   deriving Repr, DecidableEq
116 
117 /-- Candidate scan. Rejected examples are prepended, defining a fixed test order. -/
118 def scan (T : Task P D Y) : List P → List D → Result P D
119   | [], E => ⟨none, [], E, 0, 0⟩
120   | p :: ps, E =>
121     let c := inspect T p E
122     match c.1 with
123     | some _ =>
124       let r := scan T ps E
125       ⟨r.answer, r.transcript, r.retained, c.2 + r.comparisons, 1 + r.visits⟩
126     | none =>
127       match teacher T p with
128       | none => ⟨some p, [(p, none)], E, c.2, 1⟩
129       | some x =>
130         let r := scan T ps (x :: E)
131         ⟨r.answer, (p, some x) :: r.transcript, r.retained,
132           c.2 + r.comparisons, 1 + r.visits⟩
133 
134 /-- Result semantics exclude only the separately metered search costs. -/
135 def SameEvidence (r s : Result P D) : Prop :=
136   r.answer = s.answer ∧ r.transcript = s.transcript ∧ r.retained = s.retained
137 
138 /-- No accepted candidate is replaced by a different but equivalent syntax. -/
139 theorem scan_answer (T : Task P D Y) (G : List P) (E : List D) :
140     (scan T G E).answer = G.find? (fun p => (teacher T p).isNone) := by
141   induction G generalizing E with
142   | nil => rfl
143   | cons p ps ih =>
144     cases hc : (inspect T p E).1 with
145     | some x =>
146       have hn : teacher T p ≠ none := by
147         intro ht
148         have hp := (teacher_accepts_iff T p).mp ht
149         have hi := inspect_none_of_correct T hp E
150         rw [hc] at hi
151         contradiction
152       cases ht : teacher T p with
153       | none => exact False.elim (hn ht)
154       | some y => simp [scan, hc, ht, ih]
155     | none =>
156       cases ht : teacher T p with
157       | none => simp [scan, hc, ht]
158       | some x => simp [scan, hc, ht, ih]
159 
160 /-- A complete scan exhausts exactly when no program in its grammar is correct. -/
161 theorem exhaustion_iff (T : Task P D Y) (G : List P) (E : List D) :
162     (scan T G E).answer = none ↔ ∀ p ∈ G, ¬ Correct T p := by
163   rw [scan_answer, List.find?_eq_none]
164   simp only [Option.isNone_iff_eq_none, teacher_accepts_iff]
165 
166 /-- The accepted syntax is the earliest globally correct grammar entry. -/
167 theorem accepted_first (T : Task P D Y) (G : List P) (E : List D) {p : P}
168     (hp : (scan T G E).answer = some p) :
169     ∃ before after, G = before ++ p :: after ∧ Correct T p ∧
170       ∀ q ∈ before, ¬ Correct T q := by
171   rw [scan_answer, List.find?_eq_some_iff_append] at hp
172   rcases hp with ⟨ht, before, after, h, hbefore⟩
173   refine ⟨before, after, h, ?_, ?_⟩
174   · exact (teacher_accepts_iff T p).mp (Option.isNone_iff_eq_none.mp ht)
175   · intro q hq hgood
176     have he := (teacher_accepts_iff T q).mpr hgood
177     have hn := hbefore q hq
178     simp [he] at hn
179 
180 /-- The teacher transcript follows the original candidate order without re-entry. -/
181 theorem transcript_sublist (T : Task P D Y) (G : List P) (E : List D) :
182     ((scan T G E).transcript.map Prod.fst).Sublist G := by
183   induction G generalizing E with
184   | nil => exact List.Sublist.refl []
185   | cons p ps ih =>
186     cases hc : (inspect T p E).1 with
187     | some x => simpa [scan, hc] using (ih E).cons p
188     | none =>
189       cases ht : teacher T p with
190       | none => simp [scan, hc, ht]
191       | some x => simpa [scan, hc, ht] using (ih (x :: E)).cons_cons p
192 
193 /-- Core 6.1's bound counts actual teacher calls, including final acceptance. -/
194 theorem teacher_calls_le (T : Task P D Y) (G : List P) (E : List D) :
195     (scan T G E).transcript.length ≤ G.length := by
196   simpa using (transcript_sublist T G E).length_le
197 
198 /-- No repeated submission in a grammar of distinct syntax objects. -/
199 theorem submitted_nodup (T : Task P D Y) (G : List P) (hG : G.Nodup) (E : List D) :
200     ((scan T G E).transcript.map Prod.fst).Nodup :=
201   hG.sublist (transcript_sublist T G E)
202 
203 /-- Every logged rejection is a real counterexample for the submitted AST. -/
204 theorem transcript_rejections (T : Task P D Y) (G : List P) (E : List D) :
205     ∀ p x, (p, some x) ∈ (scan T G E).transcript → T.eval p x ≠ T.target x := by
206   induction G generalizing E with
207   | nil => simp [scan]
208   | cons p ps ih =>
209     cases hc : (inspect T p E).1 with
210     | some x => simpa [scan, hc] using ih E
211     | none =>
212       cases ht : teacher T p with
213       | none => simp [scan, hc, ht]
214       | some x =>
215         intro q y hy
216         simp only [scan, hc, ht, List.mem_cons, Prod.mk.injEq, Option.some.injEq] at hy
217         rcases hy with ⟨rfl, rfl⟩ | hy
218         · exact teacher_refutes T ht
219         · exact ih (x :: E) q y hy
220 
221 /-- Old evidence remains available; a short scan cannot erase a constraint. -/
222 theorem retained_persistent (T : Task P D Y) (G : List P) (E : List D) :
223     ∀ x ∈ E, x ∈ (scan T G E).retained := by
224   induction G generalizing E with
225   | nil => simp [scan]
226   | cons p ps ih =>
227     cases hc : (inspect T p E).1 with
228     | some x => simpa [scan, hc] using ih E
229     | none =>
230       cases ht : teacher T p with
231       | none => simp [scan, hc, ht]
232       | some x =>
233         intro y hy
234         simpa [scan, hc, ht] using ih (x :: E) y (List.mem_cons_of_mem x hy)
235 
236 /-- One explicit source-facing contract bundles termination outcomes and call bound. -/
237 theorem finite_synthesis (T : Task P D Y) (G : List P) (E : List D) :
238     (scan T G E).transcript.length ≤ G.length ∧
239     ((scan T G E).answer = none ↔ ∀ p ∈ G, ¬ Correct T p) ∧
240     (∀ p, (scan T G E).answer = some p →
241       ∃ before after, G = before ++ p :: after ∧ Correct T p ∧
242         ∀ q ∈ before, ¬ Correct T q) := by
243   exact ⟨teacher_calls_le T G E, exhaustion_iff T G E, fun _ hp => accepted_first T G E hp⟩
244 
245 end Komorebi.MachineTheory.Synthesis

Back to source controls