Move up to Raw and free lemmas

Author: jt0202

src/Std/Data/DHashMap/Basic.lean

@@ -366,7 +366,8 @@ section Unverified
 
 @[inline, inherit_doc Raw.partition] def partition (f : (a : α) → β a → Bool)
     (m : DHashMap α β) : DHashMap α β × DHashMap α β :=
-  ⟨⟨(m.1.partition f).1, Raw.WF.fst_partition m.2⟩, ⟨(m.1.partition f).2, Raw.WF.snd_partition m.2⟩⟩
+  ⟨⟨(Raw₀.partition f ⟨m.1, m.2.size_buckets_pos⟩).1, Raw.WF.fst_partition₀⟩,
+    ⟨(Raw₀.partition f ⟨m.1, m.2.size_buckets_pos⟩).2, Raw.WF.snd_partition₀⟩⟩
 
 @[inline, inherit_doc Raw.values] def values {β : Type v}
     (m : DHashMap α (fun _ => β)) : List β :=

src/Std/Data/DHashMap/Internal/RawLemmas.lean

@@ -1032,6 +1032,20 @@ theorem distinct_keys_toList [EquivBEq α] [LawfulHashable α] (h : m.1.WF) :
     m.1.toList.Pairwise (fun a b => (a.1 == b.1) = false) := by
   simp_to_model [toList] using List.pairwise_fst_eq_false
 
+theorem nodup_toList [EquivBEq α] [LawfulHashable α] (h : m.1.WF) :
+    m.1.toList.Nodup := by
+  simp_to_model [toList] using List.nodup_of_distinctKeys
+
+theorem mem_toList_insert_of_contains_eq_false [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
+    {k : α} {v : β k} {x : (a : α) × β a} (h' : m.contains k = false) :
+    x ∈ (m.insert k v).1.toList ↔ x = ⟨k, v⟩ ∨ x ∈ m.1.toList := by
+  rw [contains_eq_containsₘ] at h'
+  simp [Raw.toList, insert_eq_insertₘ, insertₘ, h', Bool.false_eq_true, ↓reduceIte,
+    Raw.foldRev_cons, List.append_nil]
+  rw [List.Perm.mem_iff (toListModel_expandIfNecessary (consₘ m k v))]
+  rw [List.Perm.mem_iff (toListModel_consₘ m (Raw.WF.out h) k v)]
+  simp
+
 namespace Const
 
 variable {β : Type v} (m : Raw₀ α (fun _ => β))
@@ -1081,6 +1095,28 @@ theorem distinct_keys_toList [EquivBEq α] [LawfulHashable α] (h : m.1.WF) :
     (Raw.Const.toList m.1).Pairwise (fun a b => (a.1 == b.1) = false) := by
   simp_to_model [Const.toList] using List.pairwise_fst_eq_false_map_toProd
 
+theorem nodup_toList [EquivBEq α] [LawfulHashable α] (h : m.1.WF) :
+    (Raw.Const.toList m.1).Nodup := by
+  simp_to_model [Const.toList] using List.nodup_map_of_distinctKeys
+
+theorem mem_toList_insert_of_contains_eq_false [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
+    {k : α} {v : β} {x : α × β} (h' : m.contains k = false) :
+    x ∈ (Raw.Const.toList (m.insert k v).1) ↔ x = ⟨k, v⟩ ∨ x ∈ Raw.Const.toList m.1 := by
+  rw [contains_eq_containsₘ] at h'
+  simp only [Raw.Const.toList, insert_eq_insertₘ, insertₘ, h', Bool.false_eq_true, ↓reduceIte,
+    Raw.foldRev_cons_mk, List.append_nil]
+  rw [← List.mem_map_toProd_iff_mem, ← List.mem_map_toProd_iff_mem]
+  rw [List.Perm.mem_iff (toListModel_expandIfNecessary (consₘ m k v))]
+  rw [List.Perm.mem_iff (toListModel_consₘ m (Raw.WF.out h) k v)]
+  simp only [List.mem_cons, Sigma.mk.injEq, heq_eq_eq]
+  have : x.fst = k ∧ x.snd = v ↔ x = (k,v) := by
+    constructor
+    · intro h
+      simp [← h.1, ← h.2]
+    · intro h
+      simp [h]
+  rw [this]
+
 end Const
 
 omit [Hashable α] [BEq α] in
@@ -5184,16 +5220,6 @@ theorem snd_partition_not_eq_fst_partition [EquivBEq α] [LawfulHashable α]
   rw [← fst_partition_not_eq_snd_partition]
   simp
 
-private theorem mem_toList_insert_of_contains_eq_false [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
-    {k : α} {v : β k} {x : (a : α) × β a} (h' : m.contains k = false) :
-    x ∈ (m.insert k v).1.toList ↔ x ∈ m.1.toList ∨ x = ⟨k, v⟩ := by
-  rw [contains_eq_containsₘ] at h'
-  simp only [Raw.toList, insert_eq_insertₘ, insertₘ, h', Bool.false_eq_true, ↓reduceIte,
-    Raw.foldRev_cons, List.append_nil]
-  rw [List.Perm.mem_iff (toListModel_expandIfNecessary (consₘ m k v))]
-  rw [List.Perm.mem_iff (toListModel_consₘ m (Raw.WF.out h) k v)]
-  simp [Or.comm]
-
 private theorem mem_toList_fst_partition [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
     {p : (a : α) → β a → Bool} (x : (a : α) × β a) :
     x ∈ (m.partition p).1.1.toList ↔ x ∈ m.1.toList ∧ p x.1 x.2 = true := by
@@ -5228,10 +5254,10 @@ private theorem mem_toList_fst_partition [EquivBEq α] [LawfulHashable α] (h :
           | inr h =>
             cases h with
             | inl h =>
-              apply Or.inr h
-            | inr h =>
               rw [h]
               simp [hhd]
+            | inr h =>
+              apply Or.inr h
         · intro h
           cases h with
           | inl h =>
@@ -5278,23 +5304,6 @@ private theorem mem_toList_fst_partition [EquivBEq α] [LawfulHashable α] (h :
       · simp only [List.pairwise_cons] at h₄
         apply h₄.2
 
-private theorem nodup_toList [EquivBEq α] [LawfulHashable α] (h : m.1.WF) : m.1.toList.Nodup := by
-  simp only [List.Nodup, ne_eq]
-  suffices ∀ (l : List ((a :α) × β a)) (h₁ : List.Pairwise (fun a b => (a.1 == b.1) = false) l),
-    List.Pairwise (fun a b => a ≠ b) l from this m.1.toList (distinct_keys_toList _ h)
-  intro l
-  induction l with
-  | nil => simp
-  | cons hd tl ih =>
-    simp
-    intro h₁ h₂
-    refine And.intro ?_ (ih h₂)
-    intro a ha
-    false_or_by_contra
-    rename_i h'
-    specialize h₁ a ha
-    simp [h'] at h₁
-
 theorem fst_partition_equiv_filter [EquivBEq α] [LawfulHashable α]
     {p : (a : α) → β a → Bool} (h : m.1.WF)  :
     (m.partition p).1.1.Equiv (m.filter p).1 := by

src/Std/Data/DHashMap/Lemmas.lean

@@ -1247,6 +1247,17 @@ theorem distinct_keys_toList [EquivBEq α] [LawfulHashable α] :
     m.toList.Pairwise (fun a b => (a.1 == b.1) = false) :=
   Raw₀.distinct_keys_toList ⟨m.1, m.2.size_buckets_pos⟩ m.2
 
+theorem nodup_toList [EquivBEq α] [LawfulHashable α] :
+    m.toList.Nodup :=
+  Raw₀.nodup_toList ⟨m.1, m.2.size_buckets_pos⟩ m.2
+
+theorem mem_toList_insert_of_not_mem [EquivBEq α] [LawfulHashable α]
+    {k : α} {v : β k} {x : (a : α) × (β a)} (h' : ¬ k ∈ m) :
+    x ∈ (m.insert k v).toList ↔ x = ⟨k, v⟩ ∨ x ∈ m.toList := by
+  apply Raw₀.mem_toList_insert_of_contains_eq_false ⟨m.1, m.2.size_buckets_pos⟩ m.2
+  rw [mem_iff_contains, Bool.not_eq_true] at h'
+  apply h'
+
 namespace Const
 
 variable {β : Type v} {m : DHashMap α (fun _ => β)}
@@ -1306,6 +1317,17 @@ theorem distinct_keys_toList [EquivBEq α] [LawfulHashable α] :
     (toList m).Pairwise (fun a b => (a.1 == b.1) = false) :=
   Raw₀.Const.distinct_keys_toList ⟨m.1, m.2.size_buckets_pos⟩ m.2
 
+theorem nodup_toList [EquivBEq α] [LawfulHashable α] :
+    (Const.toList m).Nodup :=
+  Raw₀.Const.nodup_toList ⟨m.1, m.2.size_buckets_pos⟩ m.2
+
+theorem mem_toList_insert_of_not_mem [EquivBEq α] [LawfulHashable α]
+    {k : α} {v : β} {x : α × β} (h' : ¬ k ∈ m) :
+    x ∈ (Const.toList (m.insert k v)) ↔ x = ⟨k, v⟩ ∨ x ∈ Const.toList m := by
+  apply Raw₀.Const.mem_toList_insert_of_contains_eq_false ⟨m.1, m.2.size_buckets_pos⟩ m.2
+  rw [mem_iff_contains, Bool.not_eq_true] at h'
+  apply h'
+
 end Const
 
 @[simp]
@@ -5312,5 +5334,34 @@ theorem toList_map {m : DHashMap α fun _ => β}
 end Const
 
 end map
+
+@[simp]
+theorem size_fst_partition_add_size_snd_partition_eq_size [EquivBEq α] [LawfulHashable α]
+    {f : (a : α) → β a → Bool} :
+    (m.partition f).1.size + (m.partition f).2.size = m.size :=
+  Raw₀.size_partition ⟨m.1, m.2.size_buckets_pos⟩ m.2
+
+@[simp]
+theorem fst_partition_not_eq_snd_partition [EquivBEq α] [LawfulHashable α]
+    {f : (a : α) → β a → Bool} :
+    (m.partition (fun a b => ! f a b)).fst = (m.partition f).snd := by
+  simp [partition, Raw₀.fst_partition_not_eq_snd_partition ⟨m.1, m.2.size_buckets_pos⟩ (p:= f)]
+
+@[simp]
+theorem snd_partition_not_eq_fst_partition [EquivBEq α] [LawfulHashable α]
+    {f : (a : α) → β a → Bool} :
+    (m.partition (fun a b => ! f a b)).snd = (m.partition f).fst := by
+  simp [partition, Raw₀.snd_partition_not_eq_fst_partition ⟨m.1, m.2.size_buckets_pos⟩ (p:= f)]
+
+theorem fst_partition_equiv_filter [EquivBEq α] [LawfulHashable α]
+    {f : (a : α) → β a → Bool} :
+    (m.partition f).fst ~m m.filter f :=
+  ⟨Raw₀.fst_partition_equiv_filter ⟨m.1, m.2.size_buckets_pos⟩ m.2⟩
+
+theorem snd_partition_equiv_filter_not [EquivBEq α] [LawfulHashable α]
+    {f : (a : α) → β a → Bool}  :
+    (m.partition f).snd ~m m.filter (fun a b => ! f a b) :=
+  ⟨Raw₀.snd_partition_equiv_filter_not ⟨m.1, m.2.size_buckets_pos⟩ m.2⟩
+
 attribute [simp] contains_eq_false_iff_not_mem
 end Std.DHashMap

src/Std/Data/DHashMap/RawLemmas.lean

@@ -1318,6 +1318,21 @@ theorem distinct_keys_toList [EquivBEq α] [LawfulHashable α] (h : m.WF) :
     m.toList.Pairwise (fun a b => (a.1 == b.1) = false) := by
   apply Raw₀.distinct_keys_toList ⟨m, h.size_buckets_pos⟩ h
 
+theorem nodup_toList [EquivBEq α] [LawfulHashable α] (h : m.WF) :
+    m.toList.Nodup := by
+  apply Raw₀.nodup_toList ⟨m, h.size_buckets_pos⟩ h
+
+theorem mem_toList_insert_of_contains_eq_false [EquivBEq α] [LawfulHashable α] (h : m.WF)
+    {k : α} {v : β k} {x : (a : α) × β a} : m.contains k = false →
+    (x ∈ (m.insert k v).toList ↔ x = ⟨k, v⟩ ∨ x ∈ m.toList) := by
+  simp_to_raw using Raw₀.mem_toList_insert_of_contains_eq_false ⟨m, h.size_buckets_pos⟩ h
+
+theorem mem_toList_insert_of_not_mem [EquivBEq α] [LawfulHashable α] (h : m.WF)
+    {k : α} {v : β k} {x : (a : α) × β a} : ¬ k ∈ m →
+    (x ∈ (m.insert k v).toList ↔ x = ⟨k, v⟩ ∨ x ∈ m.toList) := by
+  rw [mem_iff_contains, Bool.not_eq_true]
+  apply mem_toList_insert_of_contains_eq_false h
+
 namespace Const
 
 variable {β : Type v} {m : Raw α (fun _ => β)}
@@ -1380,6 +1395,21 @@ theorem distinct_keys_toList [EquivBEq α] [LawfulHashable α] (h : m.WF) :
     (Raw.Const.toList m).Pairwise (fun a b => (a.1 == b.1) = false) := by
   apply Raw₀.Const.distinct_keys_toList ⟨m, h.size_buckets_pos⟩ h
 
+theorem nodup_toList [EquivBEq α] [LawfulHashable α] (h : m.WF) :
+    (Raw.Const.toList m).Nodup := by
+  apply Raw₀.Const.nodup_toList ⟨m, h.size_buckets_pos⟩ h
+
+theorem mem_toList_insert_of_contains_eq_false [EquivBEq α] [LawfulHashable α] (h : m.WF)
+    {k : α} {v : β} {x : α × β} : m.contains k = false →
+    (x ∈ (Raw.Const.toList (m.insert k v)) ↔ x = ⟨k, v⟩ ∨ x ∈ Raw.Const.toList m) := by
+  simp_to_raw using Raw₀.Const.mem_toList_insert_of_contains_eq_false ⟨m, h.size_buckets_pos⟩ h
+
+theorem mem_toList_insert_of_not_mem [EquivBEq α] [LawfulHashable α] (h : m.WF)
+    {k : α} {v : β} {x : α × β} : ¬ k ∈ m →
+    (x ∈ (Raw.Const.toList (m.insert k v)) ↔ x = ⟨k, v⟩ ∨ x ∈ Raw.Const.toList m) := by
+  rw [mem_iff_contains, Bool.not_eq_true]
+  apply mem_toList_insert_of_contains_eq_false h
+
 end Const
 
 @[simp]
@@ -5994,20 +6024,21 @@ end Const
 
 end map
 
+@[simp]
 theorem size_fst_partition_add_size_snd_partition_eq_size [EquivBEq α] [LawfulHashable α]
     {p : (a : α) → β a → Bool} (h : m.WF) :
     (m.partition p).1.size + (m.partition p).2.size = m.size := by
   simp_to_raw using Raw₀.size_partition
 
 @[simp]
-theorem fst_partition_not_eq_partition_snd [EquivBEq α] [LawfulHashable α]
+theorem fst_partition_not_eq_snd_partition [EquivBEq α] [LawfulHashable α]
     {p : (a : α) → β a → Bool} (h : m.WF) :
     (m.partition (fun a b => ! p a b)).fst = (m.partition p).snd := by
   simp_to_raw
   rw [Raw₀.fst_partition_not_eq_snd_partition]
 
 @[simp]
-theorem snd_partition_not_eq_partition_fst [EquivBEq α] [LawfulHashable α]
+theorem snd_partition_not_eq_fst_partition [EquivBEq α] [LawfulHashable α]
     {p : (a : α) → β a → Bool} (h : m.WF) :
     (m.partition (fun a b => ! p a b)).snd = (m.partition p).fst := by
   simp_to_raw

src/Std/Data/Internal/List/Associative.lean

@@ -2585,6 +2585,18 @@ theorem pairwise_fst_eq_false [BEq α] {l : List ((a : α) × β a)} (h : Distin
   rw [DistinctKeys.def] at h
   assumption
 
+theorem nodup_of_distinctKeys [BEq α] [ReflBEq α] {l : List ((a : α) × β a)} (h : DistinctKeys l) :
+    l.Nodup := by
+  rw [DistinctKeys.def] at h
+  induction l with
+  | nil => simp
+  | cons hd tl ih =>
+    simp only [pairwise_cons, List.nodup_cons] at h ⊢
+    refine And.intro ?_ (ih h.2)
+    intro h'
+    have := h.1 hd h'
+    simp at this
+
 theorem map_fst_map_toProd_eq_keys {β : Type v} {l : List ((_ : α) × β)} :
     List.map Prod.fst (List.map (fun x => (x.fst, x.snd)) l) = List.keys l := by
   induction l with
@@ -2663,7 +2675,6 @@ theorem getValue?_eq_some_iff_exists_beq_and_mem_toList {β : Type v} [BEq α] [
     exists ⟨k', v⟩
     simp only [and_true, getEntry?_congr k_k', h']
 
-
 theorem mem_map_toProd_iff_getKey?_eq_some_and_getValue?_eq_some [BEq α] [EquivBEq α]
     {β : Type v} {k: α} {v : β} {l : List ((_ : α) × β)} (h : DistinctKeys l) :
     (k, v) ∈ l.map (fun x => (x.fst, x.snd)) ↔ getKey? k l = some k ∧ getValue? k l = some v := by
@@ -2677,6 +2688,19 @@ theorem pairwise_fst_eq_false_map_toProd [BEq α] {β : Type v}
   simp [List.pairwise_map]
   assumption
 
+theorem nodup_map_of_distinctKeys [BEq α] [ReflBEq α] {β : Type v} {l : List ((_ : α) × β)} (h : DistinctKeys l) :
+    (l.map (fun x => (x.fst, x.snd))).Nodup := by
+  rw [DistinctKeys.def] at h
+  induction l with
+  | nil => simp
+  | cons hd tl ih =>
+    simp only [pairwise_cons, List.map_cons, List.nodup_cons, List.mem_map, Prod.mk.injEq,
+      not_exists, not_and] at h ⊢
+    refine And.intro ?_ (ih h.2)
+    intro x h' hx₁ _
+    have := h.1 x h'
+    simp [hx₁] at this
+
 theorem foldlM_eq_foldlM_toProd {β : Type v} {δ : Type w} {m' : Type w → Type w'} [Monad m']
     [LawfulMonad m'] {l : List ((_ : α) × β)} {f : δ → (a : α) → β → m' δ} {init : δ} :
     l.foldlM (fun a b => f a b.fst b.snd) init =