StoredBudgetCompiler.lean

1 module
2 public import QuantizedTreeCompiler
3 import all QuantizedTreeCompiler
4 import all ExactTreeCompiler
5 import all BudgetConvolution
6 public import DiscretePrecision
7 import all DiscretePrecision
8 public import Init.Data.Fin.Lemmas
9 public import Init.Data.Vector.OfFn
10 public import Mathlib.Data.Fintype.Sigma
11 public import Mathlib.Data.Fintype.BigOperators
12 
13 /-!
14 Author: Komorebi P.
15 Paper VIII 9.9 and executable refinements of 9.8 and 8.7.
16 Tables are real array-backed Vectors: every child table is computed once and
17 convolutions read cached entries. This is not the exponentially recomputing
18 functional recurrence used to state the specification.
19 Work counts use unit-cost table cells and min-plus candidate trials, excluding
20 arbitrary-precision bit complexity and hardware timing.
21 -/
22 public section
23 set_option autoImplicit false
24 set_option backward.isDefEq.respectTransparency false
25 set_option backward.isDefEq.respectTransparency.types false
26 set_option maxRecDepth 2048
27 namespace KomorebiPaperVIII
28 open scoped BigOperators
29 namespace BudgetDP
30 variable {R : Type*} [Field R] [LinearOrder R] [IsStrictOrderedRing R]
31 
32 abbrev StoredTable (R : Type*) (B : ℕ) := Vector (Option R) (B + 1)
33 
34 theorem vector_get_ofFn {T : Type*} {n : ℕ} (f : Fin n → T) (i : Fin n) :
35     (Vector.ofFn f).get i = f i := by
36   simp only [Vector.get, Vector.toArray_ofFn, Fin.val_cast, Array.getElem_ofFn, Fin.eta]
37 
38 def tabulate (B : ℕ) (F : ℕ → Option R) : StoredTable R B :=
39   Vector.ofFn (fun b => F b.val)
40 
41 def lookup {B : ℕ} (T : StoredTable R B) (b : ℕ) : Option R :=
42   if h : b ≤ B then T.get ⟨b, Nat.lt_succ_of_le h⟩ else none
43 
44 omit [Field R] [LinearOrder R] [IsStrictOrderedRing R] in
45 theorem lookup_tabulate (B : ℕ) (F : ℕ → Option R) (b : ℕ) (hb : b ≤ B) :
46     lookup (tabulate B F) b = F b := by
47   simp only [lookup, hb, ↓reduceDIte, tabulate, vector_get_ofFn]
48 
49 omit [Field R] [IsStrictOrderedRing R] in
50 theorem bestOver_congr {ι : Type*} (xs : List ι) (F G : ι → Option R)
51     (h : ∀ i ∈ xs, F i = G i) : bestOver F xs = bestOver G xs := by
52   induction xs with
53   | nil => rfl
54   | cons i xs ih =>
55     simp only [bestOver]
56     rw [h i (by simp), ih (fun j hj => h j (by simp [hj]))]
57 
58 /- Only entries at most the requested output weight can affect a convolution. -/
59 omit [IsStrictOrderedRing R] in
60 theorem convolution_congr_local (F G F' G' : ℕ → Option R) (b : ℕ)
61     (hF : ∀ k ≤ b, F k = F' k) (hG : ∀ k ≤ b, G k = G' k) :
62     convolution F G b = convolution F' G' b := by
63   apply bestOver_congr
64   intro k hk
65   have hkb : k ≤ b := Nat.lt_succ_iff.mp (List.mem_range.mp hk)
66   rw [hF k hkb, hG (b - k) (Nat.sub_le _ _)]
67 
68 omit [IsStrictOrderedRing R] in
69 theorem combine_congr_local {n : ℕ} (F G : Fin n → ℕ → Option R) (b : ℕ)
70     (h : ∀ i k, k ≤ b → F i k = G i k) : combine F b = combine G b := by
71   induction n generalizing b with
72   | zero => rfl
73   | succ n ih =>
74     apply convolution_congr_local
75     · exact h 0
76     · intro k hk
77       exact ih (fun i => F i.succ) (fun i => G i.succ) k
78         (fun i l hl => h i.succ l (hl.trans hk))
79 
80 /- Every entry is computed once from two already stored tables. -/
81 def mergeStored {B : ℕ} (F G : StoredTable R B) : StoredTable R B :=
82   tabulate B (convolution (lookup F) (lookup G))
83 
84 /- A linear number of table merges combines arbitrary finite branching. -/
85 def combineStored {B : ℕ} : {n : ℕ} → (Fin n → StoredTable R B) → StoredTable R B
86   | 0, _ => tabulate B (singletonTable 0 0)
87   | n + 1, F =>
88     let tail := combineStored (fun i : Fin n => F i.succ)
89     mergeStored (F 0) tail
90 
91 omit [IsStrictOrderedRing R] in
92 theorem combineStored_correct {B n : ℕ} (F : Fin n → StoredTable R B)
93     (b : ℕ) (hb : b ≤ B) :
94     lookup (combineStored F) b = combine (fun i => lookup (F i)) b := by
95   induction n generalizing b with
96   | zero => exact lookup_tabulate B _ b hb
97   | succ n ih =>
98     change lookup (mergeStored (F 0) (combineStored (fun i : Fin n => F i.succ))) b = _
99     rw [mergeStored, lookup_tabulate _ _ _ hb]
100     apply convolution_congr_local _ _ _ _ b (fun _ _ => rfl)
101     intro k hk
102     exact ih (fun i => F i.succ) k (hk.trans hb)
103 end BudgetDP
104 
105 namespace CandidateTree
106 variable {α R : Type*} [Field R] [LinearOrder R] [IsStrictOrderedRing R]
107 
108 /- Bottom-up tabulation. Child arrays are eagerly cached before merging. -/
109 def storedTree (B : ℕ) (κ : α → R) (w : α → ℕ) (σ : α → R) :
110     CandidateTree α → BudgetDP.StoredTable R B
111   | .leaf a => BudgetDP.tabulate B (BudgetDP.singletonTable (w a) (κ a))
112   | .node a n ts =>
113     let cached := Vector.ofFn (fun i => storedTree B κ w σ (ts i))
114     let merged := BudgetDP.combineStored (fun i : Fin (n + 1) => cached.get i)
115     BudgetDP.tabulate B (fun b => BudgetDP.choose (BudgetDP.singletonTable (w a) (κ a) b)
116       (BudgetDP.add (some (σ a)) (BudgetDP.lookup merged b)))
117 
118 /- The implemented cached array agrees entrywise with the proved exact recurrence. -/
119 omit [IsStrictOrderedRing R] in
120 theorem storedTree_correct (B : ℕ) (κ : α → R) (w : α → ℕ) (σ : α → R)
121     (t : CandidateTree α) (b : ℕ) (hb : b ≤ B) :
122     BudgetDP.lookup (storedTree B κ w σ t) b = budgetTable κ w σ t b := by
123   induction t generalizing b with
124   | leaf a => exact BudgetDP.lookup_tabulate B _ b hb
125   | node a n ts ih =>
126     simp only [storedTree, budgetTable, BudgetDP.lookup_tabulate _ _ _ hb]
127     congr 2
128     rw [BudgetDP.combineStored_correct _ b hb]
129     apply BudgetDP.combine_congr_local
130     intro i k hk
131     simpa only [BudgetDP.vector_get_ofFn] using ih i k (hk.trans hb)
132 
133 /- The executable tabulated compiler scans its stored root table. -/
134 def storedBudget (B : ℕ) (κ : α → R) (w : α → ℕ) (σ : α → R)
135     (t : CandidateTree α) : Option R :=
136   let rootTable := storedTree B κ w σ t
137   BudgetDP.withinBudget (BudgetDP.lookup rootTable) B
138 
139 omit [IsStrictOrderedRing R] in
140 theorem storedBudget_correct (B : ℕ) (κ : α → R) (w : α → ℕ) (σ : α → R)
141     (t : CandidateTree α) : storedBudget B κ w σ t = compileBudget κ w σ t B := by
142   apply BudgetDP.bestOver_congr
143   intro b hb
144   exact storedTree_correct B κ w σ t b (Nat.lt_succ_iff.mp (List.mem_range.mp hb))
145 
146 /- Optimality and attainment apply to the actual array-backed implementation. -/
147 theorem storedBudget_minimum (B : ℕ) (κ : α → R) (w : α → ℕ) (σ : α → R)
148     (t : CandidateTree α) :
149     BudgetDP.IsMinimum (storedBudget B κ w σ t)
150       (fun z => ∃ c : Cut t, cutWeight w c ≤ B ∧ cutValue κ σ c = z) := by
151   rw [storedBudget_correct]
152   exact quantized_budget_compiler κ w σ t B
153 end CandidateTree
154 
155 namespace BudgetDP
156 variable {R : Type*} [Field R] [LinearOrder R] [IsStrictOrderedRing R]
157 
158 /- Discrete precision tabulation caches the preceding edge table once. -/
159 def storedDiscrete (B : ℕ) : List (List (ℕ × R)) → StoredTable R B
160   | [] => tabulate B (singletonTable 0 0)
161   | opts :: edges =>
162     let prior := storedDiscrete B edges
163     tabulate B (fun b => bestOver (fun o => if o.1 ≤ b then
164       add (lookup prior (b - o.1)) (some o.2) else none) opts)
165 
166 omit [IsStrictOrderedRing R] in
167 theorem storedDiscrete_correct (B : ℕ) (edges : List (List (ℕ × R)))
168     (b : ℕ) (hb : b ≤ B) : lookup (storedDiscrete B edges) b = discreteTable edges b := by
169   induction edges generalizing b with
170   | nil => exact lookup_tabulate B _ b hb
171   | cons opts edges ih =>
172     simp only [storedDiscrete, discreteTable, lookup_tabulate _ _ _ hb]
173     apply bestOver_congr
174     intro o _
175     by_cases ho : o.1 ≤ b
176     · simp only [ho, ↓reduceIte]
177       rw [ih (b - o.1) ((Nat.sub_le _ _).trans hb)]
178     · simp only [ho, ↓reduceIte]
179 
180 /- Cached implementation of the discrete precision optimizer. -/
181 def storedDiscreteBudget (B : ℕ) (edges : List (List (ℕ × R))) : Option R :=
182   let finalTable := storedDiscrete B edges
183   withinBudget (lookup finalTable) B
184 
185 omit [IsStrictOrderedRing R] in
186 theorem storedDiscreteBudget_correct (B : ℕ) (edges : List (List (ℕ × R))) :
187     storedDiscreteBudget B edges = discreteBudget edges B := by
188   apply bestOver_congr
189   intro b hb
190   exact storedDiscrete_correct B edges b (Nat.lt_succ_iff.mp (List.mem_range.mp hb))
191 end BudgetDP
192 
193 namespace CandidateTree
194 variable {α : Type*}
195 
196 /- Number of nodes in the independently supplied candidate tree. -/
197 def nodeCount : CandidateTree α → ℕ
198   | .leaf _ => 1
199   | .node _ _ ts => 1 + ∑ i, nodeCount (ts i)
200 
201 /- Number of child-table merges actually used by the tabulator. -/
202 def mergeCount : CandidateTree α → ℕ
203   | .leaf _ => 0
204   | .node _ n ts => n + 1 + ∑ i, mergeCount (ts i)
205 
206 /- A nonempty finite tree has one fewer child edges than nodes. -/
207 theorem mergeCount_add_one (t : CandidateTree α) : mergeCount t + 1 = nodeCount t := by
208   induction t with
209   | leaf => rfl
210   | node a n ts ih =>
211     simp only [mergeCount, nodeCount]
212     have h : (∑ i, mergeCount (ts i)) + (n + 1) = ∑ i, nodeCount (ts i) := by
213       simpa only [Finset.sum_add_distrib, Finset.sum_const, Finset.card_univ,
214         Fintype.card_fin, smul_eq_mul, mul_one] using
215           (Finset.sum_congr rfl (fun i (_ : i ∈ Finset.univ) => ih i))
216     omega
217 
218 /- Concrete indices of the candidate trials in one complete convolution table. -/
219 abbrev MergeTrial (B : ℕ) := (b : Fin (B + 1)) × Fin (b.val + 1)
220 
221 
222 theorem merge_trial_count (B : ℕ) :
223     Fintype.card (MergeTrial B) = ∑ b ∈ Finset.range (B + 1), (b + 1) := by
224   simp [MergeTrial, Fintype.card_sigma, ← Fin.sum_univ_eq_sum_range]
225 
226 theorem merge_trial_bound (B : ℕ) : Fintype.card (MergeTrial B) ≤ (B + 1) ^ 2 := by
227   rw [merge_trial_count]
228   calc
229     _ ≤ ∑ _b ∈ Finset.range (B + 1), (B + 1) :=
230       Finset.sum_le_sum (fun b hb => by have := Finset.mem_range.mp hb; omega)
231     _ = _ := by simp [pow_two]
232 
233 /- Unit-cost model: table-cell construction plus each tested min-plus candidate.
234 The empty combination table costs B+1 cells at every internal node as well. -/
235 def tabulationWork (B : ℕ) : CandidateTree α → ℕ
236   | .leaf _ => B + 1
237   | .node _ n ts =>
238     2 * (B + 1) + (n + 1) * (B + 1 + Fintype.card (MergeTrial B)) +
239       ∑ i, tabulationWork B (ts i)
240 
241 /- Corollary 9.9: an explicit O(nodes * (B+1)^2) bound in the declared model. -/
242 theorem tabulation_work_bound (B : ℕ) (t : CandidateTree α) :
243     tabulationWork B t ≤
244       2 * (B + 1) * nodeCount t +
245         ((B + 1) + (B + 1)^2) * mergeCount t := by
246   induction t with
247   | leaf => simp [tabulationWork, nodeCount, mergeCount]
248   | node a n ts ih =>
249     simp only [tabulationWork, nodeCount, mergeCount]
250     have hs := Finset.sum_le_sum (fun i (_ : i ∈ Finset.univ) => ih i)
251     have hm := Nat.mul_le_mul_left (n + 1) (merge_trial_bound B)
252     simp only [Finset.sum_add_distrib, ← Finset.mul_sum] at hs
253     nlinarith
254 
255 /- The bound is polynomial in numeric budget, not in its binary input length. -/
256 theorem tabulation_pseudopolynomial (B : ℕ) (t : CandidateTree α) :
257     tabulationWork B t ≤ nodeCount t * (3 * (B + 1) + (B + 1)^2) := by
258   have h := tabulation_work_bound B t
259   have hm := mergeCount_add_one t
260   nlinarith
261 end CandidateTree
262 end KomorebiPaperVIII
263 
264 #print axioms KomorebiPaperVIII.BudgetDP.vector_get_ofFn
265 #print axioms KomorebiPaperVIII.BudgetDP.lookup_tabulate
266 #print axioms KomorebiPaperVIII.BudgetDP.bestOver_congr
267 #print axioms KomorebiPaperVIII.BudgetDP.convolution_congr_local
268 #print axioms KomorebiPaperVIII.BudgetDP.combine_congr_local
269 #print axioms KomorebiPaperVIII.BudgetDP.combineStored_correct
270 #print axioms KomorebiPaperVIII.CandidateTree.storedTree_correct
271 #print axioms KomorebiPaperVIII.CandidateTree.storedBudget_correct
272 #print axioms KomorebiPaperVIII.CandidateTree.storedBudget_minimum
273 #print axioms KomorebiPaperVIII.BudgetDP.storedDiscrete_correct
274 #print axioms KomorebiPaperVIII.BudgetDP.storedDiscreteBudget_correct
275 #print axioms KomorebiPaperVIII.CandidateTree.mergeCount_add_one
276 #print axioms KomorebiPaperVIII.CandidateTree.merge_trial_count
277 #print axioms KomorebiPaperVIII.CandidateTree.merge_trial_bound
278 #print axioms KomorebiPaperVIII.CandidateTree.tabulation_work_bound
279 #print axioms KomorebiPaperVIII.CandidateTree.tabulation_pseudopolynomial
280 #print axioms KomorebiPaperVIII.CandidateTree.storedTree
281 #print axioms KomorebiPaperVIII.BudgetDP.storedDiscrete

Back to source controls