feat: add grind tactic (#6459)

This PR adds the (WIP) `grind` tactic. It currently generates a warning
message to make it clear that the tactic is not ready for production.

src/Init/Grind.lean

@@ -9,3 +9,4 @@ import Init.Grind.Tactics
 import Init.Grind.Lemmas
 import Init.Grind.Cases
 import Init.Grind.Propagator
+import Init.Grind.Util

src/Init/Grind/Tactics.lean

@@ -19,7 +19,15 @@ structure Config where
   eager : Bool := false
   deriving Inhabited, BEq
 
+end Lean.Grind
+
+namespace Lean.Parser.Tactic
+
 /-!
 `grind` tactic and related tactics.
 -/
-end Lean.Grind
+
+-- TODO: configuration option, parameters
+syntax (name := grind) "grind" : tactic
+
+end Lean.Parser.Tactic

src/Lean/Elab/Tactic.lean

@@ -44,3 +44,4 @@ import Lean.Elab.Tactic.DiscrTreeKey
 import Lean.Elab.Tactic.BVDecide
 import Lean.Elab.Tactic.BoolToPropSimps
 import Lean.Elab.Tactic.Classical
+import Lean.Elab.Tactic.Grind

src/Lean/Elab/Tactic/Grind.lean

@@ -0,0 +1,27 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Init.Grind.Tactics
+import Lean.Meta.Tactic.Grind
+import Lean.Elab.Tactic.Basic
+
+namespace Lean.Elab.Tactic
+open Meta
+
+def grind (mvarId : MVarId) (mainDeclName : Name) : MetaM Unit := do
+  let mvarIds ← Grind.main mvarId mainDeclName
+  unless mvarIds.isEmpty do
+    throwError "`grind` failed\n{goalsToMessageData mvarIds}"
+
+@[builtin_tactic Lean.Parser.Tactic.grind] def evalApplyRfl : Tactic := fun stx => do
+  match stx with
+  | `(tactic| grind) =>
+    logWarningAt stx "The `grind` tactic is experimental and still under development. Avoid using it in production projects"
+    let declName := (← Term.getDeclName?).getD `_grind
+    withMainContext do liftMetaFinishingTactic (grind · declName)
+  | _ => throwUnsupportedSyntax
+
+end Lean.Elab.Tactic

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

@@ -79,7 +79,7 @@ where
       proof?  := proofNew?
     }
 
-private def markAsInconsistent : GoalM Unit :=
+private def markAsInconsistent : GoalM Unit := do
   modify fun s => { s with inconsistent := true }
 
 /--

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

@@ -160,7 +160,12 @@ def preprocess (mvarId : MVarId) (mainDeclName : Name) : MetaM Preprocessor.Stat
   Preprocessor.preprocess mvarId |>.run |>.run mainDeclName
 
 def main (mvarId : MVarId) (mainDeclName : Name) : MetaM (List MVarId) := do
-  let s ← preprocess mvarId mainDeclName
-  return s.goals.toList.map (·.mvarId)
+  let go : GrindM (List MVarId) := do
+    let s ← Preprocessor.preprocess mvarId |>.run
+    let goals ← s.goals.toList.filterM fun goal => do
+      let (done, _) ← GoalM.run goal closeIfInconsistent
+      return !done
+    return goals.map (·.mvarId)
+  go.run mainDeclName
 
 end Lean.Meta.Grind

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

@@ -249,4 +249,15 @@ It assumes `a` and `False` are in the same equivalence class.
 def mkEqFalseProof (a : Expr) : GoalM Expr := do
   mkEqProof a (← getFalseExpr)
 
+def closeIfInconsistent : GoalM Bool := do
+  if (← isInconsistent) then
+    let mvarId := (← get).mvarId
+    unless (← mvarId.isAssigned) do
+      let trueEqFalse ← mkEqFalseProof (← getTrueExpr)
+      let falseProof ← mkEqMP trueEqFalse (mkConst ``True.intro)
+      mvarId.assign falseProof
+    return true
+  else
+    return false
+
 end Lean.Meta.Grind

tests/lean/run/grind_congr1.lean

@@ -1,67 +1,47 @@
-import Lean
-
-open Lean Meta Elab Tactic Grind in
-elab "grind_test" : tactic => withMainContext do
-  let declName := (← Term.getDeclName?).getD `_main
-  Meta.Grind.preprocessAndProbe (← getMainGoal) declName do
-    unless (← isInconsistent) do
-      throwError "inconsistent state expected"
-
+set_option warningAsError false
 set_option grind.debug true
 set_option grind.debug.proofs true
 
 example (a b : Nat) (f : Nat → Nat) : (h₁ : a = b) → f a = f b := by
-  grind_test
-  sorry
+  grind
 
 example (a b : Nat) (f : Nat → Nat) : (h₁ : a = b) → (h₂ : f a ≠ f b) → False := by
-  grind_test
-  sorry
+  grind
 
 example (a b : Nat) (f : Nat → Nat) : a = b → f (f a) ≠ f (f b) → False := by
-  grind_test
-  sorry
+  grind
 
 example (a b c : Nat) (f : Nat → Nat) : a = b → c = b → f (f a) ≠ f (f c) → False := by
-  grind_test
-  sorry
+  grind
 
 example (a b c : Nat) (f : Nat → Nat → Nat) : a = b → c = b → f (f a b) a ≠ f (f c c) c → False := by
-  grind_test
-  sorry
+  grind
 
 example (a b c : Nat) (f : Nat → Nat → Nat) : a = b → c = b → f (f a b) a = f (f c c) c := by
-  grind_test
-  sorry
+  grind
 
 example (a b c d : Nat) : a = b → b = c → c = d → a = d := by
-  grind_test
-  sorry
+  grind
 
 infix:50 "===" => HEq
 
 example (a b c d : Nat) : a === b → b = c → c === d → a === d := by
-  grind_test
-  sorry
+  grind
 
 example (a b c d : Nat) : a = b → b = c → c === d → a === d := by
-  grind_test
-  sorry
+  grind
 
 opaque f {α : Type} : α → α → α := fun a _ => a
 opaque g : Nat → Nat
 
 example (a b c : Nat) : a = b → g a === g b := by
-  grind_test
-  sorry
+  grind
 
 example (a b c : Nat) : a = b → c = b → f (f a b) (g c) = f (f c a) (g b) := by
-  grind_test
-  sorry
+  grind
 
 example (a b c d e x y : Nat) : a = b → a = x → b = y → c = d → c = e → c = b → a = e := by
-  grind_test
-  sorry
+  grind
 
 namespace Ex1
 opaque f (a b : Nat) : a > b → Nat
@@ -73,37 +53,33 @@ example (a₁ a₂ b₁ b₂ c d : Nat)
         a₁ = c → a₂ = c →
         b₁ = d → d  = b₂ →
         g (g (f a₁ b₁ H₁)) = g (g (f a₂ b₂ H₂)) := by
-  grind_test
-  sorry
+  grind
 end Ex1
 
 namespace Ex2
 def f (α : Type) (a : α) : α := a
 
 example (a : α) (b : β) : (h₁ : α = β) → (h₂ : HEq a b) → HEq (f α a) (f β b) := by
-  grind_test
-  sorry
+  grind
 
 end Ex2
 
 example (f g : (α : Type) → α → α) (a : α) (b : β) : (h₁ : α = β) → (h₂ : HEq a b) → (h₃ : f = g) → HEq (f α a) (g β b) := by
-  grind_test
-  sorry
+  grind
 
 set_option trace.grind.proof true in
 set_option trace.grind.proof.detail true in
 example (f : {α : Type} → α → Nat → Bool → Nat) (a b : Nat) : f a 0 true = v₁ → f b 0 true = v₂ → a = b → v₁ = v₂ := by
-  grind_test
-  sorry
+  grind
 
 set_option trace.grind.proof true in
 set_option trace.grind.proof.detail true in
 example (f : {α : Type} → α → Nat → Bool → Nat) (a b : Nat) : f a b x = v₁ → f a b y = v₂ → x = y → v₁ = v₂ := by
-  grind_test
-  sorry
+  grind
 
 set_option trace.grind.proof true in
 set_option trace.grind.proof.detail true in
-example (f : {α : Type} → α → Nat → Bool → Nat) (a b c : Nat) : f a b x = v₁ → f c b y = v₂ → a = c → x = y → v₁ = v₂ := by
-  grind_test
-  sorry
+theorem ex1 (f : {α : Type} → α → Nat → Bool → Nat) (a b c : Nat) : f a b x = v₁ → f c b y = v₂ → a = c → x = y → v₁ = v₂ := by
+  grind
+
+#print ex1

tests/lean/run/grind_pre.lean

@@ -1,20 +1,11 @@
-import Lean
-
-open Lean Meta Elab Tactic Grind in
-elab "grind_pre" : tactic => do
-  let declName := (← Term.getDeclName?).getD `_main
-  liftMetaTactic fun mvarId => do
-    Meta.Grind.main mvarId declName
-
 abbrev f (a : α) := a
 
 set_option grind.debug true
 set_option grind.debug.proofs true
 
 /--
-warning: declaration uses 'sorry'
----
-info: a b c : Bool
+error: `grind` failed
+a b c : Bool
 p q : Prop
 left✝ : a = true
 right✝ : b = true ∨ c = true
@@ -23,17 +14,14 @@ right : q
 x✝ : b = false ∨ a = false
 ⊢ False
 -/
-#guard_msgs in
+#guard_msgs (error) in
 theorem ex (h : (f a && (b || f (f c))) = true) (h' : p ∧ q) : b && a := by
-  grind_pre
-  trace_state
-  all_goals sorry
+  grind
 
 open Lean.Grind.Eager in
 /--
-warning: declaration uses 'sorry'
----
-info: a b c : Bool
+error: `grind` failed
+a b c : Bool
 p q : Prop
 left✝ : a = true
 h✝ : b = true
@@ -69,29 +57,31 @@ right : q
 h : a = false
 ⊢ False
 -/
-#guard_msgs in
+#guard_msgs (error) in
 theorem ex2 (h : (f a && (b || f (f c))) = true) (h' : p ∧ q) : b && a := by
-  grind_pre
-  trace_state
-  all_goals sorry
-
+  grind
 
 def g (i : Nat) (j : Nat) (_ : i > j := by omega) := i + j
 
+/--
+error: `grind` failed
+i j : Nat
+h : j + 1 < i + 1
+h✝ : j + 1 ≤ i
+x✝ : ¬g (i + 1) j ⋯ = i + j + 1
+⊢ False
+-/
+#guard_msgs (error) in
 example (i j : Nat) (h : i + 1 > j + 1) : g (i+1) j = f ((fun x => x) i) + f j + 1 := by
-  grind_pre
-  next hn =>
-  guard_hyp hn : ¬g (i + 1) j _ = i + j + 1
-  simp_arith [g] at hn
+  grind
 
 structure Point where
   x : Nat
   y : Int
 
 /--
-warning: declaration uses 'sorry'
----
-info: a₁ : Point
+error: `grind` failed
+a₁ : Point
 a₂ : Nat
 a₃ : Int
 as : List Point
@@ -105,25 +95,32 @@ y_eq : a₃ = b₃
 tail_eq : as = bs
 ⊢ False
 -/
-#guard_msgs in
+#guard_msgs (error) in
 theorem ex3 (h : a₁ :: { x := a₂, y := a₃ : Point } :: as = b₁ :: { x := b₂, y := b₃} :: bs) : False := by
-  grind_pre
-  trace_state
-  sorry
+  grind
 
 def h (a : α) := a
 
 set_option trace.grind.pre true in
-example (p : Prop) (a b c : Nat) : p → a = 0 → a = b → h a = h c → a = c ∧ c = a → a = b ∧ b = a → a ≠ c := by
-  grind_pre
-  sorry
+example (p : Prop) (a b c : Nat) : p → a = 0 → a = b → h a = h c → a = c ∧ c = a → a = b ∧ b = a → a = c := by
+  grind
 
 set_option trace.grind.proof.detail true
 set_option trace.grind.proof true
+set_option trace.grind.pre true
+/--
+error: `grind` failed
+α : Type
+a : α
+p q r : Prop
+h₁ : HEq p a
+h₂ : HEq q a
+h₃ : p = r
+⊢ False
+-/
+#guard_msgs (error) in
 example (a : α) (p q r : Prop) : (h₁ : HEq p a) → (h₂ : HEq q a) → (h₃ : p = r) → False := by
-  grind_pre
-  sorry
+  grind
 
 example (a b : Nat) (f : Nat → Nat) : (h₁ : a = b) → (h₂ : f a ≠ f b) → False := by
-  grind_pre
-  sorry
+  grind