feat: add support for constructors and axioms to the grind E-matching module (#6839)

This PR ensures `grind` can use constructors and axioms for heuristic
instantiation based on E-matching. It also allows patterns without
pattern variables for theorems such as `theorem evenz : Even 0`.

src/Lean/Declaration.lean

@@ -478,6 +478,10 @@ def isCtor : ConstantInfo → Bool
   | .ctorInfo _ => true
   | _           => false
 
+def isAxiom : ConstantInfo → Bool
+  | .axiomInfo _ => true
+  | _            => false
+
 def isInductive : ConstantInfo → Bool
   | .inductInfo _ => true
   | _             => false

src/Lean/Elab/Tactic/Grind.lean

@@ -93,7 +93,7 @@ where
   addEMatchTheorem (params : Grind.Params) (declName : Name) (kind : Grind.EMatchTheoremKind) : MetaM Grind.Params := do
     let info ← getConstInfo declName
     match info with
-    | .thmInfo _ =>
+    | .thmInfo _ | .axiomInfo _ | .ctorInfo _ =>
       if kind == .eqBoth then
         let params := { params with extra := params.extra.push (← Grind.mkEMatchTheoremForDecl declName .eqLhs) }
         return { params with extra := params.extra.push (← Grind.mkEMatchTheoremForDecl declName .eqRhs) }

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

@@ -359,9 +359,7 @@ def getPatternSupportMask (f : Expr) (numArgs : Nat) : MetaM (Array Bool) := do
       else
         return (← x.fvarId!.getDecl).binderInfo matches .instImplicit
 
-private partial def go (pattern : Expr) (root := false) : M Expr := do
-  if root && !pattern.hasLooseBVars then
-    throwError "invalid pattern, it does not have pattern variables"
+private partial def go (pattern : Expr) : M Expr := do
   if let some (e, k) := isOffsetPattern? pattern then
     let e ← goArg e (isSupport := false)
     if e == dontCare then
@@ -550,9 +548,11 @@ def mkEMatchTheoremCore (origin : Origin) (levelParams : Array Name) (numParams
     levelParams, origin, kind
   }
 
-private def getProofFor (declName : Name) : CoreM Expr := do
-  let .thmInfo info ← getConstInfo declName
-    | throwError "`{declName}` is not a theorem"
+private def getProofFor (declName : Name) : MetaM Expr := do
+  let info ← getConstInfo declName
+  unless info.isTheorem do
+    unless (← isProp info.type) do
+      throwError "invalid E-matching theorem `{declName}`, type is not a proposition"
   let us := info.levelParams.map mkLevelParam
   return mkConst declName us
 
@@ -699,7 +699,55 @@ private def collectPatterns? (proof : Expr) (xs : Array Expr) (searchPlaces : Ar
     | return none
   return some (ps, s.symbols.toList)
 
-def mkEMatchTheoremWithKind? (origin : Origin) (levelParams : Array Name) (proof : Expr) (kind : EMatchTheoremKind) : MetaM (Option EMatchTheorem) := do
+/--
+Tries to find a ground pattern to activate the theorem.
+This is used for theorems such as `theorem evenZ : Even 0`.
+This function is only used if `collectPatterns?` returns `none`.
+-/
+private partial def collectGroundPattern? (proof : Expr) (xs : Array Expr) (searchPlaces : Array Expr) : MetaM (Option (Expr × List HeadIndex)) := do
+  unless (← checkCoverage proof xs.size {}) matches .ok do
+    return none
+  let go? : CollectorM (Option Expr) := do
+    for place in searchPlaces do
+      let place ← preprocessPattern place
+      if let some r ← visit? place then
+        return r
+    return none
+  let (some p, s) ← go? { proof, xs } |>.run' {} |>.run {}
+    | return none
+  return some (p, s.symbols.toList)
+where
+  visit? (e : Expr) : CollectorM (Option Expr) := do
+    match e with
+    | .app .. =>
+      let f := e.getAppFn
+      if (← isPatternFnCandidate f) then
+        let e ← NormalizePattern.normalizePattern e
+        return some e
+      else
+        let args := e.getAppArgs
+        for arg in args, flag in (← NormalizePattern.getPatternSupportMask f args.size) do
+          unless flag do
+            if let some r ← visit? arg then
+              return r
+        return none
+    | .forallE _ d b _ =>
+      if (← pure e.isArrow <&&> isProp d <&&> isProp b) then
+        if let some d ← visit? d then return d
+        visit? b
+      else
+        return none
+    | _ => return none
+
+/--
+Creates an E-match theorem using the given proof and kind.
+If `groundPatterns` is `true`, it accepts patterns without pattern variables. This is useful for
+theorems such as `theorem evenZ : Even 0`. For local theorems, we use `groundPatterns := false`
+since the theorem is already in the `grind` state and there is nothing to be instantiated.
+-/
+def mkEMatchTheoremWithKind?
+      (origin : Origin) (levelParams : Array Name) (proof : Expr) (kind : EMatchTheoremKind)
+      (groundPatterns := true) : MetaM (Option EMatchTheorem) := do
   if kind == .eqLhs then
     return (← mkEMatchEqTheoremCore origin levelParams proof (normalizePattern := true) (useLhs := true))
   else if kind == .eqRhs then
@@ -720,8 +768,14 @@ def mkEMatchTheoremWithKind? (origin : Origin) (levelParams : Array Name) (proof
     go xs searchPlaces
 where
   go (xs : Array Expr) (searchPlaces : Array Expr) : MetaM (Option EMatchTheorem) := do
-    let some (patterns, symbols) ← collectPatterns? proof xs searchPlaces
-      | return none
+    let (patterns, symbols) ← if let some r ← collectPatterns? proof xs searchPlaces then
+      pure r
+    else if !groundPatterns then
+      return none
+    else if let some (pattern, symbols) ← collectGroundPattern? proof xs searchPlaces then
+      pure ([pattern], symbols)
+    else
+      return none
     let numParams := xs.size
     trace[grind.ematch.pattern] "{← origin.pp}: {patterns.map ppPattern}"
     return some {
@@ -774,11 +828,13 @@ def addEMatchAttr (declName : Name) (attrKind : AttributeKind) (thmKind : EMatch
   else if thmKind == .eqBoth then
     addGrindEqAttr declName attrKind thmKind (useLhs := true)
     addGrindEqAttr declName attrKind thmKind (useLhs := false)
-  else if !(← getConstInfo declName).isTheorem then
-    addGrindEqAttr declName attrKind thmKind
   else
-    let thm ← mkEMatchTheoremForDecl declName thmKind
-    ematchTheoremsExt.add thm attrKind
+    let info ← getConstInfo declName
+    if !info.isTheorem && !info.isCtor && !info.isAxiom then
+      addGrindEqAttr declName attrKind thmKind
+    else
+      let thm ← mkEMatchTheoremForDecl declName thmKind
+      ematchTheoremsExt.add thm attrKind
 
 def eraseEMatchAttr (declName : Name) : MetaM Unit := do
   /-

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

@@ -55,7 +55,7 @@ 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) : MetaM (Option EMatchTheorem) := do
   try
-    mkEMatchTheoremWithKind? origin #[] proof kind
+    mkEMatchTheoremWithKind? origin #[] proof kind (groundPatterns := false)
   catch _ =>
     return none
 

tests/lean/run/grind_ctor_ematch.lean

@@ -0,0 +1,69 @@
+inductive Even : Nat → Prop
+  | zero : Even 0
+  | plus_two {n} : Even n → Even (n + 2)
+
+example : Even 2 := by
+  grind [Even.plus_two, Even.zero]
+
+attribute [grind] Even.zero
+attribute [grind] Even.plus_two
+
+example : Even 2 := by
+  grind
+
+example : Even 4 := by
+  grind
+
+/--
+error: `grind` failed
+case grind
+x✝ : ¬Even 16
+⊢ False
+[grind] Diagnostics
+  [facts] Asserted facts
+    [prop] ¬Even 16
+    [prop] Even 14 → Even 16
+    [prop] Even 12 → Even 14
+    [prop] Even 10 → Even 12
+    [prop] Even 8 → Even 10
+    [prop] Even 6 → Even 8
+  [eqc] True propositions
+    [prop] Even 14 → Even 16
+    [prop] Even 12 → Even 14
+    [prop] Even 10 → Even 12
+    [prop] Even 8 → Even 10
+    [prop] Even 6 → Even 8
+  [eqc] False propositions
+    [prop] Even 16
+  [ematch] E-matching patterns
+    [thm] Even.plus_two: [Even (Lean.Grind.offset #1 (2))]
+    [thm] Even.zero: [Even `[0]]
+  [limits] Thresholds reached
+    [limit] maximum number of E-matching rounds has been reached, threshold: `(ematch := 5)`
+    [limit] maximum term generation has been reached, threshold: `(gen := 5)`
+[grind] Counters
+  [thm] E-Matching instances
+    [thm] Even.plus_two ↦ 5
+-/
+#guard_msgs (error) in
+example : Even 16 := by
+  grind
+
+example : Even 16 := by
+  grind (gen := 9) (ematch := 9)
+
+opaque f : Nat → Nat
+
+axiom fax (x : Nat) : f (f x) = f x
+
+example : f (f (f x)) = f x := by
+  grind [fax]
+
+attribute [grind] fax
+
+example : f (f (f x)) = f x := by
+  grind
+
+/-- error: invalid E-matching theorem `Nat.succ`, type is not a proposition -/
+#guard_msgs in
+attribute [grind] Nat.succ

tests/lean/run/grind_pattern1.lean

@@ -19,9 +19,7 @@ grind_pattern List.mem_concat_self => a ∈ xs ++ [a]
 
 def foo (x : Nat) := x + x
 
-/--
-error: `foo` is not a theorem
--/
+/-- error: invalid E-matching theorem `foo`, type is not a proposition -/
 #guard_msgs in
 grind_pattern foo => x + x