Planning.lean

1 import MachineTheory.Feedback
2 import Mathlib.Data.Finset.Max
3 
4 /-!
5 Reviewed Core 0.2, Theorem 5.4: finite-horizon inquiry on observable information states.
6 Menus are finite and depend on the retained state; terminal menus are nonempty.
7 A successor is requested only with a proof that its report has positive probability.
8 An observation tree chooses actions using reports, never the hidden physical state.
9 -/
10 namespace Komorebi.MachineTheory
11 namespace Planning
12 open scoped BigOperators
13 noncomputable section
14 
15 /-- Finite minimum, with nonemptiness retained as a premise rather than a default value. -/
16 def finiteMin {I : Type*} (s : Finset I) (hs : s.Nonempty) (f : I → ℝ) : ℝ := by
17   classical
18   exact (s.image f).min' (hs.image f)
19 
20 theorem finiteMin_le {I : Type*} (s : Finset I) (hs : s.Nonempty) (f : I → ℝ)
21     (i : I) (hi : i ∈ s) : finiteMin s hs f ≤ f i := by
22   classical
23   exact Finset.min'_le _ _ (Finset.mem_image.mpr ⟨i, hi, rfl⟩)
24 
25 theorem finiteMin_attained {I : Type*} (s : Finset I) (hs : s.Nonempty) (f : I → ℝ) :
26     ∃ i ∈ s, f i = finiteMin s hs f := by
27   classical
28   exact Finset.mem_image.mp (Finset.min'_mem _ (hs.image f))
29 
30 theorem le_finiteMin {I : Type*} (s : Finset I) (hs : s.Nonempty) (f : I → ℝ)
31     (v : ℝ) (hv : ∀ i ∈ s, v ≤ f i) : v ≤ finiteMin s hs f := by
32   obtain ⟨i, hi, he⟩ := finiteMin_attained s hs f
33   rw [← he]
34   exact hv i hi
35 
36 theorem finiteMin_congr {I : Type*} (s t : Finset I) (hs : s.Nonempty) (ht : t.Nonempty)
37     (f g : I → ℝ) (hst : s = t) (hfg : ∀ i ∈ s, f i = g i) :
38     finiteMin s hs f = finiteMin t ht g := by
39   subst t
40   apply le_antisymm
41   · apply le_finiteMin
42     intro i hi
43     rw [← hfg i hi]
44     exact finiteMin_le s hs f i hi
45   · apply le_finiteMin
46     intro i hi
47     rw [hfg i hi]
48     exact finiteMin_le s ht g i hi
49 
50 /-- S is the information available to planning, not an unobserved physical state. -/
51 structure Model (S A O D : Type*) [Fintype O] where
52   actions : S → Finset A
53   decisions : S → Finset D
54   decisions_nonempty : ∀ s, (decisions s).Nonempty
55   cost : S → A → ℝ
56   cost_nonnegative : ∀ s a, 0 ≤ cost s a
57   loss : S → D → ℝ
58   prob : S → A → O → ℝ
59   nonnegative : ∀ s a o, 0 ≤ prob s a o
60   normalized : ∀ s a, ∑ o, prob s a o = 1
61   next : (s : S) → (a : A) → (o : O) → 0 < prob s a o → S
62 
63 /-- Syntax of finite report-dependent plans. No hidden-state argument is available to a node. -/
64 inductive Tree (A O D : Type*) where
65   | stop : D → Tree A O D
66   | experiment : A → (O → Tree A O D) → Tree A O D
67 
68 /-- A syntactic height bound also covers dormant, impossible-report branches. -/
69 def Tree.Bounded {A O D : Type*} : Nat → Tree A O D → Prop
70   | _, .stop _ => True
71   | 0, .experiment _ _ => False
72   | h + 1, .experiment _ k => ∀ o, Tree.Bounded h (k o)
73 
74 variable {S A O D : Type*} [Fintype O]
75 
76 /-- Expected charge plus terminal loss. A zero-mass report contributes zero and has no successor. -/
77 def evaluate (M : Model S A O D) : Tree A O D → S → ℝ
78   | .stop d, s => M.loss s d
79   | .experiment a k, s => M.cost s a + ∑ o,
80       if ho : 0 < M.prob s a o then
81         M.prob s a o * evaluate M (k o) (M.next s a o ho) else 0
82 
83 /-- Admissibility is imposed at every reachable information state, including terminal choices. -/
84 def Feasible (M : Model S A O D) : Nat → S → Tree A O D → Prop
85   | _, s, .stop d => d ∈ M.decisions s
86   | 0, _, .experiment _ _ => False
87   | h + 1, s, .experiment a k => a ∈ M.actions s ∧
88       ∀ o (ho : 0 < M.prob s a o), Feasible M h (M.next s a o ho) (k o)
89 
90 /-- The same first-choice type names both stopping and experiments. -/
91 def menu (M : Model S A O D) (s : S) : Finset (D ⊕ A) := by
92   classical
93   exact (M.decisions s).image Sum.inl ∪ (M.actions s).image Sum.inr
94 
95 theorem menu_nonempty (M : Model S A O D) (s : S) : (menu M s).Nonempty := by
96   classical
97   obtain ⟨d, hd⟩ := M.decisions_nonempty s
98   exact ⟨Sum.inl d, by simp [menu, hd]⟩
99 
100 @[simp] theorem stop_mem_menu (M : Model S A O D) (s : S) (d : D) :
101     Sum.inl d ∈ menu M s ↔ d ∈ M.decisions s := by
102   classical
103   simp [menu]
104 
105 @[simp] theorem experiment_mem_menu (M : Model S A O D) (s : S) (a : A) :
106     Sum.inr a ∈ menu M s ↔ a ∈ M.actions s := by
107   classical
108   simp [menu]
109 
110 /-- One backup of a supplied continuation function. -/
111 def backup (M : Model S A O D) (V : S → ℝ) (s : S) (a : A) : ℝ :=
112   M.cost s a + ∑ o, if ho : 0 < M.prob s a o then
113     M.prob s a o * V (M.next s a o ho) else 0
114 
115 /-- Finite Bellman recursion: no experiment is available at horizon zero. -/
116 def value (M : Model S A O D) : Nat → S → ℝ
117   | 0, s => finiteMin (M.decisions s) (M.decisions_nonempty s) (M.loss s)
118   | h + 1, s => finiteMin (menu M s) (menu_nonempty M s)
119       (fun c => match c with
120         | Sum.inl d => M.loss s d
121         | Sum.inr a => backup M (value M h) s a)
122 
123 /-- Stop and experiment values at a positive horizon, with the same continuation value. -/
124 def firstValue (M : Model S A O D) (h : Nat) (s : S) : D ⊕ A → ℝ
125   | Sum.inl d => M.loss s d
126   | Sum.inr a => backup M (value M h) s a
127 
128 theorem value_le_stop (M : Model S A O D) (h : Nat) (s : S) (d : D)
129     (hd : d ∈ M.decisions s) : value M h s ≤ M.loss s d := by
130   cases h with
131   | zero => exact finiteMin_le _ _ _ d hd
132   | succ h => exact finiteMin_le _ _ _ (Sum.inl d) ((stop_mem_menu M s d).mpr hd)
133 
134 theorem value_le_experiment (M : Model S A O D) (h : Nat) (s : S) (a : A)
135     (ha : a ∈ M.actions s) : value M (h + 1) s ≤ backup M (value M h) s a :=
136   finiteMin_le _ _ _ (Sum.inr a) ((experiment_mem_menu M s a).mpr ha)
137 
138 /-- Bellman's number is a lower bound on the cost of every admissible report-dependent tree. -/
139 theorem value_le_tree (M : Model S A O D) (h : Nat) (s : S) (P : Tree A O D)
140     (hP : Feasible M h s P) : value M h s ≤ evaluate M P s := by
141   induction h generalizing s P with
142   | zero =>
143       cases P with
144       | stop d => exact value_le_stop M 0 s d hP
145       | experiment a k => exact False.elim hP
146   | succ h ih =>
147       cases P with
148       | stop d => exact value_le_stop M (h + 1) s d hP
149       | experiment a k =>
150           apply le_trans (value_le_experiment M h s a hP.1)
151           simp only [backup, evaluate]
152           apply add_le_add le_rfl
153           apply Finset.sum_le_sum
154           intro o _
155           split_ifs with ho
156           · exact mul_le_mul_of_nonneg_left (ih (M.next s a o ho) (k o) (hP.2 o ho))
157               (M.nonnegative s a o)
158           · exact le_rfl
159 
160 /-- A minimizing tree exists; the proof builds each child from the same actual first choice. -/
161 theorem minimizing_tree_exists (M : Model S A O D) (h : Nat) (s : S) :
162     ∃ P : Tree A O D, P.Bounded h ∧ Feasible M h s P ∧ evaluate M P s = value M h s := by
163   classical
164   induction h generalizing s with
165   | zero =>
166       obtain ⟨d, hd, he⟩ := finiteMin_attained (M.decisions s) (M.decisions_nonempty s) (M.loss s)
167       exact ⟨.stop d, trivial, hd, he⟩
168   | succ h ih =>
169       obtain ⟨c, hc, he⟩ := finiteMin_attained (menu M s) (menu_nonempty M s) (firstValue M h s)
170       cases c with
171       | inl d =>
172           exact ⟨.stop d, trivial, (stop_mem_menu M s d).mp hc, he⟩
173       | inr a =>
174           let child : O → Tree A O D := fun o =>
175             if ho : 0 < M.prob s a o then (ih (M.next s a o ho)).choose
176             else .stop (M.decisions_nonempty s).choose
177           refine ⟨.experiment a child, ?_, ?_, ?_⟩
178           · intro o
179             dsimp [child]
180             split_ifs with ho
181             · exact (ih (M.next s a o ho)).choose_spec.1
182             · simp only [Tree.Bounded]
183           · refine ⟨(experiment_mem_menu M s a).mp hc, ?_⟩
184             intro o ho
185             dsimp [child]
186             rw [dite_eq_left ho]
187             exact (ih (M.next s a o ho)).choose_spec.2.1
188           · change M.cost s a + _ = value M (h+1) s
189             calc
190               M.cost s a + _ = backup M (value M h) s a := by
191                 unfold backup
192                 congr 1
193                 apply Finset.sum_congr rfl
194                 intro o _
195                 split_ifs with ho
196                 · congr 1
197                   dsimp [child]
198                   rw [dite_eq_left ho]
199                   exact (ih (M.next s a o ho)).choose_spec.2.2
200                 · rfl
201               _ = value M (h+1) s := he
202 
203 /-- The Bellman value is characterized by actual finite trees, not defined as an unproved infimum. -/
204 theorem optimal_value_characterization (M : Model S A O D) (h : Nat) (s : S) :
205     (∃ P, P.Bounded h ∧ Feasible M h s P ∧ evaluate M P s = value M h s) ∧
206       (∀ P, Feasible M h s P → value M h s ≤ evaluate M P s) :=
207   ⟨minimizing_tree_exists M h s, fun P hp => value_le_tree M h s P hp⟩
208 
209 /-- Immediate terminal optimality is meaningful at every horizon, including zero. -/
210 def OptimalStop (M : Model S A O D) (h : Nat) (s : S) (d : D) : Prop :=
211   d ∈ M.decisions s ∧ M.loss s d = value M h s
212 
213 /-- An optimal first choice, including a specified terminal decision. -/
214 def OptimalFirst (M : Model S A O D) (h : Nat) (s : S) (c : D ⊕ A) : Prop :=
215   c ∈ menu M s ∧ firstValue M h s c = value M (h + 1) s
216 
217 theorem optimal_first_exists (M : Model S A O D) (h : Nat) (s : S) :
218     ∃ c, OptimalFirst M h s c :=
219   finiteMin_attained (menu M s) (menu_nonempty M s) (firstValue M h s)
220 
221 /-- A finite randomized mixture of valid trees cannot beat their common Bellman lower bound. -/
222 theorem randomized_tree_lower_bound (M : Model S A O D) (h : Nat) (s : S)
223     {I : Type*} [Fintype I] (w : I → ℝ) (hw : ∀ i, 0 ≤ w i) (hsum : ∑ i, w i = 1)
224     (P : I → Tree A O D) (hP : ∀ i, Feasible M h s (P i)) :
225     value M h s ≤ ∑ i, w i * evaluate M (P i) s := by
226   calc
227     value M h s = (∑ i, w i) * value M h s := by rw [hsum, one_mul]
228     _ = ∑ i, w i * value M h s := by rw [Finset.sum_mul]
229     _ ≤ ∑ i, w i * evaluate M (P i) s :=
230       Finset.sum_le_sum (fun i _ => mul_le_mul_of_nonneg_left (value_le_tree M h s (P i) (hP i)) (hw i))
231 
232 /-- Returning a minimizing tree is noncomputable choice over a finite mathematical search.
233 It is not a claim of an efficient extracted solver. -/
234 def optimalTree (M : Model S A O D) (h : Nat) (s : S) : Tree A O D :=
235   (minimizing_tree_exists M h s).choose
236 
237 theorem optimalTree_spec (M : Model S A O D) (h : Nat) (s : S) :
238     (optimalTree M h s).Bounded h ∧ Feasible M h s (optimalTree M h s) ∧
239       evaluate M (optimalTree M h s) s = value M h s :=
240   (minimizing_tree_exists M h s).choose_spec
241 
242 end
243 end Planning
244 end Komorebi.MachineTheory

Back to source controls