Documentation

Std.Data.TreeMap.Raw.WF

Well-formedness proofs for raw tree maps #

This file contains well-formedness proofs about Std.Data.TreeMap.Raw.Basic. Most of the lemmas require TransCmp cmp for the comparison function cmp.

theorem Std.TreeMap.Raw.WF.empty {α : Type u} {β : Type v} {cmp : α → α → Ordering} :

theorem Std.TreeMap.Raw.WF.emptyc {α : Type u} {β : Type v} {cmp : α → α → Ordering} :

theorem Std.TreeMap.Raw.WF.erase {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] {a : α} (h : t.WF) :

(t.erase a).WF

theorem Std.TreeMap.Raw.WF.insert {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] {a : α} {b : β} (h : t.WF) :

(t.insert a b).WF

theorem Std.TreeMap.Raw.WF.insertIfNew {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] {a : α} {b : β} (h : t.WF) :

(t.insertIfNew a b).WF

theorem Std.TreeMap.Raw.WF.containsThenInsert {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] {a : α} {b : β} (h : t.WF) :

(t.containsThenInsert a b).snd.WF

theorem Std.TreeMap.Raw.WF.containsThenInsertIfNew {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] {a : α} {b : β} (h : t.WF) :

(t.containsThenInsertIfNew a b).snd.WF

theorem Std.TreeMap.Raw.WF.getThenInsertIfNew? {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] {a : α} {b : β} (h : t.WF) :

(t.getThenInsertIfNew? a b).snd.WF

theorem Std.TreeMap.Raw.WF.filter {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] {f : α → β → Bool} (h : t.WF) :

(Raw.filter f t).WF

theorem Std.TreeMap.Raw.WF.filterMap {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] {f : α → β → Option β} (h : t.WF) :

(Raw.filterMap f t).WF

theorem Std.TreeMap.Raw.WF.partition_fst {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] {f : α → β → Bool} :

(partition f t).fst.WF

theorem Std.TreeMap.Raw.WF.partition_snd {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] {f : α → β → Bool} :

(partition f t).snd.WF

theorem Std.TreeMap.Raw.WF.eraseMany {α : Type u} {β : Type v} {cmp : α → α → Ordering} [TransCmp cmp] {ρ : Type u_1} [ForIn Id ρ α] {l : ρ} {t : Raw α β cmp} (h : t.WF) :

(t.eraseMany l).WF

theorem Std.TreeMap.Raw.WF.insertMany {α : Type u} {β : Type v} {cmp : α → α → Ordering} [TransCmp cmp] {ρ : Type u_1} [ForIn Id ρ (α × β)] {l : ρ} {t : Raw α β cmp} (h : t.WF) :

(t.insertMany l).WF

theorem Std.TreeMap.Raw.WF.insertManyIfNewUnit {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] {ρ : Type u_1} [ForIn Id ρ α] {l : ρ} {t : Raw α Unit cmp} (h : t.WF) :

(t.insertManyIfNewUnit l).WF

theorem Std.TreeMap.Raw.WF.ofList {α : Type u} {β : Type v} {cmp : α → α → Ordering} [TransCmp cmp] {l : List (α × β)} :

(Raw.ofList l cmp).WF

theorem Std.TreeMap.Raw.WF.ofArray {α : Type u} {β : Type v} {cmp : α → α → Ordering} [TransCmp cmp] {a : Array (α × β)} :

(Raw.ofArray a cmp).WF

theorem Std.TreeMap.Raw.WF.alter {α : Type u} {β : Type v} {cmp : α → α → Ordering} {a : α} {f : Option β → Option β} {t : Raw α β cmp} (h : t.WF) :

(t.alter a f).WF

theorem Std.TreeMap.Raw.WF.modify {α : Type u} {β : Type v} {cmp : α → α → Ordering} {a : α} {f : β → β} {t : Raw α β cmp} (h : t.WF) :

(t.modify a f).WF

theorem Std.TreeMap.Raw.WF.unitOfList {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] {l : List α} :

(Raw.unitOfList l cmp).WF

theorem Std.TreeMap.Raw.WF.unitOfArray {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] {a : Array α} :

(Raw.unitOfArray a cmp).WF

theorem Std.TreeMap.Raw.WF.mergeWith {α : Type u} {β : Type v} {cmp : α → α → Ordering} {mergeFn : α → β → β → β} {t₁ t₂ : Raw α β cmp} (h : t₁.WF) :

(Raw.mergeWith mergeFn t₁ t₂).WF