SynthesisProtocol.lean

1 import MachineTheory.SynthesisTrace
2 
3 /-!
4 # Any truthful counterexample choice obeys the finite bound
5 
6 Core 6.1 does not need a first-counterexample oracle. This relation admits any
7 truthful reply at each call, including history-dependent choices, and also finite
8 open prefixes. The fixed complete teacher is used only for the actual reference
9 implementation and for Core 6.2's exact-trace comparison.
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 inductive TraceStatus (P : Type u) where
18   | pending | exhausted | accepted (p : P)
19   deriving Repr, DecidableEq
20 
21 /-- The last constructor permits a truthful teacher to choose any counterexample. -/
22 inductive TruthfulProtocol (T : Task P D Y) (G : List P) :
23     List D → List (P × Option D) → TraceStatus P → Prop
24   | pending (E) : TruthfulProtocol T G E [] .pending
25   | exhausted (E) (h : select T G E = none) : TruthfulProtocol T G E [] .exhausted
26   | accepted (E p) (hs : select T G E = some p) (hc : Correct T p) :
27       TruthfulProtocol T G E [(p,none)] (.accepted p)
28   | rejected (E p x tr out) (hs : select T G E = some p)
29       (hx : T.eval p x ≠ T.target x) (rest : TruthfulProtocol T G (x :: E) tr out) :
30       TruthfulProtocol T G E ((p,some x) :: tr) out
31 
32 theorem truthful_excludes_refuted (T : Task P D Y) {G : List P} {E : List D}
33     {tr : List (P × Option D)} {out : TraceStatus P}
34     (h : TruthfulProtocol T G E tr out) {p : P} (hp : Refuted T E p) :
35     p ∉ tr.map Prod.fst := by
36   induction h with
37   | pending => simp
38   | exhausted => simp
39   | accepted E q hs hc =>
40     have hn : p ≠ q := by
41       intro he; subst q
42       exact refuted_not_consistent T hp (select_some_consistent T G E hs)
43     simpa using hn
44   | rejected E q x tr out hs hx rest ih =>
45     have hn : p ≠ q := by
46       intro he; subst q
47       exact refuted_not_consistent T hp (select_some_consistent T G E hs)
48     simpa using And.intro hn (ih (refuted_cons T hp x))
49 
50 theorem truthful_nodup (T : Task P D Y) {G : List P} {E : List D}
51     {tr : List (P × Option D)} {out : TraceStatus P}
52     (h : TruthfulProtocol T G E tr out) : (tr.map Prod.fst).Nodup := by
53   induction h with
54   | pending => simp
55   | exhausted => simp
56   | accepted => simp
57   | rejected E p x tr out hs hx rest ih =>
58     have hr : Refuted T (x :: E) p := ⟨x, List.mem_cons_self, hx⟩
59     simpa using And.intro (truthful_excludes_refuted T rest hr) ih
60 
61 theorem truthful_members (T : Task P D Y) {G : List P} {E : List D}
62     {tr : List (P × Option D)} {out : TraceStatus P}
63     (h : TruthfulProtocol T G E tr out) : tr.map Prod.fst ⊆ G := by
64   induction h with
65   | pending => simp
66   | exhausted => simp
67   | accepted E p hs hc =>
68     have hp : p ∈ G := List.mem_of_find?_eq_some hs
69     simpa using hp
70   | rejected E p x tr out hs hx rest ih =>
71     have hp : p ∈ G := List.mem_of_find?_eq_some hs
72     simpa using And.intro hp ih
73 
74 /-- Applies even to open finite prefixes and arbitrary truthful reply choices. -/
75 theorem truthful_call_bound (T : Task P D Y) {G : List P} {E : List D}
76     {tr : List (P × Option D)} {out : TraceStatus P}
77     (h : TruthfulProtocol T G E tr out) : tr.length ≤ G.length := by
78   simpa using (truthful_nodup T h).length_le_of_subset (truthful_members T h)
79 
80 /-- An unbounded sequence of truthful teacher calls would give an impossible prefix. -/
81 theorem no_unbounded_truthful_calls (T : Task P D Y) (G : List P) (E : List D) :
82     ¬ (∀ n : Nat, ∃ tr out, TruthfulProtocol T G E tr out ∧ tr.length = n) := by
83   intro h
84   obtain ⟨tr, out, hr, hn⟩ := h (G.length + 1)
85   have hb := truthful_call_bound T hr
86   omega
87 
88 /-- Current finite exhaustion is an explicit statement about the declared grammar. -/
89 theorem select_none_excludes_correct (T : Task P D Y) (G : List P) (E : List D)
90     (h : select T G E = none) : ∀ p ∈ G, ¬ Correct T p := by
91   have hh := List.find?_eq_none.mp h
92   intro p hp hc
93   have hn := hh p hp
94   have hi := inspect_none_of_correct T hc E
95   simp [hi] at hn
96 
97 /-- The earliest consistent correct entry is the earliest globally correct entry. -/
98 theorem selected_correct_is_first (T : Task P D Y) (G : List P) (E : List D) {p : P}
99     (h : select T G E = some p) (hc : Correct T p) :
100     G.find? (fun q => (teacher T q).isNone) = some p := by
101   have hsplit := List.find?_eq_some_iff_append.mp h
102   rcases hsplit with ⟨_, before, after, hG, hbefore⟩
103   apply List.find?_eq_some_iff_append.mpr
104   refine ⟨Option.isNone_iff_eq_none.mpr ((teacher_accepts_iff T p).mpr hc), before, after, hG, ?_⟩
105   intro q hq
106   have hbad := hbefore q hq
107   have hnot : ¬ Correct T q := by
108     intro hgood
109     have he := inspect_none_of_correct T hgood E
110     simp [he] at hbad
111   cases ht : teacher T q with
112   | none => exact False.elim (hnot ((teacher_accepts_iff T q).mp ht))
113   | some x => rfl
114 
115 /-- Final answers and grammar exhaustion are sound for ANY truthful protocol. -/
116 theorem truthful_outcome (T : Task P D Y) {G : List P} {E : List D}
117     {tr : List (P × Option D)} {out : TraceStatus P}
118     (h : TruthfulProtocol T G E tr out) :
119     (∀ p, out = .accepted p → G.find? (fun q => (teacher T q).isNone) = some p) ∧
120     (out = .exhausted → ∀ p ∈ G, ¬ Correct T p) := by
121   induction h with
122   | pending => simp
123   | exhausted E hs =>
124     exact ⟨by simp, fun _ => select_none_excludes_correct T G E hs⟩
125   | accepted E p hs hc =>
126     constructor
127     · intro q hq
128       cases hq
129       exact selected_correct_is_first T G E hs hc
130     · simp
131   | rejected E p x tr out hs hx rest ih => exact ih
132 
133 /-- The executable complete teacher is one realization of the general reply contract. -/
134 theorem protocol_is_truthful (T : Task P D Y) {G : List P} {E : List D}
135     {tr : List (P × Option D)} {ans : Option P} (h : Protocol T G E tr ans) :
136     TruthfulProtocol T G E tr (match ans with | none => .exhausted | some p => .accepted p) := by
137   induction h with
138   | exhausted E hs => exact TruthfulProtocol.exhausted E hs
139   | accepted E p hs ht => exact TruthfulProtocol.accepted E p hs ((teacher_accepts_iff T p).mp ht)
140   | rejected E p x tr ans hs ht rest ih =>
141     cases ans <;> exact TruthfulProtocol.rejected E p x tr _ hs (teacher_refutes T ht) ih
142 
143 end Komorebi.MachineTheory.Synthesis

Back to source controls