Skip to content

Commit 02b00a4

Browse files
wkrozowskiwkrozowski
committed
push intermediate work
1 parent fb6192e commit 02b00a4

File tree

1 file changed

+242
-37
lines changed

1 file changed

+242
-37
lines changed

‎src/Std/Data/DTreeMap/Slice.lean‎

Lines changed: 242 additions & 37 deletions
Original file line numberDiff line numberDiff line change
@@ -16,65 +16,97 @@ public import Std.Data.DTreeMap
1616
namespace Std.DTreeMap
1717
open Std.Iterators
1818

19-
-- Zipper-based iterator for tree maps
20-
inductive MapIterator (α : Type u) (β : α → Type v) where
19+
public def Internal.Impl.treeSize : Internal.Impl α β → Nat
20+
| .leaf => 0
21+
| .inner _ _ _ l r => 1 + l.treeSize + treeSize r
22+
23+
section MapIterator
24+
public inductive Zipper (α : Type u) (β : α → Type v) where
2125
| done
22-
| cons (k : α) (v : β k) (tree : Internal.Impl α β) (next : MapIterator α β)
26+
| cons (k : α) (v : β k) (tree : Internal.Impl α β) (next : Zipper α β)
2327

24-
def MapIterator.toList : MapIterator α β → List ((a : α) × β a)
28+
variable {α : Type u} {β : α → Type v}
29+
30+
public def Zipper.toList : Zipper α β → List ((a : α) × β a)
2531
| .done => []
2632
| .cons k v tree next => ⟨k,v⟩ :: tree.toList ++ next.toList
2733

28-
def treeSize : Internal.Impl α β → Nat
29-
| .leaf => 0
30-
| .inner _ _ _ l r => 1 + treeSize l + treeSize r
34+
public def Zipper.keys : Zipper α β → List α
35+
| .done => []
36+
| .cons k _ tree next => k :: tree.keys ++ next.keys
3137

32-
def MapIterator.size : MapIterator α β → Nat
38+
def Zipper.size : Zipper α β → Nat
3339
| .done => 0
34-
| .cons _ _ tree next => 1 + treeSize (tree) + next.size
40+
| .cons _ _ tree next => 1 + tree.treeSize + next.size
41+
42+
public def Zipper.WF [Ord α] : Zipper α β → Prop
43+
| .done => True
44+
| .cons k _ tree next => tree.keys.all (fun key => (compare key k).isLE) ∧ next.keys.all (fun key => (compare key k).isLE)
3545

36-
def MapIterator.prependMap : Internal.Impl α β → MapIterator α β → MapIterator α β
46+
public def Zipper.prependMap : Internal.Impl α β → Zipper α β → Zipper α β
3747
| .leaf, it => it
3848
| .inner _ k v l r, it => prependMap l (.cons k v r it)
3949

40-
def prependMap_to_list (t : Internal.Impl α β) (it : MapIterator α β) : (MapIterator.prependMap t it).toList = t.toList ++ it.toList := by
50+
theorem prependMap_WF_inv [Ord α] [TransOrd α] {t : Internal.Impl α β} {wf : Internal.Impl.WF t} {z : Zipper α β} {z_wf : Zipper.WF z} : Zipper.WF (Zipper.prependMap t z) := by
51+
induction t generalizing z
52+
case leaf =>
53+
simp [Zipper.prependMap]
54+
exact z_wf
55+
case inner _ k v l r l_ih r_ih =>
56+
simp [Zipper.prependMap]
57+
apply l_ih
58+
. sorry
59+
. constructor
60+
sorry
61+
sorry
62+
63+
public theorem Zipper.prependMap_to_list (t : Internal.Impl α β) (it : Zipper α β) : (Zipper.prependMap t it).toList = t.toList ++ it.toList := by
4164
induction t generalizing it
4265
case leaf =>
43-
simp [MapIterator.prependMap, Internal.Impl.toList_eq_toListModel]
66+
simp [prependMap, Internal.Impl.toList_eq_toListModel]
4467
case inner _ k v l r l_ih r_ih =>
45-
simp only [MapIterator.prependMap]
46-
specialize l_ih (MapIterator.cons k v r it)
68+
simp only [Zipper.prependMap]
69+
specialize l_ih (Zipper.cons k v r it)
4770
rw [l_ih]
48-
simp [MapIterator.toList, Internal.Impl.toList_eq_toListModel]
71+
simp [toList, Internal.Impl.toList_eq_toListModel]
4972

50-
variable (α : Type u) (β : α → Type v)
51-
theorem prependMap_size (t : Internal.Impl α β) (it : MapIterator α β) : (MapIterator.prependMap t it).size = treeSize t + it.size := by
52-
fun_induction MapIterator.prependMap
73+
theorem Zipper.prependMap_size (t : Internal.Impl α β) (it : Zipper α β) : (Zipper.prependMap t it).size = t.treeSize + it.size := by
74+
fun_induction Zipper.prependMap
5375
case case1 =>
54-
simp only [treeSize, Nat.zero_add]
76+
simp only [Internal.Impl.treeSize, Nat.zero_add]
5577
case case2 size k v l r it ih =>
56-
simp only [ih, MapIterator.size, treeSize, ← Nat.add_assoc, Nat.add_comm]
78+
simp only [ih, Zipper.size, Internal.Impl.treeSize, ← Nat.add_assoc, Nat.add_comm]
5779

58-
structure RxcIterator (cmp : α → α → Ordering) where
59-
iter : MapIterator α β
80+
end MapIterator
81+
82+
section Rxc
83+
84+
public structure RxcIterator (α : Type u) (β : α → Type v) (cmp : α → α → Ordering) where
85+
iter : Zipper α β
6086
upper : α
6187

62-
def RxcIterator.inBounds {cmp : α → α → Ordering} (it : RxcIterator α β cmp) (k : α) : Bool :=
88+
variable {α : Type u} {β : α → Type v}
89+
90+
public def RxcIterator.inBounds {cmp : α → α → Ordering} (it : RxcIterator α β cmp) (k : α) : Bool :=
6391
(cmp k it.upper).isLE
6492

65-
def RxcIterator.step {cmp : α → α → Ordering} : RxcIterator α β cmp → IterStep (IterM (α := RxcIterator α β cmp) Id ((a : α) × β a)) ((a : α) × β a)
93+
public def RxcIterator.step {cmp : α → α → Ordering} : RxcIterator α β cmp → IterStep (IterM (α := RxcIterator α β cmp) Id ((a : α) × β a)) ((a : α) × β a)
6694
| ⟨.done, _⟩ => .done
6795
| ⟨.cons k v t it, upper⟩ =>
6896
if (cmp k upper).isLE then
6997
.yield ⟨it.prependMap t, upper⟩ ⟨k, v⟩
7098
else
7199
.done
72100

73-
instance : Iterator (RxcIterator α β cmp) Id ((a : α) × β a) where
101+
public instance : Iterator (RxcIterator α β cmp) Id ((a : α) × β a) where
74102
IsPlausibleStep it step := it.internalState.step = step
75103
step it := ⟨it.internalState.step, rfl⟩
76104

77-
def RxC_finite : FinitenessRelation (RxcIterator α β cmp) Id where
105+
public instance : IteratorCollect (RxcIterator α β cmp) Id Id := .defaultImplementation
106+
107+
public instance : IteratorCollectPartial (RxcIterator α β cmp) Id Id := .defaultImplementation
108+
109+
def instFinitenessRelation : FinitenessRelation (RxcIterator α β cmp) Id where
78110
rel t' t := t'.internalState.iter.size < t.internalState.iter.size
79111
wf := by
80112
apply InvImage.wf
@@ -104,24 +136,197 @@ def RxC_finite : FinitenessRelation (RxcIterator α β cmp) Id where
104136
contradiction
105137
case isTrue heq =>
106138
simp at h'
107-
simp only [h2, ← h'.1, prependMap_size, MapIterator.size, Nat.add_lt_add_iff_right,
139+
simp only [h2, ← h'.1, Zipper.prependMap_size, Zipper.size, Nat.add_lt_add_iff_right,
108140
Nat.lt_add_left_iff_pos, Nat.lt_add_one]
109141

110-
instance instFinite [TransCmp cmp] : Finite (RxcIterator α β cmp) Id :=
111-
.of_finitenessRelation (RxC_finite α β)
142+
@[no_expose]
143+
public instance instFinite : Finite (RxcIterator α β cmp) Id :=
144+
.of_finitenessRelation instFinitenessRelation
112145

113-
instance : IteratorCollect (RxcIterator α β cmp) Id Id := .defaultImplementation
146+
public theorem toList_lemma {it : Iter (α := RxcIterator α β cmp) ((a : α) × β a)} : it.toList = it.internalState.iter.toList.filter (fun e => (cmp e.fst bound).isLE) := by
147+
unfold Iter.toList
148+
simp [Iter.toIterM]
149+
unfold Iter.internalState
150+
simp [instIteratorCollectRxcIteratorIdSigma]
151+
sorry
114152

115-
instance : IteratorCollectPartial (RxcIterator α β cmp) Id Id := .defaultImplementation
153+
public theorem step_rxcIterator_eq_match {cmp : α → α → Ordering} {it : IterM (α := RxcIterator α β cmp) Id ((a : α) × β a)} :
154+
it.step = ⟨match it.internalState with
155+
| { iter := Zipper.done, upper := _ } => IterStep.done
156+
| { iter := Zipper.cons k v t it, upper := upper } =>
157+
if (cmp k upper).isLE = true then
158+
IterStep.yield { internalState := { iter := Zipper.prependMap t it, upper := upper } } ⟨k, v⟩
159+
else IterStep.done,
160+
(by simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep, RxcIterator.step]; split; all_goals (rename_i heq; simp only [heq]))⟩ := by
161+
simp [IterM.step, Iterator.step, RxcIterator.step]
162+
ext
163+
congr 1
116164

117-
def test : Internal.Impl Nat fun _ => Nat :=
118-
.ofList [⟨1, 2⟩, ⟨5, 4⟩, ⟨3, 1⟩, ⟨2, 8⟩, ⟨7, 9⟩, ⟨10, 5⟩]
165+
public structure RicSliceData (α : Type u) (β : α → Type v) (cmp : α → α → Ordering := by exact compare) where
166+
treeMap : DTreeMap.Raw α β cmp
167+
range : Ric α
119168

120-
def iterLE (t : Internal.Impl α β) (comp : α → α → Ordering) (bound : α) : IterM (α := RxcIterator α β comp) Id ((a : α) × β a) :=
121-
⟨{iter := MapIterator.prependMap t .done, upper := bound }⟩
169+
public abbrev RicSlice α β cmp := Slice (RicSliceData α β cmp)
170+
171+
public instance : Ric.Sliceable (DTreeMap.Raw α β cmp) α (RicSlice α β cmp) where
172+
mkSlice carrier range := ⟨carrier, range⟩
173+
174+
@[always_inline]
175+
public def RicSlice.Internal.iterM (s : RicSlice α β cmp) : IterM (α := RxcIterator α β cmp) Id ((a : α) × β a) :=
176+
⟨⟨Zipper.done.prependMap s.1.treeMap.inner, s.1.range.upper⟩⟩
177+
178+
public instance {s : RicSlice α β cmp} : ToIterator s Id ((a : α) × β a) where
179+
State := RxcIterator α β cmp
180+
iterMInternal := RicSlice.Internal.iterM s
181+
182+
def test : DTreeMap.Raw Nat (fun _ => Nat) compare := .ofList [⟨0, 0⟩, ⟨1, 1⟩, ⟨100, 3⟩, ⟨101, 4⟩]
183+
184+
-- RxcIterator α β cmp
185+
public theorem step_iter_ricSlice_eq_match {α β} {cmp : α → α → Ordering} {t : DTreeMap.Raw α β cmp} {a b : α} :
186+
t[*...=b].iter.step = ⟨match ({ iter := Zipper.prependMap t.inner Zipper.done, upper := b } : RxcIterator α β cmp) with
187+
| { iter := Zipper.done, upper := upper } => IterStep.done
188+
| { iter := Zipper.cons k v t it, upper := upper } =>
189+
if (cmp k upper).isLE = true then
190+
IterStep.yield { internalState := { iter := Zipper.prependMap t it, upper := upper } } ⟨k, v⟩
191+
else IterStep.done, (sorry)⟩ := by
192+
rw [Slice.iter_eq_toIteratorIter]
193+
simp only [Ric.Sliceable.mkSlice, instSliceableRawRicSlice, RicSlice.Internal.iterM, ToIterator.iter_eq, IterM.toIter, Iter.step]
194+
rw [step_rxcIterator_eq_match]
195+
simp only [Iter.toIterM]
196+
simp only [IterM.Step.toPure, IterStep.mapIterator, Id.run]
197+
congr
198+
split
199+
case h_1 =>
200+
rename_i heq
201+
split at heq
202+
any_goals contradiction
203+
. rename_i heq2
204+
simp at heq2
205+
split at heq
206+
. simp at heq
207+
rename_i heq3
208+
simp [heq3, ← heq.1, heq.2, IterM.toIter]
209+
. contradiction
210+
case h_2 =>
211+
rename_i heq
212+
split at heq
213+
any_goals contradiction
214+
. rename_i heq
215+
split at heq
216+
. contradiction
217+
. contradiction
218+
case h_3 =>
219+
rename_i heq
220+
split at heq
221+
any_goals trivial
222+
split at heq
223+
. contradiction
224+
. rename_i heq2
225+
simp [heq2]
226+
227+
public theorem toList_rocSlice_eq_filter_toList {α β} {cmp : α → α → Ordering}
228+
{t : DTreeMap.Raw α β cmp} (h : t.WF) {bound : α} :
229+
t[*...=bound].toList = t.toList.filter (fun e => (cmp e.fst bound).isLE) := by
230+
simp only [Slice.toList_eq_toList_iter]
231+
rw [Iter.toList_eq_match_step]
232+
rw [step_iter_ricSlice_eq_match]
233+
split
234+
case h_1 x it' out heq =>
235+
split at heq
236+
any_goals contradiction
237+
rename_i x' k v t it upper heq2
238+
simp at heq2
239+
split at heq
240+
any_goals contradiction
241+
simp at heq
242+
rename_i isLE
243+
rename_i t'
244+
have ⟨heq₁, heq₂⟩ := heq
245+
rw [← heq₂]
246+
have := @Zipper.prependMap_to_list α β t'.inner .done
247+
rw [heq2.1] at this
248+
simp [Zipper.toList] at this
249+
rw [← heq₁]
250+
have toList_lemma := @toList_lemma α β cmp bound { internalState := { iter := Zipper.prependMap t it, upper := upper } }
251+
simp at toList_lemma
252+
rw [toList_lemma]
253+
simp only [Raw.toList]
254+
rw [← this]
255+
simp only [List.filter, isLE, heq2.2]
256+
congr
257+
simp [Zipper.prependMap_to_list]
258+
case h_2 =>
259+
rename_i heq
260+
split at heq
261+
any_goals contradiction
262+
. split at heq
263+
any_goals contradiction
264+
case h_3 x heq =>
265+
split at heq
266+
case h_1 it upper heq2 =>
267+
simp at heq2
268+
unfold Zipper.prependMap at heq2
269+
split at heq2
270+
. rename_i eq_empty
271+
simp only [Raw.toList]
272+
rw [eq_empty]
273+
rw [Internal.Impl.toList_eq_toListModel]
274+
simp only [Internal.Impl.toListModel_leaf, List.filter_nil]
275+
. rename_i t₁ t₂ _ k v l r heq3
276+
replace heq2 := heq2.1
277+
sorry
278+
case h_2 x' k v t it upper heq2 =>
279+
split at heq
280+
. contradiction
281+
. rename_i t' notLE
282+
simp at heq2
283+
have ⟨heq2₁, heq2₂⟩ := heq2
284+
clear heq2
285+
have prependMap_to_List := @Zipper.prependMap_to_list α β t'.inner Zipper.done
286+
simp [heq2₁, Zipper.toList] at prependMap_to_List
287+
simp only [Raw.toList]
288+
rw [← prependMap_to_List]
289+
simp only [List.filter]
290+
rw [← heq2₂] at notLE
291+
simp only [notLE]
292+
293+
sorry
294+
exact bound
295+
296+
297+
298+
299+
300+
301+
302+
303+
304+
305+
306+
307+
308+
309+
310+
311+
312+
313+
314+
315+
316+
317+
318+
319+
320+
321+
322+
323+
324+
325+
326+
327+
328+
#eval test[*...=1].toList
122329

123-
#eval (iterLE _ _ test compare 5).allowNontermination.toList
124330

125-
section Rxc
126331
end Rxc
127332
end Std.DTreeMap

0 commit comments

Comments
 (0)