(s ⊆ t) = ∀ x ∈ s, x ∈ t -- discoverable for new users?

Stream: new members

[Isak Colboubrani]

Consider the following:

example (α : Type) (s : Set α) : s ⊆ s := by sorry

From first principles, the proof can be done succinctly with intro x hx and then assumption.

This relies on knowing that s ⊆ t is defined as ∀ x ∈ s, x ∈ t, which is clear after reading Set.subset_def.

However, a new user might not immediately know the name Set.subset_def.

For someone new to Mathlib encountering this example for the first time, what is the recommended way within VS Code to discover that s ⊆ t unfolds to ∀ x ∈ s, x ∈ t—and consequently that intro x hx is the appropriate approach?

[Jireh Loreaux]

Well, I would have said:
@loogle |- ((?s : Set ?α) ⊆ ?t) ↔ ?_

[loogle]

:search: Set.subset_kernImage_iff, Set.univ_subset_iff, and 220 more

[Jireh Loreaux]

But this gives garbage because docs#Set.subset_def uses an equality, and not an ↔ (would you mind changing this in Mathlib?). So the user would need to do this:
@loogle |- ((?s : Set ?α) ⊆ ?t) = ?_

[loogle]

:search: Set.subset_def

[Jireh Loreaux]

However, another good option is rw?, which gives this as the first hit.

[Jireh Loreaux]

hint also closes the goal in a way that tells you a bit about what's going on.

[Kyle Miller]

There's been talk about somehow getting notations to show type-specific documentation on hover. The Set one could say what the definition is and that you're meant to take advantage of it.

[Isak Colboubrani]

@Kyle Miller The hover-based approach appears very promising for enhancing discoverability. Is it enough to simply add documentation to the existing code in the sense that I can do it via a PR, or will additional infrastructure be required?

The current workflow places quite a few demands on the user:

1. They need to realize they should look up the definition of a subset.
2. They must understand that there is no straightforward built-in method to access that definition.
3. They must know about an external search engine that can provide the definition.
4. They need to be familiar with the search engine’s syntax.
5. They must be able to match their current goal to the right query.
6. They must be able to write |- ((?s : Set ?α) ⊆ ?t) ↔ ?_ or |- ((?s : Set ?α) ⊆ ?t) = ?_ without typos.

I suspect the subset of new users who can manage all these steps is only slightly larger than $\emptyset$.

[Kyle Miller]

It will need additional infrastructure

[Kyle Miller]

There's another workflow by the way that you can do completely from within VS Code. I've haven't used the one you're describing, and it seems hard to carry out (as you say!)

I won't say it's obvious, but let's say you have s ⊆ t in the infoview. First, hover over it:

image.png

Second, realize that this is a generic notation, so move your mouse over the instance argument and (on a mac) command-click it to go to definition:

image.png

Third, pause and wonder why the definition is in terms of LE, but notice that it's defined right above:

image.png

Go to Set.Subset, and see how it's defined:

image.png

[Kevin Buzzard]

This argument assumes that the user is trying to work out everything by themselves rather than following a tutorial where this is all explained to them

[Philippe Duchon]

Jireh Loreaux said:

But this gives garbage because docs#Set.subset_def uses an equality, and not an ↔ (would you mind changing this in Mathlib?). So the user would need to do this:
loogle |- ((?s : Set ?α) ⊆ ?t) = ?_

Is there some special syntax to using loogle from within VS code? I installed the loogle extension, and some searches go through correctly, but it seems that, when the query includes the turnstile |-, loogle doesn't understand me.

When I copy and paste Jireh's example above, I get an error in VS code, but it works fine on the loogle webpage. Hovering seems to indicate my | is seen as the opening for an absolute value, so I tried looking for a similar-looking-but-different Unicode character, but I'm not sure where to look (at least, I failed).

[Kevin Buzzard]

#mwe :

import Mathlib.Algebra.Order.Group.Unbundled.Abs
import LeanSearchClient

#loogle |- ((?s : Set ?α) ⊆ ?t) = ?_ -- expected no space before

[Isak Colboubrani]

Kevin Buzzard said:

This argument assumes that the user is trying to work out everything by themselves rather than following a tutorial where this is all explained to them

In my experience, new users typically blend "explicit learning" and "implicit learning".

There are many excellent tutorials available, which are great for explicit learning—such as reading manuals or following step-by-step guides.

However, new users often complement this explicit approach with implicit (or intuitive) learning, figuring things out by directly interacting with the interface (hovering, clicking, etc.). There seems to be room for improvement in discoverability (how easily users can learn how something works without external guidance) in this case. Once the necessary "hover infrastructure" Kyle mentioned is in place, I’d be happy to contribute by adding documentation!

[Kevin Buzzard]

Looking back, I think I did a mixture of explicit learning (i.e. reading #tpil) and implicit-learning-which-constantly-ran-into-roadblocks-so-I-would-ask-here. I think that my personality lent itself very well to this approach because I was not scared to constantly ask basic questions and look foolish, and Mario was constantly happy to answer them (this was back when this Zulip had 20 users not 10000). I agree that this approach does not work for everyone.

[Jireh Loreaux]

@Philippe Duchon in VS Code it works if you use the unicode turnstile:

import Mathlib.Algebra.Order.Group.Unbundled.Abs
import LeanSearchClient

#loogle ⊢ ((?s : Set ?α) ⊆ ?t) = ?_

(although this doesn't work in the web editor because it doesn't have network access)

[Philippe Duchon]

Thanks! I did not know how to type the unicode turnstile (\|-and others), and the symbol rarely appears in a position where I can just get the information from VS code.

[Aaron Liu]

For loogle and a lot of other things |- works too

[Philippe Duchon]

From VS code, |- generates an error ("expected no space before", reporting the error in the next line, so this looks like a parsing problem). This was what I tried first :)

[suhr]

This argument assumes that the user is trying to work out everything by themselves rather than following a tutorial where this is all explained to them

Why yes, that's exactly how I approach learning things. How could you tell?

[suhr]

Unfolding definitions is not a bad way to figure out how things work. That's what #print is for.

[Kevin Buzzard]

I think that in some parts of mathlib, unfolding definitions is a terrible idea, and reading the API around a definition is the sensible thing to do. I think your advice is true sometimes but definitely not true always.

[suhr]

That depends on how many layers of definitions are there. Navigable documentation could be much more helpful, of course, but it's often missing (for example, Set.instHasSubset is not documented).

[Philippe Duchon]

How I understand Kevin's meaning is that, sometimes in Mathlib, the definition is not easy to understand - perhaps the definition is more general than you'd think, or it uses a different formulation for some other reason. So when the definition by itself does not "tell" you much, you should have a look at the various theorems in the library (the "API"), which may be more informative of how things work than just "what they are".

(The reason for such implementation choices are not always clear; I find that the headers of individual files sometimes give a little information.)

[Jireh Loreaux]

A good example of something which is probably surprising to new users is the definition of docs#Commute, which is in terms of docs#SemiconjBy

[Jireh Loreaux]

It's not that hard to understand when you look at the definition, but it's sure surpising when someone is expecting to see directly a * b = b * a.

[Kevin Buzzard]

Another example is docs#IsCompact .