Documentation

Std.Data.DTreeMap.Raw.WF

Well-formedness proofs for raw dependent tree maps #

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

@[instance_reducible]

def Std.DTreeMap.Raw.WF.instCoeTypeForall {α : Type u} :

Coe (Type v) (α → Type v)

Equations

Std.DTreeMap.Raw.WF.instCoeTypeForall = { coe := fun (γ : Type ?u.1) (x : α) => γ }

Instances For

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

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

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

(t.erase a).WF

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

(t.insert a b).WF

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

(t.insertIfNew a b).WF

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

(t.containsThenInsert a b).snd.WF

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

(t.containsThenInsertIfNew a b).snd.WF

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

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

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

(Raw.filter f t).WF

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

(Raw.filterMap f t).WF

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

(partition f t).fst.WF

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

(partition f t).snd.WF

theorem Std.DTreeMap.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.DTreeMap.Raw.WF.insertMany {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] {ρ : Type u_1} [ForIn Id ρ ((a : α) × β a)] {l : ρ} {t : Raw α β cmp} (h : t.WF) :

(t.insertMany l).WF

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

(Raw.ofList l cmp).WF

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

(Raw.ofArray a cmp).WF

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

(t.alter a f).WF

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

(t.modify a f).WF

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

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

theorem Std.DTreeMap.Raw.WF.constGetThenInsertIfNew? {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Raw α (fun (x : α) => β) cmp} [TransCmp cmp] {a : α} {b : β} (h : t.WF) :

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

theorem Std.DTreeMap.Raw.WF.constInsertMany {α : Type u} {cmp : α → α → Ordering} {β : Type v} [TransCmp cmp] {ρ : Type u_1} [ForIn Id ρ (α × β)] {l : ρ} {t : Raw α (fun (x : α) => β) cmp} (h : t.WF) :

(Const.insertMany t l).WF

theorem Std.DTreeMap.Raw.WF.constInsertManyIfNewUnit {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] {ρ : Type u_1} [ForIn Id ρ α] {l : ρ} {t : Raw α (fun (x : α) => Unit) cmp} (h : t.WF) :

(Const.insertManyIfNewUnit t l).WF

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

(Const.ofList l cmp).WF

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

(Const.ofArray a cmp).WF

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

(Const.unitOfList l cmp).WF

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

(Const.unitOfArray a cmp).WF

theorem Std.DTreeMap.Raw.WF.constAlter {α : Type u} {cmp : α → α → Ordering} {β : Type v} {a : α} {f : Option β → Option β} {t : Raw α (fun (x : α) => β) cmp} (h : t.WF) :

(Const.alter t a f).WF

theorem Std.DTreeMap.Raw.WF.constModify {α : Type u} {cmp : α → α → Ordering} {β : Type v} {a : α} {f : β → β} {t : Raw α (fun (x : α) => β) cmp} (h : t.WF) :

(Const.modify t a f).WF

theorem Std.DTreeMap.Raw.WF.constMergeWith {α : Type u} {cmp : α → α → Ordering} {β : Type v} {mergeFn : α → β → β → β} {t₁ t₂ : Raw α (fun (x : α) => β) cmp} (h : t₁.WF) :

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

theorem Std.DTreeMap.Raw.WF.union {α : Type u} {cmp : α → α → Ordering} {β : Type v} [TransCmp cmp] {t₁ t₂ : Raw α (fun (x : α) => β) cmp} (h₁ : t₁.WF) (h₂ : t₂.WF) :

(t₁ ∪ t₂).WF

theorem Std.DTreeMap.Raw.WF.inter {α : Type u} {cmp : α → α → Ordering} {β : Type v} [TransCmp cmp] {t₁ t₂ : Raw α (fun (x : α) => β) cmp} (h₁ : t₁.WF) :

(t₁ ∩ t₂).WF

theorem Std.DTreeMap.Raw.WF.diff {α : Type u} {cmp : α → α → Ordering} {β : Type v} [TransCmp cmp] {t₁ t₂ : Raw α (fun (x : α) => β) cmp} (h₁ : t₁.WF) :

(t₁ \ t₂).WF