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.
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.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.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.modify
{α : Type u}
{β : α → Type v}
{cmp : α → α → Ordering}
[LawfulEqCmp cmp]
{a : α}
{f : β a → β a}
{t : Raw α β cmp}
(h : t.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.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.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