From 47b353f1552f41db13014e0ec7ac8016dbab9595 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 2 Jun 2025 22:50:21 +1000 Subject: [PATCH] chore: adjust HashMap grind lemmas (#8587) This PR adjusts the grind annotation on `Std.HashMap.map_fst_toList_eq_keys` and variants, so `grind` can reason bidirectionally between `m.keys` and `m.toList`. --- src/Std/Data/DHashMap/Lemmas.lean | 4 ++-- src/Std/Data/DHashMap/RawLemmas.lean | 4 ++-- src/Std/Data/DTreeMap/Lemmas.lean | 4 ++-- src/Std/Data/DTreeMap/Raw/Lemmas.lean | 4 ++-- src/Std/Data/HashMap/Lemmas.lean | 2 +- src/Std/Data/HashMap/RawLemmas.lean | 2 +- src/Std/Data/TreeMap/Lemmas.lean | 2 +- src/Std/Data/TreeMap/Raw/Lemmas.lean | 2 +- 8 files changed, 12 insertions(+), 12 deletions(-) diff --git a/src/Std/Data/DHashMap/Lemmas.lean b/src/Std/Data/DHashMap/Lemmas.lean index 42863c4851..db18814426 100644 --- a/src/Std/Data/DHashMap/Lemmas.lean +++ b/src/Std/Data/DHashMap/Lemmas.lean @@ -1158,7 +1158,7 @@ theorem distinct_keys [EquivBEq α] [LawfulHashable α] : m.keys.Pairwise (fun a b => (a == b) = false) := Raw₀.distinct_keys ⟨m.1, m.2.size_buckets_pos⟩ m.2 -@[simp, grind =] +@[simp, grind _=_] theorem map_fst_toList_eq_keys [EquivBEq α] [LawfulHashable α] : m.toList.map Sigma.fst = m.keys := Raw₀.map_fst_toList_eq_keys ⟨m.1, m.2.size_buckets_pos⟩ @@ -1209,7 +1209,7 @@ namespace Const variable {β : Type v} {m : DHashMap α (fun _ => β)} -@[simp, grind =] +@[simp, grind _=_] theorem map_fst_toList_eq_keys [EquivBEq α] [LawfulHashable α] : (toList m).map Prod.fst = m.keys := Raw₀.Const.map_fst_toList_eq_keys ⟨m.1, m.2.size_buckets_pos⟩ diff --git a/src/Std/Data/DHashMap/RawLemmas.lean b/src/Std/Data/DHashMap/RawLemmas.lean index 409eca9416..0dbaa1898f 100644 --- a/src/Std/Data/DHashMap/RawLemmas.lean +++ b/src/Std/Data/DHashMap/RawLemmas.lean @@ -1226,7 +1226,7 @@ theorem distinct_keys [EquivBEq α] [LawfulHashable α] (h : m.WF) : m.keys.Pairwise (fun a b => (a == b) = false) := by simp_to_raw using Raw₀.distinct_keys ⟨m, h.size_buckets_pos⟩ h -@[simp, grind =] +@[simp, grind _=_] theorem map_fst_toList_eq_keys [EquivBEq α] [LawfulHashable α] (h : m.WF) : m.toList.map Sigma.fst = m.keys := by apply Raw₀.map_fst_toList_eq_keys ⟨m, h.size_buckets_pos⟩ @@ -1277,7 +1277,7 @@ namespace Const variable {β : Type v} {m : Raw α (fun _ => β)} -@[simp, grind =] +@[simp, grind _=_] theorem map_fst_toList_eq_keys [EquivBEq α] [LawfulHashable α] (h : m.WF) : (Raw.Const.toList m).map Prod.fst = m.keys := by apply Raw₀.Const.map_fst_toList_eq_keys ⟨m, h.size_buckets_pos⟩ diff --git a/src/Std/Data/DTreeMap/Lemmas.lean b/src/Std/Data/DTreeMap/Lemmas.lean index 3985d60ef2..437c0706fd 100644 --- a/src/Std/Data/DTreeMap/Lemmas.lean +++ b/src/Std/Data/DTreeMap/Lemmas.lean @@ -1053,7 +1053,7 @@ theorem ordered_keys [TransCmp cmp] : t.keys.Pairwise (fun a b => cmp a b = .lt) := Impl.ordered_keys t.wf -@[simp, grind =] +@[simp, grind _=_] theorem map_fst_toList_eq_keys : t.toList.map Sigma.fst = t.keys := Impl.map_fst_toList_eq_keys @@ -1098,7 +1098,7 @@ namespace Const variable {β : Type v} {t : DTreeMap α β cmp} -@[simp, grind =] +@[simp, grind _=_] theorem map_fst_toList_eq_keys : (toList t).map Prod.fst = t.keys := Impl.Const.map_fst_toList_eq_keys diff --git a/src/Std/Data/DTreeMap/Raw/Lemmas.lean b/src/Std/Data/DTreeMap/Raw/Lemmas.lean index 476479e914..3ae6ded976 100644 --- a/src/Std/Data/DTreeMap/Raw/Lemmas.lean +++ b/src/Std/Data/DTreeMap/Raw/Lemmas.lean @@ -1063,7 +1063,7 @@ theorem ordered_keys [TransCmp cmp] (h : t.WF) : t.keys.Pairwise (fun a b => cmp a b = .lt) := Impl.ordered_keys h.out -@[simp, grind =] +@[simp, grind _=_] theorem map_fst_toList_eq_keys : t.toList.map Sigma.fst = t.keys := Impl.map_fst_toList_eq_keys @@ -1108,7 +1108,7 @@ namespace Const variable {β : Type v} {t : Raw α β cmp} -@[simp, grind =] +@[simp, grind _=_] theorem map_fst_toList_eq_keys : (toList t).map Prod.fst = t.keys := Impl.Const.map_fst_toList_eq_keys diff --git a/src/Std/Data/HashMap/Lemmas.lean b/src/Std/Data/HashMap/Lemmas.lean index 362908c8e1..cf3181ac41 100644 --- a/src/Std/Data/HashMap/Lemmas.lean +++ b/src/Std/Data/HashMap/Lemmas.lean @@ -854,7 +854,7 @@ theorem distinct_keys [EquivBEq α] [LawfulHashable α] : m.keys.Pairwise (fun a b => (a == b) = false) := DHashMap.distinct_keys -@[simp, grind =] +@[simp, grind _=_] theorem map_fst_toList_eq_keys [EquivBEq α] [LawfulHashable α] : m.toList.map Prod.fst = m.keys := DHashMap.Const.map_fst_toList_eq_keys diff --git a/src/Std/Data/HashMap/RawLemmas.lean b/src/Std/Data/HashMap/RawLemmas.lean index d1bf4fde70..b3c9982693 100644 --- a/src/Std/Data/HashMap/RawLemmas.lean +++ b/src/Std/Data/HashMap/RawLemmas.lean @@ -869,7 +869,7 @@ theorem distinct_keys [EquivBEq α] [LawfulHashable α] (h : m.WF) : m.keys.Pairwise (fun a b => (a == b) = false) := DHashMap.Raw.distinct_keys h.out -@[simp, grind =] +@[simp, grind _=_] theorem map_fst_toList_eq_keys [EquivBEq α] [LawfulHashable α] (h : m.WF) : m.toList.map Prod.fst = m.keys := DHashMap.Raw.Const.map_fst_toList_eq_keys h.out diff --git a/src/Std/Data/TreeMap/Lemmas.lean b/src/Std/Data/TreeMap/Lemmas.lean index d4bf09c83f..d22642c5ec 100644 --- a/src/Std/Data/TreeMap/Lemmas.lean +++ b/src/Std/Data/TreeMap/Lemmas.lean @@ -795,7 +795,7 @@ theorem ordered_keys [TransCmp cmp] : t.keys.Pairwise (fun a b => cmp a b = .lt) := DTreeMap.ordered_keys -@[simp, grind =] +@[simp, grind _=_] theorem map_fst_toList_eq_keys : (toList t).map Prod.fst = t.keys := DTreeMap.Const.map_fst_toList_eq_keys diff --git a/src/Std/Data/TreeMap/Raw/Lemmas.lean b/src/Std/Data/TreeMap/Raw/Lemmas.lean index 39135b71b4..8be9824ed6 100644 --- a/src/Std/Data/TreeMap/Raw/Lemmas.lean +++ b/src/Std/Data/TreeMap/Raw/Lemmas.lean @@ -789,7 +789,7 @@ theorem ordered_keys [TransCmp cmp] (h : t.WF) : t.keys.Pairwise (fun a b => cmp a b = .lt) := DTreeMap.Raw.ordered_keys h -@[simp, grind =] +@[simp, grind _=_] theorem map_fst_toList_eq_keys : (toList t).map Prod.fst = t.keys := DTreeMap.Raw.Const.map_fst_toList_eq_keys