feat: tree map lemmas for ofList (#7360)
This PR provides lemmas about the tree map function `ofList` and interactions with other functions for which lemmas already exist. --------- Co-authored-by: Paul Reichert <6992158+datokrat@users.noreply.github.com>
This commit is contained in:
Paul Reichert
GitHub
parent
20d191bc8e
commit
d0f4e7c590
8 changed files with 1475 additions and 3 deletions
|
|
@ -2235,8 +2235,7 @@ theorem isEmpty_unitOfList [EquivBEq α] [LawfulHashable α]
|
|||
@[simp]
|
||||
theorem get?_unitOfList [EquivBEq α] [LawfulHashable α]
|
||||
{l : List α} {k : α} :
|
||||
get? (unitOfList l) k =
|
||||
if l.contains k then some () else none := by
|
||||
get? (unitOfList l) k = if l.contains k then some () else none := by
|
||||
simp_to_raw using Raw₀.Const.get?_insertManyIfNewUnit_empty_list
|
||||
|
||||
@[simp]
|
||||
|
|
|
|||
|
|
@ -2726,4 +2726,301 @@ theorem getKeyD_insertMany_empty_list_of_mem [TransOrd α]
|
|||
(insertMany empty l WF.empty.balanced).1.getKeyD k' fallback = k := by
|
||||
rw [getKeyD_insertMany_list_of_mem WF.empty k_beq distinct mem]
|
||||
|
||||
theorem size_insertMany_empty_list [TransOrd α]
|
||||
{l : List ((a : α) × β a)} (distinct : l.Pairwise (fun a b => ¬ compare a.1 b.1 = .eq)) :
|
||||
(insertMany empty l WF.empty.balanced).1.size = l.length := by
|
||||
rw [size_insertMany_list WF.empty distinct]
|
||||
· simp only [size_empty, Nat.zero_add]
|
||||
· simp only [contains_empty, Bool.false_eq_true, false_implies, implies_true]
|
||||
|
||||
theorem size_insertMany_empty_list_le [TransOrd α]
|
||||
{l : List ((a : α) × β a)} :
|
||||
(insertMany empty l WF.empty.balanced).1.size ≤ l.length := by
|
||||
rw [← Nat.zero_add l.length]
|
||||
apply size_insertMany_list_le WF.empty
|
||||
|
||||
theorem isEmpty_insertMany_empty_list [TransOrd α]
|
||||
{l : List ((a : α) × β a)} :
|
||||
(insertMany empty l WF.empty.balanced).1.isEmpty = l.isEmpty := by
|
||||
simp [isEmpty_insertMany_list WF.empty, isEmpty_empty]
|
||||
|
||||
namespace Const
|
||||
variable {β : Type v}
|
||||
|
||||
@[simp]
|
||||
theorem insertMany_empty_list_nil :
|
||||
(insertMany empty ([] : List (α × β)) WF.empty.balanced).1 = empty := by
|
||||
rfl
|
||||
|
||||
@[simp]
|
||||
theorem insertMany_empty_list_singleton {k : α} {v : β} :
|
||||
(insertMany empty [⟨k, v⟩] WF.empty.balanced).1 = (empty.insert k v WF.empty.balanced).impl := by
|
||||
rfl
|
||||
|
||||
theorem insertMany_empty_list_cons {k : α} {v : β}
|
||||
{tl : List (α × β)} :
|
||||
(insertMany empty (⟨k, v⟩ :: tl) WF.empty.balanced) =
|
||||
(insertMany (empty.insert k v WF.empty.balanced).1 tl WF.empty.insert.balanced).1 := by
|
||||
rw [insertMany_cons WF.empty]
|
||||
|
||||
theorem insertMany_empty_list_cons_eq_insertMany! {k : α} {v : β}
|
||||
{tl : List (α × β)} :
|
||||
(insertMany empty (⟨k, v⟩ :: tl) WF.empty.balanced) =
|
||||
(insertMany! (empty.insert! k v) tl).1 := by
|
||||
rw [insertMany_cons WF.empty, insertMany_eq_insertMany!, insert_eq_insert!]
|
||||
|
||||
theorem contains_insertMany_empty_list [TransOrd α] [BEq α] [LawfulBEqOrd α]
|
||||
{l : List (α × β)} {k : α} :
|
||||
(insertMany (empty : Impl α β) l WF.empty.balanced).1.contains k =
|
||||
(l.map Prod.fst).contains k := by
|
||||
simp [contains_insertMany_list WF.empty, contains_empty]
|
||||
|
||||
theorem get?_insertMany_empty_list_of_contains_eq_false [TransOrd α] [BEq α] [LawfulBEqOrd α]
|
||||
{l : List (α × β)} {k : α} (h : (l.map Prod.fst).contains k = false) :
|
||||
get? (insertMany (empty : Impl α β) l WF.empty.balanced).1 k = none := by
|
||||
rw [get?_insertMany_list_of_contains_eq_false WF.empty h]
|
||||
apply get?_empty
|
||||
|
||||
theorem get?_insertMany_empty_list_of_mem [TransOrd α]
|
||||
{l : List (α × β)} {k k' : α} (k_beq : compare k k' = .eq) {v : β}
|
||||
(distinct : l.Pairwise (fun a b => ¬ compare a.1 b.1 = .eq))
|
||||
(mem : ⟨k, v⟩ ∈ l) :
|
||||
get? (insertMany (empty : Impl α β) l WF.empty.balanced) k' = some v := by
|
||||
rw [get?_insertMany_list_of_mem WF.empty k_beq distinct mem]
|
||||
|
||||
theorem get_insertMany_empty_list_of_mem [TransOrd α]
|
||||
{l : List (α × β)} {k k' : α} (k_beq : compare k k' = .eq) {v : β}
|
||||
(distinct : l.Pairwise (fun a b => ¬ compare a.1 b.1 = .eq))
|
||||
(mem : ⟨k, v⟩ ∈ l)
|
||||
{h} :
|
||||
get (insertMany (empty : Impl α β) l WF.empty.balanced) k' h = v := by
|
||||
rw [get_insertMany_list_of_mem WF.empty k_beq distinct mem]
|
||||
|
||||
theorem get!_insertMany_empty_list_of_contains_eq_false [TransOrd α] [BEq α] [LawfulBEqOrd α]
|
||||
{l : List (α × β)} {k : α} [Inhabited β]
|
||||
(h : (l.map Prod.fst).contains k = false) :
|
||||
get! (insertMany (empty : Impl α β) l WF.empty.balanced) k = (default : β) := by
|
||||
rw [get!_insertMany_list_of_contains_eq_false WF.empty h]
|
||||
apply get!_empty
|
||||
|
||||
theorem get!_insertMany_empty_list_of_mem [TransOrd α]
|
||||
{l : List (α × β)} {k k' : α} (k_beq : compare k k' = .eq) {v : β} [Inhabited β]
|
||||
(distinct : l.Pairwise (fun a b => ¬ compare a.1 b.1 = .eq))
|
||||
(mem : ⟨k, v⟩ ∈ l) :
|
||||
get! (insertMany (empty : Impl α β) l WF.empty.balanced) k' = v := by
|
||||
rw [get!_insertMany_list_of_mem WF.empty k_beq distinct mem]
|
||||
|
||||
theorem getD_insertMany_empty_list_of_contains_eq_false [TransOrd α] [BEq α] [LawfulBEqOrd α]
|
||||
{l : List (α × β)} {k : α} {fallback : β}
|
||||
(contains_eq_false : (l.map Prod.fst).contains k = false) :
|
||||
getD (insertMany (empty : Impl α β) l WF.empty.balanced) k fallback = fallback := by
|
||||
rw [getD_insertMany_list_of_contains_eq_false WF.empty contains_eq_false]
|
||||
apply getD_empty
|
||||
|
||||
theorem getD_insertMany_empty_list_of_mem [TransOrd α]
|
||||
{l : List (α × β)} {k k' : α} (k_beq : compare k k' = .eq) {v : β} {fallback : β}
|
||||
(distinct : l.Pairwise (fun a b => ¬ compare a.1 b.1 = .eq))
|
||||
(mem : ⟨k, v⟩ ∈ l) :
|
||||
getD (insertMany (empty : Impl α β) l WF.empty.balanced) k' fallback = v := by
|
||||
rw [getD_insertMany_list_of_mem WF.empty k_beq distinct mem]
|
||||
|
||||
theorem getKey?_insertMany_empty_list_of_contains_eq_false [TransOrd α] [BEq α] [LawfulBEqOrd α]
|
||||
{l : List (α × β)} {k : α}
|
||||
(h : (l.map Prod.fst).contains k = false) :
|
||||
(insertMany (empty : Impl α β) l WF.empty.balanced).1.getKey? k = none := by
|
||||
rw [getKey?_insertMany_list_of_contains_eq_false WF.empty h]
|
||||
apply getKey?_empty
|
||||
|
||||
theorem getKey?_insertMany_empty_list_of_mem [TransOrd α]
|
||||
{l : List (α × β)}
|
||||
{k k' : α} (k_beq : compare k k' = .eq)
|
||||
(distinct : l.Pairwise (fun a b => ¬ compare a.1 b.1 = .eq))
|
||||
(mem : k ∈ l.map Prod.fst) :
|
||||
(insertMany (empty : Impl α β) l WF.empty.balanced).1.getKey? k' = some k := by
|
||||
rw [getKey?_insertMany_list_of_mem WF.empty k_beq distinct mem]
|
||||
|
||||
theorem getKey_insertMany_empty_list_of_mem [TransOrd α]
|
||||
{l : List (α × β)}
|
||||
{k k' : α} (k_beq : compare k k' = .eq)
|
||||
(distinct : l.Pairwise (fun a b => ¬ compare a.1 b.1 = .eq))
|
||||
(mem : k ∈ l.map Prod.fst)
|
||||
{h'} :
|
||||
(insertMany (empty : Impl α β) l WF.empty.balanced).1.getKey k' h' = k := by
|
||||
rw [getKey_insertMany_list_of_mem WF.empty k_beq distinct mem]
|
||||
|
||||
theorem getKey!_insertMany_empty_list_of_contains_eq_false [TransOrd α] [BEq α] [LawfulBEqOrd α]
|
||||
[Inhabited α] {l : List (α × β)} {k : α}
|
||||
(h : (l.map Prod.fst).contains k = false) :
|
||||
(insertMany (empty : Impl α β) l WF.empty.balanced).1.getKey! k = default := by
|
||||
rw [getKey!_insertMany_list_of_contains_eq_false WF.empty h]
|
||||
apply getKey!_empty
|
||||
|
||||
theorem getKey!_insertMany_empty_list_of_mem [TransOrd α] [Inhabited α]
|
||||
{l : List (α × β)}
|
||||
{k k' : α} (k_beq : compare k k' = .eq)
|
||||
(distinct : l.Pairwise (fun a b => ¬ compare a.1 b.1 = .eq))
|
||||
(mem : k ∈ l.map Prod.fst) :
|
||||
(insertMany (empty : Impl α β) l WF.empty.balanced).1.getKey! k' = k := by
|
||||
rw [getKey!_insertMany_list_of_mem WF.empty k_beq distinct mem]
|
||||
|
||||
theorem getKeyD_insertMany_empty_list_of_contains_eq_false [TransOrd α] [BEq α] [LawfulBEqOrd α]
|
||||
{l : List (α × β)} {k fallback : α}
|
||||
(h : (l.map Prod.fst).contains k = false) :
|
||||
(insertMany (empty : Impl α β) l WF.empty.balanced).1.getKeyD k fallback = fallback := by
|
||||
rw [getKeyD_insertMany_list_of_contains_eq_false WF.empty h]
|
||||
apply getKeyD_empty
|
||||
|
||||
theorem getKeyD_insertMany_empty_list_of_mem [TransOrd α]
|
||||
{l : List (α × β)}
|
||||
{k k' fallback : α} (k_beq : compare k k' = .eq)
|
||||
(distinct : l.Pairwise (fun a b => ¬ compare a.1 b.1 = .eq))
|
||||
(mem : k ∈ l.map Prod.fst) :
|
||||
(insertMany (empty : Impl α β) l WF.empty.balanced).1.getKeyD k' fallback = k := by
|
||||
rw [getKeyD_insertMany_list_of_mem WF.empty k_beq distinct mem]
|
||||
|
||||
theorem size_insertMany_empty_list [TransOrd α]
|
||||
{l : List (α × β)} (distinct : l.Pairwise (fun a b => ¬ compare a.1 b.1 = .eq)) :
|
||||
(insertMany (empty : Impl α β) l WF.empty.balanced).1.size = l.length := by
|
||||
rw [size_insertMany_list WF.empty distinct]
|
||||
· simp only [size_empty, Nat.zero_add]
|
||||
· simp only [contains_empty, Bool.false_eq_true, false_implies, implies_true]
|
||||
|
||||
theorem size_insertMany_empty_list_le [TransOrd α]
|
||||
{l : List (α × β)} :
|
||||
(insertMany (empty : Impl α β) l WF.empty.balanced).1.size ≤ l.length := by
|
||||
rw [← Nat.zero_add l.length]
|
||||
apply (size_insertMany_list_le WF.empty)
|
||||
|
||||
theorem isEmpty_insertMany_empty_list [TransOrd α]
|
||||
{l : List (α × β)} :
|
||||
(insertMany (empty : Impl α β) l WF.empty.balanced).1.isEmpty = l.isEmpty := by
|
||||
simp [isEmpty_insertMany_list WF.empty, isEmpty_empty]
|
||||
|
||||
@[simp]
|
||||
theorem insertManyIfNewUnit_empty_list_nil :
|
||||
insertManyIfNewUnit (empty : Impl α Unit) ([] : List α) WF.empty.balanced =
|
||||
(empty : Impl α Unit) :=
|
||||
rfl
|
||||
|
||||
@[simp]
|
||||
theorem insertManyIfNewUnit_empty_list_singleton {k : α} :
|
||||
(insertManyIfNewUnit (empty : Impl α Unit) [k] WF.empty.balanced).1 =
|
||||
(empty.insertIfNew k () WF.empty.balanced).1 :=
|
||||
rfl
|
||||
|
||||
theorem insertManyIfNewUnit_empty_list_cons {hd : α} {tl : List α} :
|
||||
(insertManyIfNewUnit (empty : Impl α Unit) (hd :: tl) WF.empty.balanced).1 =
|
||||
(insertManyIfNewUnit (empty.insertIfNew hd () WF.empty.balanced).1 tl
|
||||
WF.empty.insertIfNew.balanced).1 := by
|
||||
rw [insertManyIfNewUnit_cons WF.empty]
|
||||
|
||||
theorem insertManyIfNewUnit_empty_list_cons_eq_insertManyIfNewUnit! {hd : α} {tl : List α} :
|
||||
(insertManyIfNewUnit (empty : Impl α Unit) (hd :: tl) WF.empty.balanced).1 =
|
||||
(insertManyIfNewUnit! (empty.insertIfNew! hd ()) tl).1 := by
|
||||
rw [insertManyIfNewUnit_empty_list_cons, insertManyIfNewUnit_eq_insertManyIfNewUnit!,
|
||||
insertIfNew_eq_insertIfNew!]
|
||||
|
||||
theorem contains_insertManyIfNewUnit_empty_list [TransOrd α] [BEq α] [LawfulBEqOrd α]
|
||||
{l : List α} {k : α} :
|
||||
(insertManyIfNewUnit (empty : Impl α Unit) l WF.empty.balanced).1.contains k =
|
||||
l.contains k := by
|
||||
simp [contains_insertManyIfNewUnit_list WF.empty, contains_empty]
|
||||
|
||||
theorem getKey?_insertManyIfNewUnit_empty_list_of_contains_eq_false [TransOrd α] [BEq α]
|
||||
[LawfulBEqOrd α] {l : List α} {k : α} (h' : l.contains k = false) :
|
||||
getKey? (insertManyIfNewUnit (empty : Impl α Unit) l WF.empty.balanced).1 k = none := by
|
||||
exact getKey?_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false WF.empty
|
||||
not_mem_empty h'
|
||||
|
||||
theorem getKey?_insertManyIfNewUnit_empty_list_of_mem [TransOrd α]
|
||||
{l : List α} {k k' : α} (k_beq : compare k k' = .eq)
|
||||
(distinct : l.Pairwise (fun a b => ¬ compare a b = .eq)) (mem : k ∈ l) :
|
||||
getKey? (insertManyIfNewUnit (empty : Impl α Unit) l WF.empty.balanced).1 k' = some k := by
|
||||
exact getKey?_insertManyIfNewUnit_list_of_not_mem_of_mem WF.empty k_beq
|
||||
not_mem_empty distinct mem
|
||||
|
||||
theorem getKey_insertManyIfNewUnit_empty_list_of_mem [TransOrd α]
|
||||
{l : List α}
|
||||
{k k' : α} (k_beq : compare k k' = .eq)
|
||||
(distinct : l.Pairwise (fun a b => ¬ compare a b = .eq))
|
||||
(mem : k ∈ l) {h'} :
|
||||
getKey (insertManyIfNewUnit (empty : Impl α Unit) l WF.empty.balanced).1 k' h' = k := by
|
||||
exact getKey_insertManyIfNewUnit_list_of_not_mem_of_mem WF.empty k_beq
|
||||
not_mem_empty distinct mem
|
||||
|
||||
theorem getKey!_insertManyIfNewUnit_empty_list_of_contains_eq_false [TransOrd α] [BEq α]
|
||||
[LawfulBEqOrd α] [Inhabited α] {l : List α} {k : α}
|
||||
(h' : l.contains k = false) :
|
||||
getKey! (insertManyIfNewUnit (empty : Impl α Unit) l WF.empty.balanced).1 k = default := by
|
||||
exact getKey!_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false WF.empty
|
||||
not_mem_empty h'
|
||||
|
||||
theorem getKey!_insertManyIfNewUnit_empty_list_of_mem [TransOrd α]
|
||||
[Inhabited α] {l : List α} {k k' : α} (k_beq : compare k k' = .eq)
|
||||
(distinct : l.Pairwise (fun a b => ¬ compare a b = .eq))
|
||||
(mem : k ∈ l) :
|
||||
getKey! (insertManyIfNewUnit (empty : Impl α Unit) l WF.empty.balanced).1 k' = k := by
|
||||
exact getKey!_insertManyIfNewUnit_list_of_not_mem_of_mem WF.empty k_beq
|
||||
not_mem_empty distinct mem
|
||||
|
||||
theorem getKeyD_insertManyIfNewUnit_empty_list_of_contains_eq_false [TransOrd α] [BEq α]
|
||||
[LawfulBEqOrd α] {l : List α} {k fallback : α}
|
||||
(h' : l.contains k = false) :
|
||||
getKeyD (insertManyIfNewUnit (empty : Impl α Unit) l WF.empty.balanced).1 k fallback =
|
||||
fallback := by
|
||||
exact getKeyD_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false
|
||||
WF.empty not_mem_empty h'
|
||||
|
||||
theorem getKeyD_insertManyIfNewUnit_empty_list_of_mem [TransOrd α]
|
||||
{l : List α} {k k' fallback : α} (k_beq : compare k k' = .eq)
|
||||
(distinct : l.Pairwise (fun a b => ¬ compare a b = .eq))
|
||||
(mem : k ∈ l) :
|
||||
getKeyD (insertManyIfNewUnit (empty : Impl α Unit) l WF.empty.balanced).1 k' fallback = k := by
|
||||
exact getKeyD_insertManyIfNewUnit_list_of_not_mem_of_mem WF.empty k_beq
|
||||
not_mem_empty distinct mem
|
||||
|
||||
theorem size_insertManyIfNewUnit_empty_list [TransOrd α]
|
||||
{l : List α}
|
||||
(distinct : l.Pairwise (fun a b => ¬ compare a b = .eq)) :
|
||||
(insertManyIfNewUnit (empty : Impl α Unit) l WF.empty.balanced).1.size = l.length := by
|
||||
rw [size_insertManyIfNewUnit_list WF.empty distinct]
|
||||
· simp [size_empty]
|
||||
· simp [not_mem_empty]
|
||||
|
||||
theorem size_insertManyIfNewUnit_empty_list_le [TransOrd α]
|
||||
{l : List α} :
|
||||
(insertManyIfNewUnit (empty : Impl α Unit) l WF.empty.balanced).1.size ≤ l.length := by
|
||||
apply Nat.le_trans (size_insertManyIfNewUnit_list_le WF.empty)
|
||||
simp [size_empty]
|
||||
|
||||
theorem isEmpty_insertManyIfNewUnit_empty_list [TransOrd α]
|
||||
{l : List α} :
|
||||
(insertManyIfNewUnit (empty : Impl α Unit) l WF.empty.balanced).1.isEmpty = l.isEmpty := by
|
||||
rw [isEmpty_insertManyIfNewUnit_list WF.empty]
|
||||
simp [isEmpty_empty]
|
||||
|
||||
theorem get?_insertManyIfNewUnit_empty_list [TransOrd α] [BEq α] [LawfulBEqOrd α]
|
||||
{l : List α} {k : α} :
|
||||
get? (insertManyIfNewUnit (empty : Impl α Unit) l WF.empty.balanced) k =
|
||||
if l.contains k then some () else none := by
|
||||
rw [get?_insertManyIfNewUnit_list WF.empty]
|
||||
simp [not_mem_empty]
|
||||
|
||||
theorem get_insertManyIfNewUnit_empty_list
|
||||
{l : List α} {k : α} {h} :
|
||||
get (insertManyIfNewUnit (empty : Impl α Unit) l WF.empty.balanced) k h = () := by
|
||||
simp
|
||||
|
||||
theorem get!_insertManyIfNewUnit_empty_list
|
||||
{l : List α} {k : α} :
|
||||
get! (insertManyIfNewUnit (empty : Impl α Unit) l WF.empty.balanced) k = () := by
|
||||
simp
|
||||
|
||||
theorem getD_insertManyIfNewUnit_empty_list
|
||||
{l : List α} {k : α} {fallback : Unit} :
|
||||
getD (insertManyIfNewUnit (empty : Impl α Unit) l WF.empty.balanced) k fallback = () := by
|
||||
simp
|
||||
|
||||
end Const
|
||||
|
||||
end Std.DTreeMap.Internal.Impl
|
||||
|
|
|
|||
|
|
@ -1761,4 +1761,265 @@ theorem getKeyD_ofList_of_mem [TransCmp cmp]
|
|||
(ofList l cmp).getKeyD k' fallback = k :=
|
||||
Impl.getKeyD_insertMany_empty_list_of_mem k_eq distinct mem
|
||||
|
||||
theorem size_ofList [TransCmp cmp]
|
||||
{l : List ((a : α) × β a)} (distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq)) :
|
||||
(ofList l cmp).size = l.length :=
|
||||
Impl.size_insertMany_empty_list distinct
|
||||
|
||||
theorem size_ofList_le [TransCmp cmp] {l : List ((a : α) × β a)} :
|
||||
(ofList l cmp).1.size ≤ l.length :=
|
||||
Impl.size_insertMany_empty_list_le
|
||||
|
||||
@[simp]
|
||||
theorem isEmpty_ofList [TransCmp cmp] {l : List ((a : α) × β a)} :
|
||||
(ofList l cmp).1.isEmpty = l.isEmpty :=
|
||||
Impl.isEmpty_insertMany_empty_list
|
||||
|
||||
namespace Const
|
||||
|
||||
variable {β : Type v}
|
||||
|
||||
@[simp]
|
||||
theorem ofList_nil :
|
||||
ofList ([] : List (α × β)) cmp = ∅ := by
|
||||
rfl
|
||||
|
||||
@[simp]
|
||||
theorem ofList_singleton {k : α} {v : β} :
|
||||
ofList [⟨k, v⟩] cmp = (∅ : DTreeMap α β cmp).insert k v := by
|
||||
rfl
|
||||
|
||||
theorem ofList_cons {k : α} {v : β} {tl : List (α × β)} :
|
||||
ofList (⟨k, v⟩ :: tl) cmp = insertMany ((∅ : DTreeMap α β cmp).insert k v) tl :=
|
||||
ext Impl.Const.insertMany_empty_list_cons
|
||||
|
||||
@[simp]
|
||||
theorem contains_ofList [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List (α × β)} {k : α} :
|
||||
(ofList l cmp).contains k = (l.map Prod.fst).contains k :=
|
||||
Impl.Const.contains_insertMany_empty_list
|
||||
|
||||
@[simp]
|
||||
theorem mem_ofList [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List (α × β)} {k : α} :
|
||||
k ∈ ofList l cmp ↔ (l.map Prod.fst).contains k := by
|
||||
simp [mem_iff_contains]
|
||||
|
||||
theorem get?_ofList_of_contains_eq_false [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
|
||||
{l : List (α × β)} {k : α}
|
||||
(contains_eq_false : (l.map Prod.fst).contains k = false) :
|
||||
get? (ofList l cmp) k = none :=
|
||||
Impl.Const.get?_insertMany_empty_list_of_contains_eq_false contains_eq_false
|
||||
|
||||
theorem get?_ofList_of_mem [TransCmp cmp]
|
||||
{l : List (α × β)} {k k' : α} (k_eq : cmp k k' = .eq) {v : β}
|
||||
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
|
||||
(mem : ⟨k, v⟩ ∈ l) :
|
||||
get? (ofList l cmp) k' = some v :=
|
||||
Impl.Const.get?_insertMany_empty_list_of_mem k_eq distinct mem
|
||||
|
||||
theorem get_ofList_of_mem [TransCmp cmp]
|
||||
{l : List (α × β)} {k k' : α} (k_eq : cmp k k' = .eq) {v : β}
|
||||
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
|
||||
(mem : ⟨k, v⟩ ∈ l)
|
||||
{h} :
|
||||
get (ofList l cmp) k' h = v :=
|
||||
Impl.Const.get_insertMany_empty_list_of_mem k_eq distinct mem
|
||||
|
||||
theorem get!_ofList_of_contains_eq_false [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
|
||||
{l : List (α × β)} {k : α} [Inhabited β]
|
||||
(contains_eq_false : (l.map Prod.fst).contains k = false) :
|
||||
get! (ofList l cmp) k = default :=
|
||||
Impl.Const.get!_insertMany_empty_list_of_contains_eq_false contains_eq_false
|
||||
|
||||
theorem get!_ofList_of_mem [TransCmp cmp]
|
||||
{l : List (α × β)} {k k' : α} (k_eq : cmp k k' = .eq) {v : β} [Inhabited β]
|
||||
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
|
||||
(mem : ⟨k, v⟩ ∈ l) :
|
||||
get! (ofList l cmp) k' = v :=
|
||||
Impl.Const.get!_insertMany_empty_list_of_mem k_eq distinct mem
|
||||
|
||||
theorem getD_ofList_of_contains_eq_false [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
|
||||
{l : List (α × β)} {k : α} {fallback : β}
|
||||
(contains_eq_false : (l.map Prod.fst).contains k = false) :
|
||||
getD (ofList l cmp) k fallback = fallback :=
|
||||
Impl.Const.getD_insertMany_empty_list_of_contains_eq_false contains_eq_false
|
||||
|
||||
theorem getD_ofList_of_mem [TransCmp cmp]
|
||||
{l : List (α × β)} {k k' : α} (k_eq : cmp k k' = .eq) {v : β} {fallback : β}
|
||||
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
|
||||
(mem : ⟨k, v⟩ ∈ l) :
|
||||
getD (ofList l cmp) k' fallback = v :=
|
||||
Impl.Const.getD_insertMany_empty_list_of_mem k_eq distinct mem
|
||||
|
||||
theorem getKey?_ofList_of_contains_eq_false [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
|
||||
{l : List (α × β)} {k : α}
|
||||
(contains_eq_false : (l.map Prod.fst).contains k = false) :
|
||||
(ofList l cmp).getKey? k = none :=
|
||||
Impl.Const.getKey?_insertMany_empty_list_of_contains_eq_false contains_eq_false
|
||||
|
||||
theorem getKey?_ofList_of_mem [TransCmp cmp]
|
||||
{l : List (α × β)}
|
||||
{k k' : α} (k_eq : cmp k k' = .eq)
|
||||
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
|
||||
(mem : k ∈ l.map Prod.fst) :
|
||||
(ofList l cmp).getKey? k' = some k :=
|
||||
Impl.Const.getKey?_insertMany_empty_list_of_mem k_eq distinct mem
|
||||
|
||||
theorem getKey_ofList_of_mem [TransCmp cmp]
|
||||
{l : List (α × β)}
|
||||
{k k' : α} (k_eq : cmp k k' = .eq)
|
||||
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
|
||||
(mem : k ∈ l.map Prod.fst)
|
||||
{h'} :
|
||||
(ofList l cmp).getKey k' h' = k :=
|
||||
Impl.Const.getKey_insertMany_empty_list_of_mem k_eq distinct mem
|
||||
|
||||
theorem getKey!_ofList_of_contains_eq_false [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
|
||||
[Inhabited α] {l : List (α × β)} {k : α}
|
||||
(contains_eq_false : (l.map Prod.fst).contains k = false) :
|
||||
(ofList l cmp).getKey! k = default :=
|
||||
Impl.Const.getKey!_insertMany_empty_list_of_contains_eq_false contains_eq_false
|
||||
|
||||
theorem getKey!_ofList_of_mem [TransCmp cmp] [Inhabited α]
|
||||
{l : List (α × β)}
|
||||
{k k' : α} (k_eq : cmp k k' = .eq)
|
||||
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
|
||||
(mem : k ∈ l.map Prod.fst) :
|
||||
(ofList l cmp).getKey! k' = k :=
|
||||
Impl.Const.getKey!_insertMany_empty_list_of_mem k_eq distinct mem
|
||||
|
||||
theorem getKeyD_ofList_of_contains_eq_false [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
|
||||
{l : List (α × β)} {k fallback : α}
|
||||
(contains_eq_false : (l.map Prod.fst).contains k = false) :
|
||||
(ofList l cmp).getKeyD k fallback = fallback :=
|
||||
Impl.Const.getKeyD_insertMany_empty_list_of_contains_eq_false contains_eq_false
|
||||
|
||||
theorem getKeyD_ofList_of_mem [TransCmp cmp]
|
||||
{l : List (α × β)}
|
||||
{k k' fallback : α} (k_eq : cmp k k' = .eq)
|
||||
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
|
||||
(mem : k ∈ l.map Prod.fst) :
|
||||
(ofList l cmp).getKeyD k' fallback = k :=
|
||||
Impl.Const.getKeyD_insertMany_empty_list_of_mem k_eq distinct mem
|
||||
|
||||
theorem size_ofList [TransCmp cmp] {l : List (α × β)}
|
||||
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq)) :
|
||||
(ofList l cmp).size = l.length :=
|
||||
Impl.Const.size_insertMany_empty_list distinct
|
||||
|
||||
theorem size_ofList_le [TransCmp cmp] {l : List (α × β)} :
|
||||
(ofList l cmp).size ≤ l.length :=
|
||||
Impl.Const.size_insertMany_empty_list_le
|
||||
|
||||
theorem isEmpty_ofList [TransCmp cmp] {l : List (α × β)} :
|
||||
(ofList l cmp).isEmpty = l.isEmpty :=
|
||||
Impl.Const.isEmpty_insertMany_empty_list
|
||||
|
||||
@[simp]
|
||||
theorem unitOfList_nil :
|
||||
unitOfList ([] : List α) cmp =
|
||||
(∅ : DTreeMap α Unit cmp) :=
|
||||
rfl
|
||||
|
||||
@[simp]
|
||||
theorem unitOfList_singleton {k : α} :
|
||||
unitOfList [k] cmp = (∅ : DTreeMap α Unit cmp).insertIfNew k () :=
|
||||
rfl
|
||||
|
||||
theorem unitOfList_cons {hd : α} {tl : List α} :
|
||||
unitOfList (hd :: tl) cmp =
|
||||
insertManyIfNewUnit ((∅ : DTreeMap α Unit cmp).insertIfNew hd ()) tl :=
|
||||
ext Impl.Const.insertManyIfNewUnit_empty_list_cons
|
||||
|
||||
@[simp]
|
||||
theorem contains_unitOfList [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List α} {k : α} :
|
||||
(unitOfList l cmp).contains k = l.contains k :=
|
||||
Impl.Const.contains_insertManyIfNewUnit_empty_list
|
||||
|
||||
@[simp]
|
||||
theorem mem_unitOfList [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List α} {k : α} :
|
||||
k ∈ unitOfList l cmp ↔ l.contains k := by
|
||||
simp [mem_iff_contains]
|
||||
|
||||
theorem getKey?_unitOfList_of_contains_eq_false [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
|
||||
{l : List α} {k : α}
|
||||
(contains_eq_false : l.contains k = false) :
|
||||
getKey? (unitOfList l cmp) k = none :=
|
||||
Impl.Const.getKey?_insertManyIfNewUnit_empty_list_of_contains_eq_false contains_eq_false
|
||||
|
||||
theorem getKey?_unitOfList_of_mem [TransCmp cmp]
|
||||
{l : List α} {k k' : α} (k_eq : cmp k k' = .eq)
|
||||
(distinct : l.Pairwise (fun a b => ¬ cmp a b = .eq)) (mem : k ∈ l) :
|
||||
getKey? (unitOfList l cmp) k' = some k :=
|
||||
Impl.Const.getKey?_insertManyIfNewUnit_empty_list_of_mem k_eq distinct mem
|
||||
|
||||
theorem getKey_unitOfList_of_mem [TransCmp cmp]
|
||||
{l : List α}
|
||||
{k k' : α} (k_eq : cmp k k' = .eq)
|
||||
(distinct : l.Pairwise (fun a b => ¬ cmp a b = .eq))
|
||||
(mem : k ∈ l) {h'} :
|
||||
getKey (unitOfList l cmp) k' h' = k :=
|
||||
Impl.Const.getKey_insertManyIfNewUnit_empty_list_of_mem k_eq distinct mem
|
||||
|
||||
theorem getKey!_unitOfList_of_contains_eq_false [TransCmp cmp] [BEq α]
|
||||
[LawfulBEqCmp cmp] [Inhabited α] {l : List α} {k : α}
|
||||
(contains_eq_false : l.contains k = false) :
|
||||
getKey! (unitOfList l cmp) k = default :=
|
||||
Impl.Const.getKey!_insertManyIfNewUnit_empty_list_of_contains_eq_false contains_eq_false
|
||||
|
||||
theorem getKey!_unitOfList_of_mem [TransCmp cmp]
|
||||
[Inhabited α] {l : List α} {k k' : α} (k_eq : cmp k k' = .eq)
|
||||
(distinct : l.Pairwise (fun a b => ¬ cmp a b = .eq))
|
||||
(mem : k ∈ l) :
|
||||
getKey! (unitOfList l cmp) k' = k :=
|
||||
Impl.Const.getKey!_insertManyIfNewUnit_empty_list_of_mem k_eq distinct mem
|
||||
|
||||
theorem getKeyD_unitOfList_of_contains_eq_false [TransCmp cmp] [BEq α]
|
||||
[LawfulBEqCmp cmp] {l : List α} {k fallback : α}
|
||||
(contains_eq_false : l.contains k = false) :
|
||||
getKeyD (unitOfList l cmp) k fallback = fallback :=
|
||||
Impl.Const.getKeyD_insertManyIfNewUnit_empty_list_of_contains_eq_false contains_eq_false
|
||||
|
||||
theorem getKeyD_unitOfList_of_mem [TransCmp cmp]
|
||||
{l : List α} {k k' fallback : α} (k_eq : cmp k k' = .eq)
|
||||
(distinct : l.Pairwise (fun a b => ¬ cmp a b = .eq))
|
||||
(mem : k ∈ l) :
|
||||
getKeyD (unitOfList l cmp) k' fallback = k :=
|
||||
Impl.Const.getKeyD_insertManyIfNewUnit_empty_list_of_mem k_eq distinct mem
|
||||
|
||||
theorem size_unitOfList [TransCmp cmp] {l : List α}
|
||||
(distinct : l.Pairwise (fun a b => ¬ cmp a b = .eq)) :
|
||||
(unitOfList l cmp).size = l.length :=
|
||||
Impl.Const.size_insertManyIfNewUnit_empty_list distinct
|
||||
|
||||
theorem size_unitOfList_le [TransCmp cmp] {l : List α} :
|
||||
(unitOfList l cmp).size ≤ l.length :=
|
||||
Impl.Const.size_insertManyIfNewUnit_empty_list_le
|
||||
|
||||
@[simp]
|
||||
theorem isEmpty_unitOfList [TransCmp cmp] {l : List α} :
|
||||
(unitOfList l cmp).isEmpty = l.isEmpty :=
|
||||
Impl.Const.isEmpty_insertManyIfNewUnit_empty_list
|
||||
|
||||
@[simp]
|
||||
theorem get?_unitOfList [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List α} {k : α} :
|
||||
get? (unitOfList l cmp) k = if l.contains k then some () else none :=
|
||||
Impl.Const.get?_insertManyIfNewUnit_empty_list
|
||||
|
||||
@[simp]
|
||||
theorem get_unitOfList {l : List α} {k : α} {h} :
|
||||
get (unitOfList l cmp) k h = () :=
|
||||
Impl.Const.get_insertManyIfNewUnit_empty_list
|
||||
|
||||
@[simp]
|
||||
theorem get!_unitOfList {l : List α} {k : α} :
|
||||
get! (unitOfList l cmp) k = () :=
|
||||
Impl.Const.get!_insertManyIfNewUnit_empty_list
|
||||
|
||||
@[simp]
|
||||
theorem getD_unitOfList {l : List α} {k : α} {fallback : Unit} :
|
||||
getD (unitOfList l cmp) k fallback = () :=
|
||||
Impl.Const.getD_insertManyIfNewUnit_empty_list
|
||||
|
||||
end Const
|
||||
|
||||
end Std.DTreeMap
|
||||
|
|
|
|||
|
|
@ -1653,7 +1653,7 @@ theorem ofList_singleton {k : α} {v : β k} :
|
|||
|
||||
theorem ofList_cons {k : α} {v : β k} {tl : List ((a : α) × (β a))} :
|
||||
ofList (⟨k, v⟩ :: tl) cmp = ((∅ : Raw α β cmp).insert k v).insertMany tl :=
|
||||
ext <| Impl.insertMany_empty_list_cons_eq_insertMany!
|
||||
ext Impl.insertMany_empty_list_cons_eq_insertMany!
|
||||
|
||||
@[simp]
|
||||
theorem contains_ofList [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
|
||||
|
|
@ -1766,4 +1766,265 @@ theorem getKeyD_ofList_of_mem [TransCmp cmp]
|
|||
(ofList l cmp).getKeyD k' fallback = k :=
|
||||
Impl.getKeyD_insertMany_empty_list_of_mem k_eq distinct mem
|
||||
|
||||
theorem size_ofList [TransCmp cmp]
|
||||
{l : List ((a : α) × β a)} (distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq)) :
|
||||
(ofList l cmp).size = l.length :=
|
||||
Impl.size_insertMany_empty_list distinct
|
||||
|
||||
theorem size_ofList_le [TransCmp cmp] {l : List ((a : α) × β a)} :
|
||||
(ofList l cmp).1.size ≤ l.length :=
|
||||
Impl.size_insertMany_empty_list_le
|
||||
|
||||
@[simp]
|
||||
theorem isEmpty_ofList [TransCmp cmp] {l : List ((a : α) × β a)} :
|
||||
(ofList l cmp).1.isEmpty = l.isEmpty :=
|
||||
Impl.isEmpty_insertMany_empty_list
|
||||
|
||||
namespace Const
|
||||
|
||||
variable {β : Type v}
|
||||
|
||||
@[simp]
|
||||
theorem ofList_nil :
|
||||
ofList ([] : List (α × β)) cmp = ∅ := by
|
||||
rfl
|
||||
|
||||
@[simp]
|
||||
theorem ofList_singleton {k : α} {v : β} :
|
||||
ofList [⟨k, v⟩] cmp = (∅ : Raw α β cmp).insert k v := by
|
||||
rfl
|
||||
|
||||
theorem ofList_cons {k : α} {v : β} {tl : List (α × β)} :
|
||||
ofList (⟨k, v⟩ :: tl) cmp = insertMany ((∅ : Raw α β cmp).insert k v) tl :=
|
||||
ext <| Impl.Const.insertMany_empty_list_cons_eq_insertMany!
|
||||
|
||||
@[simp]
|
||||
theorem contains_ofList [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List (α × β)} {k : α} :
|
||||
(ofList l cmp).contains k = (l.map Prod.fst).contains k :=
|
||||
Impl.Const.contains_insertMany_empty_list
|
||||
|
||||
@[simp]
|
||||
theorem mem_ofList [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List (α × β)} {k : α} :
|
||||
k ∈ ofList l cmp ↔ (l.map Prod.fst).contains k := by
|
||||
simp [mem_iff_contains]
|
||||
|
||||
theorem get?_ofList_of_contains_eq_false [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
|
||||
{l : List (α × β)} {k : α}
|
||||
(contains_eq_false : (l.map Prod.fst).contains k = false) :
|
||||
get? (ofList l cmp) k = none :=
|
||||
Impl.Const.get?_insertMany_empty_list_of_contains_eq_false contains_eq_false
|
||||
|
||||
theorem get?_ofList_of_mem [TransCmp cmp]
|
||||
{l : List (α × β)} {k k' : α} (k_eq : cmp k k' = .eq) {v : β}
|
||||
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
|
||||
(mem : ⟨k, v⟩ ∈ l) :
|
||||
get? (ofList l cmp) k' = some v :=
|
||||
Impl.Const.get?_insertMany_empty_list_of_mem k_eq distinct mem
|
||||
|
||||
theorem get_ofList_of_mem [TransCmp cmp]
|
||||
{l : List (α × β)} {k k' : α} (k_eq : cmp k k' = .eq) {v : β}
|
||||
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
|
||||
(mem : ⟨k, v⟩ ∈ l)
|
||||
{h} :
|
||||
get (ofList l cmp) k' h = v :=
|
||||
Impl.Const.get_insertMany_empty_list_of_mem k_eq distinct mem
|
||||
|
||||
theorem get!_ofList_of_contains_eq_false [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
|
||||
{l : List (α × β)} {k : α} [Inhabited β]
|
||||
(contains_eq_false : (l.map Prod.fst).contains k = false) :
|
||||
get! (ofList l cmp) k = default :=
|
||||
Impl.Const.get!_insertMany_empty_list_of_contains_eq_false contains_eq_false
|
||||
|
||||
theorem get!_ofList_of_mem [TransCmp cmp]
|
||||
{l : List (α × β)} {k k' : α} (k_eq : cmp k k' = .eq) {v : β} [Inhabited β]
|
||||
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
|
||||
(mem : ⟨k, v⟩ ∈ l) :
|
||||
get! (ofList l cmp) k' = v :=
|
||||
Impl.Const.get!_insertMany_empty_list_of_mem k_eq distinct mem
|
||||
|
||||
theorem getD_ofList_of_contains_eq_false [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
|
||||
{l : List (α × β)} {k : α} {fallback : β}
|
||||
(contains_eq_false : (l.map Prod.fst).contains k = false) :
|
||||
getD (ofList l cmp) k fallback = fallback :=
|
||||
Impl.Const.getD_insertMany_empty_list_of_contains_eq_false contains_eq_false
|
||||
|
||||
theorem getD_ofList_of_mem [TransCmp cmp]
|
||||
{l : List (α × β)} {k k' : α} (k_eq : cmp k k' = .eq) {v : β} {fallback : β}
|
||||
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
|
||||
(mem : ⟨k, v⟩ ∈ l) :
|
||||
getD (ofList l cmp) k' fallback = v :=
|
||||
Impl.Const.getD_insertMany_empty_list_of_mem k_eq distinct mem
|
||||
|
||||
theorem getKey?_ofList_of_contains_eq_false [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
|
||||
{l : List (α × β)} {k : α}
|
||||
(contains_eq_false : (l.map Prod.fst).contains k = false) :
|
||||
(ofList l cmp).getKey? k = none :=
|
||||
Impl.Const.getKey?_insertMany_empty_list_of_contains_eq_false contains_eq_false
|
||||
|
||||
theorem getKey?_ofList_of_mem [TransCmp cmp]
|
||||
{l : List (α × β)}
|
||||
{k k' : α} (k_eq : cmp k k' = .eq)
|
||||
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
|
||||
(mem : k ∈ l.map Prod.fst) :
|
||||
(ofList l cmp).getKey? k' = some k :=
|
||||
Impl.Const.getKey?_insertMany_empty_list_of_mem k_eq distinct mem
|
||||
|
||||
theorem getKey_ofList_of_mem [TransCmp cmp]
|
||||
{l : List (α × β)}
|
||||
{k k' : α} (k_eq : cmp k k' = .eq)
|
||||
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
|
||||
(mem : k ∈ l.map Prod.fst)
|
||||
{h'} :
|
||||
(ofList l cmp).getKey k' h' = k :=
|
||||
Impl.Const.getKey_insertMany_empty_list_of_mem k_eq distinct mem
|
||||
|
||||
theorem getKey!_ofList_of_contains_eq_false [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
|
||||
[Inhabited α] {l : List (α × β)} {k : α}
|
||||
(contains_eq_false : (l.map Prod.fst).contains k = false) :
|
||||
(ofList l cmp).getKey! k = default :=
|
||||
Impl.Const.getKey!_insertMany_empty_list_of_contains_eq_false contains_eq_false
|
||||
|
||||
theorem getKey!_ofList_of_mem [TransCmp cmp] [Inhabited α]
|
||||
{l : List (α × β)}
|
||||
{k k' : α} (k_eq : cmp k k' = .eq)
|
||||
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
|
||||
(mem : k ∈ l.map Prod.fst) :
|
||||
(ofList l cmp).getKey! k' = k :=
|
||||
Impl.Const.getKey!_insertMany_empty_list_of_mem k_eq distinct mem
|
||||
|
||||
theorem getKeyD_ofList_of_contains_eq_false [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
|
||||
{l : List (α × β)} {k fallback : α}
|
||||
(contains_eq_false : (l.map Prod.fst).contains k = false) :
|
||||
(ofList l cmp).getKeyD k fallback = fallback :=
|
||||
Impl.Const.getKeyD_insertMany_empty_list_of_contains_eq_false contains_eq_false
|
||||
|
||||
theorem getKeyD_ofList_of_mem [TransCmp cmp]
|
||||
{l : List (α × β)}
|
||||
{k k' fallback : α} (k_eq : cmp k k' = .eq)
|
||||
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
|
||||
(mem : k ∈ l.map Prod.fst) :
|
||||
(ofList l cmp).getKeyD k' fallback = k :=
|
||||
Impl.Const.getKeyD_insertMany_empty_list_of_mem k_eq distinct mem
|
||||
|
||||
theorem size_ofList [TransCmp cmp] {l : List (α × β)}
|
||||
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq)) :
|
||||
(ofList l cmp).size = l.length :=
|
||||
Impl.Const.size_insertMany_empty_list distinct
|
||||
|
||||
theorem size_ofList_le [TransCmp cmp] {l : List (α × β)} :
|
||||
(ofList l cmp).size ≤ l.length :=
|
||||
Impl.Const.size_insertMany_empty_list_le
|
||||
|
||||
theorem isEmpty_ofList [TransCmp cmp] {l : List (α × β)} :
|
||||
(ofList l cmp).isEmpty = l.isEmpty :=
|
||||
Impl.Const.isEmpty_insertMany_empty_list
|
||||
|
||||
@[simp]
|
||||
theorem unitOfList_nil :
|
||||
unitOfList ([] : List α) cmp =
|
||||
(∅ : Raw α Unit cmp) :=
|
||||
rfl
|
||||
|
||||
@[simp]
|
||||
theorem unitOfList_singleton {k : α} :
|
||||
unitOfList [k] cmp = (∅ : Raw α Unit cmp).insertIfNew k () :=
|
||||
rfl
|
||||
|
||||
theorem unitOfList_cons {hd : α} {tl : List α} :
|
||||
unitOfList (hd :: tl) cmp =
|
||||
insertManyIfNewUnit ((∅ : Raw α Unit cmp).insertIfNew hd ()) tl :=
|
||||
ext Impl.Const.insertManyIfNewUnit_empty_list_cons_eq_insertManyIfNewUnit!
|
||||
|
||||
@[simp]
|
||||
theorem contains_unitOfList [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List α} {k : α} :
|
||||
(unitOfList l cmp).contains k = l.contains k :=
|
||||
Impl.Const.contains_insertManyIfNewUnit_empty_list
|
||||
|
||||
@[simp]
|
||||
theorem mem_unitOfList [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List α} {k : α} :
|
||||
k ∈ unitOfList l cmp ↔ l.contains k := by
|
||||
simp [mem_iff_contains]
|
||||
|
||||
theorem getKey?_unitOfList_of_contains_eq_false [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
|
||||
{l : List α} {k : α}
|
||||
(contains_eq_false : l.contains k = false) :
|
||||
getKey? (unitOfList l cmp) k = none :=
|
||||
Impl.Const.getKey?_insertManyIfNewUnit_empty_list_of_contains_eq_false contains_eq_false
|
||||
|
||||
theorem getKey?_unitOfList_of_mem [TransCmp cmp]
|
||||
{l : List α} {k k' : α} (k_eq : cmp k k' = .eq)
|
||||
(distinct : l.Pairwise (fun a b => ¬ cmp a b = .eq)) (mem : k ∈ l) :
|
||||
getKey? (unitOfList l cmp) k' = some k :=
|
||||
Impl.Const.getKey?_insertManyIfNewUnit_empty_list_of_mem k_eq distinct mem
|
||||
|
||||
theorem getKey_unitOfList_of_mem [TransCmp cmp]
|
||||
{l : List α}
|
||||
{k k' : α} (k_eq : cmp k k' = .eq)
|
||||
(distinct : l.Pairwise (fun a b => ¬ cmp a b = .eq))
|
||||
(mem : k ∈ l) {h'} :
|
||||
getKey (unitOfList l cmp) k' h' = k :=
|
||||
Impl.Const.getKey_insertManyIfNewUnit_empty_list_of_mem k_eq distinct mem
|
||||
|
||||
theorem getKey!_unitOfList_of_contains_eq_false [TransCmp cmp] [BEq α]
|
||||
[LawfulBEqCmp cmp] [Inhabited α] {l : List α} {k : α}
|
||||
(contains_eq_false : l.contains k = false) :
|
||||
getKey! (unitOfList l cmp) k = default :=
|
||||
Impl.Const.getKey!_insertManyIfNewUnit_empty_list_of_contains_eq_false contains_eq_false
|
||||
|
||||
theorem getKey!_unitOfList_of_mem [TransCmp cmp]
|
||||
[Inhabited α] {l : List α} {k k' : α} (k_eq : cmp k k' = .eq)
|
||||
(distinct : l.Pairwise (fun a b => ¬ cmp a b = .eq))
|
||||
(mem : k ∈ l) :
|
||||
getKey! (unitOfList l cmp) k' = k :=
|
||||
Impl.Const.getKey!_insertManyIfNewUnit_empty_list_of_mem k_eq distinct mem
|
||||
|
||||
theorem getKeyD_unitOfList_of_contains_eq_false [TransCmp cmp] [BEq α]
|
||||
[LawfulBEqCmp cmp] {l : List α} {k fallback : α}
|
||||
(contains_eq_false : l.contains k = false) :
|
||||
getKeyD (unitOfList l cmp) k fallback = fallback :=
|
||||
Impl.Const.getKeyD_insertManyIfNewUnit_empty_list_of_contains_eq_false contains_eq_false
|
||||
|
||||
theorem getKeyD_unitOfList_of_mem [TransCmp cmp]
|
||||
{l : List α} {k k' fallback : α} (k_eq : cmp k k' = .eq)
|
||||
(distinct : l.Pairwise (fun a b => ¬ cmp a b = .eq))
|
||||
(mem : k ∈ l) :
|
||||
getKeyD (unitOfList l cmp) k' fallback = k :=
|
||||
Impl.Const.getKeyD_insertManyIfNewUnit_empty_list_of_mem k_eq distinct mem
|
||||
|
||||
theorem size_unitOfList [TransCmp cmp] {l : List α}
|
||||
(distinct : l.Pairwise (fun a b => ¬ cmp a b = .eq)) :
|
||||
(unitOfList l cmp).size = l.length :=
|
||||
Impl.Const.size_insertManyIfNewUnit_empty_list distinct
|
||||
|
||||
theorem size_unitOfList_le [TransCmp cmp] {l : List α} :
|
||||
(unitOfList l cmp).size ≤ l.length :=
|
||||
Impl.Const.size_insertManyIfNewUnit_empty_list_le
|
||||
|
||||
@[simp]
|
||||
theorem isEmpty_unitOfList [TransCmp cmp] {l : List α} :
|
||||
(unitOfList l cmp).isEmpty = l.isEmpty :=
|
||||
Impl.Const.isEmpty_insertManyIfNewUnit_empty_list
|
||||
|
||||
@[simp]
|
||||
theorem get?_unitOfList [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List α} {k : α} :
|
||||
get? (unitOfList l cmp) k = if l.contains k then some () else none :=
|
||||
Impl.Const.get?_insertManyIfNewUnit_empty_list
|
||||
|
||||
@[simp]
|
||||
theorem get_unitOfList {l : List α} {k : α} {h} :
|
||||
get (unitOfList l cmp) k h = () :=
|
||||
Impl.Const.get_insertManyIfNewUnit_empty_list
|
||||
|
||||
@[simp]
|
||||
theorem get!_unitOfList {l : List α} {k : α} :
|
||||
get! (unitOfList l cmp) k = () :=
|
||||
Impl.Const.get!_insertManyIfNewUnit_empty_list
|
||||
|
||||
@[simp]
|
||||
theorem getD_unitOfList {l : List α} {k : α} {fallback : Unit} :
|
||||
getD (unitOfList l cmp) k fallback = () :=
|
||||
Impl.Const.getD_insertManyIfNewUnit_empty_list
|
||||
|
||||
end Const
|
||||
|
||||
end Std.DTreeMap.Raw
|
||||
|
|
|
|||
|
|
@ -1103,4 +1103,245 @@ theorem getD_insertManyIfNewUnit_list
|
|||
getD (insertManyIfNewUnit t l) k fallback = () :=
|
||||
rfl
|
||||
|
||||
@[simp]
|
||||
theorem ofList_nil :
|
||||
ofList ([] : List (α × β)) cmp = ∅ := by
|
||||
rfl
|
||||
|
||||
@[simp]
|
||||
theorem ofList_singleton {k : α} {v : β} :
|
||||
ofList [⟨k, v⟩] cmp = (∅ : TreeMap α β cmp).insert k v := by
|
||||
rfl
|
||||
|
||||
theorem ofList_cons {k : α} {v : β} {tl : List (α × β)} :
|
||||
ofList (⟨k, v⟩ :: tl) cmp = insertMany ((∅ : TreeMap α β cmp).insert k v) tl :=
|
||||
ext DTreeMap.Const.ofList_cons
|
||||
|
||||
@[simp]
|
||||
theorem contains_ofList [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List (α × β)} {k : α} :
|
||||
(ofList l cmp).contains k = (l.map Prod.fst).contains k :=
|
||||
DTreeMap.Const.contains_ofList
|
||||
|
||||
@[simp]
|
||||
theorem mem_ofList [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List (α × β)} {k : α} :
|
||||
k ∈ ofList l cmp ↔ (l.map Prod.fst).contains k :=
|
||||
DTreeMap.Const.mem_ofList
|
||||
|
||||
theorem getElem?_ofList_of_contains_eq_false [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
|
||||
{l : List (α × β)} {k : α}
|
||||
(contains_eq_false : (l.map Prod.fst).contains k = false) :
|
||||
(ofList l cmp)[k]? = none :=
|
||||
DTreeMap.Const.get?_ofList_of_contains_eq_false contains_eq_false
|
||||
|
||||
theorem getElem?_ofList_of_mem [TransCmp cmp]
|
||||
{l : List (α × β)} {k k' : α} (k_eq : cmp k k' = .eq) {v : β}
|
||||
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
|
||||
(mem : ⟨k, v⟩ ∈ l) :
|
||||
(ofList l cmp)[k']? = some v :=
|
||||
DTreeMap.Const.get?_ofList_of_mem k_eq distinct mem
|
||||
|
||||
theorem getElem_ofList_of_mem [TransCmp cmp]
|
||||
{l : List (α × β)} {k k' : α} (k_eq : cmp k k' = .eq) {v : β}
|
||||
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
|
||||
(mem : ⟨k, v⟩ ∈ l)
|
||||
{h} :
|
||||
(ofList l cmp)[k']'h = v :=
|
||||
DTreeMap.Const.get_ofList_of_mem k_eq distinct mem
|
||||
|
||||
theorem getElem!_ofList_of_contains_eq_false [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
|
||||
{l : List (α × β)} {k : α} [Inhabited β]
|
||||
(contains_eq_false : (l.map Prod.fst).contains k = false) :
|
||||
(ofList l cmp)[k]! = default :=
|
||||
DTreeMap.Const.get!_ofList_of_contains_eq_false contains_eq_false
|
||||
|
||||
theorem getElem!_ofList_of_mem [TransCmp cmp]
|
||||
{l : List (α × β)} {k k' : α} (k_eq : cmp k k' = .eq) {v : β} [Inhabited β]
|
||||
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
|
||||
(mem : ⟨k, v⟩ ∈ l) :
|
||||
(ofList l cmp)[k']! = v :=
|
||||
DTreeMap.Const.get!_ofList_of_mem k_eq distinct mem
|
||||
|
||||
theorem getD_ofList_of_contains_eq_false [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
|
||||
{l : List (α × β)} {k : α} {fallback : β}
|
||||
(contains_eq_false : (l.map Prod.fst).contains k = false) :
|
||||
getD (ofList l cmp) k fallback = fallback :=
|
||||
DTreeMap.Const.getD_ofList_of_contains_eq_false contains_eq_false
|
||||
|
||||
theorem getD_ofList_of_mem [TransCmp cmp]
|
||||
{l : List (α × β)} {k k' : α} (k_eq : cmp k k' = .eq) {v : β} {fallback : β}
|
||||
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
|
||||
(mem : ⟨k, v⟩ ∈ l) :
|
||||
getD (ofList l cmp) k' fallback = v :=
|
||||
DTreeMap.Const.getD_ofList_of_mem k_eq distinct mem
|
||||
|
||||
theorem getKey?_ofList_of_contains_eq_false [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
|
||||
{l : List (α × β)} {k : α}
|
||||
(contains_eq_false : (l.map Prod.fst).contains k = false) :
|
||||
(ofList l cmp).getKey? k = none :=
|
||||
DTreeMap.Const.getKey?_ofList_of_contains_eq_false contains_eq_false
|
||||
|
||||
theorem getKey?_ofList_of_mem [TransCmp cmp]
|
||||
{l : List (α × β)}
|
||||
{k k' : α} (k_eq : cmp k k' = .eq)
|
||||
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
|
||||
(mem : k ∈ l.map Prod.fst) :
|
||||
(ofList l cmp).getKey? k' = some k :=
|
||||
DTreeMap.Const.getKey?_ofList_of_mem k_eq distinct mem
|
||||
|
||||
theorem getKey_ofList_of_mem [TransCmp cmp]
|
||||
{l : List (α × β)}
|
||||
{k k' : α} (k_eq : cmp k k' = .eq)
|
||||
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
|
||||
(mem : k ∈ l.map Prod.fst)
|
||||
{h'} :
|
||||
(ofList l cmp).getKey k' h' = k :=
|
||||
DTreeMap.Const.getKey_ofList_of_mem k_eq distinct mem
|
||||
|
||||
theorem getKey!_ofList_of_contains_eq_false [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
|
||||
[Inhabited α] {l : List (α × β)} {k : α}
|
||||
(contains_eq_false : (l.map Prod.fst).contains k = false) :
|
||||
(ofList l cmp).getKey! k = default :=
|
||||
DTreeMap.Const.getKey!_ofList_of_contains_eq_false contains_eq_false
|
||||
|
||||
theorem getKey!_ofList_of_mem [TransCmp cmp] [Inhabited α]
|
||||
{l : List (α × β)}
|
||||
{k k' : α} (k_eq : cmp k k' = .eq)
|
||||
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
|
||||
(mem : k ∈ l.map Prod.fst) :
|
||||
(ofList l cmp).getKey! k' = k :=
|
||||
DTreeMap.Const.getKey!_ofList_of_mem k_eq distinct mem
|
||||
|
||||
theorem getKeyD_ofList_of_contains_eq_false [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
|
||||
{l : List (α × β)} {k fallback : α}
|
||||
(contains_eq_false : (l.map Prod.fst).contains k = false) :
|
||||
(ofList l cmp).getKeyD k fallback = fallback :=
|
||||
DTreeMap.Const.getKeyD_ofList_of_contains_eq_false contains_eq_false
|
||||
|
||||
theorem getKeyD_ofList_of_mem [TransCmp cmp]
|
||||
{l : List (α × β)}
|
||||
{k k' fallback : α} (k_eq : cmp k k' = .eq)
|
||||
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
|
||||
(mem : k ∈ l.map Prod.fst) :
|
||||
(ofList l cmp).getKeyD k' fallback = k :=
|
||||
DTreeMap.Const.getKeyD_ofList_of_mem k_eq distinct mem
|
||||
|
||||
theorem size_ofList [TransCmp cmp] {l : List (α × β)}
|
||||
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq)) :
|
||||
(ofList l cmp).size = l.length :=
|
||||
DTreeMap.Const.size_ofList distinct
|
||||
|
||||
theorem size_ofList_le [TransCmp cmp] {l : List (α × β)} :
|
||||
(ofList l cmp).size ≤ l.length :=
|
||||
DTreeMap.Const.size_ofList_le
|
||||
|
||||
theorem isEmpty_ofList [TransCmp cmp] {l : List (α × β)} :
|
||||
(ofList l cmp).isEmpty = l.isEmpty :=
|
||||
DTreeMap.Const.isEmpty_ofList
|
||||
|
||||
@[simp]
|
||||
theorem unitOfList_nil :
|
||||
unitOfList ([] : List α) cmp =
|
||||
(∅ : TreeMap α Unit cmp) :=
|
||||
rfl
|
||||
|
||||
@[simp]
|
||||
theorem unitOfList_singleton {k : α} :
|
||||
unitOfList [k] cmp = (∅ : TreeMap α Unit cmp).insertIfNew k () :=
|
||||
rfl
|
||||
|
||||
theorem unitOfList_cons {hd : α} {tl : List α} :
|
||||
unitOfList (hd :: tl) cmp =
|
||||
insertManyIfNewUnit ((∅ : TreeMap α Unit cmp).insertIfNew hd ()) tl :=
|
||||
ext DTreeMap.Const.unitOfList_cons
|
||||
|
||||
@[simp]
|
||||
theorem contains_unitOfList [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List α} {k : α} :
|
||||
(unitOfList l cmp).contains k = l.contains k :=
|
||||
DTreeMap.Const.contains_unitOfList
|
||||
|
||||
@[simp]
|
||||
theorem mem_unitOfList [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List α} {k : α} :
|
||||
k ∈ unitOfList l cmp ↔ l.contains k := by
|
||||
simp [mem_iff_contains]
|
||||
|
||||
theorem getKey?_unitOfList_of_contains_eq_false [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
|
||||
{l : List α} {k : α}
|
||||
(contains_eq_false : l.contains k = false) :
|
||||
getKey? (unitOfList l cmp) k = none :=
|
||||
DTreeMap.Const.getKey?_unitOfList_of_contains_eq_false contains_eq_false
|
||||
|
||||
theorem getKey?_unitOfList_of_mem [TransCmp cmp]
|
||||
{l : List α} {k k' : α} (k_eq : cmp k k' = .eq)
|
||||
(distinct : l.Pairwise (fun a b => ¬ cmp a b = .eq)) (mem : k ∈ l) :
|
||||
getKey? (unitOfList l cmp) k' = some k :=
|
||||
DTreeMap.Const.getKey?_unitOfList_of_mem k_eq distinct mem
|
||||
|
||||
theorem getKey_unitOfList_of_mem [TransCmp cmp]
|
||||
{l : List α}
|
||||
{k k' : α} (k_eq : cmp k k' = .eq)
|
||||
(distinct : l.Pairwise (fun a b => ¬ cmp a b = .eq))
|
||||
(mem : k ∈ l) {h'} :
|
||||
getKey (unitOfList l cmp) k' h' = k :=
|
||||
DTreeMap.Const.getKey_unitOfList_of_mem k_eq distinct mem
|
||||
|
||||
theorem getKey!_unitOfList_of_contains_eq_false [TransCmp cmp] [BEq α]
|
||||
[LawfulBEqCmp cmp] [Inhabited α] {l : List α} {k : α}
|
||||
(contains_eq_false : l.contains k = false) :
|
||||
getKey! (unitOfList l cmp) k = default :=
|
||||
DTreeMap.Const.getKey!_unitOfList_of_contains_eq_false contains_eq_false
|
||||
|
||||
theorem getKey!_unitOfList_of_mem [TransCmp cmp]
|
||||
[Inhabited α] {l : List α} {k k' : α} (k_eq : cmp k k' = .eq)
|
||||
(distinct : l.Pairwise (fun a b => ¬ cmp a b = .eq))
|
||||
(mem : k ∈ l) :
|
||||
getKey! (unitOfList l cmp) k' = k :=
|
||||
DTreeMap.Const.getKey!_unitOfList_of_mem k_eq distinct mem
|
||||
|
||||
theorem getKeyD_unitOfList_of_contains_eq_false [TransCmp cmp] [BEq α]
|
||||
[LawfulBEqCmp cmp] {l : List α} {k fallback : α}
|
||||
(contains_eq_false : l.contains k = false) :
|
||||
getKeyD (unitOfList l cmp) k fallback = fallback :=
|
||||
DTreeMap.Const.getKeyD_unitOfList_of_contains_eq_false contains_eq_false
|
||||
|
||||
theorem getKeyD_unitOfList_of_mem [TransCmp cmp]
|
||||
{l : List α} {k k' fallback : α} (k_eq : cmp k k' = .eq)
|
||||
(distinct : l.Pairwise (fun a b => ¬ cmp a b = .eq))
|
||||
(mem : k ∈ l) :
|
||||
getKeyD (unitOfList l cmp) k' fallback = k :=
|
||||
DTreeMap.Const.getKeyD_unitOfList_of_mem k_eq distinct mem
|
||||
|
||||
theorem size_unitOfList [TransCmp cmp] {l : List α}
|
||||
(distinct : l.Pairwise (fun a b => ¬ cmp a b = .eq)) :
|
||||
(unitOfList l cmp).size = l.length :=
|
||||
DTreeMap.Const.size_unitOfList distinct
|
||||
|
||||
theorem size_unitOfList_le [TransCmp cmp] {l : List α} :
|
||||
(unitOfList l cmp).size ≤ l.length :=
|
||||
DTreeMap.Const.size_unitOfList_le
|
||||
|
||||
@[simp]
|
||||
theorem isEmpty_unitOfList [TransCmp cmp] {l : List α} :
|
||||
(unitOfList l cmp).isEmpty = l.isEmpty :=
|
||||
DTreeMap.Const.isEmpty_unitOfList
|
||||
|
||||
@[simp]
|
||||
theorem getElem?_unitOfList [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List α} {k : α} :
|
||||
(unitOfList l cmp)[k]? = if l.contains k then some () else none :=
|
||||
DTreeMap.Const.get?_unitOfList
|
||||
|
||||
@[simp]
|
||||
theorem getElem_unitOfList {l : List α} {k : α} {h} :
|
||||
(unitOfList l cmp)[k]'h = () :=
|
||||
DTreeMap.Const.get_unitOfList
|
||||
|
||||
@[simp]
|
||||
theorem getElem!_unitOfList {l : List α} {k : α} :
|
||||
(unitOfList l cmp)[k]! = () :=
|
||||
DTreeMap.Const.get!_unitOfList
|
||||
|
||||
@[simp]
|
||||
theorem getD_unitOfList {l : List α} {k : α} {fallback : Unit} :
|
||||
getD (unitOfList l cmp) k fallback = () :=
|
||||
DTreeMap.Const.getD_unitOfList
|
||||
|
||||
end Std.TreeMap
|
||||
|
|
|
|||
|
|
@ -1111,4 +1111,245 @@ theorem getD_insertManyIfNewUnit_list
|
|||
getD (insertManyIfNewUnit t l) k fallback = () :=
|
||||
rfl
|
||||
|
||||
@[simp]
|
||||
theorem ofList_nil :
|
||||
ofList ([] : List (α × β)) cmp = ∅ := by
|
||||
rfl
|
||||
|
||||
@[simp]
|
||||
theorem ofList_singleton {k : α} {v : β} :
|
||||
ofList [⟨k, v⟩] cmp = (∅ : Raw α β cmp).insert k v := by
|
||||
rfl
|
||||
|
||||
theorem ofList_cons {k : α} {v : β} {tl : List (α × β)} :
|
||||
ofList (⟨k, v⟩ :: tl) cmp = insertMany ((∅ : Raw α β cmp).insert k v) tl :=
|
||||
ext DTreeMap.Raw.Const.ofList_cons
|
||||
|
||||
@[simp]
|
||||
theorem contains_ofList [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List (α × β)} {k : α} :
|
||||
(ofList l cmp).contains k = (l.map Prod.fst).contains k :=
|
||||
DTreeMap.Raw.Const.contains_ofList
|
||||
|
||||
@[simp]
|
||||
theorem mem_ofList [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List (α × β)} {k : α} :
|
||||
k ∈ ofList l cmp ↔ (l.map Prod.fst).contains k :=
|
||||
DTreeMap.Raw.Const.mem_ofList
|
||||
|
||||
theorem getElem?_ofList_of_contains_eq_false [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
|
||||
{l : List (α × β)} {k : α}
|
||||
(contains_eq_false : (l.map Prod.fst).contains k = false) :
|
||||
(ofList l cmp)[k]? = none :=
|
||||
DTreeMap.Raw.Const.get?_ofList_of_contains_eq_false contains_eq_false
|
||||
|
||||
theorem getElem?_ofList_of_mem [TransCmp cmp]
|
||||
{l : List (α × β)} {k k' : α} (k_eq : cmp k k' = .eq) {v : β}
|
||||
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
|
||||
(mem : ⟨k, v⟩ ∈ l) :
|
||||
(ofList l cmp)[k']? = some v :=
|
||||
DTreeMap.Raw.Const.get?_ofList_of_mem k_eq distinct mem
|
||||
|
||||
theorem getElem_ofList_of_mem [TransCmp cmp]
|
||||
{l : List (α × β)} {k k' : α} (k_eq : cmp k k' = .eq) {v : β}
|
||||
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
|
||||
(mem : ⟨k, v⟩ ∈ l)
|
||||
{h} :
|
||||
(ofList l cmp)[k']'h = v :=
|
||||
DTreeMap.Raw.Const.get_ofList_of_mem k_eq distinct mem
|
||||
|
||||
theorem getElem!_ofList_of_contains_eq_false [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
|
||||
{l : List (α × β)} {k : α} [Inhabited β]
|
||||
(contains_eq_false : (l.map Prod.fst).contains k = false) :
|
||||
(ofList l cmp)[k]! = default :=
|
||||
DTreeMap.Raw.Const.get!_ofList_of_contains_eq_false contains_eq_false
|
||||
|
||||
theorem getElem!_ofList_of_mem [TransCmp cmp]
|
||||
{l : List (α × β)} {k k' : α} (k_eq : cmp k k' = .eq) {v : β} [Inhabited β]
|
||||
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
|
||||
(mem : ⟨k, v⟩ ∈ l) :
|
||||
(ofList l cmp)[k']! = v :=
|
||||
DTreeMap.Raw.Const.get!_ofList_of_mem k_eq distinct mem
|
||||
|
||||
theorem getD_ofList_of_contains_eq_false [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
|
||||
{l : List (α × β)} {k : α} {fallback : β}
|
||||
(contains_eq_false : (l.map Prod.fst).contains k = false) :
|
||||
getD (ofList l cmp) k fallback = fallback :=
|
||||
DTreeMap.Raw.Const.getD_ofList_of_contains_eq_false contains_eq_false
|
||||
|
||||
theorem getD_ofList_of_mem [TransCmp cmp]
|
||||
{l : List (α × β)} {k k' : α} (k_eq : cmp k k' = .eq) {v : β} {fallback : β}
|
||||
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
|
||||
(mem : ⟨k, v⟩ ∈ l) :
|
||||
getD (ofList l cmp) k' fallback = v :=
|
||||
DTreeMap.Raw.Const.getD_ofList_of_mem k_eq distinct mem
|
||||
|
||||
theorem getKey?_ofList_of_contains_eq_false [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
|
||||
{l : List (α × β)} {k : α}
|
||||
(contains_eq_false : (l.map Prod.fst).contains k = false) :
|
||||
(ofList l cmp).getKey? k = none :=
|
||||
DTreeMap.Raw.Const.getKey?_ofList_of_contains_eq_false contains_eq_false
|
||||
|
||||
theorem getKey?_ofList_of_mem [TransCmp cmp]
|
||||
{l : List (α × β)}
|
||||
{k k' : α} (k_eq : cmp k k' = .eq)
|
||||
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
|
||||
(mem : k ∈ l.map Prod.fst) :
|
||||
(ofList l cmp).getKey? k' = some k :=
|
||||
DTreeMap.Raw.Const.getKey?_ofList_of_mem k_eq distinct mem
|
||||
|
||||
theorem getKey_ofList_of_mem [TransCmp cmp]
|
||||
{l : List (α × β)}
|
||||
{k k' : α} (k_eq : cmp k k' = .eq)
|
||||
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
|
||||
(mem : k ∈ l.map Prod.fst)
|
||||
{h'} :
|
||||
(ofList l cmp).getKey k' h' = k :=
|
||||
DTreeMap.Raw.Const.getKey_ofList_of_mem k_eq distinct mem
|
||||
|
||||
theorem getKey!_ofList_of_contains_eq_false [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
|
||||
[Inhabited α] {l : List (α × β)} {k : α}
|
||||
(contains_eq_false : (l.map Prod.fst).contains k = false) :
|
||||
(ofList l cmp).getKey! k = default :=
|
||||
DTreeMap.Raw.Const.getKey!_ofList_of_contains_eq_false contains_eq_false
|
||||
|
||||
theorem getKey!_ofList_of_mem [TransCmp cmp] [Inhabited α]
|
||||
{l : List (α × β)}
|
||||
{k k' : α} (k_eq : cmp k k' = .eq)
|
||||
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
|
||||
(mem : k ∈ l.map Prod.fst) :
|
||||
(ofList l cmp).getKey! k' = k :=
|
||||
DTreeMap.Raw.Const.getKey!_ofList_of_mem k_eq distinct mem
|
||||
|
||||
theorem getKeyD_ofList_of_contains_eq_false [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
|
||||
{l : List (α × β)} {k fallback : α}
|
||||
(contains_eq_false : (l.map Prod.fst).contains k = false) :
|
||||
(ofList l cmp).getKeyD k fallback = fallback :=
|
||||
DTreeMap.Raw.Const.getKeyD_ofList_of_contains_eq_false contains_eq_false
|
||||
|
||||
theorem getKeyD_ofList_of_mem [TransCmp cmp]
|
||||
{l : List (α × β)}
|
||||
{k k' fallback : α} (k_eq : cmp k k' = .eq)
|
||||
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
|
||||
(mem : k ∈ l.map Prod.fst) :
|
||||
(ofList l cmp).getKeyD k' fallback = k :=
|
||||
DTreeMap.Raw.Const.getKeyD_ofList_of_mem k_eq distinct mem
|
||||
|
||||
theorem size_ofList [TransCmp cmp] {l : List (α × β)}
|
||||
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq)) :
|
||||
(ofList l cmp).size = l.length :=
|
||||
DTreeMap.Raw.Const.size_ofList distinct
|
||||
|
||||
theorem size_ofList_le [TransCmp cmp] {l : List (α × β)} :
|
||||
(ofList l cmp).size ≤ l.length :=
|
||||
DTreeMap.Raw.Const.size_ofList_le
|
||||
|
||||
theorem isEmpty_ofList [TransCmp cmp] {l : List (α × β)} :
|
||||
(ofList l cmp).isEmpty = l.isEmpty :=
|
||||
DTreeMap.Raw.Const.isEmpty_ofList
|
||||
|
||||
@[simp]
|
||||
theorem unitOfList_nil :
|
||||
unitOfList ([] : List α) cmp =
|
||||
(∅ : Raw α Unit cmp) :=
|
||||
rfl
|
||||
|
||||
@[simp]
|
||||
theorem unitOfList_singleton {k : α} :
|
||||
unitOfList [k] cmp = (∅ : Raw α Unit cmp).insertIfNew k () :=
|
||||
rfl
|
||||
|
||||
theorem unitOfList_cons {hd : α} {tl : List α} :
|
||||
unitOfList (hd :: tl) cmp =
|
||||
insertManyIfNewUnit ((∅ : Raw α Unit cmp).insertIfNew hd ()) tl :=
|
||||
ext DTreeMap.Raw.Const.unitOfList_cons
|
||||
|
||||
@[simp]
|
||||
theorem contains_unitOfList [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List α} {k : α} :
|
||||
(unitOfList l cmp).contains k = l.contains k :=
|
||||
DTreeMap.Raw.Const.contains_unitOfList
|
||||
|
||||
@[simp]
|
||||
theorem mem_unitOfList [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List α} {k : α} :
|
||||
k ∈ unitOfList l cmp ↔ l.contains k := by
|
||||
simp [mem_iff_contains]
|
||||
|
||||
theorem getKey?_unitOfList_of_contains_eq_false [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
|
||||
{l : List α} {k : α}
|
||||
(contains_eq_false : l.contains k = false) :
|
||||
getKey? (unitOfList l cmp) k = none :=
|
||||
DTreeMap.Raw.Const.getKey?_unitOfList_of_contains_eq_false contains_eq_false
|
||||
|
||||
theorem getKey?_unitOfList_of_mem [TransCmp cmp]
|
||||
{l : List α} {k k' : α} (k_eq : cmp k k' = .eq)
|
||||
(distinct : l.Pairwise (fun a b => ¬ cmp a b = .eq)) (mem : k ∈ l) :
|
||||
getKey? (unitOfList l cmp) k' = some k :=
|
||||
DTreeMap.Raw.Const.getKey?_unitOfList_of_mem k_eq distinct mem
|
||||
|
||||
theorem getKey_unitOfList_of_mem [TransCmp cmp]
|
||||
{l : List α}
|
||||
{k k' : α} (k_eq : cmp k k' = .eq)
|
||||
(distinct : l.Pairwise (fun a b => ¬ cmp a b = .eq))
|
||||
(mem : k ∈ l) {h'} :
|
||||
getKey (unitOfList l cmp) k' h' = k :=
|
||||
DTreeMap.Raw.Const.getKey_unitOfList_of_mem k_eq distinct mem
|
||||
|
||||
theorem getKey!_unitOfList_of_contains_eq_false [TransCmp cmp] [BEq α]
|
||||
[LawfulBEqCmp cmp] [Inhabited α] {l : List α} {k : α}
|
||||
(contains_eq_false : l.contains k = false) :
|
||||
getKey! (unitOfList l cmp) k = default :=
|
||||
DTreeMap.Raw.Const.getKey!_unitOfList_of_contains_eq_false contains_eq_false
|
||||
|
||||
theorem getKey!_unitOfList_of_mem [TransCmp cmp]
|
||||
[Inhabited α] {l : List α} {k k' : α} (k_eq : cmp k k' = .eq)
|
||||
(distinct : l.Pairwise (fun a b => ¬ cmp a b = .eq))
|
||||
(mem : k ∈ l) :
|
||||
getKey! (unitOfList l cmp) k' = k :=
|
||||
DTreeMap.Raw.Const.getKey!_unitOfList_of_mem k_eq distinct mem
|
||||
|
||||
theorem getKeyD_unitOfList_of_contains_eq_false [TransCmp cmp] [BEq α]
|
||||
[LawfulBEqCmp cmp] {l : List α} {k fallback : α}
|
||||
(contains_eq_false : l.contains k = false) :
|
||||
getKeyD (unitOfList l cmp) k fallback = fallback :=
|
||||
DTreeMap.Raw.Const.getKeyD_unitOfList_of_contains_eq_false contains_eq_false
|
||||
|
||||
theorem getKeyD_unitOfList_of_mem [TransCmp cmp]
|
||||
{l : List α} {k k' fallback : α} (k_eq : cmp k k' = .eq)
|
||||
(distinct : l.Pairwise (fun a b => ¬ cmp a b = .eq))
|
||||
(mem : k ∈ l) :
|
||||
getKeyD (unitOfList l cmp) k' fallback = k :=
|
||||
DTreeMap.Raw.Const.getKeyD_unitOfList_of_mem k_eq distinct mem
|
||||
|
||||
theorem size_unitOfList [TransCmp cmp] {l : List α}
|
||||
(distinct : l.Pairwise (fun a b => ¬ cmp a b = .eq)) :
|
||||
(unitOfList l cmp).size = l.length :=
|
||||
DTreeMap.Raw.Const.size_unitOfList distinct
|
||||
|
||||
theorem size_unitOfList_le [TransCmp cmp] {l : List α} :
|
||||
(unitOfList l cmp).size ≤ l.length :=
|
||||
DTreeMap.Raw.Const.size_unitOfList_le
|
||||
|
||||
@[simp]
|
||||
theorem isEmpty_unitOfList [TransCmp cmp] {l : List α} :
|
||||
(unitOfList l cmp).isEmpty = l.isEmpty :=
|
||||
DTreeMap.Raw.Const.isEmpty_unitOfList
|
||||
|
||||
@[simp]
|
||||
theorem getElem?_unitOfList [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List α} {k : α} :
|
||||
(unitOfList l cmp)[k]? = if l.contains k then some () else none :=
|
||||
DTreeMap.Raw.Const.get?_unitOfList
|
||||
|
||||
@[simp]
|
||||
theorem getElem_unitOfList {l : List α} {k : α} {h} :
|
||||
(unitOfList l cmp)[k]'h = () :=
|
||||
DTreeMap.Raw.Const.get_unitOfList
|
||||
|
||||
@[simp]
|
||||
theorem getElem!_unitOfList {l : List α} {k : α} :
|
||||
(unitOfList l cmp)[k]! = () :=
|
||||
DTreeMap.Raw.Const.get!_unitOfList
|
||||
|
||||
@[simp]
|
||||
theorem getD_unitOfList {l : List α} {k : α} {fallback : Unit} :
|
||||
getD (unitOfList l cmp) k fallback = () :=
|
||||
DTreeMap.Raw.Const.getD_unitOfList
|
||||
|
||||
end Std.TreeMap.Raw
|
||||
|
|
|
|||
|
|
@ -515,4 +515,90 @@ theorem isEmpty_insertMany_list [TransCmp cmp] {l : List α} :
|
|||
(insertMany t l).isEmpty = (t.isEmpty && l.isEmpty) :=
|
||||
TreeMap.isEmpty_insertManyIfNewUnit_list
|
||||
|
||||
@[simp]
|
||||
theorem ofList_nil :
|
||||
ofList ([] : List α) cmp =
|
||||
(∅ : TreeSet α cmp) :=
|
||||
rfl
|
||||
|
||||
@[simp]
|
||||
theorem ofList_singleton {k : α} :
|
||||
ofList [k] cmp = (∅ : TreeSet α cmp).insert k :=
|
||||
rfl
|
||||
|
||||
theorem ofList_cons {hd : α} {tl : List α} :
|
||||
ofList (hd :: tl) cmp =
|
||||
insertMany ((∅ : TreeSet α cmp).insert hd) tl :=
|
||||
ext TreeMap.unitOfList_cons
|
||||
|
||||
@[simp]
|
||||
theorem contains_ofList [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List α} {k : α} :
|
||||
(ofList l cmp).contains k = l.contains k :=
|
||||
TreeMap.contains_unitOfList
|
||||
|
||||
@[simp]
|
||||
theorem mem_ofList [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List α} {k : α} :
|
||||
k ∈ ofList l cmp ↔ l.contains k := by
|
||||
simp [mem_iff_contains]
|
||||
|
||||
theorem get?_ofList_of_contains_eq_false [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
|
||||
{l : List α} {k : α}
|
||||
(contains_eq_false : l.contains k = false) :
|
||||
get? (ofList l cmp) k = none :=
|
||||
TreeMap.getKey?_unitOfList_of_contains_eq_false contains_eq_false
|
||||
|
||||
theorem get?_ofList_of_mem [TransCmp cmp]
|
||||
{l : List α} {k k' : α} (k_eq : cmp k k' = .eq)
|
||||
(distinct : l.Pairwise (fun a b => ¬ cmp a b = .eq)) (mem : k ∈ l) :
|
||||
get? (ofList l cmp) k' = some k :=
|
||||
TreeMap.getKey?_unitOfList_of_mem k_eq distinct mem
|
||||
|
||||
theorem get_ofList_of_mem [TransCmp cmp]
|
||||
{l : List α}
|
||||
{k k' : α} (k_eq : cmp k k' = .eq)
|
||||
(distinct : l.Pairwise (fun a b => ¬ cmp a b = .eq))
|
||||
(mem : k ∈ l) {h'} :
|
||||
get (ofList l cmp) k' h' = k :=
|
||||
TreeMap.getKey_unitOfList_of_mem k_eq distinct mem
|
||||
|
||||
theorem get!_ofList_of_contains_eq_false [TransCmp cmp] [BEq α]
|
||||
[LawfulBEqCmp cmp] [Inhabited α] {l : List α} {k : α}
|
||||
(contains_eq_false : l.contains k = false) :
|
||||
get! (ofList l cmp) k = default :=
|
||||
TreeMap.getKey!_unitOfList_of_contains_eq_false contains_eq_false
|
||||
|
||||
theorem get!_ofList_of_mem [TransCmp cmp]
|
||||
[Inhabited α] {l : List α} {k k' : α} (k_eq : cmp k k' = .eq)
|
||||
(distinct : l.Pairwise (fun a b => ¬ cmp a b = .eq))
|
||||
(mem : k ∈ l) :
|
||||
get! (ofList l cmp) k' = k :=
|
||||
TreeMap.getKey!_unitOfList_of_mem k_eq distinct mem
|
||||
|
||||
theorem getD_ofList_of_contains_eq_false [TransCmp cmp] [BEq α]
|
||||
[LawfulBEqCmp cmp] {l : List α} {k fallback : α}
|
||||
(contains_eq_false : l.contains k = false) :
|
||||
getD (ofList l cmp) k fallback = fallback :=
|
||||
TreeMap.getKeyD_unitOfList_of_contains_eq_false contains_eq_false
|
||||
|
||||
theorem getD_ofList_of_mem [TransCmp cmp]
|
||||
{l : List α} {k k' fallback : α} (k_eq : cmp k k' = .eq)
|
||||
(distinct : l.Pairwise (fun a b => ¬ cmp a b = .eq))
|
||||
(mem : k ∈ l) :
|
||||
getD (ofList l cmp) k' fallback = k :=
|
||||
TreeMap.getKeyD_unitOfList_of_mem k_eq distinct mem
|
||||
|
||||
theorem size_ofList [TransCmp cmp] {l : List α}
|
||||
(distinct : l.Pairwise (fun a b => ¬ cmp a b = .eq)) :
|
||||
(ofList l cmp).size = l.length :=
|
||||
TreeMap.size_unitOfList distinct
|
||||
|
||||
theorem size_ofList_le [TransCmp cmp] {l : List α} :
|
||||
(ofList l cmp).size ≤ l.length :=
|
||||
TreeMap.size_unitOfList_le
|
||||
|
||||
@[simp]
|
||||
theorem isEmpty_ofList [TransCmp cmp] {l : List α} :
|
||||
(ofList l cmp).isEmpty = l.isEmpty :=
|
||||
TreeMap.isEmpty_unitOfList
|
||||
|
||||
end Std.TreeSet
|
||||
|
|
|
|||
|
|
@ -511,4 +511,90 @@ theorem isEmpty_insertMany_list [TransCmp cmp] (h : t.WF) {l : List α} :
|
|||
(insertMany t l).isEmpty = (t.isEmpty && l.isEmpty) :=
|
||||
TreeMap.Raw.isEmpty_insertManyIfNewUnit_list h
|
||||
|
||||
@[simp]
|
||||
theorem ofList_nil :
|
||||
ofList ([] : List α) cmp =
|
||||
(∅ : Raw α cmp) :=
|
||||
rfl
|
||||
|
||||
@[simp]
|
||||
theorem ofList_singleton {k : α} :
|
||||
ofList [k] cmp = (∅ : Raw α cmp).insert k :=
|
||||
rfl
|
||||
|
||||
theorem ofList_cons {hd : α} {tl : List α} :
|
||||
ofList (hd :: tl) cmp =
|
||||
insertMany ((∅ : Raw α cmp).insert hd) tl :=
|
||||
ext TreeMap.Raw.unitOfList_cons
|
||||
|
||||
@[simp]
|
||||
theorem contains_ofList [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List α} {k : α} :
|
||||
(ofList l cmp).contains k = l.contains k :=
|
||||
TreeMap.Raw.contains_unitOfList
|
||||
|
||||
@[simp]
|
||||
theorem mem_ofList [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List α} {k : α} :
|
||||
k ∈ ofList l cmp ↔ l.contains k := by
|
||||
simp [mem_iff_contains]
|
||||
|
||||
theorem get?_ofList_of_contains_eq_false [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
|
||||
{l : List α} {k : α}
|
||||
(contains_eq_false : l.contains k = false) :
|
||||
get? (ofList l cmp) k = none :=
|
||||
TreeMap.Raw.getKey?_unitOfList_of_contains_eq_false contains_eq_false
|
||||
|
||||
theorem get?_ofList_of_mem [TransCmp cmp]
|
||||
{l : List α} {k k' : α} (k_eq : cmp k k' = .eq)
|
||||
(distinct : l.Pairwise (fun a b => ¬ cmp a b = .eq)) (mem : k ∈ l) :
|
||||
get? (ofList l cmp) k' = some k :=
|
||||
TreeMap.Raw.getKey?_unitOfList_of_mem k_eq distinct mem
|
||||
|
||||
theorem get_ofList_of_mem [TransCmp cmp]
|
||||
{l : List α}
|
||||
{k k' : α} (k_eq : cmp k k' = .eq)
|
||||
(distinct : l.Pairwise (fun a b => ¬ cmp a b = .eq))
|
||||
(mem : k ∈ l) {h'} :
|
||||
get (ofList l cmp) k' h' = k :=
|
||||
TreeMap.Raw.getKey_unitOfList_of_mem k_eq distinct mem
|
||||
|
||||
theorem get!_ofList_of_contains_eq_false [TransCmp cmp] [BEq α]
|
||||
[LawfulBEqCmp cmp] [Inhabited α] {l : List α} {k : α}
|
||||
(contains_eq_false : l.contains k = false) :
|
||||
get! (ofList l cmp) k = default :=
|
||||
TreeMap.Raw.getKey!_unitOfList_of_contains_eq_false contains_eq_false
|
||||
|
||||
theorem get!_ofList_of_mem [TransCmp cmp]
|
||||
[Inhabited α] {l : List α} {k k' : α} (k_eq : cmp k k' = .eq)
|
||||
(distinct : l.Pairwise (fun a b => ¬ cmp a b = .eq))
|
||||
(mem : k ∈ l) :
|
||||
get! (ofList l cmp) k' = k :=
|
||||
TreeMap.Raw.getKey!_unitOfList_of_mem k_eq distinct mem
|
||||
|
||||
theorem getD_ofList_of_contains_eq_false [TransCmp cmp] [BEq α]
|
||||
[LawfulBEqCmp cmp] {l : List α} {k fallback : α}
|
||||
(contains_eq_false : l.contains k = false) :
|
||||
getD (ofList l cmp) k fallback = fallback :=
|
||||
TreeMap.Raw.getKeyD_unitOfList_of_contains_eq_false contains_eq_false
|
||||
|
||||
theorem getD_ofList_of_mem [TransCmp cmp]
|
||||
{l : List α} {k k' fallback : α} (k_eq : cmp k k' = .eq)
|
||||
(distinct : l.Pairwise (fun a b => ¬ cmp a b = .eq))
|
||||
(mem : k ∈ l) :
|
||||
getD (ofList l cmp) k' fallback = k :=
|
||||
TreeMap.Raw.getKeyD_unitOfList_of_mem k_eq distinct mem
|
||||
|
||||
theorem size_ofList [TransCmp cmp] {l : List α}
|
||||
(distinct : l.Pairwise (fun a b => ¬ cmp a b = .eq)) :
|
||||
(ofList l cmp).size = l.length :=
|
||||
TreeMap.Raw.size_unitOfList distinct
|
||||
|
||||
theorem size_ofList_le [TransCmp cmp] {l : List α} :
|
||||
(ofList l cmp).size ≤ l.length :=
|
||||
TreeMap.Raw.size_unitOfList_le
|
||||
|
||||
@[simp]
|
||||
theorem isEmpty_ofList [TransCmp cmp] {l : List α} :
|
||||
(ofList l cmp).isEmpty = l.isEmpty :=
|
||||
TreeMap.Raw.isEmpty_unitOfList
|
||||
|
||||
end Std.TreeSet.Raw
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue