BernsteinGridSearch.lean

1 import KomorebiLSM.DyadicBernsteinCertificate
2 import Mathlib.Logic.Encodable.Pi
3 
4 set_option autoImplicit false
5 namespace Komorebi.LSM.BernsteinGridSearch
6 open TensorBernsteinCertificate
7 noncomputable section
8 
9 /-- Proof-free finite rational leaf data; dimensions and every coefficient are enumerated. -/
10 abbrev LeafData := Σ m : ℕ, Σ n : ℕ, Fin (m+1) → Fin (n+1) → ℚ
11 
12 def leafValid (p : Polynomial₂) (R : Rectangle) (d : LeafData) : Prop :=
13   (∀ i j,0≤d.2.2 i j) ∧ R.localPolynomial p=tensorPolynomial d.2.2
14 
15 instance decidableLeafValid (p : Polynomial₂) (R : Rectangle) (d : LeafData) :
16     Decidable (leafValid p R d) := by unfold leafValid; infer_instance
17 
18 def leafCertificate (p : Polynomial₂) (R : Rectangle) (d : LeafData) (h : leafValid p R d) :
19     LocalCertificate p R where
20   degreeX := d.1
21   degreeY := d.2.1
22   coefficient := d.2.2
23   nonneg := h.1
24   identity := h.2
25 
26 def leafData {p : Polynomial₂} {R : Rectangle} (c : LocalCertificate p R) : LeafData :=
27   ⟨c.degreeX,c.degreeY,c.coefficient⟩
28 
29 theorem leafData_valid {p : Polynomial₂} {R : Rectangle} (c : LocalCertificate p R) :
30     leafValid p R (leafData c) := ⟨c.nonneg,c.identity⟩
31 
32 /-- Every round has all four children; no arbitrary rectangle list is accepted. -/
33 def GridData : ℕ → Type
34   | 0 => LeafData
35   | N+1 => Bool → Bool → GridData N
36 
37 instance encodableGridData (N : ℕ) : Encodable (GridData N) := by
38   induction N with
39   | zero => change Encodable LeafData; infer_instance
40   | succ N ih => change Encodable (Bool → Bool → GridData N); infer_instance
41 
42 def gridValid (p : Polynomial₂) (R : Rectangle) : (N : ℕ) → GridData N → Prop
43   | 0,d => leafValid p R d
44   | N+1,d => ∀ a b,gridValid p (R.quarter a b) N (d a b)
45 
46 instance decidableGridValid (p : Polynomial₂) (R : Rectangle) (N : ℕ) (d : GridData N) :
47     Decidable (gridValid p R N d) := by
48   induction N generalizing R with
49   | zero => exact decidableLeafValid p R d
50   | succ N ih =>
51     change Decidable (∀ a b,gridValid p (R.quarter a b) N (d a b))
52     letI (a b : Bool) : Decidable (gridValid p (R.quarter a b) N (d a b)) := ih _ _
53     infer_instance
54 
55 def toUniform (p : Polynomial₂) (R : Rectangle) :
56     {N : ℕ} → (d : GridData N) → gridValid p R N d → UniformCertificate p R N
57   | 0,d,h => leafCertificate p R d h
58   | _+1,d,h => fun a b => toUniform p (R.quarter a b) (d a b) (h a b)
59 
60 def ofUniform {p : Polynomial₂} {R : Rectangle} :
61     {N : ℕ} → UniformCertificate p R N → GridData N
62   | 0,c => leafData c
63   | _+1,c => fun a b => ofUniform (c a b)
64 
65 theorem ofUniform_valid {p : Polynomial₂} {R : Rectangle} {N : ℕ}
66     (c : UniformCertificate p R N) : gridValid p R N (ofUniform c) := by
67   induction N generalizing R with
68   | zero => exact leafData_valid c
69   | succ N ih => exact fun a b => ih (c a b)
70 
71 theorem ofUniform_toUniform (p : Polynomial₂) (R : Rectangle) {N : ℕ}
72     (d : GridData N) (h : gridValid p R N d) : ofUniform (toUniform p R d h)=d := by
73   induction N generalizing R with
74   | zero => rfl
75   | succ N ih =>
76     funext a b
77     exact ih (R.quarter a b) (d a b) (h a b)
78 
79 /-- Acceptance is equivalent to a certificate with exactly the enumerated finite data. -/
80 theorem gridValid_iff (p : Polynomial₂) (R : Rectangle) (N : ℕ) (d : GridData N) :
81     gridValid p R N d ↔ ∃ c : UniformCertificate p R N, ofUniform c=d := by
82   constructor
83   · intro h
84     exact ⟨toUniform p R d h,ofUniform_toUniform p R d h⟩
85   · rintro ⟨c,hc⟩
86     rw [← hc]
87     exact ofUniform_valid c
88 
89 section Enumeration
90 variable {α : Type*} [Encodable α] (valid : α → Prop) [DecidablePred valid]
91 
92 /-- One actual decoded finite description is tested at each dovetailed stage. -/
93 def step (k : ℕ) : Option α :=
94   match (Encodable.decode k : Option α) with
95   | none => none
96   | some a => if valid a then some a else none
97 
98 theorem step_sound {k : ℕ} {a : α} (h : step valid k=some a) : valid a := by
99   unfold step at h
100   cases hd : (Encodable.decode k : Option α) with
101   | none => simp [hd] at h
102   | some b =>
103     rw [hd] at h
104     by_cases hb : valid b
105     · simp [hb] at h
106       subst a
107       exact hb
108     · simp [hb] at h
109 
110 theorem step_complete (a : α) (ha : valid a) :
111     step valid (Encodable.encode a)=some a := by simp [step,ha]
112 
113 /-- The bounded search retains the first accepted description. -/
114 def search : ℕ → Option α
115   | 0 => step valid 0
116   | k+1 => match search k with
117     | none => step valid (k+1)
118     | some a => some a
119 
120 theorem search_sound {k : ℕ} {a : α} (h : search valid k=some a) : valid a := by
121   induction k with
122   | zero => exact step_sound valid h
123   | succ k ih =>
124     cases hk : search valid k with
125     | none => exact step_sound valid (by simpa [search,hk] using h)
126     | some b =>
127       have he : b=a := by simpa [search,hk] using h
128       subst a
129       exact ih hk
130 
131 theorem search_add {k : ℕ} {a : α} (h : search valid k=some a) (j : ℕ) :
132     search valid (k+j)=some a := by
133   induction j with
134   | zero => simpa using h
135   | succ j ih => simp [search,ih]
136 
137 theorem search_eventually (hexists : ∃ a,valid a) :
138     ∃ k a,valid a ∧ ∀ m,k≤m → search valid m=some a := by
139   obtain ⟨a,ha⟩ := hexists
140   have hk := step_complete valid a ha
141   have hfound (k : ℕ) : (∃ a,step valid k=some a) → ∃ a,search valid k=some a := by
142     cases k with
143     | zero => exact fun h => h
144     | succ k =>
145       intro h
146       cases hs : search valid k with
147       | none => simpa [search,hs] using h
148       | some b => exact ⟨b,by simp [search,hs]⟩
149   obtain ⟨b,hb⟩ := hfound (Encodable.encode a) ⟨a,hk⟩
150   refine ⟨Encodable.encode a,b,search_sound valid hb,?_⟩
151   intro m hm
152   have h := search_add valid hb (m-Encodable.encode a)
153   simpa only [Nat.add_sub_of_le hm] using h
154 end Enumeration
155 
156 end
157 end Komorebi.LSM.BernsteinGridSearch

Back to source controls