BinaryExecution.lean

1 import MachineTheory.BinaryDiagnosis
2 
3 /-! # Execution meaning of the binary lower bounds -/
4 namespace Komorebi.MachineTheory.BinaryDiagnosis
5 open HardInquiry Finset
6 variable {X E C : Type} [DecidableEq X]
7 
8 /-- An actual successful run attains the worst-case online coordinate.
9 The terminal is charged one unit on every reachable state. Empty supports are not runs. -/
10 theorem worst_execution_attained (M : Model X E Bool C Unit) (s : Scope M)
11     (h : ℕ) (V : Finset X) (t : Tree E Bool C h) (ht : M.Valid h V t) :
12     ∃ x ∈ V, ∃ r, M.execute (fun _ _ _ => 1) h t x = some r ∧
13       r.cost () = (M.profile h V t).1 () := by
14   induction h generalizing V with
15   | zero =>
16     obtain ⟨x,hx⟩ := ht.1
17     exact ⟨x,hx,⟨x,t,fun _ => 1,[]⟩,rfl,(s.terminal_cost t V ht.1).symm⟩
18   | succ h ih =>
19     cases t with
20     | inl c =>
21       obtain ⟨x,hx⟩ := ht.1
22       exact ⟨x,hx,⟨x,c,fun _ => 1,[]⟩,rfl,(s.terminal_cost c V ht.1).symm⟩
23     | inr ek =>
24       obtain ⟨e,k⟩ := ek
25       let f : Bool → ℕ := fun o => (Model.optional ((k o).map (M.profile h (M.update V e o)))).1 ()
26       have hpos : 0 < univ.sup f := by
27         obtain ⟨x,hx⟩ := ht.1.1
28         obtain ⟨u,hu,hv⟩ := (M.valid_child ht (M.observe e x)).mp ⟨_,M.actual_next_mem hx e⟩
29         have hcost : 1 ≤ f (M.observe e x) := by
30           simp only [f,hu,Option.map_some,Model.optional,Option.getD_some]
31           rw [work_eq_depth_succ M s h _ u hv]
32           omega
33         exact lt_of_lt_of_le (Nat.lt_of_lt_of_le Nat.zero_lt_one hcost)
34           (Finset.le_sup (f := f) (mem_univ (M.observe e x)))
35       obtain ⟨o,_,hmax⟩ := (univ : Finset Bool).exists_mem_eq_sup univ_nonempty f
36       cases he : k o with
37       | none =>
38         have hz : f o = 0 := by simp [f,he,Model.optional]
39         omega
40       | some child =>
41         have hv : M.Valid h (M.update V e o) child := by simpa only [he] using ht.2 o
42         obtain ⟨y,hy,r,hr,hcost⟩ := ih _ child hv
43         obtain ⟨x,hx,hobs,hnext⟩ := (M.mem_update V e o y).mp hy
44         have hp := ht.1.2 x hx
45         refine ⟨x,hx,M.prepend e o r,?_,?_⟩
46         · simp only [Model.execute,hp,ite_true,hobs,he,Option.bind_some,hnext,hr,Option.map_some]
47         · change M.stepCost e () + r.cost () = M.stepCost e () + univ.sup f
48           rw [hmax,hcost]
49           simp only [f,he,Option.map_some,Model.optional,Option.getD_some]
50 
51 /-- The information bound is a lower bound on an actual possible execution, not just a ledger. -/
52 theorem actual_run_lower_bound (M : Model X E Bool C Unit) (s : Scope M)
53     (h : ℕ) (V : Finset X) (t : Tree E Bool C h) (ht : M.Valid h V t) :
54     ∃ x ∈ V, ∃ r, M.execute (fun _ _ _ => 1) h t x = some r ∧
55       1 + Nat.clog 2 V.card ≤ r.cost () := by
56   obtain ⟨x,hx,r,hr,hcost⟩ := worst_execution_attained M s h V t ht
57   exact ⟨x,hx,r,hr,hcost ▸ (binary_lower_bounds M s h V t ht).2.1⟩
58 
59 end Komorebi.MachineTheory.BinaryDiagnosis

Back to source controls