Merge branch 'wojciech/hashmap_beq2' into wojciech/hashmap_deceq

Author: wkrozowski

src/Std/Data/DHashMap/Basic.lean

@@ -362,6 +362,7 @@ instance [BEq α] [Hashable α] : SDiff (DHashMap α β) := ⟨diff⟩
 
 /--
 Compares two hash maps using Boolean equality on keys and values.
+
 Returns `true` if the maps contain the same key-value pairs, `false` otherwise.
 -/
 def beq [LawfulBEq α] [∀ k, BEq (β k)] (a b : DHashMap α β) : Bool :=

src/Std/Data/DHashMap/Raw.lean

@@ -513,25 +513,20 @@ instance [BEq α] [Hashable α] : Inter (Raw α β) := ⟨inter⟩
 
 /--
 Compares two hash maps using Boolean equality on keys and values.
+
 Returns `true` if the maps contain the same key-value pairs, `false` otherwise.
 -/
 def beq [BEq α] [Hashable α] [LawfulBEq α] [∀ k, BEq (β k)] (m₁ m₂ : Raw α β) : Bool :=
-    if h₁ : 0 < m₁.buckets.size then
-      if h₂ : 0 < m₂.buckets.size then
-        Raw₀.beq ⟨m₁, h₁⟩ ⟨m₂, h₂⟩
-      else
-        false
+    if h : 0 < m₁.buckets.size ∧ 0 < m₂.buckets.size then
+      Raw₀.beq ⟨m₁, h.1⟩ ⟨m₂, h.2⟩
     else
       false
 
 instance [BEq α] [Hashable α] [LawfulBEq α] [∀ k, BEq (β k)] : BEq (Raw α β) := ⟨beq⟩
 
 @[inherit_doc DHashMap.Raw.beq] def Const.beq {β : Type v} [BEq α] [Hashable α] [BEq β] (m₁ m₂ : Raw α (fun _ => β)) : Bool :=
-   if h₁ : 0 < m₁.buckets.size then
-      if h₂ : 0 < m₂.buckets.size then
-        Raw₀.Const.beq ⟨m₁, h₁⟩ ⟨m₂, h₂⟩
-      else
-        false
+   if h : 0 < m₁.buckets.size ∧ 0 < m₂.buckets.size then
+        Raw₀.Const.beq ⟨m₁, h.1⟩ ⟨m₂, h.2⟩
     else
       false
 

src/Std/Data/DHashMap/RawLemmas.lean

@@ -3766,11 +3766,13 @@ theorem Equiv.beq [∀ k, ReflBEq (β k)] (h₁ : m₁.WF) (h₂ : m₂.WF) (h :
   simp only [BEq.beq]
   simp_to_raw using Raw₀.Equiv.beq
 
-theorem equiv_of_beq [∀ k, LawfulBEq (β k)] (h₁ : m₁.WF) (h₂ : m₂.WF) (h : beq m₁ m₂ = true) : m₁ ~m m₂ := by
+theorem equiv_of_beq [∀ k, LawfulBEq (β k)] (h₁ : m₁.WF) (h₂ : m₂.WF) (h : m₁ == m₂) : m₁ ~m m₂ := by
   revert h
+  simp only [BEq.beq]
   simp_to_raw using Raw₀.equiv_of_beq
 
-theorem Equiv.beq_congr {m₃ m₄ : Raw α β} (h₁ : m₁.WF) (h₂ : m₂.WF) (h₃ : m₃.WF) (h₄ : m₄.WF) (w₁ : m₁ ~m m₃) (w₂ : m₂ ~m m₄) : Raw.beq m₁ m₂ = Raw.beq m₃ m₄ := by
+theorem Equiv.beq_congr {m₃ m₄ : Raw α β} (h₁ : m₁.WF) (h₂ : m₂.WF) (h₃ : m₃.WF) (h₄ : m₄.WF) (w₁ : m₁ ~m m₃) (w₂ : m₂ ~m m₄) : (m₁ == m₂) = (m₃ == m₄) := by
+  simp only [BEq.beq]
   simp_to_raw using Raw₀.Equiv.beq_congr
 
 end BEq
@@ -3782,7 +3784,7 @@ variable {β : Type v} {m₁ m₂ : Raw α (fun _ => β)}
 theorem Const.Equiv.beq [EquivBEq α] [LawfulHashable α] [BEq β] [ReflBEq β] (h₁ : m₁.WF) (h₂ : m₂.WF) (h : m₁ ~m m₂) : beq m₁ m₂ := by
   simp_to_raw using Raw₀.Const.Equiv.beq
 
-theorem Const.equiv_of_beq [LawfulBEq α] [BEq β] [LawfulBEq β] (h₁ : m₁.WF) (h₂ : m₂.WF) (h : beq m₁ m₂ = true ) : m₁ ~m m₂ := by
+theorem Const.equiv_of_beq [LawfulBEq α] [BEq β] [LawfulBEq β] (h₁ : m₁.WF) (h₂ : m₂.WF) (h : beq m₁ m₂ = true) : m₁ ~m m₂ := by
   revert h
   simp_to_raw using Raw₀.Const.equiv_of_beq
 

src/Std/Data/ExtHashMap/Basic.lean

@@ -256,8 +256,7 @@ instance [EquivBEq α] [LawfulHashable α] [BEq β] [ReflBEq β] : ReflBEq (ExtH
   rfl := ExtDHashMap.Const.beq_of_eq _ _ rfl
 
 instance [LawfulBEq α] [BEq β] [LawfulBEq β] : LawfulBEq (ExtHashMap α β) where
-  eq_of_beq {a} {b} hyp :=
-  by
+  eq_of_beq {a} {b} hyp := by
     have ⟨_⟩ := a
     have ⟨_⟩ := b
     simp only [mk.injEq] at |- hyp

src/Std/Data/ExtHashSet/Basic.lean

@@ -211,7 +211,7 @@ instance [EquivBEq α] [LawfulHashable α] : ReflBEq (ExtHashSet α) where
   rfl := ExtDHashMap.Const.beq_of_eq _ _ rfl
 
 instance [LawfulBEq α] : LawfulBEq (ExtHashSet α) where
-  eq_of_beq {a} {b} hyp  := by
+  eq_of_beq {a} {b} hyp := by
     have ⟨⟨_⟩⟩ := a
     have ⟨⟨_⟩⟩ := b
     simp only [mk.injEq, ExtHashMap.mk.injEq] at |- hyp

src/Std/Data/HashSet/Basic.lean

@@ -262,7 +262,8 @@ instance [BEq α] [Hashable α] : Inter (HashSet α) := ⟨inter⟩
 
 /--
 Compares two hash sets using Boolean equality on keys.
-Returns `true` if the sets contain the same keys pairs, `false` otherwise.
+
+Returns `true` if the sets contain the same keys, `false` otherwise.
 -/
 def beq [BEq α] (m₁ m₂ : HashSet α) : Bool :=
   HashMap.beq m₁.inner m₂.inner

src/Std/Data/HashSet/Raw.lean

@@ -246,7 +246,8 @@ instance [BEq α] [Hashable α] : Inter (Raw α) := ⟨inter⟩
 
 /--
 Compares two hash sets using Boolean equality on keys.
-Returns `true` if the sets contain the same keys pairs, `false` otherwise.
+
+Returns `true` if the sets contain the same keys, `false` otherwise.
 -/
 def beq [BEq α] [Hashable α] (m₁ m₂ : Raw α) : Bool :=
   HashMap.Raw.beq m₁.inner m₂.inner

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

@@ -3589,12 +3589,9 @@ theorem length_le_length_of_containsKey [BEq α] [EquivBEq α]
     have hc := h hd.1 (by rw [containsKey_cons_self])
     suffices tl.length ≤ (eraseKey hd.1 l₂).length by
       rw [List.length_eraseKey, hc] at this
-      simp at this
-      simp
-      have : l₂.length > 0 := by
-        cases l₂
-        case nil => simp at hc
-        case cons => simp
+      simp only [↓reduceIte] at this
+      simp only [List.length_cons, ge_iff_le]
+      have : l₂.length > 0 := by cases l₂ <;> simp_all
       omega
     apply ih
     · rw [List.distinctKeys_cons_iff] at dl₁
@@ -3621,7 +3618,7 @@ theorem containsKey_of_length_eq [BEq α] [EquivBEq α] {l₁ l₂ : List ((a :
   intro a ha
   apply Classical.byContradiction
   intro hb
-  simp at hb
+  simp only [Bool.not_eq_true] at hb
   suffices l₁.length < l₂.length by omega
   suffices l₁.length ≤ (eraseKey a l₂).length ∧ 1 + (eraseKey a l₂).length = l₂.length by omega
   apply And.intro
@@ -3640,9 +3637,9 @@ theorem containsKey_of_length_eq [BEq α] [EquivBEq α] {l₁ l₂ : List ((a :
       exact mem₂
   · simp only [length_eraseKey, ha, ↓reduceIte]
     have : l₂.length > 0 := by
-      cases l₂
-      · simp at ha
-      · simp
+      cases l₂ with
+      | nil => simp at ha
+      | _ => simp
     omega
 
 section
@@ -7633,7 +7630,7 @@ theorem isEmpty_filter_key_iff [BEq α] [EquivBEq α] {f : α → Bool}
     simp only [getKey, getKey?_eq_getEntry?, this] at h
     exact h
 
-theorem beqModel_eq_true_of_perm [BEq α] [LawfulBEq α] [LawfulBEq α] [∀ k, BEq (β k)] [∀ k, ReflBEq (β k)] {l₁ l₂ : List ((a : α) × β a)} (hl₁ : DistinctKeys l₁) : l₁.Perm l₂ → beqModel l₁ l₂ := by
+theorem beqModel_eq_true_of_perm [BEq α] [LawfulBEq α] [∀ k, BEq (β k)] [∀ k, ReflBEq (β k)] {l₁ l₂ : List ((a : α) × β a)} (hl₁ : DistinctKeys l₁) : l₁.Perm l₂ → beqModel l₁ l₂ := by
   intro hyp
   rw [beqModel, if_neg (by simpa using hyp.length_eq)]
   simp only [List.all_eq_true]