chore: missing grind modifiers and local grind theorems configuration

This PR makes explicit missing `grind` modifiers, and ensures `grind` uses
"minIndexable" for local theorems.

src/Init/Control/Lawful/Basic.lean

@@ -147,7 +147,7 @@ class LawfulMonad (m : Type u → Type v) [Monad m] : Prop extends LawfulApplica
 
 export LawfulMonad (bind_pure_comp bind_map pure_bind bind_assoc)
 attribute [simp] pure_bind bind_assoc bind_pure_comp
-attribute [grind] pure_bind
+attribute [grind <=] pure_bind
 
 @[simp] theorem bind_pure [Monad m] [LawfulMonad m] (x : m α) : x >>= pure = x := by
   change x >>= (fun a => pure (id a)) = x

src/Init/Data/Array/Attach.lean

@@ -194,7 +194,7 @@ theorem attachWith_map_subtype_val {p : α → Prop} {xs : Array α} (H : ∀ a
     (xs.attachWith p H).map Subtype.val = xs := by
   cases xs; simp
 
-@[simp, grind]
+@[simp, grind ←]
 theorem mem_attach (xs : Array α) : ∀ x, x ∈ xs.attach
   | ⟨a, h⟩ => by
     have := mem_map.1 (by rw [attach_map_subtype_val] <;> exact h)

src/Init/Data/Array/Lemmas.lean

@@ -1474,7 +1474,7 @@ theorem forall_mem_filter {p : α → Bool} {xs : Array α} {P : α → Prop} :
     (∀ (i) (_ : i ∈ xs.filter p), P i) ↔ ∀ (j) (_ : j ∈ xs), p j → P j := by
   simp
 
-@[grind] theorem getElem_filter {xs : Array α} {p : α → Bool} {i : Nat} (h : i < (xs.filter p).size) :
+@[grind ←] theorem getElem_filter {xs : Array α} {p : α → Bool} {i : Nat} (h : i < (xs.filter p).size) :
     p (xs.filter p)[i] :=
   (mem_filter.mp (getElem_mem h)).2
 
@@ -3251,7 +3251,7 @@ rather than `(arr.push a).size` as the argument.
   simp [← foldrM_push, h]
 
 -- TODO: a multi-pattern is being selected there because E-matching does not go inside lambdas.
-@[simp, grind] theorem _root_.List.foldrM_push_eq_append [Monad m] [LawfulMonad m] {l : List α} {f : α → m β} {xs : Array β} :
+@[simp, grind! ←] theorem _root_.List.foldrM_push_eq_append [Monad m] [LawfulMonad m] {l : List α} {f : α → m β} {xs : Array β} :
     l.foldrM (fun x xs => xs.push <$> f x) xs = do return xs ++ (← l.reverse.mapM f).toArray := by
   induction l with
   | nil => simp
@@ -3264,7 +3264,7 @@ rather than `(arr.push a).size` as the argument.
     simp
 
 -- TODO: a multi-pattern is being selected there because E-matching does not go inside lambdas.
-@[simp, grind] theorem _root_.List.foldlM_push_eq_append [Monad m] [LawfulMonad m] {l : List α} {f : α → m β} {xs : Array β} :
+@[simp, grind! ←] theorem _root_.List.foldlM_push_eq_append [Monad m] [LawfulMonad m] {l : List α} {f : α → m β} {xs : Array β} :
     l.foldlM (fun xs x => xs.push <$> f x) xs = do return xs ++ (← l.mapM f).toArray := by
   induction l generalizing xs <;> simp [*]
 
@@ -3338,7 +3338,7 @@ rather than `(arr.push a).size` as the argument.
   foldrM_push' h
 
 -- TODO: a multi-pattern is being selected there because E-matching does not go inside lambdas.
-@[simp, grind] theorem foldl_push_eq_append {as : Array α} {bs : Array β} {f : α → β} (w : stop = as.size) :
+@[simp, grind! ←] theorem foldl_push_eq_append {as : Array α} {bs : Array β} {f : α → β} (w : stop = as.size) :
     as.foldl (fun acc a => acc.push (f a)) bs 0 stop = bs ++ as.map f := by
   subst w
   rcases as with ⟨as⟩
@@ -3347,14 +3347,14 @@ rather than `(arr.push a).size` as the argument.
   induction as generalizing bs <;> simp [*]
 
 -- TODO: a multi-pattern is being selected there because E-matching does not go inside lambdas.
-@[simp, grind] theorem foldl_cons_eq_append {as : Array α} {bs : List β} {f : α → β} (w : stop = as.size) :
+@[simp, grind! ←] theorem foldl_cons_eq_append {as : Array α} {bs : List β} {f : α → β} (w : stop = as.size) :
     as.foldl (fun acc a => (f a) :: acc) bs 0 stop = (as.map f).reverse.toList ++ bs := by
   subst w
   rcases as with ⟨as⟩
   simp
 
 -- TODO: a multi-pattern is being selected there because E-matching does not go inside lambdas.
-@[simp, grind] theorem foldr_cons_eq_append {as : Array α} {bs : List β} {f : α → β} (w : start = as.size) :
+@[simp, grind! ←] theorem foldr_cons_eq_append {as : Array α} {bs : List β} {f : α → β} (w : start = as.size) :
     as.foldr (fun a acc => (f a) :: acc) bs start 0 = (as.map f).toList ++ bs := by
   subst w
   rcases as with ⟨as⟩
@@ -3368,7 +3368,7 @@ rather than `(arr.push a).size` as the argument.
   simp
 
 -- TODO: a multi-pattern is being selected there because E-matching does not go inside lambdas.
-@[simp, grind] theorem _root_.List.foldr_push_eq_append {l : List α} {f : α → β} {xs : Array β} :
+@[simp, grind! ←] theorem _root_.List.foldr_push_eq_append {l : List α} {f : α → β} {xs : Array β} :
     l.foldr (fun x xs => xs.push (f x)) xs = xs ++ (l.reverse.map f).toArray := by
   induction l <;> simp [*]
 
@@ -3378,7 +3378,7 @@ rather than `(arr.push a).size` as the argument.
   induction l <;> simp [*]
 
 -- TODO: a multi-pattern is being selected there because E-matching does not go inside lambdas.
-@[simp, grind] theorem _root_.List.foldl_push_eq_append {l : List α} {f : α → β} {xs : Array β} :
+@[simp, grind! ←] theorem _root_.List.foldl_push_eq_append {l : List α} {f : α → β} {xs : Array β} :
     l.foldl (fun xs x => xs.push (f x)) xs = xs ++ (l.map f).toArray := by
   induction l generalizing xs <;> simp [*]
 
@@ -3396,28 +3396,28 @@ theorem _root_.List.foldr_push {l : List α} {as : Array α} : l.foldr (fun a bs
   rw [List.foldr_eq_foldl_reverse, List.foldl_push_eq_append']
 
 -- TODO: a multi-pattern is being selected there because E-matching does not go inside lambdas.
-@[simp, grind] theorem foldr_append_eq_append {xs : Array α} {f : α → Array β} {ys : Array β} :
+@[simp, grind! ←] theorem foldr_append_eq_append {xs : Array α} {f : α → Array β} {ys : Array β} :
     xs.foldr (f · ++ ·) ys = (xs.map f).flatten ++ ys := by
   rcases xs with ⟨xs⟩
   rcases ys with ⟨ys⟩
   induction xs <;> simp_all [Function.comp_def, flatten_toArray]
 
 -- TODO: a multi-pattern is being selected there because E-matching does not go inside lambdas.
-@[simp, grind] theorem foldl_append_eq_append {xs : Array α} {f : α → Array β} {ys : Array β} :
+@[simp, grind! ←] theorem foldl_append_eq_append {xs : Array α} {f : α → Array β} {ys : Array β} :
     xs.foldl (· ++ f ·) ys = ys ++ (xs.map f).flatten := by
   rcases xs with ⟨xs⟩
   rcases ys with ⟨ys⟩
   induction xs generalizing ys <;> simp_all [Function.comp_def, flatten_toArray]
 
 -- TODO: a multi-pattern is being selected there because E-matching does not go inside lambdas.
-@[simp, grind] theorem foldr_flip_append_eq_append {xs : Array α} {f : α → Array β} {ys : Array β} :
+@[simp, grind! ←] theorem foldr_flip_append_eq_append {xs : Array α} {f : α → Array β} {ys : Array β} :
     xs.foldr (fun x acc => acc ++ f x) ys = ys ++ (xs.map f).reverse.flatten := by
   rcases xs with ⟨xs⟩
   rcases ys with ⟨ys⟩
   induction xs generalizing ys <;> simp_all [Function.comp_def, flatten_toArray]
 
 -- TODO: a multi-pattern is being selected there because E-matching does not go inside lambdas.
-@[simp, grind] theorem foldl_flip_append_eq_append {xs : Array α} {f : α → Array β} {ys : Array β} :
+@[simp, grind! ←] theorem foldl_flip_append_eq_append {xs : Array α} {f : α → Array β} {ys : Array β} :
     xs.foldl (fun acc y => f y ++ acc) ys = (xs.map f).reverse.flatten ++ ys:= by
   rcases xs with ⟨l⟩
   rcases ys with ⟨l'⟩

src/Init/Data/List/Attach.lean

@@ -167,7 +167,7 @@ theorem attachWith_map_subtype_val {p : α → Prop} {l : List α} (H : ∀ a
     (l.attachWith p H).map Subtype.val = l :=
   (attachWith_map_val _).trans (List.map_id _)
 
-@[simp, grind]
+@[simp, grind ←]
 theorem mem_attach (l : List α) : ∀ x, x ∈ l.attach
   | ⟨a, h⟩ => by
     have := mem_map.1 (by rw [attach_map_subtype_val]; exact h)

src/Init/Data/List/Lemmas.lean

@@ -28,14 +28,14 @@ For each `List` operation, we would like theorems describing the following, when
 * the length of the result `(f L).length`
 * the `i`-th element, described via `(f L)[i]` and/or `(f L)[i]?` (these should typically be `@[simp]`)
 * consequences for `f L` of the fact `x ∈ L` or `x ∉ L`
-* conditions characterising `x ∈ f L` (often but not always `@[simp]`)
+* conditions characterizing `x ∈ f L` (often but not always `@[simp]`)
 * injectivity statements, or congruence statements of the form `p L M → f L = f M`.
-* conditions characterising the result, i.e. of the form `f L = M ↔ p M` for some predicate `p`,
+* conditions characterizing the result, i.e. of the form `f L = M ↔ p M` for some predicate `p`,
   along with special cases of `M` (e.g. `List.append_eq_nil : L ++ M = [] ↔ L = [] ∧ M = []`)
-* negative characterisations are also useful, e.g. `List.cons_ne_nil`
+* negative characterizations are also useful, e.g. `List.cons_ne_nil`
 * interactions with all previously described `List` operations where possible
   (some of these should be `@[simp]`, particularly if the result can be described by a single operation)
-* characterising `(∀ (i) (_ : i ∈ f L), P i)`, for some predicate `P`
+* characterizing `(∀ (i) (_ : i ∈ f L), P i)`, for some predicate `P`
 
 Of course for any individual operation, not all of these will be relevant or helpful, so some judgement is required.
 

src/Init/Data/List/Sublist.lean

@@ -151,11 +151,11 @@ theorem subset_replicate {n : Nat} {a : α} {l : List α} (h : n ≠ 0) : l ⊆
 
 /-! ### Sublist and isSublist -/
 
-@[simp, grind] theorem nil_sublist : ∀ l : List α, [] <+ l
+@[simp, grind ←] theorem nil_sublist : ∀ l : List α, [] <+ l
   | [] => .slnil
   | a :: l => (nil_sublist l).cons a
 
-@[simp, grind] theorem Sublist.refl : ∀ l : List α, l <+ l
+@[simp, grind ←] theorem Sublist.refl : ∀ l : List α, l <+ l
   | [] => .slnil
   | a :: l => (Sublist.refl l).cons₂ a
 
@@ -172,7 +172,7 @@ theorem Sublist.trans {l₁ l₂ l₃ : List α} (h₁ : l₁ <+ l₂) (h₂ : l
 
 instance : Trans (@Sublist α) Sublist Sublist := ⟨Sublist.trans⟩
 
-attribute [simp, grind] Sublist.cons
+attribute [simp, grind ←] Sublist.cons
 
 theorem sublist_cons_self (a : α) (l : List α) : l <+ a :: l := (Sublist.refl l).cons _
 
@@ -664,20 +664,20 @@ theorem IsSuffix.isInfix : l₁ <:+ l₂ → l₁ <:+: l₂ := fun ⟨t, h⟩ =>
 
 grind_pattern IsSuffix.isInfix => l₁ <:+ l₂, IsInfix
 
-@[simp, grind] theorem nil_prefix {l : List α} : [] <+: l := ⟨l, rfl⟩
+@[simp, grind ←] theorem nil_prefix {l : List α} : [] <+: l := ⟨l, rfl⟩
 
-@[simp, grind] theorem nil_suffix {l : List α} : [] <:+ l := ⟨l, append_nil _⟩
+@[simp, grind ←] theorem nil_suffix {l : List α} : [] <:+ l := ⟨l, append_nil _⟩
 
-@[simp, grind] theorem nil_infix {l : List α} : [] <:+: l := nil_prefix.isInfix
+@[simp, grind ←] theorem nil_infix {l : List α} : [] <:+: l := nil_prefix.isInfix
 
 theorem prefix_refl (l : List α) : l <+: l := ⟨[], append_nil _⟩
-@[simp, grind] theorem prefix_rfl {l : List α} : l <+: l := prefix_refl l
+@[simp, grind ←] theorem prefix_rfl {l : List α} : l <+: l := prefix_refl l
 
 theorem suffix_refl (l : List α) : l <:+ l := ⟨[], rfl⟩
-@[simp, grind] theorem suffix_rfl {l : List α} : l <:+ l := suffix_refl l
+@[simp, grind ←] theorem suffix_rfl {l : List α} : l <:+ l := suffix_refl l
 
 theorem infix_refl (l : List α) : l <:+: l := prefix_rfl.isInfix
-@[simp, grind] theorem infix_rfl {l : List α} : l <:+: l := infix_refl l
+@[simp, grind ←] theorem infix_rfl {l : List α} : l <:+: l := infix_refl l
 
 @[simp] theorem suffix_cons (a : α) : ∀ l, l <:+ a :: l := suffix_append [a]
 

src/Init/Data/Option/Lemmas.lean

@@ -52,7 +52,7 @@ theorem get_of_mem : ∀ {o : Option α} (h : isSome o), a ∈ o → o.get h = a
 theorem get_of_eq_some : ∀ {o : Option α} (h : isSome o), o = some a → o.get h = a
   | _, _, rfl => rfl
 
-@[simp, grind] theorem not_mem_none (a : α) : a ∉ (none : Option α) := nofun
+@[simp, grind ←] theorem not_mem_none (a : α) : a ∉ (none : Option α) := nofun
 
 theorem getD_of_ne_none {x : Option α} (hx : x ≠ none) (y : α) : some (x.getD y) = x := by
   cases x; {contradiction}; rw [getD_some]

src/Init/Data/Option/List.lean

@@ -43,7 +43,7 @@ namespace Option
     o.toList.foldr f a = o.elim a (fun b => f b a) := by
   cases o <;> simp
 
-@[simp, grind]
+@[simp, grind ←]
 theorem pairwise_toList {P : α → α → Prop} {o : Option α} : o.toList.Pairwise P := by
   cases o <;> simp
 

src/Init/Data/Sum/Basic.lean

@@ -142,9 +142,9 @@ inductive LiftRel (r : α → γ → Prop) (s : β → δ → Prop) : α ⊕ β
 @[simp, grind =] theorem liftRel_inl_inl : LiftRel r s (inl a) (inl c) ↔ r a c :=
   ⟨fun h => by cases h; assumption, LiftRel.inl⟩
 
-@[simp, grind] theorem not_liftRel_inl_inr : ¬LiftRel r s (inl a) (inr d) := nofun
+@[simp, grind ←] theorem not_liftRel_inl_inr : ¬LiftRel r s (inl a) (inr d) := nofun
 
-@[simp, grind] theorem not_liftRel_inr_inl : ¬LiftRel r s (inr b) (inl c) := nofun
+@[simp, grind ←] theorem not_liftRel_inr_inl : ¬LiftRel r s (inr b) (inl c) := nofun
 
 @[simp, grind =] theorem liftRel_inr_inr : LiftRel r s (inr b) (inr d) ↔ s b d :=
   ⟨fun h => by cases h; assumption, LiftRel.inr⟩
@@ -179,7 +179,7 @@ attribute [simp] Lex.sep
 @[simp, grind =] theorem lex_inr_inr : Lex r s (inr b₁) (inr b₂) ↔ s b₁ b₂ :=
   ⟨fun h => by cases h; assumption, Lex.inr⟩
 
-@[simp, grind] theorem lex_inr_inl : ¬Lex r s (inr b) (inl a) := nofun
+@[simp, grind ←] theorem lex_inr_inl : ¬Lex r s (inr b) (inl a) := nofun
 
 instance instDecidableRelSumLex [DecidableRel r] [DecidableRel s] : DecidableRel (Lex r s)
   | inl _, inl _ => decidable_of_iff' _ lex_inl_inl

src/Lean/Meta/Tactic/Grind/ForallProp.lean

@@ -63,7 +63,9 @@ private def isEqTrueHyp? (proof : Expr) : Option FVarId := Id.run do
 /-- Similar to `mkEMatchTheoremWithKind?`, but swallow any exceptions. -/
 private def mkEMatchTheoremWithKind'? (origin : Origin) (proof : Expr) (kind : EMatchTheoremKind) (prios : SymbolPriorities) : MetaM (Option EMatchTheorem) := do
   try
-    mkEMatchTheoremWithKind? origin #[] proof kind prios (groundPatterns := false)
+    -- **Note**: for local theorems, we want to use very general patterns, this is why we set `minIndexable := true`
+    -- The same approach is used in Z3.
+    mkEMatchTheoremWithKind? origin #[] proof kind prios (groundPatterns := false) (minIndexable := true)
   catch _ =>
     return none
 

src/Std/Data/DHashMap/Lemmas.lean

@@ -75,7 +75,7 @@ theorem mem_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a == b) :
 theorem contains_emptyWithCapacity {a : α} {c} : (emptyWithCapacity c : DHashMap α β).contains a = false :=
   Raw₀.contains_emptyWithCapacity
 
-@[simp, grind] theorem not_mem_emptyWithCapacity {a : α} {c} : ¬a ∈ (emptyWithCapacity c : DHashMap α β) := by
+@[simp, grind ←] theorem not_mem_emptyWithCapacity {a : α} {c} : ¬a ∈ (emptyWithCapacity c : DHashMap α β) := by
   simp [← contains_iff_mem]
 
 @[simp, grind =] theorem contains_empty {a : α} : (∅ : DHashMap α β).contains a = false :=

src/Std/Data/DHashMap/RawLemmas.lean

@@ -123,7 +123,7 @@ theorem mem_congr [EquivBEq α] [LawfulHashable α] (h : m.WF) {a b : α} (hab :
 @[simp, grind =] theorem contains_emptyWithCapacity {a : α} {c} : (emptyWithCapacity c : Raw α β).contains a = false := by
   simp_to_raw using Raw₀.contains_emptyWithCapacity
 
-@[simp, grind] theorem not_mem_emptyWithCapacity {a : α} {c} : ¬a ∈ (emptyWithCapacity c : Raw α β) := by
+@[simp, grind ←] theorem not_mem_emptyWithCapacity {a : α} {c} : ¬a ∈ (emptyWithCapacity c : Raw α β) := by
   simp [← contains_iff_mem]
 
 @[simp, grind =] theorem contains_empty {a : α} : (∅ : Raw α β).contains a = false :=

src/Std/Data/HashMap/Lemmas.lean

@@ -73,7 +73,7 @@ theorem mem_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a == b) :
 theorem contains_emptyWithCapacity {a : α} {c} : (emptyWithCapacity c : HashMap α β).contains a = false :=
   DHashMap.contains_emptyWithCapacity
 
-@[simp, grind] theorem not_mem_emptyWithCapacity {a : α} {c} : ¬a ∈ (emptyWithCapacity c : HashMap α β) :=
+@[simp, grind ←] theorem not_mem_emptyWithCapacity {a : α} {c} : ¬a ∈ (emptyWithCapacity c : HashMap α β) :=
   DHashMap.not_mem_emptyWithCapacity
 
 @[simp, grind =] theorem contains_empty {a : α} : (∅ : HashMap α β).contains a = false :=

src/Std/Data/HashMap/RawLemmas.lean

@@ -89,7 +89,7 @@ theorem mem_congr [EquivBEq α] [LawfulHashable α] (h : m.WF) {a b : α} (hab :
 theorem contains_emptyWithCapacity {a : α} {c} : (emptyWithCapacity c : Raw α β).contains a = false :=
   DHashMap.Raw.contains_emptyWithCapacity
 
-@[simp, grind] theorem not_mem_emptyWithCapacity {a : α} {c} : ¬a ∈ (emptyWithCapacity c : Raw α β) :=
+@[simp, grind ←] theorem not_mem_emptyWithCapacity {a : α} {c} : ¬a ∈ (emptyWithCapacity c : Raw α β) :=
   DHashMap.Raw.not_mem_emptyWithCapacity
 
 @[simp, grind =] theorem contains_empty {a : α} : (∅ : Raw α β).contains a = false :=

src/Std/Data/HashSet/Lemmas.lean

@@ -69,7 +69,7 @@ theorem mem_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a == b) :
 theorem contains_emptyWithCapacity {a : α} {c} : (emptyWithCapacity c : HashSet α).contains a = false :=
   HashMap.contains_emptyWithCapacity
 
-@[simp, grind] theorem not_mem_emptyWithCapacity {a : α} {c} : ¬a ∈ (emptyWithCapacity c : HashSet α) :=
+@[simp, grind ←] theorem not_mem_emptyWithCapacity {a : α} {c} : ¬a ∈ (emptyWithCapacity c : HashSet α) :=
   HashMap.not_mem_emptyWithCapacity
 
 @[simp, grind =] theorem contains_empty {a : α} : (∅ : HashSet α).contains a = false :=

src/Std/Data/HashSet/RawLemmas.lean

@@ -87,7 +87,7 @@ theorem mem_congr [EquivBEq α] [LawfulHashable α] (h : m.WF) {a b : α} (hab :
 @[simp, grind =] theorem contains_emptyWithCapacity {a : α} {c} : (emptyWithCapacity c : Raw α).contains a = false :=
   HashMap.Raw.contains_emptyWithCapacity
 
-@[simp, grind] theorem not_mem_emptyWithCapacity {a : α} {c} : ¬a ∈ (emptyWithCapacity c : Raw α) :=
+@[simp, grind ←] theorem not_mem_emptyWithCapacity {a : α} {c} : ¬a ∈ (emptyWithCapacity c : Raw α) :=
   HashMap.Raw.not_mem_emptyWithCapacity
 
 @[simp, grind =] theorem contains_empty {a : α} : (∅ : Raw α).contains a = false :=