feat: implementation of `@[use_set_notation]` by JovanGerb · Pull Request #37347 · leanprover-community/mathlib4

JovanGerb · 2026-03-29T23:28:17Z

This PR is the implementation part of #32983, without using the feature yet.

github-actions · 2026-03-29T23:29:21Z

PR summary e885514426

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

+ delabGe
+ delabGt
+ delabLe
+ delabLt
+ elabSsubsetStx'
+ elabSsupsetStx'
+ elabSubsetLike
+ elabSubsetStx'
+ elabSupsetStx'
+ useSetNotationFor

You can run this locally as follows

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

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

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

thorimur

This looks great! :) My comments here are mostly administrative or minor; the content of the metaprogramming looks solid. I've gone through carefully and ensured all names and syntax precedences line up, and everything checks out. :)

Also, could you please copy-paste most of the PR description from #32983 into this PR? I think it would be helpful to have it available in the git blame for this file.

thorimur · 2026-04-03T01:49:27Z

Mathlib/Tactic/SetNotation.lean

+
+/-- Delaborate `x ≤ y` into `x ⊆ y` if the type is tagged with `@[use_set_notation]`. -/
+@[app_delab LE.le]
+def delabLe : Delab := whenNotPPOption getPPExplicit <| whenPPOption getPPNotation do


We should probably namespace these under some appropriate SetNotation-related namespace, but see the file-level suggestion on naming.

thorimur · 2026-04-03T01:51:17Z

Mathlib/Tactic/SetNotation.lean

+  let x ← withNaryArg 2 delab
+  let y ← withNaryArg 3 delab
+  let stx ← `($x ⊆ $y)
+  annotateGoToDef stx `Mathlib.Meta.delabLe


(Here and below, to make this stable under refactors)

Suggested change

annotateGoToDef stx `Mathlib.Meta.delabLe

annotateGoToDef stx decl_name%

thorimur · 2026-04-03T01:53:01Z

Mathlib/Tactic/SetNotation.lean

+
+/-! ## Elaboration -/
+
+/-- This relation is an implementation detail of the `⊆` elatorator. -/


Typo:

Suggested change

/-- This relation is an implementation detail of the `⊆` elatorator. -/

/-- This relation is an implementation detail of the `⊆` elaborator. -/

thorimur · 2026-04-03T02:03:13Z

Mathlib/Tactic/SetNotation.lean

+/-- Elaborate a notation like `a ⊆ b` by elaborating `a` and `b`, and then deciding
+based on their type whether to return `a ⊆ b` or `a ≤ b`.
+Use `a ≤ b` whenever `useSetNotationFor` returns true for the type.
+If the type is not known, elaboration of this term is postponed. -/


Suggested change

If the type is not known, elaboration of this term is postponed. -/

If the type is not known, elaboration of this term is postponed.

We assume that `le` and `sub` are names for declarations of exactly the form

`decl.{u} {α : Type u} [Cls.{u} α] (a b : α) : Prop`, and that likewise `leCls` and `subCls` are

names for declarations of exactly the form `Cls.{u} (α : Type u) : Type u`. -/

thorimur · 2026-04-03T03:52:57Z

Mathlib/Tactic/SetNotation.lean

What do you think about calling this file SetlikeOrderNotation, and renaming the definitions in it accordingly? E.g. @[setlike_order_notation].

I know there are plans to expand this functionality; do they all have to do with using setlike notation for order-related operations, or do some have to do with {}, {|}, complementation, and ∈? That's the ambiguity in the phrase "set notation" I'm trying to eliminate here; SetNotation is by itself a bit broad!

That sound good to me, indeed it seems that all set notations involved are about order. (Note that for complements, we already use the same constant for sets and boolean algebras)

thorimur · 2026-04-03T19:56:23Z

Mathlib/Tactic/SetNotation.lean

+  if ← useSetNotationFor α then
+    let inst ← mkInstMVar <| .app (.const leCls f.constLevels!) α
+    return mkApp4 (.const le f.constLevels!) α inst x y
+  else
+    let inst ← mkInstMVar <| .app (.const subCls f.constLevels!) α
+    return mkApp4 (.const sub f.constLevels!) α inst x y


Note: I wonder if it's worth adding hover info to the subset token specifically to show which relation it wound up elaborating to. 🤔 However, command-clicking brings up the instances, so I think this is likely fine as-is, and my experiments in adding hover info to the token actually interfere with that command-clicking on the broader term. Let me know if you have thoughts here, though.

thorimur · 2026-04-03T19:56:46Z

Mathlib/Tactic/SetNotation.lean

+
+/-- Elaborator for `x ⊂ y` notation. -/
+@[term_elab ssubsetStx']
+def elabSsubsetStx' : TermElab


(Following HasSSubset)

Suggested change

def elabSsubsetStx' : TermElab

def elabSSubsetStx' : TermElab

thorimur · 2026-04-03T19:57:11Z

Mathlib/Tactic/SetNotation.lean

+
+/-- Elaborator for `x ⊃ y` notation. -/
+@[term_elab ssupsetStx']
+def elabSsupsetStx' : TermElab


(Following HasSSubset)

Suggested change

def elabSsupsetStx' : TermElab

def elabSSupsetStx' : TermElab

thorimur · 2026-04-03T20:13:31Z

MathlibTest/Delab/Subset.lean

Could you please

Move this file out of Delab, and name it analogously to the source file it's testing

Include tests for the elaborating/delaborating the other 3 relations? It's alright if they're minimal (or combined in a single statement!), I just want to make sure we test them since I anticipate they won't be used very much (and so it might not be obvious if they break).

thorimur · 2026-04-03T20:23:16Z

Mathlib/Tactic/SetNotation.lean

+
+/-- Whether to use set notation for the given type or not. -/
+def useSetNotationFor (type : Expr) : MetaM Bool := do
+  let .const n _ := (← whnfR type).getAppFn | return false


I think this is probably appropriate, especially given that we might use it after synthesizeSyntheticMVars* later on:

Suggested change

let .const n _ := (← whnfR type).getAppFn | return false

let .const n _ := (← whnfR <| ← instantiateMVars type).getAppFn | return false

thorimur · 2026-04-03T22:50:17Z

Here's a half-thought re: the simp_rw ... _ ≤ _ issue that comes up in the application PR. Currently if α contains a metavariable we just default to using Subset. Could we instead allow the class to be solved by unification in that case, somehow? (This might require some thought, and intuition says delayed-assigned mvars might be involved. This option might wind up being too fragile once explored, too, if it even works.)

JovanGerb · 2026-04-04T17:14:37Z

Note that these issues arise in simp_rw and not in rw. This is because simp_rw has to fully elaborate the term beforehand.

Another solution would be to default to LE.le when the type is a metavariable. I think it could work, but is not a very principled solution.

feat: implementation of @[use_set_notation]

b287a99

github-actions bot added the t-meta Tactics, attributes or user commands label Mar 29, 2026

JovanGerb mentioned this pull request Mar 29, 2026

feat: use LE.le for subset relation in Set, Finset, PSet, ZFSet #32983

Open

5 tasks

mathlib-triage bot assigned alexjbest and thorimur Mar 30, 2026

thorimur reviewed Apr 3, 2026

View reviewed changes

	annotateGoToDef stx `Mathlib.Meta.delabLe
	annotateGoToDef stx decl_name%


		/-! ## Elaboration -/

		/-- This relation is an implementation detail of the `⊆` elatorator. -/

-If the type is not known, elaboration of this term is postponed. -/
+If the type is not known, elaboration of this term is postponed.
+We assume that `le` and `sub` are names for declarations of exactly the form
+`decl.{u} {α : Type u} [Cls.{u} α] (a b : α) : Prop`, and that likewise `leCls` and `subCls` are
+names for declarations of exactly the form  `Cls.{u} (α : Type u) : Type u`. -/

	def elabSsubsetStx' : TermElab
	def elabSSubsetStx' : TermElab

	def elabSsupsetStx' : TermElab
	def elabSSupsetStx' : TermElab

	let .const n _ := (← whnfR type).getAppFn \| return false
	let .const n _ := (← whnfR <\| ← instantiateMVars type).getAppFn \| return false

Conversation

JovanGerb commented Mar 29, 2026

Uh oh!

github-actions bot commented Mar 29, 2026

PR summary e885514426

Import changes for modified files

Declarations diff

Uh oh!

thorimur left a comment • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

thorimur Apr 3, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

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!

thorimur Apr 3, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

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!

thorimur Apr 3, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

thorimur commented Apr 3, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

JovanGerb commented Apr 4, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

thorimur left a comment •

edited

Loading

thorimur Apr 3, 2026 •

edited

Loading

thorimur Apr 3, 2026 •

edited

Loading

thorimur Apr 3, 2026 •

edited

Loading

thorimur commented Apr 3, 2026 •

edited

Loading