From f7ead9667b2308cfcd91e434e526848d3f2aa8f8 Mon Sep 17 00:00:00 2001
From: Kim Morrison <477956+kim-em@users.noreply.github.com>
Date: Fri, 14 Nov 2025 16:27:23 +1100
Subject: [PATCH] =?UTF-8?q?feat:=20`=E2=88=8E`=20macro=20for=20`try=3F`=20?=
 =?UTF-8?q?(#11170)?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

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             |  9 ++++++
 src/Lean/Elab/Tactic/Try.lean | 35 ++++++++++++++++++++--
 tests/lean/run/qed_macro.lean | 56 +++++++++++++++++++++++++++++++++++
 3 files changed, 98 insertions(+), 2 deletions(-)
 create mode 100644 tests/lean/run/qed_macro.lean

diff --git a/src/Init/Try.lean b/src/Init/Try.lean
index bc05b0d9f8..b5f8d79ada 100644
--- a/src/Init/Try.lean
+++ b/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))
diff --git a/src/Lean/Elab/Tactic/Try.lean b/src/Lean/Elab/Tactic/Try.lean
index d2d3cf8fc5..57ec2815b7 100644
--- a/src/Lean/Elab/Tactic/Try.lean
+++ b/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
diff --git a/tests/lean/run/qed_macro.lean b/tests/lean/run/qed_macro.lean
new file mode 100644
index 0000000000..b44cf4c0b9
--- /dev/null
+++ b/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
+  ∎