PrefixSemantics.lean

1 import MachineTheory.OrderedCompiler
2 
3 /-!
4 # Linking scanned rows and compiled trees to the inherited model
5 
6 Numerical feasibility of filling two bins is not sufficient for diagnosis. Here
7 capacity necessity follows from the actual immutable/singleton tree semantics.
8 The full ordered compiler is proved sound and complete for the supplied finite
9 query and repair catalogues. The streaming theorem transfers those conclusions.
10 -/
11 namespace Komorebi.MachineTheory.OrderedCompiler
12 open HardInquiry BinaryDiagnosis Finset
13 variable {X E C : Type} [DecidableEq X]
14 
15 /-- A successful inherited tree cannot have more cases than its binary leaf capacity. -/
16 theorem valid_capacity (M : Model X E Bool C Unit) (s : Scope M)
17     (h : ℕ) (V : Finset X) (t : Tree E Bool C h) (ht : M.Valid h V t) : V.card ≤ 2^h := by
18   exact (cases_le_leaves M s h V t ht).trans ((leaves_le_pow_depth h t).trans
19     (Nat.pow_le_pow_right (by decide : 0<2) (depth_le_horizon h t)))
20 
21 theorem partition_support (M : Model X E Bool C Unit) (s : Scope M) (xs : List X) (e : E) :
22     (PrefixScan.partition (M.observe e) xs).1.toFinset = M.update xs.toFinset e false ∧
23     (PrefixScan.partition (M.observe e) xs).2.toFinset = M.update xs.toFinset e true := by
24   rw [PrefixScan.partition_filters,update_immutable M s,update_immutable M s]
25   constructor <;> ext x <;> simp
26 
27 omit [DecidableEq X] in
28 theorem partition_nodup (f : X → Bool) (xs : List X) (hn : xs.Nodup) :
29     (PrefixScan.partition f xs).1.Nodup ∧ (PrefixScan.partition f xs).2.Nodup := by
30   rw [PrefixScan.partition_filters]
31   exact ⟨hn.filter _,hn.filter _⟩
32 
33 /-- The final two capacities are necessary for the ACTUAL root and child horizon. -/
34 theorem valid_root_capacity (M : Model X E Bool C Unit) (s : Scope M)
35     (h : ℕ) (xs : List X) (hn : xs.Nodup) (e : E) (k : Bool → Option (Tree E Bool C h))
36     (hv : M.Valid (h+1) xs.toFinset (.inr (e,k))) :
37     max (PrefixScan.partition (M.observe e) xs).1.length
38       (PrefixScan.partition (M.observe e) xs).2.length ≤ 2^h := by
39   have bc : ∀ o, (M.update xs.toFinset e o).card ≤ 2^h := by
40     intro o
41     cases he : k o with
42     | none =>
43       have hz : M.update xs.toFinset e o = ∅ := by simpa only [he] using hv.2 o
44       simp only [hz,card_empty]; exact Nat.zero_le _
45     | some u => exact valid_capacity M s h _ u (by simpa only [he] using hv.2 o)
46   have hp := partition_support M s xs e
47   have hd := partition_nodup (M.observe e) xs hn
48   have h0 := bc false
49   have h1 := bc true
50   rw [← hp.1,List.toFinset_card_of_nodup hd.1] at h0
51   rw [← hp.2,List.toFinset_card_of_nodup hd.2] at h1
52   exact max_le h0 h1
53 
54 /-- Early rejection rules out every valid continuation under that root, not just the searched candidate. -/
55 theorem rejected_root_impossible (M : Model X E Bool C Unit) (s : Scope M)
56     (h : ℕ) (xs : List X) (hn : xs.Nodup) (e : E)
57     (hr : (streamScanner (M.observe e) (2^h) xs).branches=none) :
58     ¬ ∃ k : Bool → Option (Tree E Bool C h), M.Valid (h+1) xs.toFinset (.inr (e,k)) := by
59   rintro ⟨k,hk⟩
60   have hc := valid_root_capacity M s h xs hn e k hk
61   have he := PrefixScan.stream_branches (M.observe e) (2^h) 0 0 xs
62   change (PrefixScan.stream _ _ _ _ _).branches=none at hr
63   rw [he] at hr
64   simp only [PrefixScan.full,Nat.zero_add,hc,ite_true] at hr
65   cases hr
66 
67 /-- A previously observed sub-support alone can certify impossibility of a root. -/
68 theorem prefix_exclusion (M : Model X E Bool C Unit) (s : Scope M)
69     (h : ℕ) (V P : Finset X) (hPV : P ⊆ V) (e : E) (o : Bool)
70     (ho : 2^h < (P.filter (fun x => M.observe e x=o)).card) :
71     ¬ ∃ k : Bool → Option (Tree E Bool C h), M.Valid (h+1) V (.inr (e,k)) := by
72   rintro ⟨k,hk⟩
73   have hsub : P.filter (fun x => M.observe e x=o) ⊆ M.update V e o := by
74     rw [update_immutable M s]
75     exact Finset.filter_subset_filter _ hPV
76   have hcap : (M.update V e o).card ≤ 2^h := by
77     cases he : k o with
78     | none =>
79       have hz : M.update V e o=∅ := by simpa only [he] using hk.2 o
80       simp only [hz,card_empty]; exact Nat.zero_le _
81     | some u => exact valid_capacity M s h _ u (by simpa only [he] using hk.2 o)
82   exact (not_le_of_gt ho) ((Finset.card_le_card hsub).trans hcap)
83 
84 /-- Helpers expose the acceptance facts without treating raw row access as hidden knowledge. -/
85 theorem nonempty_support (xs : List X) (hx : xs.isEmpty=false) : xs.toFinset.Nonempty := by
86   cases xs with
87   | nil => cases hx
88   | cons x xs => exact ⟨x,by simp⟩
89 
90 theorem terminal_of_find (M : Model X E Bool C Unit) (xs : List X) (cs : List C)
91     (hx : xs.isEmpty=false) (c : C)
92     (hc : cs.find? (fun c => xs.all (fun x => M.accept x c))=some c) : M.Terminal xs.toFinset c := by
93   refine ⟨nonempty_support xs hx,?_⟩
94   have ha := List.find?_some hc
95   intro x h
96   exact List.all_eq_true.mp ha x (List.mem_toFinset.mp h)
97 
98 theorem child_correct (M : Model X E Bool C Unit) (h : ℕ) (next : List X → Run (Tree E Bool C h)) (xs : List X)
99     (sound : ∀ ys t, (next ys).answer=some t → M.Valid h ys.toFinset t)
100     (t : Option (Tree E Bool C h)) (ht : (child next xs).answer=some t) :
101     match t with
102     | none => xs.toFinset=∅
103     | some u => M.Valid h xs.toFinset u := by
104   by_cases hx : xs.isEmpty
105   · have he : xs=[] := List.isEmpty_iff.mp hx
106     subst xs
107     simp only [child,List.isEmpty_nil,ite_true,Run.pure] at ht
108     cases ht
109     rfl
110   · simp only [child,hx,Run.map] at ht
111     obtain ⟨u,hu,he⟩ := Option.map_eq_some_iff.mp ht
112     cases he
113     exact sound xs u hu
114 
115 /-- A returned root's stored children are exactly the possible report branches. -/
116 theorem attempt_sound (M : Model X E Bool C Unit) (s : Scope M) (h : ℕ)
117     (next : List X → Run (Tree E Bool C h)) (sound : ∀ ys t, (next ys).answer=some t → M.Valid h ys.toFinset t)
118     (xs : List X) (hx : xs.isEmpty=false) (e : E) (t : Tree E Bool C (h+1))
119     (ht : (attempt fullScanner M h next xs e).answer=some t) : M.Valid (h+1) xs.toFinset t := by
120   by_cases ha : xs.all (M.permitted e)
121   · simp only [attempt,ha,ite_true] at ht
122     obtain ⟨p,hp,hbuild⟩ := (Run.bind_some_iff _ _ _).mp ht
123     have hp' : p=PrefixScan.partition (M.observe e) xs := by
124       change (if max (0+_ ) (0+_) ≤ 2^h then some (PrefixScan.partition (M.observe e) xs) else none)=some p at hp
125       split at hp <;> simp_all
126     subst p
127     obtain ⟨l,hl,hRightBuild⟩ := (Run.bind_some_iff _ _ _).mp hbuild
128     obtain ⟨r,hRight,he⟩ := (Run.bind_some_iff _ _ _).mp hRightBuild
129     have he' : Sum.inr (e,fun o => if o then r else l)=t := Option.some.inj he
130     subst t
131     refine ⟨⟨nonempty_support xs hx,?_⟩,?_⟩
132     · intro x h
133       exact List.all_eq_true.mp ha x (List.mem_toFinset.mp h)
134     · have hleft := child_correct M h next _ sound l hl
135       have hright := child_correct M h next _ sound r hRight
136       have hp := partition_support M s xs e
137       intro o
138       cases o
139       · cases l <;> simpa only [Bool.false_eq_true,ite_false,hp.1] using hleft
140       · cases r <;> simpa only [ite_true,hp.2] using hright
141   · simp only [attempt,ha,Run.fail] at ht
142     cases ht
143 
144 /-- Soundness: each returned syntax is valid under the actual inherited semantics. -/
145 theorem full_search_sound (M : Model X E Bool C Unit) (s : Scope M) (es : List E) (cs : List C)
146     (h : ℕ) (xs : List X) (t : Tree E Bool C h)
147     (ht : (search fullScanner M es cs h xs).answer=some t) : M.Valid h xs.toFinset t := by
148   induction h generalizing xs with
149   | zero =>
150     by_cases hx : xs.isEmpty
151     · simp only [search,hx,ite_true,Run.fail] at ht; cases ht
152     · have hx' : xs.isEmpty=false := Bool.eq_false_iff.mpr hx
153       cases hc : cs.find? (fun c => xs.all (fun x => M.accept x c)) with
154       | none => simp only [search,hx,hc,Run.fail] at ht; cases ht
155       | some c =>
156         have ht' : (some c : Option (Tree E Bool C 0))=some t := by simpa [search,hx,hc,Run.pure] using ht
157         have he := Option.some.inj ht'
158         subst t
159         exact terminal_of_find M xs cs hx' c hc
160   | succ h ih =>
161     by_cases hx : xs.isEmpty
162     · simp only [search,hx,ite_true,Run.fail] at ht; cases ht
163     · have hx' : xs.isEmpty=false := Bool.eq_false_iff.mpr hx
164       cases hc : cs.find? (fun c => xs.all (fun x => M.accept x c)) with
165       | none =>
166         have hh : (Run.first (attempt fullScanner M h (search fullScanner M es cs h) xs) es).answer=some t := by
167           simpa [search,hx,hc] using ht
168         obtain ⟨e,_,he⟩ := Run.first_some_mem _ es t hh
169         exact attempt_sound M s h _ (fun ys u hu => ih ys u hu) xs hx' e t he
170       | some c =>
171         have ht' : (some (.inl c) : Option (Tree E Bool C (h+1)))=some t := by simpa [search,hx,hc,Run.pure] using ht
172         have he := Option.some.inj ht'
173         subst t
174         exact terminal_of_find M xs cs hx' c hc
175 
176 
177 
178 omit [DecidableEq X] in
179 /-- Absent reports have no installed child. A live report must actually be solved. -/
180 theorem child_exists (next : List X → Run A) (xs : List X)
181     (hx : xs=[] ∨ ∃ u, (next xs).answer=some u) :
182     ∃ t, (child next xs).answer=some t := by
183   by_cases he : xs.isEmpty
184   · exact ⟨none,by simp [child,he,Run.pure]⟩
185   · rcases hx with hz | ⟨u,hu⟩
186     · subst xs; simp at he
187     · exact ⟨some u,by simp [child,he,Run.map,hu]⟩
188 
189 theorem attempt_complete (M : Model X E Bool C Unit) (s : Scope M) (h : ℕ)
190     (next : List X → Run (Tree E Bool C h))
191     (complete : ∀ ys, ys.Nodup → ∀ u, M.Valid h ys.toFinset u → ∃ t, (next ys).answer=some t)
192     (xs : List X) (hn : xs.Nodup) (e : E) (k : Bool → Option (Tree E Bool C h))
193     (hv : M.Valid (h+1) xs.toFinset (.inr (e,k))) :
194     ∃ t, (attempt fullScanner M h next xs e).answer=some t := by
195   have ha : xs.all (M.permitted e)=true := by
196     apply List.all_eq_true.mpr
197     intro x hx
198     exact hv.1.2 x (List.mem_toFinset.mpr hx)
199   have hcap := valid_root_capacity M s h xs hn e k hv
200   have hp := partition_support M s xs e
201   have hd := partition_nodup (M.observe e) xs hn
202   have live (ys : List X) (hy : ys.Nodup) (o : Bool)
203       (he : ys.toFinset=M.update xs.toFinset e o) :
204       ∃ t, (child next ys).answer=some t := by
205     apply child_exists
206     by_cases hz : ys=[]
207     · exact Or.inl hz
208     · right
209       have hn' : (M.update xs.toFinset e o).Nonempty := by
210         rw [← he]
211         exact nonempty_support ys (by cases ys <;> simp_all)
212       obtain ⟨u,_,hu⟩ := (M.valid_child hv o).mp hn'
213       exact complete ys hy u (by simpa only [he] using hu)
214   obtain ⟨l,hl⟩ := live _ hd.1 false hp.1
215   obtain ⟨r,hr⟩ := live _ hd.2 true hp.2
216   refine ⟨.inr (e,fun o => if o then r else l),?_⟩
217   simp only [attempt,ha,ite_true,scanRun,fullScanner,PrefixScan.full,Nat.zero_add,hcap]
218   simp only [Run.bind,assemble,hl,hr,Run.pure]
219 
220 /-- Complete menus and a nonduplicated support connect absence to finite-depth impossibility. -/
221 theorem full_search_complete (M : Model X E Bool C Unit) (s : Scope M) (es : List E) (cs : List C)
222     (he : ∀ e, e ∈ es) (hc : ∀ c, c ∈ cs) (h : ℕ) (xs : List X) (hn : xs.Nodup)
223     (t : Tree E Bool C h) (hv : M.Valid h xs.toFinset t) :
224     ∃ u, (search fullScanner M es cs h xs).answer=some u := by
225   induction h generalizing xs with
226   | zero =>
227     have hn' : xs.isEmpty=false := by
228       have hh := M.valid_nonempty hv
229       cases xs <;> simp_all
230     cases hf : cs.find? (fun c => xs.all (fun x => M.accept x c)) with
231     | some c => exact ⟨c,by simp [search,hn',hf,Run.pure]⟩
232     | none =>
233       have hf' := (List.find?_eq_none.mp hf) t (hc t)
234       have hy : xs.all (fun x => M.accept x t)=true := by
235         exact List.all_eq_true.mpr (fun x hx => hv.2 x (List.mem_toFinset.mpr hx))
236       exact False.elim (hf' hy)
237   | succ h ih =>
238     have hn' : xs.isEmpty=false := by
239       have hh := M.valid_nonempty hv
240       cases xs <;> simp_all
241     cases hf : cs.find? (fun c => xs.all (fun x => M.accept x c)) with
242     | some c => exact ⟨.inl c,by simp [search,hn',hf,Run.pure]⟩
243     | none =>
244       cases t with
245       | inl c =>
246         have hf' := (List.find?_eq_none.mp hf) c (hc c)
247         have hy : xs.all (fun x => M.accept x c)=true := by
248           exact List.all_eq_true.mpr (fun x hx => hv.2 x (List.mem_toFinset.mpr hx))
249         exact False.elim (hf' hy)
250       | inr ek =>
251         obtain ⟨e,k⟩ := ek
252         obtain ⟨u,hu⟩ := attempt_complete M s h _ (fun ys hys v hv => ih ys hys v hv) xs hn e k hv
253         have hsome : ∃ v, (Run.first (attempt fullScanner M h (search fullScanner M es cs h) xs) es).answer=some v := by
254           cases hh : (Run.first (attempt fullScanner M h (search fullScanner M es cs h) xs) es).answer with
255           | some v => exact ⟨v,rfl⟩
256           | none =>
257             have hh' := (Run.first_none_iff _ es).mp hh e (he e)
258             rw [hu] at hh'
259             cases hh'
260         simpa [search,hn',hf] using hsome
261 
262 /-- The source's first-tree preservation comes with validity and complete finite failure. -/
263 theorem streaming_sound_complete (M : Model X E Bool C Unit) (s : Scope M)
264     (es : List E) (cs : List C) (he : ∀ e,e∈es) (hc : ∀ c,c∈cs)
265     (h : ℕ) (xs : List X) (hn : xs.Nodup) :
266     (∀ t, (search streamScanner M es cs h xs).answer=some t → M.Valid h xs.toFinset t) ∧
267     ((search streamScanner M es cs h xs).answer=none ↔
268       ¬ ∃ t : Tree E Bool C h, M.Valid h xs.toFinset t) := by
269   have hs : ∀ t, (search streamScanner M es cs h xs).answer=some t → M.Valid h xs.toFinset t := by
270     intro t ht
271     rw [same_returned_tree] at ht
272     exact full_search_sound M s es cs h xs t ht
273   refine ⟨hs,?_⟩
274   constructor
275   · intro hz hw
276     obtain ⟨t,ht⟩ := hw
277     obtain ⟨u,hu⟩ := full_search_complete M s es cs he hc h xs hn t ht
278     rw [same_returned_tree,hu] at hz
279     cases hz
280   · intro hnone
281     cases hr : (search streamScanner M es cs h xs).answer with
282     | none => rfl
283     | some t => exact False.elim (hnone ⟨t,hs t hr⟩)
284 
285 /-- Core 6.4: literal-result preservation, read dominance and actual finite-depth completeness. -/
286 theorem source_prefix_certificate (M : Model X E Bool C Unit) (s : Scope M)
287     (es : List E) (cs : List C) (he : ∀ e,e∈es) (hc : ∀ c,c∈cs)
288     (h : ℕ) (xs : List X) (hn : xs.Nodup) :
289     (search streamScanner M es cs h xs).answer=(search fullScanner M es cs h xs).answer ∧
290     (search streamScanner M es cs h xs).reads≤(search fullScanner M es cs h xs).reads ∧
291     ((search streamScanner M es cs h xs).answer=none ↔
292       ¬ ∃ t : Tree E Bool C h, M.Valid h xs.toFinset t) :=
293   ⟨same_returned_tree M es cs h xs,no_more_report_reads M es cs h xs,
294     (streaming_sound_complete M s es cs he hc h xs hn).2⟩
295 
296 end Komorebi.MachineTheory.OrderedCompiler

Back to source controls