feat: TreeMap iterators

[datokrat]

Plan of attack:

• Mostly implement slices and their iterators for Roc- and Rcc-based slices and characterize them in terms of toList for DTreeMap
• Prove the required lemmas about getEntryGE? and getEntryGT?
• Prove the two iterator-independent sorryed lemmas in Std.Data.DTreeMap.Slice
• Fill in the two sorryed proofs about
• Clean up, perhaps add other essential lemmas
• Implement Ric-based slices and all the other shapes by copy-pasting and slightly modifying (the ubiquitous match expressions make automation difficult, at least for the lower-level theorems!)
• Implement slices for TreeMap and TreeSet as wrappers around DTreeMap slices (and potentially provide key/value iterators where possible?)

Open questions/future work:

• Do we need/want slices and iterators for the raw versions? It's a bit unclear where the well-formedness proof could be supplied to the slice, and that proof is needed in order to prove the iterator finite.. I would prefer to have a way of promoting a raw map to a bundled one.
• The current implementation makes a getEntryGT? call on each step. It might be more efficient to use a zipper. Using a zipper would also allow for finite iterators on raw tree maps, I guess.

[Rob23oba]

Here also an idea for how you could work with a list-like, zipper-ish iterator:

Inductive map iterator

import Std

namespace Std.DTreeMap.Internal.Impl

open Std.Iterators

inductive MapIterator (α : Type u) (β : α → Type v) where
  | done
  | cons (k : α) (v : β k) (tree : Impl α β) (next : MapIterator α β)

-- `cmp` is something like `compare k`
def MapIterator.prependMapGE (t : Impl α β) (cmp : α → Ordering) (it : MapIterator α β) : MapIterator α β :=
  match t with
  | .leaf => it
  | .inner _ k v l r =>
    match cmp k with
    | .lt => prependMapGE l cmp (.cons k v r it)
    | .eq => .cons k v r it
    | .gt => prependMapGE r cmp it

def MapIterator.prependMap : Impl α β → MapIterator α β → MapIterator α β
  | .leaf, it => it
  | .inner _ k v l r, it => prependMap l (.cons k v r it)

@[inline]
def MapIterator.step : MapIterator α β → IterStep (IterM (α := MapIterator α β) Id ((a : α) × β a)) ((a : α) × β a)
  | .done => .done
  | .cons k v t it => .yield ⟨it.prependMap t⟩ ⟨k, v⟩

instance : Iterator (MapIterator α β) Id ((a : α) × β a) where
  IsPlausibleStep it step := it.internalState.step = step
  step it := ⟨it.internalState.step, rfl⟩

def iterGE (t : Impl α β) (cmp : α → Ordering) : IterM (α := MapIterator α β) Id ((a : α) × β a) :=
  ⟨MapIterator.prependMapGE t cmp .done⟩

def test : Impl Nat fun _ => Nat :=
  .ofList [⟨1, 2⟩, ⟨5, 4⟩, ⟨3, 1⟩, ⟨2, 8⟩, ⟨7, 9⟩, ⟨10, 5⟩]

instance [Monad n] : IteratorCollectPartial (MapIterator α β) Id n := .defaultImplementation

#eval (test.iterGE (compare 5)).allowNontermination.toList

[datokrat]

Thanks, @Rob23oba -- @wkrozowski is working on a zipper-based solution in #10776 now, so I'll close this PR.