OrderedCompiler.lean

1 import MachineTheory.PrefixScan
2 import MachineTheory.BinaryDiagnosis
3 
4 /-!
5 # A concrete ordered depth-first compiler on the inherited controller type
6 
7 The full and streaming compilers have identical repair order, experiment order,
8 left-before-right recursion, permissions, horizons and empty-branch handling.
9 Only the root-table scan differs. Model acquisition, permission and terminal
10 checking, list allocation and capacity arithmetic are not free by convention:
11 the two counters here deliberately meter report reads and capacity tests only.
12 -/
13 namespace Komorebi.MachineTheory.OrderedCompiler
14 open HardInquiry
15 variable {X E C A B : Type}
16 
17 structure Run (A : Type) where
18   answer : Option A
19   reads : ℕ
20   checks : ℕ
21   deriving Repr, DecidableEq
22 
23 namespace Run
24 
25 def fail : Run A := ⟨none,0,0⟩
26 def pure (a : A) : Run A := ⟨some a,0,0⟩
27 
28 def bind (r : Run A) (f : A → Run B) : Run B :=
29   match r.answer with
30   | none => ⟨none,r.reads,r.checks⟩
31   | some a => let s := f a; ⟨s.answer,r.reads+s.reads,r.checks+s.checks⟩
32 
33 def map (f : A → B) (r : Run A) : Run B :=
34   ⟨r.answer.map f,r.reads,r.checks⟩
35 
36 /-- Same result and no more report-table reads; extra predicate work is separate. -/
37 def Refines (s t : Run A) : Prop := s.answer=t.answer ∧ s.reads≤t.reads
38 
39 theorem refines_refl (r : Run A) : Refines r r := ⟨rfl,le_rfl⟩
40 
41 theorem bind_refines (r s : Run A) (f g : A → Run B) (hr : Refines r s)
42     (hf : ∀ a, Refines (f a) (g a)) : Refines (bind r f) (bind s g) := by
43   rcases hr with ⟨he,hle⟩
44   cases ha : r.answer with
45   | none => simp only [bind,ha,← he,Refines]; exact ⟨trivial,hle⟩
46   | some a =>
47     simp only [bind,ha,← he,Refines]
48     exact ⟨(hf a).1,Nat.add_le_add hle (hf a).2⟩
49 
50 theorem map_refines (f : A → B) (r s : Run A) (h : Refines r s) :
51     Refines (map f r) (map f s) := by
52   exact ⟨congrArg (Option.map f) h.1,h.2⟩
53 
54 theorem bind_some_iff (r : Run A) (f : A → Run B) (b : B) :
55     (bind r f).answer=some b ↔ ∃ a, r.answer=some a ∧ (f a).answer=some b := by
56   cases he : r.answer <;> simp [bind,he]
57 
58 /-- Ordered backtracking retains the first successful result and charges failed attempts. -/
59 def first (f : A → Run B) : List A → Run B
60   | [] => fail
61   | a::as =>
62       let r := f a
63       match r.answer with
64       | some b => ⟨some b,r.reads,r.checks⟩
65       | none => let s := first f as; ⟨s.answer,r.reads+s.reads,r.checks+s.checks⟩
66 
67 theorem first_refines (f g : A → Run B) (h : ∀ a, Refines (f a) (g a)) (xs : List A) :
68     Refines (first f xs) (first g xs) := by
69   induction xs with
70   | nil => exact refines_refl _
71   | cons a xs ih =>
72     have he := (h a).1
73     cases ha : (f a).answer with
74     | none =>
75       simp only [first,ha,← he,Refines]
76       exact ⟨ih.1,Nat.add_le_add (h a).2 ih.2⟩
77     | some b =>
78       simp only [first,ha,← he,Refines]
79       exact ⟨trivial,(h a).2⟩
80 
81 theorem first_some_mem (f : A → Run B) (xs : List A) (b : B)
82     (hs : (first f xs).answer=some b) : ∃ a ∈ xs, (f a).answer=some b := by
83   induction xs with
84   | nil => cases hs
85   | cons a xs ih =>
86     cases he : (f a).answer with
87     | none =>
88       have ht : (first f xs).answer=some b := by simpa only [first,he] using hs
89       obtain ⟨c,hc,hv⟩ := ih ht
90       exact ⟨c,List.mem_cons_of_mem a hc,hv⟩
91     | some c =>
92       have hc : c=b := Option.some.inj (by simpa only [first,he] using hs)
93       exact ⟨a,List.mem_cons_self,by simpa only [hc] using he⟩
94 
95 theorem first_none_iff (f : A → Run B) (xs : List A) :
96     (first f xs).answer=none ↔ ∀ a ∈ xs, (f a).answer=none := by
97   induction xs with
98   | nil => simp [first,fail]
99   | cons a xs ih =>
100     cases he : (f a).answer with
101     | none => simp [first,he,ih]
102     | some b => simp [first,he]
103 
104 end Run
105 
106 abbrev Scanner (X : Type) := (X → Bool) → ℕ → List X → PrefixScan.Result X
107 
108 def fullScanner : Scanner X := fun f C xs => PrefixScan.full f C 0 0 xs
109 def streamScanner : Scanner X := fun f C xs => PrefixScan.stream f C 0 0 xs
110 
111 def scanRun (scan : Scanner X) (f : X → Bool) (C : ℕ) (xs : List X) : Run (List X × List X) :=
112   let r := scan f C xs
113   ⟨r.branches,r.reads,r.checks⟩
114 
115 theorem scan_refines (f : X → Bool) (C : ℕ) (xs : List X) :
116     Run.Refines (scanRun streamScanner f C xs) (scanRun fullScanner f C xs) :=
117   ⟨PrefixScan.stream_branches f C 0 0 xs,PrefixScan.stream_reads_le f C 0 0 xs⟩
118 
119 def stop : (h : ℕ) → C → Tree E Bool C h
120   | 0,c => c
121   | _+1,c => .inl c
122 
123 /-- `some none` is an impossible branch; outer `none` means live-branch failure. -/
124 def child (next : List X → Run A) (xs : List X) : Run (Option A) :=
125   if xs.isEmpty then Run.pure none else (next xs).map some
126 
127 def assemble (h : ℕ) (e : E) (next : List X → Run (Tree E Bool C h))
128     (p : List X × List X) : Run (Tree E Bool C (h+1)) :=
129   (child next p.1).bind fun l => (child next p.2).bind fun r =>
130     Run.pure (.inr (e,fun o => if o then r else l))
131 
132 def attempt (scan : Scanner X) (M : Model X E Bool C Unit) (h : ℕ)
133     (next : List X → Run (Tree E Bool C h)) (xs : List X) (e : E) : Run (Tree E Bool C (h+1)) :=
134   if xs.all (M.permitted e) then
135     (scanRun scan (M.observe e) (2^h) xs).bind (assemble h e next)
136   else Run.fail
137 
138 /-- The primitive program, not a relation assuming its returned tree is correct. -/
139 def search (scan : Scanner X) (M : Model X E Bool C Unit) (experiments : List E)
140     (repairs : List C) : (h : ℕ) → List X → Run (Tree E Bool C h)
141   | 0,xs =>
142       if xs.isEmpty then Run.fail else
143         match repairs.find? (fun c => xs.all (fun x => M.accept x c)) with
144         | some c => Run.pure c
145         | none => Run.fail
146   | h+1,xs =>
147       if xs.isEmpty then Run.fail else
148         match repairs.find? (fun c => xs.all (fun x => M.accept x c)) with
149         | some c => Run.pure (.inl c)
150         | none => Run.first (attempt scan M h (search scan M experiments repairs h) xs) experiments
151 
152 theorem child_refines (f g : List X → Run A) (h : ∀ xs, Run.Refines (f xs) (g xs)) (xs : List X) :
153     Run.Refines (child f xs) (child g xs) := by
154   by_cases he : xs.isEmpty
155   · simp only [child,he,ite_true]; exact Run.refines_refl _
156   · simp only [child,he]; exact Run.map_refines _ _ _ (h xs)
157 
158 theorem assemble_refines (h : ℕ) (e : E) (f g : List X → Run (Tree E Bool C h))
159     (hf : ∀ xs, Run.Refines (f xs) (g xs)) (p : List X × List X) :
160     Run.Refines (assemble h e f p) (assemble h e g p) := by
161   apply Run.bind_refines _ _ _ _ (child_refines f g hf p.1)
162   intro l
163   apply Run.bind_refines _ _ _ _ (child_refines f g hf p.2)
164   intro r
165   exact Run.refines_refl _
166 
167 /-- Equality includes the literal ordered tree, with no relabeling of equal optima. -/
168 theorem streaming_preserves_search (M : Model X E Bool C Unit) (experiments : List E)
169     (repairs : List C) (h : ℕ) (xs : List X) :
170     Run.Refines (search streamScanner M experiments repairs h xs)
171       (search fullScanner M experiments repairs h xs) := by
172   induction h generalizing xs with
173   | zero => exact Run.refines_refl _
174   | succ h ih =>
175     by_cases he : xs.isEmpty
176     · simp only [search,he,ite_true]; exact Run.refines_refl _
177     · simp only [search,he]
178       cases hr : repairs.find? (fun c => xs.all (fun x => M.accept x c)) with
179       | some c => exact Run.refines_refl _
180       | none =>
181         apply Run.first_refines
182         intro e
183         by_cases hp : xs.all (M.permitted e)
184         · simp only [attempt,hp,ite_true]
185           exact Run.bind_refines _ _ _ _ (scan_refines _ _ _)
186             (assemble_refines h e _ _ ih)
187         · simp only [attempt,hp]; exact Run.refines_refl _
188 
189 /-- Backtracking and finite-depth failure are identical, including arbitrary changed row orders. -/
190 theorem same_returned_tree (M : Model X E Bool C Unit) (es : List E) (cs : List C)
191     (h : ℕ) (xs : List X) :
192     (search streamScanner M es cs h xs).answer = (search fullScanner M es cs h xs).answer :=
193   (streaming_preserves_search M es cs h xs).1
194 
195 theorem no_more_report_reads (M : Model X E Bool C Unit) (es : List E) (cs : List C)
196     (h : ℕ) (xs : List X) :
197     (search streamScanner M es cs h xs).reads ≤ (search fullScanner M es cs h xs).reads :=
198   (streaming_preserves_search M es cs h xs).2
199 
200 /-- The same fallback is invoked on the same completed failure, never on a timeout. -/
201 def withFallback (r : Run A) (fallback : Run A) : Run A :=
202   match r.answer with
203   | some _ => r
204   | none => ⟨fallback.answer,r.reads+fallback.reads,r.checks+fallback.checks⟩
205 
206 theorem same_fallback (M : Model X E Bool C Unit) (es : List E) (cs : List C)
207     (h : ℕ) (xs : List X) (fallback : Run (Tree E Bool C h)) :
208     (withFallback (search streamScanner M es cs h xs) fallback).answer =
209       (withFallback (search fullScanner M es cs h xs) fallback).answer := by
210   have he := same_returned_tree M es cs h xs
211   cases hr : (search fullScanner M es cs h xs).answer <;> simp [withFallback,he,hr]
212 
213 end Komorebi.MachineTheory.OrderedCompiler

Back to source controls