feat: grind -revert (#11248)

This PR implements the option `revert`, which is set to `false` by
default. To recover the old `grind` behavior, you should use `grind
+revert`. Previously, `grind` used the `RevSimpIntro` idiom, i.e., it
would revert all hypotheses and then re-introduce them while simplifying
and applying eager `cases`. This idiom created several problems:

* Users reported that `grind` would include unnecessary parameters. See
[here](https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Grind.20aggressively.20includes.20local.20hypotheses.2E/near/554887715).
* Unnecessary section variables were also being introduced. See the new
test contributed by Sebastian Graf.
* Finally, it prevented us from supporting arbitrary parameters as we do
in `simp`. In `simp`, I implemented a mechanism that simulates local
universe-polymorphic theorems, but this approach could not be used in
`grind` because there is no mechanism for reverting (and re-introducing)
local universe-polymorphic theorems. Adding such a mechanism would
require substantial work: I would need to modify the local context
object. I considered maintaining a substitution from the original
variables to the new ones, but this is also tricky, because the mapping
would have to be stored in the `grind` goal objects, and it is not just
a simple mapping. After reverting everything, I would need to keep a
sequence of original variables that must be added to the mapping as we
re-introduce them, but eager case splits complicate this quite a bit.
The whole approach felt overly messy.

The new behavior `grind -revert` addresses all these issues. None of the
`grind` proofs in our test suite broke after we fixed the bugs exposed
by the new feature. That said, the traces and counterexamples produced
by `grind` are different. The new proof terms are also different.

Author: leodemoura

src/Init/Grind/Config.lean

@@ -167,6 +167,11 @@ structure Config where
   When `trace := true`, uses `sorry` to close unsolved branches.
   -/
   useSorry := true
+  /--
+  When `true`, it reverts all hypotheses during the preprocessing step,
+  and then reintroduces them while simplifying and applying eager `cases`.
+  -/
+  revert := false
   deriving Inhabited, BEq
 
 /--

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

@@ -10,17 +10,25 @@ import Lean.Meta.Tactic.Grind.Simp
 public section
 namespace Lean.Meta.Grind
 
-private partial def propagateInjEqs (eqs : Expr) (proof : Expr) : GoalM Unit := do
+private partial def propagateInjEqs (eqs : Expr) (proof : Expr) (generation : Nat) : GoalM Unit := do
   -- Remark: we must use `shareCommon` before using `pushEq` and `pushHEq`.
   -- This is needed because the result type of the injection theorem may allocate
   match_expr eqs with
   | And left right =>
-    propagateInjEqs left (.proj ``And 0 proof)
-    propagateInjEqs right (.proj ``And 1 proof)
+    propagateInjEqs left (.proj ``And 0 proof) generation
+    propagateInjEqs right (.proj ``And 1 proof) generation
   | Eq _ lhs rhs    =>
-    pushEq (← preprocessLight lhs) (← preprocessLight rhs) proof
+    let lhs ← preprocessLight lhs
+    let rhs ← preprocessLight rhs
+    internalize lhs generation
+    internalize rhs generation
+    pushEq lhs rhs proof
   | HEq _ lhs _ rhs =>
-    pushHEq (← preprocessLight lhs) (← preprocessLight rhs) proof
+    let lhs ← preprocessLight lhs
+    let rhs ← preprocessLight rhs
+    internalize lhs generation
+    internalize rhs generation
+    pushHEq lhs rhs proof
   | _ =>
    reportIssue! "unexpected injectivity theorem result type{indentExpr eqs}"
    return ()
@@ -51,7 +59,8 @@ def propagateCtor (a b : Expr) : GoalM Unit := do
     let mask := mask.set! (n-1) (some (← mkExpectedTypeHint (← mkEqProof a b) (← mkEq a b)))
     let injLemma ← mkAppOptM injDeclName mask
     let injLemmaType ← inferType injLemma
-    propagateInjEqs injLemmaType injLemma
+    let gen := max (← getGeneration a) (← getGeneration b)
+    propagateInjEqs injLemmaType injLemma gen
   else
     let .const declName _ := aType.getAppFn | return ()
     let noConfusionDeclName := Name.mkStr declName "noConfusion"

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

@@ -38,7 +38,7 @@ Similar to `Grind.preprocess`, but does not simplify `e` if
 We added this feature because it may be coming from external sources
 (e.g., manually applying an function induction principle before invoking `grind`).
 -/
-private def preprocessHypothesis (e : Expr) : GoalM Simp.Result := do
+def preprocessHypothesis (e : Expr) : GoalM Simp.Result := do
   if isMatchCondCandidate e then
     preprocess (markAsPreMatchCond e)
   else if let some c := isAlreadyNorm? e then

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

@@ -26,6 +26,8 @@ import Lean.Meta.Tactic.Grind.SimpUtil
 import Lean.Meta.Tactic.Grind.LawfulEqCmp
 import Lean.Meta.Tactic.Grind.ReflCmp
 import Lean.Meta.Tactic.Grind.PP
+import Lean.Meta.Tactic.Grind.Simp
+import Lean.Meta.Tactic.Grind.Core
 public section
 namespace Lean.Meta.Grind
 
@@ -199,19 +201,48 @@ def Result.toMessageData (result : Result) : MetaM MessageData := do
       msgs := msgs ++ [msg]
   return MessageData.joinSep msgs m!"\n"
 
+/--
+When `Config.revert := false`, we preprocess the hypotheses, and add them to the `grind` state.
+-/
+private def addHypotheses (goal : Goal) : GrindM Goal := GoalM.run' goal do
+  let mvarDecl ← goal.mvarId.getDecl
+  for localDecl in mvarDecl.lctx do
+    if (← isInconsistent) then return ()
+    let type := localDecl.type
+    if (← isProp type) then
+      let r ← preprocessHypothesis type
+      match r.proof? with
+      | none => add r.expr localDecl.toExpr
+      | some h => add r.expr <| mkApp4 (mkConst ``Eq.mp [0]) type r.expr h localDecl.toExpr
+    else
+      /-
+      **Note**: We must internalize local variables because their types may be empty, and may not be
+      referenced anywhere else. Example:
+      ```
+      example (a : { x : Int // x < 0 ∧ x > 0 }) : False := by grind
+      ```
+      -/
+      let e ← shareCommon localDecl.toExpr
+      internalize e 0
+  processNewFacts
+
 private def initCore (mvarId : MVarId) (params : Params) : GrindM Goal := do
   /-
   **Note**: We used to use `abstractMVars` and `clearImpDetails` here.
   These operations are now performed at `withProtectedMCtx`
   -/
   -- let mvarId ← mvarId.abstractMVars
   -- let mvarId ← mvarId.clearImplDetails
-  let mvarId ← if params.config.clean then pure mvarId else mvarId.markAccessible
-  let mvarId ← mvarId.revertAll
+  let mvarId ← if params.config.clean || !params.config.revert then pure mvarId else mvarId.markAccessible
+  let mvarId ← if params.config.revert then mvarId.revertAll else pure mvarId
   let mvarId ← mvarId.unfoldReducible
   let mvarId ← mvarId.betaReduce
   appendTagSuffix mvarId `grind
-  mkGoal mvarId params
+  let goal ← mkGoal mvarId params
+  if params.config.revert then
+    return goal
+  else
+    addHypotheses goal
 
 def mkResult (params : Params) (failure? : Option Goal) : GrindM Result := do
   let issues     := (← get).issues

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

@@ -95,6 +95,7 @@ A lighter version of `preprocess` which produces a definitionally equal term,
 but ensures assumptions made by `grind` are satisfied.
 -/
 def preprocessLight (e : Expr) : GoalM Expr := do
+  let e ← instantiateMVars e
   shareCommon (← canon (← normalizeLevels (← foldProjs (← eraseIrrelevantMData (← markNestedSubsingletons (← unfoldReducible e))))))
 
 end Lean.Meta.Grind

tests/lean/run/grind_11081.lean

@@ -27,7 +27,7 @@ open List
 error: `grind` failed
 case grind.1.1.1.1.1.1.1.1.1
 α : Type
-inst : (a b : α) → Decidable (a = b)
+inst : DecidableEq α
 l₁ l₂ : List α
 hl : l₂.Subperm l₁
 p : α → Bool

tests/lean/run/grind_11124.lean

@@ -113,7 +113,7 @@ error: `grind` failed
 case grind.1.1.2.2.1.1.1
 α : Type
 β : α → Type
-inst : (a b : α) → Decidable (a = b)
+inst : DecidableEq α
 s₁ s₂ : AList β
 h : s₁.Disjoint s₂
 x : α

tests/lean/run/grind_11134.lean

@@ -72,7 +72,7 @@ inst_1 : One α
 inst_2 : Zero α
 x y : α
 h : DvdNotUnit x y
-hx0 : ¬x = 0
+hx0 : x ≠ 0
 d : α
 hdu : ¬IsUnit d
 hdx : y = x * d

tests/lean/run/grind_const_pattern.lean

@@ -76,9 +76,9 @@ h : ¬f x = 11
   [ematch] E-matching patterns
     [thm] fa: [f `[a]]
   [cutsat] Assignment satisfying linear constraints
-    [assign] x := 3
-    [assign] a := 2
-    [assign] f x := 1
+    [assign] x := 1
+    [assign] a := 3
+    [assign] f x := 2
 -/
 #guard_msgs (error) in
 example : f x = 10 + 1 := by

tests/lean/run/grind_cutsat_le_2.lean

@@ -15,6 +15,7 @@ trace: [grind.lia.model] a := 7
 [grind.lia.model] b := 0
 [grind.lia.model] c := 3
 [grind.lia.model] d := 2
+[grind.lia.model] e := 4
 -/
 #guard_msgs (trace) in
 example (a b c d e : Int) :