HardSemantics.lean

1 import MachineTheory.HardExecution
2 
3 /-! # Horizon embeddings, closed resource invariants and attained worst-case work -/
4 namespace Komorebi.MachineTheory.HardInquiry
5 open Finset
6 variable {X E O C R : Type}
7 namespace Model
8 
9 /-- Increase the permitted horizon without inserting an experiment. -/
10 def promote : (h : ℕ) → Tree E O C h → Tree E O C (h+1)
11   | 0, c => .inl c
12   | _+1, .inl c => .inl c
13   | h+1, .inr (e,k) => .inr (e, fun o => (k o).map (promote h))
14 
15 variable [DecidableEq X] [Fintype O] [DecidableEq O]
16 
17 omit [Fintype O] in
18 theorem promote_valid (M : Model X E O C R) (h : ℕ) (V : Finset X) (t : Tree E O C h) :
19     M.Valid (h+1) V (promote h t) ↔ M.Valid h V t := by
20   induction h generalizing V with
21   | zero => rfl
22   | succ h ih =>
23     cases t with
24     | inl c => rfl
25     | inr ek =>
26       obtain ⟨e,k⟩ := ek
27       change (M.Allowed V e ∧ _) ↔ (M.Allowed V e ∧ _)
28       apply and_congr_right
29       intro _
30       apply forall_congr'
31       intro o
32       cases he : k o with
33       | none => simp only [he,Option.map_none]
34       | some child => simpa only [he,Option.map_some] using ih (M.update V e o) child
35 
36 theorem promote_profile (M : Model X E O C R) (h : ℕ) (V : Finset X) (t : Tree E O C h) :
37     M.profile (h+1) V (promote h t) = M.profile h V t := by
38   induction h generalizing V with
39   | zero => rfl
40   | succ h ih =>
41     cases t with
42     | inl c => rfl
43     | inr ek =>
44       obtain ⟨e,k⟩ := ek
45       change M.nodeProfile e _ = M.nodeProfile e _
46       congr 1
47       funext o
48       cases he : k o with
49       | none => simp only [he,Option.map_none]
50       | some child => simp only [he,Option.map_some,ih]
51 
52 theorem pad_horizon (M : Model X E O C R) (h n : ℕ) (V : Finset X) (t : Tree E O C h)
53     (ht : M.Valid h V t) : ∃ u : Tree E O C (h+n), M.Valid (h+n) V u ∧ M.profile (h+n) V u = M.profile h V t := by
54   induction n with
55   | zero => exact ⟨t,ht,rfl⟩
56   | succ n ih =>
57     obtain ⟨u,hu,he⟩ := ih
58     exact ⟨promote (h+n) u, (M.promote_valid _ _ _).mpr hu, (M.promote_profile _ _ _).trans he⟩
59 
60 variable [Fintype E] [Fintype C] [Fintype R]
61 
62 /-- A finite closed backup table supplies lower bounds at EVERY horizon. -/
63 theorem closed_family_dominates (M : Model X E O C R) (F : Finset X → Finset (Profile R))
64     (closed : ∀ V, prune (M.backup F V) = F V) (h : ℕ) (V : Finset X) (t : Tree E O C h)
65     (ht : M.Valid h V t) : ∃ p ∈ F V, p ≤ M.profile h V t := by
66   induction h generalizing V with
67   | zero =>
68     have hm : (M.terminalCost t V,1) ∈ M.backup F V :=
69       (M.mem_backup F V _).mpr (Or.inl ((M.mem_stops V _).mpr ⟨t,ht,rfl⟩))
70     obtain ⟨p,hp,hle⟩ := HardPareto.exists_frontier_le _ hm
71     rw [← prune_eq_frontier,closed] at hp
72     exact ⟨p,hp,hle⟩
73   | succ h ih =>
74     obtain ⟨p,hp,hle⟩ := M.backup_dominates h F ih V t ht
75     obtain ⟨q,hq,hqp⟩ := HardPareto.exists_frontier_le _ hp
76     rw [← prune_eq_frontier,closed] at hq
77     exact ⟨q,hq,hqp.trans hle⟩
78 
79 /-- A closed family is an antichain at each support. -/
80 theorem closed_family_antichain (M : Model X E O C R) (F : Finset X → Finset (Profile R))
81     (closed : ∀ V, prune (M.backup F V) = F V) (V : Finset X)
82     {p q : Profile R} (hp : p ∈ F V) (hq : q ∈ F V) (hqp : q ≤ p) : p ≤ q := by
83   have hf : HardPareto.frontier (M.backup F V) = F V := by rw [← prune_eq_frontier,closed]
84   rw [← hf] at hp hq
85   exact ((HardPareto.mem_frontier _ _).mp hp).2 q (HardPareto.frontier_subset _ hq) hqp
86 
87 /-- Once its retained profiles are realizable, a closed table is the exact frontier. -/
88 theorem closed_family_exact (M : Model X E O C R) (F : Finset X → Finset (Profile R))
89     (closed : ∀ V, prune (M.backup F V) = F V) (h : ℕ) (V : Finset X)
90     (witness : ∀ p ∈ F V, ∃ t : Tree E O C h, M.Valid h V t ∧ M.profile h V t = p) :
91     M.solve h V = F V := by
92   ext p
93   rw [M.exact_frontier]
94   constructor
95   · rintro ⟨⟨t,ht,he⟩,hmin⟩
96     obtain ⟨q,hq,hqt⟩ := M.closed_family_dominates F closed h V t ht
97     rw [he] at hqt
98     obtain ⟨u,hu,hue⟩ := witness q hq
99     have hpq : p ≤ q := by simpa only [hue] using hmin u hu (by simpa only [hue] using hqt)
100     exact (le_antisymm hpq hqt) ▸ hq
101   · intro hp
102     refine ⟨witness p hp,?_⟩
103     intro t ht htp
104     obtain ⟨q,hq,hqt⟩ := M.closed_family_dominates F closed h V t ht
105     exact (M.closed_family_antichain F closed V hp hq (hqt.trans htp)).trans hqt
106 
107 omit [Fintype O] [Fintype E] [Fintype C] [Fintype R] in
108 /-- Strictly possible reports are exactly the stored children of a valid query. -/
109 theorem valid_child (M : Model X E O C R) {h : ℕ} {V : Finset X}
110     {e : E} {k : O → Option (Tree E O C h)} (hv : M.Valid (h+1) V (.inr (e,k))) (o : O) :
111     (M.update V e o).Nonempty ↔ ∃ t, k o = some t ∧ M.Valid h (M.update V e o) t := by
112   constructor
113   · intro hn
114     cases he : k o with
115     | none =>
116       have hz : M.update V e o = ∅ := by simpa only [he] using hv.2 o
117       exact False.elim (hn.ne_empty hz)
118     | some t => exact ⟨t,rfl,by simpa only [he] using hv.2 o⟩
119   · rintro ⟨t,_,ht⟩
120     exact M.valid_nonempty ht
121 
122 /-- Stronger than merely bounding terminal work: each coordinate is its exact maximum. -/
123 def ExactCharges (M : Model X E O C R) (charge : C → X → R → ℕ) : Prop :=
124   ∀ c V r, M.terminalCost c V r = V.sup (fun x => charge c x r)
125 
126 omit [DecidableEq X] [Fintype E] [Fintype O] [DecidableEq O] [Fintype C] [Fintype R] in
127  theorem ExactCharges.bounded {M : Model X E O C R} {charge : C → X → R → ℕ}
128     (h : M.ExactCharges charge) : M.ChargesBounded charge := by
129   intro c V x hx r
130   rw [h c V r]
131   exact Finset.le_sup (f := fun x => charge c x r) hx
132 
133 omit [Fintype E] [Fintype C] [Fintype R] in
134 /-- Each online coordinate has a realizing initial case. Different coordinates may use different cases. -/
135 theorem worst_coordinate_attained (M : Model X E O C R) (charge : C → X → R → ℕ)
136     (hc : M.ExactCharges charge) (h : ℕ) (V : Finset X) (t : Tree E O C h)
137     (hv : M.Valid h V t) (j : R) :
138     ∃ x ∈ V, ∃ r, M.execute charge h t x = some r ∧ r.cost j = (M.profile h V t).1 j := by
139   induction h generalizing V with
140   | zero =>
141     obtain ⟨x,hx,he⟩ := V.exists_mem_eq_sup hv.1 (fun x => charge t x j)
142     exact ⟨x,hx,⟨x,t,charge t x,[]⟩,rfl,he.symm.trans (hc t V j).symm⟩
143   | succ h ih =>
144     cases t with
145     | inl c =>
146       obtain ⟨x,hx,he⟩ := V.exists_mem_eq_sup hv.1 (fun x => charge c x j)
147       exact ⟨x,hx,⟨x,c,charge c x,[]⟩,rfl,he.symm.trans (hc c V j).symm⟩
148     | inr ek =>
149       obtain ⟨e,k⟩ := ek
150       let live : Finset O := univ.filter (fun o => (M.update V e o).Nonempty)
151       let f : O → ℕ := fun o => (optional ((k o).map (M.profile h (M.update V e o)))).1 j
152       have hn : live.Nonempty := by
153         obtain ⟨x,hx⟩ := hv.1.1
154         exact ⟨M.observe e x, mem_filter.mpr ⟨mem_univ _, ⟨_,M.actual_next_mem hx e⟩⟩⟩
155       have he : univ.sup f = live.sup f := by
156         apply le_antisymm
157         · apply Finset.sup_le
158           intro o _
159           by_cases hl : (M.update V e o).Nonempty
160           · exact Finset.le_sup (f := f) (mem_filter.mpr ⟨mem_univ _,hl⟩)
161           · have hz : k o = none := by
162               cases ho : k o with
163               | none => rfl
164               | some c => exact False.elim (hl ((M.valid_child hv o).mpr ⟨c,ho,by simpa only [ho] using hv.2 o⟩))
165             simp [f,hz,optional]
166         · apply Finset.sup_le
167           intro o _
168           exact Finset.le_sup (f := f) (mem_univ o)
169       obtain ⟨o,ho,hmax⟩ := live.exists_mem_eq_sup hn f
170       obtain ⟨child,hchild,hvalid⟩ := (M.valid_child hv o).mp (mem_filter.mp ho).2
171       obtain ⟨y,hy,r,hr,hcost⟩ := ih _ child hvalid
172       obtain ⟨x,hx,hobs,hnext⟩ := (M.mem_update V e o y).mp hy
173       have hperm := hv.1.2 x hx
174       refine ⟨x,hx,M.prepend e o r,?_,?_⟩
175       · simp only [execute,hperm,ite_true,hobs,hchild,Option.bind_some,hnext,hr,Option.map_some]
176       · change M.stepCost e j + r.cost j = M.stepCost e j + univ.sup f
177         rw [hcost,he,hmax]
178         simp only [f,hchild,Option.map_some,optional,Option.getD_some]
179 
180 end Model
181 end Komorebi.MachineTheory.HardInquiry

Back to source controls