chore: rename register_tag_attr, and explain relation to registerTagAttribute (#2124)

Per [zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/TagAttribute/near/325879024).




Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Author: kim-em

Mathlib.lean

@@ -969,6 +969,7 @@ import Mathlib.Tactic.InferParam
 import Mathlib.Tactic.Inhabit
 import Mathlib.Tactic.IntervalCases
 import Mathlib.Tactic.IrreducibleDef
+import Mathlib.Tactic.LabelAttr
 import Mathlib.Tactic.LeftRight
 import Mathlib.Tactic.LibrarySearch
 import Mathlib.Tactic.Lift
@@ -1028,7 +1029,6 @@ import Mathlib.Tactic.Spread
 import Mathlib.Tactic.Substs
 import Mathlib.Tactic.SudoSetOption
 import Mathlib.Tactic.SwapVar
-import Mathlib.Tactic.TagAttr
 import Mathlib.Tactic.Tauto
 import Mathlib.Tactic.ToAdditive
 import Mathlib.Tactic.Trace

Mathlib/Tactic/LabelAttr.lean

@@ -0,0 +1,96 @@
+/-
+Copyright (c) 2023 Scott Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Morrison
+-/
+import Lean
+
+/-!
+# "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 initalized 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 atributes" constructed here adding (or locally removing) the attribute
+either at the moment of declaration, or later.
+
+-/
+
+namespace Mathlib.Tactic.LabelAttr
+
+open 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. -/
+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 => 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
+
+/--
+Initialize a new "label" attribute.
+Declarations tagged with the attribute can be retrieved using `Mathlib.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 s!"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)
+
+/-- When `attrName` is an attribute created using `register_labelled_attr`,
+return the names of all declarations labelled using that attribute. -/
+def labelled (attrName : Name) : MetaM (Array Name) := do
+  match (← labelExtensionMapRef.get).find? attrName with
+  | none => throwError "No extension named {attrName}"
+  | some ext => pure <| ext.getState (← getEnv)
+
+/-- A dummy label attribute, to ease testing. -/
+register_label_attr dummy_label_attr

Mathlib/Tactic/SolveByElim.lean

@@ -10,7 +10,7 @@ import Mathlib.Lean.LocalContext
 import Mathlib.Tactic.Relation.Symm
 import Mathlib.Control.Basic
 import Mathlib.Data.Sum.Basic
-import Mathlib.Tactic.TagAttr
+import Mathlib.Tactic.LabelAttr
 
 /-!
 A work-in-progress replacement for Lean3's `solve_by_elim` tactic.
@@ -294,7 +294,7 @@ def _root_.Lean.MVarId.applyRules (cfg : Config) (lemmas : List Expr) (only : Bo
   solveByElim { cfg.noBackTracking with failAtMaxDepth := false } lemmas ctx [g]
 
 open Lean.Parser.Tactic
-open Mathlib.Tactic.TagAttr
+open Mathlib.Tactic.LabelAttr
 
 /--
 `mkAssumptionSet` builds a collection of lemmas for use in
@@ -351,12 +351,12 @@ def mkAssumptionSet (noDefaults star : Bool) (add remove : List Term) (use : Arr
 
   let defaults : List (TermElabM Expr) :=
     [← `(rfl), ← `(trivial), ← `(congrFun), ← `(congrArg)].map elab'
-  let taggedLemmas := (← use.mapM (tagged ·.raw.getId)).flatten.toList
+  let labelledLemmas := (← use.mapM (labelled ·.raw.getId)).flatten.toList
     |>.map (liftM <| mkConstWithFreshMVarLevels ·)
   let lemmas := if noDefaults then
-    add.map elab' ++ taggedLemmas
+    add.map elab' ++ labelledLemmas
   else
-    add.map elab' ++ taggedLemmas ++ defaults
+    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 `*`."
@@ -378,7 +378,7 @@ syntax star := "*"
 syntax arg := star <|> erase <|> term
 /-- Syntax for adding and removing terms in `solve_by_elim`. -/
 syntax args := " [" SolveByElim.arg,* "] "
-/-- Syntax for using all lemmas tagged with an attribute in `solve_by_elim`. -/
+/-- Syntax for using all lemmas labelled with an attribute in `solve_by_elim`. -/
 syntax using_ := " using " ident,*
 
 open Syntax
@@ -431,8 +431,8 @@ The assumptions can be modified with similar syntax as for `simp`:
 * `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 tagged
-  with the attributes `aᵢ` (these attributes must be created using `register_tag_attr`).
+* `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.
@@ -484,8 +484,8 @@ 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 tagged
-with the attributes `aᵢ` (these attributes must be created using `register_tag_attr`).
+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`.
 
@@ -518,8 +518,8 @@ 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 tagged
-with the attributes `aᵢ` (these attributes must be created using `register_tag_attr`).
+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`).

Mathlib/Tactic/TagAttr.lean

@@ -151,22 +151,22 @@ end apply_assumption
 
 section «using»
 
-@[dummy_tag_attr] axiom foo : 1 = 2
+@[dummy_label_attr] axiom foo : 1 = 2
 
 example : 1 = 2 := by
   fail_if_success solve_by_elim
-  solve_by_elim using dummy_tag_attr
+  solve_by_elim using dummy_label_attr
 
 end «using»
 
 section issue1581
 
 axiom mySorry {α} : α
 
-@[dummy_tag_attr] theorem le_rfl [LE α] {b c : α} (_h : b = c) : b ≤ c := mySorry
+@[dummy_label_attr] theorem le_rfl [LE α] {b c : α} (_h : b = c) : b ≤ c := mySorry
 
 example : 5 ≤ 7 := by
-  apply_rules using dummy_tag_attr
+  apply_rules using dummy_label_attr
   guard_target = 5 = 7
   exact mySorry