feat: implement try? using evalAndSuggest (#6965)

This PR re-implements the `try?` tactic using the new `evalAndSuggest` infrastructure.
2025-02-05 20:47:26 -08:00 · 2025-02-05 20:47:26 -08:00 · fbeec32c2b
commit fbeec32c2b
parent de99c8015a
5 changed files with 153 additions and 151 deletions
--- a/src/Lean/Elab/Tactic/Grind.lean
+++ b/src/Lean/Elab/Tactic/Grind.lean
@ -158,11 +158,10 @@ 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
@ -170,9 +169,6 @@ def evalGrindCore
  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

--- a/src/Lean/Elab/Tactic/Try.lean
+++ b/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
-
-private abbrev M := ReaderT Try.Context TacticM
-
-instance : OrElse (M α) where
-  orElse a b := fun ctx => a ctx <|> b () ctx
-
-open Tactic in
-private def addSuggestion (stx : TryThis.Suggestion) : M Bool := do
-  TryThis.addSuggestion (← read).tk stx (origSpan? := (← getRef))
-  return true
-
-- TODO: vanilla `induction`.
-- TODO: cleanup the whole file, and use better combinators
-- TODO: make it extensible.
-- TODO: librarySearch integration.
-- TODO: premise selection.
-
-private def failed (msg : MessageData) : M Bool := do
-  trace[«try»] msg
-  return false
-
-private def tryTac (stx : TSyntax `tactic) (msg : MessageData) : M Bool :=
-  (do
-    focusAndDone <| evalTactic stx
-    addSuggestion stx)
-  <|> failed msg
-
-private def trySimp : M Bool := do
-  tryTac (← `(tactic| simp)) "`simp` failed"
-
-set_option hygiene false in
-private def trySimpArith : M Bool := do
-  tryTac (← `(tactic| simp +arith)) "`simp +arith` failed"
-
-private def tryGrind : M Bool := do
-  (do
-    evalTactic (← `(tactic| grind -verbose))
-    addSuggestion (← `(tactic| grind?)))
-  <|> failed "`grind` failed"
-
-private def collect : M Try.Info := do
-  Try.collect (← read).mvarId (← read).config
+/-! Helper functions -/

+/-- Converts a declaraion name into an identifier. -/
 private def toIdent (declName : Name) : MetaM Ident := do
  return mkIdent (← unresolveNameGlobalAvoidingLocals declName)

-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
+private def mkFirstStx (tacs : Array (TSyntax `tactic)) : CoreM (TSyntax `tactic) :=
+  if tacs.size = 1 then
+    return tacs[0]!
  else
-    let paramsStx := #[mkAtom "[", (mkAtom ",").mkSep params, mkAtom "]"]
-    return ⟨result.raw.setArg 3 (mkNullNode paramsStx)⟩
+    `(tactic| first $[| $tacs:tactic]*)

-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
+/-! `grind` tactic syntax generator based on collected information. -/

-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")
+/-- 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 tryGrindEqns (info : Try.Info) : M Bool := do
-  if info.eqnCandidates.isEmpty then return false
-  tryTac' (← mkGrindEqnsStx info.eqnCandidates)
+/-- 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 tryGrindUnfold (info : Try.Info) : M Bool := do
-  if info.unfoldCandidates.isEmpty then return false
-  tryTac' (← mkGrindEqnsStx info.unfoldCandidates)
+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
+
+/-! Other generators -/
+
+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)
+
+/-- `simple` tactics -/
+private def mkSimpleTacStx : CoreM (TSyntax `tactic) :=
+  `(tactic| attempt_all | rfl | assumption | contradiction)
+
+/-! Function induction generators -/

 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
+    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

 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}"
+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
+    -- TODO: use `expose_names`
+    throwError "`induction` failed, majors contain inaccessible vars"

-  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 def mkAllFunIndStx (info : Try.Info) (cont : TSyntax `tactic) : MetaM (TSyntax `tactic) := do
+  let tacs ← info.funIndCandidates.toArray.mapM (mkFunIndStx · cont)
+  mkFirstStx tacs

-private partial def tryFunIndsGrind (info : Try.Info) : M Bool :=
-  tryFunIndsCore info (mkGrindStx #[])
+/-! Main code -/

-private partial def tryFunIndsGrindEqns (info : Try.Info) : M Bool := do
-  if info.eqnCandidates.isEmpty then return false
-  tryFunIndsCore info (← mkGrindEqnsStx info.eqnCandidates)
+/-- 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)

-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
--- a/tests/lean/run/eval_suggest1.lean
+++ b/tests/lean/run/eval_suggest1.lean
@ -6,7 +6,7 @@ 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
@ -14,6 +14,7 @@ opaque f : Nat → Nat
 /--
 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?
--- a/tests/lean/run/grind_constProp.lean
+++ b/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?
--- a/tests/lean/run/try_trace1.lean
+++ b/tests/lean/run/try_trace1.lean
@ -1,16 +1,32 @@
 set_option grind.warning false

-/-- info: Try this: simp -/
+/--
+info: Try these:
+• simp
+• simp only [ne_eq, reduceCtorEq, not_false_eq_true]
+• grind
+• grind only
+-/
 #guard_msgs (info) in
 example : [1, 2] ≠ [] := by
  try?

-/-- info: Try this: simp +arith -/
+/--
+info: Try these:
+• simp +arith
+• simp +arith only [ge_iff_le]
+• grind
+• grind only
+-/
 #guard_msgs (info) in
 example : 4 + x + y ≥ 1 + x  := by
  try?

-/-- info: Try this: grind? -/
+/--
+info: Try these:
+• grind
+• grind only
+-/
 #guard_msgs (info) in
 example (f : Nat → Nat) : f a = b → a = c → f c = b := by
  try?
@ -19,12 +35,20 @@ def f : Nat → Nat
  | 0 => 1
  | _ => 2

-/-- info: Try this: grind? [= f] -/
+/--
+info: Try these:
+• grind [= f]
+• grind only [f]
+-/
 #guard_msgs (info) in
 example : f (f 0) > 0 := by
  try?

-/-- info: Try this: grind? [= f.eq_def] -/
+/--
+info: Try these:
+• grind [= f.eq_def]
+• grind only [= f.eq_def]
+-/
 #guard_msgs (info) in
 example : f x > 0 := by
  try?
@ -33,12 +57,21 @@ def app : List α → List α → List α
  | [], bs => bs
  | a::as, bs => a :: app as bs

-/-- info: Try this: grind? [= app] -/
+/--
+info: Try these:
+• rfl
+• grind [= app]
+• grind only [app]
+-/
 #guard_msgs (info) in
 example : app [a, b] [c] = [a, b, c] := by
  try?

-/-- info: Try this: (induction as, bs using app.induct) <;> grind? [= app] -/
+/--
+info: Try these:
+• (induction as, bs using app.induct) <;> grind [= app]
+• (induction as, bs using app.induct) <;> grind only [app]
+-/
 #guard_msgs (info) in
 example : app (app as bs) cs = app as (app bs cs) := by
  try?