fix: typo

This PR fixes an incorrect optimization in the `grind`
canonicalizer. See new test for an example that exposes the problem.

src/Init/Grind/Attr.lean

@@ -129,6 +129,14 @@ If `grind!` is used, then only minimal indexable subexpressions are considered.
 -/
 syntax grindLR     := patternIgnore("⇒" <|> "=>")
 /--
+The `.` modifier instructs `grind` to select a multi-pattern by traversing the conclusion of the
+theorem, and then the hypotheses from eft to right. We say this is the default modifier.
+Each time it encounters a subexpression which covers an argument which was not
+previously covered, it adds that subexpression as a pattern, until all arguments have been covered.
+If `grind!` is used, then only minimal indexable subexpressions are considered.
+-/
+syntax grindDef    := "." (grindGen)?
+/--
 The `usr` modifier indicates that this theorem was applied using a
 **user-defined instantiation pattern**. Such patterns are declared with
 the `grind_pattern` command, which lets you specify how `grind` should
@@ -206,6 +214,7 @@ syntax grindMod :=
     grindEqBoth <|> grindEqRhs <|> grindEq <|> grindEqBwd <|> grindBwd
     <|> grindFwd <|> grindRL <|> grindLR <|> grindUsr <|> grindCasesEager
     <|> grindCases <|> grindIntro <|> grindExt <|> grindGen <|> grindSym <|> grindInj
+    <|> grindDef
 syntax (name := grind) "grind" (ppSpace grindMod)? : attr
 syntax (name := grind!) "grind!" (ppSpace grindMod)? : attr
 syntax (name := grind?) "grind?" (ppSpace grindMod)? : attr

src/Lean/Elab/Tactic/Grind.lean

@@ -70,13 +70,14 @@ def elabInitGrindNorm : CommandElab := fun stx =>
   | _ => throwUnsupportedSyntax
 
 private def warnRedundantEMatchArg (s : Grind.EMatchTheorems) (declName : Name) : MetaM Unit := do
+  let minIndexable := false -- TODO: infer it
   let kinds ← match s.getKindsFor (.decl declName) with
     | [] => return ()
-    | [k] => pure m!"@{k.toAttribute}"
+    | [k] => pure m!"@{k.toAttribute minIndexable}"
     | [.eqLhs gen, .eqRhs _]
-    | [.eqRhs gen, .eqLhs _] => pure m!"@{(Grind.EMatchTheoremKind.eqBoth gen).toAttribute}"
+    | [.eqRhs gen, .eqLhs _] => pure m!"@{(Grind.EMatchTheoremKind.eqBoth gen).toAttribute minIndexable}"
     | ks =>
-      let ks := ks.map fun k => m!"@{k.toAttribute}"
+      let ks := ks.map fun k => m!"@{k.toAttribute minIndexable}"
       pure m!"{ks}"
   logWarning m!"this parameter is redundant, environment already contains `{declName}` annotated with `{kinds}`"
 
@@ -132,7 +133,7 @@ where
       for thm in thms do
         params := { params with extra := params.extra.push thm }
     | .ematch kind =>
-      params ← withRef p <| addEMatchTheorem params declName kind minIndexable
+      params ← withRef p <| addEMatchTheorem params id declName kind minIndexable
     | .cases eager =>
       ensureNoMinIndexable minIndexable
       withRef p <| Grind.validateCasesAttr declName eager
@@ -140,7 +141,7 @@ where
     | .intro =>
       if let some info ← Grind.isCasesAttrPredicateCandidate? declName false then
         for ctor in info.ctors do
-          params ← withRef p <| addEMatchTheorem params ctor (.default false) minIndexable
+          params ← withRef p <| addEMatchTheorem params id ctor (.default false) minIndexable
       else
         throwError "invalid use of `intro` modifier, `{.ofConstName declName}` is not an inductive predicate"
     | .inj =>
@@ -155,17 +156,17 @@ where
           -- If it is an inductive predicate,
           -- we also add the constructors (intro rules) as E-matching rules
           for ctor in info.ctors do
-            params ← withRef p <| addEMatchTheorem params ctor (.default false) minIndexable
+            params ← withRef p <| addEMatchTheorem params id ctor (.default false) minIndexable
       else
-        params ← withRef p <| addEMatchTheorem params declName (.default false) minIndexable
+        params ← withRef p <| addEMatchTheorem params id declName (.default false) minIndexable (suggest := true)
     | .symbol prio =>
       ensureNoMinIndexable minIndexable
       params := { params with symPrios := params.symPrios.insert declName prio }
     return params
 
-  addEMatchTheorem (params : Grind.Params) (declName : Name)
+  addEMatchTheorem (params : Grind.Params) (id : Ident) (declName : Name)
       (kind : Grind.EMatchTheoremKind)
-      (minIndexable : Bool) : MetaM Grind.Params := do
+      (minIndexable : Bool) (suggest : Bool := false) : MetaM Grind.Params := do
     let info ← getAsyncConstInfo declName
     match info.kind with
     | .thm | .axiom | .ctor =>
@@ -181,7 +182,10 @@ where
       | _ =>
         if kind matches .eqLhs _ | .eqRhs _ then
           ensureNoMinIndexable minIndexable
-        let thm ← Grind.mkEMatchTheoremForDecl declName kind params.symPrios (minIndexable := minIndexable)
+        let thm ← if suggest && !Grind.backward.grind.inferPattern.get (← getOptions) then
+          Grind.mkEMatchTheoremAndSuggest id declName params.symPrios minIndexable (isParam := true)
+        else
+          Grind.mkEMatchTheoremForDecl declName kind params.symPrios (minIndexable := minIndexable)
         if params.ematch.containsWithSamePatterns thm.origin thm.patterns then
           warnRedundantEMatchArg params.ematch declName
         return { params with extra := params.extra.push thm }

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

@@ -25,9 +25,11 @@ inductive AttrKind where
 def getAttrKindCore (stx : Syntax) : CoreM AttrKind := do
   match stx with
   | `(Parser.Attr.grindMod|=) => return .ematch (.eqLhs false)
+  | `(Parser.Attr.grindMod|.) => return .ematch (.default false)
   | `(Parser.Attr.grindMod|= gen) => return .ematch (.eqLhs true)
   | `(Parser.Attr.grindMod|→) => return .ematch .fwd
   | `(Parser.Attr.grindMod|←) => return .ematch (.bwd false)
+  | `(Parser.Attr.grindMod|. gen) => return .ematch (.default true)
   | `(Parser.Attr.grindMod|← gen) => return .ematch (.bwd true)
   | `(Parser.Attr.grindMod|=_) => return .ematch (.eqRhs false)
   | `(Parser.Attr.grindMod|=_ gen) => return .ematch (.eqRhs true)

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

@@ -74,40 +74,53 @@ If `useIsDefEqBounded` is `true`, we try `isDefEqBounded` before returning false
 -/
 private def canonElemCore (parent : Expr) (f : Expr) (i : Nat) (e : Expr) (useIsDefEqBounded : Bool) : GoalM Expr := do
   let s ← get'
-  if let some c := s.canon.find? e then
+  let key := { f, i, arg := e : CanonArgKey }
+  /-
+  **Note**: We used to use `s.canon.find? e` instead of `s.canonArg.find? key`. This was incorrect.
+  First, for types and implicit arguments, we recursively visit `e` before invoking this function.
+  Thus, `s.canon.find? e` always returns some value `c`, causing us to miss possible canonicalization opportunities.
+  Moreover, `e` may be the argument of two different `f` functions.
+  -/
+  if let some c := s.canonArg.find? key then
     return c
-  let key := (f, i)
-  let eType ← inferType e
-  let cs := s.argMap.find? key |>.getD []
-  for (c, cType) in cs do
-    /-
-    We first check the types
-    The following checks are a performance bottleneck.
-    For example, in the test `grind_ite.lean`, there are many checks of the form:
-    ```
-    w_4 ∈ assign.insert v true → Prop =?= w_1 ∈ assign.insert v false → Prop
-    ```
-    where `grind` unfolds the definition of `DHashMap.insert` and `TreeMap.insert`.
-    -/
-    if (← isDefEqD eType cType) then
-      if (← isDefEq e c) then
-        -- We used to check `c.fvarsSubset e` because it is not
-        -- in general safe to replace `e` with `c` if `c` has more free variables than `e`.
-        -- However, we don't revert previously canonicalized elements in the `grind` tactic.
-        -- Moreover, we store the canonicalizer state in the `Goal` because we case-split
-        -- and different locals are added in different branches.
-        modify' fun s => { s with canon := s.canon.insert e c }
-        trace_goal[grind.debug.canon] "found {e} ===> {c}"
-        return c
-      if useIsDefEqBounded then
-        -- If `e` and `c` are not types, we use `isDefEqBounded`
-        if (← isDefEqBounded e c parent) then
+  let c ← go
+  modify' fun s => { s with canonArg := s.canonArg.insert key c }
+  return c
+where
+  go : GoalM Expr := do
+    let s ← get'
+    let key := (f, i)
+    let eType ← inferType e
+    let cs := s.argMap.find? key |>.getD []
+    for (c, cType) in cs do
+      /-
+      We first check the types
+      The following checks are a performance bottleneck.
+      For example, in the test `grind_ite.lean`, there are many checks of the form:
+      ```
+      w_4 ∈ assign.insert v true → Prop =?= w_1 ∈ assign.insert v false → Prop
+      ```
+      where `grind` unfolds the definition of `DHashMap.insert` and `TreeMap.insert`.
+      -/
+      if (← isDefEqD eType cType) then
+        if (← isDefEq e c) then
+          -- We used to check `c.fvarsSubset e` because it is not
+          -- in general safe to replace `e` with `c` if `c` has more free variables than `e`.
+          -- However, we don't revert previously canonicalized elements in the `grind` tactic.
+          -- Moreover, we store the canonicalizer state in the `Goal` because we case-split
+          -- and different locals are added in different branches.
           modify' fun s => { s with canon := s.canon.insert e c }
-          trace_goal[grind.debug.canon] "found using `isDefEqBounded`: {e} ===> {c}"
+          trace_goal[grind.debug.canon] "found {e} ===> {c}"
           return c
-  trace_goal[grind.debug.canon] "({f}, {i}) ↦ {e}"
-  modify' fun s => { s with canon := s.canon.insert e e, argMap := s.argMap.insert key ((e, eType)::cs) }
-  return e
+        if useIsDefEqBounded then
+          -- If `e` and `c` are not types, we use `isDefEqBounded`
+          if (← isDefEqBounded e c parent) then
+            modify' fun s => { s with canon := s.canon.insert e c }
+            trace_goal[grind.debug.canon] "found using `isDefEqBounded`: {e} ===> {c}"
+            return c
+    trace_goal[grind.debug.canon] "({f}, {i}) ↦ {e}"
+    modify' fun s => { s with canon := s.canon.insert e e, argMap := s.argMap.insert key ((e, eType)::cs) }
+    return e
 
 private abbrev canonType (parent f : Expr) (i : Nat) (e : Expr) := withDefault <| canonElemCore parent f i e (useIsDefEqBounded := false)
 private abbrev canonInst (parent f : Expr) (i : Nat) (e : Expr) := withReducibleAndInstances <| canonElemCore parent f i e (useIsDefEqBounded := true)

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

@@ -312,25 +312,31 @@ def EMatchTheoremKind.isDefault : EMatchTheoremKind → Bool
   | .default _ => true
   | _ => false
 
-def EMatchTheoremKind.toAttributeCore : EMatchTheoremKind → String
-  | .eqLhs true     => " = gen"
-  | .eqLhs false    => " ="
-  | .eqRhs true     => " =_ gen"
-  | .eqRhs false    => " =_"
-  | .eqBoth false   => " _=_"
-  | .eqBoth true    => " _=_ gen"
-  | .eqBwd          => " ←="
-  | .fwd            => " →"
-  | .bwd false      => " ←"
-  | .bwd true       => " ← gen"
-  | .leftRight      => " =>"
-  | .rightLeft      => " <="
-  | .default false  => ""
-  | .default true   => " gen"
+def EMatchTheoremKind.toAttributeCore (kind : EMatchTheoremKind) : String :=
+  match kind with
+  | .eqLhs true     => "= gen"
+  | .eqLhs false    => "="
+  | .eqRhs true     => "=_ gen"
+  | .eqRhs false    => "=_"
+  | .eqBoth false   => "_=_"
+  | .eqBoth true    => "_=_ gen"
+  | .eqBwd          => "←="
+  | .fwd            => "→"
+  | .bwd false      => "←"
+  | .bwd true       => "← gen"
+  | .leftRight      => "=>"
+  | .rightLeft      => "<="
+  | .default false  => "."
+  | .default true   => ". gen"
   | .user           => ""
 
-def EMatchTheoremKind.toAttribute (k : EMatchTheoremKind) : String :=
-  s!"[grind{toAttributeCore k}]"
+def EMatchTheoremKind.toAttribute (k : EMatchTheoremKind) (minIndexable : Bool): String :=
+  if k matches .user then
+    "[grind]"
+  else if minIndexable then
+    s!"[grind! {toAttributeCore k}]"
+  else
+    s!"[grind {toAttributeCore k}]"
 
 private def EMatchTheoremKind.explainFailure : EMatchTheoremKind → String
   | .eqLhs _   => "failed to find pattern in the left-hand side of the theorem's conclusion"
@@ -1302,7 +1308,7 @@ where
 def mkEMatchTheoremForDecl (declName : Name) (thmKind : EMatchTheoremKind) (prios : SymbolPriorities)
     (showInfo := false) (minIndexable := false) : MetaM EMatchTheorem := do
   let some thm ← mkEMatchTheoremWithKind? (.decl declName) #[] (← getProofFor declName) thmKind prios (showInfo := showInfo) (minIndexable := minIndexable)
-    | throwError "`@{thmKind.toAttribute} theorem {.ofConstName declName}` {thmKind.explainFailure}, consider using different options or the `grind_pattern` command"
+    | throwError "`@{thmKind.toAttribute minIndexable} theorem {.ofConstName declName}` {thmKind.explainFailure}, consider using different options or the `grind_pattern` command"
   return thm
 
 def mkEMatchEqTheoremsForDef? (declName : Name) (showInfo := false) : MetaM (Option (Array EMatchTheorem)) := do
@@ -1318,7 +1324,7 @@ private def addGrindEqAttr (declName : Name) (attrKind : AttributeKind) (thmKind
       throwError "`{.ofConstName declName}` is a definition, you must only use the left-hand side for extracting patterns"
     thms.forM (ematchTheoremsExt.add · attrKind)
   else
-    throwError s!"`{thmKind.toAttribute}` attribute can only be applied to equational theorems or function definitions"
+    throwError s!"`{thmKind.toAttribute false}` attribute can only be applied to equational theorems or function definitions"
 
 def EMatchTheorems.eraseDecl (s : EMatchTheorems) (declName : Name) : MetaM EMatchTheorems := do
   let throwErr {α} : MetaM α :=
@@ -1369,29 +1375,126 @@ private structure SelectM.State where
 
 private abbrev SelectM := StateT SelectM.State MetaM
 
-private def save (thm : EMatchTheorem) (minIndexable : Bool) : SelectM Unit := do
+def EMatchTheoremKind.toSyntax (kind : EMatchTheoremKind) : CoreM (TSyntax ``Parser.Attr.grindMod) :=
+  match kind with
+  | .eqLhs true     => `(Parser.Attr.grindMod| = gen)
+  | .eqLhs false    => `(Parser.Attr.grindMod|=)
+  | .eqRhs true     => `(Parser.Attr.grindMod|=_ gen)
+  | .eqRhs false    => `(Parser.Attr.grindMod|=_)
+  | .eqBoth false   => `(Parser.Attr.grindMod|_=_)
+  | .eqBoth true    => `(Parser.Attr.grindMod|_=_ gen)
+  | .eqBwd          => `(Parser.Attr.grindMod|←=)
+  | .fwd            => `(Parser.Attr.grindMod|→)
+  | .bwd false      => `(Parser.Attr.grindMod|←)
+  | .bwd true       => `(Parser.Attr.grindMod|← gen)
+  | .leftRight      => `(Parser.Attr.grindMod|=>)
+  | .rightLeft      => `(Parser.Attr.grindMod|<=)
+  | .default false  => `(Parser.Attr.grindMod|.)
+  | .default true   => `(Parser.Attr.grindMod|. gen)
+  | .user           => throwError "`grind` theorem kind is not a modifier"
+
+private def save (ref : Syntax) (thm : EMatchTheorem) (isParam : Bool) (minIndexable : Bool) : SelectM Unit := do
   -- We only save `thm` if the pattern is different from the ones that were already found.
   if (← get).thms.all fun thm' => thm.patterns != thm'.patterns then
-    let baseAttr := if minIndexable then "grind!" else "grind"
-    let msg := s!"] for pattern: {← thm.patterns.mapM fun p => (ppPattern p).toString}"
+    let pats ← thm.patterns.mapM fun p => (ppPattern p).toString
+    let openBracket  := if isParam then "" else "["
+    let closeBracket := if isParam then "" else "]"
+    let msg := s!"{closeBracket} for pattern: {pats}"
+    let suggestion : Tactic.TryThis.SuggestionText ← match isParam, minIndexable with
+      | false, true  => pure <| Tactic.TryThis.SuggestionText.tsyntax (← `(attr|grind! $(← thm.kind.toSyntax)))
+      | false, false => pure <| .tsyntax (← `(attr|grind $(← thm.kind.toSyntax)))
+      | true,  true  => pure <| .tsyntax (← `(Parser.Tactic.grindParam|!$(← thm.kind.toSyntax)$(⟨ref⟩):ident))
+      | true, false  => pure <| .tsyntax (← `(Parser.Tactic.grindParam|$(← thm.kind.toSyntax) $(⟨ref⟩):ident))
     modify fun s => { s with
       thms := s.thms.push thm
       suggestions := s.suggestions.push {
-        suggestion := .string s!"{baseAttr}{thm.kind.toAttributeCore}"
+        suggestion
         -- **Note**: small hack to include brackets in the suggestion
-        preInfo?   := some "["
-        -- **Note**: appears only on the info view.
+        preInfo?   := some openBracket
+        -- **Note**: appears only in the info view.
         postInfo?  := some msg
       }
     }
 
+register_builtin_option grind.param.codeAction : Bool := {
+  defValue := false
+  descr    := "code-action for `grind` parameters"
+}
+
+/-- Helper type for generating suggestions for `grind` parameters -/
+inductive MinIndexableMode where
+  | /-- `minIndexable := true` -/
+    yes
+  | /-- `minIndexable := false` -/
+    no
+  | /--
+    Tries with and without the minimal indexable subexpression condition, if both produce the
+    same pattern, use the one `minIndexable := false` since it is more compact.
+    -/
+    both
+
+/--
+Tries different modifiers, logs info messages with modifiers that worked, but returns just the first one that worked.
+-/
+def mkEMatchTheoremAndSuggest (ref : Syntax) (declName : Name) (prios : SymbolPriorities)
+    (minIndexable : Bool) (isParam : Bool := false) : MetaM EMatchTheorem := do
+  let tryModifier (thmKind : EMatchTheoremKind) (minIndexable : MinIndexableMode) : SelectM Unit := do
+    try
+      match minIndexable with
+      | .yes =>
+        let thm ← mkEMatchTheoremForDecl declName thmKind prios (showInfo := false) (minIndexable := true)
+        save ref thm (minIndexable := true) (isParam := isParam)
+      | .no =>
+        let thm ← mkEMatchTheoremForDecl declName thmKind prios (showInfo := false) (minIndexable := false)
+        save ref thm (minIndexable := false) (isParam := isParam)
+      | .both =>
+        let thm₁ ← mkEMatchTheoremForDecl declName thmKind prios (showInfo := false) (minIndexable := true)
+        let thm₂ ← mkEMatchTheoremForDecl declName thmKind prios (showInfo := false) (minIndexable := false)
+        if thm₁.patterns == thm₂.patterns then
+          -- If both produce the same pattern, we save only `minIndexable := false` since it is more compact
+          save ref thm₂ (minIndexable := false) (isParam := isParam)
+        else
+          save ref thm₁ (minIndexable := true) (isParam := isParam)
+          save ref thm₂ (minIndexable := false) (isParam := isParam)
+    catch _ =>
+      return ()
+  let searchCore (minIndexable : MinIndexableMode) : SelectM Unit := do
+    tryModifier (.default false) minIndexable
+    tryModifier (.bwd false) minIndexable
+    tryModifier .fwd minIndexable
+    tryModifier .rightLeft minIndexable
+    tryModifier .leftRight minIndexable
+  let search : SelectM Unit := do
+    if minIndexable then
+      searchCore .yes
+    else if isParam then
+      searchCore .both
+      tryModifier (.eqLhs false) .no
+      tryModifier (.eqRhs false) .no
+    else
+      tryModifier (.eqLhs false) .no
+      tryModifier (.eqRhs false) .no
+      searchCore .no
+      searchCore .yes
+  let (_, s) ← search.run {}
+  if h₁ : 0 < s.thms.size then
+    if !isParam || grind.param.codeAction.get (← getOptions) then
+      if s.suggestions.size == 1 then
+        Tactic.TryThis.addSuggestion ref s.suggestions[0]!
+      else
+        Tactic.TryThis.addSuggestions ref s.suggestions
+    return s.thms[0]
+  else
+    throwError "invalid `grind` theorem, failed to find an usable pattern using different modifiers"
+
 /--
 Tries different modifiers, logs info messages with modifiers that worked, but stores just the first one that worked.
 
 Remark: if `backward.grind.inferPattern` is `true`, then `.default false` is used.
 The parameter `showInfo` is only taken into account when `backward.grind.inferPattern` is `true`.
 -/
-def addEMatchAttrAndSuggest (ref : Syntax) (declName : Name) (attrKind : AttributeKind) (prios : SymbolPriorities) (minIndexable : Bool) (showInfo : Bool) : MetaM Unit := do
+def addEMatchAttrAndSuggest (ref : Syntax) (declName : Name) (attrKind : AttributeKind) (prios : SymbolPriorities)
+    (minIndexable : Bool) (showInfo : Bool) (isParam : Bool := false) : MetaM Unit := do
   let info ← getConstInfo declName
   if !wasOriginallyTheorem (← getEnv) declName && !info.isCtor && !info.isAxiom then
     ensureNoMinIndexable minIndexable
@@ -1399,34 +1502,8 @@ def addEMatchAttrAndSuggest (ref : Syntax) (declName : Name) (attrKind : Attribu
   else if backward.grind.inferPattern.get (← getOptions) then
     addEMatchAttr declName attrKind (.default false) prios (minIndexable := minIndexable) (showInfo := showInfo)
   else
-    let tryModifier (thmKind : EMatchTheoremKind) (minIndexable : Bool) : SelectM Unit := do
-      try
-        let thm ← mkEMatchTheoremForDecl declName thmKind prios (showInfo := false) (minIndexable := minIndexable)
-        save thm minIndexable
-      catch _ =>
-        return ()
-    let searchCore (minIndexable : Bool) : SelectM Unit := do
-      tryModifier (.bwd false) minIndexable
-      tryModifier .fwd minIndexable
-      tryModifier .rightLeft minIndexable
-      tryModifier .leftRight minIndexable
-    let search : SelectM Unit := do
-      if minIndexable then
-        searchCore true
-      else
-        tryModifier (.eqLhs false) false
-        tryModifier (.eqRhs false) false
-        searchCore false
-        searchCore true
-    let (_, s) ← search.run {}
-    if h₁ : 0 < s.thms.size then
-      if s.suggestions.size == 1 then
-        Tactic.TryThis.addSuggestion ref s.suggestions[0]!
-      else
-        Tactic.TryThis.addSuggestions ref s.suggestions
-      ematchTheoremsExt.add s.thms[0] attrKind
-    else
-      throwError "invalid `grind` theorem, failed to find an usable pattern using different modifiers"
+    let thm ← mkEMatchTheoremAndSuggest ref declName prios minIndexable isParam
+    ematchTheoremsExt.add thm attrKind
 
 def eraseEMatchAttr (declName : Name) : MetaM Unit := do
   /-

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

@@ -600,11 +600,18 @@ structure NewRawFact where
   splitSource  : SplitSource
   deriving Inhabited
 
+structure CanonArgKey where
+  f   : Expr
+  i   : Nat
+  arg : Expr
+  deriving BEq, Hashable
+
 /-- Canonicalizer state. See `Canon.lean` for additional details. -/
 structure Canon.State where
   argMap     : PHashMap (Expr × Nat) (List (Expr × Expr)) := {}
   canon      : PHashMap Expr Expr := {}
   proofCanon : PHashMap Expr Expr := {}
+  canonArg   : PHashMap CanonArgKey Expr := {}
   deriving Inhabited
 
 /-- Trace information for a case split. -/

tests/lean/run/grind_9610.lean

@@ -7,4 +7,4 @@ theorem foo (x: UInt32) :
 
 theorem aa (x : UInt32) :
   x.toNat ≤ sixteen.toNat := by
-  grind [!foo]
+  grind [foo]

tests/lean/run/grind_canon_bug_2.lean

@@ -0,0 +1,21 @@
+import Std.Data.ExtHashMap
+open Std
+set_option warn.sorry false
+
+-- The following trace should contain only one `m[k]` and `(m.insert 1 3)[k]`
+/--
+trace: [grind.cutsat.model] k := 101
+[grind.cutsat.model] (ExtHashMap.filter (fun k x => decide (101 ≤ k)) (m.insert 1 3))[k] := 4
+[grind.cutsat.model] (m.insert 1 2)[k] := 4
+[grind.cutsat.model] (m.insert 1 3)[k] := 4
+[grind.cutsat.model] m[k] := 4
+[grind.cutsat.model] (m.insert 1 2).getKey k ⋯ := 101
+[grind.cutsat.model] m.getKey k ⋯ := 101
+-/
+#guard_msgs in
+example (m : ExtHashMap Nat Nat) :
+    (m.insert 1 2).filter (fun k _ => k > 1000) = (m.insert 1 3).filter fun k _ => k > 100 := by
+  ext1 k
+  set_option trace.grind.cutsat.model true in
+  fail_if_success grind (splits := 4)
+  sorry

tests/lean/run/grind_pat_sel.lean

@@ -64,7 +64,7 @@ opaque r : Nat → Nat → Nat
 
 /--
 info: Try these:
-  • [grind! ←] for pattern: [r #2 (f #1)]
+  • [grind! .] for pattern: [r #2 (f #1)]
   • [grind! =>] for pattern: [f #2, f #1]
 -/
 #guard_msgs in
@@ -72,7 +72,7 @@ info: Try these:
 
 /--
 info: Try these:
-  • [grind! <=] for pattern: [f #1, f #2]
+  • [grind! .] for pattern: [f #1, f #2]
   • [grind! =>] for pattern: [f #2, f #1]
 -/
 #guard_msgs in
@@ -80,9 +80,9 @@ info: Try these:
 
 /--
 info: Try these:
-  • [grind <=] for pattern: [r #1 (f #1), p (f #2)]
+  • [grind .] for pattern: [r #1 (f #1), p (f #2)]
   • [grind =>] for pattern: [p (f #2), r #1 (f #1)]
-  • [grind! <=] for pattern: [f #1, f #2]
+  • [grind! .] for pattern: [f #1, f #2]
   • [grind! =>] for pattern: [f #2, f #1]
 -/
 #guard_msgs in
@@ -101,7 +101,7 @@ info: Try these:
 /--
 info: Try these:
   • [grind =] for pattern: [f (g #0)]
-  • [grind! ←] for pattern: [g #0]
+  • [grind! .] for pattern: [g #0]
 -/
 #guard_msgs in
 @[grind] axiom fg₆ : f (g x) = x
@@ -110,7 +110,7 @@ info: Try these:
 info: Try these:
   • [grind =] for pattern: [f (g #0)]
   • [grind =_] for pattern: [r #0 #0]
-  • [grind! ←] for pattern: [g #0]
+  • [grind! .] for pattern: [g #0]
 -/
 #guard_msgs in
 @[grind] axiom fg₇ : f (g x) = r x x
@@ -132,13 +132,13 @@ axiom fooInv_foo : fooInv (foo x) = x
 #guard_msgs in
 set_option trace.grind.ematch.pattern true in
 example : foo x = foo y → x = y := by
-  grind [!fooInv_foo]
+  grind [!←fooInv_foo]
 
 /-- trace: [grind.ematch.pattern] fooInv_foo: [fooInv (foo #0)] -/
 #guard_msgs in
 set_option trace.grind.ematch.pattern true in
 example : foo x = foo y → x = y := by
-  fail_if_success grind [fooInv_foo]
+  fail_if_success grind [←fooInv_foo]
   sorry
 
 opaque bar : Nat → Nat

tests/lean/run/grind_primes.lean

@@ -41,7 +41,7 @@ and showing that `n! + 1` has a prime factor larger than `n`.
 -/
 theorem InfinitudeOfPrimes : ∀ n, ∃ p > n, IsPrime p := by
   intro n
-  have : 1 < n ! + 1 := by grind [!factorial_pos]
+  have : 1 < n ! + 1 := by grind [factorial_pos]
   obtain ⟨p, hp, _⟩ := exists_prime_factor (n ! + 1) this
   suffices ¬p ≤ n by grind
   intro (_ : p ≤ n)

tests/lean/run/grind_usr.lean

@@ -12,7 +12,7 @@ public theorem fthm : f (f x) = f x := sorry
 #guard_msgs (trace) in
 set_option trace.grind.ematch.pattern true in
 example : f (f (f x)) = f x := by
-  grind only [!fthm]
+  grind only [!←fthm]
 
 /--
 trace: [grind.ematch.instance] fthm: f (f x) = f x

tests/lean/run/grind_warn_param.lean

@@ -41,7 +41,7 @@ example : True := by grind [→ pqf, = Array.size_set]
 warning: this parameter is redundant, environment already contains `Array.size_set` annotated with `@[grind =]`
 -/
 #guard_msgs (warning) in
-example : True := by grind [Array.size_set]
+example : True := by grind [= Array.size_set]
 
 /--
 warning: this parameter is redundant, environment already contains `hg` annotated with `@[grind _=_]`
@@ -59,7 +59,7 @@ example : True := by grind [=_ hg]
 warning: this parameter is redundant, environment already contains `Array.size_set` annotated with `@[grind =]`
 -/
 #guard_msgs (warning) in
-example : True := by grind [Array.size_set]
+example : True := by grind [= Array.size_set]
 
 #guard_msgs (warning) in
 example : True := by grind [pqf]