Well-formedness predicate on size-bounded trees

This file defines the well-formedness predicate WF on the internal size-bounded tree data structure Impl and proves well-formedness for those operations that aren't per definition.

A central consequence of well-formedness, balancedness, is shown for all well-formed trees.

@[instance_reducible]

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

Equations

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

inductive Std.DTreeMap.Internal.Impl.WF {α : Type u} [Ord α] {β : α → Type v} : Impl α β → Prop

Well-formedness of tree maps.

• wf {α : Type u} [Ord α] {x✝ : α → Type v} {t : Impl α x✝} : t.Balanced → (∀ [TransOrd α], t.Ordered) → t.WF

  This is the actual well-formedness invariant: the tree must be a balanced BST.

• empty {α : Type u} [Ord α] {x✝ : α → Type v} : Impl.empty.WF

  The empty tree is well-formed. Later shown to be subsumed by .wf.

• insert {α : Type u} [Ord α] {x✝ : α → Type v} {t : Impl α x✝} {h : t.Balanced} {k : α} {v : x✝ k} : t.WF → (Impl.insert k v t h).impl.WF

  insert preserves well-formedness. Later shown to be subsumed by .wf.

• insertIfNew {α : Type u} [Ord α] {x✝ : α → Type v} {t : Impl α x✝} {h : t.Balanced} {k : α} {v : x✝ k} : t.WF → (Impl.insertIfNew k v t h).impl.WF

  insertIfNew preserves well-formedness. Later shown to be subsumed by .wf.

• erase {α : Type u} [Ord α] {x✝ : α → Type v} {t : Impl α x✝} {h : t.Balanced} {k : α} : t.WF → (Impl.erase k t h).impl.WF

  erase preserves well-formedness. Later shown to be subsumed by .wf.

• alter {α : Type u} [Ord α] {x✝ : α → Type v} [LawfulEqOrd α] {t : Impl α x✝} {h : t.Balanced} {k : α} {f : Option (x✝ k) → Option (x✝ k)} : t.WF → (Impl.alter k f t h).impl.WF

  alter preserves well-formedness. Later shown to be subsumed by .wf.

• constAlter {α : Type u} [Ord α] {x✝ : Type v} {t : Impl α fun (x : α) => x✝} {h : t.Balanced} {k : α} {f : Option x✝ → Option x✝} : t.WF → (Const.alter k f t h).impl.WF

  alter preserves well-formedness. Later shown to be subsumed by .wf.

• modify {α : Type u} [Ord α] {x✝ : α → Type v} [LawfulEqOrd α] {t : Impl α x✝} {k : α} {f : x✝ k → x✝ k} : t.WF → (Impl.modify k f t).WF

  modify preserves well-formedness. Later shown to be subsumed by .wf.

• constModify {α : Type u} [Ord α] {x✝ : Type v} {t : Impl α fun (x : α) => x✝} {k : α} {f : x✝ → x✝} : t.WF → (Const.modify k f t).WF

  modify preserves well-formedness. Later shown to be subsumed by .wf.

• containsThenInsert {α : Type u} [Ord α] {x✝ : α → Type v} {t : Impl α x✝} {h : t.Balanced} {k : α} {v : x✝ k} : t.WF → (Impl.containsThenInsert k v t h).snd.impl.WF

  containsThenInsert preserves well-formedness. Later shown to be subsumed by .wf.

• containsThenInsertIfNew {α : Type u} [Ord α] {x✝ : α → Type v} {t : Impl α x✝} {h : t.Balanced} {k : α} {v : x✝ k} : t.WF → (Impl.containsThenInsertIfNew k v t h).snd.impl.WF

  containsThenInsertIfNew preserves well-formedness. Later shown to be subsumed by .wf.

• filter {α : Type u} [Ord α] {x✝ : α → Type v} {t : Impl α x✝} {h : t.Balanced} {f : (a : α) → x✝ a → Bool} : t.WF → (Impl.filter f t h).impl.WF

  filter preserves well-formedness. Later shown to be subsumed by .wf.

• mergeWith {α : Type u} [Ord α] {x✝ : α → Type v} {t₁ t₂ : Impl α x✝} {f : (a : α) → x✝ a → x✝ a → x✝ a} {h : t₁.Balanced} [LawfulEqOrd α] : t₁.WF → (Impl.mergeWith f t₁ t₂ h).impl.WF

  mergeWith preserves well-formedness. Later shown to be subsumed by .wf.

• constMergeWith {α : Type u} [Ord α] {x✝ : Type v} {t₁ t₂ : Impl α fun (x : α) => x✝} {f : α → x✝ → x✝ → x✝} {h : t₁.Balanced} : t₁.WF → (Const.mergeWith f t₁ t₂ h).impl.WF

  mergeWith preserves well-formedness. Later shown to be subsumed by .wf.

• inter {α : Type u} [Ord α] {x✝ : α → Type v} {t₁ t₂ : Impl α x✝} {h : t₁.Balanced} : t₁.WF → (t₁.inter t₂ h).WF

  inter preserves well-formedness. Later shown to be subsumed by .wf.

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

A well-formed tree is balanced. This is needed here already because we need to know that the tree is balanced to call the optimized modification functions.

theorem Std.DTreeMap.Internal.Impl.WF.eraseManyEntries {α : Type u} {β : α → Type v} [Ord α] {ρ : Type u_1} [ForIn Id ρ ((a : α) × β a)] {t : Impl α β} {l : ρ} {h : t.Balanced} (hwf : t.WF) : (t.eraseManyEntries l h).val.WF

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

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

theorem Std.DTreeMap.Internal.Impl.WF.insertManyIfNew {α : Type u} {β : α → Type v} [Ord α] {ρ : Type u_1} [ForIn Id ρ ((a : α) × β a)] {t : Impl α β} {l : ρ} {h : t.Balanced} (hwf : t.WF) : (t.insertManyIfNew l h).val.WF

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

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

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

theorem Std.DTreeMap.Internal.Impl.WF.union {α : Type u} {β : α → Type v} [Ord α] {t₁ : Impl α β} {h₁ : t₁.WF} {t₂ : Impl α β} {h₂ : t₂.WF} : (t₁.union t₂ ⋯ ⋯).WF

theorem Std.DTreeMap.Internal.Impl.WF.diff {α : Type u} {β : α → Type v} [Ord α] {t₁ : Impl α β} {h₁ : t₁.WF} {t₂ : Impl α β} : (t₁.diff t₂ ⋯).WF

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