Skip to content

Commit 135b94f

Browse files
datokratdatokrat
committed
wip
1 parent feb974b commit 135b94f

File tree

2 files changed

+225
-49
lines changed

2 files changed

+225
-49
lines changed

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

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -928,6 +928,14 @@ theorem getEntryGT?_eq_some_iff {k e} :
928928
e ∈ t.toList ∧ cmp k e.fst = .lt ∧ ∀ k' ∈ keys t, cmp k k' = .lt → (cmp e.fst k').isLE := by
929929
sorry
930930

931+
theorem getEntryGE?_of_isEmpty {k} (h : t.isEmpty) :
932+
t.getEntryGE? k = none := by
933+
sorry
934+
935+
theorem getEntryGT?_of_isEmpty {k} (h : t.isEmpty) :
936+
t.getEntryGT? k = none := by
937+
sorry
938+
931939
theorem getKeyGE?_eq_some_iff {k k'} :
932940
t.getKeyGE? k = some k' ↔
933941
k' ∈ keys t ∧ (cmp k k').isLE ∧ ∀ k'' ∈ keys t, (cmp k k'').isLE → (cmp k' k'').isLE := by

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

Lines changed: 217 additions & 49 deletions
Original file line numberDiff line numberDiff line change
@@ -144,6 +144,14 @@ public theorem step_rxcIterator_eq_match' {α β} {cmp : α → α → Ordering}
144144
rw [step_rxcIterator_eq_match]
145145
sorry
146146

147+
public theorem val_step_rxcIterator_eq_match' {α β} {cmp : α → α → Ordering} [TransCmp cmp] {it : Iter (α := RxcIterator α β cmp) _} :
148+
it.step.val = (match it.internalState.next.filter (fun e => (cmp e.fst it.internalState.bound).isLE) with
149+
| some next =>
150+
.yield ⟨it.internalState.treeMap, it.internalState.treeMap.getEntryGT? next.fst, it.internalState.bound, (by apply getEntryGE?_getEntryGT?_eq_some)⟩ next
151+
| none =>
152+
.done ) := by
153+
sorry
154+
147155
-- public theorem RxcIterator.induct {α β} {cmp : α → α → Ordering} [TransCmp cmp]
148156
-- (motive : Iter (α := RxcIterator α β cmp) _ → Sort x)
149157
-- (step : (it : Iter (α := RxcIterator α β cmp) _) →
@@ -152,6 +160,189 @@ public theorem step_rxcIterator_eq_match' {α β} {cmp : α → α → Ordering}
152160

153161
end Rxc
154162

163+
public structure RocSliceData (α : Type u) (β : α → Type v)
164+
(cmp : α → α → Ordering := by exact compare) where
165+
treeMap : DTreeMap α β cmp
166+
range : Roc α
167+
168+
public abbrev RocSlice α β cmp := Slice (RocSliceData α β cmp)
169+
170+
public instance : Roc.Sliceable (DTreeMap α β cmp) α (RocSlice α β cmp) where
171+
mkSlice carrier range := ⟨carrier, range⟩
172+
173+
@[always_inline]
174+
public def RocSlice.Internal.iterM (s : RocSlice α β cmp) : IterM (α := RxcIterator α β cmp) Id ((a : α) × β a) :=
175+
⟨⟨s.1.treeMap, s.1.treeMap.getEntryGT? s.1.range.lower, s.1.range.upper,
176+
by apply getEntryGE?_getEntryGT?_eq_some⟩⟩
177+
178+
public instance {s : RocSlice α β cmp} : ToIterator s Id ((a : α) × β a) where
179+
State := RxcIterator α β cmp
180+
/-
181+
There is a good reason to extract the iterator into a separate function `RccSlice.Internal.iterM`:
182+
The `Iterator` instance on `ToIterator.State` needs to unfold `ToIterator.State`, which requires
183+
unfolding this `ToIterator` instance. In consequence, the definition of `iterMInternal` is also
184+
unfolded. Because it is complex and highly dependent, this is not desirable.
185+
See `Std.Iterators.instIteratorState`.
186+
-/
187+
iterMInternal := RocSlice.Internal.iterM s
188+
189+
#eval (.ofList [⟨0, 0⟩, ⟨1, 1⟩, ⟨100, 3⟩, ⟨101, 4⟩] : DTreeMap Nat (fun _ => Nat) compare)[1<...=102].toList
190+
191+
public theorem step_iter_rocSlice_eq_match {α β} {cmp : α → α → Ordering} [TransCmp cmp] {t : DTreeMap α β cmp} {a b : α} :
192+
t[a<...=b].iter.step = (match h : t.getEntryGT? a with
193+
| some next =>
194+
if h' : (cmp next.fst b).isLE then
195+
.yield ⟨t, t.getEntryGT? next.fst, b, (by apply getEntryGE?_getEntryGT?_eq_some)⟩ next
196+
(by simp [Iter.IsPlausibleStep, IterM.IsPlausibleStep, Iterator.IsPlausibleStep, Slice.iter_eq_toIteratorIter, ToIterator.iter_eq, RocSlice.Internal.iterM, Roc.Sliceable.mkSlice, Iter.toIterM, IterM.toIter, h', h])
197+
else
198+
.done (by simpa [Iter.IsPlausibleStep, IterM.IsPlausibleStep, Iterator.IsPlausibleStep, Slice.iter_eq_toIteratorIter, ToIterator.iter_eq, RocSlice.Internal.iterM, Roc.Sliceable.mkSlice, h] using h')
199+
| none =>
200+
.done (by simp [Iter.IsPlausibleStep, IterM.IsPlausibleStep, Iterator.IsPlausibleStep, Slice.iter_eq_toIteratorIter, ToIterator.iter_eq, RocSlice.Internal.iterM, Roc.Sliceable.mkSlice, h])) := by
201+
simp only [Iter.step, PlausibleIterStep.yield, PlausibleIterStep.done]
202+
rw [step_rxcIterator_eq_match]
203+
simp only [PlausibleIterStep.yield, PlausibleIterStep.done, Id.run_pure]
204+
simp only [RocSlice.Internal.iterM, Iter.toIterM, Slice.iter_eq_toIteratorIter, ToIterator.iter_eq, IterM.toIter]
205+
simp [Roc.Sliceable.mkSlice]
206+
split <;> rename_i heq
207+
· simp only [Slice.iter_eq_toIteratorIter, ToIterator.iter_eq, IterM.toIter, RocSlice.Internal.iterM] at heq
208+
split <;> split <;> simp_all [IterM.toIter]
209+
· simp only [Slice.iter_eq_toIteratorIter, ToIterator.iter_eq, IterM.toIter, RocSlice.Internal.iterM] at heq
210+
split <;> simp_all
211+
212+
public theorem val_step_iter_rocSlice_eq_match {α β} {cmp : α → α → Ordering} [TransCmp cmp] {t : DTreeMap α β cmp} {a b : α} :
213+
t[a<...=b].iter.step.val = (match t.getEntryGT? a with
214+
| some next =>
215+
if (cmp next.fst b).isLE then
216+
.yield ⟨t, t.getEntryGT? next.fst, b, (by apply getEntryGE?_getEntryGT?_eq_some)⟩ next
217+
else
218+
.done
219+
| none =>
220+
.done) := by
221+
rw [step_iter_rocSlice_eq_match]
222+
split <;> split <;> simp_all
223+
224+
public theorem val_step_iter_rocSlice_eq_match' {α β} {cmp : α → α → Ordering} [TransCmp cmp] {t : DTreeMap α β cmp} {a b : α} :
225+
t[a<...=b].iter.step.val = (match (t.getEntryGT? a).filter (fun e => (cmp e.fst b).isLE) with
226+
| some next =>
227+
.yield ⟨t, t.getEntryGT? next.fst, b, (by apply getEntryGE?_getEntryGT?_eq_some)⟩ next
228+
| none =>
229+
.done) := by
230+
rw [val_step_iter_rocSlice_eq_match]
231+
split
232+
· split <;> simp_all [Option.filter_some]
233+
· simp_all
234+
235+
public theorem filter_toList_eq_match_lt_and_isLE {α β} {cmp : α → α → Ordering} [TransCmp cmp] {t : DTreeMap α β cmp} {a b : α} :
236+
t.toList.filter (fun e => cmp a e.fst = .lt ∧ (cmp e.fst b).isLE) = (match (t.getEntryGT? a).filter (fun e => (cmp e.fst b).isLE) with
237+
| some next =>
238+
next :: t.toList.filter (fun e => cmp next.fst e.fst = .lt ∧ (cmp e.fst b).isLE)
239+
| none =>
240+
[]) := by
241+
induction hs : t.size
242+
· rw [← beq_iff_eq, ← DTreeMap.isEmpty_eq_size_eq_zero] at hs
243+
have : t.toList = [] := by simpa [← DTreeMap.isEmpty_toList] using hs
244+
simp [getEntryGT?_of_isEmpty hs, this]
245+
· sorry
246+
247+
public theorem toList_rocSlice_eq_filter_toList {α β} {cmp : α → α → Ordering} [TransCmp cmp]
248+
{t : DTreeMap α β cmp} {a b : α} :
249+
t[a<...=b].toList = t.toList.filter (fun e => cmp a e.fst = .lt ∧ (cmp e.fst b).isLE) := by
250+
rw [filter_toList_eq_match_lt_and_isLE, Slice.toList_eq_toList_iter, Iter.toList_eq_match_step,
251+
val_step_iter_rocSlice_eq_match']
252+
cases Option.filter (fun e => (cmp e.fst b).isLE) (t.getEntryGT? a)
253+
· simp
254+
· rename_i next
255+
suffices h : t[next.fst<...=b].toList = t.toList.filter (fun e => cmp next.fst e.fst = .lt ∧ (cmp e.fst b).isLE) by
256+
simpa [Slice.toList_eq_toList_iter, Slice.iter_eq_toIteratorIter, ToIterator.iter_eq,
257+
RocSlice.Internal.iterM, Roc.Sliceable.mkSlice] using h
258+
apply toList_rocSlice_eq_filter_toList
259+
termination_by (t.toList.filter (fun e => cmp a e.fst = .lt ∧ (cmp e.fst b).isLE)).length
260+
decreasing_by
261+
rename_i next hnext
262+
simp
263+
simp only [getEntryGT?_eq_some_iff, Option.filter_eq_some_iff] at hnext
264+
apply List.length_filter_strict_mono (a := next)
265+
· simp
266+
intro e hne heb
267+
exact ⟨TransCmp.lt_trans hnext.1.2.1 hne, heb⟩
268+
· exact hnext.1.1
269+
· simp [ReflCmp.compare_self]
270+
· simp
271+
exact ⟨hnext.1.2.1, hnext.2⟩
272+
273+
theorem toList_rocSlice_eq_toList_rocSlice {α β} {cmp : α → α → Ordering} [TransCmp cmp] {t t': DTreeMap α β cmp} {a b a' b' : α}
274+
(h : ∀ c, (c ∈ t.toList ∧ cmp a c.fst = .lt ∧ (cmp c.fst b).isLE) ↔ (c ∈ t'.toList ∧ cmp a' c.fst = .lt ∧ (cmp c.fst b').isLE)) :
275+
t[a<...=b].toList = t'[a'<...=b'].toList := by
276+
-- simp only [Slice.toList_eq_toList_iter, Slice.iter_eq_toIteratorIter, ToIterator.iter_eq,
277+
-- RccSlice.Internal.iterM, Rcc.Sliceable.mkSlice, IterM.toIter]
278+
simp only [Slice.toList_eq_toList_iter]
279+
generalize hi : Slice.iter (Roc.Sliceable.mkSlice t a<...=b) = it
280+
change Iter (α := RxcIterator α β cmp) _ at it
281+
induction it using Iter.inductSteps generalizing a b a' b' with | step it ihy ihs
282+
rw [← hi]
283+
simp only [Slice.iter_eq_toIteratorIter, ToIterator.iter_eq, RocSlice.Internal.iterM, Roc.Sliceable.mkSlice, IterM.toIter]
284+
rw [Iter.toList_eq_match_step, Iter.toList_eq_match_step]
285+
rw [val_step_rxcIterator_eq_match', val_step_rxcIterator_eq_match']
286+
simp only
287+
have : (t.getEntryGT? a).filter (fun e => (cmp e.fst b).isLE) =
288+
(t'.getEntryGT? a').filter (fun e => (cmp e.fst b').isLE) := by
289+
ext e
290+
simp [getEntryGT?_eq_some_iff]
291+
specialize h
292+
constructor
293+
· intro h'
294+
have he := (h e).mp ⟨h'.1.1, h'.1.2.1, h'.2⟩
295+
refine ⟨⟨he.1, he.2.1, ?_⟩, he.2.2⟩
296+
intro k hk hk'
297+
by_cases hkb : (cmp k b').isLE
298+
· simp only [← map_fst_toList_eq_keys, List.mem_map] at hk
299+
obtain ⟨f, hfm, rfl⟩ := hk
300+
have hf := (h f).mpr ⟨hfm, hk', hkb⟩
301+
apply h'.1.2.2
302+
· simpa only [← map_fst_toList_eq_keys] using List.mem_map_of_mem hf.1
303+
· exact hf.2.1
304+
· refine TransCmp.isLE_trans he.2.2 ?_
305+
apply Ordering.isLE_of_eq_lt
306+
simpa [OrientedCmp.gt_iff_lt] using hkb
307+
· intro h'
308+
have he := (h e).mpr ⟨h'.1.1, h'.1.2.1, h'.2⟩
309+
refine ⟨⟨he.1, he.2.1, ?_⟩, he.2.2⟩
310+
intro k hk hk'
311+
by_cases hkb : (cmp k b).isLE
312+
· simp only [← map_fst_toList_eq_keys, List.mem_map] at hk
313+
obtain ⟨f, hfm, rfl⟩ := hk
314+
have hf := (h f).mp ⟨hfm, hk', hkb⟩
315+
apply h'.1.2.2
316+
· simpa only [← map_fst_toList_eq_keys] using List.mem_map_of_mem hf.1
317+
· exact hf.2.1
318+
· refine TransCmp.isLE_trans he.2.2 ?_
319+
apply Ordering.isLE_of_eq_lt
320+
simpa [OrientedCmp.gt_iff_lt] using hkb
321+
simp [this]
322+
cases heq : Option.filter (fun e => (cmp e.fst b').isLE) (t'.getEntryGT? a')
323+
· simp
324+
· rename_i out
325+
simp
326+
simp [Slice.iter_eq_toIteratorIter, ToIterator.iter_eq, RocSlice.Internal.iterM, Roc.Sliceable.mkSlice,
327+
← hi] at ihy
328+
apply ihy (a := out.fst) (a' := out.fst) (b := b) (b' := b') (out := out)
329+
· simp [Iter.IsPlausibleStep, IterM.IsPlausibleStep, Iterator.IsPlausibleStep, Iter.toIterM,
330+
IterM.toIter]
331+
rw [← this, Option.filter_eq_some_iff, and_comm] at heq
332+
simpa using heq
333+
· intro e
334+
have heq' := heq
335+
rw [← this, Option.filter_eq_some_iff, getEntryGT?_eq_some_iff] at heq'
336+
rw [Option.filter_eq_some_iff, getEntryGT?_eq_some_iff] at heq
337+
constructor
338+
· intro h'
339+
have he := (h e).mp ⟨h'.1, TransCmp.lt_trans heq'.1.2.1 h'.2.1, h'.2.2⟩
340+
exact ⟨he.1, h'.2.1, he.2.2⟩
341+
· intro h'
342+
have he := (h e).mpr ⟨h'.1, TransCmp.lt_trans heq.1.2.1 h'.2.1, h'.2.2⟩
343+
exact ⟨he.1, h'.2.1, he.2.2⟩
344+
· rfl
345+
155346
public structure RccSliceData (α : Type u) (β : α → Type v)
156347
(cmp : α → α → Ordering := by exact compare) where
157348
treeMap : DTreeMap α β cmp
@@ -224,16 +415,22 @@ public theorem val_step_iter_rccSlice_eq_match' {α β} {cmp : α → α → Ord
224415
· split <;> simp_all [Option.filter_some]
225416
· simp_all
226417

418+
public theorem filter_toList_eq_match {α β} {cmp : α → α → Ordering} [TransCmp cmp] {t : DTreeMap α β cmp} {a b : α} :
419+
t.toList.filter (fun e => (cmp a e.fst).isLE ∧ (cmp e.fst b).isLE) = (match (t.getEntryGE? a).filter (fun e => (cmp e.fst b).isLE) with
420+
| some next =>
421+
next :: t.toList.filter (fun e => cmp next.fst e.fst = .lt ∧ (cmp e.fst b).isLE)
422+
| none =>
423+
[]) := by
424+
sorry
425+
227426
theorem toList_rccSlice_eq_toList_rccSlice {α β} {cmp : α → α → Ordering} [TransCmp cmp] {t t': DTreeMap α β cmp} {a b a' b' : α}
228427
(h : ∀ c, (c ∈ t.toList ∧ (cmp a c.fst).isLE ∧ (cmp c.fst b).isLE) ↔ (c ∈ t'.toList ∧ (cmp a' c.fst).isLE ∧ (cmp c.fst b').isLE)) :
229428
t[a...=b].toList = t'[a'...=b'].toList := by
230-
-- simp only [Slice.toList_eq_toList_iter, Slice.iter_eq_toIteratorIter, ToIterator.iter_eq,
231-
-- RccSlice.Internal.iterM, Rcc.Sliceable.mkSlice, IterM.toIter]
232429
simp only [Slice.toList_eq_toList_iter]
233-
induction hi : Slice.iter (Rcc.Sliceable.mkSlice t a...=b) using Iter.inductSteps
234-
rw [← hi]
430+
simp only [Slice.iter_eq_toIteratorIter, ToIterator.iter_eq, RccSlice.Internal.iterM, Rcc.Sliceable.mkSlice, IterM.toIter]
235431
rw [Iter.toList_eq_match_step, Iter.toList_eq_match_step]
236-
simp only [val_step_iter_rccSlice_eq_match']
432+
rw [val_step_rxcIterator_eq_match', val_step_rxcIterator_eq_match']
433+
simp only
237434
have : (t.getEntryGE? a).filter (fun e => (cmp e.fst b).isLE) =
238435
(t'.getEntryGE? a').filter (fun e => (cmp e.fst b').isLE) := by
239436
ext e
@@ -269,54 +466,25 @@ theorem toList_rccSlice_eq_toList_rccSlice {α β} {cmp : α → α → Ordering
269466
apply Ordering.isLE_of_eq_lt
270467
simpa [OrientedCmp.gt_iff_lt] using hkb
271468
simp [this]
272-
cases Option.filter (fun e => (cmp e.fst b').isLE) (t'.getEntryGE? a')
469+
cases heq : Option.filter (fun e => (cmp e.fst b').isLE) (t'.getEntryGE? a')
273470
· simp
274-
· simp
275-
276-
match hn : t.getEntryGE? a, hn' : t'.getEntryGE? a' with
277-
| none, none => simp
278-
| some next, some next' =>
279-
have heq : ∀ e, (e ∈ t.toList ∧ (cmp a e.fst).isLE ∧ ∀ k, k ∈ t.keys → (cmp a k).isLE → (cmp e.fst k).isLE) →
280-
e = next := by simp [← getEntryGE?_eq_some_iff, hn, Option.some_inj]
281-
simp [getEntryGE?_eq_some_iff] at hn hn'
282-
have hm : next.fst ∈ t.keys := by simpa only [← map_fst_toList_eq_keys] using List.mem_map_of_mem hn.1
283-
have hm' : next'.fst ∈ t'.keys := by simpa only [← map_fst_toList_eq_keys] using List.mem_map_of_mem hn'.1
284-
have hle : (cmp next.fst b).isLE → (cmp next'.fst next.fst).isLE := by
285-
intro h'
286-
have := (h next).mp ⟨hn.1, hn.2.1, h'⟩
287-
exact hn'.2.2 next.fst
288-
(by simpa only [← map_fst_toList_eq_keys] using List.mem_map_of_mem this.1)
289-
this.2.1
290-
have hle' : (cmp next'.fst b').isLE → (cmp next.fst next'.fst).isLE := by
291-
intro h'
292-
have := (h next').mpr ⟨hn'.1, hn'.2.1, h'⟩
293-
exact hn.2.2 next'.fst
294-
(by simpa only [← map_fst_toList_eq_keys] using List.mem_map_of_mem this.1)
295-
this.2.1
296-
have : (cmp next.fst b).isLE ↔ (cmp next'.fst b').isLE := by
471+
· rename_i out
472+
simp
473+
have hroc := @toList_rocSlice_eq_toList_rocSlice
474+
simp [Slice.toList_eq_toList_iter, Slice.iter_eq_toIteratorIter, ToIterator.iter_eq, RocSlice.Internal.iterM,
475+
Roc.Sliceable.mkSlice] at hroc
476+
apply hroc
477+
· intro e
478+
have heq' := heq
479+
rw [← this, Option.filter_eq_some_iff, getEntryGE?_eq_some_iff] at heq'
480+
rw [Option.filter_eq_some_iff, getEntryGE?_eq_some_iff] at heq
297481
constructor
298482
· intro h'
299-
have := (h next).mp ⟨hn.1, hn.2.1, h'⟩
300-
exact TransCmp.isLE_trans (hle h') this.2.2
483+
have he := (h e).mp ⟨h'.1, TransCmp.isLE_trans heq'.1.2.1 (Ordering.isLE_of_eq_lt h'.2.1), h'.2.2⟩
484+
exact ⟨he.1, h'.2.1, he.2.2⟩
301485
· intro h'
302-
have := (h next').mpr ⟨hn'.1, hn'.2.1, h'⟩
303-
exact TransCmp.isLE_trans (hle' h') this.2.2
304-
by_cases h' : (cmp next.fst b).isLE
305-
· have : next' = next := by
306-
apply heq
307-
have h'' := this.mp h'
308-
have := (h next').mpr ⟨hn'.1, hn'.2.1, h''⟩
309-
refine ⟨this.1, this.2.1, ?_⟩
310-
intro k hk hk'
311-
exact TransCmp.isLE_trans (hle h') (hn.2.2 k hk hk')
312-
cases this
313-
simp [h', this.mp h']
314-
· have : ¬ (cmp next'.fst b').isLE := by simpa [this] using h'
315-
simp [h', this]
316-
| none, some x =>
317-
sorry
318-
| some x, none =>
319-
sorry
486+
have he := (h e).mpr ⟨h'.1, TransCmp.isLE_trans heq.1.2.1 (Ordering.isLE_of_eq_lt h'.2.1), h'.2.2⟩
487+
exact ⟨he.1, h'.2.1, he.2.2⟩
320488

321489
theorem rccSlice_toList_eq_filter_toList {α β} {cmp : α → α → Ordering} [TransCmp cmp] {t : DTreeMap α β cmp} {a b : α} :
322490
t[a...=b].toList = t.toList.filter (fun e => (cmp a e.fst).isLE ∧ (cmp e.fst b).isLE)

0 commit comments

Comments
 (0)