feat: implement try? using evalAndSuggest

src/Lean/Elab/Tactic/Grind.lean

@@ -158,21 +158,17 @@ private def elabFallback (fallback? : Option Term) : TermElabM (Grind.GoalM Unit
 
 def evalGrindCore
     (ref : Syntax)
-    (config : TSyntax `Lean.Parser.Tactic.optConfig)
+    (config : Grind.Config)
     (only : Option Syntax)
     (params : Option (Syntax.TSepArray `Lean.Parser.Tactic.grindParam ","))
     (fallback? : Option Term)
-    (trace : Bool)
     : TacticM Grind.Trace := do
   let fallback ← elabFallback fallback?
   let only := only.isSome
   let params := if let some params := params then params.getElems else #[]
   if Grind.grind.warning.get (← getOptions) then
     logWarningAt ref "The `grind` tactic is experimental and still under development. Avoid using it in production projects"
   let declName := (← Term.getDeclName?).getD `_grind
-  let mut config ← elabGrindConfig config
-  if trace then
-    config := { config with trace }
   withMainContext do
     let result ← grind (← getMainGoal) config only params declName fallback
     replaceMainGoal []
@@ -231,14 +227,17 @@ def mkGrindOnly
 @[builtin_tactic Lean.Parser.Tactic.grind] def evalGrind : Tactic := fun stx => do
   match stx with
   | `(tactic| grind $config:optConfig $[only%$only]?  $[ [$params:grindParam,*] ]? $[on_failure $fallback?]?) =>
-    discard <| evalGrindCore stx config only params fallback? false
+    let config ← elabGrindConfig config
+    discard <| evalGrindCore stx config only params fallback?
   | _ => throwUnsupportedSyntax
 
 @[builtin_tactic Lean.Parser.Tactic.grindTrace] def evalGrindTrace : Tactic := fun stx => do
   match stx with
-  | `(tactic| grind?%$tk $config:optConfig $[only%$only]?  $[ [$params:grindParam,*] ]? $[on_failure $fallback?]?) =>
-    let trace ← evalGrindCore stx config only params fallback? true
-    let stx ← mkGrindOnly config fallback? trace
+  | `(tactic| grind?%$tk $configStx:optConfig $[only%$only]?  $[ [$params:grindParam,*] ]? $[on_failure $fallback?]?) =>
+    let config ← elabGrindConfig configStx
+    let config := { config with trace := true }
+    let trace ← evalGrindCore stx config only params fallback?
+    let stx ← mkGrindOnly configStx fallback? trace
     Tactic.TryThis.addSuggestion tk stx (origSpan? := ← getRef)
   | _ => throwUnsupportedSyntax
 

src/Lean/Elab/Tactic/Try.lean

@@ -171,9 +171,13 @@ private def simpTraceToSimp (tac : TSyntax `tactic) : TacticM (TSyntax `tactic)
 
 private def evalSuggestGrindTrace (tac : TSyntax `tactic) : TacticM (TSyntax `tactic) := do
   match tac with
-  | `(tactic| grind? $config:optConfig $[only%$only]?  $[ [$params:grindParam,*] ]? $[on_failure $fallback?]?) =>
-    let trace ← evalGrindCore tac config only params fallback? true
-    mkGrindOnly config fallback? trace
+  | `(tactic| grind? $configStx:optConfig $[only%$only]?  $[ [$params:grindParam,*] ]? $[on_failure $fallback?]?) =>
+    let config ← elabGrindConfig configStx
+    let config := { config with trace := true, verbose := false }
+    let trace ← evalGrindCore tac config only params fallback?
+    let tac ← grindTraceToGrind tac
+    let tac' ← mkGrindOnly configStx fallback? trace
+    mkTrySuggestions #[tac, tac']
   | _ => throwUnsupportedSyntax
 
 private def evalSuggestSimpTrace (tac : TSyntax `tactic) : TacticM (TSyntax `tactic) := withMainContext do
@@ -182,7 +186,8 @@ private def evalSuggestSimpTrace (tac : TSyntax `tactic) : TacticM (TSyntax `tac
     let tac ← simpTraceToSimp tac
     let { ctx, simprocs, .. } ← mkSimpContext tac (eraseLocal := false)
     let stats ← simpLocation ctx (simprocs := simprocs) none <| (loc.map expandLocation).getD (.targets #[] true)
-    mkSimpCallStx tac stats.usedTheorems
+    let tac' ← mkSimpCallStx tac stats.usedTheorems
+    mkTrySuggestions #[tac, tac']
   | _ => throwUnsupportedSyntax
 
 abbrev TacticResult (α : Type) := EStateM.Result Exception SavedState α
@@ -317,151 +322,103 @@ def evalAndSuggest (tk : Syntax) (tac : TSyntax `tactic) : TacticM Unit := do
   else
     addSuggestions tk s
 
--- TODO: rewrite the following code using `evalSuggest`
-
-structure Try.Context where
-  mvarId : MVarId
-  config : Try.Config
-  tk     : Syntax
+/-! Helper functions -/
 
-private abbrev M := ReaderT Try.Context TacticM
+/-- Converts a declaraion name into an identifier. -/
+private def toIdent (declName : Name) : MetaM Ident := do
+  return mkIdent (← unresolveNameGlobalAvoidingLocals declName)
 
-instance : OrElse (M α) where
-  orElse a b := fun ctx => a ctx <|> b () ctx
+private def mkFirstStx (tacs : Array (TSyntax `tactic)) : CoreM (TSyntax `tactic) :=
+  if tacs.size = 1 then
+    return tacs[0]!
+  else
+    `(tactic| first $[| $tacs:tactic]*)
 
-open Tactic in
-private def addSuggestion (stx : TryThis.Suggestion) : M Bool := do
-  TryThis.addSuggestion (← read).tk stx (origSpan? := (← getRef))
-  return true
+/-! `grind` tactic syntax generator based on collected information. -/
 
--- TODO: vanilla `induction`.
--- TODO: cleanup the whole file, and use better combinators
--- TODO: make it extensible.
--- TODO: librarySearch integration.
--- TODO: premise selection.
+/-- Given a `grind` tactic syntax `tac`, sets its parameters using `params`. -/
+private def setGrindParams (tac : TSyntax `tactic) (params : Array (TSyntax ``Parser.Tactic.grindParam)) : TSyntax `tactic :=
+  let paramsStx := #[mkAtom "[", (mkAtom ",").mkSep params, mkAtom "]"]
+  ⟨tac.raw.setArg 3 (mkNullNode paramsStx)⟩
 
-private def failed (msg : MessageData) : M Bool := do
-  trace[«try»] msg
-  return false
+/-- Given a set of declaration names, returns `grind` parameters of the form `= <declName>` -/
+private def mkGrindEqnParams (declNames : Std.HashSet Name) : MetaM (Array (TSyntax ``Parser.Tactic.grindParam)) := do
+  declNames.toArray.mapM fun declName => do
+    `(Parser.Tactic.grindParam| = $(← toIdent declName))
 
-private def tryTac (stx : TSyntax `tactic) (msg : MessageData) : M Bool :=
-  (do
-    focusAndDone <| evalTactic stx
-    addSuggestion stx)
-  <|> failed msg
+private def mkGrindStx (info : Try.Info) : MetaM (TSyntax `tactic) := do
+  let grind ← `(tactic| grind?)
+  let mut tacs := #[grind]
+  unless info.eqnCandidates.isEmpty do
+    tacs := tacs.push (setGrindParams grind (← mkGrindEqnParams info.eqnCandidates))
+  unless info.unfoldCandidates.isEmpty do
+    tacs := tacs.push (setGrindParams grind (← mkGrindEqnParams info.unfoldCandidates))
+  mkFirstStx tacs
 
-private def trySimp : M Bool := do
-  tryTac (← `(tactic| simp)) "`simp` failed"
+/-! Other generators -/
 
-set_option hygiene false in
-private def trySimpArith : M Bool := do
-  tryTac (← `(tactic| simp +arith)) "`simp +arith` failed"
+set_option hygiene false in -- Avoid tagger at `+arith`
+/-- `simp` tactic syntax generator -/
+private def mkSimpStx : CoreM (TSyntax `tactic) :=
+  `(tactic| first | simp?; done | simp? +arith; done | simp_all; done)
 
-private def tryGrind : M Bool := do
-  (do
-    evalTactic (← `(tactic| grind -verbose))
-    addSuggestion (← `(tactic| grind?)))
-  <|> failed "`grind` failed"
+/-- `simple` tactics -/
+private def mkSimpleTacStx : CoreM (TSyntax `tactic) :=
+  `(tactic| attempt_all | rfl | assumption | contradiction)
 
-private def collect : M Try.Info := do
-  Try.collect (← read).mvarId (← read).config
+/-! Function induction generators -/
 
-private def toIdent (declName : Name) : MetaM Ident := do
-  return mkIdent (← unresolveNameGlobalAvoidingLocals declName)
+private def allAccessible (majors : Array FVarId) : MetaM Bool :=
+  majors.allM fun major => do
+    let localDecl ← major.getDecl
+    if localDecl.userName.hasMacroScopes then
+      return false
+    else
+      -- Check whether variable has been shadowed
+      let some localDecl' := (← getLCtx).findFromUserName? localDecl.userName
+        | return false
+      return localDecl'.fvarId == localDecl.fvarId
 
-inductive TacticKind where
-  | exec
-  | suggestion
-  | error
-
-private def mkGrindStx (params : Array (TSyntax ``Parser.Tactic.grindParam)) (kind : TacticKind) : MetaM (TSyntax `tactic) := do
-  let result ← match kind with
-    | .exec => `(tactic| grind -verbose)
-    | .suggestion => `(tactic| grind?)
-    | .error => `(tactic| grind)
-  if params.isEmpty then
-    return result
+open Try.Collector in
+private def mkFunIndStx (c : FunIndCandidate) (cont : TSyntax `tactic) : MetaM (TSyntax `tactic) := do
+  if (← allAccessible c.majors) then
+    let mut terms := #[]
+    for major in c.majors do
+      let localDecl ← major.getDecl
+      terms := terms.push (← `($(mkIdent localDecl.userName):term))
+    let indFn ← toIdent c.funIndDeclName
+    `(tactic| induction $terms,* using $indFn <;> $cont)
   else
-    let paramsStx := #[mkAtom "[", (mkAtom ",").mkSep params, mkAtom "]"]
-    return ⟨result.raw.setArg 3 (mkNullNode paramsStx)⟩
-
-private def mkGrindEqnsStx (declNames : Std.HashSet Name) : M (TacticKind → MetaM (TSyntax `tactic)) := do
-  let mut params := #[]
-  for declName in declNames do
-    params := params.push (← `(Parser.Tactic.grindParam| = $(← toIdent declName)))
-  return mkGrindStx params
-
-private def tryTac' (mkTac : TacticKind → MetaM (TSyntax `tactic)) : M Bool := do
-  let stx ← mkTac .exec
-  (do
-    focusAndDone <| evalTactic stx
-    addSuggestion (← mkTac .suggestion))
-  <|>
-  (do failed m!"`{← mkTac .error}` failed")
+    -- TODO: use `expose_names`
+    throwError "`induction` failed, majors contain inaccessible vars"
 
-private def tryGrindEqns (info : Try.Info) : M Bool := do
-  if info.eqnCandidates.isEmpty then return false
-  tryTac' (← mkGrindEqnsStx info.eqnCandidates)
+private def mkAllFunIndStx (info : Try.Info) (cont : TSyntax `tactic) : MetaM (TSyntax `tactic) := do
+  let tacs ← info.funIndCandidates.toArray.mapM (mkFunIndStx · cont)
+  mkFirstStx tacs
 
-private def tryGrindUnfold (info : Try.Info) : M Bool := do
-  if info.unfoldCandidates.isEmpty then return false
-  tryTac' (← mkGrindEqnsStx info.unfoldCandidates)
+/-! Main code -/
 
-private def allAccessible (majors : Array FVarId) : MetaM Bool :=
-  majors.allM fun major => do
-    let localDecl ← major.getDecl
-    -- TODO: we are not checking shadowed variables
-    return !localDecl.userName.hasMacroScopes
+/-- Returns tactic for `evalAndSuggest` -/
+private def mkTryEvalSuggestStx (info : Try.Info) : MetaM (TSyntax `tactic) := do
+  let simple ← mkSimpleTacStx
+  let simp ← mkSimpStx
+  let grind ← mkGrindStx info
+  let atomic ← `(tactic| attempt_all | $simple:tactic | $simp:tactic | $grind:tactic)
+  let funInds ← mkAllFunIndStx info atomic
+  `(tactic| first | $atomic:tactic | $funInds:tactic)
 
-open Try.Collector in
-private partial def tryFunIndsCore (info : Try.Info) (mkBody : TacticKind → MetaM (TSyntax `tactic)) : M Bool := do
-  go info.funIndCandidates.toList
-where
-  go' (c : FunIndCandidate) : M Bool := do
-    if (← allAccessible c.majors) then
-      let mut terms := #[]
-      for major in c.majors do
-        let localDecl ← major.getDecl
-        terms := terms.push (← `($(mkIdent localDecl.userName):term))
-      let indFn ← toIdent c.funIndDeclName
-      tryTac' fun k => do
-        let body ← mkBody k
-        `(tactic| induction $terms,* using $indFn <;> $body)
-    else
-      -- TODO: use `rename_i`
-      failed "`induction` failed, majors contain inaccessible vars {c.majors.map mkFVar}"
-
-  go (cs : List FunIndCandidate) : M Bool := do
-    match cs with
-    | [] => return false
-    | c::cs =>
-      trace[try.debug.funInd] "{c.funIndDeclName}, {c.majors.map mkFVar}"
-      go' c <||> go cs
-
-private partial def tryFunIndsGrind (info : Try.Info) : M Bool :=
-  tryFunIndsCore info (mkGrindStx #[])
-
-private partial def tryFunIndsGrindEqns (info : Try.Info) : M Bool := do
-  if info.eqnCandidates.isEmpty then return false
-  tryFunIndsCore info (← mkGrindEqnsStx info.eqnCandidates)
-
-private def evalTryTraceCore : M Unit := do
-  if (← trySimp) then return ()
-  if (← trySimpArith) then return ()
-  if (← tryGrind) then return ()
-  let info ← collect
-  if (← tryGrindEqns info) then return ()
-  if (← tryGrindUnfold info) then return ()
-  if (← tryFunIndsGrind info) then return ()
-  if (← tryFunIndsGrindEqns info) then return ()
-  Meta.throwTacticEx `«try?» (← read).mvarId "consider using `grind` manually, `set_option trace.try true` shows everything `try?` tried"
+-- TODO: vanilla `induction`.
+-- TODO: make it extensible.
+-- TODO: librarySearch integration.
+-- TODO: premise selection.
 
 @[builtin_tactic Lean.Parser.Tactic.tryTrace] def evalTryTrace : Tactic := fun stx => do
   match stx with
-  | `(tactic| try?%$tk $config:optConfig) =>
-    let mvarId ← getMainGoal
+  | `(tactic| try?%$tk $config:optConfig) => focus do withMainContext do
     let config ← elabTryConfig config
-    evalTryTraceCore { config, tk, mvarId }
+    let info ← Try.collect (← getMainGoal) config
+    let stx ← mkTryEvalSuggestStx info
+    evalAndSuggest tk stx
   | _ => throwUnsupportedSyntax
 
 end Lean.Elab.Tactic

tests/lean/run/eval_suggest1.lean

@@ -6,14 +6,15 @@ elab tk:"eval_suggest" tac:tactic : tactic => do
   evalAndSuggest tk tac
 
 set_option hygiene false in
-macro "try_simple?" : tactic => `(tactic| eval_suggest (intros; attempt_all | rfl | (first | simp; done | simp +arith; done) | grind | grind?))
+macro "try_simple?" : tactic => `(tactic| eval_suggest (intros; attempt_all | rfl | (first | simp?; done | simp? +arith; done | simp_all) | grind?))
 
 opaque f : Nat → Nat
 @[simp, grind =] theorem fthm : f x = x := sorry
 
 /--
 info: Try these:
 • simp +arith
+• simp +arith only [Nat.reduceAdd, fthm]
 • grind
 • grind only [= fthm]
 -/
@@ -25,6 +26,7 @@ example (x : Nat) : 1 + 1 + f x = x + 2 := by
 info: Try these:
 • rfl
 • simp
+• simp only [Nat.succ_eq_add_one]
 • grind
 • grind only
 -/
@@ -36,9 +38,20 @@ example (x : Nat) : x + 1 = Nat.succ x := by
 info: Try these:
 • · intros; rfl
 • · intros; simp
+• · intros; simp only [Nat.succ_eq_add_one]
 • · intros; grind
 • · intros; grind only
 -/
 #guard_msgs (info) in
 example (x : Nat) : True → x + 1 = Nat.succ x := by
   try_simple?
+
+/--
+info: Try these:
+• simp_all
+• grind
+• grind only
+-/
+#guard_msgs (info) in
+example (h : 0 + x = y) : f x = f y := by
+  try_simple?

tests/lean/run/grind_constProp.lean

@@ -140,12 +140,12 @@ set_option hygiene false -- HACK: allow forward reference in notation
 local notation:60 "(" σ ", " s ")"  " ⇓ " σ':60 => Bigstep σ s σ'
 
 inductive Bigstep : State → Stmt → State → Prop where
-  | skip       : (σ, .skip) ⇓ σ
-  | assign     : e.eval σ = some v → (σ,  x ::= e) ⇓ σ.update x v
-  | seq        : (σ₁, s₁) ⇓ σ₂ → (σ₂, s₂) ⇓ σ₃ → (σ₁, s₁ ;; s₂) ⇓ σ₃
-  | ifTrue     : evalTrue c σ₁ → (σ₁, t) ⇓ σ₂ → (σ₁, .ite c t e) ⇓ σ₂
-  | ifFalse    : evalFalse c σ₁ → (σ₁, e) ⇓ σ₂ → (σ₁, .ite c t e) ⇓ σ₂
-  | whileTrue  : evalTrue c σ₁ → (σ₁, b) ⇓ σ₂ → (σ₂, .while c b) ⇓ σ₃ → (σ₁, .while c b) ⇓ σ₃
+  | skip : (σ, .skip) ⇓ σ
+  | assign: e.eval σ = some v → (σ,  x ::= e) ⇓ σ.update x v
+  | seq : (σ₁, s₁) ⇓ σ₂ → (σ₂, s₂) ⇓ σ₃ → (σ₁, s₁ ;; s₂) ⇓ σ₃
+  | ifTrue : evalTrue c σ₁ → (σ₁, t) ⇓ σ₂ → (σ₁, .ite c t e) ⇓ σ₂
+  | ifFalse : evalFalse c σ₁ → (σ₁, e) ⇓ σ₂ → (σ₁, .ite c t e) ⇓ σ₂
+  | whileTrue : evalTrue c σ₁ → (σ₁, b) ⇓ σ₂ → (σ₂, .while c b) ⇓ σ₃ → (σ₁, .while c b) ⇓ σ₃
   | whileFalse : evalFalse c σ → (σ, .while c b) ⇓ σ
 
 end
@@ -205,7 +205,7 @@ def evalExpr (e : Expr) : EvalM Val := do
 @[grind] theorem UnaryOp.simplify_eval (op : UnaryOp) : (op.simplify a).eval σ = (Expr.una op a).eval σ := by
   grind [UnaryOp.simplify.eq_def]
 
-/-- info: Try this: (induction e using Expr.simplify.induct) <;> grind? -/
+/-- info: Try this: (induction e using Expr.simplify.induct) <;> grind -/
 #guard_msgs (info) in
 example (e : Expr) : e.simplify.eval σ = e.eval σ := by
   try?
@@ -304,7 +304,7 @@ theorem State.cons_le_of_eq (h₁ : σ' ≼ σ) (h₂ : σ.find? x = some v) : (
 @[grind] theorem State.join_le_left_of (h : σ₁ ≼ σ₂) (σ₃ : State) : σ₁.join σ₃ ≼ σ₂ := by
   grind
 
-/-- info: Try this: (induction σ₁, σ₂ using State.join.induct) <;> grind? -/
+/-- info: Try this: (induction σ₁, σ₂ using State.join.induct) <;> grind -/
 #guard_msgs (info) in
 example (σ₁ σ₂ : State) : σ₁.join σ₂ ≼ σ₂ := by
   try?