chore: remove bif from hash map lemmas (#4791)

The original idea was to use `bif` in computation contexts and `if` in
propositional contexts, but this turned out to be really inconvenient in
practice.

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

@@ -145,7 +145,7 @@ 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} :
-    (m.insert k v).1.size = bif m.contains k then m.1.size else m.1.size + 1 := by
+    (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} :
@@ -169,7 +169,7 @@ theorem contains_of_contains_erase [EquivBEq α] [LawfulHashable α] {k a : α}
   simp_to_model using List.containsKey_of_containsKey_eraseKey
 
 theorem size_erase [EquivBEq α] [LawfulHashable α] {k : α} :
-    (m.erase k).1.size = bif m.contains k then m.1.size - 1 else m.1.size := by
+    (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 : α} :
@@ -215,7 +215,7 @@ theorem get?_eq_none [LawfulBEq α] {a : α} : m.contains a = false → m.get? a
   simp_to_model using List.getValueCast?_eq_none
 
 theorem get?_erase [LawfulBEq α] {k a : α} :
-    (m.erase k).get? a = bif k == a then none else m.get? a := by
+    (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
@@ -234,7 +234,7 @@ theorem get?_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} :
   simp_to_model; empty
 
 theorem get?_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
-    get? (m.insert k v) a = bif k == a then some v else get? m a := by
+    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 : β} :
@@ -250,7 +250,7 @@ theorem get?_eq_none [EquivBEq α] [LawfulHashable α] {a : α} :
   simp_to_model using List.getValue?_eq_none.2
 
 theorem get?_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
-    Const.get? (m.erase k) a = bif k == a then none else get? m a := by
+    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 : α} :
@@ -340,7 +340,7 @@ theorem get!_eq_default [LawfulBEq α] {a : α} [Inhabited (β a)] :
   simp_to_model using List.getValueCast!_eq_default
 
 theorem get!_erase [LawfulBEq α] {k a : α} [Inhabited (β a)] :
-    (m.erase k).get! a = bif k == a then default else m.get! a := by
+    (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)] :
@@ -372,7 +372,7 @@ theorem get!_of_isEmpty [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α
   simp_to_model; empty
 
 theorem get!_insert [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} {v : β} :
-    get! (m.insert k v) a = bif k == a then v else get! m a := by
+    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 : β} :
@@ -384,7 +384,7 @@ theorem get!_eq_default [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α
   simp_to_model using List.getValue!_eq_default
 
 theorem get!_erase [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} :
-    get! (m.erase k) a = bif k == a then default else get! m a := by
+    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 : α} :
@@ -435,7 +435,7 @@ theorem getD_eq_fallback [LawfulBEq α] {a : α} {fallback : β a} :
   simp_to_model using List.getValueCastD_eq_fallback
 
 theorem getD_erase [LawfulBEq α] {k a : α} {fallback : β a} :
-    (m.erase k).getD a fallback = bif k == a then fallback else m.getD a fallback := by
+    (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} :
@@ -471,7 +471,7 @@ theorem getD_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} {fallback : 
   simp_to_model; empty
 
 theorem getD_insert [EquivBEq α] [LawfulHashable α] {k a : α} {fallback v : β} :
-    getD (m.insert k v) a fallback = bif k == a then v else getD m a fallback := by
+    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 : β} :
@@ -483,7 +483,7 @@ theorem getD_eq_fallback [EquivBEq α] [LawfulHashable α] {a : α} {fallback :
   simp_to_model using List.getValueD_eq_fallback
 
 theorem getD_erase [EquivBEq α] [LawfulHashable α] {k a : α} {fallback : β} :
-    getD (m.erase k) a fallback = bif k == a then fallback else getD m a fallback := by
+    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 : β} :
@@ -539,7 +539,7 @@ theorem contains_of_contains_insertIfNew' [EquivBEq α] [LawfulHashable α] {k a
   simp_to_model using List.containsKey_of_containsKey_insertEntryIfNew'
 
 theorem size_insertIfNew [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
-    (m.insertIfNew k v).1.size = bif m.contains k then m.1.size else m.1.size + 1 := by
+    (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} :
@@ -575,7 +575,7 @@ namespace Const
 variable {β : Type v} (m : Raw₀ α (fun _ => β)) (h : m.1.WF)
 
 theorem get?_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
-    get? (m.insertIfNew k v) a = bif k == a && !m.contains k then some v else get? m a := by
+    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₁} :
@@ -585,12 +585,12 @@ theorem get_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} {h
   simp_to_model using List.getValue_insertEntryIfNew
 
 theorem get!_insertIfNew [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} {v : β} :
-    get! (m.insertIfNew k v) a = bif k == a && !m.contains k then v else get! m a := by
+    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 : β} :
     getD (m.insertIfNew k v) a fallback =
-      bif k == a && !m.contains k then v else getD m a fallback := by
+      if k == a ∧ m.contains k = false then v else getD m a fallback := by
   simp_to_model using List.getValueD_insertEntryIfNew
 
 end Const

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

@@ -472,7 +472,8 @@ theorem wfImp_eraseₘaux [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable 
   buckets_hash_self := isHashSelf_eraseₘaux m a h
   size_eq := by
     rw [(toListModel_eraseₘaux m a h).length_eq, eraseₘaux, length_eraseKey,
-      ← containsₘ_eq_containsKey h, h', cond_true, h.size_eq]
+      ← containsₘ_eq_containsKey h, h']
+    simp [h.size_eq]
   distinct := h.distinct.eraseKey.perm (toListModel_eraseₘaux m a h)
 
 theorem toListModel_perm_eraseKey_of_containsₘ_eq_false [BEq α] [Hashable α] [EquivBEq α]

src/Std/Data/DHashMap/Lemmas.lean

@@ -102,7 +102,7 @@ theorem size_emptyc : (∅ : DHashMap α β).size = 0 :=
 theorem isEmpty_eq_size_eq_zero : m.isEmpty = (m.size == 0) := rfl
 
 theorem size_insert [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
-    (m.insert k v).size = bif m.contains k then m.size else m.size + 1 :=
+    (m.insert k v).size = if k ∈ m then m.size else m.size + 1 :=
   Raw₀.size_insert ⟨m.1, _⟩ m.2
 
 theorem size_le_size_insert [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
@@ -140,7 +140,7 @@ theorem mem_of_mem_erase [EquivBEq α] [LawfulHashable α] {k a : α} : a ∈ m.
   simp
 
 theorem size_erase [EquivBEq α] [LawfulHashable α] {k : α} :
-    (m.erase k).size = bif m.contains k then m.size - 1 else m.size :=
+    (m.erase k).size = if k ∈ m then m.size - 1 else m.size :=
   Raw₀.size_erase _ m.2
 
 theorem size_erase_le [EquivBEq α] [LawfulHashable α] {k : α} : (m.erase k).size ≤ m.size :=
@@ -194,7 +194,7 @@ theorem get?_eq_none [LawfulBEq α] {a : α} : ¬a ∈ m → m.get? a = none :=
   simpa [mem_iff_contains] using get?_eq_none_of_contains_eq_false
 
 theorem get?_erase [LawfulBEq α] {k a : α} :
-    (m.erase k).get? a = bif k == a then none else m.get? a :=
+    (m.erase k).get? a = if k == a then none else m.get? a :=
   Raw₀.get?_erase ⟨m.1, _⟩ m.2
 
 @[simp]
@@ -218,7 +218,7 @@ theorem get?_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} :
   Raw₀.Const.get?_of_isEmpty ⟨m.1, _⟩ m.2
 
 theorem get?_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
-    get? (m.insert k v) a = bif k == a then some v else get? m a :=
+    get? (m.insert k v) a = if k == a then some v else get? m a :=
   Raw₀.Const.get?_insert ⟨m.1, _⟩ m.2
 
 @[simp]
@@ -238,7 +238,7 @@ theorem get?_eq_none [EquivBEq α] [LawfulHashable α] {a : α } : ¬a ∈ m →
   simpa [mem_iff_contains] using get?_eq_none_of_contains_eq_false
 
 theorem get?_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
-    Const.get? (m.erase k) a = bif k == a then none else get? m a :=
+    Const.get? (m.erase k) a = if k == a then none else get? m a :=
   Raw₀.Const.get?_erase ⟨m.1, _⟩ m.2
 
 @[simp]
@@ -339,7 +339,7 @@ theorem get!_eq_default [LawfulBEq α] {a : α} [Inhabited (β a)] :
   simpa [mem_iff_contains] using get!_eq_default_of_contains_eq_false
 
 theorem get!_erase [LawfulBEq α] {k a : α} [Inhabited (β a)] :
-    (m.erase k).get! a = bif k == a then default else m.get! a :=
+    (m.erase k).get! a = if k == a then default else m.get! a :=
   Raw₀.get!_erase ⟨m.1, _⟩ m.2
 
 @[simp]
@@ -381,7 +381,7 @@ theorem get!_of_isEmpty [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α
   Raw₀.Const.get!_of_isEmpty ⟨m.1, _⟩ m.2
 
 theorem get!_insert [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} {v : β} :
-    get! (m.insert k v) a = bif k == a then v else get! m a :=
+    get! (m.insert k v) a = if k == a then v else get! m a :=
   Raw₀.Const.get!_insert ⟨m.1, _⟩ m.2
 
 @[simp]
@@ -398,7 +398,7 @@ theorem get!_eq_default [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α
   simpa [mem_iff_contains] using get!_eq_default_of_contains_eq_false
 
 theorem get!_erase [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} :
-    get! (m.erase k) a = bif k == a then default else get! m a :=
+    get! (m.erase k) a = if k == a then default else get! m a :=
   Raw₀.Const.get!_erase ⟨m.1, _⟩ m.2
 
 @[simp]
@@ -465,7 +465,7 @@ theorem getD_eq_fallback [LawfulBEq α] {a : α} {fallback : β a} :
   simpa [mem_iff_contains] using getD_eq_fallback_of_contains_eq_false
 
 theorem getD_erase [LawfulBEq α] {k a : α} {fallback : β a} :
-    (m.erase k).getD a fallback = bif k == a then fallback else m.getD a fallback :=
+    (m.erase k).getD a fallback = if k == a then fallback else m.getD a fallback :=
   Raw₀.getD_erase ⟨m.1, _⟩ m.2
 
 @[simp]
@@ -512,7 +512,7 @@ theorem getD_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} {fallback : 
   Raw₀.Const.getD_of_isEmpty ⟨m.1, _⟩ m.2
 
 theorem getD_insert [EquivBEq α] [LawfulHashable α] {k a : α} {fallback v : β} :
-    getD (m.insert k v) a fallback = bif k == a then v else getD m a fallback :=
+    getD (m.insert k v) a fallback = if k == a then v else getD m a fallback :=
   Raw₀.Const.getD_insert ⟨m.1, _⟩ m.2
 
 @[simp]
@@ -529,7 +529,7 @@ theorem getD_eq_fallback [EquivBEq α] [LawfulHashable α] {a : α} {fallback :
   simpa [mem_iff_contains] using getD_eq_fallback_of_contains_eq_false
 
 theorem getD_erase [EquivBEq α] [LawfulHashable α] {k a : α} {fallback : β} :
-    getD (m.erase k) a fallback = bif k == a then fallback else getD m a fallback :=
+    getD (m.erase k) a fallback = if k == a then fallback else getD m a fallback :=
   Raw₀.Const.getD_erase ⟨m.1, _⟩ m.2
 
 @[simp]
@@ -611,7 +611,7 @@ theorem mem_of_mem_insertIfNew' [EquivBEq α] [LawfulHashable α] {k a : α} {v
   simpa [mem_iff_contains, -contains_insertIfNew] using contains_of_contains_insertIfNew'
 
 theorem size_insertIfNew [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
-    (m.insertIfNew k v).size = bif m.contains k then m.size else m.size + 1 :=
+    (m.insertIfNew k v).size = if k ∈ m then m.size else m.size + 1 :=
   Raw₀.size_insertIfNew ⟨m.1, _⟩ m.2
 
 theorem size_le_size_insertIfNew [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
@@ -647,8 +647,9 @@ namespace Const
 variable {β : Type v} {m : DHashMap α (fun _ => β)}
 
 theorem get?_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
-    get? (m.insertIfNew k v) a = bif k == a && !m.contains k then some v else get? m a :=
-  Raw₀.Const.get?_insertIfNew ⟨m.1, _⟩ m.2
+    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]
+  exact Raw₀.Const.get?_insertIfNew ⟨m.1, _⟩ m.2
 
 theorem get_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} {h₁} :
     get (m.insertIfNew k v) a h₁ =
@@ -657,13 +658,15 @@ theorem get_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} {h
   exact Raw₀.Const.get_insertIfNew ⟨m.1, _⟩ m.2
 
 theorem get!_insertIfNew [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} {v : β} :
-    get! (m.insertIfNew k v) a = bif k == a && !m.contains k then v else get! m a :=
-  Raw₀.Const.get!_insertIfNew ⟨m.1, _⟩ m.2
+    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]
+  exact Raw₀.Const.get!_insertIfNew ⟨m.1, _⟩ m.2
 
 theorem getD_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {fallback v : β} :
     getD (m.insertIfNew k v) a fallback =
-      bif k == a && !m.contains k then v else getD m a fallback :=
-  Raw₀.Const.getD_insertIfNew ⟨m.1, _⟩ m.2
+      if k == a ∧ ¬k ∈ m then v else getD m a fallback := by
+  simp only [mem_iff_contains, Bool.not_eq_true]
+  exact Raw₀.Const.getD_insertIfNew ⟨m.1, _⟩ m.2
 
 end Const