feat: non-chronological backtracking for grind (WIP) (#8440)

This PR implements non-chronological backtracking for the `grind`
tactic. This feature ensures that `grind` does not need to process
irrelevant branches after performing a case-split that is not relevant.
It is not just about performance, but also the size of the final proof
term. The new test demonstrates this feature in practice.
```lean
-- In the following test, the first 8 case-splits are irrelevant,
-- and non-choronological backtracking is used to avoid searching
-- (2^8 - 1) irrelevant branches
/--
trace: 
[grind.split] p8 ∨ q8, generation: 0
[grind.split] p7 ∨ q7, generation: 0
[grind.split] p6 ∨ q6, generation: 0
[grind.split] p5 ∨ q5, generation: 0
[grind.split] p4 ∨ q4, generation: 0
[grind.split] p3 ∨ q3, generation: 0
[grind.split] p2 ∨ q2, generation: 0
[grind.split] p1 ∨ q1, generation: 0
[grind.split] ¬p ∨ ¬q, generation: 0
-/
#guard_msgs (trace) in
set_option trace.grind.split true in
theorem ex
    : p ∨ q →
      ¬ p ∨ q →
      p ∨ ¬ q →
      ¬ p ∨ ¬ q →
      p1 ∨ q1 →
      p2 ∨ q2 →
      p3 ∨ q3 →
      p4 ∨ q4 →
      p5 ∨ q5 →
      p6 ∨ q6 →
      p7 ∨ q7 →
      p8 ∨ q8 →
      False := by
  grind (splits := 10)
```

Author: leodemoura

src/Init/MetaTypes.lean

@@ -244,6 +244,11 @@ structure Config where
   `let x := v; e` simplifies to `e` when `x` does not occur in `e`.
   -/
   zetaUnused : Bool := true
+  /--
+  When `true` (default : `true`), then simps will catch runtime exceptions and
+  convert them into `simp` exceptions.
+  -/
+  catchRuntime : Bool := true
   deriving Inhabited, BEq
 
 -- Configuration object for `simp_all`

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/MBTC.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import Lean.Meta.Tactic.Grind.Combinators
 import Lean.Meta.Tactic.Grind.Canon
 import Lean.Meta.Tactic.Grind.MBTC
 import Lean.Meta.Tactic.Grind.Arith.Cutsat.Model
@@ -36,8 +35,8 @@ private def eqAssignment (a b : Expr) : GoalM Bool := do
   let some v₂ ← getAssignmentExt? b | return false
   return v₁ == v₂
 
-def mbtcTac : GrindTactic :=
-  Grind.mbtcTac {
+def mbtc : GoalM Bool := do
+  Grind.mbtc {
     hasTheoryVar := hasTheoryVar
     isInterpreted := isInterpreted
     eqAssignment := eqAssignment

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

@@ -5,7 +5,6 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Lean.Meta.Tactic.Grind.PropagatorAttr
-import Lean.Meta.Tactic.Grind.Combinators
 import Lean.Meta.Tactic.Grind.Arith.Offset
 import Lean.Meta.Tactic.Grind.Arith.Cutsat.LeCnstr
 import Lean.Meta.Tactic.Grind.Arith.Cutsat.Search
@@ -37,20 +36,13 @@ builtin_grind_propagator propagateLE ↓LE.le := fun e => do
       Offset.assertFalse c (← mkEqFalseProof e)
     Cutsat.propagateIfSupportedLe e (eqTrue := false)
 
-def check : GrindTactic := fun goal => do
-  let (progress, goal) ← GoalM.run goal do
-    let c₁ ← Cutsat.check
-    let c₂ ← CommRing.check
-    if c₁ || c₂ then
-      processNewFacts
-      return true
-    else
-      return false
-  unless progress do
-    return none
-  if goal.inconsistent then
-    return some []
+def check : GoalM Bool := do
+  let c₁ ← Cutsat.check
+  let c₂ ← CommRing.check
+  if c₁ || c₂ then
+    processNewFacts
+    return true
   else
-    return some [goal]
+    return false
 
 end Lean.Meta.Grind.Arith

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

@@ -150,6 +150,10 @@ def cases (mvarId : MVarId) (e : Expr) : MetaM (List MVarId) := mvarId.withConte
   let k (mvarId : MVarId) (fvarId : FVarId) (indices : Array FVarId) : MetaM (List MVarId) := do
     let indicesExpr := indices.map mkFVar
     let recursor ← mkRecursorAppPrefix mvarId `grind.cases fvarId recursorInfo indicesExpr
+    let lctx ← getLCtx
+    let lctx := lctx.setKind fvarId .implDetail
+    let lctx := indices.foldl (init := lctx) fun lctx fvarId => lctx.setKind fvarId .implDetail
+    let localInsts ← getLocalInstances
     let mut recursor := mkApp (mkAppN recursor indicesExpr) (mkFVar fvarId)
     let mut recursorType ← inferType recursor
     let mut mvarIdsNew := #[]
@@ -159,10 +163,9 @@ def cases (mvarId : MVarId) (e : Expr) : MetaM (List MVarId) := mvarId.withConte
         | throwTacticEx `grind.cases mvarId "unexpected recursor type"
       recursorType := recursorTypeNew
       let tagNew := if recursorInfo.numMinors > 1 then Name.num tag idx else tag
-      let mvar ← mkFreshExprSyntheticOpaqueMVar targetNew tagNew
+      let mvar ← mkFreshExprMVarAt lctx localInsts targetNew .syntheticOpaque tagNew
       recursor := mkApp recursor mvar
-      let mvarIdNew ← mvar.mvarId!.tryClearMany (indices.push fvarId)
-      mvarIdsNew := mvarIdsNew.push mvarIdNew
+      mvarIdsNew := mvarIdsNew.push mvar.mvarId!
       idx := idx + 1
     mvarId.assign recursor
     return mvarIdsNew.toList

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

@@ -489,13 +489,10 @@ private def ematchCore : GoalM Unit := do
       ematch.num       := s.ematch.num + 1
     }
 
-/-- Performs one round of E-matching. -/
-def ematch : GrindTactic := fun goal => do
-  let numInstances := goal.ematch.numInstances
-  let goal ← GoalM.run' goal ematchCore
-  if goal.ematch.numInstances == numInstances then
-    return none
-  else
-    return [goal]
+/-- Performs one round of E-matching, and returns `true` if new instances were generated. -/
+def ematch : GoalM Bool := do
+  let numInstances := (← get).ematch.numInstances
+  ematchCore
+  return (← get).ematch.numInstances != numInstances
 
 end Lean.Meta.Grind

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

@@ -12,7 +12,7 @@ import Lean.Meta.Tactic.Grind.Cases
 import Lean.Meta.Tactic.Grind.CasesMatch
 import Lean.Meta.Tactic.Grind.Injection
 import Lean.Meta.Tactic.Grind.Core
-import Lean.Meta.Tactic.Grind.Combinators
+import Lean.Meta.Tactic.Grind.SearchM
 
 namespace Lean.Meta.Grind
 
@@ -184,23 +184,6 @@ private def isCheapInductive (type : Expr) : CoreM Bool := do
   let .inductInfo info ← getConstInfo declName | return false
   return info.numCtors <= 1
 
-private def applyCases? (goal : Goal) (fvarId : FVarId) : GrindM (Option (List Goal)) := goal.mvarId.withContext do
-  /-
-  Remark: we used to use `whnfD`. This was a mistake, we don't want to unfold user-defined abstractions.
-  Example: `a ∣ b` is defined as `∃ x, b = a * x`
-  -/
-  let type ← whnf (← fvarId.getType)
-  if isEagerCasesCandidate goal type then
-    if (← cheapCasesOnly) then
-      unless (← isCheapInductive type) do
-        return none
-    if let .const declName _ := type.getAppFn then
-      saveCases declName true
-    let mvarIds ← cases goal.mvarId (mkFVar fvarId)
-    return mvarIds.map fun mvarId => { goal with mvarId }
-  else
-    return none
-
 private def applyInjection? (goal : Goal) (fvarId : FVarId) : MetaM (Option Goal) := do
   if let some mvarId ← injection? goal.mvarId fvarId then
     return some { goal with mvarId }
@@ -213,60 +196,104 @@ private def exfalsoIfNotProp (goal : Goal) : MetaM Goal := goal.mvarId.withConte
   else
     return { goal with mvarId := (← goal.mvarId.exfalso) }
 
-/-- Introduce new hypotheses (and apply `by_contra`) until goal is of the form `... ⊢ False` -/
-partial def intros (generation : Nat) : GrindTactic' := fun goal => do
-  let rec go (goal : Goal) : StateRefT (Array Goal) GrindM Unit := do
-    if goal.inconsistent then
+private def applyCases? (fvarId : FVarId) (generation : Nat) : SearchM Bool := withCurrGoalContext do
+  /-
+  Remark: we used to use `whnfD`. This was a mistake, we don't want to unfold user-defined abstractions.
+  Example: `a ∣ b` is defined as `∃ x, b = a * x`
+  -/
+  let type ← whnf (← fvarId.getType)
+  if isEagerCasesCandidate (← getGoal) type then
+    if (← cheapCasesOnly) then
+      unless (← isCheapInductive type) do
+        return false
+    if let .const declName _ := type.getAppFn then
+      saveCases declName true
+    let mvarId ← mkAuxMVarForCurrGoal
+    let mvarIds ← cases mvarId (mkFVar fvarId)
+    let goal ← getGoal
+    let goals := mvarIds.map fun mvarId => { goal with mvarId }
+    mkChoice (mkMVar mvarId) goals generation
+    return true
+  return false
+
+/--
+Introduce new hypotheses (and apply `by_contra`) until goal is of the form `... ⊢ False`
+or is inconsistent.
+-/
+def intros (generation : Nat) : SearchM Unit := withCurrGoalContext do
+  repeat
+    if (← isInconsistent) then
       return ()
-    match (← introNext goal generation) with
+    match (← introNext (← getGoal) generation) with
     | .done goal =>
       let goal ← exfalsoIfNotProp goal
       if let some mvarId ← goal.mvarId.byContra? then
-        go { goal with mvarId }
+        setGoal { goal with mvarId }
       else
-        modify fun s => s.push goal
-    | .newHyp fvarId goal =>
-      if let some goals ← applyCases? goal fvarId then
-        goals.forM go
-      else if let some goal ← applyInjection? goal fvarId then
-        go goal
-      else
-        go (← GoalM.run' goal <| addHypothesis fvarId generation)
+        setGoal goal
+        return ()
     | .newDepHyp goal =>
-      go goal
+      setGoal goal
     | .newLocal fvarId goal =>
-      if let some goals ← applyCases? goal fvarId then
-        goals.forM go
+      setGoal goal
+      discard <| applyCases? fvarId generation
+    | .newHyp fvarId goal =>
+      if let some goal ← applyInjection? goal fvarId then
+        setGoal goal
       else
-        go goal
-  let (_, goals) ← (go goal).run #[]
-  return goals.toList
+        setGoal goal
+        if (← applyCases? fvarId generation) then
+          pure ()
+        else
+          addHypothesis fvarId generation
+
+/--
+Similar to `intros`, but returns `true` if new hypotheses have been added,
+and `false` otherwise.
+-/
+def intros' (generation : Nat) : SearchM Bool := do
+  let target ← (← getGoal).mvarId.getType
+  if target.isFalse then return false
+  intros generation
+  return true
 
 /-- Asserts a new fact `prop` with proof `proof` to the given `goal`. -/
-def assertAt (proof : Expr) (prop : Expr) (generation : Nat) : GrindTactic' := fun goal => do
-  if isEagerCasesCandidate goal prop then
+def assertAt (proof : Expr) (prop : Expr) (generation : Nat) : SearchM Unit := do
+  if isEagerCasesCandidate (← getGoal) prop then
+    let goal ← getGoal
     let mvarId ← goal.mvarId.assert (← mkFreshUserName `h) prop proof
-    let goal := { goal with mvarId }
-    intros generation goal
-  else
-    let goal ← GoalM.run' goal do
-      let r ← preprocess prop
-      let prop' := r.expr
-      let proof' := mkApp4 (mkConst ``Eq.mp [levelZero]) prop r.expr (← r.getProof) proof
-      add prop' proof' generation
-    if goal.inconsistent then return [] else return [goal]
+    setGoal { goal with mvarId }
+    intros generation
+  else withCurrGoalContext do
+    let r ← preprocess prop
+    let prop' := r.expr
+    let proof' := mkApp4 (mkConst ``Eq.mp [levelZero]) prop r.expr (← r.getProof) proof
+    add prop' proof' generation
 
-/-- Asserts next fact in the `goal` fact queue. -/
-def assertNext : GrindTactic := fun goal => do
+/--
+Asserts next fact in the `goal` fact queue.
+Returns `true` if the queue was not empty and `false` otherwise.
+-/
+def assertNext : SearchM Bool := do
+  if (← isInconsistent) then return false
+  let goal ← getGoal
   let some (fact, newRawFacts) := goal.newRawFacts.dequeue?
-    | return none
-  assertAt fact.proof fact.prop fact.generation { goal with newRawFacts }
+    | return false
+  setGoal { goal with newRawFacts }
+  assertAt fact.proof fact.prop fact.generation
+  return true
 
-/-- Asserts all facts in the `goal` fact queue. -/
-partial def assertAll : GrindTactic := fun goal =>
-  if goal.newRawFacts.isEmpty then
-    return none
-  else
-    assertNext.iterate goal
+/--
+Asserts all facts in the `goal` fact queue.
+Returns `true` if the queue was not empty and `false` otherwise.
+-/
+def assertAll : SearchM Bool := do
+  let mut progress := false
+  repeat
+    if (← assertNext) then
+      progress := true
+    else
+      return progress
+  unreachable!
 
 end Lean.Meta.Grind