SynthesisTrace.lean

1 import MachineTheory.SynthesisQuotient
2 
3 /-!
4 # The scan is the stated restart-earliest protocol
5 
6 The operational relation searches the entire original grammar again at each
7 teacher call. Its proof from `scan` shows that omitting already refuted prefixes
8 changes neither submissions nor retained evidence. Repeated syntax entries in a
9 list cannot cause repeated submission after rejection.
10 -/
11 
12 namespace Komorebi.MachineTheory.Synthesis
13 
14 universe u v w
15 variable {P : Type u} {D : Type v} {Y : Type w} [DecidableEq Y]
16 
17 def select (T : Task P D Y) (G : List P) (E : List D) : Option P :=
18   G.find? (fun p => ((inspect T p E).1).isNone)
19 
20 theorem select_some_consistent (T : Task P D Y) (G : List P) (E : List D)
21     {p : P} (h : select T G E = some p) : Consistent T E p := by
22   have hh := List.find?_some h
23   exact (inspect_none_iff T p E).mp (Option.isNone_iff_eq_none.mp hh)
24 
25 omit [DecidableEq Y] in
26 theorem refuted_not_consistent (T : Task P D Y) {E : List D} {p : P}
27     (h : Refuted T E p) : ¬ Consistent T E p := by
28   rcases h with ⟨x, hx, hdiff⟩
29   exact fun hc => hdiff (hc x hx)
30 
31 theorem select_refuted_prefix (T : Task P D Y) (B G : List P) (E : List D)
32     (hb : ∀ p ∈ B, Refuted T E p) : select T (B ++ G) E = select T G E := by
33   induction B with
34   | nil => rfl
35   | cons p ps ih =>
36     have hn := (refuted_iff_inspect_ne_none T E p).mp (hb p List.mem_cons_self)
37     have ht : ∀ q ∈ ps, Refuted T E q := fun q hq => hb q (List.mem_cons_of_mem p hq)
38     cases hc : (inspect T p E).1 with
39     | none => exact False.elim (hn hc)
40     | some x => simpa [select, hc] using ih ht
41 
42 /-- Genuine earliest-consistent interaction on the WHOLE supplied grammar. -/
43 inductive Protocol (T : Task P D Y) (G : List P) :
44     List D → List (P × Option D) → Option P → Prop
45   | exhausted (E) (h : select T G E = none) : Protocol T G E [] none
46   | accepted (E p) (hs : select T G E = some p) (ht : teacher T p = none) :
47       Protocol T G E [(p, none)] (some p)
48   | rejected (E p x tr ans) (hs : select T G E = some p) (ht : teacher T p = some x)
49       (rest : Protocol T G (x :: E) tr ans) :
50       Protocol T G E ((p, some x) :: tr) ans
51 
52 /-- Refuted prefixes stay refuted at every later restart of the protocol. -/
53 theorem protocol_prefix (T : Task P D Y) {G : List P} {E : List D}
54     {tr : List (P × Option D)} {ans : Option P} (h : Protocol T G E tr ans)
55     (B : List P) (hb : ∀ p ∈ B, Refuted T E p) : Protocol T (B ++ G) E tr ans := by
56   induction h with
57   | exhausted E hs =>
58     exact Protocol.exhausted E ((select_refuted_prefix T B G E hb).trans hs)
59   | accepted E p hs ht =>
60     exact Protocol.accepted E p ((select_refuted_prefix T B G E hb).trans hs) ht
61   | rejected E p x tr ans hs ht rest ih =>
62     apply Protocol.rejected E p x tr ans
63       ((select_refuted_prefix T B G E hb).trans hs) ht
64     exact ih (fun q hq => refuted_cons T (hb q hq) x)
65 
66 /-- A structurally recursive implementation realizes the specified learner exactly. -/
67 theorem scan_protocol (T : Task P D Y) (G : List P) (E : List D) :
68     Protocol T G E (scan T G E).transcript (scan T G E).answer := by
69   induction G generalizing E with
70   | nil => exact Protocol.exhausted E rfl
71   | cons p ps ih =>
72     cases hc : (inspect T p E).1 with
73     | some x =>
74       have hp : Refuted T E p :=
75         ⟨x, (inspect_some T p E x hc).1, (inspect_some T p E x hc).2⟩
76       have hprefix := protocol_prefix T (ih E) [p] (by simpa using hp)
77       simpa [scan, hc] using hprefix
78     | none =>
79       have hs : select T (p :: ps) E = some p := by simp [select, hc]
80       cases ht : teacher T p with
81       | none => simpa [scan, hc, ht] using Protocol.accepted (T := T) E p hs ht
82       | some x =>
83         have hp : Refuted T (x :: E) p :=
84           ⟨x, List.mem_cons_self, teacher_refutes T ht⟩
85         have hprefix := protocol_prefix T (ih (x :: E)) [p] (by simpa using hp)
86         simpa [scan, hc, ht] using Protocol.rejected E p x
87           (scan T ps (x :: E)).transcript (scan T ps (x :: E)).answer hs ht hprefix
88 
89 /-- Rejection is exclusion from every future teacher call, even with duplicate syntax. -/
90 theorem protocol_excludes_refuted (T : Task P D Y) {G : List P} {E : List D}
91     {tr : List (P × Option D)} {ans : Option P} (h : Protocol T G E tr ans)
92     {p : P} (hp : Refuted T E p) : p ∉ tr.map Prod.fst := by
93   induction h with
94   | exhausted => simp
95   | accepted E q hs ht =>
96     have hne : p ≠ q := by
97       intro he
98       subst q
99       exact refuted_not_consistent T hp (select_some_consistent T G E hs)
100     simpa using hne
101   | rejected E q x tr ans hs ht rest ih =>
102     have hne : p ≠ q := by
103       intro he
104       subst q
105       exact refuted_not_consistent T hp (select_some_consistent T G E hs)
106     have hn := ih (refuted_cons T hp x)
107     simpa [List.map_cons] using And.intro hne hn
108 
109 /-- Distinct calls need no duplicate-free assumption on the original catalogue. -/
110 theorem protocol_nodup (T : Task P D Y) {G : List P} {E : List D}
111     {tr : List (P × Option D)} {ans : Option P} (h : Protocol T G E tr ans) :
112     (tr.map Prod.fst).Nodup := by
113   induction h with
114   | exhausted => simp
115   | accepted => simp
116   | rejected E p x tr ans hs ht rest ih =>
117     have hr : Refuted T (x :: E) p := ⟨x, List.mem_cons_self, teacher_refutes T ht⟩
118     have hn := protocol_excludes_refuted T rest hr
119     simpa using And.intro hn ih
120 
121 theorem no_repeated_submission (T : Task P D Y) (G : List P) (E : List D) :
122     ((scan T G E).transcript.map Prod.fst).Nodup :=
123   protocol_nodup T (scan_protocol T G E)
124 
125 /-- Every reported counterexample, not just initial evidence, remains in final memory. -/
126 theorem rejected_evidence_retained (T : Task P D Y) (G : List P) (E : List D) :
127     ∀ p x, (p, some x) ∈ (scan T G E).transcript → x ∈ (scan T G E).retained := by
128   induction G generalizing E with
129   | nil => simp [scan]
130   | cons p ps ih =>
131     cases hc : (inspect T p E).1 with
132     | some x => simpa [scan, hc] using ih E
133     | none =>
134       cases ht : teacher T p with
135       | none => simp [scan, hc, ht]
136       | some x =>
137         intro q y hy
138         simp only [scan, hc, ht, List.mem_cons, Prod.mk.injEq, Option.some.injEq] at hy
139         simp only [scan, hc, ht]
140         rcases hy with ⟨rfl, rfl⟩ | hy
141         · exact retained_persistent T ps (y :: E) y List.mem_cons_self
142         · exact ih (x :: E) q y hy
143 
144 /-- Core 6.1, with the actual restart protocol and unconditional no-repeat property. -/
145 theorem counterexample_guided_synthesis (T : Task P D Y) (G : List P) :
146     Protocol T G [] (scan T G []).transcript (scan T G []).answer ∧
147     ((scan T G []).transcript.map Prod.fst).Nodup ∧
148     (scan T G []).transcript.length ≤ G.length ∧
149     ((scan T G []).answer = none ↔ ∀ p ∈ G, ¬ Correct T p) := by
150   exact ⟨scan_protocol T G [], no_repeated_submission T G [],
151     teacher_calls_le T G [], exhaustion_iff T G []⟩
152 
153 end Komorebi.MachineTheory.Synthesis

Back to source controls