diff --git a/src/Std/Data/DHashMap/Internal/RawLemmas.lean b/src/Std/Data/DHashMap/Internal/RawLemmas.lean index e8da7ecc06..73d33cde2c 100644 --- a/src/Std/Data/DHashMap/Internal/RawLemmas.lean +++ b/src/Std/Data/DHashMap/Internal/RawLemmas.lean @@ -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 diff --git a/src/Std/Data/DHashMap/RawLemmas.lean b/src/Std/Data/DHashMap/RawLemmas.lean index 1700ce0562..55f838b85c 100644 --- a/src/Std/Data/DHashMap/RawLemmas.lean +++ b/src/Std/Data/DHashMap/RawLemmas.lean @@ -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 _) diff --git a/src/Std/Data/HashMap/RawLemmas.lean b/src/Std/Data/HashMap/RawLemmas.lean index 5f2f577b61..d126bbb96e 100644 --- a/src/Std/Data/HashMap/RawLemmas.lean +++ b/src/Std/Data/HashMap/RawLemmas.lean @@ -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) diff --git a/src/Std/Data/HashSet/RawLemmas.lean b/src/Std/Data/HashSet/RawLemmas.lean index 0b07f35462..1a7c55cf64 100644 --- a/src/Std/Data/HashSet/RawLemmas.lean +++ b/src/Std/Data/HashSet/RawLemmas.lean @@ -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