refactor: port Grind/Intro.lean to SearchM

Author: leodemoura

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

@@ -12,7 +12,8 @@ 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
+import Lean.Meta.Tactic.Grind.Combinators -- TODO: delete
 
 namespace Lean.Meta.Grind
 
@@ -196,6 +197,96 @@ private def exfalsoIfNotProp (goal : Goal) : MetaM Goal := goal.mvarId.withConte
   else
     return { goal with mvarId := (← goal.mvarId.exfalso) }
 
+private def applyCases? (fvarId : FVarId) : 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
+    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 := do
+  repeat
+    if (← isInconsistent) then
+      return ()
+    match (← introNext (← getGoal) generation) with
+    | .done goal =>
+      let goal ← exfalsoIfNotProp goal
+      if let some mvarId ← goal.mvarId.byContra? then
+        setGoal { goal with mvarId }
+      else
+        setGoal goal
+        return ()
+    | .newDepHyp goal =>
+      setGoal goal
+    | .newLocal fvarId goal =>
+      setGoal goal
+      discard <| applyCases? fvarId
+    | .newHyp fvarId goal =>
+      if let some goal ← applyInjection? goal fvarId then
+        setGoal goal
+      else
+        setGoal goal
+        withCurrGoalContext do
+        unless (← applyCases? fvarId) do
+          addHypothesis fvarId generation
+
+/-- Asserts a new fact `prop` with proof `proof` to the given `goal`. -/
+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
+    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.
+Returns `true` if the queue was not empty and `false` otherwise.
+-/
+def assertNext : SearchM Bool := do
+  let goal ← getGoal
+  let some (fact, newRawFacts) := goal.newRawFacts.dequeue?
+    | return false
+  setGoal { goal with newRawFacts }
+  assertAt fact.proof fact.prop fact.generation
+  return true
+
+/--
+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!
+
+/-! All functions after this point will be deleted after we move to `SearchM` -/
+
 private def applyCasesOld? (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.

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

@@ -20,9 +20,9 @@ structure Choice where
   /--
   Expression to be assigned to `goalOld.mvarId` if it is not possible to perform
   non-chronological backtracking.
-  `val` is often a `casesOn` application.
+  `proof` is often a `casesOn` application containing meta-variables.
   -/
-  val      : Expr
+  proof    : Expr
   /--
   Subgoals that still need to be processed.
   -/
@@ -35,6 +35,15 @@ structure SearchM.State where
 
 abbrev SearchM := StateRefT SearchM.State GrindM
 
+def getGoal : SearchM Goal :=
+  return (← get).goal
+
+def setGoal (goal : Goal) : SearchM Unit :=
+  modify fun s => { s with goal }
+
+abbrev withCurrGoalContext (x : SearchM α) : SearchM α := do
+  (← getGoal).mvarId.withContext x
+
 abbrev liftGoalM (x : GoalM α) : SearchM α := do
   let (a, goal) ← x.runCore (← get).goal
   modify fun s => { s with goal }
@@ -46,6 +55,42 @@ instance : MonadLift GoalM SearchM where
 @[inline] def SearchM.run (goal : Goal) (x : SearchM α) : GrindM (α × SearchM.State) :=
   goal.mvarId.withContext do StateRefT'.run x { goal }
 
+/--
+Given a proof containing meta-variables corresponding to the given subgoals,
+create a choice point.
+- If there are no choice points, we just close the current goal using `proof`.
+- If there is only one subgoal `s`, we close the current goal using `proof`, and
+update current goal using `s`.
+- If there are more than one `s :: ss`, we create a choice point using the current
+goal as the pending goal, and update the current goal with `s`.
+-/
+def mkChoice (proof : Expr) (subgoals : List Goal) : SearchM Unit := do
+  assert! !(← isInconsistent)
+  match subgoals with
+  | [] =>
+    (← getGoal).mvarId.assign proof
+  | [subgoal] =>
+    (← getGoal).mvarId.assign proof
+    setGoal subgoal
+  | subgoal :: subgoals =>
+    let goalPending ← getGoal
+    modify fun s => { s with
+      goal := subgoal
+      choiceStack := { goalPending, proof, todo := subgoals } :: s.choiceStack
+    }
+
+/--
+Create an auxiliary metavariable with the same type and tag of the metavariable
+associated with the current goal.
+We use this function to perform `cases` on the current goal without eagerly assignining it.
+-/
+def mkAuxMVarForCurrGoal : SearchM MVarId := withCurrGoalContext do
+  let mvarId := (← getGoal).mvarId
+  let tag ← mvarId.getTag
+  let type ← mvarId.getType
+  let mvarNew ← mkFreshExprSyntheticOpaqueMVar type tag
+  return mvarNew.mvarId!
+
 private def findMaxFVarIdx? (e : Expr) : MetaM (Option Nat) := do
   let go (e : Expr) : StateT (Option Nat) MetaM Bool := do
     unless e.hasFVar do return false
@@ -90,7 +135,7 @@ private def nextChronoGoal : SearchM Bool := do
       | [] =>
         -- Choice point has been fully resolved.
         -- Go to next one.
-        choice.goalPending.mvarId.assign choice.val
+        choice.goalPending.mvarId.assign choice.proof
         choices := choices'
       | goal :: todo =>
         let choice := { choice with todo }
@@ -144,8 +189,8 @@ def nextGoal : SearchM Bool := do
       choices := choices'
     else match choice.todo with
       | [] =>
-        -- All subgoals have been solved. We can finally assign `choice.val` to `goalOld.mvarId`.
-        let proof ← instantiateMVars choice.val
+        -- All subgoals have been solved. We can finally assign `choice.proof` to `goalOld.mvarId`.
+        let proof ← instantiateMVars choice.proof
         choice.goalPending.mvarId.assign proof
         if (← isTargetFalse choice.goalPending.mvarId) then
           -- `proof` is a proof of `False`, we can continue using non-chronological backtracking