chore: remove oldSectionVars from hash map lemmas (#5023)
This commit is contained in:
Markus Himmel
GitHub
parent
7c5d8661f4
commit
dcadfd1c89
4 changed files with 462 additions and 422 deletions
|
|
@ -57,9 +57,15 @@ end empty
|
|||
|
||||
namespace Raw₀
|
||||
|
||||
variable (m : Raw₀ α β)
|
||||
|
||||
@[simp]
|
||||
theorem size_empty {c} : (empty c : Raw₀ α β).1.size = 0 := rfl
|
||||
|
||||
theorem isEmpty_eq_size_eq_zero : m.1.isEmpty = (m.1.size == 0) := by
|
||||
simp [Raw.isEmpty]
|
||||
|
||||
variable [BEq α] [Hashable α]
|
||||
variable (m : Raw₀ α β) (h : m.1.WF)
|
||||
set_option deprecated.oldSectionVars true
|
||||
|
||||
/-- Internal implementation detail of the hash map -/
|
||||
scoped macro "wf_trivial" : tactic => `(tactic|
|
||||
|
|
@ -109,11 +115,11 @@ theorem isEmpty_empty {c} : (empty c : Raw₀ α β).1.isEmpty := by
|
|||
rw [Raw.isEmpty_eq_isEmpty wfImp_empty, toListModel_buckets_empty, List.isEmpty_nil]
|
||||
|
||||
@[simp]
|
||||
theorem isEmpty_insert [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
|
||||
theorem isEmpty_insert [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k : α} {v : β k} :
|
||||
(m.insert k v).1.isEmpty = false := by
|
||||
simp_to_model using List.isEmpty_insertEntry
|
||||
|
||||
theorem contains_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a == b) :
|
||||
theorem contains_congr [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {a b : α} (hab : a == b) :
|
||||
m.contains a = m.contains b := by
|
||||
simp_to_model using List.containsKey_congr hab
|
||||
|
||||
|
|
@ -121,45 +127,39 @@ theorem contains_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a ==
|
|||
theorem contains_empty {a : α} {c : Nat} : (empty c : Raw₀ α β).contains a = false := by
|
||||
simp [contains]
|
||||
|
||||
theorem contains_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} :
|
||||
theorem contains_of_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {a : α} :
|
||||
m.1.isEmpty = true → m.contains a = false := by
|
||||
simp_to_model; empty
|
||||
|
||||
theorem isEmpty_eq_false_iff_exists_contains_eq_true [EquivBEq α] [LawfulHashable α] :
|
||||
theorem isEmpty_eq_false_iff_exists_contains_eq_true [EquivBEq α] [LawfulHashable α] (h : m.1.WF) :
|
||||
m.1.isEmpty = false ↔ ∃ a, m.contains a = true := by
|
||||
simp_to_model using List.isEmpty_eq_false_iff_exists_containsKey
|
||||
|
||||
theorem isEmpty_iff_forall_contains [EquivBEq α] [LawfulHashable α] :
|
||||
theorem isEmpty_iff_forall_contains [EquivBEq α] [LawfulHashable α] (h : m.1.WF) :
|
||||
m.1.isEmpty ↔ ∀ a, m.contains a = false := by
|
||||
simp_to_model using List.isEmpty_iff_forall_containsKey
|
||||
|
||||
theorem contains_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
|
||||
theorem contains_insert [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k a : α} {v : β k} :
|
||||
(m.insert k v).contains a = ((k == a) || m.contains a) := by
|
||||
simp_to_model using List.containsKey_insertEntry
|
||||
|
||||
theorem contains_of_contains_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
|
||||
(m.insert k v).contains a → (k == a) = false → m.contains a := by
|
||||
theorem contains_of_contains_insert [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k a : α}
|
||||
{v : β k} : (m.insert k v).contains a → (k == a) = false → m.contains a := by
|
||||
simp_to_model using List.containsKey_of_containsKey_insertEntry
|
||||
|
||||
theorem contains_insert_self [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
|
||||
theorem contains_insert_self [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k : α} {v : β k} :
|
||||
(m.insert k v).contains k := by
|
||||
simp_to_model using List.containsKey_insertEntry_self
|
||||
|
||||
@[simp]
|
||||
theorem size_empty {c} : (empty c : Raw₀ α β).1.size = 0 := rfl
|
||||
|
||||
theorem isEmpty_eq_size_eq_zero : m.1.isEmpty = (m.1.size == 0) := by
|
||||
simp [Raw.isEmpty]
|
||||
|
||||
theorem size_insert [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
|
||||
theorem size_insert [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k : α} {v : β k} :
|
||||
(m.insert k v).1.size = if m.contains k then m.1.size else m.1.size + 1 := by
|
||||
simp_to_model using List.length_insertEntry
|
||||
|
||||
theorem size_le_size_insert [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
|
||||
theorem size_le_size_insert [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k : α} {v : β k} :
|
||||
m.1.size ≤ (m.insert k v).1.size := by
|
||||
simp_to_model using List.length_le_length_insertEntry
|
||||
|
||||
theorem size_insert_le [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
|
||||
theorem size_insert_le [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k : α} {v : β k} :
|
||||
(m.insert k v).1.size ≤ m.1.size + 1 := by
|
||||
simp_to_model using List.length_insertEntry_le
|
||||
|
||||
|
|
@ -167,27 +167,27 @@ theorem size_insert_le [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
|
|||
theorem erase_empty {k : α} {c : Nat} : (empty c : Raw₀ α β).erase k = empty c := by
|
||||
simp [erase, empty]
|
||||
|
||||
theorem isEmpty_erase [EquivBEq α] [LawfulHashable α] {k : α} :
|
||||
theorem isEmpty_erase [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k : α} :
|
||||
(m.erase k).1.isEmpty = (m.1.isEmpty || (m.1.size == 1 && m.contains k)) := by
|
||||
simp_to_model using List.isEmpty_eraseKey
|
||||
|
||||
theorem contains_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
|
||||
theorem contains_erase [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k a : α} :
|
||||
(m.erase k).contains a = (!(k == a) && m.contains a) := by
|
||||
simp_to_model using List.containsKey_eraseKey
|
||||
|
||||
theorem contains_of_contains_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
|
||||
theorem contains_of_contains_erase [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k a : α} :
|
||||
(m.erase k).contains a → m.contains a := by
|
||||
simp_to_model using List.containsKey_of_containsKey_eraseKey
|
||||
|
||||
theorem size_erase [EquivBEq α] [LawfulHashable α] {k : α} :
|
||||
theorem size_erase [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k : α} :
|
||||
(m.erase k).1.size = if m.contains k then m.1.size - 1 else m.1.size := by
|
||||
simp_to_model using List.length_eraseKey
|
||||
|
||||
theorem size_erase_le [EquivBEq α] [LawfulHashable α] {k : α} :
|
||||
theorem size_erase_le [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k : α} :
|
||||
(m.erase k).1.size ≤ m.1.size := by
|
||||
simp_to_model using List.length_eraseKey_le
|
||||
|
||||
theorem size_le_size_erase [EquivBEq α] [LawfulHashable α] {k : α} :
|
||||
theorem size_le_size_erase [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k : α} :
|
||||
m.1.size ≤ (m.erase k).1.size + 1 := by
|
||||
simp_to_model using List.length_le_length_eraseKey
|
||||
|
||||
|
|
@ -213,27 +213,31 @@ theorem containsThenInsertIfNew_snd {k : α} {v : β k} :
|
|||
theorem get?_empty [LawfulBEq α] {a : α} {c} : (empty c : Raw₀ α β).get? a = none := by
|
||||
simp [get?]
|
||||
|
||||
theorem get?_of_isEmpty [LawfulBEq α] {a : α} : m.1.isEmpty = true → m.get? a = none := by
|
||||
theorem get?_of_isEmpty [LawfulBEq α] (h : m.1.WF) {a : α} :
|
||||
m.1.isEmpty = true → m.get? a = none := by
|
||||
simp_to_model; empty
|
||||
|
||||
theorem get?_insert [LawfulBEq α] {a k : α} {v : β k} : (m.insert k v).get? a =
|
||||
theorem get?_insert [LawfulBEq α] (h : m.1.WF) {a k : α} {v : β k} : (m.insert k v).get? a =
|
||||
if h : k == a then some (cast (congrArg β (eq_of_beq h)) v) else m.get? a := by
|
||||
simp_to_model using List.getValueCast?_insertEntry
|
||||
|
||||
theorem get?_insert_self [LawfulBEq α] {k : α} {v : β k} : (m.insert k v).get? k = some v := by
|
||||
theorem get?_insert_self [LawfulBEq α] (h : m.1.WF) {k : α} {v : β k} :
|
||||
(m.insert k v).get? k = some v := by
|
||||
simp_to_model using List.getValueCast?_insertEntry_self
|
||||
|
||||
theorem contains_eq_isSome_get? [LawfulBEq α] {a : α} : m.contains a = (m.get? a).isSome := by
|
||||
theorem contains_eq_isSome_get? [LawfulBEq α] (h : m.1.WF) {a : α} :
|
||||
m.contains a = (m.get? a).isSome := by
|
||||
simp_to_model using List.containsKey_eq_isSome_getValueCast?
|
||||
|
||||
theorem get?_eq_none [LawfulBEq α] {a : α} : m.contains a = false → m.get? a = none := by
|
||||
theorem get?_eq_none [LawfulBEq α] (h : m.1.WF) {a : α} :
|
||||
m.contains a = false → m.get? a = none := by
|
||||
simp_to_model using List.getValueCast?_eq_none
|
||||
|
||||
theorem get?_erase [LawfulBEq α] {k a : α} :
|
||||
theorem get?_erase [LawfulBEq α] (h : m.1.WF) {k a : α} :
|
||||
(m.erase k).get? a = if k == a then none else m.get? a := by
|
||||
simp_to_model using List.getValueCast?_eraseKey
|
||||
|
||||
theorem get?_erase_self [LawfulBEq α] {k : α} : (m.erase k).get? k = none := by
|
||||
theorem get?_erase_self [LawfulBEq α] (h : m.1.WF) {k : α} : (m.erase k).get? k = none := by
|
||||
simp_to_model using List.getValueCast?_eraseKey_self
|
||||
|
||||
namespace Const
|
||||
|
|
@ -244,44 +248,44 @@ variable {β : Type v} (m : Raw₀ α (fun _ => β)) (h : m.1.WF)
|
|||
theorem get?_empty {a : α} {c} : get? (empty c : Raw₀ α (fun _ => β)) a = none := by
|
||||
simp [get?]
|
||||
|
||||
theorem get?_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} :
|
||||
theorem get?_of_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {a : α} :
|
||||
m.1.isEmpty = true → get? m a = none := by
|
||||
simp_to_model; empty
|
||||
|
||||
theorem get?_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
|
||||
theorem get?_insert [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k a : α} {v : β} :
|
||||
get? (m.insert k v) a = if k == a then some v else get? m a := by
|
||||
simp_to_model using List.getValue?_insertEntry
|
||||
|
||||
theorem get?_insert_self [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
|
||||
theorem get?_insert_self [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k : α} {v : β} :
|
||||
get? (m.insert k v) k = some v := by
|
||||
simp_to_model using List.getValue?_insertEntry_self
|
||||
|
||||
theorem contains_eq_isSome_get? [EquivBEq α] [LawfulHashable α] {a : α} :
|
||||
theorem contains_eq_isSome_get? [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {a : α} :
|
||||
m.contains a = (get? m a).isSome := by
|
||||
simp_to_model using List.containsKey_eq_isSome_getValue?
|
||||
|
||||
theorem get?_eq_none [EquivBEq α] [LawfulHashable α] {a : α} :
|
||||
theorem get?_eq_none [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {a : α} :
|
||||
m.contains a = false → get? m a = none := by
|
||||
simp_to_model using List.getValue?_eq_none.2
|
||||
|
||||
theorem get?_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
|
||||
theorem get?_erase [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k a : α} :
|
||||
Const.get? (m.erase k) a = if k == a then none else get? m a := by
|
||||
simp_to_model using List.getValue?_eraseKey
|
||||
|
||||
theorem get?_erase_self [EquivBEq α] [LawfulHashable α] {k : α} :
|
||||
theorem get?_erase_self [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k : α} :
|
||||
get? (m.erase k) k = none := by
|
||||
simp_to_model using List.getValue?_eraseKey_self
|
||||
|
||||
theorem get?_eq_get? [LawfulBEq α] {a : α} : get? m a = m.get? a := by
|
||||
theorem get?_eq_get? [LawfulBEq α] (h : m.1.WF) {a : α} : get? m a = m.get? a := by
|
||||
simp_to_model using List.getValue?_eq_getValueCast?
|
||||
|
||||
theorem get?_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a == b) :
|
||||
theorem get?_congr [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {a b : α} (hab : a == b) :
|
||||
get? m a = get? m b := by
|
||||
simp_to_model using List.getValue?_congr
|
||||
|
||||
end Const
|
||||
|
||||
theorem get_insert [LawfulBEq α] {k a : α} {v : β k} {h₁} :
|
||||
theorem get_insert [LawfulBEq α] (h : m.1.WF) {k a : α} {v : β k} {h₁} :
|
||||
(m.insert k v).get a h₁ =
|
||||
if h₂ : k == a then
|
||||
cast (congrArg β (eq_of_beq h₂)) v
|
||||
|
|
@ -289,45 +293,45 @@ theorem get_insert [LawfulBEq α] {k a : α} {v : β k} {h₁} :
|
|||
m.get a (contains_of_contains_insert _ h h₁ (Bool.eq_false_iff.2 h₂)) := by
|
||||
simp_to_model using List.getValueCast_insertEntry
|
||||
|
||||
theorem get_insert_self [LawfulBEq α] {k : α} {v : β k} :
|
||||
theorem get_insert_self [LawfulBEq α] (h : m.1.WF) {k : α} {v : β k} :
|
||||
(m.insert k v).get k (contains_insert_self _ h) = v := by
|
||||
simp_to_model using List.getValueCast_insertEntry_self
|
||||
|
||||
@[simp]
|
||||
theorem get_erase [LawfulBEq α] {k a : α} {h'} :
|
||||
theorem get_erase [LawfulBEq α] (h : m.1.WF) {k a : α} {h'} :
|
||||
(m.erase k).get a h' = m.get a (contains_of_contains_erase _ h h') := by
|
||||
simp_to_model using List.getValueCast_eraseKey
|
||||
|
||||
theorem get?_eq_some_get [LawfulBEq α] {a : α} {h} : m.get? a = some (m.get a h) := by
|
||||
theorem get?_eq_some_get [LawfulBEq α] (h : m.1.WF) {a : α} {h} : m.get? a = some (m.get a h) := by
|
||||
simp_to_model using List.getValueCast?_eq_some_getValueCast
|
||||
|
||||
namespace Const
|
||||
|
||||
variable {β : Type v} (m : Raw₀ α (fun _ => β)) (h : m.1.WF)
|
||||
|
||||
theorem get_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} {h₁} :
|
||||
theorem get_insert [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k a : α} {v : β} {h₁} :
|
||||
get (m.insert k v) a h₁ =
|
||||
if h₂ : k == a then v
|
||||
else get m a (contains_of_contains_insert _ h h₁ (Bool.eq_false_iff.2 h₂)) := by
|
||||
simp_to_model using List.getValue_insertEntry
|
||||
|
||||
theorem get_insert_self [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
|
||||
theorem get_insert_self [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k : α} {v : β} :
|
||||
get (m.insert k v) k (contains_insert_self _ h) = v := by
|
||||
simp_to_model using List.getValue_insertEntry_self
|
||||
|
||||
@[simp]
|
||||
theorem get_erase [EquivBEq α] [LawfulHashable α] {k a : α} {h'} :
|
||||
theorem get_erase [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k a : α} {h'} :
|
||||
get (m.erase k) a h' = get m a (contains_of_contains_erase _ h h') := by
|
||||
simp_to_model using List.getValue_eraseKey
|
||||
|
||||
theorem get?_eq_some_get [EquivBEq α] [LawfulHashable α] {a : α} {h} :
|
||||
theorem get?_eq_some_get [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {a : α} {h} :
|
||||
get? m a = some (get m a h) := by
|
||||
simp_to_model using List.getValue?_eq_some_getValue
|
||||
|
||||
theorem get_eq_get [LawfulBEq α] {a : α} {h} : get m a h = m.get a h := by
|
||||
theorem get_eq_get [LawfulBEq α] (h : m.1.WF) {a : α} {h} : get m a h = m.get a h := by
|
||||
simp_to_model using List.getValue_eq_getValueCast
|
||||
|
||||
theorem get_congr [LawfulBEq α] {a b : α} (hab : a == b) {h'} :
|
||||
theorem get_congr [LawfulBEq α] (h : m.1.WF) {a b : α} (hab : a == b) {h'} :
|
||||
get m a h' = get m b ((contains_congr _ h hab).symm.trans h') := by
|
||||
simp_to_model using List.getValue_congr
|
||||
|
||||
|
|
@ -337,40 +341,40 @@ theorem get!_empty [LawfulBEq α] {a : α} [Inhabited (β a)] {c} :
|
|||
(empty c : Raw₀ α β).get! a = default := by
|
||||
simp [get!, empty]
|
||||
|
||||
theorem get!_of_isEmpty [LawfulBEq α] {a : α} [Inhabited (β a)] :
|
||||
theorem get!_of_isEmpty [LawfulBEq α] (h : m.1.WF) {a : α} [Inhabited (β a)] :
|
||||
m.1.isEmpty = true → m.get! a = default := by
|
||||
simp_to_model; empty
|
||||
|
||||
theorem get!_insert [LawfulBEq α] {k a : α} [Inhabited (β a)] {v : β k} :
|
||||
theorem get!_insert [LawfulBEq α] (h : m.1.WF) {k a : α} [Inhabited (β a)] {v : β k} :
|
||||
(m.insert k v).get! a =
|
||||
if h : k == a then cast (congrArg β (eq_of_beq h)) v else m.get! a := by
|
||||
simp_to_model using List.getValueCast!_insertEntry
|
||||
|
||||
theorem get!_insert_self [LawfulBEq α] {a : α} [Inhabited (β a)] {b : β a} :
|
||||
theorem get!_insert_self [LawfulBEq α] (h : m.1.WF) {a : α} [Inhabited (β a)] {b : β a} :
|
||||
(m.insert a b).get! a = b := by
|
||||
simp_to_model using List.getValueCast!_insertEntry_self
|
||||
|
||||
theorem get!_eq_default [LawfulBEq α] {a : α} [Inhabited (β a)] :
|
||||
theorem get!_eq_default [LawfulBEq α] (h : m.1.WF) {a : α} [Inhabited (β a)] :
|
||||
m.contains a = false → m.get! a = default := by
|
||||
simp_to_model using List.getValueCast!_eq_default
|
||||
|
||||
theorem get!_erase [LawfulBEq α] {k a : α} [Inhabited (β a)] :
|
||||
theorem get!_erase [LawfulBEq α] (h : m.1.WF) {k a : α} [Inhabited (β a)] :
|
||||
(m.erase k).get! a = if k == a then default else m.get! a := by
|
||||
simp_to_model using List.getValueCast!_eraseKey
|
||||
|
||||
theorem get!_erase_self [LawfulBEq α] {k : α} [Inhabited (β k)] :
|
||||
theorem get!_erase_self [LawfulBEq α] (h : m.1.WF) {k : α} [Inhabited (β k)] :
|
||||
(m.erase k).get! k = default := by
|
||||
simp_to_model using List.getValueCast!_eraseKey_self
|
||||
|
||||
theorem get?_eq_some_get! [LawfulBEq α] {a : α} [Inhabited (β a)] :
|
||||
theorem get?_eq_some_get! [LawfulBEq α] (h : m.1.WF) {a : α} [Inhabited (β a)] :
|
||||
m.contains a = true → m.get? a = some (m.get! a) := by
|
||||
simp_to_model using List.getValueCast?_eq_some_getValueCast!
|
||||
|
||||
theorem get!_eq_get!_get? [LawfulBEq α] {a : α} [Inhabited (β a)] :
|
||||
theorem get!_eq_get!_get? [LawfulBEq α] (h : m.1.WF) {a : α} [Inhabited (β a)] :
|
||||
m.get! a = (m.get? a).get! := by
|
||||
simp_to_model using List.getValueCast!_eq_getValueCast?
|
||||
|
||||
theorem get_eq_get! [LawfulBEq α] {a : α} [Inhabited (β a)] {h} :
|
||||
theorem get_eq_get! [LawfulBEq α] (h : m.1.WF) {a : α} [Inhabited (β a)] {h} :
|
||||
m.get a h = m.get! a := by
|
||||
simp_to_model using List.getValueCast_eq_getValueCast!
|
||||
|
||||
|
|
@ -382,48 +386,48 @@ theorem get!_empty [Inhabited β] {a : α} {c} :
|
|||
get! (empty c : Raw₀ α (fun _ => β)) a = default := by
|
||||
simp [get!, empty]
|
||||
|
||||
theorem get!_of_isEmpty [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α} :
|
||||
theorem get!_of_isEmpty [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.1.WF) {a : α} :
|
||||
m.1.isEmpty = true → get! m a = default := by
|
||||
simp_to_model; empty
|
||||
|
||||
theorem get!_insert [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} {v : β} :
|
||||
theorem get!_insert [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.1.WF) {k a : α} {v : β} :
|
||||
get! (m.insert k v) a = if k == a then v else get! m a := by
|
||||
simp_to_model using List.getValue!_insertEntry
|
||||
|
||||
theorem get!_insert_self [EquivBEq α] [LawfulHashable α] [Inhabited β] {k : α} {v : β} :
|
||||
get! (m.insert k v) k = v := by
|
||||
theorem get!_insert_self [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.1.WF) {k : α}
|
||||
{v : β} : get! (m.insert k v) k = v := by
|
||||
simp_to_model using List.getValue!_insertEntry_self
|
||||
|
||||
theorem get!_eq_default [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α} :
|
||||
theorem get!_eq_default [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.1.WF) {a : α} :
|
||||
m.contains a = false → get! m a = default := by
|
||||
simp_to_model using List.getValue!_eq_default
|
||||
|
||||
theorem get!_erase [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} :
|
||||
theorem get!_erase [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.1.WF) {k a : α} :
|
||||
get! (m.erase k) a = if k == a then default else get! m a := by
|
||||
simp_to_model using List.getValue!_eraseKey
|
||||
|
||||
theorem get!_erase_self [EquivBEq α] [LawfulHashable α] [Inhabited β] {k : α} :
|
||||
theorem get!_erase_self [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.1.WF) {k : α} :
|
||||
get! (m.erase k) k = default := by
|
||||
simp_to_model using List.getValue!_eraseKey_self
|
||||
|
||||
theorem get?_eq_some_get! [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α} :
|
||||
theorem get?_eq_some_get! [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.1.WF) {a : α} :
|
||||
m.contains a = true → get? m a = some (get! m a) := by
|
||||
simp_to_model using List.getValue?_eq_some_getValue!
|
||||
|
||||
theorem get!_eq_get!_get? [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α} :
|
||||
theorem get!_eq_get!_get? [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.1.WF) {a : α} :
|
||||
get! m a = (get? m a).get! := by
|
||||
simp_to_model using List.getValue!_eq_getValue?
|
||||
|
||||
theorem get_eq_get! [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α} {h} :
|
||||
theorem get_eq_get! [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.1.WF) {a : α} {h} :
|
||||
get m a h = get! m a := by
|
||||
simp_to_model using List.getValue_eq_getValue!
|
||||
|
||||
theorem get!_eq_get! [LawfulBEq α] [Inhabited β] {a : α} :
|
||||
theorem get!_eq_get! [LawfulBEq α] [Inhabited β] (h : m.1.WF) {a : α} :
|
||||
get! m a = m.get! a := by
|
||||
simp_to_model using List.getValue!_eq_getValueCast!
|
||||
|
||||
theorem get!_congr [EquivBEq α] [LawfulHashable α] [Inhabited β] {a b : α} (hab : a == b) :
|
||||
get! m a = get! m b := by
|
||||
theorem get!_congr [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.1.WF) {a b : α}
|
||||
(hab : a == b) : get! m a = get! m b := by
|
||||
simp_to_model using List.getValue!_congr
|
||||
|
||||
end Const
|
||||
|
|
@ -432,44 +436,44 @@ theorem getD_empty [LawfulBEq α] {a : α} {fallback : β a} {c} :
|
|||
(empty c : Raw₀ α β).getD a fallback = fallback := by
|
||||
simp [getD, empty]
|
||||
|
||||
theorem getD_of_isEmpty [LawfulBEq α] {a : α} {fallback : β a} :
|
||||
theorem getD_of_isEmpty [LawfulBEq α] (h : m.1.WF) {a : α} {fallback : β a} :
|
||||
m.1.isEmpty = true → m.getD a fallback = fallback := by
|
||||
simp_to_model; empty
|
||||
|
||||
theorem getD_insert [LawfulBEq α] {k a : α} {fallback : β a} {v : β k} :
|
||||
theorem getD_insert [LawfulBEq α] (h : m.1.WF) {k a : α} {fallback : β a} {v : β k} :
|
||||
(m.insert k v).getD a fallback =
|
||||
if h : k == a then cast (congrArg β (eq_of_beq h)) v else m.getD a fallback := by
|
||||
simp_to_model using List.getValueCastD_insertEntry
|
||||
|
||||
theorem getD_insert_self [LawfulBEq α] {a : α} {fallback b : β a} :
|
||||
theorem getD_insert_self [LawfulBEq α] (h : m.1.WF) {a : α} {fallback b : β a} :
|
||||
(m.insert a b).getD a fallback = b := by
|
||||
simp_to_model using List.getValueCastD_insertEntry_self
|
||||
|
||||
theorem getD_eq_fallback [LawfulBEq α] {a : α} {fallback : β a} :
|
||||
theorem getD_eq_fallback [LawfulBEq α] (h : m.1.WF) {a : α} {fallback : β a} :
|
||||
m.contains a = false → m.getD a fallback = fallback := by
|
||||
simp_to_model using List.getValueCastD_eq_fallback
|
||||
|
||||
theorem getD_erase [LawfulBEq α] {k a : α} {fallback : β a} :
|
||||
theorem getD_erase [LawfulBEq α] (h : m.1.WF) {k a : α} {fallback : β a} :
|
||||
(m.erase k).getD a fallback = if k == a then fallback else m.getD a fallback := by
|
||||
simp_to_model using List.getValueCastD_eraseKey
|
||||
|
||||
theorem getD_erase_self [LawfulBEq α] {k : α} {fallback : β k} :
|
||||
theorem getD_erase_self [LawfulBEq α] (h : m.1.WF) {k : α} {fallback : β k} :
|
||||
(m.erase k).getD k fallback = fallback := by
|
||||
simp_to_model using List.getValueCastD_eraseKey_self
|
||||
|
||||
theorem get?_eq_some_getD [LawfulBEq α] {a : α} {fallback : β a} :
|
||||
theorem get?_eq_some_getD [LawfulBEq α] (h : m.1.WF) {a : α} {fallback : β a} :
|
||||
m.contains a = true → m.get? a = some (m.getD a fallback) := by
|
||||
simp_to_model using List.getValueCast?_eq_some_getValueCastD
|
||||
|
||||
theorem getD_eq_getD_get? [LawfulBEq α] {a : α} {fallback : β a} :
|
||||
theorem getD_eq_getD_get? [LawfulBEq α] (h : m.1.WF) {a : α} {fallback : β a} :
|
||||
m.getD a fallback = (m.get? a).getD fallback := by
|
||||
simp_to_model using List.getValueCastD_eq_getValueCast?
|
||||
|
||||
theorem get_eq_getD [LawfulBEq α] {a : α} {fallback : β a} {h} :
|
||||
theorem get_eq_getD [LawfulBEq α] (h : m.1.WF) {a : α} {fallback : β a} {h} :
|
||||
m.get a h = m.getD a fallback := by
|
||||
simp_to_model using List.getValueCast_eq_getValueCastD
|
||||
|
||||
theorem get!_eq_getD_default [LawfulBEq α] {a : α} [Inhabited (β a)] :
|
||||
theorem get!_eq_getD_default [LawfulBEq α] (h : m.1.WF) {a : α} [Inhabited (β a)] :
|
||||
m.get! a = m.getD a default := by
|
||||
simp_to_model using List.getValueCast!_eq_getValueCastD_default
|
||||
|
||||
|
|
@ -481,109 +485,110 @@ theorem getD_empty {a : α} {fallback : β} {c} :
|
|||
getD (empty c : Raw₀ α (fun _ => β)) a fallback = fallback := by
|
||||
simp [getD, empty]
|
||||
|
||||
theorem getD_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} {fallback : β} :
|
||||
theorem getD_of_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {a : α} {fallback : β} :
|
||||
m.1.isEmpty = true → getD m a fallback = fallback := by
|
||||
simp_to_model; empty
|
||||
|
||||
theorem getD_insert [EquivBEq α] [LawfulHashable α] {k a : α} {fallback v : β} :
|
||||
theorem getD_insert [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k a : α} {fallback v : β} :
|
||||
getD (m.insert k v) a fallback = if k == a then v else getD m a fallback := by
|
||||
simp_to_model using List.getValueD_insertEntry
|
||||
|
||||
theorem getD_insert_self [EquivBEq α] [LawfulHashable α] {k : α} {fallback v : β} :
|
||||
theorem getD_insert_self [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k : α} {fallback v : β} :
|
||||
getD (m.insert k v) k fallback = v := by
|
||||
simp_to_model using List.getValueD_insertEntry_self
|
||||
|
||||
theorem getD_eq_fallback [EquivBEq α] [LawfulHashable α] {a : α} {fallback : β} :
|
||||
theorem getD_eq_fallback [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {a : α} {fallback : β} :
|
||||
m.contains a = false → getD m a fallback = fallback := by
|
||||
simp_to_model using List.getValueD_eq_fallback
|
||||
|
||||
theorem getD_erase [EquivBEq α] [LawfulHashable α] {k a : α} {fallback : β} :
|
||||
theorem getD_erase [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k a : α} {fallback : β} :
|
||||
getD (m.erase k) a fallback = if k == a then fallback else getD m a fallback := by
|
||||
simp_to_model using List.getValueD_eraseKey
|
||||
|
||||
theorem getD_erase_self [EquivBEq α] [LawfulHashable α] {k : α} {fallback : β} :
|
||||
theorem getD_erase_self [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k : α} {fallback : β} :
|
||||
getD (m.erase k) k fallback = fallback := by
|
||||
simp_to_model using List.getValueD_eraseKey_self
|
||||
|
||||
theorem get?_eq_some_getD [EquivBEq α] [LawfulHashable α] {a : α} {fallback : β} :
|
||||
theorem get?_eq_some_getD [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {a : α} {fallback : β} :
|
||||
m.contains a = true → get? m a = some (getD m a fallback) := by
|
||||
simp_to_model using List.getValue?_eq_some_getValueD
|
||||
|
||||
theorem getD_eq_getD_get? [EquivBEq α] [LawfulHashable α] {a : α} {fallback : β} :
|
||||
theorem getD_eq_getD_get? [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {a : α} {fallback : β} :
|
||||
getD m a fallback = (get? m a).getD fallback := by
|
||||
simp_to_model using List.getValueD_eq_getValue?
|
||||
|
||||
theorem get_eq_getD [EquivBEq α] [LawfulHashable α] {a : α} {fallback : β} {h} :
|
||||
theorem get_eq_getD [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {a : α} {fallback : β} {h} :
|
||||
get m a h = getD m a fallback := by
|
||||
simp_to_model using List.getValue_eq_getValueD
|
||||
|
||||
theorem get!_eq_getD_default [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α} :
|
||||
theorem get!_eq_getD_default [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.1.WF) {a : α} :
|
||||
get! m a = getD m a default := by
|
||||
simp_to_model using List.getValue!_eq_getValueD_default
|
||||
|
||||
theorem getD_eq_getD [LawfulBEq α] {a : α} {fallback : β} :
|
||||
theorem getD_eq_getD [LawfulBEq α] (h : m.1.WF) {a : α} {fallback : β} :
|
||||
getD m a fallback = m.getD a fallback := by
|
||||
simp_to_model using List.getValueD_eq_getValueCastD
|
||||
|
||||
theorem getD_congr [EquivBEq α] [LawfulHashable α] {a b : α} {fallback : β} (hab : a == b) :
|
||||
getD m a fallback = getD m b fallback := by
|
||||
theorem getD_congr [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {a b : α} {fallback : β}
|
||||
(hab : a == b) : getD m a fallback = getD m b fallback := by
|
||||
simp_to_model using List.getValueD_congr
|
||||
|
||||
end Const
|
||||
|
||||
theorem isEmpty_insertIfNew [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
|
||||
theorem isEmpty_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k : α} {v : β k} :
|
||||
(m.insertIfNew k v).1.isEmpty = false := by
|
||||
simp_to_model using List.isEmpty_insertEntryIfNew
|
||||
|
||||
theorem contains_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
|
||||
theorem contains_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k a : α} {v : β k} :
|
||||
(m.insertIfNew k v).contains a = (k == a || m.contains a) := by
|
||||
simp_to_model using List.containsKey_insertEntryIfNew
|
||||
|
||||
theorem contains_insertIfNew_self [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
|
||||
theorem contains_insertIfNew_self [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k : α} {v : β k} :
|
||||
(m.insertIfNew k v).contains k := by
|
||||
simp_to_model using List.containsKey_insertEntryIfNew_self
|
||||
|
||||
theorem contains_of_contains_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
|
||||
(m.insertIfNew k v).contains a → (k == a) = false → m.contains a := by
|
||||
theorem contains_of_contains_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k a : α}
|
||||
{v : β k} : (m.insertIfNew k v).contains a → (k == a) = false → m.contains a := by
|
||||
simp_to_model using List.containsKey_of_containsKey_insertEntryIfNew
|
||||
|
||||
/-- This is a restatement of `contains_insertIfNew` that is written to exactly match the proof
|
||||
obligation in the statement of `get_insertIfNew`. -/
|
||||
theorem contains_of_contains_insertIfNew' [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
|
||||
theorem contains_of_contains_insertIfNew' [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k a : α}
|
||||
{v : β k} :
|
||||
(m.insertIfNew k v).contains a → ¬((k == a) ∧ m.contains k = false) → m.contains a := by
|
||||
simp_to_model using List.containsKey_of_containsKey_insertEntryIfNew'
|
||||
|
||||
theorem size_insertIfNew [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
|
||||
theorem size_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k : α} {v : β k} :
|
||||
(m.insertIfNew k v).1.size = if m.contains k then m.1.size else m.1.size + 1 := by
|
||||
simp_to_model using List.length_insertEntryIfNew
|
||||
|
||||
theorem size_le_size_insertIfNew [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
|
||||
theorem size_le_size_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k : α} {v : β k} :
|
||||
m.1.size ≤ (m.insertIfNew k v).1.size := by
|
||||
simp_to_model using List.length_le_length_insertEntryIfNew
|
||||
|
||||
theorem size_insertIfNew_le [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
|
||||
theorem size_insertIfNew_le [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k : α} {v : β k} :
|
||||
(m.insertIfNew k v).1.size ≤ m.1.size + 1 := by
|
||||
simp_to_model using List.length_insertEntryIfNew_le
|
||||
|
||||
theorem get?_insertIfNew [LawfulBEq α] {k a : α} {v : β k} :
|
||||
theorem get?_insertIfNew [LawfulBEq α] (h : m.1.WF) {k a : α} {v : β k} :
|
||||
(m.insertIfNew k v).get? a =
|
||||
if h : k == a ∧ m.contains k = false then some (cast (congrArg β (eq_of_beq h.1)) v)
|
||||
else m.get? a := by
|
||||
simp_to_model using List.getValueCast?_insertEntryIfNew
|
||||
|
||||
theorem get_insertIfNew [LawfulBEq α] {k a : α} {v : β k} {h₁} :
|
||||
theorem get_insertIfNew [LawfulBEq α] (h : m.1.WF) {k a : α} {v : β k} {h₁} :
|
||||
(m.insertIfNew k v).get a h₁ =
|
||||
if h₂ : k == a ∧ m.contains k = false then cast (congrArg β (eq_of_beq h₂.1)) v
|
||||
else m.get a (contains_of_contains_insertIfNew' _ h h₁ h₂) := by
|
||||
simp_to_model using List.getValueCast_insertEntryIfNew
|
||||
|
||||
theorem get!_insertIfNew [LawfulBEq α] {k a : α} [Inhabited (β a)] {v : β k} :
|
||||
theorem get!_insertIfNew [LawfulBEq α] (h : m.1.WF) {k a : α} [Inhabited (β a)] {v : β k} :
|
||||
(m.insertIfNew k v).get! a =
|
||||
if h : k == a ∧ m.contains k = false then cast (congrArg β (eq_of_beq h.1)) v
|
||||
else m.get! a := by
|
||||
simp_to_model using List.getValueCast!_insertEntryIfNew
|
||||
|
||||
theorem getD_insertIfNew [LawfulBEq α] {k a : α} {fallback : β a} {v : β k} :
|
||||
theorem getD_insertIfNew [LawfulBEq α] (h : m.1.WF) {k a : α} {fallback : β a} {v : β k} :
|
||||
(m.insertIfNew k v).getD a fallback =
|
||||
if h : k == a ∧ m.contains k = false then cast (congrArg β (eq_of_beq h.1)) v
|
||||
else m.getD a fallback := by
|
||||
|
|
@ -593,21 +598,22 @@ namespace Const
|
|||
|
||||
variable {β : Type v} (m : Raw₀ α (fun _ => β)) (h : m.1.WF)
|
||||
|
||||
theorem get?_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
|
||||
theorem get?_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k a : α} {v : β} :
|
||||
get? (m.insertIfNew k v) a = if k == a ∧ m.contains k = false then some v else get? m a := by
|
||||
simp_to_model using List.getValue?_insertEntryIfNew
|
||||
|
||||
theorem get_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} {h₁} :
|
||||
theorem get_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k a : α} {v : β} {h₁} :
|
||||
get (m.insertIfNew k v) a h₁ =
|
||||
if h₂ : k == a ∧ m.contains k = false then v
|
||||
else get m a (contains_of_contains_insertIfNew' _ h h₁ h₂) := by
|
||||
simp_to_model using List.getValue_insertEntryIfNew
|
||||
|
||||
theorem get!_insertIfNew [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} {v : β} :
|
||||
theorem get!_insertIfNew [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.1.WF) {k a : α}
|
||||
{v : β} :
|
||||
get! (m.insertIfNew k v) a = if k == a ∧ m.contains k = false then v else get! m a := by
|
||||
simp_to_model using List.getValue!_insertEntryIfNew
|
||||
|
||||
theorem getD_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {fallback v : β} :
|
||||
theorem getD_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k a : α} {fallback v : β} :
|
||||
getD (m.insertIfNew k v) a fallback =
|
||||
if k == a ∧ m.contains k = false then v else getD m a fallback := by
|
||||
simp_to_model using List.getValueD_insertEntryIfNew
|
||||
|
|
|
|||
|
|
@ -22,7 +22,7 @@ set_option autoImplicit false
|
|||
|
||||
universe u v
|
||||
|
||||
variable {α : Type u} {β : α → Type v} [BEq α] [Hashable α]
|
||||
variable {α : Type u} {β : α → Type v}
|
||||
|
||||
namespace Std.DHashMap
|
||||
|
||||
|
|
@ -74,8 +74,20 @@ namespace Raw
|
|||
|
||||
open Internal.Raw₀ Internal.Raw
|
||||
|
||||
variable {m : Raw α β} (h : m.WF)
|
||||
set_option deprecated.oldSectionVars true
|
||||
variable {m : Raw α β}
|
||||
|
||||
@[simp]
|
||||
theorem size_empty {c} : (empty c : Raw α β).size = 0 := by
|
||||
simp_to_raw using Raw₀.size_empty
|
||||
|
||||
@[simp]
|
||||
theorem size_emptyc : (∅ : Raw α β).size = 0 :=
|
||||
size_empty
|
||||
|
||||
theorem isEmpty_eq_size_eq_zero : m.isEmpty = (m.size == 0) := by
|
||||
simp [isEmpty]
|
||||
|
||||
variable [BEq α] [Hashable α]
|
||||
|
||||
@[simp]
|
||||
theorem isEmpty_empty {c} : (empty c : Raw α β).isEmpty := by
|
||||
|
|
@ -86,18 +98,19 @@ theorem isEmpty_emptyc : (∅ : Raw α β).isEmpty :=
|
|||
isEmpty_empty
|
||||
|
||||
@[simp]
|
||||
theorem isEmpty_insert [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
|
||||
theorem isEmpty_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β k} :
|
||||
(m.insert k v).isEmpty = false := by
|
||||
simp_to_raw using Raw₀.isEmpty_insert
|
||||
|
||||
theorem mem_iff_contains [BEq α] [Hashable α] {m : Raw α β} {a : α} :
|
||||
theorem mem_iff_contains {m : Raw α β} {a : α} :
|
||||
a ∈ m ↔ m.contains a := Iff.rfl
|
||||
|
||||
theorem contains_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a == b) :
|
||||
theorem contains_congr [EquivBEq α] [LawfulHashable α] (h : m.WF) {a b : α} (hab : a == b) :
|
||||
m.contains a = m.contains b := by
|
||||
simp_to_raw using Raw₀.contains_congr
|
||||
|
||||
theorem mem_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a == b) : a ∈ m ↔ b ∈ m := by
|
||||
theorem mem_congr [EquivBEq α] [LawfulHashable α] (h : m.WF) {a b : α} (hab : a == b) :
|
||||
a ∈ m ↔ b ∈ m := by
|
||||
simp [mem_iff_contains, contains_congr h hab]
|
||||
|
||||
@[simp] theorem contains_empty {a : α} {c} : (empty c : Raw α β).contains a = false := by
|
||||
|
|
@ -112,78 +125,68 @@ theorem mem_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a == b) :
|
|||
@[simp] theorem not_mem_emptyc {a : α} : ¬a ∈ (∅ : Raw α β) :=
|
||||
not_mem_empty
|
||||
|
||||
theorem contains_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} :
|
||||
theorem contains_of_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
|
||||
m.isEmpty → m.contains a = false := by
|
||||
simp_to_raw using Raw₀.contains_of_isEmpty ⟨m, _⟩
|
||||
|
||||
theorem not_mem_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} :
|
||||
theorem not_mem_of_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
|
||||
m.isEmpty → ¬a ∈ m := by
|
||||
simpa [mem_iff_contains] using contains_of_isEmpty h
|
||||
|
||||
theorem isEmpty_eq_false_iff_exists_contains_eq_true [EquivBEq α] [LawfulHashable α] :
|
||||
theorem isEmpty_eq_false_iff_exists_contains_eq_true [EquivBEq α] [LawfulHashable α] (h : m.WF) :
|
||||
m.isEmpty = false ↔ ∃ a, m.contains a = true := by
|
||||
simp_to_raw using Raw₀.isEmpty_eq_false_iff_exists_contains_eq_true ⟨m, _⟩
|
||||
|
||||
theorem isEmpty_eq_false_iff_exists_mem [EquivBEq α] [LawfulHashable α] :
|
||||
theorem isEmpty_eq_false_iff_exists_mem [EquivBEq α] [LawfulHashable α] (h : m.WF) :
|
||||
m.isEmpty = false ↔ ∃ a, a ∈ m := by
|
||||
simpa [mem_iff_contains] using isEmpty_eq_false_iff_exists_contains_eq_true h
|
||||
|
||||
theorem isEmpty_iff_forall_contains [EquivBEq α] [LawfulHashable α] :
|
||||
theorem isEmpty_iff_forall_contains [EquivBEq α] [LawfulHashable α] (h : m.WF) :
|
||||
m.isEmpty = true ↔ ∀ a, m.contains a = false := by
|
||||
simp_to_raw using Raw₀.isEmpty_iff_forall_contains ⟨m, _⟩
|
||||
|
||||
theorem isEmpty_iff_forall_not_mem [EquivBEq α] [LawfulHashable α] :
|
||||
theorem isEmpty_iff_forall_not_mem [EquivBEq α] [LawfulHashable α] (h : m.WF) :
|
||||
m.isEmpty = true ↔ ∀ a, ¬a ∈ m := by
|
||||
simpa [mem_iff_contains] using isEmpty_iff_forall_contains h
|
||||
|
||||
@[simp]
|
||||
theorem contains_insert [EquivBEq α] [LawfulHashable α] {a k : α} {v : β k} :
|
||||
theorem contains_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {a k : α} {v : β k} :
|
||||
(m.insert k v).contains a = (k == a || m.contains a) := by
|
||||
simp_to_raw using Raw₀.contains_insert
|
||||
|
||||
@[simp]
|
||||
theorem mem_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
|
||||
theorem mem_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {v : β k} :
|
||||
a ∈ m.insert k v ↔ k == a ∨ a ∈ m := by
|
||||
simp [mem_iff_contains, contains_insert h]
|
||||
|
||||
theorem contains_of_contains_insert [EquivBEq α] [LawfulHashable α] {a k : α} {v : β k} :
|
||||
theorem contains_of_contains_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {a k : α} {v : β k} :
|
||||
(m.insert k v).contains a → (k == a) = false → m.contains a := by
|
||||
simp_to_raw using Raw₀.contains_of_contains_insert
|
||||
|
||||
theorem mem_of_mem_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
|
||||
theorem mem_of_mem_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {v : β k} :
|
||||
a ∈ m.insert k v → (k == a) = false → a ∈ m := by
|
||||
simpa [mem_iff_contains] using contains_of_contains_insert h
|
||||
|
||||
@[simp]
|
||||
theorem contains_insert_self [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
|
||||
theorem contains_insert_self [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β k} :
|
||||
(m.insert k v).contains k := by
|
||||
simp_to_raw using Raw₀.contains_insert_self
|
||||
|
||||
@[simp]
|
||||
theorem mem_insert_self [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} : k ∈ m.insert k v := by
|
||||
theorem mem_insert_self [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β k} :
|
||||
k ∈ m.insert k v := by
|
||||
simp [mem_iff_contains, contains_insert_self h]
|
||||
|
||||
@[simp]
|
||||
theorem size_empty {c} : (empty c : Raw α β).size = 0 := by
|
||||
simp_to_raw using Raw₀.size_empty
|
||||
|
||||
@[simp]
|
||||
theorem size_emptyc : (∅ : Raw α β).size = 0 :=
|
||||
size_empty
|
||||
|
||||
theorem isEmpty_eq_size_eq_zero : m.isEmpty = (m.size == 0) := by
|
||||
simp [isEmpty]
|
||||
|
||||
theorem size_insert [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
|
||||
theorem size_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β k} :
|
||||
(m.insert k v).size = if k ∈ m then m.size else m.size + 1 := by
|
||||
simp only [mem_iff_contains]
|
||||
simp_to_raw using Raw₀.size_insert
|
||||
|
||||
theorem size_le_size_insert [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
|
||||
theorem size_le_size_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β k} :
|
||||
m.size ≤ (m.insert k v).size := by
|
||||
simp_to_raw using Raw₀.size_le_size_insert ⟨m, _⟩ h
|
||||
|
||||
theorem size_insert_le [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
|
||||
theorem size_insert_le [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β k} :
|
||||
(m.insert k v).size ≤ m.size + 1 := by
|
||||
simp_to_raw using Raw₀.size_insert_le ⟨m, _⟩ h
|
||||
|
||||
|
|
@ -197,54 +200,58 @@ theorem erase_emptyc {k : α} : (∅ : Raw α β).erase k = ∅ :=
|
|||
erase_empty
|
||||
|
||||
@[simp]
|
||||
theorem isEmpty_erase [EquivBEq α] [LawfulHashable α] {k : α} :
|
||||
theorem isEmpty_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
|
||||
(m.erase k).isEmpty = (m.isEmpty || (m.size == 1 && m.contains k)) := by
|
||||
simp_to_raw using Raw₀.isEmpty_erase
|
||||
|
||||
@[simp]
|
||||
theorem contains_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
|
||||
theorem contains_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} :
|
||||
(m.erase k).contains a = (!(k == a) && m.contains a) := by
|
||||
simp_to_raw using Raw₀.contains_erase
|
||||
|
||||
@[simp]
|
||||
theorem mem_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
|
||||
theorem mem_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} :
|
||||
a ∈ m.erase k ↔ (k == a) = false ∧ a ∈ m := by
|
||||
simp [mem_iff_contains, contains_erase h]
|
||||
|
||||
theorem contains_of_contains_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
|
||||
theorem contains_of_contains_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} :
|
||||
(m.erase k).contains a → m.contains a := by
|
||||
simp_to_raw using Raw₀.contains_of_contains_erase
|
||||
|
||||
theorem mem_of_mem_erase [EquivBEq α] [LawfulHashable α] {k a : α} : a ∈ m.erase k → a ∈ m := by
|
||||
theorem mem_of_mem_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} :
|
||||
a ∈ m.erase k → a ∈ m := by
|
||||
simpa [mem_iff_contains] using contains_of_contains_erase h
|
||||
|
||||
theorem size_erase [EquivBEq α] [LawfulHashable α] {k : α} :
|
||||
theorem size_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
|
||||
(m.erase k).size = if k ∈ m then m.size - 1 else m.size := by
|
||||
simp only [mem_iff_contains]
|
||||
simp_to_raw using Raw₀.size_erase
|
||||
|
||||
theorem size_erase_le [EquivBEq α] [LawfulHashable α] {k : α} : (m.erase k).size ≤ m.size := by
|
||||
theorem size_erase_le [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
|
||||
(m.erase k).size ≤ m.size := by
|
||||
simp_to_raw using Raw₀.size_erase_le
|
||||
|
||||
theorem size_le_size_erase [EquivBEq α] [LawfulHashable α] {k : α} :
|
||||
theorem size_le_size_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
|
||||
m.size ≤ (m.erase k).size + 1 := by
|
||||
simp_to_raw using Raw₀.size_le_size_erase ⟨m, _⟩
|
||||
|
||||
@[simp]
|
||||
theorem containsThenInsert_fst {k : α} {v : β k} : (m.containsThenInsert k v).1 = m.contains k := by
|
||||
theorem containsThenInsert_fst (h : m.WF) {k : α} {v : β k} :
|
||||
(m.containsThenInsert k v).1 = m.contains k := by
|
||||
simp_to_raw using Raw₀.containsThenInsert_fst
|
||||
|
||||
@[simp]
|
||||
theorem containsThenInsert_snd {k : α} {v : β k} : (m.containsThenInsert k v).2 = m.insert k v := by
|
||||
theorem containsThenInsert_snd (h : m.WF) {k : α} {v : β k} :
|
||||
(m.containsThenInsert k v).2 = m.insert k v := by
|
||||
simp_to_raw using congrArg Subtype.val (Raw₀.containsThenInsert_snd _)
|
||||
|
||||
@[simp]
|
||||
theorem containsThenInsertIfNew_fst {k : α} {v : β k} :
|
||||
theorem containsThenInsertIfNew_fst (h : m.WF) {k : α} {v : β k} :
|
||||
(m.containsThenInsertIfNew k v).1 = m.contains k := by
|
||||
simp_to_raw using Raw₀.containsThenInsertIfNew_fst
|
||||
|
||||
@[simp]
|
||||
theorem containsThenInsertIfNew_snd {k : α} {v : β k} :
|
||||
theorem containsThenInsertIfNew_snd (h : m.WF) {k : α} {v : β k} :
|
||||
(m.containsThenInsertIfNew k v).2 = m.insertIfNew k v := by
|
||||
simp_to_raw using congrArg Subtype.val (Raw₀.containsThenInsertIfNew_snd _)
|
||||
|
||||
|
|
@ -256,33 +263,35 @@ theorem get?_empty [LawfulBEq α] {a : α} {c} : (empty c : Raw α β).get? a =
|
|||
theorem get?_emptyc [LawfulBEq α] {a : α} : (∅ : Raw α β).get? a = none :=
|
||||
get?_empty
|
||||
|
||||
theorem get?_of_isEmpty [LawfulBEq α] {a : α} : m.isEmpty = true → m.get? a = none := by
|
||||
theorem get?_of_isEmpty [LawfulBEq α] (h : m.WF) {a : α} : m.isEmpty = true → m.get? a = none := by
|
||||
simp_to_raw using Raw₀.get?_of_isEmpty ⟨m, _⟩
|
||||
|
||||
theorem get?_insert [LawfulBEq α] {a k : α} {v : β k} : (m.insert k v).get? a =
|
||||
theorem get?_insert [LawfulBEq α] (h : m.WF) {a k : α} {v : β k} : (m.insert k v).get? a =
|
||||
if h : k == a then some (cast (congrArg β (eq_of_beq h)) v) else m.get? a := by
|
||||
simp_to_raw using Raw₀.get?_insert
|
||||
|
||||
@[simp]
|
||||
theorem get?_insert_self [LawfulBEq α] {k : α} {v : β k} : (m.insert k v).get? k = some v := by
|
||||
theorem get?_insert_self [LawfulBEq α] (h : m.WF) {k : α} {v : β k} :
|
||||
(m.insert k v).get? k = some v := by
|
||||
simp_to_raw using Raw₀.get?_insert_self
|
||||
|
||||
theorem contains_eq_isSome_get? [LawfulBEq α] {a : α} : m.contains a = (m.get? a).isSome := by
|
||||
theorem contains_eq_isSome_get? [LawfulBEq α] (h : m.WF) {a : α} :
|
||||
m.contains a = (m.get? a).isSome := by
|
||||
simp_to_raw using Raw₀.contains_eq_isSome_get?
|
||||
|
||||
theorem get?_eq_none_of_contains_eq_false [LawfulBEq α] {a : α} :
|
||||
theorem get?_eq_none_of_contains_eq_false [LawfulBEq α] (h : m.WF) {a : α} :
|
||||
m.contains a = false → m.get? a = none := by
|
||||
simp_to_raw using Raw₀.get?_eq_none
|
||||
|
||||
theorem get?_eq_none [LawfulBEq α] {a : α} : ¬a ∈ m → m.get? a = none := by
|
||||
theorem get?_eq_none [LawfulBEq α] (h : m.WF) {a : α} : ¬a ∈ m → m.get? a = none := by
|
||||
simpa [mem_iff_contains] using get?_eq_none_of_contains_eq_false h
|
||||
|
||||
theorem get?_erase [LawfulBEq α] {k a : α} :
|
||||
theorem get?_erase [LawfulBEq α] (h : m.WF) {k a : α} :
|
||||
(m.erase k).get? a = if k == a then none else m.get? a := by
|
||||
simp_to_raw using Raw₀.get?_erase
|
||||
|
||||
@[simp]
|
||||
theorem get?_erase_self [LawfulBEq α] {k : α} : (m.erase k).get? k = none := by
|
||||
theorem get?_erase_self [LawfulBEq α] (h : m.WF) {k : α} : (m.erase k).get? k = none := by
|
||||
simp_to_raw using Raw₀.get?_erase_self
|
||||
|
||||
namespace Const
|
||||
|
|
@ -297,48 +306,50 @@ theorem get?_empty {a : α} {c} : get? (empty c : Raw α (fun _ => β)) a = none
|
|||
theorem get?_emptyc {a : α} : get? (∅ : Raw α (fun _ => β)) a = none :=
|
||||
get?_empty
|
||||
|
||||
theorem get?_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} :
|
||||
theorem get?_of_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
|
||||
m.isEmpty = true → get? m a = none := by
|
||||
simp_to_raw using Raw₀.Const.get?_of_isEmpty ⟨m, _⟩
|
||||
|
||||
theorem get?_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
|
||||
theorem get?_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {v : β} :
|
||||
get? (m.insert k v) a = if k == a then some v else get? m a := by
|
||||
simp_to_raw using Raw₀.Const.get?_insert
|
||||
|
||||
@[simp]
|
||||
theorem get?_insert_self [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
|
||||
theorem get?_insert_self [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β} :
|
||||
get? (m.insert k v) k = some v := by
|
||||
simp_to_raw using Raw₀.Const.get?_insert_self
|
||||
|
||||
theorem contains_eq_isSome_get? [EquivBEq α] [LawfulHashable α] {a : α} :
|
||||
theorem contains_eq_isSome_get? [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
|
||||
m.contains a = (get? m a).isSome := by
|
||||
simp_to_raw using Raw₀.Const.contains_eq_isSome_get?
|
||||
|
||||
theorem get?_eq_none_of_contains_eq_false [EquivBEq α] [LawfulHashable α] {a : α} :
|
||||
theorem get?_eq_none_of_contains_eq_false [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
|
||||
m.contains a = false → get? m a = none := by
|
||||
simp_to_raw using Raw₀.Const.get?_eq_none
|
||||
|
||||
theorem get?_eq_none [EquivBEq α] [LawfulHashable α] {a : α} : ¬a ∈ m → get? m a = none := by
|
||||
simpa [mem_iff_contains] using get?_eq_none_of_contains_eq_false h
|
||||
theorem get?_eq_none [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
|
||||
¬a ∈ m → get? m a = none := by
|
||||
simpa [mem_iff_contains] using get?_eq_none_of_contains_eq_false h
|
||||
|
||||
theorem get?_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
|
||||
theorem get?_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} :
|
||||
Const.get? (m.erase k) a = if k == a then none else get? m a := by
|
||||
simp_to_raw using Raw₀.Const.get?_erase
|
||||
|
||||
@[simp]
|
||||
theorem get?_erase_self [EquivBEq α] [LawfulHashable α] {k : α} : get? (m.erase k) k = none := by
|
||||
theorem get?_erase_self [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
|
||||
get? (m.erase k) k = none := by
|
||||
simp_to_raw using Raw₀.Const.get?_erase_self
|
||||
|
||||
theorem get?_eq_get? [LawfulBEq α] {a : α} : get? m a = m.get? a := by
|
||||
theorem get?_eq_get? [LawfulBEq α] (h : m.WF) {a : α} : get? m a = m.get? a := by
|
||||
simp_to_raw using Raw₀.Const.get?_eq_get?
|
||||
|
||||
theorem get?_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a == b) :
|
||||
theorem get?_congr [EquivBEq α] [LawfulHashable α] (h : m.WF) {a b : α} (hab : a == b) :
|
||||
get? m a = get? m b := by
|
||||
simp_to_raw using Raw₀.Const.get?_congr
|
||||
|
||||
end Const
|
||||
|
||||
theorem get_insert [LawfulBEq α] {k a : α} {v : β k} {h₁} :
|
||||
theorem get_insert [LawfulBEq α] (h : m.WF) {k a : α} {v : β k} {h₁} :
|
||||
(m.insert k v).get a h₁ =
|
||||
if h₂ : k == a then
|
||||
cast (congrArg β (eq_of_beq h₂)) v
|
||||
|
|
@ -347,45 +358,45 @@ theorem get_insert [LawfulBEq α] {k a : α} {v : β k} {h₁} :
|
|||
simp_to_raw using Raw₀.get_insert ⟨m, _⟩
|
||||
|
||||
@[simp]
|
||||
theorem get_insert_self [LawfulBEq α] {k : α} {v : β k} :
|
||||
theorem get_insert_self [LawfulBEq α] (h : m.WF) {k : α} {v : β k} :
|
||||
(m.insert k v).get k (mem_insert_self h) = v := by
|
||||
simp_to_raw using Raw₀.get_insert_self ⟨m, _⟩
|
||||
|
||||
@[simp]
|
||||
theorem get_erase [LawfulBEq α] {k a : α} {h'} :
|
||||
theorem get_erase [LawfulBEq α] (h : m.WF) {k a : α} {h'} :
|
||||
(m.erase a).get k h' = m.get k (mem_of_mem_erase h h') := by
|
||||
simp_to_raw using Raw₀.get_erase ⟨m, _⟩
|
||||
|
||||
theorem get?_eq_some_get [LawfulBEq α] {a : α} {h} : m.get? a = some (m.get a h) := by
|
||||
theorem get?_eq_some_get [LawfulBEq α] (h : m.WF) {a : α} {h} : m.get? a = some (m.get a h) := by
|
||||
simp_to_raw using Raw₀.get?_eq_some_get
|
||||
|
||||
namespace Const
|
||||
|
||||
variable {β : Type v} {m : DHashMap.Raw α (fun _ => β)} (h : m.WF)
|
||||
|
||||
theorem get_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} {h₁} :
|
||||
theorem get_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {v : β} {h₁} :
|
||||
get (m.insert k v) a h₁ =
|
||||
if h₂ : k == a then v else get m a (mem_of_mem_insert h h₁ (Bool.eq_false_iff.2 h₂)) := by
|
||||
simp_to_raw using Raw₀.Const.get_insert ⟨m, _⟩
|
||||
|
||||
@[simp]
|
||||
theorem get_insert_self [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
|
||||
theorem get_insert_self [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β} :
|
||||
get (m.insert k v) k (mem_insert_self h) = v := by
|
||||
simp_to_raw using Raw₀.Const.get_insert_self ⟨m, _⟩
|
||||
|
||||
@[simp]
|
||||
theorem get_erase [EquivBEq α] [LawfulHashable α] {k a : α} {h'} :
|
||||
theorem get_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {h'} :
|
||||
get (m.erase k) a h' = get m a (mem_of_mem_erase h h') := by
|
||||
simp_to_raw using Raw₀.Const.get_erase ⟨m, _⟩
|
||||
|
||||
theorem get?_eq_some_get [EquivBEq α] [LawfulHashable α] {a : α} {h : a ∈ m} :
|
||||
theorem get?_eq_some_get [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} {h : a ∈ m} :
|
||||
get? m a = some (get m a h) := by
|
||||
simp_to_raw using Raw₀.Const.get?_eq_some_get
|
||||
|
||||
theorem get_eq_get [LawfulBEq α] {a : α} {h} : get m a h = m.get a h := by
|
||||
theorem get_eq_get [LawfulBEq α] (h : m.WF) {a : α} {h} : get m a h = m.get a h := by
|
||||
simp_to_raw using Raw₀.Const.get_eq_get
|
||||
|
||||
theorem get_congr [LawfulBEq α] {a b : α} (hab : a == b) {h'} :
|
||||
theorem get_congr [LawfulBEq α] (h : m.WF) {a b : α} (hab : a == b) {h'} :
|
||||
get m a h' = get m b ((mem_congr h hab).1 h') := by
|
||||
simp_to_raw using Raw₀.Const.get_congr
|
||||
|
||||
|
|
@ -401,49 +412,49 @@ theorem get!_emptyc [LawfulBEq α] {a : α} [Inhabited (β a)] :
|
|||
(∅ : Raw α β).get! a = default :=
|
||||
get!_empty
|
||||
|
||||
theorem get!_of_isEmpty [LawfulBEq α] {a : α} [Inhabited (β a)] :
|
||||
theorem get!_of_isEmpty [LawfulBEq α] (h : m.WF) {a : α} [Inhabited (β a)] :
|
||||
m.isEmpty = true → m.get! a = default := by
|
||||
simp_to_raw using Raw₀.get!_of_isEmpty ⟨m, _⟩
|
||||
|
||||
theorem get!_insert [LawfulBEq α] {k a : α} [Inhabited (β a)] {v : β k} : (m.insert k v).get! a =
|
||||
if h : k == a then cast (congrArg β (eq_of_beq h)) v else m.get! a := by
|
||||
theorem get!_insert [LawfulBEq α] (h : m.WF) {k a : α} [Inhabited (β a)] {v : β k} :
|
||||
(m.insert k v).get! a = if h : k == a then cast (congrArg β (eq_of_beq h)) v else m.get! a := by
|
||||
simp_to_raw using Raw₀.get!_insert
|
||||
|
||||
@[simp]
|
||||
theorem get!_insert_self [LawfulBEq α] {k : α} [Inhabited (β k)] {v : β k} :
|
||||
theorem get!_insert_self [LawfulBEq α] (h : m.WF) {k : α} [Inhabited (β k)] {v : β k} :
|
||||
(m.insert k v).get! k = v := by
|
||||
simp_to_raw using Raw₀.get!_insert_self
|
||||
|
||||
theorem get!_eq_default_of_contains_eq_false [LawfulBEq α] {a : α} [Inhabited (β a)] :
|
||||
theorem get!_eq_default_of_contains_eq_false [LawfulBEq α] (h : m.WF) {a : α} [Inhabited (β a)] :
|
||||
m.contains a = false → m.get! a = default := by
|
||||
simp_to_raw using Raw₀.get!_eq_default
|
||||
|
||||
theorem get!_eq_default [LawfulBEq α] {a : α} [Inhabited (β a)] :
|
||||
theorem get!_eq_default [LawfulBEq α] (h : m.WF) {a : α} [Inhabited (β a)] :
|
||||
¬a ∈ m → m.get! a = default := by
|
||||
simpa [mem_iff_contains] using get!_eq_default_of_contains_eq_false h
|
||||
|
||||
theorem get!_erase [LawfulBEq α] {k a : α} [Inhabited (β a)] :
|
||||
theorem get!_erase [LawfulBEq α] (h : m.WF) {k a : α} [Inhabited (β a)] :
|
||||
(m.erase k).get! a = if k == a then default else m.get! a := by
|
||||
simp_to_raw using Raw₀.get!_erase
|
||||
|
||||
@[simp]
|
||||
theorem get!_erase_self [LawfulBEq α] {k : α} [Inhabited (β k)] :
|
||||
theorem get!_erase_self [LawfulBEq α] (h : m.WF) {k : α} [Inhabited (β k)] :
|
||||
(m.erase k).get! k = default := by
|
||||
simp_to_raw using Raw₀.get!_erase_self
|
||||
|
||||
theorem get?_eq_some_get!_of_contains [LawfulBEq α] {a : α} [Inhabited (β a)] :
|
||||
theorem get?_eq_some_get!_of_contains [LawfulBEq α] (h : m.WF) {a : α} [Inhabited (β a)] :
|
||||
m.contains a = true → m.get? a = some (m.get! a) := by
|
||||
simp_to_raw using Raw₀.get?_eq_some_get!
|
||||
|
||||
theorem get?_eq_some_get! [LawfulBEq α] {a : α} [Inhabited (β a)] :
|
||||
theorem get?_eq_some_get! [LawfulBEq α] (h : m.WF) {a : α} [Inhabited (β a)] :
|
||||
a ∈ m → m.get? a = some (m.get! a) := by
|
||||
simpa [mem_iff_contains] using get?_eq_some_get!_of_contains h
|
||||
|
||||
theorem get!_eq_get!_get? [LawfulBEq α] {a : α} [Inhabited (β a)] :
|
||||
theorem get!_eq_get!_get? [LawfulBEq α] (h : m.WF) {a : α} [Inhabited (β a)] :
|
||||
m.get! a = (m.get? a).get! := by
|
||||
simp_to_raw using Raw₀.get!_eq_get!_get?
|
||||
|
||||
theorem get_eq_get! [LawfulBEq α] {a : α} [Inhabited (β a)] {h} :
|
||||
theorem get_eq_get! [LawfulBEq α] (h : m.WF) {a : α} [Inhabited (β a)] {h} :
|
||||
m.get a h = m.get! a := by
|
||||
simp_to_raw using Raw₀.get_eq_get!
|
||||
|
||||
|
|
@ -459,58 +470,59 @@ theorem get!_empty [Inhabited β] {a : α} {c} : get! (empty c : Raw α (fun _ =
|
|||
theorem get!_emptyc [Inhabited β] {a : α} : get! (∅ : Raw α (fun _ => β)) a = default :=
|
||||
get!_empty
|
||||
|
||||
theorem get!_of_isEmpty [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α} :
|
||||
theorem get!_of_isEmpty [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.WF) {a : α} :
|
||||
m.isEmpty = true → get! m a = default := by
|
||||
simp_to_raw using Raw₀.Const.get!_of_isEmpty ⟨m, _⟩
|
||||
|
||||
theorem get!_insert [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} {v : β} :
|
||||
theorem get!_insert [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.WF) {k a : α} {v : β} :
|
||||
get! (m.insert k v) a = if k == a then v else get! m a := by
|
||||
simp_to_raw using Raw₀.Const.get!_insert
|
||||
|
||||
@[simp]
|
||||
theorem get!_insert_self [EquivBEq α] [LawfulHashable α] [Inhabited β] {k : α} {v : β} :
|
||||
theorem get!_insert_self [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.WF) {k : α} {v : β} :
|
||||
get! (m.insert k v) k = v := by
|
||||
simp_to_raw using Raw₀.Const.get!_insert_self
|
||||
|
||||
theorem get!_eq_default_of_contains_eq_false [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α} :
|
||||
theorem get!_eq_default_of_contains_eq_false [EquivBEq α] [LawfulHashable α] [Inhabited β]
|
||||
(h : m.WF) {a : α} :
|
||||
m.contains a = false → get! m a = default := by
|
||||
simp_to_raw using Raw₀.Const.get!_eq_default
|
||||
|
||||
theorem get!_eq_default [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α} :
|
||||
theorem get!_eq_default [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.WF) {a : α} :
|
||||
¬a ∈ m → get! m a = default := by
|
||||
simpa [mem_iff_contains] using get!_eq_default_of_contains_eq_false h
|
||||
|
||||
theorem get!_erase [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} :
|
||||
theorem get!_erase [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.WF) {k a : α} :
|
||||
get! (m.erase k) a = if k == a then default else get! m a := by
|
||||
simp_to_raw using Raw₀.Const.get!_erase
|
||||
|
||||
@[simp]
|
||||
theorem get!_erase_self [EquivBEq α] [LawfulHashable α] [Inhabited β] {k : α} :
|
||||
theorem get!_erase_self [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.WF) {k : α} :
|
||||
get! (m.erase k) k = default := by
|
||||
simp_to_raw using Raw₀.Const.get!_erase_self
|
||||
|
||||
theorem get?_eq_some_get!_of_contains [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α} :
|
||||
m.contains a = true → get? m a = some (get! m a) := by
|
||||
theorem get?_eq_some_get!_of_contains [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.WF)
|
||||
{a : α} : m.contains a = true → get? m a = some (get! m a) := by
|
||||
simp_to_raw using Raw₀.Const.get?_eq_some_get!
|
||||
|
||||
theorem get?_eq_some_get! [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α} :
|
||||
theorem get?_eq_some_get! [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.WF) {a : α} :
|
||||
a ∈ m → get? m a = some (get! m a) := by
|
||||
simpa [mem_iff_contains] using get?_eq_some_get!_of_contains h
|
||||
|
||||
theorem get!_eq_get!_get? [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α} :
|
||||
theorem get!_eq_get!_get? [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.WF) {a : α} :
|
||||
get! m a = (get? m a).get! := by
|
||||
simp_to_raw using Raw₀.Const.get!_eq_get!_get?
|
||||
|
||||
theorem get_eq_get! [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α} {h} :
|
||||
theorem get_eq_get! [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.WF) {a : α} {h} :
|
||||
get m a h = get! m a := by
|
||||
simp_to_raw using Raw₀.Const.get_eq_get!
|
||||
|
||||
theorem get!_eq_get! [LawfulBEq α] [Inhabited β] {a : α} :
|
||||
theorem get!_eq_get! [LawfulBEq α] [Inhabited β] (h : m.WF) {a : α} :
|
||||
get! m a = m.get! a := by
|
||||
simp_to_raw using Raw₀.Const.get!_eq_get!
|
||||
|
||||
theorem get!_congr [EquivBEq α] [LawfulHashable α] [Inhabited β] {a b : α} (hab : a == b) :
|
||||
get! m a = get! m b := by
|
||||
theorem get!_congr [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.WF) {a b : α}
|
||||
(hab : a == b) : get! m a = get! m b := by
|
||||
simp_to_raw using Raw₀.Const.get!_congr
|
||||
|
||||
end Const
|
||||
|
|
@ -525,54 +537,54 @@ theorem getD_emptyc [LawfulBEq α] {a : α} {fallback : β a} :
|
|||
(∅ : Raw α β).getD a fallback = fallback :=
|
||||
getD_empty
|
||||
|
||||
theorem getD_of_isEmpty [LawfulBEq α] {a : α} {fallback : β a} :
|
||||
theorem getD_of_isEmpty [LawfulBEq α] (h : m.WF) {a : α} {fallback : β a} :
|
||||
m.isEmpty = true → m.getD a fallback = fallback := by
|
||||
simp_to_raw using Raw₀.getD_of_isEmpty ⟨m, _⟩
|
||||
|
||||
theorem getD_insert [LawfulBEq α] {k a : α} {fallback : β a} {v : β k} :
|
||||
theorem getD_insert [LawfulBEq α] (h : m.WF) {k a : α} {fallback : β a} {v : β k} :
|
||||
(m.insert k v).getD a fallback =
|
||||
if h : k == a then cast (congrArg β (eq_of_beq h)) v else m.getD a fallback := by
|
||||
simp_to_raw using Raw₀.getD_insert
|
||||
|
||||
@[simp]
|
||||
theorem getD_insert_self [LawfulBEq α] {a : α} {fallback b : β a} :
|
||||
theorem getD_insert_self [LawfulBEq α] (h : m.WF) {a : α} {fallback b : β a} :
|
||||
(m.insert a b).getD a fallback = b := by
|
||||
simp_to_raw using Raw₀.getD_insert_self
|
||||
|
||||
theorem getD_eq_fallback_of_contains_eq_false [LawfulBEq α] {a : α} {fallback : β a} :
|
||||
theorem getD_eq_fallback_of_contains_eq_false [LawfulBEq α] (h : m.WF) {a : α} {fallback : β a} :
|
||||
m.contains a = false → m.getD a fallback = fallback := by
|
||||
simp_to_raw using Raw₀.getD_eq_fallback
|
||||
|
||||
theorem getD_eq_fallback [LawfulBEq α] {a : α} {fallback : β a} :
|
||||
theorem getD_eq_fallback [LawfulBEq α] (h : m.WF) {a : α} {fallback : β a} :
|
||||
¬a ∈ m → m.getD a fallback = fallback := by
|
||||
simpa [mem_iff_contains] using getD_eq_fallback_of_contains_eq_false h
|
||||
|
||||
theorem getD_erase [LawfulBEq α] {k a : α} {fallback : β a} :
|
||||
theorem getD_erase [LawfulBEq α] (h : m.WF) {k a : α} {fallback : β a} :
|
||||
(m.erase k).getD a fallback = if k == a then fallback else m.getD a fallback := by
|
||||
simp_to_raw using Raw₀.getD_erase
|
||||
|
||||
@[simp]
|
||||
theorem getD_erase_self [LawfulBEq α] {k : α} {fallback : β k} :
|
||||
theorem getD_erase_self [LawfulBEq α] (h : m.WF) {k : α} {fallback : β k} :
|
||||
(m.erase k).getD k fallback = fallback := by
|
||||
simp_to_raw using Raw₀.getD_erase_self
|
||||
|
||||
theorem get?_eq_some_getD_of_contains [LawfulBEq α] {a : α} {fallback : β a} :
|
||||
theorem get?_eq_some_getD_of_contains [LawfulBEq α] (h : m.WF) {a : α} {fallback : β a} :
|
||||
m.contains a = true → m.get? a = some (m.getD a fallback) := by
|
||||
simp_to_raw using Raw₀.get?_eq_some_getD
|
||||
|
||||
theorem get?_eq_some_getD [LawfulBEq α] {a : α} {fallback : β a} :
|
||||
theorem get?_eq_some_getD [LawfulBEq α] (h : m.WF) {a : α} {fallback : β a} :
|
||||
a ∈ m → m.get? a = some (m.getD a fallback) := by
|
||||
simpa [mem_iff_contains] using get?_eq_some_getD_of_contains h
|
||||
|
||||
theorem getD_eq_getD_get? [LawfulBEq α] {a : α} {fallback : β a} :
|
||||
theorem getD_eq_getD_get? [LawfulBEq α] (h : m.WF) {a : α} {fallback : β a} :
|
||||
m.getD a fallback = (m.get? a).getD fallback := by
|
||||
simp_to_raw using Raw₀.getD_eq_getD_get?
|
||||
|
||||
theorem get_eq_getD [LawfulBEq α] {a : α} {fallback : β a} {h} :
|
||||
theorem get_eq_getD [LawfulBEq α] (h : m.WF) {a : α} {fallback : β a} {h} :
|
||||
m.get a h = m.getD a fallback := by
|
||||
simp_to_raw using Raw₀.get_eq_getD
|
||||
|
||||
theorem get!_eq_getD_default [LawfulBEq α] {a : α} [Inhabited (β a)] :
|
||||
theorem get!_eq_getD_default [LawfulBEq α] (h : m.WF) {a : α} [Inhabited (β a)] :
|
||||
m.get! a = m.getD a default := by
|
||||
simp_to_raw using Raw₀.get!_eq_getD_default
|
||||
|
||||
|
|
@ -589,143 +601,144 @@ theorem getD_empty {a : α} {fallback : β} {c} :
|
|||
theorem getD_emptyc {a : α} {fallback : β} : getD (∅ : Raw α (fun _ => β)) a fallback = fallback :=
|
||||
getD_empty
|
||||
|
||||
theorem getD_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} {fallback : β} :
|
||||
theorem getD_of_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} {fallback : β} :
|
||||
m.isEmpty = true → getD m a fallback = fallback := by
|
||||
simp_to_raw using Raw₀.Const.getD_of_isEmpty ⟨m, _⟩
|
||||
|
||||
theorem getD_insert [EquivBEq α] [LawfulHashable α] {k a : α} {fallback v : β} :
|
||||
theorem getD_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {fallback v : β} :
|
||||
getD (m.insert k v) a fallback = if k == a then v else getD m a fallback := by
|
||||
simp_to_raw using Raw₀.Const.getD_insert
|
||||
|
||||
@[simp]
|
||||
theorem getD_insert_self [EquivBEq α] [LawfulHashable α] {k : α} {fallback v : β} :
|
||||
theorem getD_insert_self [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {fallback v : β} :
|
||||
getD (m.insert k v) k fallback = v := by
|
||||
simp_to_raw using Raw₀.Const.getD_insert_self
|
||||
|
||||
theorem getD_eq_fallback_of_contains_eq_false [EquivBEq α] [LawfulHashable α] {a : α}
|
||||
theorem getD_eq_fallback_of_contains_eq_false [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α}
|
||||
{fallback : β} : m.contains a = false → getD m a fallback = fallback := by
|
||||
simp_to_raw using Raw₀.Const.getD_eq_fallback
|
||||
|
||||
theorem getD_eq_fallback [EquivBEq α] [LawfulHashable α] {a : α} {fallback : β} :
|
||||
theorem getD_eq_fallback [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} {fallback : β} :
|
||||
¬a ∈ m → getD m a fallback = fallback := by
|
||||
simpa [mem_iff_contains] using getD_eq_fallback_of_contains_eq_false h
|
||||
|
||||
theorem getD_erase [EquivBEq α] [LawfulHashable α] {k a : α} {fallback : β} :
|
||||
theorem getD_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {fallback : β} :
|
||||
getD (m.erase k) a fallback = if k == a then fallback else getD m a fallback := by
|
||||
simp_to_raw using Raw₀.Const.getD_erase
|
||||
|
||||
@[simp]
|
||||
theorem getD_erase_self [EquivBEq α] [LawfulHashable α] {k : α} {fallback : β} :
|
||||
theorem getD_erase_self [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {fallback : β} :
|
||||
getD (m.erase k) k fallback = fallback := by
|
||||
simp_to_raw using Raw₀.Const.getD_erase_self
|
||||
|
||||
theorem get?_eq_some_getD_of_contains [EquivBEq α] [LawfulHashable α] {a : α} {fallback : β} :
|
||||
m.contains a = true → get? m a = some (getD m a fallback) := by
|
||||
theorem get?_eq_some_getD_of_contains [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α}
|
||||
{fallback : β} : m.contains a = true → get? m a = some (getD m a fallback) := by
|
||||
simp_to_raw using Raw₀.Const.get?_eq_some_getD
|
||||
|
||||
theorem get?_eq_some_getD [EquivBEq α] [LawfulHashable α] {a : α} {fallback : β} :
|
||||
theorem get?_eq_some_getD [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} {fallback : β} :
|
||||
a ∈ m → get? m a = some (getD m a fallback) := by
|
||||
simpa [mem_iff_contains] using get?_eq_some_getD_of_contains h
|
||||
|
||||
theorem getD_eq_getD_get? [EquivBEq α] [LawfulHashable α] {a : α} {fallback : β} :
|
||||
theorem getD_eq_getD_get? [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} {fallback : β} :
|
||||
getD m a fallback = (get? m a).getD fallback := by
|
||||
simp_to_raw using Raw₀.Const.getD_eq_getD_get?
|
||||
|
||||
theorem get_eq_getD [EquivBEq α] [LawfulHashable α] {a : α} {fallback : β} {h} :
|
||||
theorem get_eq_getD [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} {fallback : β} {h} :
|
||||
get m a h = getD m a fallback := by
|
||||
simp_to_raw using Raw₀.Const.get_eq_getD
|
||||
|
||||
theorem get!_eq_getD_default [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α} :
|
||||
theorem get!_eq_getD_default [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.WF) {a : α} :
|
||||
get! m a = getD m a default := by
|
||||
simp_to_raw using Raw₀.Const.get!_eq_getD_default
|
||||
|
||||
theorem getD_eq_getD [LawfulBEq α] {a : α} {fallback : β} :
|
||||
theorem getD_eq_getD [LawfulBEq α] (h : m.WF) {a : α} {fallback : β} :
|
||||
getD m a fallback = m.getD a fallback := by
|
||||
simp_to_raw using Raw₀.Const.getD_eq_getD
|
||||
|
||||
theorem getD_congr [EquivBEq α] [LawfulHashable α] {a b : α} {fallback : β} (hab : a == b) :
|
||||
getD m a fallback = getD m b fallback := by
|
||||
theorem getD_congr [EquivBEq α] [LawfulHashable α] (h : m.WF) {a b : α} {fallback : β}
|
||||
(hab : a == b) : getD m a fallback = getD m b fallback := by
|
||||
simp_to_raw using Raw₀.Const.getD_congr
|
||||
|
||||
end Const
|
||||
|
||||
@[simp]
|
||||
theorem isEmpty_insertIfNew [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
|
||||
theorem isEmpty_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β k} :
|
||||
(m.insertIfNew k v).isEmpty = false := by
|
||||
simp_to_raw using Raw₀.isEmpty_insertIfNew
|
||||
|
||||
@[simp]
|
||||
theorem contains_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
|
||||
theorem contains_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {v : β k} :
|
||||
(m.insertIfNew k v).contains a = (k == a || m.contains a) := by
|
||||
simp_to_raw using Raw₀.contains_insertIfNew
|
||||
|
||||
@[simp]
|
||||
theorem mem_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
|
||||
theorem mem_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {v : β k} :
|
||||
a ∈ m.insertIfNew k v ↔ k == a ∨ a ∈ m := by
|
||||
simp [mem_iff_contains, contains_insertIfNew h]
|
||||
|
||||
theorem contains_insertIfNew_self [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
|
||||
theorem contains_insertIfNew_self [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β k} :
|
||||
(m.insertIfNew k v).contains k := by
|
||||
simp_to_raw using Raw₀.contains_insertIfNew_self
|
||||
|
||||
theorem mem_insertIfNew_self [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
|
||||
theorem mem_insertIfNew_self [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β k} :
|
||||
k ∈ m.insertIfNew k v := by
|
||||
simpa [mem_iff_contains, -contains_insertIfNew] using contains_insertIfNew_self h
|
||||
|
||||
theorem contains_of_contains_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
|
||||
(m.insertIfNew k v).contains a → (k == a) = false → m.contains a := by
|
||||
theorem contains_of_contains_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α}
|
||||
{v : β k} : (m.insertIfNew k v).contains a → (k == a) = false → m.contains a := by
|
||||
simp_to_raw using Raw₀.contains_of_contains_insertIfNew
|
||||
|
||||
theorem mem_of_mem_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
|
||||
theorem mem_of_mem_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {v : β k} :
|
||||
a ∈ m.insertIfNew k v → (k == a) = false → a ∈ m := by
|
||||
simpa [mem_iff_contains, -contains_insertIfNew] using contains_of_contains_insertIfNew h
|
||||
|
||||
/-- This is a restatement of `contains_insertIfNew` that is written to exactly match the proof
|
||||
obligation in the statement of `get_insertIfNew`. -/
|
||||
theorem contains_of_contains_insertIfNew' [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
|
||||
theorem contains_of_contains_insertIfNew' [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α}
|
||||
{v : β k} :
|
||||
(m.insertIfNew k v).contains a → ¬((k == a) ∧ m.contains k = false) → m.contains a := by
|
||||
simp_to_raw using Raw₀.contains_of_contains_insertIfNew'
|
||||
|
||||
/-- This is a restatement of `mem_insertIfNew` that is written to exactly match the proof obligation
|
||||
in the statement of `get_insertIfNew`. -/
|
||||
theorem mem_of_mem_insertIfNew' [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
|
||||
theorem mem_of_mem_insertIfNew' [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {v : β k} :
|
||||
a ∈ m.insertIfNew k v → ¬((k == a) ∧ ¬k ∈ m) → a ∈ m := by
|
||||
simpa [mem_iff_contains] using contains_of_contains_insertIfNew' h
|
||||
|
||||
theorem size_insertIfNew [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
|
||||
theorem size_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β k} :
|
||||
(m.insertIfNew k v).size = if k ∈ m then m.size else m.size + 1 := by
|
||||
simp only [mem_iff_contains]
|
||||
simp_to_raw using Raw₀.size_insertIfNew
|
||||
|
||||
theorem size_le_size_insertIfNew [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
|
||||
theorem size_le_size_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β k} :
|
||||
m.size ≤ (m.insertIfNew k v).size := by
|
||||
simp_to_raw using Raw₀.size_le_size_insertIfNew ⟨m, _⟩
|
||||
|
||||
theorem size_insertIfNew_le [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
|
||||
theorem size_insertIfNew_le [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β k} :
|
||||
(m.insertIfNew k v).size ≤ m.size + 1 := by
|
||||
simp_to_raw using Raw₀.size_insertIfNew_le
|
||||
|
||||
theorem get?_insertIfNew [LawfulBEq α] {k a : α} {v : β k} :
|
||||
theorem get?_insertIfNew [LawfulBEq α] (h : m.WF) {k a : α} {v : β k} :
|
||||
(m.insertIfNew k v).get? a =
|
||||
if h : k == a ∧ ¬k ∈ m then some (cast (congrArg β (eq_of_beq h.1)) v)
|
||||
else m.get? a := by
|
||||
simp only [mem_iff_contains, Bool.not_eq_true]
|
||||
simp_to_raw using Raw₀.get?_insertIfNew ⟨m, _⟩
|
||||
|
||||
theorem get_insertIfNew [LawfulBEq α] {k a : α} {v : β k} {h₁} :
|
||||
theorem get_insertIfNew [LawfulBEq α] (h : m.WF) {k a : α} {v : β k} {h₁} :
|
||||
(m.insertIfNew k v).get a h₁ =
|
||||
if h₂ : k == a ∧ ¬k ∈ m then cast (congrArg β (eq_of_beq h₂.1)) v
|
||||
else m.get a (mem_of_mem_insertIfNew' h h₁ h₂) := by
|
||||
simp only [mem_iff_contains, Bool.not_eq_true]
|
||||
simp_to_raw using Raw₀.get_insertIfNew ⟨m, _⟩
|
||||
|
||||
theorem get!_insertIfNew [LawfulBEq α] {k a : α} [Inhabited (β a)] {v : β k} :
|
||||
theorem get!_insertIfNew [LawfulBEq α] (h : m.WF) {k a : α} [Inhabited (β a)] {v : β k} :
|
||||
(m.insertIfNew k v).get! a =
|
||||
if h : k == a ∧ ¬k ∈ m then cast (congrArg β (eq_of_beq h.1)) v else m.get! a := by
|
||||
simp only [mem_iff_contains, Bool.not_eq_true]
|
||||
simp_to_raw using Raw₀.get!_insertIfNew ⟨m, _⟩
|
||||
|
||||
theorem getD_insertIfNew [LawfulBEq α] {k a : α} {fallback : β a} {v : β k} :
|
||||
theorem getD_insertIfNew [LawfulBEq α] (h : m.WF) {k a : α} {fallback : β a} {v : β k} :
|
||||
(m.insertIfNew k v).getD a fallback =
|
||||
if h : k == a ∧ ¬k ∈ m then cast (congrArg β (eq_of_beq h.1)) v
|
||||
else m.getD a fallback := by
|
||||
|
|
@ -736,24 +749,24 @@ namespace Const
|
|||
|
||||
variable {β : Type v} {m : DHashMap.Raw α (fun _ => β)} (h : m.WF)
|
||||
|
||||
theorem get?_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
|
||||
theorem get?_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {v : β} :
|
||||
get? (m.insertIfNew k v) a = if k == a ∧ ¬k ∈ m then some v else get? m a := by
|
||||
simp only [mem_iff_contains, Bool.not_eq_true]
|
||||
simp_to_raw using Raw₀.Const.get?_insertIfNew
|
||||
|
||||
theorem get_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} {h₁} :
|
||||
theorem get_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {v : β} {h₁} :
|
||||
get (m.insertIfNew k v) a h₁ =
|
||||
if h₂ : k == a ∧ ¬k ∈ m then v
|
||||
else get m a (mem_of_mem_insertIfNew' h h₁ h₂) := by
|
||||
simp only [mem_iff_contains, Bool.not_eq_true]
|
||||
simp_to_raw using Raw₀.Const.get_insertIfNew ⟨m, _⟩
|
||||
|
||||
theorem get!_insertIfNew [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} {v : β} :
|
||||
get! (m.insertIfNew k v) a = if k == a ∧ ¬k ∈ m then v else get! m a := by
|
||||
theorem get!_insertIfNew [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.WF) {k a : α}
|
||||
{v : β} : get! (m.insertIfNew k v) a = if k == a ∧ ¬k ∈ m then v else get! m a := by
|
||||
simp only [mem_iff_contains, Bool.not_eq_true]
|
||||
simp_to_raw using Raw₀.Const.get!_insertIfNew
|
||||
|
||||
theorem getD_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {fallback v : β} :
|
||||
theorem getD_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {fallback v : β} :
|
||||
getD (m.insertIfNew k v) a fallback =
|
||||
if k == a ∧ ¬k ∈ m then v else getD m a fallback := by
|
||||
simp only [mem_iff_contains, Bool.not_eq_true]
|
||||
|
|
@ -762,12 +775,12 @@ theorem getD_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {fallback
|
|||
end Const
|
||||
|
||||
@[simp]
|
||||
theorem getThenInsertIfNew?_fst [LawfulBEq α] {k : α} {v : β k} :
|
||||
theorem getThenInsertIfNew?_fst [LawfulBEq α] (h : m.WF) {k : α} {v : β k} :
|
||||
(m.getThenInsertIfNew? k v).1 = m.get? k := by
|
||||
simp_to_raw using Raw₀.getThenInsertIfNew?_fst
|
||||
|
||||
@[simp]
|
||||
theorem getThenInsertIfNew?_snd [LawfulBEq α] {k : α} {v : β k} :
|
||||
theorem getThenInsertIfNew?_snd [LawfulBEq α] (h : m.WF) {k : α} {v : β k} :
|
||||
(m.getThenInsertIfNew? k v).2 = m.insertIfNew k v := by
|
||||
simp_to_raw using congrArg Subtype.val (Raw₀.getThenInsertIfNew?_snd _)
|
||||
|
||||
|
|
@ -776,11 +789,12 @@ namespace Const
|
|||
variable {β : Type v} {m : DHashMap.Raw α (fun _ => β)} (h : m.WF)
|
||||
|
||||
@[simp]
|
||||
theorem getThenInsertIfNew?_fst {k : α} {v : β} : (getThenInsertIfNew? m k v).1 = get? m k := by
|
||||
theorem getThenInsertIfNew?_fst (h : m.WF) {k : α} {v : β} :
|
||||
(getThenInsertIfNew? m k v).1 = get? m k := by
|
||||
simp_to_raw using Raw₀.Const.getThenInsertIfNew?_fst
|
||||
|
||||
@[simp]
|
||||
theorem getThenInsertIfNew?_snd {k : α} {v : β} :
|
||||
theorem getThenInsertIfNew?_snd (h : m.WF) {k : α} {v : β} :
|
||||
(getThenInsertIfNew? m k v).2 = m.insertIfNew k v := by
|
||||
simp_to_raw using congrArg Subtype.val (Raw₀.Const.getThenInsertIfNew?_snd _)
|
||||
|
||||
|
|
|
|||
|
|
@ -20,18 +20,30 @@ set_option autoImplicit false
|
|||
|
||||
universe u v
|
||||
|
||||
variable {α : Type u} {β : Type v} [BEq α] [Hashable α]
|
||||
variable {α : Type u} {β : Type v}
|
||||
|
||||
namespace Std.HashMap
|
||||
|
||||
namespace Raw
|
||||
|
||||
variable {m : Raw α β} (h : m.WF)
|
||||
set_option deprecated.oldSectionVars true
|
||||
variable {m : Raw α β}
|
||||
|
||||
@[simp]
|
||||
theorem size_empty {c} : (empty c : Raw α β).size = 0 :=
|
||||
DHashMap.Raw.size_empty
|
||||
|
||||
@[simp]
|
||||
theorem size_emptyc : (∅ : Raw α β).size = 0 :=
|
||||
DHashMap.Raw.size_emptyc
|
||||
|
||||
theorem isEmpty_eq_size_eq_zero : m.isEmpty = (m.size == 0) :=
|
||||
DHashMap.Raw.isEmpty_eq_size_eq_zero
|
||||
|
||||
private theorem ext {m m' : Raw α β} : m.inner = m'.inner → m = m' := by
|
||||
cases m; cases m'; rintro rfl; rfl
|
||||
|
||||
variable [BEq α] [Hashable α]
|
||||
|
||||
@[simp]
|
||||
theorem isEmpty_empty {c} : (empty c : Raw α β).isEmpty :=
|
||||
DHashMap.Raw.isEmpty_empty
|
||||
|
|
@ -41,18 +53,19 @@ theorem isEmpty_emptyc : (∅ : Raw α β).isEmpty :=
|
|||
DHashMap.Raw.isEmpty_emptyc
|
||||
|
||||
@[simp]
|
||||
theorem isEmpty_insert [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
|
||||
theorem isEmpty_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β} :
|
||||
(m.insert k v).isEmpty = false :=
|
||||
DHashMap.Raw.isEmpty_insert h.out
|
||||
|
||||
theorem mem_iff_contains {a : α} : a ∈ m ↔ m.contains a :=
|
||||
DHashMap.Raw.mem_iff_contains
|
||||
|
||||
theorem contains_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a == b) :
|
||||
theorem contains_congr [EquivBEq α] [LawfulHashable α] (h : m.WF) {a b : α} (hab : a == b) :
|
||||
m.contains a = m.contains b :=
|
||||
DHashMap.Raw.contains_congr h.out hab
|
||||
|
||||
theorem mem_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a == b) : a ∈ m ↔ b ∈ m :=
|
||||
theorem mem_congr [EquivBEq α] [LawfulHashable α] (h : m.WF) {a b : α} (hab : a == b) :
|
||||
a ∈ m ↔ b ∈ m :=
|
||||
DHashMap.Raw.mem_congr h.out hab
|
||||
|
||||
@[simp] theorem contains_empty {a : α} {c} : (empty c : Raw α β).contains a = false :=
|
||||
|
|
@ -71,77 +84,67 @@ theorem mem_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a == b) :
|
|||
@[simp] theorem not_mem_emptyc {a : α} : ¬a ∈ (∅ : Raw α β) :=
|
||||
DHashMap.Raw.not_mem_emptyc
|
||||
|
||||
theorem contains_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} :
|
||||
theorem contains_of_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
|
||||
m.isEmpty → m.contains a = false :=
|
||||
DHashMap.Raw.contains_of_isEmpty h.out
|
||||
|
||||
theorem not_mem_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} :
|
||||
theorem not_mem_of_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
|
||||
m.isEmpty → ¬a ∈ m :=
|
||||
DHashMap.Raw.not_mem_of_isEmpty h.out
|
||||
|
||||
theorem isEmpty_eq_false_iff_exists_contains_eq_true [EquivBEq α] [LawfulHashable α] :
|
||||
theorem isEmpty_eq_false_iff_exists_contains_eq_true [EquivBEq α] [LawfulHashable α] (h : m.WF) :
|
||||
m.isEmpty = false ↔ ∃ a, m.contains a = true :=
|
||||
DHashMap.Raw.isEmpty_eq_false_iff_exists_contains_eq_true h.out
|
||||
|
||||
theorem isEmpty_eq_false_iff_exists_mem [EquivBEq α] [LawfulHashable α] :
|
||||
theorem isEmpty_eq_false_iff_exists_mem [EquivBEq α] [LawfulHashable α] (h : m.WF) :
|
||||
m.isEmpty = false ↔ ∃ a, a ∈ m :=
|
||||
DHashMap.Raw.isEmpty_eq_false_iff_exists_mem h.out
|
||||
|
||||
theorem isEmpty_iff_forall_contains [EquivBEq α] [LawfulHashable α] :
|
||||
theorem isEmpty_iff_forall_contains [EquivBEq α] [LawfulHashable α] (h : m.WF) :
|
||||
m.isEmpty = true ↔ ∀ a, m.contains a = false :=
|
||||
DHashMap.Raw.isEmpty_iff_forall_contains h.out
|
||||
|
||||
theorem isEmpty_iff_forall_not_mem [EquivBEq α] [LawfulHashable α] :
|
||||
theorem isEmpty_iff_forall_not_mem [EquivBEq α] [LawfulHashable α] (h : m.WF) :
|
||||
m.isEmpty = true ↔ ∀ a, ¬a ∈ m :=
|
||||
DHashMap.Raw.isEmpty_iff_forall_not_mem h.out
|
||||
|
||||
@[simp]
|
||||
theorem contains_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
|
||||
theorem contains_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {v : β} :
|
||||
(m.insert k v).contains a = (k == a || m.contains a) :=
|
||||
DHashMap.Raw.contains_insert h.out
|
||||
|
||||
@[simp]
|
||||
theorem mem_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
|
||||
theorem mem_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {v : β} :
|
||||
a ∈ m.insert k v ↔ k == a ∨ a ∈ m :=
|
||||
DHashMap.Raw.mem_insert h.out
|
||||
|
||||
theorem contains_of_contains_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
|
||||
theorem contains_of_contains_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {v : β} :
|
||||
(m.insert k v).contains a → (k == a) = false → m.contains a :=
|
||||
DHashMap.Raw.contains_of_contains_insert h.out
|
||||
|
||||
theorem mem_of_mem_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
|
||||
theorem mem_of_mem_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {v : β} :
|
||||
a ∈ m.insert k v → (k == a) = false → a ∈ m :=
|
||||
DHashMap.Raw.mem_of_mem_insert h.out
|
||||
|
||||
@[simp]
|
||||
theorem contains_insert_self [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
|
||||
theorem contains_insert_self [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β} :
|
||||
(m.insert k v).contains k :=
|
||||
DHashMap.Raw.contains_insert_self h.out
|
||||
|
||||
@[simp]
|
||||
theorem mem_insert_self [EquivBEq α] [LawfulHashable α] {k : α} {v : β} : k ∈ m.insert k v :=
|
||||
theorem mem_insert_self [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β} :
|
||||
k ∈ m.insert k v :=
|
||||
DHashMap.Raw.mem_insert_self h.out
|
||||
|
||||
@[simp]
|
||||
theorem size_empty {c} : (empty c : Raw α β).size = 0 :=
|
||||
DHashMap.Raw.size_empty
|
||||
|
||||
@[simp]
|
||||
theorem size_emptyc : (∅ : Raw α β).size = 0 :=
|
||||
DHashMap.Raw.size_emptyc
|
||||
|
||||
theorem isEmpty_eq_size_eq_zero : m.isEmpty = (m.size == 0) :=
|
||||
DHashMap.Raw.isEmpty_eq_size_eq_zero
|
||||
|
||||
theorem size_insert [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
|
||||
theorem size_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β} :
|
||||
(m.insert k v).size = if k ∈ m then m.size else m.size + 1 :=
|
||||
DHashMap.Raw.size_insert h.out
|
||||
|
||||
theorem size_le_size_insert [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
|
||||
theorem size_le_size_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β} :
|
||||
m.size ≤ (m.insert k v).size :=
|
||||
DHashMap.Raw.size_le_size_insert h.out
|
||||
|
||||
theorem size_insert_le [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
|
||||
theorem size_insert_le [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β} :
|
||||
(m.insert k v).size ≤ m.size + 1 :=
|
||||
DHashMap.Raw.size_insert_le h.out
|
||||
|
||||
|
|
@ -154,53 +157,57 @@ theorem erase_emptyc {k : α} : (∅ : Raw α β).erase k = ∅ :=
|
|||
ext DHashMap.Raw.erase_emptyc
|
||||
|
||||
@[simp]
|
||||
theorem isEmpty_erase [EquivBEq α] [LawfulHashable α] {k : α} :
|
||||
theorem isEmpty_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
|
||||
(m.erase k).isEmpty = (m.isEmpty || (m.size == 1 && m.contains k)) :=
|
||||
DHashMap.Raw.isEmpty_erase h.out
|
||||
|
||||
@[simp]
|
||||
theorem contains_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
|
||||
theorem contains_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} :
|
||||
(m.erase k).contains a = (!(k == a) && m.contains a) :=
|
||||
DHashMap.Raw.contains_erase h.out
|
||||
|
||||
@[simp]
|
||||
theorem mem_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
|
||||
theorem mem_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} :
|
||||
a ∈ m.erase k ↔ (k == a) = false ∧ a ∈ m :=
|
||||
DHashMap.Raw.mem_erase h.out
|
||||
|
||||
theorem contains_of_contains_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
|
||||
theorem contains_of_contains_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} :
|
||||
(m.erase k).contains a → m.contains a :=
|
||||
DHashMap.Raw.contains_of_contains_erase h.out
|
||||
|
||||
theorem mem_of_mem_erase [EquivBEq α] [LawfulHashable α] {k a : α} : a ∈ m.erase k → a ∈ m :=
|
||||
theorem mem_of_mem_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} :
|
||||
a ∈ m.erase k → a ∈ m :=
|
||||
DHashMap.Raw.mem_of_mem_erase h.out
|
||||
|
||||
theorem size_erase [EquivBEq α] [LawfulHashable α] {k : α} :
|
||||
theorem size_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
|
||||
(m.erase k).size = if k ∈ m then m.size - 1 else m.size :=
|
||||
DHashMap.Raw.size_erase h.out
|
||||
|
||||
theorem size_erase_le [EquivBEq α] [LawfulHashable α] {k : α} : (m.erase k).size ≤ m.size :=
|
||||
theorem size_erase_le [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
|
||||
(m.erase k).size ≤ m.size :=
|
||||
DHashMap.Raw.size_erase_le h.out
|
||||
|
||||
theorem size_le_size_erase [EquivBEq α] [LawfulHashable α] {k : α} :
|
||||
theorem size_le_size_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
|
||||
m.size ≤ (m.erase k).size + 1 :=
|
||||
DHashMap.Raw.size_le_size_erase h.out
|
||||
|
||||
@[simp]
|
||||
theorem containsThenInsert_fst {k : α} {v : β} : (m.containsThenInsert k v).1 = m.contains k :=
|
||||
theorem containsThenInsert_fst (h : m.WF) {k : α} {v : β} :
|
||||
(m.containsThenInsert k v).1 = m.contains k :=
|
||||
DHashMap.Raw.containsThenInsert_fst h.out
|
||||
|
||||
@[simp]
|
||||
theorem containsThenInsert_snd {k : α} {v : β} : (m.containsThenInsert k v).2 = m.insert k v :=
|
||||
theorem containsThenInsert_snd (h : m.WF) {k : α} {v : β} :
|
||||
(m.containsThenInsert k v).2 = m.insert k v :=
|
||||
ext (DHashMap.Raw.containsThenInsert_snd h.out)
|
||||
|
||||
@[simp]
|
||||
theorem containsThenInsertIfNew_fst {k : α} {v : β} :
|
||||
theorem containsThenInsertIfNew_fst (h : m.WF) {k : α} {v : β} :
|
||||
(m.containsThenInsertIfNew k v).1 = m.contains k :=
|
||||
DHashMap.Raw.containsThenInsertIfNew_fst h.out
|
||||
|
||||
@[simp]
|
||||
theorem containsThenInsertIfNew_snd {k : α} {v : β} :
|
||||
theorem containsThenInsertIfNew_snd (h : m.WF) {k : α} {v : β} :
|
||||
(m.containsThenInsertIfNew k v).2 = m.insertIfNew k v :=
|
||||
ext (DHashMap.Raw.containsThenInsertIfNew_snd h.out)
|
||||
|
||||
|
|
@ -212,61 +219,64 @@ theorem getElem?_empty {a : α} {c} : (empty c : Raw α β)[a]? = none :=
|
|||
theorem getElem?_emptyc {a : α} : (∅ : Raw α β)[a]? = none :=
|
||||
DHashMap.Raw.Const.get?_emptyc
|
||||
|
||||
theorem getElem?_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} :
|
||||
theorem getElem?_of_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
|
||||
m.isEmpty = true → m[a]? = none :=
|
||||
DHashMap.Raw.Const.get?_of_isEmpty h.out
|
||||
|
||||
theorem getElem?_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
|
||||
theorem getElem?_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {v : β} :
|
||||
(m.insert k v)[a]? = if k == a then some v else m[a]? :=
|
||||
DHashMap.Raw.Const.get?_insert h.out
|
||||
|
||||
@[simp]
|
||||
theorem getElem?_insert_self [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
|
||||
theorem getElem?_insert_self [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β} :
|
||||
(m.insert k v)[k]? = some v :=
|
||||
DHashMap.Raw.Const.get?_insert_self h.out
|
||||
|
||||
theorem contains_eq_isSome_getElem? [EquivBEq α] [LawfulHashable α] {a : α} :
|
||||
theorem contains_eq_isSome_getElem? [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
|
||||
m.contains a = m[a]?.isSome :=
|
||||
DHashMap.Raw.Const.contains_eq_isSome_get? h.out
|
||||
|
||||
theorem getElem?_eq_none_of_contains_eq_false [EquivBEq α] [LawfulHashable α] {a : α} :
|
||||
theorem getElem?_eq_none_of_contains_eq_false [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
|
||||
m.contains a = false → m[a]? = none :=
|
||||
DHashMap.Raw.Const.get?_eq_none_of_contains_eq_false h.out
|
||||
|
||||
theorem getElem?_eq_none [EquivBEq α] [LawfulHashable α] {a : α} : ¬a ∈ m → m[a]? = none :=
|
||||
theorem getElem?_eq_none [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
|
||||
¬a ∈ m → m[a]? = none :=
|
||||
DHashMap.Raw.Const.get?_eq_none h.out
|
||||
|
||||
theorem getElem?_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
|
||||
theorem getElem?_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} :
|
||||
(m.erase k)[a]? = if k == a then none else m[a]? :=
|
||||
DHashMap.Raw.Const.get?_erase h.out
|
||||
|
||||
@[simp]
|
||||
theorem getElem?_erase_self [EquivBEq α] [LawfulHashable α] {k : α} : (m.erase k)[k]? = none :=
|
||||
theorem getElem?_erase_self [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
|
||||
(m.erase k)[k]? = none :=
|
||||
DHashMap.Raw.Const.get?_erase_self h.out
|
||||
|
||||
theorem getElem?_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a == b) : m[a]? = m[b]? :=
|
||||
theorem getElem?_congr [EquivBEq α] [LawfulHashable α] (h : m.WF) {a b : α} (hab : a == b) :
|
||||
m[a]? = m[b]? :=
|
||||
DHashMap.Raw.Const.get?_congr h.out hab
|
||||
|
||||
theorem getElem_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} {h₁} :
|
||||
theorem getElem_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {v : β} {h₁} :
|
||||
(m.insert k v)[a]'h₁ =
|
||||
if h₂ : k == a then v else m[a]'(mem_of_mem_insert h h₁ (Bool.eq_false_iff.2 h₂)) :=
|
||||
DHashMap.Raw.Const.get_insert (h₁ := h₁) h.out
|
||||
|
||||
@[simp]
|
||||
theorem getElem_insert_self [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
|
||||
theorem getElem_insert_self [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β} :
|
||||
(m.insert k v)[k]'(mem_insert_self h) = v :=
|
||||
DHashMap.Raw.Const.get_insert_self h.out
|
||||
|
||||
@[simp]
|
||||
theorem getElem_erase [EquivBEq α] [LawfulHashable α] {k a : α} {h'} :
|
||||
theorem getElem_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {h'} :
|
||||
(m.erase k)[a]'h' = m[a]'(mem_of_mem_erase h h') :=
|
||||
DHashMap.Raw.Const.get_erase (h' := h') h.out
|
||||
|
||||
theorem getElem?_eq_some_getElem [EquivBEq α] [LawfulHashable α] {a : α} {h' : a ∈ m} :
|
||||
theorem getElem?_eq_some_getElem [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} {h' : a ∈ m} :
|
||||
m[a]? = some (m[a]'h') :=
|
||||
@DHashMap.Raw.Const.get?_eq_some_get _ _ _ _ _ h.out _ _ _ h'
|
||||
@DHashMap.Raw.Const.get?_eq_some_get _ _ _ _ _ _ _ h.out _ h'
|
||||
|
||||
theorem getElem_congr [LawfulBEq α] {a b : α} (hab : a == b) {h'} :
|
||||
theorem getElem_congr [LawfulBEq α] (h : m.WF) {a b : α} (hab : a == b) {h'} :
|
||||
m[a]'h' = m[b]'((mem_congr h hab).1 h') :=
|
||||
DHashMap.Raw.Const.get_congr h.out hab (h' := h')
|
||||
|
||||
|
|
@ -278,54 +288,54 @@ theorem getElem!_empty [Inhabited β] {a : α} {c} : (empty c : Raw α β)[a]! =
|
|||
theorem getElem!_emptyc [Inhabited β] {a : α} : (∅ : Raw α β)[a]! = default :=
|
||||
DHashMap.Raw.Const.get!_emptyc
|
||||
|
||||
theorem getElem!_of_isEmpty [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α} :
|
||||
theorem getElem!_of_isEmpty [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.WF) {a : α} :
|
||||
m.isEmpty = true → m[a]! = default :=
|
||||
DHashMap.Raw.Const.get!_of_isEmpty h.out
|
||||
|
||||
theorem getElem!_insert [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} {v : β} :
|
||||
theorem getElem!_insert [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.WF) {k a : α} {v : β} :
|
||||
(m.insert k v)[a]! = if k == a then v else m[a]! :=
|
||||
DHashMap.Raw.Const.get!_insert h.out
|
||||
|
||||
@[simp]
|
||||
theorem getElem!_insert_self [EquivBEq α] [LawfulHashable α] [Inhabited β] {k : α} {v : β} :
|
||||
(m.insert k v)[k]! = v :=
|
||||
theorem getElem!_insert_self [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.WF) {k : α}
|
||||
{v : β} : (m.insert k v)[k]! = v :=
|
||||
DHashMap.Raw.Const.get!_insert_self h.out
|
||||
|
||||
theorem getElem!_eq_default_of_contains_eq_false [EquivBEq α] [LawfulHashable α] [Inhabited β]
|
||||
{a : α} : m.contains a = false → m[a]! = default :=
|
||||
(h : m.WF) {a : α} : m.contains a = false → m[a]! = default :=
|
||||
DHashMap.Raw.Const.get!_eq_default_of_contains_eq_false h.out
|
||||
|
||||
theorem getElem!_eq_default [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α} :
|
||||
theorem getElem!_eq_default [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.WF) {a : α} :
|
||||
¬a ∈ m → m[a]! = default :=
|
||||
DHashMap.Raw.Const.get!_eq_default h.out
|
||||
|
||||
theorem getElem!_erase [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} :
|
||||
theorem getElem!_erase [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.WF) {k a : α} :
|
||||
(m.erase k)[a]! = if k == a then default else m[a]! :=
|
||||
DHashMap.Raw.Const.get!_erase h.out
|
||||
|
||||
@[simp]
|
||||
theorem getElem!_erase_self [EquivBEq α] [LawfulHashable α] [Inhabited β] {k : α} :
|
||||
theorem getElem!_erase_self [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.WF) {k : α} :
|
||||
(m.erase k)[k]! = default :=
|
||||
DHashMap.Raw.Const.get!_erase_self h.out
|
||||
|
||||
theorem getElem?_eq_some_getElem!_of_contains [EquivBEq α] [LawfulHashable α] [Inhabited β]
|
||||
{a : α} : m.contains a = true → m[a]? = some m[a]! :=
|
||||
(h : m.WF) {a : α} : m.contains a = true → m[a]? = some m[a]! :=
|
||||
DHashMap.Raw.Const.get?_eq_some_get!_of_contains h.out
|
||||
|
||||
theorem getElem?_eq_some_getElem! [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α} :
|
||||
theorem getElem?_eq_some_getElem! [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.WF) {a : α} :
|
||||
a ∈ m → m[a]? = some m[a]! :=
|
||||
DHashMap.Raw.Const.get?_eq_some_get! h.out
|
||||
|
||||
theorem getElem!_eq_get!_getElem? [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α} :
|
||||
theorem getElem!_eq_get!_getElem? [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.WF) {a : α} :
|
||||
m[a]! = m[a]?.get! :=
|
||||
DHashMap.Raw.Const.get!_eq_get!_get? h.out
|
||||
|
||||
theorem getElem_eq_getElem! [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α} {h'} :
|
||||
theorem getElem_eq_getElem! [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.WF) {a : α} {h'} :
|
||||
m[a]'h' = m[a]! :=
|
||||
@DHashMap.Raw.Const.get_eq_get! _ _ _ _ _ h.out _ _ _ _ h'
|
||||
@DHashMap.Raw.Const.get_eq_get! _ _ _ _ _ _ _ _ h.out _ h'
|
||||
|
||||
theorem getElem!_congr [EquivBEq α] [LawfulHashable α] [Inhabited β] {a b : α} (hab : a == b) :
|
||||
m[a]! = m[b]! :=
|
||||
theorem getElem!_congr [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.WF) {a b : α}
|
||||
(hab : a == b) : m[a]! = m[b]! :=
|
||||
DHashMap.Raw.Const.get!_congr h.out hab
|
||||
|
||||
@[simp]
|
||||
|
|
@ -336,139 +346,140 @@ theorem getD_empty {a : α} {fallback : β} {c} : (empty c : Raw α β).getD a f
|
|||
theorem getD_emptyc {a : α} {fallback : β} : (∅ : Raw α β).getD a fallback = fallback :=
|
||||
DHashMap.Raw.Const.getD_empty
|
||||
|
||||
theorem getD_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} {fallback : β} :
|
||||
theorem getD_of_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} {fallback : β} :
|
||||
m.isEmpty = true → m.getD a fallback = fallback :=
|
||||
DHashMap.Raw.Const.getD_of_isEmpty h.out
|
||||
|
||||
theorem getD_insert [EquivBEq α] [LawfulHashable α] {k a : α} {fallback v : β} :
|
||||
theorem getD_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {fallback v : β} :
|
||||
(m.insert k v).getD a fallback = if k == a then v else m.getD a fallback :=
|
||||
DHashMap.Raw.Const.getD_insert h.out
|
||||
|
||||
@[simp]
|
||||
theorem getD_insert_self [EquivBEq α] [LawfulHashable α] {k : α} {fallback v : β} :
|
||||
theorem getD_insert_self [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {fallback v : β} :
|
||||
(m.insert k v).getD k fallback = v :=
|
||||
DHashMap.Raw.Const.getD_insert_self h.out
|
||||
|
||||
theorem getD_eq_fallback_of_contains_eq_false [EquivBEq α] [LawfulHashable α] {a : α}
|
||||
theorem getD_eq_fallback_of_contains_eq_false [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α}
|
||||
{fallback : β} : m.contains a = false → m.getD a fallback = fallback :=
|
||||
DHashMap.Raw.Const.getD_eq_fallback_of_contains_eq_false h.out
|
||||
|
||||
theorem getD_eq_fallback [EquivBEq α] [LawfulHashable α] {a : α} {fallback : β} :
|
||||
theorem getD_eq_fallback [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} {fallback : β} :
|
||||
¬a ∈ m → m.getD a fallback = fallback :=
|
||||
DHashMap.Raw.Const.getD_eq_fallback h.out
|
||||
|
||||
theorem getD_erase [EquivBEq α] [LawfulHashable α] {k a : α} {fallback : β} :
|
||||
theorem getD_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {fallback : β} :
|
||||
(m.erase k).getD a fallback = if k == a then fallback else m.getD a fallback :=
|
||||
DHashMap.Raw.Const.getD_erase h.out
|
||||
|
||||
@[simp]
|
||||
theorem getD_erase_self [EquivBEq α] [LawfulHashable α] {k : α} {fallback : β} :
|
||||
theorem getD_erase_self [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {fallback : β} :
|
||||
(m.erase k).getD k fallback = fallback :=
|
||||
DHashMap.Raw.Const.getD_erase_self h.out
|
||||
|
||||
theorem getElem?_eq_some_getD_of_contains [EquivBEq α] [LawfulHashable α] {a : α} {fallback : β} :
|
||||
m.contains a = true → m[a]? = some (m.getD a fallback) :=
|
||||
theorem getElem?_eq_some_getD_of_contains [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α}
|
||||
{fallback : β} : m.contains a = true → m[a]? = some (m.getD a fallback) :=
|
||||
DHashMap.Raw.Const.get?_eq_some_getD_of_contains h.out
|
||||
|
||||
theorem getElem?_eq_some_getD [EquivBEq α] [LawfulHashable α] {a : α} {fallback : β} :
|
||||
theorem getElem?_eq_some_getD [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} {fallback : β} :
|
||||
a ∈ m → m[a]? = some (m.getD a fallback) :=
|
||||
DHashMap.Raw.Const.get?_eq_some_getD h.out
|
||||
|
||||
theorem getD_eq_getD_getElem? [EquivBEq α] [LawfulHashable α] {a : α} {fallback : β} :
|
||||
theorem getD_eq_getD_getElem? [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} {fallback : β} :
|
||||
m.getD a fallback = m[a]?.getD fallback :=
|
||||
DHashMap.Raw.Const.getD_eq_getD_get? h.out
|
||||
|
||||
theorem getElem_eq_getD [EquivBEq α] [LawfulHashable α] {a : α} {fallback : β} {h'} :
|
||||
theorem getElem_eq_getD [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} {fallback : β} {h'} :
|
||||
m[a]'h' = m.getD a fallback :=
|
||||
@DHashMap.Raw.Const.get_eq_getD _ _ _ _ _ h.out _ _ _ _ h'
|
||||
@DHashMap.Raw.Const.get_eq_getD _ _ _ _ _ _ _ h.out _ _ h'
|
||||
|
||||
theorem getElem!_eq_getD_default [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α} :
|
||||
theorem getElem!_eq_getD_default [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.WF) {a : α} :
|
||||
m[a]! = m.getD a default :=
|
||||
DHashMap.Raw.Const.get!_eq_getD_default h.out
|
||||
|
||||
theorem getD_congr [EquivBEq α] [LawfulHashable α] {a b : α} {fallback : β} (hab : a == b) :
|
||||
m.getD a fallback = m.getD b fallback :=
|
||||
theorem getD_congr [EquivBEq α] [LawfulHashable α] (h : m.WF) {a b : α} {fallback : β}
|
||||
(hab : a == b) : m.getD a fallback = m.getD b fallback :=
|
||||
DHashMap.Raw.Const.getD_congr h.out hab
|
||||
|
||||
@[simp]
|
||||
theorem isEmpty_insertIfNew [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
|
||||
theorem isEmpty_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β} :
|
||||
(m.insertIfNew k v).isEmpty = false :=
|
||||
DHashMap.Raw.isEmpty_insertIfNew h.out
|
||||
|
||||
@[simp]
|
||||
theorem contains_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
|
||||
theorem contains_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {v : β} :
|
||||
(m.insertIfNew k v).contains a = (k == a || m.contains a) :=
|
||||
DHashMap.Raw.contains_insertIfNew h.out
|
||||
|
||||
@[simp]
|
||||
theorem mem_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
|
||||
theorem mem_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {v : β} :
|
||||
a ∈ m.insertIfNew k v ↔ k == a ∨ a ∈ m :=
|
||||
DHashMap.Raw.mem_insertIfNew h.out
|
||||
|
||||
theorem contains_insertIfNew_self [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
|
||||
theorem contains_insertIfNew_self [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β} :
|
||||
(m.insertIfNew k v).contains k :=
|
||||
DHashMap.Raw.contains_insertIfNew_self h.out
|
||||
|
||||
theorem mem_insertIfNew_self [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
|
||||
theorem mem_insertIfNew_self [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β} :
|
||||
k ∈ m.insertIfNew k v :=
|
||||
DHashMap.Raw.mem_insertIfNew_self h.out
|
||||
|
||||
theorem contains_of_contains_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
|
||||
(m.insertIfNew k v).contains a → (k == a) = false → m.contains a :=
|
||||
theorem contains_of_contains_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α}
|
||||
{v : β} : (m.insertIfNew k v).contains a → (k == a) = false → m.contains a :=
|
||||
DHashMap.Raw.contains_of_contains_insertIfNew h.out
|
||||
|
||||
theorem mem_of_mem_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
|
||||
theorem mem_of_mem_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {v : β} :
|
||||
a ∈ m.insertIfNew k v → (k == a) = false → a ∈ m :=
|
||||
DHashMap.Raw.mem_of_mem_insertIfNew h.out
|
||||
|
||||
/-- This is a restatement of `contains_insertIfNew` that is written to exactly match the proof
|
||||
obligation in the statement of `getElem_insertIfNew`. -/
|
||||
theorem contains_of_contains_insertIfNew' [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
|
||||
(m.insertIfNew k v).contains a → ¬((k == a) ∧ m.contains k = false) → m.contains a :=
|
||||
theorem contains_of_contains_insertIfNew' [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α}
|
||||
{v : β} : (m.insertIfNew k v).contains a → ¬((k == a) ∧ m.contains k = false) → m.contains a :=
|
||||
DHashMap.Raw.contains_of_contains_insertIfNew' h.out
|
||||
|
||||
/-- This is a restatement of `mem_insertIfNew` that is written to exactly match the proof obligation
|
||||
in the statement of `getElem_insertIfNew`. -/
|
||||
theorem mem_of_mem_insertIfNew' [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
|
||||
theorem mem_of_mem_insertIfNew' [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {v : β} :
|
||||
a ∈ m.insertIfNew k v → ¬((k == a) ∧ ¬k ∈ m) → a ∈ m :=
|
||||
DHashMap.Raw.mem_of_mem_insertIfNew' h.out
|
||||
|
||||
theorem size_insertIfNew [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
|
||||
theorem size_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β} :
|
||||
(m.insertIfNew k v).size = if k ∈ m then m.size else m.size + 1 :=
|
||||
DHashMap.Raw.size_insertIfNew h.out
|
||||
|
||||
theorem size_le_size_insertIfNew [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
|
||||
theorem size_le_size_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β} :
|
||||
m.size ≤ (m.insertIfNew k v).size :=
|
||||
DHashMap.Raw.size_le_size_insertIfNew h.out
|
||||
|
||||
theorem size_insertIfNew_le [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
|
||||
theorem size_insertIfNew_le [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β} :
|
||||
(m.insertIfNew k v).size ≤ m.size + 1 :=
|
||||
DHashMap.Raw.size_insertIfNew_le h.out
|
||||
|
||||
theorem getElem?_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
|
||||
theorem getElem?_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {v : β} :
|
||||
(m.insertIfNew k v)[a]? = if k == a ∧ ¬k ∈ m then some v else m[a]? :=
|
||||
DHashMap.Raw.Const.get?_insertIfNew h.out
|
||||
|
||||
theorem getElem_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} {h₁} :
|
||||
theorem getElem_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {v : β} {h₁} :
|
||||
(m.insertIfNew k v)[a]'h₁ =
|
||||
if h₂ : k == a ∧ ¬k ∈ m then v else m[a]'(mem_of_mem_insertIfNew' h h₁ h₂) :=
|
||||
DHashMap.Raw.Const.get_insertIfNew h.out (h₁ := h₁)
|
||||
|
||||
theorem getElem!_insertIfNew [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} {v : β} :
|
||||
(m.insertIfNew k v)[a]! = if k == a ∧ ¬k ∈ m then v else m[a]! :=
|
||||
theorem getElem!_insertIfNew [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.WF) {k a : α}
|
||||
{v : β} : (m.insertIfNew k v)[a]! = if k == a ∧ ¬k ∈ m then v else m[a]! :=
|
||||
DHashMap.Raw.Const.get!_insertIfNew h.out
|
||||
|
||||
theorem getD_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {fallback v : β} :
|
||||
theorem getD_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {fallback v : β} :
|
||||
(m.insertIfNew k v).getD a fallback =
|
||||
if k == a ∧ ¬k ∈ m then v else m.getD a fallback :=
|
||||
DHashMap.Raw.Const.getD_insertIfNew h.out
|
||||
|
||||
@[simp]
|
||||
theorem getThenInsertIfNew?_fst {k : α} {v : β} : (getThenInsertIfNew? m k v).1 = get? m k :=
|
||||
theorem getThenInsertIfNew?_fst (h : m.WF) {k : α} {v : β} :
|
||||
(getThenInsertIfNew? m k v).1 = get? m k :=
|
||||
DHashMap.Raw.Const.getThenInsertIfNew?_fst h.out
|
||||
|
||||
@[simp]
|
||||
theorem getThenInsertIfNew?_snd {k : α} {v : β} :
|
||||
theorem getThenInsertIfNew?_snd (h : m.WF) {k : α} {v : β} :
|
||||
(getThenInsertIfNew? m k v).2 = m.insertIfNew k v :=
|
||||
ext (DHashMap.Raw.Const.getThenInsertIfNew?_snd h.out)
|
||||
|
||||
|
|
|
|||
|
|
@ -20,18 +20,30 @@ set_option autoImplicit false
|
|||
|
||||
universe u v
|
||||
|
||||
variable {α : Type u} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α]
|
||||
variable {α : Type u}
|
||||
|
||||
namespace Std.HashSet
|
||||
|
||||
namespace Raw
|
||||
|
||||
variable {m : Raw α} (h : m.WF)
|
||||
set_option deprecated.oldSectionVars true
|
||||
variable {m : Raw α}
|
||||
|
||||
private theorem ext {m m' : Raw α} : m.inner = m'.inner → m = m' := by
|
||||
cases m; cases m'; rintro rfl; rfl
|
||||
|
||||
@[simp]
|
||||
theorem size_empty {c} : (empty c : Raw α).size = 0 :=
|
||||
HashMap.Raw.size_empty
|
||||
|
||||
@[simp]
|
||||
theorem size_emptyc : (∅ : Raw α).size = 0 :=
|
||||
HashMap.Raw.size_emptyc
|
||||
|
||||
theorem isEmpty_eq_size_eq_zero : m.isEmpty = (m.size == 0) :=
|
||||
HashMap.Raw.isEmpty_eq_size_eq_zero
|
||||
|
||||
variable [BEq α] [Hashable α]
|
||||
|
||||
@[simp]
|
||||
theorem isEmpty_empty {c} : (empty c : Raw α).isEmpty :=
|
||||
HashMap.Raw.isEmpty_empty
|
||||
|
|
@ -41,17 +53,19 @@ theorem isEmpty_emptyc : (∅ : Raw α).isEmpty :=
|
|||
HashMap.Raw.isEmpty_emptyc
|
||||
|
||||
@[simp]
|
||||
theorem isEmpty_insert [EquivBEq α] [LawfulHashable α] {a : α} : (m.insert a).isEmpty = false :=
|
||||
theorem isEmpty_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
|
||||
(m.insert a).isEmpty = false :=
|
||||
HashMap.Raw.isEmpty_insertIfNew h.out
|
||||
|
||||
theorem mem_iff_contains {a : α} : a ∈ m ↔ m.contains a :=
|
||||
HashMap.Raw.mem_iff_contains
|
||||
|
||||
theorem contains_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a == b) :
|
||||
theorem contains_congr [EquivBEq α] [LawfulHashable α] (h : m.WF) {a b : α} (hab : a == b) :
|
||||
m.contains a = m.contains b :=
|
||||
HashMap.Raw.contains_congr h.out hab
|
||||
|
||||
theorem mem_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a == b) : a ∈ m ↔ b ∈ m :=
|
||||
theorem mem_congr [EquivBEq α] [LawfulHashable α] (h : m.WF) {a b : α} (hab : a == b) :
|
||||
a ∈ m ↔ b ∈ m :=
|
||||
HashMap.Raw.mem_congr h.out hab
|
||||
|
||||
@[simp] theorem contains_empty {a : α} {c} : (empty c : Raw α).contains a = false :=
|
||||
|
|
@ -66,74 +80,67 @@ theorem mem_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a == b) :
|
|||
@[simp] theorem not_mem_emptyc {a : α} : ¬a ∈ (∅ : Raw α) :=
|
||||
HashMap.Raw.not_mem_emptyc
|
||||
|
||||
theorem contains_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} :
|
||||
theorem contains_of_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
|
||||
m.isEmpty → m.contains a = false :=
|
||||
HashMap.Raw.contains_of_isEmpty h.out
|
||||
|
||||
theorem not_mem_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} :
|
||||
theorem not_mem_of_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
|
||||
m.isEmpty → ¬a ∈ m :=
|
||||
HashMap.Raw.not_mem_of_isEmpty h.out
|
||||
|
||||
theorem isEmpty_eq_false_iff_exists_contains_eq_true [EquivBEq α] [LawfulHashable α] :
|
||||
theorem isEmpty_eq_false_iff_exists_contains_eq_true [EquivBEq α] [LawfulHashable α] (h : m.WF) :
|
||||
m.isEmpty = false ↔ ∃ a, m.contains a = true :=
|
||||
HashMap.Raw.isEmpty_eq_false_iff_exists_contains_eq_true h.out
|
||||
|
||||
theorem isEmpty_eq_false_iff_exists_mem [EquivBEq α] [LawfulHashable α] :
|
||||
theorem isEmpty_eq_false_iff_exists_mem [EquivBEq α] [LawfulHashable α] (h : m.WF) :
|
||||
m.isEmpty = false ↔ ∃ a, a ∈ m :=
|
||||
HashMap.Raw.isEmpty_eq_false_iff_exists_mem h.out
|
||||
|
||||
theorem isEmpty_iff_forall_contains [EquivBEq α] [LawfulHashable α] :
|
||||
theorem isEmpty_iff_forall_contains [EquivBEq α] [LawfulHashable α] (h : m.WF) :
|
||||
m.isEmpty = true ↔ ∀ a, m.contains a = false :=
|
||||
HashMap.Raw.isEmpty_iff_forall_contains h.out
|
||||
|
||||
theorem isEmpty_iff_forall_not_mem [EquivBEq α] [LawfulHashable α] :
|
||||
theorem isEmpty_iff_forall_not_mem [EquivBEq α] [LawfulHashable α] (h : m.WF) :
|
||||
m.isEmpty = true ↔ ∀ a, ¬a ∈ m :=
|
||||
HashMap.Raw.isEmpty_iff_forall_not_mem h.out
|
||||
|
||||
@[simp]
|
||||
theorem contains_insert [EquivBEq α] [LawfulHashable α] {k a : α} :
|
||||
theorem contains_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} :
|
||||
(m.insert k).contains a = (k == a || m.contains a) :=
|
||||
HashMap.Raw.contains_insertIfNew h.out
|
||||
|
||||
@[simp]
|
||||
theorem mem_insert [EquivBEq α] [LawfulHashable α] {k a : α} : a ∈ m.insert k ↔ k == a ∨ a ∈ m :=
|
||||
theorem mem_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} :
|
||||
a ∈ m.insert k ↔ k == a ∨ a ∈ m :=
|
||||
HashMap.Raw.mem_insertIfNew h.out
|
||||
|
||||
theorem contains_of_contains_insert [EquivBEq α] [LawfulHashable α] {k a : α} :
|
||||
theorem contains_of_contains_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} :
|
||||
(m.insert k).contains a → (k == a) = false → m.contains a :=
|
||||
HashMap.Raw.contains_of_contains_insertIfNew h.out
|
||||
|
||||
theorem mem_of_mem_insert [EquivBEq α] [LawfulHashable α] {k a : α} :
|
||||
theorem mem_of_mem_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} :
|
||||
a ∈ m.insert k → (k == a) = false → a ∈ m :=
|
||||
HashMap.Raw.mem_of_mem_insertIfNew h.out
|
||||
|
||||
@[simp]
|
||||
theorem contains_insert_self [EquivBEq α] [LawfulHashable α] {k : α} : (m.insert k).contains k :=
|
||||
theorem contains_insert_self [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
|
||||
(m.insert k).contains k :=
|
||||
HashMap.Raw.contains_insertIfNew_self h.out
|
||||
|
||||
@[simp]
|
||||
theorem mem_insert_self [EquivBEq α] [LawfulHashable α] {k : α} : k ∈ m.insert k :=
|
||||
theorem mem_insert_self [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} : k ∈ m.insert k :=
|
||||
HashMap.Raw.mem_insertIfNew_self h.out
|
||||
|
||||
@[simp]
|
||||
theorem size_empty {c} : (empty c : Raw α).size = 0 :=
|
||||
HashMap.Raw.size_empty
|
||||
|
||||
@[simp]
|
||||
theorem size_emptyc : (∅ : Raw α).size = 0 :=
|
||||
HashMap.Raw.size_emptyc
|
||||
|
||||
theorem isEmpty_eq_size_eq_zero : m.isEmpty = (m.size == 0) :=
|
||||
HashMap.Raw.isEmpty_eq_size_eq_zero
|
||||
|
||||
theorem size_insert [EquivBEq α] [LawfulHashable α] {k : α} :
|
||||
theorem size_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
|
||||
(m.insert k).size = if k ∈ m then m.size else m.size + 1 :=
|
||||
HashMap.Raw.size_insertIfNew h.out
|
||||
|
||||
theorem size_le_size_insert [EquivBEq α] [LawfulHashable α] {k : α} : m.size ≤ (m.insert k).size :=
|
||||
theorem size_le_size_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
|
||||
m.size ≤ (m.insert k).size :=
|
||||
HashMap.Raw.size_le_size_insertIfNew h.out
|
||||
|
||||
theorem size_insert_le [EquivBEq α] [LawfulHashable α] {k : α} : (m.insert k).size ≤ m.size + 1 :=
|
||||
theorem size_insert_le [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
|
||||
(m.insert k).size ≤ m.size + 1 :=
|
||||
HashMap.Raw.size_insertIfNew_le h.out
|
||||
|
||||
@[simp]
|
||||
|
|
@ -145,44 +152,46 @@ theorem erase_emptyc {k : α} : (∅ : Raw α).erase k = ∅ :=
|
|||
ext HashMap.Raw.erase_emptyc
|
||||
|
||||
@[simp]
|
||||
theorem isEmpty_erase [EquivBEq α] [LawfulHashable α] {k : α} :
|
||||
theorem isEmpty_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
|
||||
(m.erase k).isEmpty = (m.isEmpty || (m.size == 1 && m.contains k)) :=
|
||||
HashMap.Raw.isEmpty_erase h.out
|
||||
|
||||
@[simp]
|
||||
theorem contains_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
|
||||
theorem contains_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} :
|
||||
(m.erase k).contains a = (!(k == a) && m.contains a) :=
|
||||
HashMap.Raw.contains_erase h.out
|
||||
|
||||
@[simp]
|
||||
theorem mem_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
|
||||
theorem mem_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} :
|
||||
a ∈ m.erase k ↔ (k == a) = false ∧ a ∈ m :=
|
||||
HashMap.Raw.mem_erase h.out
|
||||
|
||||
theorem contains_of_contains_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
|
||||
theorem contains_of_contains_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} :
|
||||
(m.erase k).contains a → m.contains a :=
|
||||
HashMap.Raw.contains_of_contains_erase h.out
|
||||
|
||||
theorem mem_of_mem_erase [EquivBEq α] [LawfulHashable α] {k a : α} : a ∈ m.erase k → a ∈ m :=
|
||||
theorem mem_of_mem_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} :
|
||||
a ∈ m.erase k → a ∈ m :=
|
||||
HashMap.Raw.mem_of_mem_erase h.out
|
||||
|
||||
theorem size_erase [EquivBEq α] [LawfulHashable α] {k : α} :
|
||||
theorem size_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
|
||||
(m.erase k).size = if k ∈ m then m.size - 1 else m.size :=
|
||||
HashMap.Raw.size_erase h.out
|
||||
|
||||
theorem size_erase_le [EquivBEq α] [LawfulHashable α] {k : α} : (m.erase k).size ≤ m.size :=
|
||||
theorem size_erase_le [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
|
||||
(m.erase k).size ≤ m.size :=
|
||||
HashMap.Raw.size_erase_le h.out
|
||||
|
||||
theorem size_le_size_erase [EquivBEq α] [LawfulHashable α] {k : α} :
|
||||
theorem size_le_size_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
|
||||
m.size ≤ (m.erase k).size + 1 :=
|
||||
HashMap.Raw.size_le_size_erase h.out
|
||||
|
||||
@[simp]
|
||||
theorem containsThenInsert_fst {k : α} : (m.containsThenInsert k).1 = m.contains k :=
|
||||
theorem containsThenInsert_fst (h : m.WF) {k : α} : (m.containsThenInsert k).1 = m.contains k :=
|
||||
HashMap.Raw.containsThenInsertIfNew_fst h.out
|
||||
|
||||
@[simp]
|
||||
theorem containsThenInsert_snd {k : α} : (m.containsThenInsert k).2 = m.insert k :=
|
||||
theorem containsThenInsert_snd (h : m.WF) {k : α} : (m.containsThenInsert k).2 = m.insert k :=
|
||||
ext (HashMap.Raw.containsThenInsertIfNew_snd h.out)
|
||||
|
||||
end Raw
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue