feat: implementation of @[use_set_notation]

[JovanGerb]

This PR allows the use of ⊆ notation while the underlying constant is ≤.
Similarly for ⊂/<, ⊇/≥ and ⊃/>.

• The idea is to later extend this feature to other set notation constants, such as union/intersection.
• There are some types for which we cannot use LE.le as the underlying constant, such as List and Multiset. So, the elaborator for the ⊆ notation needs to make a decision which underlying constant to elaborate to, depending on the type. Sometimes the type is not known yet, which makes things awkward. Most of these cases are solved by delaying the elaboration until later when the type is known.
• However, in some cases this doesn't work either, such as simp_rw [and_comm (_ ⊆ _)], where it is impossible to tell the type when elaborating the term. So, some such cases need to be fixed by making it simp_rw [and_comm (_ ≤ _)]. This is because simp_rw, unlike rw, fully elaborates the rewrite rules before using them. So, when we get the new rewrite tactic, this problem will mostly go away.

See also https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/Any.20infimum.20based.20version.20of.20.60OmegaCompletePartialOrder.60.3F/near/579333629

---

[github-actions]

PR summary 6bc2280e53

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]

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

Suggested change

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

[JovanGerb]

Another question is whether we actually want the go-to-def to go to the delaborator. But I imagined that it is best to avoid ambiguity.= like this.

[thorimur]

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!

[JovanGerb]

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)

[JovanGerb]

Thinking about this more, I'm not sure whether I like the rename to e.g. @[setlike_order_notation]. It is true that all examples I'm thinking of are for order notations. But there is nothing inherently about orders with this attribute. The attribute is just to mark a type as set-like, and then anyone implementing a new notation could use this to make their notation different for set-like types.

[thorimur]

anyone implementing a new notation could use this to make their notation different for set-like types

Hmm, that assumes that that notation would be the only possible interpretation for the piece of set notation it decides to overwrite for setlike types, though. And conversely, any type tagged with @[use_set_notation] would be using all of the interpretation choices for set notation by any notation-consumer of @[use_set_notation], e.g. they'd always bidirectionally interpret ⊆ as ≤, and so on for any new notation.

So I guess the question is: will all setlike types want to make the same choices? (Maybe! This is not a rhetorical question :) But probably requires coordination with people.)

[JovanGerb]

This is all quite hypothetical. But yes, the way I think about it is that we use a different notation because the type is like a set. So the use_set_notation attribute would decide whether to use various different notations.

[thorimur]

Hmm, okay. I suspect that there may be types that want to interpret set notation not as order notation, or want to use the future non-order interpretations you're talking about without using the order interpretations...but this is not a case in favor of @[use_set_notation], since @[use_set_notation] would demand we uniformly interpret certain set operations as order operations.

I think we only earn the generic, non-order-related name if either

• we may eventually allow set notation "classes", e.g. @[use_set_notation order] for alternate interpretations of set notation and finer-grained buy-in
• or, we expect every type tagged with @[use_set_notation] to also be able to uniformly support non-order interpretations of other set notation, even while @[use_set_notation] insists on order-based interpretations of ⊆ etc.

Otherwise, we do wind up remaining tied to order relations/operations.

[thorimur]

But to be clear, while I think we should figure this out (the naming is the shadow of a larger design question), I'm not going to hold up this PR over the naming itself, which in this case would be easy to change later on :)

[thorimur]

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.

[JovanGerb]

Hmm, I think that would be nice, but I don't know how to do it. Currently it just shows the doc-string

Subset relation: a ⊆ b.

For types tagged with @[use_set_notation], this elaborates to a ≤ b.

[thorimur]

My experiments were somewhere in the space of passing along the tk and using an appropriate addTermInfo' and/or running mkInstMVar under a withRef tk (seeing as it registers the metavariable to the current ref), but these were fragile for various reasons. :/

But I have another idea... :) It's probably worth a small separate PR, though. Instead of attaching it directly to the token, we call addTermInfo' on the entire ref with isDisplayableTerm := true, attach mdata to the expression fed to addTermInfo' (not in the returned expression), and create a delaborator for that mdata which sets pp.notation to false at the current position (easier than I initially thought; this does not affect subexpressions). Then for a term like

[1, 2, 3] ⊆ b

we end up with a hover that looks like:

[thorimur]

Oh, hang on. There's built-in support for this! :) It doesn't need to be another PR. Consider using e.g.

    let e := mkApp4 (.const le f.constLevels!) α inst x y
    addTermInfo' (← getRef) (isDisplayableTerm := true) <|
      e.setOption `pp.notation false
    return e

Thankfully this turns off notation at the position of delaborating e, but not its arguments/subexpresssions. There's also e.g. e.setPPExplicit true if we want to show the implicit arguments, too, which could be useful. What do you think?

(It might make sense to deduplicate between the two branches of useSetNotationFor at this point.)

[JovanGerb]

If I understand correctly, a typical hover in the source code only shows the type. You want to also show the value, and in particular show the value with notation turned off, so that we can see either Subset or LE.le?

[thorimur]

Correct. :) (The addTermInfo' + e.setOption snippet above produces the hover shown in the screenshot.)

Some justification:

• Simply showing Prop is not very helpful when elaboration may have made nontrivial decisions for us.
• The influence is important enough to allude to in the docstring, so we may as well not leave the user to figure it out themselves.
• The current mechanism effectively only turns off notation at the head, so the expressions should not be extremely long.
• We do sometimes show the value of terms in hover, not just the type, when appropriate; however, the only heuristic available in full generality is when the value is small (a constant or pretty-printed to something atomic). (The comment nearby in lean4 source says simply “Try not to show too scary internals” :) ) Adding extra information in a custom manner is what the isDisplayableTerm flag is for; grind does this in certain cases to show terms on anchors, for example. I think we should add this sort of hover information on notation more often as long as we can keep the length under control. :)
• Attaching hover information to the token ⊆ specifically was impractical in my experiments: it destroyed the syntax docstring and interfered with command/ctrl-clicking. In any case, such an approach would also make it more finicky to position the cursor and view the useful information.

[JovanGerb]

The disadvantage of showing the whole term without notation is that hovering over something like (a ∪ a) ⊆ (b ∩ b) will show you LE.le (Union.union a a) (Inter.inter b b) : Prop.

How about we instead show only the relation itself, without the arguments? In this case that would give LE.le : Set Nat → Set Nat → Prop.

[JovanGerb]

Another option would be to simply add the information of just the constant, so that would be LE.le.{u} {α : Type u} [self : LE α] : α → α → Prop. But I would think that is less useful.

[thorimur]

The disadvantage of showing the whole term without notation is that hovering over something like (a ∪ a) ⊆ (b ∩ b) will show you LE.le (Union.union a a) (Inter.inter b b) : Prop.

No, luckily, it won't! :) This is the point I'm trying to make by saying it effectively only affects the head, not the whole term, and the length is under control. Look at the screenshot; notation is still active for [1,2,3,4], unlike if we had set pp.notation false ambiently (which would show List.cons etc.).

Here it is in action for an example similar to the above:

It turns out that when you use e.setOption to set an option on an expression for the delaborator, it sets it only at the position of the wrapped expression, and not for its subexpressions.

(Looks like we could just modify the options ambiently before adding the term info if for some reason we did want it to affect the whole expression; that seems to be how term mode set_option ... in works. But the mdata-based e.setOption only affects the optionsPerPos.)

[thorimur]

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]

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.