How to determine the intended API of an object

Stream: new members

[Luna]

I've been picking up MIL again and I've been attempting the following problem in Section 9 on groups:

example (φ : G →* H) (S T : Subgroup H) (hST : S ≤ T) : comap φ S ≤ comap φ T := by
  sorry

This took me hours because I was trying to figure out how to properly interact with the ≤ operator. At first I looked at just using theorems in lattices thinking that I could show that if comap φ · behaves monotonically, then this should be trivial. But I wasn't able to get anything to work on that end and gave up here.

Then I played around a while trying to get S and T to be sets and this also didn't work! Finally after a long time of looking I found the theorem SetLike.le_def and then used this to create the following (very simple) proof:

example (φ : G →* H) (S T : Subgroup H) (hST : S ≤ T) : comap φ S ≤ comap φ T := by
    rw [SetLike.le_def]
    rw [SetLike.le_def] at hST
    simp
    intro g phi_g_in_S
    exact hST phi_g_in_S

After this I looked in the solutions page to see if there was something easy and I saw this:

example (φ : G →* H) (S T : Subgroup H) (hST : S ≤ T) : comap φ S ≤ comap φ T := by
  intro x hx
  rw [mem_comap] at * -- Lean does not need this line
  exact hST hx

But this solution is very confusing to me because how am I supposed to know upfront that under the hood the objects are defined like x → hx → ...?

[Kenny Lau]

@Luna if you're not in the context of MIL, then the correct thing to do would be to ask loogle, for example this statement is about Subgroup.comap, and is about "mono", so I put Subgroup.comap, "mono" to Loogle and the first result is what you need

if you are in the context of proving this by yourself, then the first thing you would want to do would be do right click on comap and click "see definition", which will bring you to the definitions "under the hood".

trying to see the definition of LE is less trivial, but there is still a way to do it using #synth:

import Mathlib

variable (G : Type*) [Group G]
#synth LE (Subgroup G)

note that the result is CompleteLattice.toCompletePartialOrder.toLE which tells you how the LE is defined, and most importantly the result is clickable, so you can click to trace the definitions

[Kevin Buzzard]

If you don't know the implementation then rw [mem_comap] at least gives you what your mental model of the definition is (I should think)

[Ruben Van de Velde]

So in theory the right answer is rewriting with SetLike.le_def as you did. In practice many people will assume that le_def is indeed the definition of \le, and will use tactics like intro that see through the definition.

[Ruben Van de Velde]

And because the definition in this case is so simple and unlikely to change, there's not much appetite for pushing towards using the API

[Luna]

@Kenny Lau I did something similar to that and came across CompleteLattice.toCompletePartialOrder.toLE but clicking "go to definition" just brings me to the definition of PartialOrder. I tried going through the stack a bit more but I couldn't find the origins of the definition of ≤ for subgroups.

And @Kevin Buzzard I saw that at first but it never came to mind to use it since the theorem doesn't contain ≤

After the fact, I finally found the definition of the instance of CompleteLattice for subgroups.

So I guess my question is, is there a way to go from A ≤ B to "definition of ≤ for the type of A?

[Ruben Van de Velde]

Luna said:

So I guess my question is, is there a way to go from A ≤ B to "definition of ≤ for the type of A?

If you find one, let me know :)

[Ruben Van de Velde]

You can probably get there by clicking the right instances in the infoview, but it's not the most obvious

[Ruben Van de Velde]

If you click on the CompleteLattice.toCompletePartialOrder part of CompleteLattice.toCompletePartialOrder.toLE, you get a popup that shows

@CompleteLattice.toCompletePartialOrder (Subgroup H) instCompleteLattice : CompletePartialOrder (Subgroup H)

and in vs code, you can control-click the instCompleteLattice part of that and you might end up in a good place

[Ruben Van de Velde]

https://github.com/leanprover-community/mathlib4/blob/e68729735c6afe9a085958187facee5f6782e312/Mathlib/Algebra/Group/Subgroup/Lattice.lean#L239-L251

[Ruben Van de Velde]

Yeah, that doesn't help either, sadly

[Kenny Lau]

Ruben Van de Velde said:

If you click on the CompleteLattice.toCompletePartialOrder part of CompleteLattice.toCompletePartialOrder.toLE, you get a popup that shows

@CompleteLattice.toCompletePartialOrder (Subgroup H) instCompleteLattice : CompletePartialOrder (Subgroup H)

and in vs code, you can control-click the instCompleteLattice part of that and you might end up in a good place

it is actually the right path, but the next steps are more non-trivial:

1. do #print Subgroup.instCompleteLattice, and run around in the infoview, until you understand the logic that it comes from let __src := completeLatticeOfInf (Subgroup G) ⋯
2. click on completeLatticeOfInf to see @completeLatticeOfInf (Subgroup G) SetLike.instPartialOrder Subgroup.instInfSet ⋯ : CompleteLattice (Subgroup G), understand the logic and realise that it comes from SetLike.instPartialOrder
3. now do #print SetLike.instPartialOrder, and see le := fun H K => ∀ ⦃x : B⦄, x ∈ H → x ∈ K in the output, and this is the info requested

[Kenny Lau]

which, i admit is very convoluted and may not be that well suited to a beginner

[Kenny Lau]

it's a bit hard to make this better, because if we just request an algorithm to "unfold all the definitions", then you'll end up unfolding the mem as well... maybe we can request the macro to accept a natural number as input to tell it the number of steps to unfold

[Ruben Van de Velde]

So @Luna please don't be discouraged that you found this hard - it is :)

[Kenny Lau]

I've brought this up in #lean4 > feature request: unfold n steps of definition

[Kenny Lau]

I suppose the algorithm would be at each step to get the head of the expression and then unfold it, and if it fails (e.g. structural projection) then get the next head, etc.

[Kenny Lau]

I can try to write something later (not today) if nobody beats me to it

[Luna]

Thank you all for looking into this! So my understanding is that the best current solution for MIL excersizes is to keep recursively looking into all the instances to try find the concrete definition, and for Mathlib to use a search engine.

The unfold approach sounds interesting and like an automated version of the above. I'd imagine that in theory one should be able to recursively unfold the function (· ≤ · : Subgroup _ → Subgroup _ → Prop) until you reach Lean primitives and then rewind until you get to the desired level.

A confusing aspect I guess is that because class instances can be chained together, its not easy to find the "original" definition. Is there an easy way to filter out instances that are generated "on-the-fly" and keep only the instances that are "user-defined"?

[Luna]

Also when in VS-code, is there an easier way to find how each instance is created other than hover over it in the info-view, and then hover over the term in the pop up window, and continuing that for arbitrarily long? It becomes very difficult to read and sometimes clicking "Go-to definition" doesn't work because moving my mouse makes the window disappear. E.g. below

image.png