feat: ∎ macro for try? (#11170)

This PR adds tactic and term mode macros for `∎` (typed `\qed`) which
expand to `try?`. The term mode version captures any produced
suggestions and prepends `by`.

Co-authored-by: Claude <noreply@anthropic.com>

src/Init/Try.lean

@@ -42,6 +42,8 @@ structure Config where
   ```
   -/
   merge := true
+  /-- If `wrapWithBy` is `true`, suggestions are wrapped with `by` for term mode usage. -/
+  wrapWithBy := false
   deriving Inhabited
 
 end Lean.Try
@@ -70,3 +72,10 @@ syntax (name := registerTryTactic) (docComment)?
   "register_try?_tactic" ("(" &"priority" ":=" num ")")? tacticSeq : command
 
 end Lean.Parser.Command
+
+/-- `∎` (typed as `\qed`) is a macro that expands to `try?` in tactic mode. -/
+macro "∎" : tactic => `(tactic| try?)
+
+/-- `∎` (typed as `\qed`) is a macro that expands to `by try? (wrapWithBy := true)` in term mode.
+    The `wrapWithBy` config option causes suggestions to be prefixed with `by`. -/
+macro "∎" : term => `(by try? (wrapWithBy := true))

src/Lean/Elab/Tactic/Try.lean

@@ -917,14 +917,45 @@ private unsafe def mkTryEvalSuggestStxUnsafe (goal : MVarId) (info : Try.Info) :
 @[implemented_by mkTryEvalSuggestStxUnsafe]
 private opaque mkTryEvalSuggestStx (goal : MVarId) (info : Try.Info) : MetaM (TSyntax `tactic)
 
+/-- Wraps a tactic suggestion as a term suggestion by prefixing with `by `. -/
+private def wrapSuggestionWithBy (sugg : Tactic.TryThis.Suggestion) : TacticM Tactic.TryThis.Suggestion := do
+  match sugg.suggestion with
+  | .tsyntax (kind := `tactic) tac =>
+    let termStx ← `(by $(⟨tac⟩):tactic)
+    return { sugg with suggestion := .tsyntax termStx }
+  | _ => return sugg
+
+/-- Version of `evalAndSuggest` that wraps tactic suggestions with `by` for term mode. -/
+private def evalAndSuggestWithBy (tk : Syntax) (tac : TSyntax `tactic) (config : Try.Config) : TacticM Unit := do
+  let initialLog ← Core.getMessageLog
+  let tac' ← try
+    evalSuggest tac |>.run { terminal := true, root := tac, config }
+  catch _ =>
+    throwEvalAndSuggestFailed config
+  -- Restore message log to suppress "Try this" messages from intermediate tactic executions
+  Core.setMessageLog initialLog
+  let suggestions := (getSuggestions tac')[*...config.max].toArray
+  if suggestions.isEmpty then
+    throwEvalAndSuggestFailed config
+  else
+    -- Wrap each suggestion with `by `
+    let termSuggestions ← suggestions.mapM wrapSuggestionWithBy
+    if termSuggestions.size == 1 then
+      Tactic.TryThis.addSuggestion tk termSuggestions[0]! (origSpan? := (← getRef))
+    else
+      Tactic.TryThis.addSuggestions tk termSuggestions (origSpan? := (← getRef))
+
 @[builtin_tactic Lean.Parser.Tactic.tryTrace] def evalTryTrace : Tactic := fun stx => do
   match stx with
   | `(tactic| try?%$tk $config:optConfig) => Tactic.focus do withMainContext do
     let config ← elabTryConfig config
     let goal ← getMainGoal
     let info ← Try.collect goal config
-    let stx ← mkTryEvalSuggestStx goal info
-    evalAndSuggest tk stx config
+    let tacStx ← mkTryEvalSuggestStx goal info
+    if config.wrapWithBy then
+      evalAndSuggestWithBy tk tacStx config
+    else
+      evalAndSuggest tk tacStx config
   | _ => throwUnsupportedSyntax
 
 end Lean.Elab.Tactic.Try

tests/lean/run/qed_macro.lean

@@ -0,0 +1,56 @@
+/-
+Test file for the ∎ (QED) macro which expands to `try?`
+-/
+
+import Lean.Elab.Tactic.Try
+
+-- Basic tactic mode usage - should suggest tactics
+/--
+info: Try these:
+  [apply] rfl
+  [apply] simp
+  [apply] simp only [Nat.reduceAdd]
+  [apply] grind
+  [apply] grind only
+  [apply] simp_all
+-/
+#guard_msgs in
+example : 1 + 1 = 2 := by
+  ∎
+
+-- Term mode usage - should suggest terms with "by"
+/--
+info: Try these:
+  [apply] by rfl
+  [apply] by simp
+  [apply] by simp only [Nat.reduceAdd]
+  [apply] by grind
+  [apply] by grind only
+  [apply] by simp_all
+-/
+#guard_msgs in
+example : 1 + 1 = 2 :=
+  ∎
+
+-- With hypotheses in term mode
+/--
+info: Try these:
+  [apply] by simp [*]
+  [apply] by simp only [h]
+  [apply] by grind
+  [apply] by grind only
+  [apply] by simp_all
+-/
+#guard_msgs in
+example (a b : Nat) (h : a = b) : b = a :=
+  ∎
+
+-- Check that error messages are appropriate when try? fails
+/--
+error: Tactic `try?` failed: consider using `grind` manually, or `try? +missing` for partial proofs containing `sorry`
+
+⊢ False
+-/
+#guard_msgs in
+example : False := by
+  ∎