TreeMap Raw slices are done

Author: wkrozowski

src/Std/Data/DTreeMap/Internal/Zipper.lean

@@ -874,6 +874,42 @@ public theorem toList_rcc {α : Type u} {β : α → Type v} [Ord α] [TransOrd
 
 end Rcc
 
+namespace Const
+
+public structure RccSliceData (α : Type u) (β : Type v) [Ord α] where
+  treeMap : Impl α (fun _ => β)
+  range : Rcc α
+
+public abbrev RccSlice α β [Ord α] := Slice (RccSliceData α β)
+
+public instance {α : Type u} {β : Type v} [Ord α] : Rcc.Sliceable (Impl α (fun _ => β)) α (RccSlice α β) where
+  mkSlice carrier range := ⟨carrier, range⟩
+
+public instance [Ord α] {s : RccSlice α β} : ToIterator s Id (α × β) := by
+  apply ToIterator.of
+  . exact (⟨RxcIterator.mk (Zipper.prependMapGE s.1.treeMap s.1.range.lower .done) s.1.range.upper⟩ : Iter ((_ : α) × β)).map fun e => (e.1, e.2)
+
+public theorem toList_rcc {α : Type u} {β : Type v} [Ord α] [TransOrd α] (t : Impl α (fun _ => β))
+    (ordered : t.Ordered) (lowerBound upperBound : α) : t[lowerBound...=upperBound].toList = (Internal.Impl.Const.toList t).filter (fun e => (compare e.fst lowerBound).isGE ∧ (compare e.fst upperBound).isLE) := by
+  simp only [Rcc.Sliceable.mkSlice, Slice.toList_eq_toList_iter, Slice.iter,
+    Slice.Internal.iter_eq_toIteratorIter, ToIterator.iter, ToIterator.iterM_eq,
+    Iter.toIter_toIterM]
+  rw [Iter.toList_map]
+  have := @toList_rccIter α (fun _ => β) _ _ t ordered lowerBound upperBound
+  rw [RccIterator] at this
+  rw [this]
+  have eq : (fun (e : (_ : α) × β) => decide ((compare e.fst lowerBound).isGE = true ∧ (compare e.fst upperBound).isLE = true)) =
+    (fun (e : α × β) => decide ((compare e.fst lowerBound).isGE = true ∧ (compare e.fst upperBound).isLE = true)) ∘ (fun e => (e.1, e.2)) := by congr
+  conv =>
+    lhs
+    rhs
+    rw [eq]
+  rw [← List.filter_map]
+  congr
+  rw [Impl.Const.toList_eq_toListModel_map, Impl.toList_eq_toListModel]
+
+end Const
+
 section Rco
 
 @[always_inline]
@@ -1023,6 +1059,43 @@ public theorem toList_roo {α : Type u} {β : α → Type v} [Ord α] [TransOrd
 
 end Roo
 
+namespace Const
+
+public structure RooSliceData (α : Type u) (β : Type v) [Ord α] where
+  treeMap : Impl α (fun _ => β)
+  range : Roo α
+
+public abbrev RooSlice α β [Ord α] := Slice (RooSliceData α β)
+
+public instance {α : Type u} {β : Type v} [Ord α] : Roo.Sliceable (Impl α (fun _ => β)) α (RooSlice α β) where
+  mkSlice carrier range := ⟨carrier, range⟩
+
+public instance [Ord α] {s : RooSlice α β} : ToIterator s Id (α × β) := by
+  apply ToIterator.of
+  . exact (⟨RxoIterator.mk (Zipper.prependMapGT s.1.treeMap s.1.range.lower .done) s.1.range.upper⟩ : Iter ((_ : α) × β)).map fun e => (e.1, e.2)
+
+public theorem toList_roo {α : Type u} {β : Type v} [Ord α] [TransOrd α] (t : Impl α (fun _ => β))
+    (ordered : t.Ordered) (lowerBound upperBound : α) : t[lowerBound<...<upperBound].toList = (Internal.Impl.Const.toList t).filter (fun e => (compare e.fst lowerBound).isGT ∧ (compare e.fst upperBound).isLT) := by
+  simp only [Roo.Sliceable.mkSlice, Slice.toList_eq_toList_iter, Slice.iter,
+    Slice.Internal.iter_eq_toIteratorIter, ToIterator.iter, ToIterator.iterM_eq,
+    Iter.toIter_toIterM]
+  rw [Iter.toList_map]
+  have := @toList_rooIter α (fun _ => β) _ _ t ordered lowerBound upperBound
+  rw [RooIterator] at this
+  rw [this]
+  have eq : (fun (e : (_ : α) × β) => decide ((compare e.fst lowerBound).isGT = true ∧ (compare e.fst upperBound).isLT = true)) =
+    (fun (e : α × β) => decide ((compare e.fst lowerBound).isGT = true ∧ (compare e.fst upperBound).isLT = true)) ∘ (fun e => (e.1, e.2)) := by congr
+  conv =>
+    lhs
+    rhs
+    rw [eq]
+  rw [← List.filter_map]
+  congr
+  rw [Impl.Const.toList_eq_toListModel_map, Impl.toList_eq_toListModel]
+
+end Const
+
+
 section Roc
 
 @[always_inline]
@@ -1080,6 +1153,42 @@ public theorem toList_roc {α : Type u} {β : α → Type v} [Ord α] [TransOrd
 
 end Roc
 
+namespace Const
+
+public structure RocSliceData (α : Type u) (β : Type v) [Ord α] where
+  treeMap : Impl α (fun _ => β)
+  range : Roc α
+
+public abbrev RocSlice α β [Ord α] := Slice (RocSliceData α β)
+
+public instance {α : Type u} {β : Type v} [Ord α] : Roc.Sliceable (Impl α (fun _ => β)) α (RocSlice α β) where
+  mkSlice carrier range := ⟨carrier, range⟩
+
+public instance [Ord α] {s : RocSlice α β} : ToIterator s Id (α × β) := by
+  apply ToIterator.of
+  . exact (⟨RxcIterator.mk (Zipper.prependMapGT s.1.treeMap s.1.range.lower .done) s.1.range.upper⟩ : Iter ((_ : α) × β)).map fun e => (e.1, e.2)
+
+public theorem toList_roc {α : Type u} {β : Type v} [Ord α] [TransOrd α] (t : Impl α (fun _ => β))
+    (ordered : t.Ordered) (lowerBound upperBound : α) : t[lowerBound<...=upperBound].toList = (Internal.Impl.Const.toList t).filter (fun e => (compare e.fst lowerBound).isGT ∧ (compare e.fst upperBound).isLE) := by
+  simp only [Roc.Sliceable.mkSlice, Slice.toList_eq_toList_iter, Slice.iter,
+    Slice.Internal.iter_eq_toIteratorIter, ToIterator.iter, ToIterator.iterM_eq,
+    Iter.toIter_toIterM]
+  rw [Iter.toList_map]
+  have := @toList_rocIter α (fun _ => β) _ _ t ordered lowerBound upperBound
+  rw [RocIterator] at this
+  rw [this]
+  have eq : (fun (e : (_ : α) × β) => decide ((compare e.fst lowerBound).isGT = true ∧ (compare e.fst upperBound).isLE = true)) =
+    (fun (e : α × β) => decide ((compare e.fst lowerBound).isGT = true ∧ (compare e.fst upperBound).isLE = true)) ∘ (fun e => (e.1, e.2)) := by congr
+  conv =>
+    lhs
+    rhs
+    rw [eq]
+  rw [← List.filter_map]
+  congr
+  rw [Impl.Const.toList_eq_toListModel_map, Impl.toList_eq_toListModel]
+
+end Const
+
 section Rci
 
 @[always_inline]
@@ -1201,6 +1310,42 @@ public theorem toList_roi {α : Type u} {β : α → Type v} [Ord α] [TransOrd
 
 end Roi
 
+namespace Const
+
+public structure RoiSliceData (α : Type u) (β : Type v) [Ord α] where
+  treeMap : Impl α (fun _ => β)
+  range : Roi α
+
+public abbrev RoiSlice α β [Ord α] := Slice (RoiSliceData α β)
+
+public instance {α : Type u} {β : Type v} [Ord α] : Roi.Sliceable (Impl α (fun _ => β)) α (RoiSlice α β) where
+  mkSlice carrier range := ⟨carrier, range⟩
+
+public instance [Ord α] {s : RoiSlice α β} : ToIterator s Id (α × β) := by
+  apply ToIterator.of
+  . exact (⟨(Zipper.prependMapGT s.1.treeMap s.1.range.lower .done)⟩ : Iter ((_ : α) × β)).map fun e => (e.1, e.2)
+
+public theorem toList_roi {α : Type u} {β : Type v} [Ord α] [TransOrd α] (t : Impl α (fun _ => β))
+    (ordered : t.Ordered) (lowerBound : α) : t[lowerBound<...*].toList = (Internal.Impl.Const.toList t).filter (fun e => (compare e.fst lowerBound).isGT) := by
+  simp only [Roi.Sliceable.mkSlice, Slice.toList_eq_toList_iter, Slice.iter,
+    Slice.Internal.iter_eq_toIteratorIter, ToIterator.iter, ToIterator.iterM_eq,
+    Iter.toIter_toIterM]
+  rw [Iter.toList_map]
+  have := @toList_roiIter α (fun _ => β) _ _ t ordered lowerBound
+  rw [RoiIterator] at this
+  rw [this]
+  have eq : (fun (e : (_ : α) × β) => ((compare e.fst lowerBound).isGT)) = ((fun (e : α × β) => ((compare e.fst lowerBound).isGT)) ∘ (fun e => (e.1,e.2))) := by congr
+  conv =>
+    lhs
+    rhs
+    rw [eq]
+  rw [← List.filter_map]
+  congr
+  rw [Impl.Const.toList_eq_toListModel_map, Impl.toList_eq_toListModel]
+
+end Const
+
+
 section Rii
 
 public def RiiIterator (t : Impl α β) : Iter (α := Zipper α β) ((a : α) × β a) :=

src/Std/Data/TreeMap/Raw/Slice.lean

@@ -68,43 +68,47 @@ public theorem toList_rco {α : Type u} {β : Type v} (cmp : α → α → Order
   apply @DTreeMap.Internal.Const.toList_rco _ _ ⟨cmp⟩ _ _
   . exact @wf.out.out.ordered _ _ ⟨cmp⟩ _
 
--- public instance {α : Type u} {β : α → Type v} (cmp : α → α → Ordering := by exact compare) :
---     Rcc.Sliceable (Raw α β cmp) α (@Internal.RccSlice α β ⟨cmp⟩) :=
---   letI _ : Ord α := ⟨cmp⟩; ⟨fun carrier range => ⟨carrier.inner, range⟩⟩
-
--- public theorem toList_rcc {α : Type u} {β : α → Type v} (cmp : α → α → Ordering := by exact compare)
---     [TransCmp cmp] {t : Raw α β cmp} {wf : t.WF} {lowerBound upperBound : α} :
---     t[lowerBound...=upperBound].toList =
---       t.toList.filter (fun e => (cmp e.fst lowerBound).isGE ∧ (cmp e.fst upperBound).isLE) :=
---   @Internal.toList_rcc α β ⟨cmp⟩ _ t.inner (@wf.out.ordered α β ⟨cmp⟩ _) lowerBound upperBound
-
--- public instance {α : Type u} {β : α → Type v} (cmp : α → α → Ordering := by exact compare) :
---     Roi.Sliceable (Raw α β cmp) α (@Internal.RoiSlice α β ⟨cmp⟩) :=
---   letI _ : Ord α := ⟨cmp⟩; ⟨fun carrier range => ⟨carrier.inner, range⟩⟩
-
--- public theorem toList_roi {α : Type u} {β : α → Type v} (cmp : α → α → Ordering := by exact compare)
---     [TransCmp cmp] {t : Raw α β cmp} {wf : t.WF} {bound: α} : t[bound<...*].toList =
---       t.toList.filter (fun e => (cmp e.fst bound).isGT) :=
---   @Internal.toList_roi α β ⟨cmp⟩ _ t.inner (@wf.out.ordered α β ⟨cmp⟩ _) bound
-
--- public instance {α : Type u} {β : α → Type v} (cmp : α → α → Ordering := by exact compare) :
---     Roc.Sliceable (Raw α β cmp) α (@Internal.RocSlice α β ⟨cmp⟩) :=
---   letI _ : Ord α := ⟨cmp⟩; ⟨fun carrier range => ⟨carrier.inner, range⟩⟩
-
--- public theorem toList_roc {α : Type u} {β : α → Type v} (cmp : α → α → Ordering := by exact compare)
---     [TransCmp cmp] {t : Raw α β cmp} {wf : t.WF} {lowerBound upperBound : α} :
---     t[lowerBound<...=upperBound].toList =
---       t.toList.filter (fun e => (cmp e.fst lowerBound).isGT ∧ (cmp e.fst upperBound).isLE) :=
---   @Internal.toList_roc α β ⟨cmp⟩ _ t.inner (@wf.out.ordered α β ⟨cmp⟩ _) lowerBound upperBound
-
--- public instance {α : Type u} {β : α → Type v} (cmp : α → α → Ordering := by exact compare) :
---     Roo.Sliceable (Raw α β cmp) α (@Internal.RooSlice α β ⟨cmp⟩) :=
---   letI _ : Ord α := ⟨cmp⟩; ⟨fun carrier range => ⟨carrier.inner, range⟩⟩
-
--- public theorem toList_roo {α : Type u} {β : α → Type v} (cmp : α → α → Ordering := by exact compare)
---     [TransCmp cmp] {t : Raw α β cmp} {wf : t.WF} {lowerBound upperBound : α} :
---     t[lowerBound<...upperBound].toList =
---       t.toList.filter (fun e => (cmp e.fst lowerBound).isGT ∧ (cmp e.fst upperBound).isLT) :=
---   @Internal.toList_roo α β ⟨cmp⟩ _ t.inner (@wf.out.ordered α β ⟨cmp⟩ _) lowerBound upperBound
+public instance {α : Type u} {β : Type v} (cmp : α → α → Ordering := by exact compare) :
+    Rcc.Sliceable (Raw α β cmp) α (@DTreeMap.Internal.Const.RccSlice α β ⟨cmp⟩) :=
+  letI _ : Ord α := ⟨cmp⟩; ⟨fun carrier range => ⟨carrier.inner.inner, range⟩⟩
+
+public theorem toList_rcc {α : Type u} {β : Type v} (cmp : α → α → Ordering := by exact compare)
+    [TransCmp cmp] {t : Raw α β cmp} {wf : t.WF} {lowerBound upperBound : α} :
+    t[lowerBound...=upperBound].toList =
+      t.toList.filter (fun e => (cmp e.fst lowerBound).isGE ∧ (cmp e.fst upperBound).isLE) := by
+  apply @DTreeMap.Internal.Const.toList_rcc _ _ ⟨cmp⟩ _ _
+  . exact @wf.out.out.ordered _ _ ⟨cmp⟩ _
+
+public instance {α : Type u} {β : Type v} (cmp : α → α → Ordering := by exact compare) :
+    Roi.Sliceable (Raw α β cmp) α (@DTreeMap.Internal.Const.RoiSlice α β ⟨cmp⟩) :=
+  letI _ : Ord α := ⟨cmp⟩; ⟨fun carrier range => ⟨carrier.inner.inner, range⟩⟩
+
+public theorem toList_roi {α : Type u} {β : Type v} (cmp : α → α → Ordering := by exact compare)
+    [TransCmp cmp] {t : Raw α β cmp} {wf : t.WF} {bound: α} : t[bound<...*].toList =
+      t.toList.filter (fun e => (cmp e.fst bound).isGT) := by
+  apply @DTreeMap.Internal.Const.toList_roi _ _ ⟨cmp⟩ _
+  . exact @wf.out.out.ordered _ _ ⟨cmp⟩ _
+
+public instance {α : Type u} {β : Type v} (cmp : α → α → Ordering := by exact compare) :
+    Roc.Sliceable (Raw α β cmp) α (@DTreeMap.Internal.Const.RocSlice α β ⟨cmp⟩) :=
+  letI _ : Ord α := ⟨cmp⟩; ⟨fun carrier range => ⟨carrier.inner.inner, range⟩⟩
+
+public theorem toList_roc {α : Type u} {β : Type v} (cmp : α → α → Ordering := by exact compare)
+    [TransCmp cmp] {t : Raw α β cmp} {wf : t.WF} {lowerBound upperBound : α} :
+    t[lowerBound<...=upperBound].toList =
+      t.toList.filter (fun e => (cmp e.fst lowerBound).isGT ∧ (cmp e.fst upperBound).isLE) := by
+  apply @DTreeMap.Internal.Const.toList_roc _ _ ⟨cmp⟩ _
+  . exact @wf.out.out.ordered _ _ ⟨cmp⟩ _
+
+public instance {α : Type u} {β : Type v} (cmp : α → α → Ordering := by exact compare) :
+    Roo.Sliceable (Raw α β cmp) α (@DTreeMap.Internal.Const.RooSlice α β ⟨cmp⟩) :=
+  letI _ : Ord α := ⟨cmp⟩; ⟨fun carrier range => ⟨carrier.inner.inner, range⟩⟩
+
+public theorem toList_roo {α : Type u} {β : Type v} (cmp : α → α → Ordering := by exact compare)
+    [TransCmp cmp] {t : Raw α β cmp} {wf : t.WF} {lowerBound upperBound : α} :
+    t[lowerBound<...upperBound].toList =
+      t.toList.filter (fun e => (cmp e.fst lowerBound).isGT ∧ (cmp e.fst upperBound).isLT) := by
+  apply @DTreeMap.Internal.Const.toList_roo _ _ ⟨cmp⟩ _
+  . exact @wf.out.out.ordered _ _ ⟨cmp⟩ _
 
 end Std.TreeMap.Raw