chore: solve_by_elim updates

src/Init/Data.lean

@@ -33,3 +33,4 @@ import Init.Data.AC
 import Init.Data.Queue
 import Init.Data.Channel
 import Init.Data.Cast
+import Init.Data.Sum

src/Init/Data/List/BasicAux.lean

@@ -5,6 +5,7 @@ Author: Leonardo de Moura
 -/
 prelude
 import Init.Data.Nat.Linear
+import Init.Data.Array.Basic
 import Init.Data.List.Basic
 import Init.Util
 
@@ -207,4 +208,23 @@ if the result of each `f a` is a pointer equal value `a`.
 def mapMono (as : List α) (f : α → α) : List α :=
   Id.run <| as.mapMonoM f
 
+/--
+Monadic generalization of `List.partition`.
+
+This uses `Array.toList` and which isn't imported by `Init.Data.List.Basic`.
+-/
+@[inline] def partitionM [Monad m] (p : α → m Bool) (l : List α) : m (List α × List α) :=
+  go l #[] #[]
+where
+  /-- Auxiliary for `partitionM`:
+  `partitionM.go p l acc₁ acc₂` returns `(acc₁.toList ++ left, acc₂.toList ++ right)`
+  if `partitionM p l` returns `(left, right)`. -/
+  @[specialize] go : List α → Array α → Array α → m (List α × List α)
+  | [], acc₁, acc₂ => pure (acc₁.toList, acc₂.toList)
+  | x :: xs, acc₁, acc₂ => do
+    if ← p x then
+      go xs (acc₁.push x) acc₂
+    else
+      go xs acc₁ (acc₂.push x)
+
 end List

src/Init/Data/String/Extra.lean

@@ -7,7 +7,6 @@ prelude
 import Init.Control.Except
 import Init.Data.ByteArray
 import Init.SimpLemmas
-import Init.Data.Nat.Linear
 import Init.Util
 import Init.WFTactics
 

src/Init/Data/Sum.lean

@@ -0,0 +1,24 @@
+/-
+Copyright (c) 2017 Mario Carneiro. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mario Carneiro, Yury G. Kudryashov
+-/
+prelude
+import Init.Core
+
+namespace Sum
+
+deriving instance DecidableEq for Sum
+deriving instance BEq for Sum
+
+/-- Check if a sum is `inl` and if so, retrieve its contents. -/
+def getLeft? : α ⊕ β → Option α
+  | inl a => some a
+  | inr _ => none
+
+/-- Check if a sum is `inr` and if so, retrieve its contents. -/
+def getRight? : α ⊕ β → Option β
+  | inr b => some b
+  | inl _ => none
+
+end Sum

src/Init/Meta.lean

@@ -9,6 +9,7 @@ prelude
 import Init.MetaTypes
 import Init.Data.Array.Basic
 import Init.Data.Option.BasicAux
+import Init.Data.String.Extra
 
 namespace Lean
 
@@ -105,6 +106,42 @@ def idEndEscape   := '»'
 def isIdBeginEscape (c : Char) : Bool := c = idBeginEscape
 def isIdEndEscape (c : Char) : Bool := c = idEndEscape
 
+private def findLeadingSpacesSize (s : String) : Nat :=
+  let it := s.iter
+  let it := it.find (· == '\n') |>.next
+  consumeSpaces it 0 s.length
+where
+  consumeSpaces (it : String.Iterator) (curr min : Nat) : Nat :=
+    if it.atEnd then min
+    else if it.curr == ' ' || it.curr == '\t' then consumeSpaces it.next (curr + 1) min
+    else if it.curr == '\n' then findNextLine it.next min
+    else findNextLine it.next (Nat.min curr min)
+  findNextLine (it : String.Iterator) (min : Nat) : Nat :=
+    if it.atEnd then min
+    else if it.curr == '\n' then consumeSpaces it.next 0 min
+    else findNextLine it.next min
+
+private def removeNumLeadingSpaces (n : Nat) (s : String) : String :=
+  consumeSpaces n s.iter ""
+where
+  consumeSpaces (n : Nat) (it : String.Iterator) (r : String) : String :=
+     match n with
+     | 0 => saveLine it r
+     | n+1 =>
+       if it.atEnd then r
+       else if it.curr == ' ' || it.curr == '\t' then consumeSpaces n it.next r
+       else saveLine it r
+  termination_by (it, 1)
+  saveLine (it : String.Iterator) (r : String) : String :=
+    if it.atEnd then r
+    else if it.curr == '\n' then consumeSpaces n it.next (r.push '\n')
+    else saveLine it.next (r.push it.curr)
+  termination_by (it, 0)
+
+def removeLeadingSpaces (s : String) : String :=
+  let n := findLeadingSpacesSize s
+  if n == 0 then s else removeNumLeadingSpaces n s
+
 namespace Name
 
 def getRoot : Name → Name
@@ -1261,6 +1298,11 @@ def expandInterpolatedStr (interpStr : TSyntax interpolatedStrKind) (type : Term
   let r ← expandInterpolatedStrChunks interpStr.raw.getArgs (fun a b => `($a ++ $b)) (fun a => `($toTypeFn $a))
   `(($r : $type))
 
+def getDocString (stx : TSyntax `Lean.Parser.Command.docComment) : String :=
+  match stx.raw[1] with
+  | Syntax.atom _ val => val.extract 0 (val.endPos - ⟨2⟩)
+  | _                 => ""
+
 end TSyntax
 
 namespace Meta
@@ -1322,7 +1364,9 @@ end Omega
 
 end Meta
 
-namespace Parser.Tactic
+namespace Parser
+
+namespace Tactic
 
 /-- `erw [rules]` is a shorthand for `rw (config := { transparency := .default }) [rules]`.
 This does rewriting up to unfolding of regular definitions (by comparison to regular `rw`
@@ -1383,6 +1427,26 @@ This will rewrite with all equation lemmas, which can be used to
 partially evaluate many definitions. -/
 declare_simp_like_tactic (dsimp := true) dsimpAutoUnfold "dsimp! " fun (c : Lean.Meta.DSimp.Config) => { c with autoUnfold := true }
 
-end Parser.Tactic
+end Tactic
+
+namespace Command
+
+/--
+Initialize a new "label" attribute.
+Declarations tagged with the attribute can be retrieved using `Std.Tactic.LabelAttr.labelled`.
+-/
+macro (name := _root_.Lean.Parser.Command.registerLabelAttr)
+  doc:(docComment)? "register_label_attr " id:ident : command => do
+  let str := id.getId.toString
+  let idParser := mkIdentFrom id (`Parser.Attr ++ id.getId)
+  let descr := quote (removeLeadingSpaces
+    (doc.map (·.getDocString) |>.getD ("labelled declarations for " ++ id.getId.toString)))
+  `($[$doc:docComment]? initialize ext : LabelExtension ←
+      registerLabelAttr $(quote id.getId) $descr $(quote id.getId)
+    $[$doc:docComment]? syntax (name := $idParser:ident) $(quote str):str : attr)
+
+end Command
+
+end Parser
 
 end Lean

src/Init/System/Uri.lean

@@ -5,6 +5,7 @@ Authors: Chris Lovett
 -/
 prelude
 import Init.Data.String.Extra
+import Init.Data.Nat.Linear
 import Init.System.FilePath
 
 namespace System

src/Init/Tactics.lean

@@ -1161,6 +1161,125 @@ syntax (name := pushCast) "push_cast" (config)? (discharger)? (&" only")?
 -/
 syntax (name := normCastAddElim) "norm_cast_add_elim" ident : command
 
+/--
+* `symm` applies to a goal whose target has the form `t ~ u` where `~` is a symmetric relation,
+  that is, a relation which has a symmetry lemma tagged with the attribute [symm].
+  It replaces the target with `u ~ t`.
+* `symm at h` will rewrite a hypothesis `h : t ~ u` to `h : u ~ t`.
+-/
+syntax (name := symm) "symm" (Parser.Tactic.location)? : tactic
+
+/-- For every hypothesis `h : a ~ b` where a `@[symm]` lemma is available,
+add a hypothesis `h_symm : b ~ a`. -/
+syntax (name := symmSaturate) "symm_saturate" : tactic
+
+namespace SolveByElim
+
+/-- Syntax for omitting a local hypothesis in `solve_by_elim`. -/
+syntax erase := "-" term:max
+/-- Syntax for including all local hypotheses in `solve_by_elim`. -/
+syntax star := "*"
+/-- Syntax for adding or removing a term, or `*`, in `solve_by_elim`. -/
+syntax arg := star <|> erase <|> term
+/-- Syntax for adding and removing terms in `solve_by_elim`. -/
+syntax args := " [" SolveByElim.arg,* "]"
+/-- Syntax for using all lemmas labelled with an attribute in `solve_by_elim`. -/
+syntax using_ := " using " ident,*
+
+end SolveByElim
+
+section SolveByElim
+open SolveByElim (args using_)
+
+/--
+`solve_by_elim` calls `apply` on the main goal to find an assumption whose head matches
+and then repeatedly calls `apply` on the generated subgoals until no subgoals remain,
+performing at most `maxDepth` (defaults to 6) recursive steps.
+
+`solve_by_elim` discharges the current goal or fails.
+
+`solve_by_elim` performs backtracking if subgoals can not be solved.
+
+By default, the assumptions passed to `apply` are the local context, `rfl`, `trivial`,
+`congrFun` and `congrArg`.
+
+The assumptions can be modified with similar syntax as for `simp`:
+* `solve_by_elim [h₁, h₂, ..., hᵣ]` also applies the given expressions.
+* `solve_by_elim only [h₁, h₂, ..., hᵣ]` does not include the local context,
+  `rfl`, `trivial`, `congrFun`, or `congrArg` unless they are explicitly included.
+* `solve_by_elim [-h₁, ... -hₙ]` removes the given local hypotheses.
+* `solve_by_elim using [a₁, ...]` uses all lemmas which have been labelled
+  with the attributes `aᵢ` (these attributes must be created using `register_label_attr`).
+
+`solve_by_elim*` tries to solve all goals together, using backtracking if a solution for one goal
+makes other goals impossible.
+(Adding or removing local hypotheses may not be well-behaved when starting with multiple goals.)
+
+Optional arguments passed via a configuration argument as `solve_by_elim (config := { ... })`
+- `maxDepth`: number of attempts at discharging generated subgoals
+- `symm`: adds all hypotheses derived by `symm` (defaults to `true`).
+- `exfalso`: allow calling `exfalso` and trying again if `solve_by_elim` fails
+  (defaults to `true`).
+- `transparency`: change the transparency mode when calling `apply`. Defaults to `.default`,
+  but it is often useful to change to `.reducible`,
+  so semireducible definitions will not be unfolded when trying to apply a lemma.
+
+See also the doc-comment for `Std.Tactic.BacktrackConfig` for the options
+`proc`, `suspend`, and `discharge` which allow further customization of `solve_by_elim`.
+Both `apply_assumption` and `apply_rules` are implemented via these hooks.
+-/
+syntax (name := solveByElim)
+  "solve_by_elim" "*"? (config)? (&" only")? (args)? (using_)? : tactic
+
+/--
+`apply_assumption` looks for an assumption of the form `... → ∀ _, ... → head`
+where `head` matches the current goal.
+
+You can specify additional rules to apply using `apply_assumption [...]`.
+By default `apply_assumption` will also try `rfl`, `trivial`, `congrFun`, and `congrArg`.
+If you don't want these, or don't want to use all hypotheses, use `apply_assumption only [...]`.
+You can use `apply_assumption [-h]` to omit a local hypothesis.
+You can use `apply_assumption using [a₁, ...]` to use all lemmas which have been labelled
+with the attributes `aᵢ` (these attributes must be created using `register_label_attr`).
+
+`apply_assumption` will use consequences of local hypotheses obtained via `symm`.
+
+If `apply_assumption` fails, it will call `exfalso` and try again.
+Thus if there is an assumption of the form `P → ¬ Q`, the new tactic state
+will have two goals, `P` and `Q`.
+
+You can pass a further configuration via the syntax `apply_rules (config := {...}) lemmas`.
+The options supported are the same as for `solve_by_elim` (and include all the options for `apply`).
+-/
+syntax (name := applyAssumption)
+  "apply_assumption" (config)? (&" only")? (args)? (using_)? : tactic
+
+/--
+`apply_rules [l₁, l₂, ...]` tries to solve the main goal by iteratively
+applying the list of lemmas `[l₁, l₂, ...]` or by applying a local hypothesis.
+If `apply` generates new goals, `apply_rules` iteratively tries to solve those goals.
+You can use `apply_rules [-h]` to omit a local hypothesis.
+
+`apply_rules` will also use `rfl`, `trivial`, `congrFun` and `congrArg`.
+These can be disabled, as can local hypotheses, by using `apply_rules only [...]`.
+
+You can use `apply_rules using [a₁, ...]` to use all lemmas which have been labelled
+with the attributes `aᵢ` (these attributes must be created using `register_label_attr`).
+
+You can pass a further configuration via the syntax `apply_rules (config := {...})`.
+The options supported are the same as for `solve_by_elim` (and include all the options for `apply`).
+
+`apply_rules` will try calling `symm` on hypotheses and `exfalso` on the goal as needed.
+This can be disabled with `apply_rules (config := {symm := false, exfalso := false})`.
+
+You can bound the iteration depth using the syntax `apply_rules (config := {maxDepth := n})`.
+
+Unlike `solve_by_elim`, `apply_rules` does not perform backtracking, and greedily applies
+a lemma from the list until it gets stuck.
+-/
+syntax (name := applyRules) "apply_rules" (config)? (&" only")? (args)? (using_)? : tactic
+end SolveByElim
+
 end Tactic
 
 namespace Attr

src/Lean.lean

@@ -35,3 +35,4 @@ import Lean.Widget
 import Lean.Log
 import Lean.Linter
 import Lean.SubExpr
+import Lean.LabelAttribute

src/Lean/Data/RBMap.lean

@@ -5,6 +5,8 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.Data.Ord
+import Init.Data.Nat.Linear
+
 namespace Lean
 universe u v w w'
 

src/Lean/DocString.lean

@@ -12,42 +12,6 @@ namespace Lean
 private builtin_initialize builtinDocStrings : IO.Ref (NameMap String) ← IO.mkRef {}
 private builtin_initialize docStringExt : MapDeclarationExtension String ← mkMapDeclarationExtension
 
-private def findLeadingSpacesSize (s : String) : Nat :=
-  let it := s.iter
-  let it := it.find (· == '\n') |>.next
-  consumeSpaces it 0 s.length
-where
-  consumeSpaces (it : String.Iterator) (curr min : Nat) : Nat :=
-    if it.atEnd then min
-    else if it.curr == ' ' || it.curr == '\t' then consumeSpaces it.next (curr + 1) min
-    else if it.curr == '\n' then findNextLine it.next min
-    else findNextLine it.next (Nat.min curr min)
-  findNextLine (it : String.Iterator) (min : Nat) : Nat :=
-    if it.atEnd then min
-    else if it.curr == '\n' then consumeSpaces it.next 0 min
-    else findNextLine it.next min
-
-private def removeNumLeadingSpaces (n : Nat) (s : String) : String :=
-  consumeSpaces n s.iter ""
-where
-  consumeSpaces (n : Nat) (it : String.Iterator) (r : String) : String :=
-     match n with
-     | 0 => saveLine it r
-     | n+1 =>
-       if it.atEnd then r
-       else if it.curr == ' ' || it.curr == '\t' then consumeSpaces n it.next r
-       else saveLine it r
-  termination_by (it, 1)
-  saveLine (it : String.Iterator) (r : String) : String :=
-    if it.atEnd then r
-    else if it.curr == '\n' then consumeSpaces n it.next (r.push '\n')
-    else saveLine it.next (r.push it.curr)
-  termination_by (it, 0)
-
-def removeLeadingSpaces (s : String) : String :=
-  let n := findLeadingSpacesSize s
-  if n == 0 then s else removeNumLeadingSpaces n s
-
 def addBuiltinDocString (declName : Name) (docString : String) : IO Unit :=
   builtinDocStrings.modify (·.insert declName (removeLeadingSpaces docString))
 
@@ -91,9 +55,4 @@ def getDocStringText [Monad m] [MonadError m] [MonadRef m] (stx : TSyntax `Lean.
   | Syntax.atom _ val => return val.extract 0 (val.endPos - ⟨2⟩)
   | _                 => throwErrorAt stx "unexpected doc string{indentD stx.raw[1]}"
 
-def TSyntax.getDocString (stx : TSyntax `Lean.Parser.Command.docComment) : String :=
-  match stx.raw[1] with
-  | Syntax.atom _ val => val.extract 0 (val.endPos - ⟨2⟩)
-  | _                 => ""
-
 end Lean

src/Lean/Elab/Tactic.lean

@@ -34,3 +34,5 @@ import Lean.Elab.Tactic.FalseOrByContra
 import Lean.Elab.Tactic.Omega
 import Lean.Elab.Tactic.Simpa
 import Lean.Elab.Tactic.NormCast
+import Lean.Elab.Tactic.Symm
+import Lean.Elab.Tactic.SolveByElim

src/Lean/Elab/Tactic/SolveByElim.lean

@@ -0,0 +1,113 @@
+/-
+Copyright (c) 2021 Scott Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Morrison, David Renshaw
+-/
+prelude
+import Lean.Meta.Tactic.SolveByElim
+import Lean.Elab.Tactic.Config
+
+namespace Lean.Elab.Tactic
+open Meta
+
+open Lean.Parser.Tactic
+open Lean.Parser.Tactic.SolveByElim
+
+open Lean.Meta.SolveByElim (SolveByElimConfig mkAssumptionSet)
+
+/--
+Allow elaboration of `Config` arguments to tactics.
+-/
+declare_config_elab elabConfig Lean.Meta.SolveByElim.SolveByElimConfig
+
+/--
+Allow elaboration of `ApplyRulesConfig` arguments to tactics.
+-/
+declare_config_elab elabApplyRulesConfig Lean.Meta.SolveByElim.ApplyRulesConfig
+
+/--
+Parse the lemma argument of a call to `solve_by_elim`.
+The first component should be true if `*` appears at least once.
+The second component should contain each term `t`in the arguments.
+The third component should contain `t` for each `-t` in the arguments.
+-/
+def parseArgs (s : Option (TSyntax ``args)) :
+    Bool × List Term × List Term :=
+  let args : Array (TSyntax ``arg) := match s with
+  | some s => match s with
+    | `(args| [$args,*]) => args.getElems
+    | _ => #[]
+  | none => #[]
+  let args : Array (Option (Term ⊕ Term)) := args.map fun t => match t with
+    | `(arg| $_:star) => none
+    | `(arg| - $t:term) => some (Sum.inr t)
+    | `(arg| $t:term) => some (Sum.inl t)
+    | _ => panic! "Unreachable parse of solve_by_elim arguments."
+  let args := args.toList
+  (args.contains none,
+    args.filterMap fun o => o.bind Sum.getLeft?,
+    args.filterMap fun o => o.bind Sum.getRight?)
+
+/-- Parse the `using ...` argument for `solve_by_elim`. -/
+def parseUsing (s : Option (TSyntax ``using_)) : Array Ident :=
+  match s with
+  | some s => match s with
+    | `(using_ | using $ids,*) => ids.getElems
+    | _ => #[]
+  | none => #[]
+
+/-- Wrapper for `solveByElim` that processes a list of `Term`s
+that specify the lemmas to use. -/
+def processSyntax (cfg : SolveByElimConfig := {}) (only star : Bool) (add remove : List Term)
+    (use : Array Ident) (goals : List MVarId) : MetaM (List MVarId) := do
+  if !remove.isEmpty && goals.length > 1 then
+    throwError "Removing local hypotheses is not supported when operating on multiple goals."
+  let ⟨lemmas, ctx⟩ ← mkAssumptionSet only star add remove use
+  SolveByElim.solveByElim cfg lemmas ctx goals
+
+@[builtin_tactic Lean.Parser.Tactic.applyAssumption]
+def evalApplyAssumption : Tactic := fun stx =>
+  match stx with
+  | `(tactic| apply_assumption $[$cfg]? $[only%$o]? $[$t:args]? $[$use:using_]?) => do
+    let (star, add, remove) := parseArgs t
+    let use := parseUsing use
+    let cfg ← elabConfig (mkOptionalNode cfg)
+    let cfg := { cfg with
+      backtracking := false
+      maxDepth := 1 }
+    replaceMainGoal (← processSyntax cfg o.isSome star add remove use [← getMainGoal])
+  | _ => throwUnsupportedSyntax
+
+/--
+Elaborator for apply_rules.
+
+See `Lean.MVarId.applyRules` for a `MetaM` level analogue of this tactic.
+-/
+@[builtin_tactic Lean.Parser.Tactic.applyRules]
+def evalApplyRules : Tactic := fun stx =>
+  match stx with
+  | `(tactic| apply_rules $[$cfg]? $[only%$o]? $[$t:args]? $[$use:using_]?) => do
+    let (star, add, remove) := parseArgs t
+    let use := parseUsing use
+    let cfg ← elabApplyRulesConfig (mkOptionalNode cfg)
+    let cfg := { cfg with backtracking := false }
+    liftMetaTactic fun g => processSyntax cfg o.isSome star add remove use [g]
+  | _ => throwUnsupportedSyntax
+
+@[builtin_tactic Lean.Parser.Tactic.solveByElim]
+def evalSolveByElim : Tactic := fun stx =>
+  match stx with
+  | `(tactic| solve_by_elim $[*%$s]? $[$cfg]? $[only%$o]? $[$t:args]? $[$use:using_]?) => do
+    let (star, add, remove) := parseArgs t
+    let use := parseUsing use
+    let goals ← if s.isSome then
+      getGoals
+    else
+      pure [← getMainGoal]
+    let cfg ← elabConfig (mkOptionalNode cfg)
+    let [] ← processSyntax cfg o.isSome star add remove use goals |
+      throwError "solve_by_elim unexpectedly returned subgoals"
+    pure ()
+  | _ => throwUnsupportedSyntax
+
+end Lean.Elab.Tactic

src/Lean/Elab/Tactic/Symm.lean

@@ -0,0 +1,26 @@
+/-
+Copyright (c) 2022 Siddhartha Gadgil. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Siddhartha Gadgil, Mario Carneiro, Scott Morrison
+-/
+prelude
+import Lean.Meta.Tactic.Symm
+import Lean.Elab.Tactic.Location
+
+namespace Lean.Elab.Tactic
+
+@[builtin_tactic Lean.Parser.Tactic.symm]
+def evalSymm : Tactic := fun stx =>
+  match stx with
+  | `(tactic| symm $(loc)) => do
+    let atHyp h := liftMetaTactic1 fun g => g.applySymmAt h
+    let atTarget := liftMetaTactic1 fun g => g.applySymm
+    withLocation (expandOptLocation loc) atHyp atTarget fun _ => throwError "symm made no progress"
+  | _ => throwUnsupportedSyntax
+
+@[builtin_tactic Lean.Parser.Tactic.symmSaturate]
+def evalSymmSaturate : Tactic := fun stx =>
+  match stx with
+  | `(tactic| symm_saturate) => do
+    liftMetaTactic1 fun g => g.symmSaturate
+  | _ => throwUnsupportedSyntax

src/Lean/LabelAttribute.lean

@@ -0,0 +1,82 @@
+/-
+Copyright (c) 2023 Scott Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Morrison
+-/
+prelude
+import Lean.ScopedEnvExtension
+import Lean.DocString
+
+/-!
+# "Label" attributes
+
+Allow creating attributes using `register_label_attr`,
+and retrieving the array of `Name`s of declarations which have been tagged with such an attribute.
+
+These differ slightly from the built-in "tag attributes" which can be initialized with the syntax:
+```
+initialize someName : TagAttribute ← registerTagAttribute `tagName "description"
+```
+in that a "tag attribute" can only be put on a declaration at the moment it is declared,
+and can not be modified by scoping commands.
+
+The "label attributes" constructed here support adding (or locally removing) the attribute
+either at the moment of declaration, or later.
+
+-/
+
+namespace Lean
+
+/-- An environment extension that just tracks an array of names. -/
+abbrev LabelExtension := SimpleScopedEnvExtension Name (Array Name)
+
+/-- The collection of all current `LabelExtension`s, indexed by name. -/
+abbrev LabelExtensionMap := HashMap Name LabelExtension
+
+/-- Store the current `LabelExtension`s. -/
+builtin_initialize labelExtensionMapRef : IO.Ref LabelExtensionMap ← IO.mkRef {}
+
+/-- Helper function for `registerLabelAttr`. -/
+def mkLabelExt (name : Name := by exact decl_name%) : IO LabelExtension :=
+  registerSimpleScopedEnvExtension {
+    name     := name
+    initial  := #[]
+    addEntry := fun d e => if d.contains e then d else d.push e
+  }
+
+/-- Helper function for `registerLabelAttr`. -/
+def mkLabelAttr (attrName : Name) (attrDescr : String) (ext : LabelExtension)
+  (ref : Name := by exact decl_name%) : IO Unit :=
+registerBuiltinAttribute {
+  ref   := ref
+  name  := attrName
+  descr := attrDescr
+  applicationTime := AttributeApplicationTime.afterCompilation
+  add   := fun declName _ _ =>
+    ext.add declName
+  erase := fun declName => do
+    let s := ext.getState (← getEnv)
+    modifyEnv fun env => ext.modifyState env fun _ => s.erase declName
+}
+
+/--
+Construct a new "label attribute",
+which does nothing except keep track of the names of the declarations with that attribute.
+
+Users will generally use the `register_label_attr` macro defined below.
+-/
+def registerLabelAttr (attrName : Name) (attrDescr : String)
+    (ref : Name := by exact decl_name%) : IO LabelExtension := do
+  let ext ← mkLabelExt ref
+  mkLabelAttr attrName attrDescr ext ref
+  labelExtensionMapRef.modify fun map => map.insert attrName ext
+  return ext
+
+/-- When `attrName` is an attribute created using `register_labelled_attr`,
+return the names of all declarations labelled using that attribute. -/
+def labelled (attrName : Name) : CoreM (Array Name) := do
+  match (← labelExtensionMapRef.get).find? attrName with
+  | none => throwError "No extension named {attrName}"
+  | some ext => pure <| ext.getState (← getEnv)
+
+end Lean

src/Lean/Meta.lean

@@ -44,3 +44,4 @@ import Lean.Meta.ExprLens
 import Lean.Meta.ExprTraverse
 import Lean.Meta.Eval
 import Lean.Meta.CoeAttr
+import Lean.Meta.Iterator

src/Lean/Meta/CollectMVars.lean

@@ -46,4 +46,39 @@ def getMVarsAtDecl (d : Declaration) : MetaM (Array MVarId) := do
   let (_, s) ← (collectMVarsAtDecl d).run {}
   pure s.result
 
+/--
+Collect the metavariables which `mvarId` depends on. These are the metavariables
+which appear in the type and local context of `mvarId`, as well as the
+metavariables which *those* metavariables depend on, etc.
+-/
+partial def _root_.Lean.MVarId.getMVarDependencies (mvarId : MVarId) (includeDelayed := false) :
+    MetaM (HashSet MVarId) :=
+  (·.snd) <$> (go mvarId).run {}
+where
+  /-- Auxiliary definition for `getMVarDependencies`. -/
+  addMVars (e : Expr) : StateRefT (HashSet MVarId) MetaM Unit := do
+    let mvars ← getMVars e
+    let mut s ← get
+    set ({} : HashSet MVarId) -- Ensure that `s` is not shared.
+    for mvarId in mvars do
+      if ← pure includeDelayed <||> notM (mvarId.isDelayedAssigned) then
+        s := s.insert mvarId
+    set s
+    mvars.forM go
+
+  /-- Auxiliary definition for `getMVarDependencies`. -/
+  go (mvarId : MVarId) : StateRefT (HashSet MVarId) MetaM Unit :=
+    withIncRecDepth do
+      let mdecl ← mvarId.getDecl
+      addMVars mdecl.type
+      for ldecl in mdecl.lctx do
+        addMVars ldecl.type
+        if let (some val) := ldecl.value? then
+          addMVars val
+      if let (some ass) ← getDelayedMVarAssignment? mvarId then
+        let pendingMVarId := ass.mvarIdPending
+        if ← notM pendingMVarId.isAssignedOrDelayedAssigned then
+          modify (·.insert pendingMVarId)
+        go pendingMVarId
+
 end Lean.Meta

src/Lean/Meta/Iterator.lean

@@ -0,0 +1,75 @@
+/-
+Copyright (c) 2024 Lean FRO. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joe Hendrix
+-/
+prelude
+import Lean.Meta.Basic
+
+namespace Lean.Meta
+
+/--
+Provides an iterface for iterating over values that are bundled with the `Meta` state
+they are valid in.
+-/
+protected structure Iterator (α : Type) where
+  /-- Function for getting next value and state pair. -/
+  next : MetaM (Option (α × Meta.SavedState))
+
+namespace Iterator
+
+/--
+Convert a list into an iterator with the current state.
+-/
+def ofList (l : List α) : MetaM (Meta.Iterator α) := do
+  let s ← saveState
+  let ref ← IO.mkRef l
+  let next := do
+    restoreState s
+    match ← ref.get with
+    | [] =>
+      pure none
+    | r :: l =>
+      ref.set l
+      pure <| some (r, ←saveState)
+  pure { next }
+
+/--
+Map and filter results of iterator and returning only those values returned
+by `f`.
+-/
+partial def filterMapM (f : α → MetaM (Option β)) (L : Meta.Iterator α) : Meta.Iterator β :=
+    { next := _next }
+  where _next := do
+    match ← L.next with
+    | none =>
+      pure none
+    | some (v, s) =>
+      restoreState s
+      let r ← f v
+      match r with
+      | none =>
+        _next
+      | some r =>
+        pure <| some (r, ←saveState)
+
+/--
+Find the first value in the iterator while resetting state or call `failure`
+if empty.
+-/
+def head (L : Meta.Iterator α) : MetaM α := do
+  match ← L.next with
+  | none =>
+    failure
+  | some (x, s) =>
+    restoreState s
+    pure x
+
+/--
+Return the first value returned by the iterator that `f` succeeds on.
+-/
+def firstM (L : Meta.Iterator α) (f : α → MetaM (Option β)) : MetaM β := L.filterMapM f |>.head
+
+end Iterator
+
+end Lean.Meta

src/Lean/Meta/Tactic.lean

@@ -33,3 +33,7 @@ import Lean.Meta.Tactic.Refl
 import Lean.Meta.Tactic.Congr
 import Lean.Meta.Tactic.Repeat
 import Lean.Meta.Tactic.NormCast
+import Lean.Meta.Tactic.IndependentOf
+import Lean.Meta.Tactic.Symm
+import Lean.Meta.Tactic.Backtrack
+import Lean.Meta.Tactic.SolveByElim

src/Lean/Meta/Tactic/Assert.lean

@@ -4,10 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import Init.Data.List.BasicAux
 import Lean.Meta.Tactic.FVarSubst
 import Lean.Meta.Tactic.Intro
 import Lean.Meta.Tactic.Revert
+import Lean.Util.ForEachExpr
 
 namespace Lean.Meta
 
@@ -28,6 +28,11 @@ def _root_.Lean.MVarId.assert (mvarId : MVarId) (name : Name) (type : Expr) (val
 def assert (mvarId : MVarId) (name : Name) (type : Expr) (val : Expr) : MetaM MVarId :=
   mvarId.assert name type val
 
+/-- Add the hypothesis `h : t`, given `v : t`, and return the new `FVarId`. -/
+def _root_.Lean.MVarId.note (g : MVarId) (h : Name) (v : Expr) (t? : Option Expr := .none) :
+    MetaM (FVarId × MVarId) := do
+  (← g.assert h (← match t? with | some t => pure t | none => inferType v) v).intro1P
+
 /--
   Convert the given goal `Ctx |- target` into `Ctx |- let name : type := val; target`.
   It assumes `val` has type `type` -/
@@ -115,4 +120,35 @@ def _root_.Lean.MVarId.assertHypotheses (mvarId : MVarId) (hs : Array Hypothesis
 def assertHypotheses (mvarId : MVarId) (hs : Array Hypothesis) : MetaM (Array FVarId × MVarId) := do
   mvarId.assertHypotheses hs
 
+
+/--
+Replace hypothesis `hyp` in goal `g` with `proof : typeNew`.
+The new hypothesis is given the same user name as the original,
+it attempts to avoid reordering hypotheses, and the original is cleared if possible.
+-/
+-- adapted from Lean.Meta.replaceLocalDeclCore
+def _root_.Lean.MVarId.replace (g : MVarId) (hyp : FVarId) (proof : Expr) (typeNew : Option Expr := none) :
+    MetaM AssertAfterResult :=
+  g.withContext do
+    let typeNew ← match typeNew with
+    | some t => pure t
+    | none => inferType proof
+    let ldecl ← hyp.getDecl
+    -- `typeNew` may contain variables that occur after `hyp`.
+    -- Thus, we use the auxiliary function `findMaxFVar` to ensure `typeNew` is well-formed
+    -- at the position we are inserting it.
+    let (_, ldecl') ← findMaxFVar typeNew |>.run ldecl
+    let result ← g.assertAfter ldecl'.fvarId ldecl.userName typeNew proof
+    (return { result with mvarId := ← result.mvarId.clear hyp }) <|> pure result
+where
+  /-- Finds the `LocalDecl` for the FVar in `e` with the highest index. -/
+  findMaxFVar (e : Expr) : StateRefT LocalDecl MetaM Unit :=
+    e.forEach' fun e => do
+      if e.isFVar then
+        let ldecl' ← e.fvarId!.getDecl
+        modify fun ldecl => if ldecl'.index > ldecl.index then ldecl' else ldecl
+        return false
+      else
+        return e.hasFVar
+
 end Lean.Meta

src/Lean/Meta/Tactic/Backtrack.lean

@@ -0,0 +1,205 @@
+/-
+Copyright (c) 2023 Scott Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Morrison
+-/
+prelude
+import Init.Data.List.BasicAux
+import Lean.Meta.Iterator
+import Lean.Meta.Tactic.IndependentOf
+
+/-!
+# `backtrack`
+
+A meta-tactic for running backtracking search, given a non-deterministic tactic
+`alternatives : MVarId → Nondet MetaM (List MVarId)`.
+
+`backtrack alternatives goals` will recursively try to solve all goals in `goals`,
+and the subgoals generated, backtracking as necessary.
+
+In its default behaviour, it will either solve all goals, or fail.
+A customisable `suspend` hook in `BacktrackConfig` allows suspend a goal (or subgoal),
+so that it will be returned instead of processed further.
+Other hooks `proc` and `discharge` (described in `BacktrackConfig`) allow running other
+tactics before `alternatives`, or if all search branches from a given goal fail.
+
+Currently only `solveByElim` is implemented in terms of `backtrack`.
+-/
+
+namespace Lean.Meta.Tactic.Backtrack
+
+open Lean Meta
+
+/--
+Configuration structure to control the behaviour of `backtrack`:
+* control the maximum depth and behaviour (fail or return subgoals) at the maximum depth,
+* and hooks allowing
+  * modifying intermediate goals before running the external tactic,
+  * 'suspending' goals, returning them in the result, and
+  * discharging subgoals if the external tactic fails.
+-/
+structure BacktrackConfig where
+  /-- Maximum recursion depth. -/
+  maxDepth : Nat := 6
+  /-- An arbitrary procedure which can be used to modify the list of goals
+  before each attempt to generate alternatives.
+  Called as `proc goals curr`, where `goals` are the original goals for `backtracking`,
+  and `curr` are the current goals.
+  Returning `some l` will replace the current goals with `l` and recurse
+  (consuming one step of maximum depth).
+  Returning `none` will proceed to generating alternative without changing goals.
+  Failure will cause backtracking.
+  (defaults to `none`) -/
+  proc : List MVarId → List MVarId → MetaM (Option (List MVarId)) := fun _ _ => pure none
+  /-- If `suspend g`, then we do not consider alternatives for `g`,
+  but return `g` as a new subgoal. (defaults to `false`) -/
+  suspend : MVarId → MetaM Bool := fun _ => pure false
+  /-- `discharge g` is called on goals for which there were no alternatives.
+  If `none` we return `g` as a new subgoal.
+  If `some l`, we replace `g` by `l` in the list of active goals, and recurse.
+  If failure, we backtrack. (defaults to failure) -/
+  discharge : MVarId → MetaM (Option (List MVarId)) := fun _ => failure
+  /--
+  If we solve any "independent" goals, don't fail.
+  See `Lean.MVarId.independent?` for the definition of independence.
+  -/
+  commitIndependentGoals : Bool := false
+
+namespace Backtrack
+
+/--
+Pretty print a list of goals.
+-/
+private def ppMVarId (g : MVarId) : MetaM Format := ppExpr =<< g.getType
+
+/--
+Pretty print a list of goals.
+-/
+private def ppMVarIds (gs : List MVarId) : MetaM (List Format) := gs.mapM ppMVarId
+
+/-- Run a monadic function on every element of a list,
+returning the list of elements on which the function fails, and the list of successful results. -/
+def tryAllM [Monad m] [Alternative m] (L : List α) (f : α → m β) : m (List α × List β) := do
+  let R ← L.mapM (fun a => (Sum.inr <$> f a) <|> (pure (Sum.inl a)))
+  return (R.filterMap (fun s => match s with | .inl a => a | _ => none),
+    R.filterMap (fun s => match s with | .inr b => b | _ => none))
+
+variable (cfg : BacktrackConfig)
+variable (trace : Name := .anonymous)
+variable (next : MVarId → (List MVarId → MetaM (Option (List MVarId))) → MetaM (List MVarId))
+
+/--
+* `n : Nat` steps remaining.
+* `curr : List MVarId` the current list of unsolved goals.
+* `acc : List MVarId` a list of "suspended" goals, which will be returned as subgoals.
+-/
+  -- `acc` is intentionally a `List` rather than an `Array` so we can share across branches.
+private def run (goals : List MVarId) (n : Nat) (curr acc : List MVarId) : MetaM (List MVarId) := do
+  match n with
+  | 0 => do
+    -- We're out of fuel.
+    throwError "backtrack exceeded the recursion limit"
+  | n + 1 => do
+  -- First, run `cfg.proc`, to see if it wants to modify the goals.
+  let procResult? ← try
+    cfg.proc goals curr
+  catch e =>
+    withTraceNode trace
+      (return m!"{exceptEmoji ·} BacktrackConfig.proc failed: {e.toMessageData}") do
+    throw e
+  match procResult? with
+  | some curr' => run goals n curr' acc
+  | none =>
+  match curr with
+  -- If there are no active goals, return the accumulated goals.
+  | [] => withTraceNode trace (return m!"{exceptEmoji ·} success!") do
+      return acc.reverse
+  | g :: gs =>
+  -- Discard any goals which have already been assigned.
+  if ← g.isAssigned then
+    withTraceNode trace (return m!"{exceptEmoji ·} discarding already assigned goal {g}") do
+      run goals (n+1) gs acc
+  else
+  withTraceNode trace
+    -- Note: the `addMessageContextFull` ensures we show the goal using the mvar context before
+    -- the `do` block below runs, potentially unifying mvars in the goal.
+    (return m!"{exceptEmoji ·} working on: {← addMessageContextFull g}")
+    do
+      -- Check if we should suspend the search here:
+      if (← cfg.suspend g) then
+        withTraceNode trace
+          (fun _ => return m!"⏸️ suspending search and returning as subgoal") do
+        run goals (n+1) gs (g :: acc)
+      else
+        try
+          -- We attempt to find an alternative,
+          -- for which all resulting sub-goals can be discharged using `run n`.
+          next g (fun r => observing? do run goals n (r ++ gs) acc)
+        catch _ =>
+          -- No lemmas could be applied:
+          match (← cfg.discharge g) with
+          | none => (withTraceNode trace
+              (fun _ => return m!"⏭️ deemed acceptable, returning as subgoal") do
+            run goals (n+1) gs (g :: acc))
+          | some l => (withTraceNode trace
+              (fun _ => return m!"⏬ discharger generated new subgoals") do
+            run goals n (l ++ gs) acc)
+
+/--
+A wrapper around `run`, which works on "independent" goals separately first,
+to reduce backtracking.
+-/
+private partial def processIndependentGoals (orig : List MVarId) (goals remaining : List MVarId) :
+    MetaM (List MVarId) := do
+  -- Partition the remaining goals into "independent" goals
+  -- (which should be solvable without affecting the solvability of other goals)
+  -- and all the others.
+  let (igs, ogs) ← remaining.partitionM (MVarId.isIndependentOf goals)
+  if igs.isEmpty then
+    -- If there are no independent goals, we solve all the goals together via backtracking search.
+    return (← run cfg trace next orig cfg.maxDepth remaining [])
+  else
+    withTraceNode trace
+      (fun _ => return m!"independent goals {← ppMVarIds igs},"
+        ++ m!" working on them before {← ppMVarIds ogs}") do
+    -- Invoke `run` on each of the independent goals separately,
+    -- gathering the subgoals on which `run` fails,
+    -- and the new subgoals generated from goals on which it is successful.
+    let (failed, newSubgoals') ← tryAllM igs fun g =>
+      run cfg trace next orig cfg.maxDepth [g] []
+    let newSubgoals := newSubgoals'.join
+    withTraceNode trace
+      (fun _ => return m!"failed: {← ppMVarIds failed}, new: {← ppMVarIds newSubgoals}") do
+    -- Update the list of goals with respect to which we need to check independence.
+    let goals' := (← goals.filterM (fun g => do pure !(← g.isAssigned))) ++ newSubgoals
+    -- If `commitIndependentGoals` is `true`, we will return the new goals
+    -- regardless of whether we can make further progress on the other goals.
+    if cfg.commitIndependentGoals && !newSubgoals.isEmpty then
+      return newSubgoals ++ failed ++ (← (processIndependentGoals orig goals' ogs <|> pure ogs))
+    else if !failed.isEmpty then
+      -- If `commitIndependentGoals` is `false`, and we failed on any of the independent goals,
+      -- then overall failure is inevitable so we can stop here.
+      failure
+    else
+      -- Finally, having solved this batch of independent goals,
+      -- recurse (potentially now finding new independent goals).
+      return newSubgoals ++ (← processIndependentGoals orig goals' ogs)
+
+end Backtrack
+
+
+/--
+Attempts to solve the `goals`, by recursively calling `next` on each
+subgoal that appears with a callback to reenter backtracking search.
+
+Further flow control options are available via the `Config` argument.
+
+Returns a list of subgoals which were "suspended" via the `suspend` or
+`discharge` hooks in `Config`. In the default configuration, `backtrack`
+will either return an empty list or fail.
+-/
+def backtrack (cfg : BacktrackConfig := {}) (trace : Name := .anonymous)
+    (next : MVarId → MetaM (Meta.Iterator (List MVarId)))
+    (goals : List MVarId) : MetaM (List MVarId) := do
+  let resolve g f := do (←next g).firstM f
+  Backtrack.processIndependentGoals cfg trace resolve goals goals goals

src/Lean/Meta/Tactic/IndependentOf.lean

@@ -0,0 +1,58 @@
+/-
+Copyright (c) 2022 Mario Carneiro. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mario Carneiro, Jannis Limperg
+-/
+prelude
+import Lean.Meta.CollectMVars
+import Lean.Meta.Tactic.Util
+
+namespace Lean.MVarId
+
+open Meta
+
+/--
+Check if a goal is "independent" of a list of other goals.
+We say a goal is independent of other goals if assigning a value to it
+can not change the assignability of the other goals.
+
+Examples:
+* `?m_1 : Type` is not independent of `?m_2 : ?m_1`,
+  because we could assign `true : Bool` to `?m_2`,
+  but if we first assign `Nat` to `?m_1` then that is no longer possible.
+* `?m_1 : Nat` is not independent of `?m_2 : Fin ?m_1`,
+  because we could assign `37 : Fin 42` to `?m_2`,
+  but if we first assign `2` to `?m_1` then that is no longer possible.
+* `?m_1 : ?m_2` is not independent of `?m_2 : Type`, because we could assign `Bool` to ?m_2`,
+  but if we first assign `0 : Nat` to `?m_1` then that is no longer possible.
+* Given `P : Prop` and `f : P → Type`, `?m_1 : P` is independent of `?m_2 : f ?m_1`
+  by proof irrelevance.
+* Similarly given `f : Fin 0 → Type`, `?m_1 : Fin 0` is independent of `?m_2 : f ?m_1`,
+  because `Fin 0` is a subsingleton.
+* Finally `?m_1 : Nat` is independent of `?m_2 : α`,
+  as long as `?m_1` does not appear in `Meta.getMVars α`
+  (note that `Meta.getMVars` follows delayed assignments).
+
+This function only calculates a conservative approximation of this condition.
+That is, it may return `false` when it should return `true`.
+(In particular it returns false whenever the type of `g` contains a metavariable,
+regardless of whether this is related to the metavariables in `L`.)
+-/
+def isIndependentOf (L : List MVarId) (g : MVarId) : MetaM Bool := g.withContext do
+  let t ← instantiateMVars (← g.getType)
+  if t.hasExprMVar then
+    -- If the goal's type contains other meta-variables,
+    -- we conservatively say that `g` is not independent.
+    -- It would be possible to check if `L` depends on these meta-variables.
+    return false
+  if (← inferType t).isProp then
+    -- If the goal is propositional,
+    -- proof-irrelevance ensures it is independent of any other goals.
+    return true
+  if ← g.isSubsingleton then
+    -- If the goal is a subsingleton, it is independent of any other goals.
+    return true
+  -- Finally, we check if the goal `g` appears in the type of any of the goals `L`.
+  L.allM fun g' => do pure !((← getMVarDependencies g').contains g)
+
+end Lean.MVarId

src/Lean/Meta/Tactic/SolveByElim.lean

@@ -0,0 +1,358 @@
+/-
+Copyright (c) 2021 Scott Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Morrison, David Renshaw
+-/
+prelude
+import Init.Data.Sum
+import Lean.LabelAttribute
+import Lean.Meta.Tactic.Apply
+import Lean.Meta.Tactic.Backtrack
+import Lean.Meta.Tactic.Constructor
+import Lean.Meta.Tactic.Repeat
+import Lean.Meta.Tactic.Symm
+import Lean.Elab.Term
+
+/-!
+# `solve_by_elim`, `apply_rules`, and `apply_assumption`.
+
+`solve_by_elim` takes a collection of facts from the local context or
+supplied as arguments by the user, and performs a backtracking
+depth-first search by attempting to `apply` these facts to the goal.
+
+It is a highly configurable tactic, with options to control the
+backtracking, to solve multiple goals simultaneously (with backtracking
+between goals), or to supply a discharging tactic for unprovable goals.
+
+`apply_rules` and `apply_assumption` are much simpler tactics which do
+not perform backtracking, but are currently implemented in terms of
+`solve_by_elim` with backtracking disabled, in order to be able to share
+the front-end customisation and parsing of user options. It would be
+reasonable to further separate these in future.
+-/
+
+open Lean Meta Elab Tactic
+
+namespace Lean.Meta.SolveByElim
+
+initialize registerTraceClass `Meta.Tactic.solveByElim
+
+/--
+`applyTactics lemmas goal` will return an iterator that applies the
+lemmas to the goal `goal` and returns ones that succeed.
+
+Providing this to the `backtracking` tactic,
+we can perform backtracking search based on applying a list of lemmas.
+
+``applyTactics (trace := `name)`` will construct trace nodes for ``name` indicating which
+calls to `apply` succeeded or failed.
+-/
+def applyTactics (cfg : ApplyConfig := {}) (transparency : TransparencyMode := .default)
+    (lemmas : List Expr) (g : MVarId) : MetaM (Lean.Meta.Iterator (List Lean.MVarId)) := do
+  pure <|
+    (← Meta.Iterator.ofList lemmas).filterMapM (fun e => observing? do
+      withTraceNode `Meta.Tactic.solveByElim (return m!"{exceptEmoji ·} trying to apply: {e}") do
+        let goals ← withTransparency transparency (g.apply e cfg)
+        -- When we call `apply` interactively, `Lean.Elab.Tactic.evalApplyLikeTactic`
+        -- deals with closing new typeclass goals by calling
+        -- `Lean.Elab.Term.synthesizeSyntheticMVarsNoPostponing`.
+        -- It seems we can't reuse that machinery down here in `MetaM`,
+        -- so we just settle for trying to close each subgoal using `inferInstance`.
+        goals.filterM fun g => try g.inferInstance; pure false catch _ => pure true)
+
+/--
+`applyFirst lemmas goal` applies the first of the `lemmas`
+which can be successfully applied to `goal`, and fails if none apply.
+
+We use this in `apply_rules` and `apply_assumption` where backtracking is not needed.
+-/
+def applyFirst (cfg : ApplyConfig := {}) (transparency : TransparencyMode := .default)
+    (lemmas : List Expr) (g : MVarId) : MetaM (List MVarId) := do
+  (←applyTactics cfg transparency lemmas g).head
+
+open Lean.Meta.Tactic.Backtrack (BacktrackConfig backtrack)
+
+/-- The default `maxDepth` for `apply_rules` is higher. -/
+structure ApplyRulesConfig extends BacktrackConfig, ApplyConfig where
+  /-- Transparency mode for calls to `apply`. -/
+  transparency : TransparencyMode := .default
+  /-- Also use symmetric versions (via `@[symm]`) of local hypotheses. -/
+  symm : Bool := true
+  /-- Try proving the goal via `exfalso` if `solve_by_elim` otherwise fails.
+  This is only used when operating on a single goal. -/
+  exfalso : Bool := true
+  maxDepth := 50
+
+/--
+Configuration structure to control the behaviour of `solve_by_elim`:
+* transparency mode for calls to `apply`
+* whether to use `symm` on hypotheses and `exfalso` on the goal as needed,
+* see also `BacktrackConfig` for hooks allowing flow control.
+-/
+structure SolveByElimConfig extends ApplyRulesConfig where
+  /-- Enable backtracking search. -/
+  backtracking : Bool := true
+  maxDepth := 6
+  /-- Trying calling `intro` if no lemmas apply. -/
+  intro : Bool := true
+  /-- Try calling `constructor` if no lemmas apply. -/
+  constructor : Bool := true
+
+namespace SolveByElimConfig
+
+instance : Coe SolveByElimConfig BacktrackConfig := ⟨(·.toApplyRulesConfig.toBacktrackConfig)⟩
+
+/-- Create or modify a `Config` which allows a class of goals to be returned as subgoals. -/
+def accept (cfg : SolveByElimConfig := {}) (test : MVarId → MetaM Bool) : SolveByElimConfig :=
+  { cfg with
+    discharge := fun g => do
+      if (← test g) then
+        pure none
+      else
+        cfg.discharge g }
+
+/--
+Create or modify a `Config` which runs a tactic on the main goal.
+If that tactic fails, fall back to the `proc` behaviour of `cfg`.
+-/
+def mainGoalProc (cfg : SolveByElimConfig := {}) (proc : MVarId → MetaM (List MVarId)) : SolveByElimConfig :=
+  { cfg with
+    proc := fun orig goals => match goals with
+    | [] => cfg.proc orig []
+    | g :: gs => try
+        return (← proc g) ++ gs
+      catch _ => cfg.proc orig goals }
+
+/-- Create or modify a `Config` which calls `intro` on each goal before applying lemmas. -/
+-- Because `SolveByElim` works on each goal in sequence, even though
+-- `mainGoalProc` only applies this operation on the main goal,
+-- it is applied to every goal before lemmas are applied.
+def intros (cfg : SolveByElimConfig := {}) : SolveByElimConfig :=
+  cfg.mainGoalProc fun g => do pure [(← g.intro1P).2]
+
+/-- Attempt typeclass inference on each goal, before applying lemmas. -/
+-- Because `SolveByElim` works on each goal in sequence, even though
+-- `mainGoalProc` only applies this operation on the main goal,
+-- it is applied to every goal before lemmas are applied.
+def synthInstance (cfg : SolveByElimConfig := {}) : SolveByElimConfig :=
+  cfg.mainGoalProc fun g => do
+    g.assign (← Lean.Meta.synthInstance (← g.getType))
+    pure []
+
+/-- Add a discharging tactic, falling back to the original discharging tactic if it fails.
+Return `none` to return the goal as a new subgoal, or `some goals` to replace it. -/
+def withDischarge (cfg : SolveByElimConfig := {}) (discharge : MVarId → MetaM (Option (List MVarId))) : SolveByElimConfig :=
+  { cfg with
+    discharge := fun g => try discharge g
+      catch _ => cfg.discharge g }
+
+/-- Create or modify a `SolveByElimConfig` which calls `intro` on any goal for which no lemma applies. -/
+def introsAfter (cfg : SolveByElimConfig := {}) : SolveByElimConfig :=
+  cfg.withDischarge fun g => do pure [(← g.intro1P).2]
+
+/-- Call `constructor` when no lemmas apply. -/
+def constructorAfter (cfg : SolveByElimConfig := {}) : SolveByElimConfig :=
+  cfg.withDischarge fun g => g.constructor {newGoals := .all}
+
+/-- Create or modify a `Config` which
+calls `synthInstance` on any goal for which no lemma applies. -/
+def synthInstanceAfter (cfg : SolveByElimConfig := {}) : SolveByElimConfig :=
+  cfg.withDischarge fun g => do
+    g.assign (← Lean.Meta.synthInstance (← g.getType))
+    pure (some [])
+
+/--
+Create or modify a `Config` which rejects branches for which `test`,
+applied to the instantiations of the original goals, fails or returns `false`.
+-/
+def testPartialSolutions (cfg : SolveByElimConfig := {}) (test : List Expr → MetaM Bool) : SolveByElimConfig :=
+  { cfg with
+    proc := fun orig goals => do
+      let .true ← test (← orig.mapM fun m => m.withContext do instantiateMVars (.mvar m)) | failure
+      cfg.proc orig goals }
+
+/--
+Create or modify a `SolveByElimConfig` which rejects complete solutions for which `test`,
+applied to the instantiations of the original goals, fails or returns `false`.
+-/
+def testSolutions (cfg : SolveByElimConfig := {}) (test : List Expr → MetaM Bool) : SolveByElimConfig :=
+  cfg.testPartialSolutions fun sols => do
+    if sols.any Expr.hasMVar then
+      pure true
+    else
+      test sols
+
+/--
+Create or modify a `Config` which only accept solutions
+for which every expression in `use` appears as a subexpression.
+-/
+def requireUsingAll (cfg : SolveByElimConfig := {}) (use : List Expr) : SolveByElimConfig :=
+  cfg.testSolutions fun sols => do
+    pure <| use.all fun e => sols.any fun s => e.occurs s
+
+/--
+Process the `intro` and `constructor` options by implementing the `discharger` tactic.
+-/
+def processOptions (cfg : SolveByElimConfig) : SolveByElimConfig :=
+  let cfg := if cfg.intro then introsAfter { cfg with intro := false } else cfg
+  let cfg := if cfg.constructor then constructorAfter { cfg with constructor := false } else cfg
+  cfg
+
+end SolveByElimConfig
+
+/--
+Elaborate a list of lemmas and local context.
+See `mkAssumptionSet` for an explanation of why this is needed.
+-/
+def elabContextLemmas (g : MVarId) (lemmas : List (TermElabM Expr)) (ctx : TermElabM (List Expr)) :
+    MetaM (List Expr) := do
+  g.withContext (Elab.Term.TermElabM.run' do pure ((← ctx) ++ (← lemmas.mapM id)))
+
+/-- Returns the list of tactics corresponding to applying the available lemmas to the goal. -/
+def applyLemmas (cfg : SolveByElimConfig) (lemmas : List (TermElabM Expr)) (ctx : TermElabM (List Expr))
+    (g : MVarId)
+    : MetaM (Meta.Iterator (List MVarId)) := do
+  let es ← elabContextLemmas g lemmas ctx
+  applyTactics cfg.toApplyConfig cfg.transparency es g
+
+/-- Applies the first possible lemma to the goal. -/
+def applyFirstLemma (cfg : SolveByElimConfig) (lemmas : List (TermElabM Expr)) (ctx : TermElabM (List Expr))
+    (g : MVarId) : MetaM (List MVarId) := do
+let es ← elabContextLemmas g lemmas ctx
+applyFirst cfg.toApplyConfig cfg.transparency es g
+
+/--
+Solve a collection of goals by repeatedly applying lemmas, backtracking as necessary.
+
+Arguments:
+* `cfg : SolveByElimConfig` additional configuration options
+  (options for `apply`, maximum depth, and custom flow control)
+* `lemmas : List (TermElabM Expr)` lemmas to apply.
+  These are thunks in `TermElabM` to avoid stuck metavariables.
+* `ctx : TermElabM (List Expr)` monadic function returning the local hypotheses to use.
+* `goals : List MVarId` the initial list of goals for `solveByElim`
+
+Returns a list of suspended goals, if it succeeded on all other subgoals.
+By default `cfg.suspend` is `false,` `cfg.discharge` fails, and `cfg.failAtMaxDepth` is `true`,
+and so the returned list is always empty.
+Custom wrappers (e.g. `apply_assumption` and `apply_rules`) may modify this behaviour.
+-/
+def solveByElim (cfg : SolveByElimConfig) (lemmas : List (TermElabM Expr)) (ctx : TermElabM (List Expr))
+    (goals : List MVarId) : MetaM (List MVarId) := do
+  let cfg := cfg.processOptions
+  -- We handle `cfg.symm` by saturating hypotheses of all goals using `symm`.
+  -- This has better performance that the mathlib3 approach.
+  let preprocessedGoals ← if cfg.symm then
+    goals.mapM fun g => g.symmSaturate
+  else
+    pure goals
+  try
+    run cfg preprocessedGoals
+  catch e => do
+    -- Implementation note: as with `cfg.symm`, this is different from the mathlib3 approach,
+    -- for (not as severe) performance reasons.
+    match preprocessedGoals, cfg.exfalso with
+    | [g], true =>
+      withTraceNode `Meta.Tactic.solveByElim
+          (fun _ => return m!"⏮️ starting over using `exfalso`") do
+        run cfg [← g.exfalso]
+    | _, _ => throw e
+where
+  /-- Run either backtracking search, or repeated application, on the list of goals. -/
+  run (cfg : SolveByElimConfig) : List MVarId → MetaM (List MVarId) :=
+    if cfg.backtracking then
+      backtrack cfg `Meta.Tactic.solveByElim (applyLemmas cfg lemmas ctx)
+    else
+      Lean.Meta.repeat1' (maxIters := cfg.maxDepth) (applyFirstLemma cfg lemmas ctx)
+
+/--
+A `MetaM` analogue of the `apply_rules` user tactic.
+
+We pass the lemmas as `TermElabM Expr` rather than just `Expr`,
+so they can be generated fresh for each application, to avoid stuck metavariables.
+
+By default it uses all local hypotheses, but you can disable this with `only := true`.
+If you need to remove particular local hypotheses, call `solveByElim` directly.
+-/
+def _root_.Lean.MVarId.applyRules (cfg : SolveByElimConfig) (lemmas : List (TermElabM Expr))
+    (only : Bool := false) (g : MVarId) : MetaM (List MVarId) := do
+  let ctx : TermElabM (List Expr) := if only then pure [] else do pure (← getLocalHyps).toList
+  solveByElim { cfg with backtracking := false } lemmas ctx [g]
+
+open Lean.Parser.Tactic
+
+/--
+`mkAssumptionSet` builds a collection of lemmas for use in
+the backtracking search in `solve_by_elim`.
+
+* By default, it includes all local hypotheses, along with `rfl`, `trivial`, `congrFun`
+  and `congrArg`.
+* The flag `noDefaults` removes these.
+* The flag `star` includes all local hypotheses, but not `rfl`, `trivial`, `congrFun`,
+  or `congrArg`. (It doesn't make sense to use `star` without `noDefaults`.)
+* The argument `add` is the list of terms inside the square brackets that did not have `-`
+  and can be used to add expressions or local hypotheses
+* The argument `remove` is the list of terms inside the square brackets that had a `-`,
+  and can be used to remove local hypotheses.
+  (It doesn't make sense to remove expressions which are not local hypotheses,
+  to remove local hypotheses unless `!noDefaults || star`,
+  and it does not make sense to use `star` unless you remove at least one local hypothesis.)
+
+`mkAssumptionSet` returns not a `List expr`, but a `List (TermElabM Expr) × TermElabM (List Expr)`.
+There are two separate problems that need to be solved.
+
+### Stuck metavariables
+
+Lemmas with implicit arguments would be filled in with metavariables if we created the
+`Expr` objects immediately, so instead we return thunks that generate the expressions
+on demand. This is the first component, with type `List (TermElabM Expr)`.
+
+As an example, we have `def rfl : ∀ {α : Sort u} {a : α}, a = a`, which on elaboration will become
+`@rfl ?m_1 ?m_2`.
+
+Because `solve_by_elim` works by repeated application of lemmas against subgoals,
+the first time such a lemma is successfully applied,
+those metavariables will be unified, and thereafter have fixed values.
+This would make it impossible to apply the lemma
+a second time with different values of the metavariables.
+
+See https://github.com/leanprover-community/mathlib/issues/2269
+
+### Relevant local hypotheses
+
+`solve_by_elim*` works with multiple goals,
+and we need to use separate sets of local hypotheses for each goal.
+The second component of the returned value provides these local hypotheses.
+(Essentially using `getLocalHyps`, along with some filtering to remove hypotheses
+that have been explicitly removed via `only` or `[-h]`.)
+
+-/
+-- These `TermElabM`s must be run inside a suitable `g.withContext`,
+-- usually using `elabContextLemmas`.
+def mkAssumptionSet (noDefaults star : Bool) (add remove : List Term) (use : Array Ident) :
+    MetaM (List (TermElabM Expr) × TermElabM (List Expr)) := do
+  if star && !noDefaults then
+    throwError "It doesn't make sense to use `*` without `only`."
+
+  let defaults : List (TermElabM Expr) :=
+    [← `(rfl), ← `(trivial), ← `(congrFun), ← `(congrArg)].map elab'
+  let labelledLemmas := (← use.mapM (Lean.labelled ·.raw.getId)).flatten.toList
+    |>.map (liftM <| mkConstWithFreshMVarLevels ·)
+  let lemmas := if noDefaults then
+    add.map elab' ++ labelledLemmas
+  else
+    add.map elab' ++ labelledLemmas ++ defaults
+
+  if !remove.isEmpty && noDefaults && !star then
+    throwError "It doesn't make sense to remove local hypotheses when using `only` without `*`."
+  let locals : TermElabM (List Expr) := if noDefaults && !star then do
+    pure []
+  else do
+    pure <| (← getLocalHyps).toList.removeAll (← remove.mapM elab')
+
+  return (lemmas, locals)
+  where
+  /-- Run `elabTerm`. -/
+  elab' (t : Term) : TermElabM Expr := Elab.Term.elabTerm t.raw none
+
+open Syntax

src/Lean/Meta/Tactic/Symm.lean

@@ -0,0 +1,115 @@
+/-
+Copyright (c) 2022 Siddhartha Gadgil. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Siddhartha Gadgil, Mario Carneiro, Scott Morrison
+-/
+prelude
+import Lean.Meta.Reduce
+import Lean.Meta.Tactic.Assert
+
+/-!
+# `symm` tactic
+
+This implements the `symm` tactic, which can apply symmetry theorems to either the goal or a
+hypothesis.
+-/
+
+open Lean Meta
+
+namespace Lean.Meta.Symm
+
+/-- Discrimation tree settings for the `symm` extension. -/
+def symmExt.config : WhnfCoreConfig := {}
+
+/-- Environment extensions for symm lemmas -/
+builtin_initialize symmExt :
+    SimpleScopedEnvExtension (Name × Array DiscrTree.Key) (DiscrTree Name) ←
+  registerSimpleScopedEnvExtension {
+    addEntry := fun dt (n, ks) => dt.insertCore ks n
+    initial := {}
+  }
+
+builtin_initialize registerBuiltinAttribute {
+  name := `symm
+  descr := "symmetric relation"
+  add := fun decl _ kind => MetaM.run' do
+    let declTy := (← getConstInfo decl).type
+    let (xs, _, targetTy) ← withReducible <| forallMetaTelescopeReducing declTy
+    let fail := throwError
+      "@[symm] attribute only applies to lemmas proving x ∼ y → y ∼ x, got {declTy}"
+    let some _ := xs.back? | fail
+    let targetTy ← reduce targetTy
+    let .app (.app rel _) _ := targetTy | fail
+    let key ← withReducible <| DiscrTree.mkPath rel symmExt.config
+    symmExt.add (decl, key) kind
+}
+
+end Lean.Meta.Symm
+
+open Lean.Meta.Symm
+
+namespace Lean.Expr
+
+/-- Return the symmetry lemmas that match the target type. -/
+def getSymmLems (tgt : Expr) : MetaM (Array Name) := do
+  let .app (.app rel _) _ := tgt
+    | throwError "symmetry lemmas only apply to binary relations, not{indentExpr tgt}"
+  (symmExt.getState (← getEnv)).getMatch rel symmExt.config
+
+/-- Given a term `e : a ~ b`, construct a term in `b ~ a` using `@[symm]` lemmas. -/
+def applySymm (e : Expr) : MetaM Expr := do
+  let tgt <- instantiateMVars (← inferType e)
+  let lems ← getSymmLems tgt
+  let s ← saveState
+  let act lem := do
+        restoreState s
+        let lem ← mkConstWithFreshMVarLevels lem
+        let (args, _, body) ← withReducible <| forallMetaTelescopeReducing (← inferType lem)
+        let .true ← isDefEq args.back e | failure
+        mkExpectedTypeHint (mkAppN lem args) (← instantiateMVars body)
+  lems.toList.firstM act
+    <|> throwError m!"no applicable symmetry lemma found for {indentExpr tgt}"
+
+end Lean.Expr
+
+namespace Lean.MVarId
+
+/--
+Apply a symmetry lemma (i.e. marked with `@[symm]`) to a metavariable.
+
+The type of `g` should be of the form `a ~ b`, and is used to index the symm lemmas.
+-/
+def applySymm (g : MVarId) : MetaM MVarId := do
+  let tgt := (← instantiateMVars (← g.getType)).cleanupAnnotations
+  let lems ← Expr.getSymmLems tgt
+  let act lem : MetaM MVarId := do
+        let lem ← mkConstWithFreshMVarLevels lem
+        let (args, _, body) ← withReducible <| forallMetaTelescopeReducing (← inferType lem)
+        let .true ← isDefEq (← g.getType) body | failure
+        g.assign (mkAppN lem args)
+        let g' := args.back.mvarId!
+        g'.setTag (← g.getTag)
+        pure g'
+  lems.toList.firstM act
+    <|> throwError m!"no applicable symmetry lemma found for {indentExpr tgt}"
+
+/-- Use a symmetry lemma (i.e. marked with `@[symm]`) to replace a hypothesis in a goal. -/
+def applySymmAt (h : FVarId) (g : MVarId) : MetaM MVarId := do
+  let h' ← (Expr.fvar h).applySymm
+  pure (← g.replace h h').mvarId
+
+/-- For every hypothesis `h : a ~ b` where a `@[symm]` lemma is available,
+add a hypothesis `h_symm : b ~ a`. -/
+def symmSaturate (g : MVarId) : MetaM MVarId := g.withContext do
+  let mut g' := g
+  let hyps ← getLocalHyps
+  let types ← hyps.mapM inferType
+  for h in hyps do try
+    let symm ← h.applySymm
+    let symmType ← inferType symm
+    if ¬ (← types.anyM (isDefEq symmType)) then
+      (_, g') ← g'.note ((← h.fvarId!.getUserName).appendAfter "_symm") symm
+  catch _ => g' ← pure g'
+  return g'
+
+end Lean.MVarId

src/Lean/Meta/Tactic/Util.lean

@@ -169,4 +169,13 @@ inductive TacticResultCNM where
   | noChange
   | modified (mvarId : MVarId)
 
+
+/-- Check if a goal is of a subsingleton type. -/
+def _root_.Lean.MVarId.isSubsingleton (g : MVarId) : MetaM Bool := do
+  try
+    discard <| synthInstance (← mkAppM ``Subsingleton #[← g.getType])
+    return true
+  catch _ =>
+    return false
+
 end Lean.Meta

src/Lean/Util/Trace.lean

@@ -275,6 +275,11 @@ def exceptOptionEmoji : Except ε (Option α) → String
   | .ok (some _) => checkEmoji
   | .ok none => crossEmoji
 
+/-- Visualize an `Except` using a checkmark or a cross. -/
+def exceptEmoji : Except ε α → String
+  | .error _ => crossEmoji
+  | .ok _ => checkEmoji
+
 class ExceptToEmoji (ε α : Type) where
   toEmoji : Except ε α → String
 

tests/lean/interactive/1265.lean.expected.out

@@ -11,6 +11,9 @@
    "detail":
    "Lean.TSyntax Lean.interpolatedStrKind → Lean.Term → Lean.Term → Lean.MacroM Lean.Term"},
   {"label": "getChar", "kind": 3, "detail": "Lean.CharLit → Char"},
+  {"label": "getDocString",
+   "kind": 3,
+   "detail": "Lean.TSyntax `Lean.Parser.Command.docComment → String"},
   {"label": "getNat", "kind": 3, "detail": "Lean.NumLit → Nat"},
   {"label": "getScientific",
    "kind": 3,
@@ -35,6 +38,9 @@
    "detail":
    "Lean.TSyntax Lean.interpolatedStrKind → Lean.Term → Lean.Term → Lean.MacroM Lean.Term"},
   {"label": "getChar", "kind": 3, "detail": "Lean.CharLit → Char"},
+  {"label": "getDocString",
+   "kind": 3,
+   "detail": "Lean.TSyntax `Lean.Parser.Command.docComment → String"},
   {"label": "getNat", "kind": 3, "detail": "Lean.NumLit → Nat"},
   {"label": "getScientific",
    "kind": 3,