feat: add sym => interactive mode (#12970)

This PR adds a `sym =>` tactic that enters an interactive symbolic simulation mode built on `grind`. Unlike `grind =>`, it does not eagerly introduce hypotheses or apply by-contradiction, giving users explicit control over `intro`, `apply`, and `internalize` steps. New tactics available in `sym =>` mode: - `intro` / `intros`: introduce binders and internalize into the E-graph by default. Use `intro~` or `intro (internalize := false)` to skip internalization. - `apply t`: apply backward rules with caching for `repeat`. - `internalize` / `internalize_all`: internalize hypotheses into the E-graph. - `by_contra`: apply proof by contradiction, negating the target. Satellite solvers (`lia`, `ring`, `linarith`) automatically introduce remaining binders and apply by-contradiction in `sym =>` mode, matching their behavior in default tactic mode. All existing `grind =>` tactics (`finish`, `instantiate`, `cases`, etc.) also work in `sym =>` mode. The sym-specific tactics are guarded and rejected in regular `grind =>` mode. ```lean example (x : Nat) : myP x → myQ x := by sym [myP_myQ] => intro h finish example (x y z : Nat) : x > 1 → x + y + z > 0 := by sym => lia ```
2026-03-18 07:29:18 -07:00 · 2026-03-18 07:29:18 -07:00 · 58ef418dda
commit 58ef418dda
parent b2aec782eb
8 changed files with 471 additions and 13 deletions
--- a/src/Init/Grind/Interactive.lean
+++ b/src/Init/Grind/Interactive.lean
@ -262,5 +262,47 @@ Adds new case-splits using model-based theory combination.
 -/
 syntax (name := mbtc) "mbtc" : grind

+/-- `intro x₁ ... xₙ` introduces binders and internalizes them into the E-graph.
+Only available in `sym =>` mode.
+`intro` with no arguments introduces one binder with an inaccessible name.
+Use `intro (internalize := false)` or `intro~` to skip internalization. -/
+syntax (name := symIntro) "intro" (ppSpace "(" &"internalize" " := " (&"true" <|> &"false") ")")? (ppSpace colGt binderIdent)* : grind
+
+/-- `intro~ x₁ ... xₙ` is shorthand for `intro (internalize := false)`. -/
+syntax (name := symIntroLight) "intro" noWs "~" (ppSpace colGt binderIdent)* : grind
+
+macro_rules
+| `(grind| intro~ $ids*) => `(grind| intro (internalize := false) $ids*)
+
+/-- `intros` introduces all remaining binders and internalizes them.
+Only available in `sym =>` mode.
+Use `intros (internalize := false)` or `intros~` to skip internalization. -/
+syntax (name := symIntros) "intros" (ppSpace "(" &"internalize" " := " (&"true" <|> &"false") ")")? : grind
+
+/-- `intros~` is shorthand for `intros (internalize := false)`. -/
+syntax (name := symIntrosLight) "intros" noWs "~" : grind
+
+macro_rules
+| `(grind| intros~) => `(grind| intros (internalize := false))
+
+/-- `apply t` applies theorem `t` as a backward rule.
+Only available in `sym =>` mode.
+When used with `repeat`, the backward rule is cached for efficiency. -/
+syntax (name := symApply) "apply " term : grind
+
+/-- `internalize` internalizes hypotheses into the grind E-graph.
+Only available in `sym =>` mode.
+- `internalize` internalizes the next hypothesis.
+- `internalize <num>` internalizes the next `<num>` hypotheses. -/
+syntax (name := symInternalize) "internalize" (ppSpace num)? : grind
+
+/-- `internalize_all` internalizes all pending hypotheses into the grind E-graph.
+Only available in `sym =>` mode. -/
+syntax (name := symInternalizeAll) "internalize_all" : grind
+
+/-- `by_contra` applies proof by contradiction, negating the target and making it `False`.
+Only available in `sym =>` mode. -/
+syntax (name := symByContra) "by_contra" : grind
+
 end Grind
 end Lean.Parser.Tactic
--- a/src/Init/Grind/Tactics.lean
+++ b/src/Init/Grind/Tactics.lean
@ -295,6 +295,24 @@ syntax (name := grindTrace)
  (" [" withoutPosition(grindParam,*) "]")?
  : tactic

+/--
+`sym` enters an interactive symbolic simulation mode built on `grind`.
+Unlike `grind =>`, it does not eagerly introduce hypotheses or apply by-contradiction,
+giving the user explicit control over `intro`, `apply`, and `internalize` steps.
+
+Example:
+```
+example (x : Nat) : myP x → myQ x := by
+  sym [myP_myQ] =>
+    intro h
+    finish
+```
+-/
+syntax (name := sym)
+  "sym" optConfig (&" only")?
+  (" [" withoutPosition(grindParam,*) "]")?
+  " => " grindSeq : tactic
+
 /--
 `cutsat` solves linear integer arithmetic goals.

--- a/src/Lean/Elab/Tactic/Grind.lean
+++ b/src/Lean/Elab/Tactic/Grind.lean
@ -15,3 +15,4 @@ public import Lean.Elab.Tactic.Grind.Config
 public import Lean.Elab.Tactic.Grind.Lint
 public import Lean.Elab.Tactic.Grind.LintExceptions
 public import Lean.Elab.Tactic.Grind.Annotated
+public import Lean.Elab.Tactic.Grind.Sym
--- a/src/Lean/Elab/Tactic/Grind/Basic.lean
+++ b/src/Lean/Elab/Tactic/Grind/Basic.lean
@ -8,6 +8,8 @@ prelude
 public import Lean.Elab.Tactic.Basic
 public import Lean.Meta.Tactic.Grind.Main
 import Lean.Meta.Tactic.Grind.Intro
+public import Lean.Meta.Sym.Apply
+public import Lean.Meta.Sym.Util
 import Init.Omega
 public section
 namespace Lean.Elab.Tactic.Grind
@ -18,13 +20,21 @@ structure Context extends Tactic.Context where
  sctx    : Meta.Sym.Context
  methods : Grind.Methods
  params  : Grind.Params
+  sym     : Bool := false

 open Meta.Grind (Goal)

+structure Cache where
+  /-- Cache for `BackwardRule`s created from declaration names (sym mode only). -/
+  backwardRuleName : PHashMap Name Sym.BackwardRule := {}
+  /-- Cache for `BackwardRule`s created from elaborated terms, keyed by syntax byte position range (sym mode only). -/
+  backwardRuleSyntax : PHashMap (Nat × Nat) Sym.BackwardRule := {}
+
 structure State where
  symState   : Meta.Sym.State
  grindState : Meta.Grind.State
  goals      : List Goal
+  cache      : Cache := {}

 structure SavedState where
  term   : Term.SavedState
@ -377,7 +387,7 @@ def mkEvalTactic' (elaborator : Name) (params : Params) : TermElabM (Goal → TS
 def mkEvalTactic (params : Params) : TacticM (Goal → TSyntax `grind → GrindM (List Goal)) := do
  mkEvalTactic' (← read).elaborator params

-def GrindTacticM.runAtGoal (mvarId : MVarId) (params : Params) (k : GrindTacticM α) : TacticM (α × State) := do
+def GrindTacticM.runAtGoal (mvarId : MVarId) (params : Params) (k : GrindTacticM α) (sym : Bool := false) : TacticM (α × State) := do
  let evalTactic ← mkEvalTactic params
  /-
  **Note**: We don't want to close branches using `sorry` after applying `intros + assertAll`.
@ -385,10 +395,17 @@ def GrindTacticM.runAtGoal (mvarId : MVarId) (params : Params) (k : GrindTacticM
  -/
  let params' := { params with config.useSorry := false }
  let (methods, ctx, sctx, state) ← liftMetaM <| GrindM.runAtGoal mvarId params' (evalTactic? := some evalTactic) fun goal => do
-      let a : Action := Action.intros 0 >> Action.assertAll
-      let goals ← match (← a.run goal) with
-        | .closed _ => pure []
-        | .stuck gs => pure gs
+      let goals ←
+        if sym then
+          /- In sym mode, skip eager intros + by-contradiction. The user controls intro/internalize.
+             Preprocess for maximal term sharing, required by Sym operations (introN, BackwardRule.apply, etc.). -/
+          let mvarId ← Sym.preprocessMVar goal.mvarId
+          pure [{ goal with mvarId }]
+        else
+          let a : Action := Action.intros 0 >> Action.assertAll
+          match (← a.run goal) with
+          | .closed _ => pure []
+          | .stuck gs => pure gs
      let methods ← getMethods
      let ctx ← readThe Meta.Grind.Context
      /- Restore original config -/
@ -398,6 +415,6 @@ def GrindTacticM.runAtGoal (mvarId : MVarId) (params : Params) (k : GrindTacticM
      let symState ← getThe Sym.State
      return (methods, ctx, sctx, { grindState, symState, goals })
  let tctx ← read
-  k { tctx with methods, ctx, sctx, params } |>.run state
+  k { tctx with methods, ctx, sctx, params, sym } |>.run state

 end Lean.Elab.Tactic.Grind
--- a/src/Lean/Elab/Tactic/Grind/BuiltinTactic.lean
+++ b/src/Lean/Elab/Tactic/Grind/BuiltinTactic.lean
@ -102,6 +102,12 @@ If the goal is not inconsistent and progress has been made,
 -/
 def evalCheck (tacticName : Name) (k : GoalM Bool)
    (pp? : Goal → MetaM (Option MessageData)) : GrindTacticM Unit := do
+  /- In sym mode, introduce remaining binders + by-contradiction + internalize
+     so that satellite solvers (lia, ring, linarith) see all hypotheses.
+     This matches the behavior of these tactics in default tactic mode
+     where `lia` can close `x > 1 → x + y + z > 0` directly. -/
+  if (← read).sym then
+    liftAction <| Action.intros 0 >> Action.assertAll
  let recover := (← read).recover
  liftGoalM do
    let progress ← k
--- a/src/Lean/Elab/Tactic/Grind/Main.lean
+++ b/src/Lean/Elab/Tactic/Grind/Main.lean
@ -242,15 +242,21 @@ def mkGrindParams
    params := { params with config.clean := false }
  return params

+def checkTerminalAsSorry (mvarId : MVarId) : TacticM Bool := do
+  if debug.terminalTacticsAsSorry.get (← getOptions) then
+    mvarId.admit
+    replaceMainGoal []
+    return true
+  else
+    return false
+
 def grind
    (mvarId : MVarId) (config : Grind.Config)
    (only : Bool)
    (ps   :  TSyntaxArray ``Parser.Tactic.grindParam)
    (seq? : Option (TSyntax `Lean.Parser.Tactic.Grind.grindSeq))
    : TacticM Unit := do
-  if debug.terminalTacticsAsSorry.get (← getOptions) then
-    mvarId.admit
-    return ()
+  if (← checkTerminalAsSorry mvarId) then return ()
  mvarId.withContext do
    let params ← mkGrindParams config only ps mvarId
    let params := if Grind.grind.unusedLemmaThreshold.get (← getOptions) > 0 then
@ -260,7 +266,7 @@ def grind
      let finalize (result : Grind.Result) : TacticM Unit := do
        if result.hasFailed then
          throwError "`grind` failed\n{← result.toMessageData}"
-        return ()
+        replaceMainGoal []
      if let some seq := seq? then
        let (result, _) ← Grind.GrindTacticM.runAtGoal mvarId' params do
          Grind.evalGrindTactic seq
@ -286,9 +292,7 @@ def evalGrindCore
  let params := if let some params := params? then params.getElems else #[]
  if Grind.grind.warning.get (← getOptions) then
    logWarningAt ref "The `grind` tactic is new and its behavior may change in the future. This project has used `set_option grind.warning true` to discourage its use."
-  withMainContext do
-    grind (← getMainGoal) config only params seq?
-    replaceMainGoal []
+  grind (← getMainGoal) config only params seq?

 /-- Position for the `[..]` child syntax in the `grind` tactic. -/
 def grindParamsPos := 3
@ -343,6 +347,25 @@ private def elabGrindConfig' (config : TSyntax ``Lean.Parser.Tactic.optConfig) (
  let config ← elabGrindConfig' config interactive
  evalGrindCore stx config only params seq

+@[builtin_tactic Lean.Parser.Tactic.sym] def evalSym : Tactic := fun stx => do
+  recordExtraModUse (isMeta := false) `Init.Grind.Tactics
+  let `(tactic| sym $config:optConfig $[only%$only]?  $[ [$params:grindParam,*] ]? => $seq:grindSeq) := stx
+    | throwUnsupportedSyntax
+  let config ← elabGrindConfig' config true
+  let only' := only.isSome
+  let params := if let some params := params then params.getElems else #[]
+  let mvarId ← getMainGoal
+  if (← checkTerminalAsSorry mvarId) then return ()
+  mvarId.withContext do
+    let params ← mkGrindParams config only' params mvarId
+    Grind.withProtectedMCtx config mvarId fun mvarId' => do
+      let (result, _) ← Grind.GrindTacticM.runAtGoal mvarId' params (sym := true) do
+        Grind.evalGrindTactic seq
+        let goal? := if let goal :: _ := (← get).goals then some goal else none
+        Grind.liftGrindM <| Grind.mkResult params goal?
+      if result.hasFailed then
+        throwError "`sym` failed\n{← result.toMessageData}"
+
 def evalGrindTraceCore (stx : Syntax) (trace := true) (verbose := true) (useSorry := true) : TacticM (Array (TSyntax `tactic)) := withMainContext do
  let `(tactic| grind? $configStx:optConfig $[only%$only]?  $[ [$params?:grindParam,*] ]?) := stx
    | throwUnsupportedSyntax
--- a/src/Lean/Elab/Tactic/Grind/Sym.lean
+++ b/src/Lean/Elab/Tactic/Grind/Sym.lean
@ -0,0 +1,138 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+module
+prelude
+import Lean.Elab.Tactic.Grind.Basic
+import Lean.Meta.Sym.Grind
+import Lean.Meta.Tactic.Apply
+import Lean.Elab.SyntheticMVars
+namespace Lean.Elab.Tactic.Grind
+open Meta Grind
+
+private def ensureSym : GrindTacticM Unit := do
+  unless (← read).sym do
+    throwError "tactic is only available in `sym =>` mode"
+
+/-- Lift a `SymM` computation into `GrindTacticM`. -/
+private def liftSymM (k : Sym.SymM α) : GrindTacticM α := do
+  -- GrindM := ... Sym.SymM, so SymM auto-lifts to GrindM
+  liftGrindM k
+
+private def evalIntroCore (internalize : Bool) (ids : TSyntaxArray `Lean.binderIdent) : GrindTacticM Unit := do
+  ensureSym
+  let goal ← getMainGoal
+  let goal ←
+    if ids.isEmpty then
+      match (← liftSymM <| Grind.Goal.introN goal 1) with
+      | .goal _ goal => pure goal
+      | .failed => throwError "`intro` failed, no binders to introduce"
+    else
+      let names ← ids.mapM fun id => match id with
+        | `(binderIdent| $name:ident) => pure name.getId
+        | `(binderIdent| $_) => mkFreshBinderNameForTactic `h
+      match (← liftSymM <| Grind.Goal.intros goal names) with
+      | .goal _ goal => pure goal
+      | .failed => throwError "`intro` failed"
+  let goal ← if internalize then liftGrindM <| Grind.Goal.internalizeAll goal else pure goal
+  replaceMainGoal [goal]
+
+@[builtin_grind_tactic Parser.Tactic.Grind.symIntro] def evalSymIntro : GrindTactic := fun stx => do
+  -- syntax: "intro" ("(" &"internalize" " := " (&"true" <|> &"false") ")")? binderIdent*
+  match stx with
+  | `(grind| intro $ids:binderIdent*) => evalIntroCore true ids
+  | `(grind| intro (internalize := false) $ids:binderIdent*) => evalIntroCore false ids
+  | `(grind| intro (internalize := true) $ids:binderIdent*) => evalIntroCore true ids
+  | _ => throwUnsupportedSyntax
+
+private def evalIntrosCore (internalize : Bool) : GrindTacticM Unit := do
+  ensureSym
+  let goal ← getMainGoal
+  match (← liftSymM <| Grind.Goal.intros goal #[]) with
+  | .goal _ goal =>
+    let goal ← if internalize then liftGrindM <| Grind.Goal.internalizeAll goal else pure goal
+    replaceMainGoal [goal]
+  | .failed => throwError "`intros` failed"
+
+@[builtin_grind_tactic Parser.Tactic.Grind.symIntros] def evalSymIntros : GrindTactic := fun stx => do
+  match stx with
+  | `(grind| intros) => evalIntrosCore true
+  | `(grind| intros (internalize := false)) => evalIntrosCore false
+  | `(grind| intros (internalize := true)) => evalIntrosCore true
+  | _ => throwUnsupportedSyntax
+
+/-- Get or create a `BackwardRule` for a declaration, using the name cache. -/
+private def getOrCreateBackwardRule (declName : Name) : GrindTacticM Sym.BackwardRule := do
+  if let some rule := (← get).cache.backwardRuleName.find? declName then
+    return rule
+  let rule ← Sym.mkBackwardRuleFromDecl declName
+  modify fun s => { s with cache.backwardRuleName := s.cache.backwardRuleName.insert declName rule }
+  return rule
+
+/-- Get or create a `BackwardRule` for a term, using the syntax position cache. -/
+private def getOrCreateBackwardRuleFromTerm (term : Syntax) : GrindTacticM Sym.BackwardRule := do
+  let startPos := term.getPos?.map (·.byteIdx) |>.getD 0
+  let endPos := term.getTailPos?.map (·.byteIdx) |>.getD 0
+  let pos := (startPos, endPos)
+  if let some rule := (← get).cache.backwardRuleSyntax.find? pos then
+    return rule
+  let e ← withMainContext do
+    let e ← Term.elabTerm term none
+    Term.synthesizeSyntheticMVars (postpone := .no)
+    instantiateMVars e
+  let rule ← Sym.mkBackwardRuleFromExpr e
+  modify fun s => { s with cache.backwardRuleSyntax := s.cache.backwardRuleSyntax.insert pos rule }
+  return rule
+
+@[builtin_grind_tactic Parser.Tactic.Grind.symApply] def evalSymApply : GrindTactic := fun stx => do
+  ensureSym
+  let `(grind| apply $term:term) := stx | throwUnsupportedSyntax
+  let goal ← getMainGoal
+  goal.withContext do
+  -- Try to interpret as a declaration name for efficient caching
+  let rule ← match term with
+  | `($id:ident) =>
+    try
+      let declName ← realizeGlobalConstNoOverload id
+      getOrCreateBackwardRule declName
+    catch _ =>
+      getOrCreateBackwardRuleFromTerm term
+  | _ =>
+    getOrCreateBackwardRuleFromTerm term
+  match (← liftSymM <| Grind.Goal.apply goal rule) with
+  | .goals subgoals => replaceMainGoal subgoals
+  | .failed => throwError "`apply` failed, rule is not applicable"
+
+@[builtin_grind_tactic Parser.Tactic.Grind.symInternalize] def evalSymInternalize : GrindTactic := fun stx => do
+  ensureSym
+  let goal ← getMainGoal
+  let num := if stx[1].isNone then 1 else stx[1][0].toNat
+  let goal ← liftGrindM <| Grind.Goal.internalize goal num
+  replaceMainGoal [goal]
+
+@[builtin_grind_tactic Parser.Tactic.Grind.symInternalizeAll] def evalSymInternalizeAll : GrindTactic := fun _ => do
+  ensureSym
+  let goal ← getMainGoal
+  let goal ← liftGrindM <| Grind.Goal.internalizeAll goal
+  replaceMainGoal [goal]
+
+@[builtin_grind_tactic Parser.Tactic.Grind.symByContra] def evalSymByContra : GrindTactic := fun _ => do
+  ensureSym
+  let goal ← getMainGoal
+  let target ← goal.mvarId.getType
+  if target.isFalse then
+    throwError "`by_contra` failed, target is already `False`"
+  -- If target is not a proposition, apply exfalso first
+  let mvarId ← if (← isProp target) then pure goal.mvarId else goal.mvarId.exfalso
+  let some mvarId ← mvarId.byContra?
+    | throwError "`by_contra` failed"
+  -- byContra? produces `⊢ ¬target → False`, introduce the negated hypothesis
+  let (_, mvarId) ← mvarId.intro1
+  let goal := { goal with mvarId }
+  -- Internalize the negated hypothesis so the E-graph can detect contradictions
+  let goal ← liftGrindM <| Grind.Goal.internalizeAll goal
+  replaceMainGoal [goal]
+
+end Lean.Elab.Tactic.Grind
--- a/tests/elab/sym_interactive1.lean
+++ b/tests/elab/sym_interactive1.lean
@ -0,0 +1,213 @@
+/-!
+# Tests for `sym =>` interactive mode (PR1)
+
+`intro` and `intros` internalize by default. Use `intro~` / `intros~` or
+`(internalize := false)` to skip internalization.
+-/
+
+opaque myP : Nat → Prop
+opaque myQ : Nat → Prop
+opaque myR : Nat → Nat → Prop
+opaque myF : Nat → Nat
+axiom myP_myQ : myP x → myQ x
+axiom myR_comm : myR x y → myR y x
+axiom myR_trans : myR x y → myR y z → myR x z
+axiom myP_step : myP x → myP (myF x)
+
+/-! ## Test 1: sym => finish (no intro, finish handles everything) -/
+
+example (x : Nat) : myP x → myQ x := by
+  sym [myP_myQ] =>
+    finish
+
+/-! ## Test 2: sym => finish with multiple binders -/
+
+example (x y z : Nat) : myR x y → myR y z → myR x z := by
+  sym [myR_trans] =>
+    finish
+
+/-! ## Test 3: intro + finish (intro internalizes by default) -/
+
+example (x : Nat) : myP x → myQ x := by
+  sym [myP_myQ] =>
+    intro h
+    have h1 := h -- should work
+    finish
+
+/-! ## Test 4: intros + finish -/
+
+example (x : Nat) : myP x → myQ x := by
+  sym [myP_myQ] =>
+    intros
+    finish
+
+/-! ## Test 5: apply backward rule -/
+
+example (a b : Prop) (ha : a) (hb : b) : a ∧ b := by
+  sym =>
+    apply And.intro
+    · tactic => exact ha
+    · tactic => exact hb
+
+/-! ## Test 6: apply with multiple subgoals -/
+
+example (a b c : Prop) (ha : a) (hbc : b ∧ c) : a ∧ b ∧ c := by
+  sym =>
+    apply And.intro
+    · tactic => exact ha
+    · tactic => exact hbc
+
+/-! ## Test 7: repeat instantiate for chain reasoning -/
+
+example (x : Nat) : myP x → myP (myF (myF x)) := by
+  sym [myP_step] =>
+    intro h
+    repeat instantiate only [→myP_step]
+    finish
+
+/-! ## Test 8: sym with only -/
+
+example (x : Nat) : myP x → myQ x := by
+  sym only [myP_myQ] =>
+    finish
+
+/-! ## Test 9: intro with named binders -/
+
+example (x y : Nat) : myR x y → myR y x := by
+  sym [myR_comm] =>
+    intro h
+    finish
+
+/-! ## Test 10: intro~ skips internalization (explicit internalize needed) -/
+
+example (x : Nat) : myP x → myQ x := by
+  sym [myP_myQ] =>
+    intro~ h
+    internalize_all
+    finish
+
+/-! ## Test 11: intro (internalize := false) -/
+
+example (x : Nat) : myP x → myQ x := by
+  sym [myP_myQ] =>
+    intro (internalize := false) h
+    internalize 1
+    finish
+
+/-! ## Test 12: intros~ -/
+
+example (x : Nat) : myP x → myQ x := by
+  sym [myP_myQ] =>
+    intros~
+    internalize_all
+    finish
+
+/-! ## Test 13: tactic escape -/
+
+example (x y : Nat) (h : x > y) : x > 0 := by
+  sym =>
+    tactic => omega
+
+/-! ## Test 14: sym-only tactics rejected in grind => mode -/
+
+/--
+error: tactic is only available in `sym =>` mode
+-/
+#guard_msgs in
+example (x : Nat) : myP x → myQ x := by
+  grind [myP_myQ] =>
+    intro h
+    done
+
+/-! ## Test 15: intro fails gracefully with no binders -/
+
+/--
+error: `intro` failed
+-/
+#guard_msgs in
+example (x : Nat) (h : myP x) : myQ x := by
+  sym [myP_myQ] =>
+    intro _
+    done
+
+/-! ## Test 16: intros on fully applied goal -/
+
+example (x : Nat) (h : myP x) : myQ x := by
+  sym [myP_myQ] =>
+    finish
+
+/-! ## Test 17: by_contra + instantiate -/
+
+example (x : Nat) : myP x → myQ x := by
+  sym =>
+    intro h
+    by_contra
+    instantiate only [→myP_myQ]
+
+/-! ## Test 18: by_contra on already-False target fails -/
+
+/--
+error: `by_contra` failed, target is already `False`
+-/
+#guard_msgs in
+example : False := by
+  sym =>
+    by_contra
+    done
+
+/-! ## Test 19: by_contra rejected in grind => mode -/
+
+/--
+error: tactic is only available in `sym =>` mode
+-/
+#guard_msgs in
+example (x : Nat) : myP x → myQ x := by
+  grind [myP_myQ] =>
+    by_contra
+    done
+
+/-! ## Test 20: compact one-liner -/
+
+example (x : Nat) : myP x → myQ x := by
+  sym [myP_myQ] =>
+    intro; by_contra; finish
+
+example (p q : Prop) : p → q → p ∧ q := by
+  sym =>
+    intro hp hq
+    apply And.intro
+    apply hp
+    apply hq
+
+example (p q : Prop) : p → q → p ∧ q := by
+  sym =>
+    intro hp hq
+    apply And.intro hp hq
+
+example (p q : Prop) : p → q → p ∧ q := by
+  sym =>
+    intro hp hq
+    tactic => exact And.intro hp hq
+
+/-! ## lia/ring/linarith auto-introduce in sym mode -/
+
+example (x y z : Nat) : x > 1 → x + y + z > 0 := by
+  sym =>
+    lia
+
+example (x y z : Nat) : x > 1 → x + y + z > 0 := by
+  sym =>
+    intro
+    lia
+
+example (x : Nat) (h : x > 0) : x * x > 0 := by
+  sym =>
+    have := Nat.mul_pos h h
+
+example (x y z : Nat) (h : x > 1) : x + y + z > 0 := by
+  sym => lia
+
+example (as : List Nat) (h : as = []) (h1 : as.length = b) : b = 0 := by
+  sym =>
+    instantiate
+    by_contra