TreeCompilerUpdates.lean

1 module
2 public import ExactTreeCompiler
3 import all ExactTreeCompiler
4 
5 /-!
6 Author: Komorebi P.
7 Paper VIII 9.11 and 9.12. Full-tree decision stability and an actual cached
8 ancestor-only update algorithm. The update receives cached sibling values,
9 not an oracle for the desired new optimum.
10 -/
11 public section
12 set_option autoImplicit false
13 namespace KomorebiPaperVIII.CandidateTree
14 open scoped BigOperators
15 variable {α R : Type*} [Field R] [LinearOrder R] [IsStrictOrderedRing R]
16 
17 /-- Scores perturbed by less than half their absolute gap keep the same order. -/
18 theorem half_gap_order (K S K' S' : R)
19     (hK : |K' - K| < |K - S| / 2) (hS : |S' - S| < |K - S| / 2) :
20     (K' ≤ S' ↔ K ≤ S) := by
21   by_cases h : K ≤ S
22   · rw [abs_of_nonpos (sub_nonpos.mpr h)] at hK hS
23     have hk := (abs_lt.mp hK).2
24     have hs := (abs_lt.mp hS).1
25     have h' : K' < S' := by linarith
26     exact iff_of_true (le_of_lt h') h
27   · have hslt : S < K := lt_of_not_ge h
28     rw [abs_of_pos (sub_pos.mpr hslt)] at hK hS
29     have hk := (abs_lt.mp hK).1
30     have hs := (abs_lt.mp hS).2
31     have h' : S' < K' := by linarith
32     exact iff_of_false (not_le_of_gt h') h
33 
34 /-- Bounds are imposed on the solved keep/split scores, at every internal node. -/
35 def GapControlled (keep overhead keep' overhead' : α → R) : CandidateTree α → Prop
36   | .leaf _ => True
37   | .node a _ ts =>
38     let oldSplit := overhead a + ∑ i, optimalValue keep overhead (ts i)
39     let newSplit := overhead' a + ∑ i, optimalValue keep' overhead' (ts i)
40     |keep' a - keep a| < |keep a - oldSplit| / 2 ∧
41     |newSplit - oldSplit| < |keep a - oldSplit| / 2 ∧
42     ∀ i, GapControlled keep overhead keep' overhead' (ts i)
43 
44 /-- Under the source's strict half-gap hypotheses the entire selected cut agrees. -/
45 theorem compiler_stability (keep overhead keep' overhead' : α → R)
46     (t : CandidateTree α) (hg : GapControlled keep overhead keep' overhead' t) :
47     compile keep' overhead' t = compile keep overhead t := by
48   induction t with
49   | leaf a => rfl
50   | node a n ts ih =>
51     rcases hg with ⟨hk, hs, hc⟩
52     have ho := half_gap_order _ _ _ _ hk hs
53     simp only [compile]
54     by_cases h : keep a ≤ overhead a + ∑ i, optimalValue keep overhead (ts i)
55     · rw [ite_eq_left h, ite_eq_left (ho.mpr h)]
56     · rw [ite_eq_right h, ite_eq_right (fun hp => h (ho.mp hp))]
57       congr 1
58       funext i
59       exact ih i (hc i)
60 
61 /-- A path to a changed subtree stores the untouched siblings and their cached values. -/
62 inductive CachedContext (α R : Type*) where
63   | hole
64   | frame (label : α) (arity : ℕ) (siblings : Fin (arity + 1) → CandidateTree α)
65       (slot : Fin (arity + 1)) (cache : Fin (arity + 1) → R) (outer : CachedContext α R)
66 
67 namespace CachedContext
68 
69 def fill : CachedContext α R → CandidateTree α → CandidateTree α
70   | .hole, t => t
71   | .frame a n siblings slot _ outer, t =>
72     fill outer (.node a n (Function.update siblings slot t))
73 
74 /-- Only the newly supplied subtree value and already cached siblings are read. -/
75 def updateValue (keep overhead : α → R) : CachedContext α R → R → R
76   | .hole, v => v
77   | .frame a _ _ slot cache outer, v =>
78     updateValue keep overhead outer
79       (min (keep a) (overhead a + ∑ i, if i = slot then v else cache i))
80 
81 def Valid (keep overhead : α → R) : CachedContext α R → Prop
82   | .hole => True
83   | .frame _ _ siblings slot cache outer =>
84     (∀ i, i ≠ slot → cache i = optimalValue keep overhead (siblings i)) ∧
85       Valid keep overhead outer
86 
87 /-- Building caches from the original model always supplies a valid context. -/
88 def refresh (keep overhead : α → R) : CachedContext α R → CachedContext α R
89   | .hole => .hole
90   | .frame a n siblings slot _ outer =>
91     .frame a n siblings slot (fun i => optimalValue keep overhead (siblings i))
92       (refresh keep overhead outer)
93 
94 omit [IsStrictOrderedRing R] in
95 theorem refresh_valid (keep overhead : α → R) (ctx : CachedContext α R) :
96     Valid keep overhead (refresh keep overhead ctx) := by
97   induction ctx with
98   | hole => trivial
99   | frame a n siblings slot cache outer ih => exact ⟨fun _ _ => rfl, ih⟩
100 
101 omit [IsStrictOrderedRing R] in
102 theorem refresh_fill (keep overhead : α → R) (ctx : CachedContext α R) (t : CandidateTree α) :
103     fill (refresh keep overhead ctx) t = fill ctx t := by
104   induction ctx generalizing t with
105   | hole => rfl
106   | frame a n siblings slot cache outer ih => exact ih _
107 
108 omit [IsStrictOrderedRing R] in
109 theorem updateValue_correct (keep overhead : α → R) (ctx : CachedContext α R)
110     (hv : Valid keep overhead ctx) (newTree : CandidateTree α) :
111     updateValue keep overhead ctx (optimalValue keep overhead newTree) =
112       optimalValue keep overhead (fill ctx newTree) := by
113   induction ctx generalizing newTree with
114   | hole => rfl
115   | frame a n siblings slot cache outer ih =>
116     rcases hv with ⟨hc, ho⟩
117     have he : (∑ i, if i = slot then optimalValue keep overhead newTree else cache i) =
118         ∑ i, optimalValue keep overhead (Function.update siblings slot newTree i) := by
119       apply Finset.sum_congr rfl
120       intro i _
121       by_cases hi : i = slot
122       · subst i; simp
123       · simp [hi, hc i hi]
124     simp only [updateValue, fill, he]
125     exact ih ho (.node a n (Function.update siblings slot newTree))
126 
127 omit [Field R] [LinearOrder R] [IsStrictOrderedRing R] in
128 theorem sibling_tree_unchanged (n : ℕ) (siblings : Fin (n + 1) → CandidateTree α)
129     (slot i : Fin (n + 1)) (t : CandidateTree α) (hi : i ≠ slot) :
130     Function.update siblings slot t i = siblings i := by
131   exact Function.update_of_ne hi t siblings
132 
133 omit [IsStrictOrderedRing R] in
134 theorem sibling_value_unchanged (keep overhead : α → R) (n : ℕ)
135     (siblings : Fin (n + 1) → CandidateTree α) (slot i : Fin (n + 1))
136     (t : CandidateTree α) (hi : i ≠ slot) :
137     optimalValue keep overhead (Function.update siblings slot t i) =
138       optimalValue keep overhead (siblings i) := by
139   rw [Function.update_of_ne hi]
140 
141 /-- The cached update is globally optimal against all cuts of the edited tree. -/
142 theorem local_recompilation (keep overhead : α → R) (ctx : CachedContext α R)
143     (hv : Valid keep overhead ctx) (newTree : CandidateTree α) :
144     (∀ c : Cut (fill ctx newTree),
145       updateValue keep overhead ctx (optimalValue keep overhead newTree) ≤
146         cutValue keep overhead c) ∧
147     ∃ c : Cut (fill ctx newTree), cutValue keep overhead c =
148       updateValue keep overhead ctx (optimalValue keep overhead newTree) := by
149   rw [updateValue_correct keep overhead ctx hv newTree]
150   exact exact_tree_compiler keep overhead (fill ctx newTree)
151 
152 end CachedContext
153 
154 /-- A strict Pareto point need not minimize any scalarized objective. -/
155 theorem unsupported_pareto_example (lam : ℚ) :
156     min (2 * lam) 2 < 3 / 2 + lam := by
157   by_cases h : lam ≤ 1
158   · exact (min_le_left _ _).trans_lt (by linarith)
159   · exact (min_le_right _ _).trans_lt (by linarith)
160 
161 end KomorebiPaperVIII.CandidateTree
162 
163 -- FINAL AXIOM AUDITS
164 #print axioms KomorebiPaperVIII.CandidateTree.half_gap_order
165 #print axioms KomorebiPaperVIII.CandidateTree.compiler_stability
166 #print axioms KomorebiPaperVIII.CandidateTree.CachedContext.refresh_valid
167 #print axioms KomorebiPaperVIII.CandidateTree.CachedContext.refresh_fill
168 #print axioms KomorebiPaperVIII.CandidateTree.CachedContext.updateValue_correct
169 #print axioms KomorebiPaperVIII.CandidateTree.CachedContext.sibling_tree_unchanged
170 #print axioms KomorebiPaperVIII.CandidateTree.CachedContext.sibling_value_unchanged
171 #print axioms KomorebiPaperVIII.CandidateTree.CachedContext.local_recompilation
172 #print axioms KomorebiPaperVIII.CandidateTree.unsupported_pareto_example
173 #print axioms KomorebiPaperVIII.CandidateTree.CachedContext.updateValue

Back to source controls