Lemmas relating operations on well-formed size-bounded trees to operations on lists

This file contains lemmas that relate Impl.toListModel to the queries and operations on Impl. The Impl.Ordered property, being defined in terms of Impl.toListModel, is then shown to be preserved by all of the operations.

However, this file does not contain lemmas that relate operations besides Impl.toListModel to each other or themselves. Such proofs crucially build on top of the lemmas in this file and can be found in Std.Data.Internal.Lemmas.

def Std.DTreeMap.Internal.Impl.instCoeTypeForall_1 {α : Type u} : Coe (Type v) (α → Type v)

Equations

• Std.DTreeMap.Internal.Impl.instCoeTypeForall_1 = { coe := fun (γ : Type ?u.10) (x : α) => γ }

toListModel for balancing operations

@[simp]

theorem Std.DTreeMap.Internal.Impl.toListModel_singleL {α : Type u} {β : α → Type v} {k : α} {v : β k} {l : Impl α β} {rk : α} {rv : β rk} {rl rr : Impl α β} : (singleL k v l rk rv rl rr).toListModel = l.toListModel ++ ⟨k, v⟩ :: (rl.toListModel ++ ⟨rk, rv⟩ :: rr.toListModel)

@[simp]

theorem Std.DTreeMap.Internal.Impl.toListModel_singleR {α : Type u} {β : α → Type v} {k : α} {v : β k} {lk : α} {lv : β lk} {ll lr r : Impl α β} : (singleR k v lk lv ll lr r).toListModel = ll.toListModel ++ ⟨lk, lv⟩ :: lr.toListModel ++ ⟨k, v⟩ :: r.toListModel

@[simp]

theorem Std.DTreeMap.Internal.Impl.toListModel_rotateL {α : Type u} {β : α → Type v} {k : α} {v : β k} {l : Impl α β} {rk : α} {rv : β rk} {rl rr : Impl α β} : (rotateL k v l rk rv rl rr).toListModel = l.toListModel ++ ⟨k, v⟩ :: (rl.toListModel ++ ⟨rk, rv⟩ :: rr.toListModel)

@[simp]

theorem Std.DTreeMap.Internal.Impl.toListModel_rotateR {α : Type u} {β : α → Type v} {k : α} {v : β k} {lk : α} {lv : β lk} {ll lr r : Impl α β} : (rotateR k v lk lv ll lr r).toListModel = ll.toListModel ++ ⟨lk, lv⟩ :: lr.toListModel ++ ⟨k, v⟩ :: r.toListModel

@[simp]

theorem Std.DTreeMap.Internal.Impl.toListModel_balanceₘ {α : Type u} {β : α → Type v} {k : α} {v : β k} {l r : Impl α β} : (balanceₘ k v l r).toListModel = l.toListModel ++ ⟨k, v⟩ :: r.toListModel

@[simp]

theorem Std.DTreeMap.Internal.Impl.toListModel_balance {α : Type u} {β : α → Type v} {k : α} {v : β k} {l r : Impl α β} {hlb : l.Balanced} {hrb : r.Balanced} {hlr : BalanceLErasePrecond l.size r.size ∨ BalanceLErasePrecond r.size l.size} : (balance k v l r hlb hrb hlr).toListModel = l.toListModel ++ ⟨k, v⟩ :: r.toListModel

@[simp]

theorem Std.DTreeMap.Internal.Impl.toListModel_balanceL {α : Type u} {β : α → Type v} {k : α} {v : β k} {l r : Impl α β} {hlb : l.Balanced} {hrb : r.Balanced} {hlr : BalanceLPrecond l.size r.size} : (balanceL k v l r hlb hrb hlr).toListModel = l.toListModel ++ ⟨k, v⟩ :: r.toListModel

@[simp]

theorem Std.DTreeMap.Internal.Impl.toListModel_balanceLErase {α : Type u} {β : α → Type v} {k : α} {v : β k} {l r : Impl α β} {hlb : l.Balanced} {hrb : r.Balanced} {hlr : BalanceLErasePrecond l.size r.size} : (balanceLErase k v l r hlb hrb hlr).toListModel = l.toListModel ++ ⟨k, v⟩ :: r.toListModel

@[simp]

theorem Std.DTreeMap.Internal.Impl.toListModel_balanceR {α : Type u} {β : α → Type v} {k : α} {v : β k} {l r : Impl α β} {hlb : l.Balanced} {hrb : r.Balanced} {hlr : BalanceLPrecond r.size l.size} : (balanceR k v l r hlb hrb hlr).toListModel = l.toListModel ++ ⟨k, v⟩ :: r.toListModel

@[simp]

theorem Std.DTreeMap.Internal.Impl.toListModel_balanceRErase {α : Type u} {β : α → Type v} {k : α} {v : β k} {l r : Impl α β} {hlb : l.Balanced} {hrb : r.Balanced} {hlr : BalanceLErasePrecond r.size l.size} : (balanceRErase k v l r hlb hrb hlr).toListModel = l.toListModel ++ ⟨k, v⟩ :: r.toListModel

@[simp]

theorem Std.DTreeMap.Internal.Impl.toListModel_minView {α : Type u} {β : α → Type v} {k : α} {v : β k} {l r : Impl α β} {hl : l.Balanced} {hr : r.Balanced} {hlr : BalancedAtRoot l.size r.size} : ⟨(minView k v l r hl hr hlr).k, (minView k v l r hl hr hlr).v⟩ :: (minView k v l r hl hr hlr).tree.impl.toListModel = l.toListModel ++ ⟨k, v⟩ :: r.toListModel

@[simp]

theorem Std.DTreeMap.Internal.Impl.toListModel_maxView {α : Type u} {β : α → Type v} {k : α} {v : β k} {l r : Impl α β} {hl : l.Balanced} {hr : r.Balanced} {hlr : BalancedAtRoot l.size r.size} : (maxView k v l r hl hr hlr).tree.impl.toListModel ++ [⟨(maxView k v l r hl hr hlr).k, (maxView k v l r hl hr hlr).v⟩] = l.toListModel ++ ⟨k, v⟩ :: r.toListModel

@[simp]

theorem Std.DTreeMap.Internal.Impl.toListModel_glue {α : Type u} {β : α → Type v} {l r : Impl α β} {hl : l.Balanced} {hr : r.Balanced} {hlr : BalancedAtRoot l.size r.size} : (l.glue r hl hr hlr).toListModel = l.toListModel ++ r.toListModel

@[simp, irreducible]

theorem Std.DTreeMap.Internal.Impl.toListModel_link2 {α : Type u} {β : α → Type v} [Ord α] {l r : Impl α β} {hl : l.Balanced} {hr : r.Balanced} : (l.link2 r hl hr).impl.toListModel = l.toListModel ++ r.toListModel

@[simp]

theorem Std.DTreeMap.Internal.Impl.toListModel_insertMin {α : Type u} {β : α → Type v} [Ord α] {k : α} {v : β k} {t : Impl α β} {h : t.Balanced} : (insertMin k v t h).impl.toListModel = ⟨k, v⟩ :: t.toListModel

@[simp]

theorem Std.DTreeMap.Internal.Impl.toListModel_insertMax {α : Type u} {β : α → Type v} [Ord α] {k : α} {v : β k} {t : Impl α β} {h : t.Balanced} : (insertMax k v t h).impl.toListModel = t.toListModel ++ [⟨k, v⟩]

@[simp, irreducible]

theorem Std.DTreeMap.Internal.Impl.toListModel_link {α : Type u} {β : α → Type v} [Ord α] {k : α} {v : β k} {l r : Impl α β} {hl : l.Balanced} {hr : r.Balanced} : (link k v l r hl hr).impl.toListModel = l.toListModel ++ ⟨k, v⟩ :: r.toListModel

Verification of model functions

theorem Std.DTreeMap.Internal.Impl.toListModel_filter_gt_of_gt {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] {k : α → Ordering} [Internal.IsStrictCut compare k] {sz : Nat} {k' : α} {v' : β k'} {l r : Impl α β} (hcmp : k k' = Ordering.gt) (ho : (inner sz k' v' l r).Ordered) : List.filter (fun (x : (a : α) × β a) => k x.fst == Ordering.gt) (inner sz k' v' l r).toListModel = l.toListModel ++ ⟨k', v'⟩ :: List.filter (fun (x : (a : α) × β a) => k x.fst == Ordering.gt) r.toListModel

theorem Std.DTreeMap.Internal.Impl.toListModel_filter_gt_of_eq {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] {k : α → Ordering} [Internal.IsStrictCut compare k] {sz : Nat} {k' : α} {v' : β k'} {l r : Impl α β} (hcmp : k k' = Ordering.eq) (ho : (inner sz k' v' l r).Ordered) : List.filter (fun (x : (a : α) × β a) => k x.fst == Ordering.gt) (inner sz k' v' l r).toListModel = l.toListModel

theorem Std.DTreeMap.Internal.Impl.toListModel_filter_gt_of_lt {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] {k : α → Ordering} [Internal.IsStrictCut compare k] {sz : Nat} {k' : α} {v' : β k'} {l r : Impl α β} (hcmp : k k' = Ordering.lt) (ho : (inner sz k' v' l r).Ordered) : List.filter (fun (x : (a : α) × β a) => k x.fst == Ordering.gt) (inner sz k' v' l r).toListModel = List.filter (fun (x : (a : α) × β a) => k x.fst == Ordering.gt) l.toListModel

theorem Std.DTreeMap.Internal.Impl.toListModel_find?_of_gt {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] {k : α → Ordering} [Internal.IsStrictCut compare k] {sz : Nat} {k' : α} {v' : β k'} {l r : Impl α β} (hcmp : k k' = Ordering.gt) (ho : (inner sz k' v' l r).Ordered) : List.find? (fun (x : (a : α) × β a) => k x.fst == Ordering.eq) (inner sz k' v' l r).toListModel = List.find? (fun (x : (a : α) × β a) => k x.fst == Ordering.eq) r.toListModel

theorem Std.DTreeMap.Internal.Impl.toListModel_find?_of_eq {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] {k : α → Ordering} [Internal.IsStrictCut compare k] {sz : Nat} {k' : α} {v' : β k'} {l r : Impl α β} (hcmp : k k' = Ordering.eq) (ho : (inner sz k' v' l r).Ordered) : List.find? (fun (x : (a : α) × β a) => k x.fst == Ordering.eq) (inner sz k' v' l r).toListModel = some ⟨k', v'⟩

theorem Std.DTreeMap.Internal.Impl.toListModel_find?_of_lt {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] {k : α → Ordering} [Internal.IsCut compare k] {sz : Nat} {k' : α} {v' : β k'} {l r : Impl α β} (hcmp : k k' = Ordering.lt) (ho : (inner sz k' v' l r).Ordered) : List.find? (fun (x : (a : α) × β a) => k x.fst == Ordering.eq) (inner sz k' v' l r).toListModel = List.find? (fun (x : (a : α) × β a) => k x.fst == Ordering.eq) l.toListModel

theorem Std.DTreeMap.Internal.Impl.toListModel_filter_lt_of_gt {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] {k : α → Ordering} [Internal.IsCut compare k] {sz : Nat} {k' : α} {v' : β k'} {l r : Impl α β} (hcmp : k k' = Ordering.gt) (ho : (inner sz k' v' l r).Ordered) : List.filter (fun (x : (a : α) × β a) => k x.fst == Ordering.lt) (inner sz k' v' l r).toListModel = List.filter (fun (x : (a : α) × β a) => k x.fst == Ordering.lt) r.toListModel

theorem Std.DTreeMap.Internal.Impl.toListModel_filter_lt_of_eq {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] {k : α → Ordering} [Internal.IsStrictCut compare k] {sz : Nat} {k' : α} {v' : β k'} {l r : Impl α β} (hcmp : k k' = Ordering.eq) (ho : (inner sz k' v' l r).Ordered) : List.filter (fun (x : (a : α) × β a) => k x.fst == Ordering.lt) (inner sz k' v' l r).toListModel = r.toListModel

theorem Std.DTreeMap.Internal.Impl.toListModel_filter_lt_of_lt {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] {k : α → Ordering} [Internal.IsCut compare k] {sz : Nat} {k' : α} {v' : β k'} {l r : Impl α β} (hcmp : k k' = Ordering.lt) (ho : (inner sz k' v' l r).Ordered) : List.filter (fun (x : (a : α) × β a) => k x.fst == Ordering.lt) (inner sz k' v' l r).toListModel = List.filter (fun (x : (a : α) × β a) => k x.fst == Ordering.lt) l.toListModel ++ ⟨k', v'⟩ :: r.toListModel

theorem Std.DTreeMap.Internal.Impl.findCell_of_gt {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] {k : α → Ordering} [Internal.IsStrictCut compare k] {sz : Nat} {k' : α} {v' : β k'} {l r : Impl α β} (hcmp : k k' = Ordering.gt) (ho : (inner sz k' v' l r).Ordered) : List.findCell (inner sz k' v' l r).toListModel k = List.findCell r.toListModel k

theorem Std.DTreeMap.Internal.Impl.findCell_of_eq {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] {k : α → Ordering} [Internal.IsStrictCut compare k] {sz : Nat} {k' : α} {v' : β k'} {l r : Impl α β} (hcmp : k k' = Ordering.eq) (ho : (inner sz k' v' l r).Ordered) : List.findCell (inner sz k' v' l r).toListModel k = Cell.ofEq k' v' ⋯

theorem Std.DTreeMap.Internal.Impl.findCell_of_lt {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] {k : α → Ordering} [Internal.IsCut compare k] {sz : Nat} {k' : α} {v' : β k'} {l r : Impl α β} (hcmp : k k' = Ordering.lt) (ho : (inner sz k' v' l r).Ordered) : List.findCell (inner sz k' v' l r).toListModel k = List.findCell l.toListModel k

theorem Std.DTreeMap.Internal.Impl.toListModel_updateCell {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] {k : α} {f : Cell α β (compare k) → Cell α β (compare k)} {l : Impl α β} (hlb : l.Balanced) (hlo : l.Ordered) : (updateCell k f l hlb).impl.toListModel = List.filter (fun (x : (a : α) × β a) => compare k x.fst == Ordering.gt) l.toListModel ++ (f (List.findCell l.toListModel (compare k))).inner.toList ++ List.filter (fun (x : (a : α) × β a) => compare k x.fst == Ordering.lt) l.toListModel

theorem Std.DTreeMap.Internal.Impl.toListModel_eq_append {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] (k : α → Ordering) [Internal.IsStrictCut compare k] {l : Impl α β} (ho : l.Ordered) : l.toListModel = List.filter (fun (x : (a : α) × β a) => k x.fst == Ordering.gt) l.toListModel ++ (List.find? (fun (x : (a : α) × β a) => k x.fst == Ordering.eq) l.toListModel).toList ++ List.filter (fun (x : (a : α) × β a) => k x.fst == Ordering.lt) l.toListModel

theorem Std.DTreeMap.Internal.Impl.ordered_updateCell {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] {k : α} {f : Cell α β (compare k) → Cell α β (compare k)} {l : Impl α β} (hlb : l.Balanced) (hlo : l.Ordered) : (updateCell k f l hlb).impl.Ordered

Connecting the tree maps machinery to the hash map machinery

theorem Std.DTreeMap.Internal.Impl.exists_cell_of_updateCell {α : Type u} {β : α → Type v} [BEq α] [Ord α] [TransOrd α] [LawfulBEqOrd α] (l : Impl α β) (hlb : l.Balanced) (hlo : l.Ordered) (k : α) (f : Cell α β (compare k) → Cell α β (compare k)) : ∃ (l' : List ((a : α) × β a)), l.toListModel.Perm ((List.find? (fun (x : (a : α) × β a) => compare k x.fst == Ordering.eq) l.toListModel).toList ++ l') ∧ (updateCell k f l hlb).impl.toListModel.Perm ((f (List.findCell l.toListModel (compare k))).inner.toList ++ l') ∧ Internal.List.containsKey k l' = false

theorem Std.DTreeMap.Internal.Impl.Ordered.distinctKeys {α : Type u} {β : α → Type v} [BEq α] [Ord α] [LawfulBEqOrd α] {l : Impl α β} (h : l.Ordered) : Internal.List.DistinctKeys l.toListModel

theorem Std.DTreeMap.Internal.Impl.toListModel_updateCell_perm {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : Impl α β} (hlb : l.Balanced) (hlo : l.Ordered) {k : α} {f : Cell α β (compare k) → Cell α β (compare k)} {g : List ((a : α) × β a) → List ((a : α) × β a)} (hfg : ∀ {c : Cell α β (compare k)}, (f c).inner.toList = g c.inner.toList) (hg₁ : ∀ {l l' : List ((a : α) × β a)}, Internal.List.DistinctKeys l → l.Perm l' → (g l).Perm (g l')) (hg₂ : ∀ {l l' : List ((a : α) × β a)}, Internal.List.containsKey k l' = false → g (l ++ l') = g l ++ l') : (updateCell k f l hlb).impl.toListModel.Perm (g l.toListModel)

This is the general theorem to show that modification operations are correct.

theorem Std.DTreeMap.Internal.Impl.contains_findCell {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] {k : α → Ordering} [Internal.IsStrictCut compare k] {l : Impl α β} (hlo : l.Ordered) (h : contains' k l = true) : (List.findCell l.toListModel k).contains = true

theorem Std.DTreeMap.Internal.Impl.applyPartition_eq {α : Type u} {β : α → Type v} {δ : Type w} [Ord α] [TransOrd α] {k : α → Ordering} [Internal.IsStrictCut compare k] {l : Impl α β} {f : List ((a : α) × β a) → (c : Cell α β k) → (contains' k l = true → c.contains = true) → List ((a : α) × β a) → δ} (hlo : l.Ordered) : applyPartition k l f = f (List.filter (fun (x : (a : α) × β a) => k x.fst == Ordering.gt) l.toListModel) (List.findCell l.toListModel k) ⋯ (List.filter (fun (x : (a : α) × β a) => k x.fst == Ordering.lt) l.toListModel)

theorem Std.DTreeMap.Internal.Impl.containsKey_toListModel {α : Type u} {β : α → Type v} [Ord α] [OrientedOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {l : Impl α β} (h : contains' (compare k) l = true) : Internal.List.containsKey k l.toListModel = true

theorem Std.DTreeMap.Internal.Impl.applyPartition_eq_apply_toListModel {α : Type u} {β : α → Type v} {δ : Type w} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {l : Impl α β} (hlo : l.Ordered) {f : List ((a : α) × β a) → (c : Cell α β (compare k)) → (contains' (compare k) l = true → c.contains = true) → List ((a : α) × β a) → δ} (g : (ll : List ((a : α) × β a)) → (contains' (compare k) l = true → Internal.List.containsKey k ll = true) → δ) (h : ∀ {ll rr : List ((a : α) × β a)} {c : Cell α β (compare k)} {h₁ : contains' (compare k) l = true → c.contains = true}, List.Pairwise (fun (a b : (a : α) × β a) => compare a.fst b.fst = Ordering.lt) (ll ++ c.inner.toList ++ rr) → (∀ (p : (a : α) × β a), p ∈ ll → compare k p.fst = Ordering.gt) → (∀ (p : (a : α) × β a), p ∈ rr → compare k p.fst = Ordering.lt) → f ll c h₁ rr = g (ll ++ c.inner.toList ++ rr) ⋯) : applyPartition (compare k) l f = g l.toListModel ⋯

theorem Std.DTreeMap.Internal.Impl.applyPartition_eq_apply_toListModel' {α : Type u} {β : α → Type v} {δ : Type w} [Ord α] [TransOrd α] {k : α → Ordering} [Internal.IsStrictCut compare k] {l : Impl α β} (hlo : l.Ordered) {f : List ((a : α) × β a) → (c : Cell α β k) → (contains' k l = true → c.contains = true) → List ((a : α) × β a) → δ} (g : List ((a : α) × β a) → δ) (h : ∀ {ll rr : List ((a : α) × β a)} {c : Cell α β k} {h₁ : contains' k l = true → c.contains = true}, List.Pairwise (fun (a b : (a : α) × β a) => compare a.fst b.fst = Ordering.lt) (ll ++ c.inner.toList ++ rr) → (∀ (p : (a : α) × β a), p ∈ ll → k p.fst = Ordering.gt) → (∀ (p : (a : α) × β a), p ∈ rr → k p.fst = Ordering.lt) → f ll c h₁ rr = g (ll ++ c.inner.toList ++ rr)) : applyPartition k l f = g l.toListModel

theorem Std.DTreeMap.Internal.Impl.applyCell_eq_apply_toListModel {α : Type u} {β : α → Type v} {δ : Type w} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {l : Impl α β} (hlo : l.Ordered) {f : (c : Cell α β (compare k)) → (contains' (compare k) l = true → c.contains = true) → δ} (g : (ll : List ((a : α) × β a)) → (contains' (compare k) l = true → Internal.List.containsKey k ll = true) → δ) (hfg : ∀ (c : Cell α β (compare k)) (hc : contains' (compare k) l = true → c.contains = true), f c hc = g c.inner.toList ⋯) (hg₁ : ∀ (l₁ l₂ : List ((a : α) × β a)) (h : contains' (compare k) l = true → Internal.List.containsKey k l₁ = true), Internal.List.DistinctKeys l₁ → ∀ (hP : l₁.Perm l₂), g l₁ h = g l₂ ⋯) (hg : ∀ (l₁ l₂ : List ((a : α) × β a)) (h : contains' (compare k) l = true → Internal.List.containsKey k (l₁ ++ l₂) = true) (h' : Internal.List.containsKey k l₂ = false), g (l₁ ++ l₂) h = g l₁ ⋯) : applyCell k l f = g l.toListModel ⋯

Verification of access operations

Equiv

theorem Std.DTreeMap.Internal.Impl.equiv_iff_toListModel_perm {α : Type u} {β : α → Type v} {t t' : Impl α β} : t.Equiv t' ↔ t.toListModel.Perm t'.toListModel

theorem Std.DTreeMap.Internal.Impl.Equiv.toListModel_eq {α : Type u} {β : α → Type v} [Ord α] [OrientedOrd α] {t t' : Impl α β} (h : t.Equiv t') (htb : t.Ordered) (htb' : t'.Ordered) : t.toListModel = t'.toListModel

isEmpty

theorem Std.DTreeMap.Internal.Impl.isEmpty_eq_isEmpty {α : Type u} {β : α → Type v} {t : Impl α β} : t.isEmpty = t.toListModel.isEmpty

size

theorem Std.DTreeMap.Internal.Impl.size_eq_length {α : Type u} {β : α → Type v} (t : Impl α β) (htb : t.Balanced) : t.size = t.toListModel.length

contains

theorem Std.DTreeMap.Internal.Impl.containsₘ_eq_containsKey {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {l : Impl α β} (hlo : l.Ordered) : l.containsₘ k = Internal.List.containsKey k l.toListModel

theorem Std.DTreeMap.Internal.Impl.contains_eq_containsKey {α : Type u} {β : α → Type v} [instBEq : BEq α] [Ord α] [LawfulBEqOrd α] [TransOrd α] {k : α} {l : Impl α β} (hlo : l.Ordered) : contains k l = Internal.List.containsKey k l.toListModel

get?

theorem Std.DTreeMap.Internal.Impl.get?ₘ_eq_getValueCast? {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [LawfulEqOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {t : Impl α β} (hto : t.Ordered) : t.get?ₘ k = Internal.List.getValueCast? k t.toListModel

theorem Std.DTreeMap.Internal.Impl.get?_eq_getValueCast? {α : Type u} {β : α → Type v} [instBEq : BEq α] [Ord α] [i : LawfulBEqOrd α] [TransOrd α] [LawfulEqOrd α] {k : α} {t : Impl α β} (hto : t.Ordered) : t.get? k = Internal.List.getValueCast? k t.toListModel

get

theorem Std.DTreeMap.Internal.Impl.contains_eq_isSome_get?ₘ {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [LawfulEqOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {t : Impl α β} (hto : t.Ordered) : contains k t = (t.get?ₘ k).isSome

theorem Std.DTreeMap.Internal.Impl.getₘ_eq_getValueCast {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [LawfulEqOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {t : Impl α β} (h : Internal.List.containsKey k t.toListModel = true) {h' : (t.get?ₘ k).isSome = true} (hto : t.Ordered) : t.getₘ k h' = Internal.List.getValueCast k t.toListModel h

theorem Std.DTreeMap.Internal.Impl.get_eq_getValueCast {α : Type u} {β : α → Type v} [instBEq : BEq α] [Ord α] [LawfulBEqOrd α] [TransOrd α] [LawfulEqOrd α] {k : α} {t : Impl α β} {h : k ∈ t} (hto : t.Ordered) : t.get k h = Internal.List.getValueCast k t.toListModel ⋯

get!

theorem Std.DTreeMap.Internal.Impl.get!ₘ_eq_getValueCast! {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [LawfulEqOrd α] [BEq α] [LawfulBEqOrd α] {k : α} [Inhabited (β k)] {t : Impl α β} (hto : t.Ordered) : t.get!ₘ k = Internal.List.getValueCast! k t.toListModel

theorem Std.DTreeMap.Internal.Impl.get!_eq_getValueCast! {α : Type u} {β : α → Type v} [instBEq : BEq α] [Ord α] [LawfulBEqOrd α] [TransOrd α] [LawfulEqOrd α] {k : α} [Inhabited (β k)] {t : Impl α β} (hto : t.Ordered) : t.get! k = Internal.List.getValueCast! k t.toListModel

getD

theorem Std.DTreeMap.Internal.Impl.getDₘ_eq_getValueCastD {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [LawfulEqOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {t : Impl α β} {fallback : β k} (hto : t.Ordered) : getDₘ k t fallback = Internal.List.getValueCastD k t.toListModel fallback

theorem Std.DTreeMap.Internal.Impl.getD_eq_getValueCastD {α : Type u} {β : α → Type v} [Ord α] [instBEq : BEq α] [LawfulBEqOrd α] [TransOrd α] [LawfulEqOrd α] {k : α} {t : Impl α β} {fallback : β k} (hto : t.Ordered) : t.getD k fallback = Internal.List.getValueCastD k t.toListModel fallback

getKey?

theorem Std.DTreeMap.Internal.Impl.getKey?ₘ_eq_getKey? {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {t : Impl α β} (hto : t.Ordered) : t.getKey?ₘ k = Internal.List.getKey? k t.toListModel

theorem Std.DTreeMap.Internal.Impl.getKey?_eq_getKey? {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [instBEq : BEq α] [LawfulBEqOrd α] {k : α} {t : Impl α β} (hto : t.Ordered) : t.getKey? k = Internal.List.getKey? k t.toListModel

getKey

theorem Std.DTreeMap.Internal.Impl.contains_eq_isSome_getKey?ₘ {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {t : Impl α β} (hto : t.Ordered) : contains k t = (t.getKey?ₘ k).isSome

theorem Std.DTreeMap.Internal.Impl.getKeyₘ_eq_getKey {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {t : Impl α β} (h : Internal.List.containsKey k t.toListModel = true) {h' : (t.getKey?ₘ k).isSome = true} (hto : t.Ordered) : t.getKeyₘ k h' = Internal.List.getKey k t.toListModel h

theorem Std.DTreeMap.Internal.Impl.getKey_eq_getKey {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [instBEq : BEq α] [LawfulBEqOrd α] {k : α} {t : Impl α β} {h : contains k t = true} (hto : t.Ordered) : t.getKey k h = Internal.List.getKey k t.toListModel ⋯

getKey!

theorem Std.DTreeMap.Internal.Impl.getKey!ₘ_eq_getKey! {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} [Inhabited α] {t : Impl α β} (hto : t.Ordered) : t.getKey!ₘ k = Internal.List.getKey! k t.toListModel

theorem Std.DTreeMap.Internal.Impl.getKey!_eq_getKey! {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [instBEq : BEq α] [LawfulBEqOrd α] {k : α} [Inhabited α] {t : Impl α β} (hto : t.Ordered) : t.getKey! k = Internal.List.getKey! k t.toListModel

getKeyD

theorem Std.DTreeMap.Internal.Impl.getKeyDₘ_eq_getKeyD {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {t : Impl α β} {fallback : α} (hto : t.Ordered) : getKeyDₘ k t fallback = Internal.List.getKeyD k t.toListModel fallback

theorem Std.DTreeMap.Internal.Impl.getKeyD_eq_getKeyD {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [instBEq : BEq α] [LawfulBEqOrd α] {k : α} {t : Impl α β} {fallback : α} (hto : t.Ordered) : t.getKeyD k fallback = Internal.List.getKeyD k t.toListModel fallback

get?

theorem Std.DTreeMap.Internal.Impl.Const.get?ₘ_eq_getValue? {α : Type u} {β : Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {t : Impl α fun (x : α) => β} (hto : t.Ordered) : get?ₘ t k = Internal.List.getValue? k t.toListModel

theorem Std.DTreeMap.Internal.Impl.Const.get?_eq_getValue? {α : Type u} {β : Type v} [Ord α] [TransOrd α] [instBEq : BEq α] [LawfulBEqOrd α] {k : α} {t : Impl α fun (x : α) => β} (hto : t.Ordered) : get? t k = Internal.List.getValue? k t.toListModel

get

theorem Std.DTreeMap.Internal.Impl.Const.contains_eq_isSome_get?ₘ {α : Type u} {β : Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {t : Impl α fun (x : α) => β} (hto : t.Ordered) : contains k t = (get?ₘ t k).isSome

theorem Std.DTreeMap.Internal.Impl.Const.getₘ_eq_getValue {α : Type u} {β : Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {t : Impl α fun (x : α) => β} (h : Internal.List.containsKey k t.toListModel = true) {h' : (get?ₘ t k).isSome = true} (hto : t.Ordered) : getₘ t k h' = Internal.List.getValue k t.toListModel h

theorem Std.DTreeMap.Internal.Impl.Const.get_eq_getValue {α : Type u} {β : Type v} [Ord α] [TransOrd α] [instBEq : BEq α] [LawfulBEqOrd α] {k : α} {t : Impl α fun (x : α) => β} {h : contains k t = true} (hto : t.Ordered) : get t k h = Internal.List.getValue k t.toListModel ⋯

get!

theorem Std.DTreeMap.Internal.Impl.Const.get!ₘ_eq_getValue! {α : Type u} {β : Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} [Inhabited β] {t : Impl α fun (x : α) => β} (hto : t.Ordered) : get!ₘ t k = Internal.List.getValue! k t.toListModel

theorem Std.DTreeMap.Internal.Impl.Const.get!_eq_getValue! {α : Type u} {β : Type v} [Ord α] [TransOrd α] [instBEq : BEq α] [LawfulBEqOrd α] {k : α} [Inhabited β] {t : Impl α fun (x : α) => β} (hto : t.Ordered) : get! t k = Internal.List.getValue! k t.toListModel

getD

theorem Std.DTreeMap.Internal.Impl.Const.getDₘ_eq_getValueD {α : Type u} {β : Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {t : Impl α fun (x : α) => β} {fallback : β} (hto : t.Ordered) : getDₘ t k fallback = Internal.List.getValueD k t.toListModel fallback

theorem Std.DTreeMap.Internal.Impl.Const.getD_eq_getValueD {α : Type u} {β : Type v} [Ord α] [TransOrd α] [instBEq : BEq α] [LawfulBEqOrd α] {k : α} {t : Impl α fun (x : α) => β} {fallback : β} (hto : t.Ordered) : getD t k fallback = Internal.List.getValueD k t.toListModel fallback

Verification of modification operations

empty

@[simp]

theorem Std.DTreeMap.Internal.Impl.toListModel_empty {α : Type u} {β : α → Type v} : empty.toListModel = []

theorem Std.DTreeMap.Internal.Impl.ordered_empty {α : Type u} {β : α → Type v} [Ord α] : empty.Ordered

insertₘ

theorem Std.DTreeMap.Internal.Impl.ordered_insertₘ {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] {k : α} {v : β k} {l : Impl α β} (hlb : l.Balanced) (hlo : l.Ordered) : (insertₘ k v l hlb).Ordered

theorem Std.DTreeMap.Internal.Impl.toListModel_insertₘ {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {v : β k} {l : Impl α β} (hlb : l.Balanced) (hlo : l.Ordered) : (insertₘ k v l hlb).toListModel.Perm (Internal.List.insertEntry k v l.toListModel)

insert

theorem Std.DTreeMap.Internal.Impl.ordered_insert {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] {k : α} {v : β k} {l : Impl α β} (hlb : l.Balanced) (hlo : l.Ordered) : (insert k v l hlb).impl.Ordered

theorem Std.DTreeMap.Internal.Impl.toListModel_insert {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {v : β k} {l : Impl α β} (hlb : l.Balanced) (hlo : l.Ordered) : (insert k v l hlb).impl.toListModel.Perm (Internal.List.insertEntry k v l.toListModel)

insert!

theorem Std.DTreeMap.Internal.Impl.WF.insert! {α : Type u} {β : α → Type v} {x✝ : Ord α} [TransOrd α] {k : α} {v : β k} {l : Impl α β} (h : l.WF) : (Impl.insert! k v l).WF

theorem Std.DTreeMap.Internal.Impl.toListModel_insert! {α : Type u} {β : α → Type v} [instBEq : BEq α] [Ord α] [LawfulBEqOrd α] [TransOrd α] {k : α} {v : β k} {l : Impl α β} (hlb : l.Balanced) (hlo : l.Ordered) : (insert! k v l).toListModel.Perm (Internal.List.insertEntry k v l.toListModel)

eraseₘ

theorem Std.DTreeMap.Internal.Impl.ordered_eraseₘ {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] {k : α} {t : Impl α β} (htb : t.Balanced) (hto : t.Ordered) : (eraseₘ k t htb).Ordered

theorem Std.DTreeMap.Internal.Impl.toListModel_eraseₘ {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {t : Impl α β} (htb : t.Balanced) (hto : t.Ordered) : (eraseₘ k t htb).toListModel.Perm (Internal.List.eraseKey k t.toListModel)

erase

theorem Std.DTreeMap.Internal.Impl.ordered_erase {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] {k : α} {t : Impl α β} (htb : t.Balanced) (hto : t.Ordered) : (erase k t htb).impl.Ordered

theorem Std.DTreeMap.Internal.Impl.toListModel_erase {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {t : Impl α β} (htb : t.Balanced) (hto : t.Ordered) : (erase k t htb).impl.toListModel.Perm (Internal.List.eraseKey k t.toListModel)

erase!

theorem Std.DTreeMap.Internal.Impl.WF.erase! {α : Type u} {β : α → Type v} {x✝ : Ord α} [TransOrd α] {k : α} {l : Impl α β} (h : l.WF) : (Impl.erase! k l).WF

theorem Std.DTreeMap.Internal.Impl.toListModel_erase! {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {l : Impl α β} (hlb : l.Balanced) (hlo : l.Ordered) : (erase! k l).toListModel.Perm (Internal.List.eraseKey k l.toListModel)

containsThenInsert

theorem Std.DTreeMap.Internal.Impl.size_containsThenInsert_eq_size {α : Type u} {β : α → Type v} [Ord α] (t : Impl α β) : containsThenInsert.size t = t.size

theorem Std.DTreeMap.Internal.Impl.containsThenInsert_fst_eq_containsₘ {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] (t : Impl α β) (htb : t.Balanced) (ho : t.Ordered) (a : α) (b : β a) : (containsThenInsert a b t htb).fst = t.containsₘ a

theorem Std.DTreeMap.Internal.Impl.ordered_containsThenInsert {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] {k : α} {v : β k} {t : Impl α β} (htb : t.Balanced) (hto : t.Ordered) : (containsThenInsert k v t htb).snd.impl.Ordered

theorem Std.DTreeMap.Internal.Impl.toListModel_containsThenInsert {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {v : β k} {t : Impl α β} (htb : t.Balanced) (hto : t.Ordered) : (containsThenInsert k v t htb).snd.impl.toListModel.Perm (Internal.List.insertEntry k v t.toListModel)

containsThenInsert!

theorem Std.DTreeMap.Internal.Impl.WF.containsThenInsert! {α : Type u} {β : α → Type v} {x✝ : Ord α} [TransOrd α] {k : α} {v : β k} {t : Impl α β} (h : t.WF) : (Impl.containsThenInsert! k v t).snd.WF

theorem Std.DTreeMap.Internal.Impl.toListModel_containsThenInsert! {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {v : β k} {t : Impl α β} (htb : t.Balanced) (hto : t.Ordered) : (containsThenInsert! k v t).snd.toListModel.Perm (Internal.List.insertEntry k v t.toListModel)

insertIfNew

theorem Std.DTreeMap.Internal.Impl.ordered_insertIfNew {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] {k : α} {v : β k} {l : Impl α β} (h : l.Balanced) (ho : l.Ordered) : (insertIfNew k v l h).impl.Ordered

theorem Std.DTreeMap.Internal.Impl.toListModel_insertIfNew {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {v : β k} {l : Impl α β} (hlb : l.Balanced) (hlo : l.Ordered) : (insertIfNew k v l hlb).impl.toListModel.Perm (Internal.List.insertEntryIfNew k v l.toListModel)

insertIfNew!

theorem Std.DTreeMap.Internal.Impl.ordered_insertIfNew! {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] {k : α} {v : β k} {l : Impl α β} (h : l.Balanced) (ho : l.Ordered) : (insertIfNew! k v l).Ordered

theorem Std.DTreeMap.Internal.Impl.WF.insertIfNew! {α : Type u} {β : α → Type v} {x✝ : Ord α} [TransOrd α] {k : α} {v : β k} {l : Impl α β} (h : l.WF) : (Impl.insertIfNew! k v l).WF

theorem Std.DTreeMap.Internal.Impl.toListModel_insertIfNew! {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {v : β k} {l : Impl α β} (hlb : l.Balanced) (hlo : l.Ordered) : (insertIfNew! k v l).toListModel.Perm (Internal.List.insertEntryIfNew k v l.toListModel)

containsThenInsertIfNew

theorem Std.DTreeMap.Internal.Impl.ordered_containsThenInsertIfNew {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] {k : α} {v : β k} {l : Impl α β} (h : l.Balanced) (ho : l.Ordered) : (containsThenInsertIfNew k v l h).snd.impl.Ordered

theorem Std.DTreeMap.Internal.Impl.toListModel_containsThenInsertIfNew {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {v : β k} {t : Impl α β} (htb : t.Balanced) (hto : t.Ordered) : (containsThenInsertIfNew k v t htb).snd.impl.toListModel.Perm (Internal.List.insertEntryIfNew k v t.toListModel)

containsThenInsertIfNew!

theorem Std.DTreeMap.Internal.Impl.ordered_containsThenInsertIfNew! {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] {k : α} {v : β k} {l : Impl α β} (h : l.Balanced) (ho : l.Ordered) : (containsThenInsertIfNew! k v l).snd.Ordered

theorem Std.DTreeMap.Internal.Impl.WF.containsThenInsertIfNew! {α : Type u} {β : α → Type v} {x✝ : Ord α} [TransOrd α] {k : α} {v : β k} {l : Impl α β} (h : l.WF) : (Impl.containsThenInsertIfNew! k v l).snd.WF

theorem Std.DTreeMap.Internal.Impl.toListModel_containsThenInsertIfNew! {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {v : β k} {t : Impl α β} (htb : t.Balanced) (hto : t.Ordered) : (containsThenInsertIfNew k v t htb).snd.impl.toListModel.Perm (Internal.List.insertEntryIfNew k v t.toListModel)

filterMap

@[simp]

theorem Std.DTreeMap.Internal.Impl.toListModel_filterMap {α : Type u} {β : α → Type v} {γ : α → Type w} [Ord α] {t : Impl α β} {h : t.Balanced} {f : (a : α) → β a → Option (γ a)} : (filterMap f t h).impl.toListModel = List.filterMap (fun (x : (a : α) × β a) => Option.map (fun (x_1 : γ x.fst) => ⟨x.fst, x_1⟩) (f x.fst x.snd)) t.toListModel

theorem Std.DTreeMap.Internal.Impl.balanced_filterMap {α : Type u} {β : α → Type v} {γ : α → Type w} [Ord α] {t : Impl α β} {h : t.Balanced} {f : (a : α) → β a → Option (γ a)} : (filterMap f t h).impl.Balanced

theorem Std.DTreeMap.Internal.Impl.ordered_filterMap {α : Type u} {β : α → Type v} {γ : α → Type w} [Ord α] {t : Impl α β} {h : t.Balanced} {f : (a : α) → β a → Option (γ a)} (ho : t.Ordered) : (filterMap f t h).impl.Ordered

filter

theorem Std.DTreeMap.Internal.Impl.filter_eq_filterMap {α : Type u} {β : α → Type v} [Ord α] {t : Impl α β} {h : t.Balanced} {f : (a : α) → β a → Bool} : filter f t h = filterMap (fun (k : α) (v : β k) => if f k v = true then some v else none) t h

theorem Std.DTreeMap.Internal.Impl.toListModel_filter {α : Type u} {β : α → Type v} [Ord α] {t : Impl α β} {h : t.Balanced} {f : (a : α) → β a → Bool} : (filter f t h).impl.toListModel = List.filter (fun (e : (a : α) × β a) => f e.fst e.snd) t.toListModel

theorem Std.DTreeMap.Internal.Impl.ordered_filter {α : Type u} {β : α → Type v} [Ord α] {t : Impl α β} {h : t.Balanced} {f : (a : α) → β a → Bool} (hto : t.Ordered) : (filter f t h).impl.Ordered

alter

theorem Std.DTreeMap.Internal.Impl.toListModel_alterₘ {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [LawfulEqOrd α] [BEq α] [LawfulBEqOrd α] {t : Impl α β} {a : α} {f : Option (β a) → Option (β a)} (htb : t.Balanced) (hto : t.Ordered) : (alterₘ a f t htb).toListModel.Perm (Internal.List.alterKey a f t.toListModel)

theorem Std.DTreeMap.Internal.Impl.alter_eq_alterₘ {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [LawfulEqOrd α] {t : Impl α β} {a : α} {f : Option (β a) → Option (β a)} (htb : t.Balanced) (hto : t.Ordered) : (alter a f t htb).impl = alterₘ a f t htb

theorem Std.DTreeMap.Internal.Impl.toListModel_alter {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [LawfulEqOrd α] [BEq α] [LawfulBEqOrd α] {t : Impl α β} {a : α} {f : Option (β a) → Option (β a)} (htb : t.Balanced) (hto : t.Ordered) : (alter a f t htb).impl.toListModel.Perm (Internal.List.alterKey a f t.toListModel)

theorem Std.DTreeMap.Internal.Impl.ordered_alter {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [LawfulEqOrd α] {t : Impl α β} {a : α} {f : Option (β a) → Option (β a)} (htb : t.Balanced) (hto : t.Ordered) : (alter a f t htb).impl.Ordered

alter!

theorem Std.DTreeMap.Internal.Impl.alter_eq_alter! {α : Type u} {β : α → Type v} [Ord α] [LawfulEqOrd α] {t : Impl α β} {a : α} {f : Option (β a) → Option (β a)} (htb : t.Balanced) : (alter a f t htb).impl = alter! a f t

theorem Std.DTreeMap.Internal.Impl.toListModel_alter! {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [LawfulEqOrd α] [BEq α] [LawfulBEqOrd α] {t : Impl α β} {a : α} {f : Option (β a) → Option (β a)} (htb : t.Balanced) (hto : t.Ordered) : (alter! a f t).toListModel.Perm (Internal.List.alterKey a f t.toListModel)

modify

theorem Std.DTreeMap.Internal.Impl.modify_eq_alter {α : Type u} {β : α → Type v} [Ord α] [LawfulEqOrd α] {t : Impl α β} {a : α} {f : β a → β a} (htb : t.Balanced) : modify a f t = (alter a (fun (x : Option (β a)) => Option.map f x) t htb).impl

theorem Std.DTreeMap.Internal.Impl.ordered_modify {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [LawfulEqOrd α] {t : Impl α β} {a : α} {f : β a → β a} (htb : t.Balanced) (hto : t.Ordered) : (modify a f t).Ordered

theorem Std.DTreeMap.Internal.Impl.toListModel_modify {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [LawfulEqOrd α] [BEq α] [LawfulBEqOrd α] {t : Impl α β} {a : α} {f : β a → β a} (htb : t.Balanced) (hto : t.Ordered) : (modify a f t).toListModel.Perm (Internal.List.modifyKey a f t.toListModel)

mergeWith

theorem Std.DTreeMap.Internal.Impl.ordered_mergeWith {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [LawfulEqOrd α] {t₁ t₂ : Impl α β} {f : (a : α) → β a → β a → β a} (htb : t₁.Balanced) (hto : t₁.Ordered) : (mergeWith f t₁ t₂ htb).impl.Ordered

foldlM

theorem Std.DTreeMap.Internal.Impl.foldlM_eq_foldlM_toListModel {α : Type u} {β : α → Type v} {t : Impl α β} {m : Type u_1 → Type u_2} {δ : Type u_1} [Monad m] [LawfulMonad m] {f : δ → (a : α) → β a → m δ} {init : δ} : foldlM f init t = List.foldlM (fun (acc : δ) (p : (a : α) × β a) => f acc p.fst p.snd) init t.toListModel

theorem Std.DTreeMap.Internal.Impl.foldlM_toListModel_eq_foldlM {α : Type u} {β : α → Type v} {t : Impl α β} {m : Type u_1 → Type u_2} {δ : Type u_1} [Monad m] [LawfulMonad m] {f : δ → (a : α) × β a → m δ} {init : δ} : List.foldlM f init t.toListModel = foldlM (fun (acc : δ) (k : α) (v : β k) => f acc ⟨k, v⟩) init t

foldl

theorem Std.DTreeMap.Internal.Impl.foldl_eq_foldl {α : Type u} {β : α → Type v} {t : Impl α β} {δ : Type u_1} {f : δ → (a : α) → β a → δ} {init : δ} : foldl f init t = List.foldl (fun (acc : δ) (p : (a : α) × β a) => f acc p.fst p.snd) init t.toListModel

foldrM

theorem Std.DTreeMap.Internal.Impl.foldrM_eq_foldrM {α : Type u} {β : α → Type v} {t : Impl α β} {m : Type u_1 → Type u_2} {δ : Type u_1} [Monad m] [LawfulMonad m] {f : (a : α) → β a → δ → m δ} {init : δ} : foldrM f init t = List.foldrM (fun (p : (a : α) × β a) (acc : δ) => f p.fst p.snd acc) init t.toListModel

foldr

theorem Std.DTreeMap.Internal.Impl.foldr_eq_foldr {α : Type u} {β : α → Type v} {t : Impl α β} {δ : Type u_1} {f : (a : α) → β a → δ → δ} {init : δ} : foldr f init t = List.foldr (fun (p : (a : α) × β a) (acc : δ) => f p.fst p.snd acc) init t.toListModel

toList

theorem Std.DTreeMap.Internal.Impl.toList_eq_toListModel {α : Type u} {β : α → Type v} {t : Impl α β} : t.toList = t.toListModel

toArray

theorem Std.DTreeMap.Internal.Impl.toArray_eq_toArray {α : Type u} {β : α → Type v} {t : Impl α β} : t.toArray = t.toListModel.toArray

keys

theorem Std.DTreeMap.Internal.Impl.keys_eq_keys {α : Type u} {β : α → Type v} {t : Impl α β} : t.keys = Internal.List.keys t.toListModel

keysArray

theorem Std.DTreeMap.Internal.Impl.keysArray_eq_toArray_keys {α : Type u} {β : α → Type v} {t : Impl α β} : t.keysArray = (Internal.List.keys t.toListModel).toArray

values

theorem Std.DTreeMap.Internal.Impl.values_eq_map_snd {α : Type u} {β : Type v} {t : Impl α fun (x : α) => β} : t.values = List.map (fun (x : (_ : α) × β) => x.snd) t.toListModel

valuesArray

theorem Std.DTreeMap.Internal.Impl.valuesArray_eq_toArray_map {α : Type u} {β : Type v} {t : Impl α fun (x : α) => β} : t.valuesArray = (List.map (fun (x : (_ : α) × β) => x.snd) t.toListModel).toArray

forM

theorem Std.DTreeMap.Internal.Impl.forM_eq_forM {α : Type u} {β : α → Type v} {t : Impl α β} {m : Type w → Type w'} [Monad m] [LawfulMonad m] {f : (a : α) → β a → m PUnit} : forM f t = t.toListModel.forM fun (a : (a : α) × β a) => f a.fst a.snd

forIn

theorem Std.DTreeMap.Internal.Impl.forInStep_eq_foldlM {α : Type u} {β : α → Type v} {δ : Type w} {t : Impl α β} {m : Type w → Type w'} [Monad m] [LawfulMonad m] {f : (a : α) → β a → δ → m (ForInStep δ)} {init : δ} : forInStep f init t = foldlM (fun (x : ForInStep δ) => match (motive := ForInStep δ → (a : α) → β a → m (ForInStep δ)) x with | ForInStep.yield d => fun (k : α) (v : β k) => f k v d | ForInStep.done d => fun (x : α) (x : β x) => pure (ForInStep.done d)) (ForInStep.yield init) t

theorem Std.DTreeMap.Internal.Impl.forIn_eq_forIn_toListModel {α : Type u} {β : α → Type v} {δ : Type w} {t : Impl α β} {m : Type w → Type w'} [Monad m] [LawfulMonad m] {f : (a : α) → β a → δ → m (ForInStep δ)} {init : δ} : forIn f init t = ForIn.forIn t.toListModel init fun (a : (a : α) × β a) (d : δ) => f a.fst a.snd d

getThenInsertIfNew?!

theorem Std.DTreeMap.Internal.Impl.Const.WF.getThenInsertIfNew?! {α : Type u} {β : Type v} [Ord α] [TransOrd α] [LawfulEqOrd α] {k : α} {v : β} {t : Impl α fun (x : α) => β} (h : t.WF) : (Const.getThenInsertIfNew?! t k v).snd.WF

alter

theorem Std.DTreeMap.Internal.Impl.Const.toListModel_alterₘ {α : Type u} {β : Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {t : Impl α fun (x : α) => β} {a : α} {f : Option β → Option β} (htb : t.Balanced) (hto : t.Ordered) : (alterₘ a f t htb).toListModel.Perm (Internal.List.Const.alterKey a f t.toListModel)

theorem Std.DTreeMap.Internal.Impl.Const.alter_eq_alterₘ {α : Type u} {β : Type v} [Ord α] [TransOrd α] {t : Impl α fun (x : α) => β} {a : α} {f : Option β → Option β} (htb : t.Balanced) (hto : t.Ordered) : (alter a f t htb).impl = alterₘ a f t htb

theorem Std.DTreeMap.Internal.Impl.Const.toListModel_alter {α : Type u} {β : Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {t : Impl α fun (x : α) => β} {a : α} {f : Option β → Option β} (htb : t.Balanced) (hto : t.Ordered) : (alter a f t htb).impl.toListModel.Perm (Internal.List.Const.alterKey a f t.toListModel)

theorem Std.DTreeMap.Internal.Impl.Const.ordered_alter {α : Type u} {β : Type v} [Ord α] [TransOrd α] {t : Impl α fun (x : α) => β} {a : α} {f : Option β → Option β} (htb : t.Balanced) (hto : t.Ordered) : (alter a f t htb).impl.Ordered

alter!

theorem Std.DTreeMap.Internal.Impl.Const.alter_eq_alter! {α : Type u} {β : Type v} [Ord α] {t : Impl α fun (x : α) => β} {a : α} {f : Option β → Option β} (htb : t.Balanced) : (alter a f t htb).impl = alter! a f t

theorem Std.DTreeMap.Internal.Impl.Const.toListModel_alter! {α : Type u} {β : Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {t : Impl α fun (x : α) => β} {a : α} {f : Option β → Option β} (htb : t.Balanced) (hto : t.Ordered) : (alter! a f t).toListModel.Perm (Internal.List.Const.alterKey a f t.toListModel)

modify

theorem Std.DTreeMap.Internal.Impl.Const.modify_eq_alter {α : Type u} {β : Type v} [Ord α] [TransOrd α] {t : Impl α fun (x : α) => β} {a : α} {f : β → β} (htb : t.Balanced) : modify a f t = (alter a (fun (x : Option β) => Option.map f x) t htb).impl

theorem Std.DTreeMap.Internal.Impl.Const.ordered_modify {α : Type u} {β : Type v} [Ord α] [TransOrd α] {t : Impl α fun (x : α) => β} {a : α} {f : β → β} (htb : t.Balanced) (hto : t.Ordered) : (modify a f t).Ordered

theorem Std.DTreeMap.Internal.Impl.Const.toListModel_modify {α : Type u} {β : Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {t : Impl α fun (x : α) => β} {a : α} {f : β → β} (htb : t.Balanced) (hto : t.Ordered) : (modify a f t).toListModel.Perm (Internal.List.Const.modifyKey a f t.toListModel)

mergeWith

theorem Std.DTreeMap.Internal.Impl.Const.ordered_mergeWith {α : Type u} {β : Type v} [Ord α] [TransOrd α] {t₁ t₂ : Impl α fun (x : α) => β} {f : α → β → β → β} (htb : t₁.Balanced) (hto : t₁.Ordered) : (mergeWith f t₁ t₂ htb).impl.Ordered

toList

theorem Std.DTreeMap.Internal.Impl.Const.toList_eq_toListModel_map {α : Type u} {β : Type v} {t : Impl α fun (x : α) => β} : toList t = List.map (fun (e : (_ : α) × β) => (e.fst, e.snd)) t.toListModel

toArray

theorem Std.DTreeMap.Internal.Impl.Const.toArray_eq_toArray_map {α : Type u} {β : Type v} {t : Impl α fun (x : α) => β} : toArray t = (List.map (fun (e : (_ : α) × β) => (e.fst, e.snd)) t.toListModel).toArray

Deducing that well-formed trees are ordered

theorem Std.DTreeMap.Internal.Impl.WF.ordered {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] {l : Impl α β} (h : l.WF) : l.Ordered

Deducing that additional operations are well-formed

inductive Std.DTreeMap.Internal.Impl.SameKeys {α : Type u} {β : α → Type v} {β' : α → Type u_1} : Impl α β → Impl α β' → Prop

Internal implementation detail of the tree map

• leaf {α : Type u} {β : α → Type v} {β' : α → Type u_1} : Impl.leaf.SameKeys Impl.leaf

  Internal implementation detail of the tree map

• inner {α : Type u} {β : α → Type v} {β' : α → Type u_1} (sz : Nat) (k : α) (v : β k) (v' : β' k) (r : Impl α β) (r' : Impl α β') (l : Impl α β) (l' : Impl α β') : r.SameKeys r' → l.SameKeys l' → (Impl.inner sz k v l r).SameKeys (Impl.inner sz k v' l' r')

  Internal implementation detail of the tree map

theorem Std.DTreeMap.Internal.Impl.SameKeys.ordered_iff_pairwise_keys {α : Type u} {β : α → Type v} [Ord α] {t : Impl α β} : t.Ordered ↔ List.Pairwise (fun (x1 x2 : α) => compare x1 x2 = Ordering.lt) (List.map (fun (x : (a : α) × β a) => x.fst) t.toListModel)

theorem Std.DTreeMap.Internal.Impl.SameKeys.symm {α : Type u} {β : α → Type v} {β' : α → Type u_1} [Ord α] {t : Impl α β} {t' : Impl α β'} (hs : t.SameKeys t') : t'.SameKeys t

theorem Std.DTreeMap.Internal.Impl.SameKeys.keys_eq {α : Type u} {β : α → Type v} {β' : α → Type u_1} [Ord α] {t : Impl α β} {t' : Impl α β'} (h : t.SameKeys t') : List.map (fun (x : (a : α) × β a) => x.fst) t.toListModel = List.map (fun (x : (a : α) × β' a) => x.fst) t'.toListModel

theorem Std.DTreeMap.Internal.Impl.SameKeys.size_eq {α : Type u} {β : α → Type v} {β' : α → Type u_1} [Ord α] {t : Impl α β} {t' : Impl α β'} (h : t.SameKeys t') : t.size = t'.size

theorem Std.DTreeMap.Internal.Impl.SameKeys.ordered {α : Type u} {β : α → Type v} {β' : α → Type u_1} [Ord α] {t : Impl α β} {t' : Impl α β'} (hs : t.SameKeys t') (h : t.Ordered) : t'.Ordered

theorem Std.DTreeMap.Internal.Impl.SameKeys.balanced {α : Type u} {β : α → Type v} {β' : α → Type u_1} [Ord α] {t : Impl α β} {t' : Impl α β'} (hs : t.SameKeys t') (h : t.Balanced) : t'.Balanced

theorem Std.DTreeMap.Internal.Impl.SameKeys.wf {α : Type u} {β : α → Type v} {β' : α → Type u_1} [Ord α] {t : Impl α β} {t' : Impl α β'} (hs : t.SameKeys t') (h : t.WF) : t'.WF

getThenInsertIfNew?!

theorem Std.DTreeMap.Internal.Impl.WF.getThenInsertIfNew?! {α : Type u} {β : α → Type v} {x✝ : Ord α} [TransOrd α] [LawfulEqOrd α] {k : α} {v : β k} {t : Impl α β} (h : t.WF) : (t.getThenInsertIfNew?! k v).snd.WF

theorem Std.DTreeMap.Internal.Impl.WF.constGetThenInsertIfNew?! {α : Type u} {β : Type v} {x✝ : Ord α} [TransOrd α] {k : α} {v : β} {t : Impl α fun (x : α) => β} (h : t.WF) : (Const.getThenInsertIfNew?! t k v).snd.WF

eraseMany!

theorem Std.DTreeMap.Internal.Impl.WF.eraseMany! {α : Type u} {β : α → Type v} {x✝ : Ord α} [TransOrd α] {ρ : Type u_1} [ForIn Id ρ α] {l : ρ} {t : Impl α β} (h : t.WF) : (t.eraseMany! l).val.WF

insertMany

theorem Std.DTreeMap.Internal.Impl.insertMany!_eq_foldl {α : Type u} {β : α → Type v} {x✝ : Ord α} {l : List ((a : α) × β a)} {t : Impl α β} : (t.insertMany! l).val = List.foldl (fun (acc : Impl α β) (x : (a : α) × β a) => match x with | ⟨k, v⟩ => insert! k v acc) t l

theorem Std.DTreeMap.Internal.Impl.insertMany_eq_foldl {α : Type u} {β : α → Type v} {x✝ : Ord α} {l : List ((a : α) × β a)} {t : Impl α β} (h : t.Balanced) : (t.insertMany l h).val = List.foldl (fun (acc : Impl α β) (x : (a : α) × β a) => match x with | ⟨k, v⟩ => insert! k v acc) t l

theorem Std.DTreeMap.Internal.Impl.insertMany_eq_insertMany! {α : Type u} {β : α → Type v} {x✝ : Ord α} {l : List ((a : α) × β a)} {t : Impl α β} (h : t.Balanced) : (t.insertMany l h).val = (t.insertMany! l).val

theorem Std.DTreeMap.Internal.Impl.toListModel_insertMany_list {α : Type u} {β : α → Type v} {x✝ : Ord α} [BEq α] [LawfulBEqOrd α] [TransOrd α] {l : List ((a : α) × β a)} {t : Impl α β} (h : t.WF) : (t.insertMany l ⋯).val.toListModel.Perm (Internal.List.insertList t.toListModel l)

theorem Std.DTreeMap.Internal.Impl.toListModel_insertMany!_list {α : Type u} {β : α → Type v} {x✝ : Ord α} [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} {t : Impl α β} (h : t.WF) : (t.insertMany! l).val.toListModel.Perm (Internal.List.insertList t.toListModel l)

theorem Std.DTreeMap.Internal.Impl.WF.insertMany! {α : Type u} {β : α → Type v} {x✝ : Ord α} [TransOrd α] {ρ : Type u_1} [ForIn Id ρ ((a : α) × β a)] {l : ρ} {t : Impl α β} (h : t.WF) : (t.insertMany! l).val.WF

theorem Std.DTreeMap.Internal.Impl.WF.constInsertMany! {α : Type u} {β : Type v} {x✝ : Ord α} [TransOrd α] {ρ : Type u_1} [ForIn Id ρ (α × β)] {l : ρ} {t : Impl α fun (x : α) => β} (h : t.WF) : (Const.insertMany! t l).val.WF

theorem Std.DTreeMap.Internal.Impl.WF.constInsertManyIfNewUnit! {α : Type u} {x✝ : Ord α} [TransOrd α] {ρ : Type u_1} [ForIn Id ρ α] {l : ρ} {t : Impl α fun (x : α) => Unit} (h : t.WF) : (Const.insertManyIfNewUnit! t l).val.WF

insertMany

theorem Std.DTreeMap.Internal.Impl.Const.insertMany!_eq_foldl {α : Type u} {β : Type v} {x✝ : Ord α} {l : List (α × β)} {t : Impl α fun (x : α) => β} : (insertMany! t l).val = List.foldl (fun (acc : Impl α fun (x : α) => β) (x : α × β) => match x with | (k, v) => insert! k v acc) t l

theorem Std.DTreeMap.Internal.Impl.Const.insertMany_eq_foldl {α : Type u} {β : Type v} {x✝ : Ord α} {l : List (α × β)} {t : Impl α fun (x : α) => β} (h : t.Balanced) : (insertMany t l h).val = List.foldl (fun (acc : Impl α fun (x : α) => β) (x : α × β) => match x with | (k, v) => insert! k v acc) t l

theorem Std.DTreeMap.Internal.Impl.Const.insertMany_eq_insertMany! {α : Type u} {β : Type v} {x✝ : Ord α} {l : List (α × β)} {t : Impl α fun (x : α) => β} (h : t.Balanced) : (insertMany t l h).val = (insertMany! t l).val

theorem Std.DTreeMap.Internal.Impl.Const.toListModel_insertMany_list {α : Type u} {β : Type v} {x✝ : Ord α} [BEq α] [TransOrd α] [LawfulBEqOrd α] {l : List (α × β)} {t : Impl α fun (x : α) => β} (h : t.WF) : (insertMany t l ⋯).val.toListModel.Perm (Internal.List.insertListConst t.toListModel l)

theorem Std.DTreeMap.Internal.Impl.Const.toListModel_insertMany!_list {α : Type u} {β : Type v} {x✝ : Ord α} [BEq α] [LawfulBEqOrd α] [TransOrd α] {l : List (α × β)} {t : Impl α fun (x : α) => β} (h : t.WF) : (insertMany! t l).val.toListModel.Perm (Internal.List.insertListConst t.toListModel l)

theorem Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit_eq_foldl {α : Type u} {x✝ : Ord α} {l : List α} {t : Impl α fun (x : α) => Unit} (h : t.Balanced) : (insertManyIfNewUnit t l h).val = List.foldl (fun (acc : Impl α fun (x : α) => Unit) (k : α) => insertIfNew! k () acc) t l

theorem Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit!_eq_foldl {α : Type u} {x✝ : Ord α} {l : List α} {t : Impl α fun (x : α) => Unit} : (insertManyIfNewUnit! t l).val = List.foldl (fun (acc : Impl α fun (x : α) => Unit) (k : α) => insertIfNew! k () acc) t l

theorem Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit_eq_insertManyIfNewUnit! {α : Type u} {x✝ : Ord α} {l : List α} {t : Impl α fun (x : α) => Unit} (h : t.Balanced) : (insertManyIfNewUnit t l h).val = (insertManyIfNewUnit! t l).val

theorem Std.DTreeMap.Internal.Impl.Const.toListModel_insertManyIfNewUnit_list {α : Type u} {x✝ : Ord α} [TransOrd α] [instBEq : BEq α] [LawfulBEqOrd α] {l : List α} {t : Impl α fun (x : α) => Unit} (h : t.WF) : (insertManyIfNewUnit t l ⋯).val.toListModel.Perm (Internal.List.insertListIfNewUnit t.toListModel l)

theorem Std.DTreeMap.Internal.Impl.Const.toListModel_insertManyIfNewUnit!_list {α : Type u} {x✝ : Ord α} [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List α} {t : Impl α fun (x : α) => Unit} (h : t.WF) : (insertManyIfNewUnit! t l).val.toListModel.Perm (Internal.List.insertListIfNewUnit t.toListModel l)

alter!

theorem Std.DTreeMap.Internal.Impl.WF.alter! {α : Type u} {β : α → Type v} {x✝ : Ord α} [LawfulEqOrd α] {t : Impl α β} {a : α} {f : Option (β a) → Option (β a)} (h : t.WF) : (Impl.alter! a f t).WF

theorem Std.DTreeMap.Internal.Impl.WF.constAlter! {α : Type u} {x✝ : Ord α} {β : Type v} {t : Impl α fun (x : α) => β} {a : α} {f : Option β → Option β} (h : t.WF) : (Const.alter! a f t).WF

mergeWith!

theorem Std.DTreeMap.Internal.Impl.mergeWith_eq_mergeWith! {α : Type u} {β : α → Type v} {x✝ : Ord α} [LawfulEqOrd α] {mergeFn : (a : α) → β a → β a → β a} {t₁ t₂ : Impl α β} (h : t₁.Balanced) : (mergeWith mergeFn t₁ t₂ h).impl = mergeWith! mergeFn t₁ t₂

theorem Std.DTreeMap.Internal.Impl.WF.mergeWith! {α : Type u} {β : α → Type v} {x✝ : Ord α} [LawfulEqOrd α] {mergeFn : (a : α) → β a → β a → β a} {t₁ t₂ : Impl α β} (h : t₁.WF) : (Impl.mergeWith! mergeFn t₁ t₂).WF

theorem Std.DTreeMap.Internal.Impl.Const.mergeWith_eq_mergeWith! {α : Type u} {β : Type v} {x✝ : Ord α} {mergeFn : α → β → β → β} {t₁ t₂ : Impl α fun (x : α) => β} (h : t₁.Balanced) : (mergeWith mergeFn t₁ t₂ h).impl = mergeWith! mergeFn t₁ t₂

theorem Std.DTreeMap.Internal.Impl.WF.constMergeWith! {α : Type u} {β : Type v} {x✝ : Ord α} {mergeFn : α → β → β → β} {t₁ t₂ : Impl α fun (x : α) => β} (h : t₁.WF) : (Const.mergeWith! mergeFn t₁ t₂).WF

filterMap

theorem Std.DTreeMap.Internal.Impl.WF.filterMap {α : Type u} {β : α → Type v} {γ : α → Type w} [Ord α] {t : Impl α β} {h : t.Balanced} {f : (a : α) → β a → Option (γ a)} (hwf : t.WF) : (Impl.filterMap f t h).impl.WF

filterMap!

theorem Std.DTreeMap.Internal.Impl.filterMap_eq_filterMap! {α : Type u} {β : α → Type v} {γ : α → Type w} [Ord α] {t : Impl α β} {h : t.Balanced} {f : (a : α) → β a → Option (γ a)} : (filterMap f t h).impl = filterMap! f t

theorem Std.DTreeMap.Internal.Impl.WF.filterMap! {α : Type u} {β : α → Type v} {γ : α → Type w} {x✝ : Ord α} {t : Impl α β} {f : (a : α) → β a → Option (γ a)} (h : t.WF) : (Impl.filterMap! f t).WF

filter!

theorem Std.DTreeMap.Internal.Impl.filter_eq_filter! {α : Type u} {β : α → Type v} [Ord α] {t : Impl α β} {h : t.Balanced} {f : (a : α) → β a → Bool} : (filter f t h).impl = filter! f t

theorem Std.DTreeMap.Internal.Impl.WF.filter! {α : Type u} {β : α → Type v} {x✝ : Ord α} {t : Impl α β} {f : (a : α) → β a → Bool} (h : t.WF) : (Impl.filter! f t).WF

map

theorem Std.DTreeMap.Internal.Impl.toListModel_map {α : Type u} {β : α → Type v} {γ : α → Type w} [Ord α] {t : Impl α β} {f : (a : α) → β a → γ a} : (map f t).toListModel = List.map (fun (x : (a : α) × β a) => ⟨x.fst, f x.fst x.snd⟩) t.toListModel

theorem Std.DTreeMap.Internal.Impl.sameKeys_map {α : Type u} {β : α → Type v} {γ : α → Type w} [Ord α] {t : Impl α β} {f : (a : α) → β a → γ a} : (map f t).SameKeys t

@[simp]

theorem Std.DTreeMap.Internal.Impl.size_map {α : Type u} {β : α → Type v} {γ : α → Type w} [Ord α] {t : Impl α β} {f : (a : α) → β a → γ a} : (map f t).size = t.size

theorem Std.DTreeMap.Internal.Impl.WF.map {α : Type u} {β : α → Type v} {γ : α → Type w} [Ord α] {t : Impl α β} {f : (a : α) → β a → γ a} (h : t.WF) : (Impl.map f t).WF

minEntry?

theorem Std.DTreeMap.Internal.Impl.minEntry?ₘ_eq_minEntry? {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] {l : Impl α β} (hlo : l.Ordered) : l.minEntry?ₘ = Internal.List.minEntry? l.toListModel

theorem Std.DTreeMap.Internal.Impl.minEntry?_eq_minEntry? {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] {l : Impl α β} (hlo : l.Ordered) : l.minEntry? = Internal.List.minEntry? l.toListModel

theorem Std.DTreeMap.Internal.Impl.minKey?_eq_minKey? {α : Type u} {β : α → Type v} {x✝ : Ord α} [TransOrd α] {l : Impl α β} (hlo : l.Ordered) : l.minKey? = Internal.List.minKey? l.toListModel

theorem Std.DTreeMap.Internal.Impl.minKey_eq_minKey {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : Impl α β} (hlo : l.Ordered) {he : l.isEmpty = false} : l.minKey he = Internal.List.minKey l.toListModel ⋯

theorem Std.DTreeMap.Internal.Impl.minKey!_eq_minKey! {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [Inhabited α] [BEq α] [LawfulBEqOrd α] {l : Impl α β} (hlo : l.Ordered) : l.minKey! = Internal.List.minKey! l.toListModel

theorem Std.DTreeMap.Internal.Impl.minKeyD_eq_minKeyD {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : Impl α β} (hlo : l.Ordered) {fallback : α} : l.minKeyD fallback = Internal.List.minKeyD l.toListModel fallback

theorem Std.DTreeMap.Internal.Impl.toListModel_reverse {α : Type u} {β : α → Type v} {l : Impl α β} : l.reverse.toListModel = l.toListModel.reverse

theorem Std.DTreeMap.Internal.Impl.Ordered.reverse {α : Type u} {β : α → Type v} [Ord α] {t : Impl α β} (h : t.Ordered) : t.reverse.Ordered

theorem Std.DTreeMap.Internal.Impl.maxEntry?_eq_minEntry? {α : Type u} {β : α → Type v} [o : Ord α] [to : TransOrd α] {t : Impl α β} (hlo : t.Ordered) : t.maxEntry? = Internal.List.minEntry? t.toListModel

theorem Std.DTreeMap.Internal.Impl.maxKey?_eq_maxKey? {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {t : Impl α β} (hlo : t.Ordered) : t.maxKey? = Internal.List.maxKey? t.toListModel

theorem Std.DTreeMap.Internal.Impl.maxKey_eq_maxKey {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {t : Impl α β} (hlo : t.Ordered) {he : t.isEmpty = false} : t.maxKey he = Internal.List.maxKey t.toListModel ⋯

theorem Std.DTreeMap.Internal.Impl.maxKey!_eq_maxKey! {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [Inhabited α] [BEq α] [LawfulBEqOrd α] {t : Impl α β} (hlo : t.Ordered) : t.maxKey! = Internal.List.maxKey! t.toListModel

theorem Std.DTreeMap.Internal.Impl.maxKeyD_eq_maxKeyD {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {t : Impl α β} (hlo : t.Ordered) {fallback : α} : t.maxKeyD fallback = Internal.List.maxKeyD t.toListModel fallback

entryAtIdx? / keyAtIdx?

theorem Std.DTreeMap.Internal.Impl.entryAtIdx?_eq_getElem? {α : Type u} {β : α → Type v} {t : Impl α β} (htb : t.Balanced) {i : Nat} : t.entryAtIdx? i = t.toListModel[i]?

theorem Std.DTreeMap.Internal.Impl.entryAtIdx_eq_getElem {α : Type u} {β : α → Type v} {t : Impl α β} (htb : t.Balanced) {i : Nat} {h : i < t.size} : t.entryAtIdx htb i h = t.toListModel[i]

theorem Std.DTreeMap.Internal.Impl.entryAtIdx!_eq_getElem! {α : Type u} {β : α → Type v} {t : Impl α β} (htb : t.Balanced) {i : Nat} [Inhabited ((a : α) × β a)] : t.entryAtIdx! i = t.toListModel[i]!

theorem Std.DTreeMap.Internal.Impl.entryAtIdxD_eq_getD {α : Type u} {β : α → Type v} {t : Impl α β} (htb : t.Balanced) {i : Nat} {fallback : (a : α) × β a} : t.entryAtIdxD i fallback = t.toListModel.getD i fallback

theorem Std.DTreeMap.Internal.Impl.keyAtIdx?_eq_getElem? {α : Type u} {β : α → Type v} {t : Impl α β} (htb : t.Balanced) {i : Nat} : t.keyAtIdx? i = Option.map (fun (x : (a : α) × β a) => x.fst) t.toListModel[i]?

theorem Std.DTreeMap.Internal.Impl.keyAtIdx_eq_getElem_fst {α : Type u} {β : α → Type v} {t : Impl α β} (htb : t.Balanced) {i : Nat} {h : i < t.size} : t.keyAtIdx htb i h = t.toListModel[i].fst

theorem Std.DTreeMap.Internal.Impl.keyAtIdx!_eq_get!_map_getElem? {α : Type u} {β : α → Type v} [Inhabited α] {t : Impl α β} (htb : t.Balanced) {i : Nat} : t.keyAtIdx! i = (Option.map (fun (x : (a : α) × β a) => x.fst) t.toListModel[i]?).get!

theorem Std.DTreeMap.Internal.Impl.keyAtIdxD_eq_getD_map_getElem? {α : Type u} {β : α → Type v} {t : Impl α β} (htb : t.Balanced) {i : Nat} {fallback : α} : t.keyAtIdxD i fallback = (Option.map (fun (x : (a : α) × β a) => x.fst) t.toListModel[i]?).getD fallback

theorem Std.DTreeMap.Internal.Impl.Const.entryAtIdx?_eq_getElem? {α : Type u} {β : Type v} {t : Impl α fun (x : α) => β} (htb : t.Balanced) {i : Nat} : entryAtIdx? t i = Option.map (fun (x : (_ : α) × β) => (x.fst, x.snd)) t.toListModel[i]?

theorem Std.DTreeMap.Internal.Impl.Const.entryAtIdx_eq_getElem {α : Type u} {β : Type v} {t : Impl α fun (x : α) => β} (htb : t.Balanced) {i : Nat} {h : i < t.size} : entryAtIdx t htb i h = (t.toListModel[i].fst, t.toListModel[i].snd)

theorem Std.DTreeMap.Internal.Impl.Const.entryAtIdx!_eq_get!_map_getElem? {α : Type u} {β : Type v} {t : Impl α fun (x : α) => β} (htb : t.Balanced) {i : Nat} [Inhabited (α × β)] : entryAtIdx! t i = (Option.map (fun (x : (_ : α) × β) => (x.fst, x.snd)) t.toListModel[i]?).get!

theorem Std.DTreeMap.Internal.Impl.Const.entryAtIdxD_eq_getD_map_getElem? {α : Type u} {β : Type v} {t : Impl α fun (x : α) => β} (htb : t.Balanced) {i : Nat} {fallback : α × β} : entryAtIdxD t i fallback = (Option.map (fun (x : (_ : α) × β) => (x.fst, x.snd)) t.toListModel[i]?).getD fallback

getEntryLE? / getKeyLE? / ...

theorem Std.DTreeMap.Internal.Impl.getEntryGE?_eq_find? {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] {t : Impl α β} (hto : t.Ordered) {k : α} : getEntryGE? k t = List.find? (fun (e : (a : α) × β a) => (compare e.fst k).isGE) t.toListModel

theorem Std.DTreeMap.Internal.Impl.getEntryGT?_eq_find? {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] {t : Impl α β} (hto : t.Ordered) {k : α} : getEntryGT? k t = List.find? (fun (e : (a : α) × β a) => (compare e.fst k).isGT) t.toListModel

theorem Std.DTreeMap.Internal.Impl.getEntryLE?_eq_findRev? {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] {t : Impl α β} (hto : t.Ordered) {k : α} : getEntryLE? k t = List.findRev? (fun (e : (a : α) × β a) => (compare e.fst k).isLE) t.toListModel

theorem Std.DTreeMap.Internal.Impl.getEntryLT?_eq_findRev? {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] {t : Impl α β} (hto : t.Ordered) {k : α} : getEntryLT? k t = List.findRev? (fun (e : (a : α) × β a) => (compare e.fst k).isLT) t.toListModel