# Zulip Chat Archive

## Stream: maths

### Topic: alternate definitions

#### Damiano Testa (Sep 01 2020 at 08:17):

Dear @Kevin Buzzard , thank you for taking the time to explain the issue! I agree that not having definitional equivalence between the usual TFAE items is not important. I guess that my point of view is that of a beginning user of Lean who has trouble converting between the various definitions and is often stuck with the implemented one, since I am not able to "jump" to another one.

Maybe in a few days/weeks time, this will not be an issue for me, but one feature that I would like to have in Lean is the possibility of somehow displaying all these non-definitionally equivalent definitions and being able to choose whichever one I prefer at whichever moment I want. I realize, as I am writing this, that likely this is already there, for the more advanced users. I still struggle with this.

In the specific case of the definition of the rational numbers, for instance, I suspect that it might be hard for me to convince Lean that `2/2`

is a rational number. Especially in the case in which such a "rational number" arises as the slope of some vector bundle. (As I have never actually played with rational numbers in Lean, I am not sure that this would really be an issue, but I hope that I have conveyed my idea, rather than the specific example!)

#### Kevin Buzzard (Sep 01 2020 at 08:21):

You are wrong that it is hard to convince Lean that 2/2 is a rational number, and this is an important thing to learn. [more to come]

#### Kevin Buzzard (Sep 01 2020 at 08:24):

The *definition* of a rational number is a coprime pair (n,d) with d>0. So the "canonical" constructor of a rational number is something which is very difficult to use. However, the authors of data.rat.basic also wrote other constructors for rational numbers, including `rat.mk n d`

which just takes two integers n and d and produces the rational number n/d, regardless of whether n and d are coprime etc.

#### Kevin Buzzard (Sep 01 2020 at 08:28):

The same is true for eliminators. The definition of `int`

is "either n, or -1-n, for n a natural". This means that if you have an integer z and you want prove something about it and you know that you want to use induction, if you type `induction z`

you'll get something horrible: you'll have to prove it for all integers of the form `of_nat n`

and all integers of the form `neg_one_of_nat n`

or whatever the constructor is called (I don't even know). I've seen students do this and it's a disaster because now you need to know the API for `of_nat`

and for the other constructor whose name I've forgotten, and this is really only something which the developers of `int`

need to know about. But again the developers have done their job -- you can apply `int.induction_on`

, a custom induction principle designed for end users, and then all of a sudden you have to check P(0), to check P(z) implies P(z+1) for z>=0, and to check P(z) implies P(z-1) for z<=0. This is the induction principle which a mathematician wants. Because the definition of int/rat are "exotic", the inbuilt constructors/eliminators are bad for mathematicians. However the trick is to make better ones and encourage mathematicians to use them instead.

#### Damiano Testa (Sep 01 2020 at 08:33):

Ok, maybe I just need to get over the fact that instead of learning different, equivalent definitions of a mathematical object, I will need to learn many different names of computer functions that represent the same mathematical concept. I still find it hard, in general, to navigate and even find/know that these equivalents exist. For instance, I learned that the submodule spanned by a set is, in Lean, the smallest submodule containing the set (a definition that I like, by the way!). Yet, it was then hard for me to obtain that an element in the span of a singleton was a multiple of the generator. After I have seen how to do it, I realize that it is not difficult, but I did spend quite a bit of time trying, before I finally gave up and asked!

I would like to be able to feel more independent and not to have to ask questions whose answers, often, are "ooh, `refl`

clearly does not work, but `exact id`

does!

Your last sentence I think is key:

"However the trick is to make better ones and encourage mathematicians to use them instead."

I would *really* like to use the better ones, but usually I am in the situation where:

- I have trouble finding out what the implemented definition is;
- I manage to find it and get stuck;
- I have no idea where to look for an alternative definition;
- I struggle to understand how to use this alternative definition.

Normally, I hover between items 1 and 2. I would like to at least reach 3 or 4 more reliably!

#### Damiano Testa (Sep 01 2020 at 08:34):

(Since tones are difficult to convey in text, I want to stress that I am finding this conversation highly enlightening and I am actually learning and having fun chatting about this!)

#### Johan Commelin (Sep 01 2020 at 08:38):

Aside: Let's move this to a different thread. @Rob Lewis Could you please cut it about 6 posts up? (The first post by Kevin today is still relevant. Maybe it can be duplicated?) Thanks!

#### Johan Commelin (Sep 01 2020 at 08:40):

@Damiano Testa To find out a definition, use `Ctrl-click`

.

#### Johan Commelin (Sep 01 2020 at 08:40):

To find alternate defintions... I think we should get a better system for that.

#### Johan Commelin (Sep 01 2020 at 08:40):

But one thing that helps is autocomplete. It is a very powerful tool.

#### Damiano Testa (Sep 01 2020 at 08:41):

Johan Commelin said:

Damiano Testa To find out a definition, use

`Ctrl-click`

.

Thank you! It is possible that I was told this already, but I was surprised by this again!

#### Johan Commelin (Sep 01 2020 at 08:41):

And the rigid naming scheme that Lean follows. It took me a while to get the hang of it, but it's really good.

#### Damiano Testa (Sep 01 2020 at 08:41):

Johan Commelin said:

But one thing that helps is autocomplete. It is a very powerful tool.

I use it, but I know that I am still in my infancy of using this!

#### Mario Carneiro (Sep 01 2020 at 08:42):

I don't see two topics in this thread

#### Damiano Testa (Sep 01 2020 at 08:42):

Johan Commelin said:

And the rigid naming scheme that Lean follows. It took me a while to get the hang of it, but it's really good.

Yes, Kevin suggested reading the naming convention and that helped a lot.

#### Johan Commelin (Sep 01 2020 at 08:42):

You have `x \in ideal.span {y}`

, and you want to do *something* with it. Well, that says something about "`x`

being a *mem* of the `span`

of a `singleton`

", so we just try `mem_span_singleton`

and see if it exists. If it exists, it will probably be (almost) what you want.

#### Johan Commelin (Sep 01 2020 at 08:43):

Even if I have no idea what `finset.bind`

is, if I see `x \in finset.bind s foobar`

, I just `rw finset.mem_bind`

. Because someone wrote a decent API, this lemma exists, and it turns my goal into something that is comprehensible again.

#### Johan Commelin (Sep 01 2020 at 08:43):

Mario Carneiro said:

I don't see two topics in this thread

Rob already split it.

#### Damiano Testa (Sep 01 2020 at 08:44):

Johan Commelin said:

You have

`x \in ideal.span {y}`

, and you want to dosomethingwith it. Well, that says something about "`x`

being amemof the`span`

of a`singleton`

", so we just try`mem_span_singleton`

and see if it exists. If it exists, it will probably be (almost) what you want.

Thank you for spelling out these implications: they really help me!

#### Patrick Massot (Sep 01 2020 at 08:46):

Damiano, one thing you can do is add your voice to https://leanprover.zulipchat.com/#narrow/stream/239415-metaprogramming-.2F.20tactics/topic/reformulate hoping some tactic writer will pity us.

#### Damiano Testa (Sep 01 2020 at 08:46):

Johan Commelin said:

Even if I have no idea what

`finset.bind`

is, if I see`x \in finset.bind s foobar`

, I just`rw finset.mem_bind`

. Because someone wrote a decent API, this lemma exists, and it turns my goal into something that is comprehensible again.

While the previous example I understood, this one is still out of reach. I will file this as "when dealing with sets, insert `mem`

and see how it autocompletes!

#### Mario Carneiro (Sep 01 2020 at 08:46):

also, it is not uncommon for those lemmas to be marked `simp`

, so one approach is to try `simp`

and see if it makes progress (and if it does make progress and you want to see how, use `squeeze_simp`

instead to see what lemma it applied, and then use ctrl-click to go to the lemma and look around there for other interesting things)

#### Damiano Testa (Sep 01 2020 at 08:48):

Mario Carneiro said:

also, it is not uncommon for those lemmas to be marked

`simp`

, so one approach is to try`simp`

and see if it makes progress (and if it does make progress and you want to see how, use`squeeze_simp`

instead to see what lemma it applied, and then use ctrl-click to go to the lemma and look around there for other interesting things)

Ok, thanks for the suggestion. I view `simp`

as a huge wave that washes over everything and, if I am lucky, I can take one further step after it washes away. Although often I undo it...

#### Mario Carneiro (Sep 01 2020 at 08:48):

Yes, it is quite often not the actual step you want to do, or it does too much, but it gives a lot of hints as it works

#### Damiano Testa (Sep 01 2020 at 08:49):

Patrick Massot said:

Damiano, one thing you can do is add your voice to https://leanprover.zulipchat.com/#narrow/stream/239415-metaprogramming-.2F.20tactics/topic/reformulate hoping some tactic writer will pity us.

Thank you: I have subscribed!

#### Patrick Massot (Sep 01 2020 at 08:49):

You can use `squeeze_simp`

and then remove stuff from the list if you want.

#### Mario Carneiro (Sep 01 2020 at 08:50):

Roughly speaking, all sets are "defined" by their membership predicate. So if you see `foo A \union bar A = univ`

and you don't know what a `foo`

is, try `ext x`

to turn it into a membership question, `x \in foo A \union bar A <->x \in univ`

, and then there will be a ton of simp lemmas that will trigger on seeing `x \in <some set>`

because that's how the simp lemmas are expressed

#### Mario Carneiro (Sep 01 2020 at 08:51):

it will usually turn the statement into some first order logic thing that you can destructure using `use`

, `cases`

, `intro`

and other such basic tactics

#### Damiano Testa (Sep 01 2020 at 08:51):

These are all great suggestions: thank you all!

I do feel like the people for whom the FAQ "have you connected your computer to the plug?" actually solves the problem...

#### Johan Commelin (Sep 01 2020 at 08:53):

@Damiano Testa You should have watched my first weeks in this chatroom...

Last updated: May 11 2021 at 00:31 UTC