Move up

Author: jt0202

src/Std/Data/HashMap/Basic.lean

@@ -283,15 +283,15 @@ instance [BEq α] [Hashable α] : Inter (HashMap α β) := ⟨inter⟩
 
 instance [BEq α] [Hashable α] : SDiff (HashMap α β) := ⟨diff⟩
 
-section Unverified
-
-/-! We currently do not provide lemmas for the functions below. -/
-
 @[inline, inherit_doc DHashMap.partition] def partition (f : α → β → Bool)
     (m : HashMap α β) : HashMap α β × HashMap α β :=
   let ⟨l, r⟩ := m.inner.partition f
   ⟨⟨l⟩, ⟨r⟩⟩
 
+section Unverified
+
+/-! We currently do not provide lemmas for the functions below. -/
+
 @[inline, inherit_doc DHashMap.values] def values (m : HashMap α β) : List β :=
   m.inner.values
 

src/Std/Data/HashMap/Lemmas.lean

@@ -943,6 +943,14 @@ theorem distinct_keys_toList [EquivBEq α] [LawfulHashable α] :
     m.toList.Pairwise (fun a b => (a.1 == b.1) = false) :=
   DHashMap.Const.distinct_keys_toList
 
+theorem nodup_toList [EquivBEq α] [LawfulHashable α] :
+    m.toList.Nodup := DHashMap.Const.nodup_toList
+
+theorem mem_toList_insert_of_not_mem [EquivBEq α] [LawfulHashable α]
+    {k : α} {v : β} {x : α × β} (h' : ¬ k ∈ m) :
+    x ∈ (m.insert k v).toList ↔ x = ⟨k, v⟩ ∨ x ∈ m.toList :=
+  DHashMap.Const.mem_toList_insert_of_not_mem h'
+
 @[simp]
 theorem toArray_toList :
     m.toList.toArray = m.toArray :=
@@ -3478,5 +3486,36 @@ theorem getKeyD_map [EquivBEq α] [LawfulHashable α]
   DHashMap.getKeyD_map
 
 end map
+
+variable {m : HashMap α β}
+
+@[simp]
+theorem size_fst_partition_add_size_snd_partition_eq_size [EquivBEq α] [LawfulHashable α]
+    {f : α → β → Bool} :
+    (m.partition f).1.size + (m.partition f).2.size = m.size :=
+  DHashMap.size_fst_partition_add_size_snd_partition_eq_size
+
+@[simp]
+theorem fst_partition_not_eq_snd_partition [EquivBEq α] [LawfulHashable α]
+    {f : α → β → Bool} :
+    (m.partition (fun a b => ! f a b)).fst = (m.partition f).snd := by
+  simp [partition, DHashMap.fst_partition_not_eq_snd_partition]
+
+@[simp]
+theorem snd_partition_not_eq_fst_partition [EquivBEq α] [LawfulHashable α]
+    {f : α → β → Bool} :
+    (m.partition (fun a b => ! f a b)).snd = (m.partition f).fst := by
+  simp [partition, DHashMap.snd_partition_not_eq_fst_partition]
+
+theorem fst_partition_equiv_filter [EquivBEq α] [LawfulHashable α]
+    {f : α → β → Bool} :
+    (m.partition f).fst ~m m.filter f :=
+  ⟨DHashMap.fst_partition_equiv_filter⟩
+
+theorem snd_partition_equiv_filter_not [EquivBEq α] [LawfulHashable α]
+    {f : α → β → Bool}  :
+    (m.partition f).snd ~m m.filter (fun a b => ! f a b) :=
+  ⟨DHashMap.snd_partition_equiv_filter_not⟩
+
 attribute [simp] contains_eq_false_iff_not_mem
 end Std.HashMap

src/Std/Data/HashMap/RawLemmas.lean

@@ -953,6 +953,14 @@ theorem distinct_keys_toList [EquivBEq α] [LawfulHashable α] (h : m.WF) :
     m.toList.Pairwise (fun a b => (a.1 == b.1) = false) :=
   DHashMap.Raw.Const.distinct_keys_toList h.out
 
+theorem nodup_toList [EquivBEq α] [LawfulHashable α] (h : m.WF) :
+    m.toList.Nodup := DHashMap.Raw.Const.nodup_toList h.out
+
+theorem mem_toList_insert_of_not_mem [EquivBEq α] [LawfulHashable α] (h : m.WF)
+    {k : α} {v : β} {x : α × β} : ¬ k ∈ m →
+    (x ∈ (m.insert k v).toList ↔ x = ⟨k, v⟩ ∨ x ∈ m.toList) :=
+  DHashMap.Raw.Const.mem_toList_insert_of_not_mem h.out
+
 @[simp]
 theorem toArray_toList (h : m.WF) :
     m.toList.toArray = m.toArray :=
@@ -3538,6 +3546,35 @@ theorem getD_map_of_getKey?_eq_some [EquivBEq α] [LawfulHashable α]
   DHashMap.Raw.Const.getD_map_of_getKey?_eq_some h.out h'
 
 end map
+
+@[simp]
+theorem size_fst_partition_add_size_snd_partition_eq_size [EquivBEq α] [LawfulHashable α]
+    {p : α → β → Bool} (h : m.WF) :
+    (m.partition p).1.size + (m.partition p).2.size = m.size :=
+  DHashMap.Raw.size_fst_partition_add_size_snd_partition_eq_size h.out
+
+@[simp]
+theorem fst_partition_not_eq_snd_partition [EquivBEq α] [LawfulHashable α]
+    {p : α → β → Bool} (h : m.WF) :
+    (m.partition (fun a b => ! p a b)).fst = (m.partition p).snd := by
+  simp [partition, DHashMap.Raw.fst_partition_not_eq_snd_partition h.out]
+
+@[simp]
+theorem snd_partition_not_eq_fst_partition [EquivBEq α] [LawfulHashable α]
+    {p : α → β → Bool} (h : m.WF) :
+    (m.partition (fun a b => ! p a b)).snd = (m.partition p).fst := by
+  simp [partition, DHashMap.Raw.snd_partition_not_eq_fst_partition h.out]
+
+theorem fst_partition_equiv_filter [EquivBEq α] [LawfulHashable α]
+    {p : α → β → Bool} (h : m.WF)  :
+    (m.partition p).fst ~m m.filter p :=
+  ⟨DHashMap.Raw.fst_partition_equiv_filter h.out⟩
+
+theorem snd_partition_equiv_filter_not [EquivBEq α] [LawfulHashable α]
+    {p : α → β → Bool} (h : m.WF)  :
+    (m.partition p).snd ~m m.filter (fun a b => ! p a b) :=
+  ⟨DHashMap.Raw.snd_partition_equiv_filter_not h.out⟩
+
 attribute [simp] contains_eq_false_iff_not_mem
 end Raw
 

src/Std/Data/HashSet/Lemmas.lean

@@ -1523,5 +1523,36 @@ theorem getD_filter [EquivBEq α] [LawfulHashable α]
   HashMap.getKeyD_filter_key
 
 end filter
+
+variable {m : HashSet α}
+
+@[simp]
+theorem size_fst_partition_add_size_snd_partition_eq_size [EquivBEq α] [LawfulHashable α]
+    {f : α → Bool} :
+    (m.partition f).1.size + (m.partition f).2.size = m.size :=
+  HashMap.size_fst_partition_add_size_snd_partition_eq_size
+
+@[simp]
+theorem fst_partition_not_eq_snd_partition [EquivBEq α] [LawfulHashable α]
+    {f : α → Bool} :
+    (m.partition (fun a => ! f a)).fst = (m.partition f).snd := by
+  simp [partition, HashMap.fst_partition_not_eq_snd_partition]
+
+@[simp]
+theorem snd_partition_not_eq_fst_partition [EquivBEq α] [LawfulHashable α]
+    {f : α → Bool} :
+    (m.partition (fun a => ! f a)).snd = (m.partition f).fst := by
+  simp [partition, HashMap.snd_partition_not_eq_fst_partition]
+
+theorem fst_partition_equiv_filter [EquivBEq α] [LawfulHashable α]
+    {f : α → Bool} :
+    (m.partition f).fst ~m m.filter f :=
+  ⟨HashMap.fst_partition_equiv_filter⟩
+
+theorem snd_partition_equiv_filter_not [EquivBEq α] [LawfulHashable α]
+    {f : α → Bool}  :
+    (m.partition f).snd ~m m.filter (fun a => ! f a) :=
+  ⟨HashMap.snd_partition_equiv_filter_not⟩
+
 attribute [simp] contains_eq_false_iff_not_mem
 end Std.HashSet

src/Std/Data/HashSet/RawLemmas.lean

@@ -1594,6 +1594,35 @@ theorem get_filter [EquivBEq α] [LawfulHashable α]
 
 end filter
 
+@[simp]
+theorem size_fst_partition_add_size_snd_partition_eq_size [EquivBEq α] [LawfulHashable α]
+    {p : α → Bool} (h : m.WF) :
+    (m.partition p).1.size + (m.partition p).2.size = m.size :=
+  HashMap.Raw.size_fst_partition_add_size_snd_partition_eq_size h.out
+
+@[simp]
+theorem fst_partition_not_eq_snd_partition [EquivBEq α] [LawfulHashable α]
+    {p : α → Bool} (h : m.WF) :
+    (m.partition (fun a => ! p a)).fst = (m.partition p).snd := by
+  simp [partition, HashMap.Raw.fst_partition_not_eq_snd_partition h.out]
+
+@[simp]
+theorem snd_partition_not_eq_fst_partition [EquivBEq α] [LawfulHashable α]
+    {p : α → Bool} (h : m.WF) :
+    (m.partition (fun a => ! p a)).snd = (m.partition p).fst := by
+  simp [partition, HashMap.Raw.snd_partition_not_eq_fst_partition h.out]
+
+theorem fst_partition_equiv_filter [EquivBEq α] [LawfulHashable α]
+    {p : α → Bool} (h : m.WF)  :
+    (m.partition p).fst ~m m.filter p :=
+  ⟨HashMap.Raw.fst_partition_equiv_filter h.out⟩
+
+theorem snd_partition_equiv_filter_not [EquivBEq α] [LawfulHashable α]
+    {p : α → Bool} (h : m.WF)  :
+    (m.partition p).snd ~m m.filter (fun a => ! p a) :=
+  ⟨HashMap.Raw.snd_partition_equiv_filter_not h.out⟩
+
+
 attribute [simp] contains_eq_false_iff_not_mem
 end Raw