SynthesisQuotient.lean

1 import MachineTheory.Synthesis
2 
3 /-!
4 # Sound ordered semantic compression
5 
6 Reviewed Core 6.2. The quotient keeps the first ORIGINAL syntax value at each key.
7 Keys are an external checked interface. A soundness premise is not replaced by
8 finite probe agreement. The same scan, teacher, target and retained-example order
9 are used on both sides. Preparation, key comparisons, index storage and dispatch
10 are not included in the retained-example comparison counter.
11 -/
12 
13 namespace Komorebi.MachineTheory.Synthesis
14 
15 universe u v w z
16 variable {P : Type u} {D : Type v} {Y : Type w} {K : Type z}
17 variable [DecidableEq Y] [DecidableEq K]
18 
19 /-- Only one direction of semantic identification is required. -/
20 def KeySound (T : Task P D Y) (key : P → K) : Prop :=
21   ∀ p q, key p = key q → ∀ x, T.eval p x = T.eval q x
22 
23 /-- Prefix keys have already been refuted by persistent available evidence. -/
24 def KeysRefuted (T : Task P D Y) (key : P → K) (seen : List K) (E : List D) : Prop :=
25   ∀ p, key p ∈ seen → Refuted T E p
26 
27 /-- Keep the first original AST at each key, never its normalized replacement. -/
28 def representatives (key : P → K) : List K → List P → List P
29   | _, [] => []
30   | seen, p :: ps =>
31     if key p ∈ seen then representatives key seen ps
32     else p :: representatives key (key p :: seen) ps
33 
34 omit [DecidableEq Y] in
35 theorem refuted_cons (T : Task P D Y) {E : List D} {p : P}
36     (h : Refuted T E p) (x : D) : Refuted T (x :: E) p := by
37   rcases h with ⟨y, hy, hdiff⟩
38   exact ⟨y, List.mem_cons_of_mem x hy, hdiff⟩
39 
40 omit [DecidableEq Y] [DecidableEq K] in
41 theorem keysRefuted_cons_evidence (T : Task P D Y) (key : P → K)
42     {seen : List K} {E : List D} (h : KeysRefuted T key seen E) (x : D) :
43     KeysRefuted T key seen (x :: E) := by
44   intro p hp
45   exact refuted_cons T (h p hp) x
46 
47 omit [DecidableEq Y] [DecidableEq K] in
48 theorem keysRefuted_add_key (T : Task P D Y) (key : P → K)
49     (hs : KeySound T key) {seen : List K} {E : List D}
50     (h : KeysRefuted T key seen E) {p : P} (hp : Refuted T E p) :
51     KeysRefuted T key (key p :: seen) E := by
52   intro q hq
53   rcases List.mem_cons.mp hq with hqp | hq
54   · rcases hp with ⟨x, hx, hdiff⟩
55     refine ⟨x, hx, ?_⟩
56     rw [hs q p hqp x]
57     exact hdiff
58   · exact h q hq
59 
60 theorem representatives_sublist (key : P → K) (seen : List K) (G : List P) :
61     (representatives key seen G).Sublist G := by
62   induction G generalizing seen with
63   | nil => exact List.Sublist.refl []
64   | cons p ps ih =>
65     by_cases hk : key p ∈ seen
66     · simpa [representatives, hk] using (ih seen).cons p
67     · simpa [representatives, hk] using (ih (key p :: seen)).cons_cons p
68 
69 /-- The deletion invariant proves full trace equality, not merely equal outputs. -/
70 theorem compression_invariant (T : Task P D Y) (key : P → K) (hs : KeySound T key)
71     (G : List P) (seen : List K) (E : List D)
72     (hseen : KeysRefuted T key seen E) :
73     SameEvidence (scan T (representatives key seen G) E) (scan T G E) ∧
74     (scan T (representatives key seen G) E).comparisons ≤ (scan T G E).comparisons ∧
75     (scan T (representatives key seen G) E).visits ≤ (scan T G E).visits := by
76   induction G generalizing seen E with
77   | nil => simp [scan, representatives, SameEvidence]
78   | cons p ps ih =>
79     by_cases hk : key p ∈ seen
80     · have hr := (refuted_iff_inspect_ne_none T E p).mp (hseen p hk)
81       cases hc : (inspect T p E).1 with
82       | none => exact False.elim (hr hc)
83       | some x =>
84         obtain ⟨⟨ha, ht, he⟩, hcost, hvis⟩ := ih seen E hseen
85         simp only [representatives, hk, ↓reduceIte, scan, hc, SameEvidence]
86         exact ⟨⟨ha, ht, he⟩, by omega, by omega⟩
87     · cases hc : (inspect T p E).1 with
88       | some x =>
89         have hp : Refuted T E p := ⟨x, (inspect_some T p E x hc).1,
90           (inspect_some T p E x hc).2⟩
91         have hn := keysRefuted_add_key T key hs hseen hp
92         obtain ⟨⟨ha, ht, he⟩, hcost, hvis⟩ := ih (key p :: seen) E hn
93         simp only [representatives, hk, ↓reduceIte, scan, hc, SameEvidence]
94         exact ⟨⟨ha, ht, he⟩, Nat.add_le_add_left hcost _, Nat.add_le_add_left hvis _⟩
95       | none =>
96         cases ht : teacher T p with
97         | none => simp [representatives, hk, scan, hc, ht, SameEvidence]
98         | some x =>
99           have hp : Refuted T (x :: E) p :=
100             ⟨x, List.mem_cons_self, teacher_refutes T ht⟩
101           have hn := keysRefuted_add_key T key hs
102             (keysRefuted_cons_evidence T key hseen x) hp
103           obtain ⟨⟨ha, htr, he⟩, hcost, hvis⟩ := ih (key p :: seen) (x :: E) hn
104           simp only [representatives, hk, ↓reduceIte, scan, hc, ht, SameEvidence]
105           exact ⟨⟨ha, congrArg ((p, some x) :: ·) htr, he⟩,
106             Nat.add_le_add_left hcost _, Nat.add_le_add_left hvis _⟩
107 
108 /-- Core 6.2: exact AST/reply/evidence preservation and nonincreasing search checks. -/
109 theorem ordered_compression (T : Task P D Y) (key : P → K) (hs : KeySound T key)
110     (G : List P) (E : List D) :
111     SameEvidence (scan T (representatives key [] G) E) (scan T G E) ∧
112     (scan T (representatives key [] G) E).comparisons ≤ (scan T G E).comparisons ∧
113     (scan T (representatives key [] G) E).visits ≤ (scan T G E).visits :=
114   compression_invariant T key hs G [] E (by simp [KeysRefuted])
115 
116 /-- Both front ends invoke the very same finite-context teacher on the same ASTs. -/
117 def teacherComparisons (T : Task P D Y) (r : Result P D) : Nat :=
118   (r.transcript.map (fun e => (inspect T e.1 T.contexts).2)).sum
119 
120 theorem teacher_work_preserved (T : Task P D Y) (key : P → K) (hs : KeySound T key)
121     (G : List P) (E : List D) :
122     teacherComparisons T (scan T (representatives key [] G) E) =
123       teacherComparisons T (scan T G E) := by
124   unfold teacherComparisons
125   rw [(ordered_compression T key hs G E).1.2.1]
126 
127 /-- Only admissible-domain soundness is used; no semantic completeness is needed. -/
128 theorem representative_search_complete (T : Task P D Y) (key : P → K)
129     (hs : KeySound T key) (G : List P) (E : List D) :
130     (scan T (representatives key [] G) E).answer = none ↔
131       ∀ p ∈ G, ¬ Correct T p := by
132   rw [(ordered_compression T key hs G E).1.1]
133   exact exhaustion_iff T G E
134 
135 
136 /-- Actual key-comparison work of the simple list-backed representative index. -/
137 def lookupKey (k : K) : List K → Bool × Nat
138   | [] => (false, 0)
139   | q :: qs => if k = q then (true, 1) else
140       let r := lookupKey k qs
141       (r.1, 1 + r.2)
142 
143 @[simp] theorem lookupKey_value (k : K) (seen : List K) :
144     (lookupKey k seen).1 = decide (k ∈ seen) := by
145   induction seen with
146   | nil => simp [lookupKey]
147   | cons q qs ih =>
148     by_cases h : k = q
149     · simp [lookupKey, h]
150     · simp [lookupKey, h, ih]
151 
152 /-- Only equality comparisons are metered here; key computation and storage are separate. -/
153 def prepare (key : P → K) : List K → List P → List P × Nat
154   | _, [] => ([], 0)
155   | seen, p :: ps =>
156     let q := lookupKey (key p) seen
157     if q.1 then
158       let r := prepare key seen ps
159       (r.1, q.2 + r.2)
160     else
161       let r := prepare key (key p :: seen) ps
162       (p :: r.1, q.2 + r.2)
163 
164 theorem prepare_value (key : P → K) (seen : List K) (G : List P) :
165     (prepare key seen G).1 = representatives key seen G := by
166   induction G generalizing seen with
167   | nil => rfl
168   | cons p ps ih =>
169     by_cases h : key p ∈ seen
170     · simp [prepare, representatives, h, ih]
171     · simp [prepare, representatives, h, ih]
172 
173 end Komorebi.MachineTheory.Synthesis

Back to source controls