feat(Tactic): `nonempty` attribute by robin-carlier · Pull Request #39782 · leanprover-community/mathlib4

robin-carlier · 2026-05-24T16:06:37Z

This PR adds a nonempty attribute. When tagging a definition of type α with [nonempty], an instance of type Nonempty α is automatically generated and registered using the definition.

Such an attribute is useful in the following scenario: certain structures are not classes (e.g., to avoid data-carrying classes potentially creating diamonds), but mere existence of terms of such structures allows to derive instances about the parameters of the structure. Using [nonempty] lets one auto-generate the instances derived instance (provided they correctly follow from [Nonempty _]).

Such is the case for the CategoryTheory.Functor.FullyFaithful structure, which allows to derive the Prop-classes CategoryTheory.Functor.Full and CategoryTheory.Functor.Faithful. Currently in mathlib, most definitions of type CategoryTheory.Functor.FullyFaithful are immediately followed by the corresponding Full and Faithful instances, adding "boilerplate" and increasing the surface for potential mistakes (like forgetting one or both of the instances.)

The attribute uses a variation of addRelatedDecl called addRelatedInstance, which handles automatic name generation and registration of instances from a given declaration and a "constructor" of type Expr → List Name → MetaM (Expr × List Name).

I believe abstracting addRelatedInst might have other possible usages: for instance, given an adjunction adj: L ⊣ R, it would be nice to have an attribute that one can tag on such adjunctions that automatically registers L.IsLeftAdjoint and R.IsRightAdjoint. The nonempty attribute here can’t really do this because R can’t be inferred from a goal of type L.IsLeftAdjoint, but the situation is quite similar, and addRelatedInst could also help writing this kind of attribute.

github-actions · 2026-05-24T16:07:56Z

PR summary 77283e5266

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.Tactic`	1

Declarations diff

+ Bar
+ Boz
+ Config
+ F
+ Faa
+ Foo
+ addRelatedInst
+ faaAux
+ faaAux'
+ foo
+ toNonempty
++++ instance {C D : Type*} [Category* C] [Category* D] (F : C ⥤ D) [Nonempty F.FullyFaithful] :

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

No changes to strong technical debt.

No changes to weak technical debt.

JovanGerb · 2026-06-04T20:45:34Z

+/-- The configuration options for the `nonempty` attribute. -/
+structure Config where
+  /-- If true, register the generated `Nonempty _` declaration as an instance. -/
+  inst : Bool := true


I also think that when using the attribute, we will always want to make this an instance. Otherwise I don't see the point of using @[nonempty].

JovanGerb · 2026-06-04T20:46:53Z

+/-- Given an expression assumed of type `α`, returns an expression for of type `Nonempty α`. -/
+def toNonempty (e : Expr) : MetaM Expr := do
+  mapForallTelescope
+    (fun e' => do
+      let e ← instantiateMVars e'
+      let e2 ← mkAppM ``Nonempty.intro #[e]
+      return e2) e


Can you just inline this function? The instantiateMVars is redundant, because there won't be any metavariables. So it is just mapForallTelescope (mkAppM ``Nonempty.intro #[·]) e

JovanGerb · 2026-06-04T20:48:03Z

+/-- This is an adaptation of `Lean.Elab.Util.mkUnusedBaseName` but
+doing everything in `MetaM` instead of `MacroM`.


You can run MacroM from MetaM right? So why copy the code?

I couldn’t get running MacroM in MetaM to work (liftMacroM wants a MonadMacroAdapter MetaM which isn’t there), which is why I had to copy things over like this.
Happy to change if you show me a nicer way to run MacroM inside MetaM (from what I understand, I’d have to build a Macro.Context by hand and run it with that, but there are a bunch of things in Macro.Context I’m not sure how to fill in).

I also didn't see a nice way to do this

JovanGerb · 2026-06-04T20:49:04Z

+  Warning: As a result, the original doc-string of `ref` will not be visible,
+  and go-to-def on `ref` will not go to the definition of `ref`.
+-/
+def addRelatedInst (src : Name) (ref : Syntax)


I think this should not be a separate function from addRelatedDecl. We should avoid code duplication when not necessary.

So you’d say instead nonempty should be the one responsible for name generation and would add the instance itself rather than registering it in in addRelatedInst? Auto-generating the name and adding the instance with the correct priority is the only extra logic here that had to make it separate from addRelatedDecl.

Maybe the name generation can be moved inside addRelatedDecl? (i.e., we turn the name parameter in addRelatedDecl to an Option and we add a prefix parameter that gets prefixed to the name and that will serve as the prefix for the name generation).

Indeed, could you simply add another argument (inst := false) to addRelatedDecl and have it deal with both cases?

It's indeed tricky right now to figure out how much is duplicated and what's new.

joneugster · 2026-07-12T17:04:08Z

+@[nonempty] def F : Foo := .unit
+
+/-- info: instNonemptyFoo : Nonempty Foo -/
+#guard_msgs in #check instNonemptyFoo


Suggested change

@[nonempty] def F : Foo := .unit

/-- info: instNonemptyFoo : Nonempty Foo -/

#guard_msgs in #check instNonemptyFoo

/--

error: failed to synthesize

Nonempty Foo

-/

#guard_msgs (substring := true) in #synth Nonempty Foo

@[nonempty] def F : Foo := .unit

I think the tests would make more sense if they check failure before adding the instance and not check the instance's autogenerated name

joneugster · 2026-07-12T17:21:39Z

+- `@[nonempty (name := foo)]` names the resulting instance `foo`.
+- `@[nonempty (priority := 123)]` gives the resulting instance a priority of `123`.
+- `@[nonempty -inst]` does not register the instance.


The implementation expects a strict ordering of arguments (priority, name, -inst) which isn't mentioned here; and even the list is in a different order.

You can achieve a better implementation by doing something like:

/-- The configuration options for the `nonempty` attribute. -/ structure Config where /-- If true, register the generated `Nonempty _` declaration as an instance. -/ inst : Bool := true priority: Nat := eval_prio default name : Option String := none

instead of defining some config-syntax manually.

joneugster · 2026-07-12T17:31:36Z

@@ -87,4 +87,86 @@ def addRelatedDecl (src tgt : Name) (ref : Syntax)
    if hoverInfo then
      Term.addTermInfo' ref (← mkConstWithLevelParams tgt) (isBinder := true)

+/-- This is an adaptation of `Lean.Elab.Util.mkUnusedBaseName` but


Suggested change

/-- This is an adaptation of `Lean.Elab.Util.mkUnusedBaseName` but

/-- This is an adaptation of `Lean.Elab.mkUnusedBaseName` but

joneugster · 2026-07-12T17:43:10Z

+  Warning: As a result, the original doc-string of `ref` will not be visible,
+  and go-to-def on `ref` will not go to the definition of `ref`.
+-/
+def addRelatedInst (src : Name) (ref : Syntax)


Indeed, could you simply add another argument (inst := false) to addRelatedDecl and have it deal with both cases?

It's indeed tricky right now to figure out how much is duplicated and what's new.

robin-carlier added 2 commits May 24, 2026 14:25

WIP

752555a

WIP

321d69f

robin-carlier added the t-meta Tactics, attributes or user commands label May 24, 2026

robin-carlier added 2 commits May 25, 2026 21:29

fix: lake exe mk_all

ed013a8

feat: document the attribute

77283e5

robin-carlier added the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label May 25, 2026

robin-carlier marked this pull request as ready for review May 25, 2026 20:13

github-actions Bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label May 25, 2026

mathlib-triage Bot assigned dwrensha May 26, 2026

JovanGerb reviewed Jun 4, 2026

View reviewed changes

mathlib-triage Bot assigned thorimur Jun 8, 2026

mathlib-triage Bot unassigned dwrensha and thorimur Jun 17, 2026

mathlib-triage Bot assigned JovanGerb Jun 26, 2026

joneugster reviewed Jul 12, 2026

View reviewed changes

joneugster self-assigned this Jul 12, 2026

joneugster added the awaiting-author A reviewer has asked the author a question or requested changes. label Jul 12, 2026

		/-- This is an adaptation of `Lean.Elab.Util.mkUnusedBaseName` but
		doing everything in `MetaM` instead of `MacroM`.

Uh oh!

Conversation

robin-carlier commented May 24, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions Bot commented May 24, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 77283e5266

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

robin-carlier commented May 24, 2026 •

edited

Loading

github-actions Bot commented May 24, 2026 •

edited

Loading