alternate definitions

Stream: maths

[Damiano Testa]

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]

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]

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]

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]

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:

1. I have trouble finding out what the implemented definition is;
2. I manage to find it and get stuck;
3. I have no idea where to look for an alternative definition;
4. 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]

(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]

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]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Damiano Testa]

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]

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]

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]

I don't see two topics in this thread

[Damiano Testa]

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]

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]

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]

Mario Carneiro said:

I don't see two topics in this thread

Rob already split it.

[Damiano Testa]

Johan Commelin said:

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.

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

[Patrick Massot]

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]

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]

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]

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]

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]

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]

You can use squeeze_simp and then remove stuff from the list if you want.

[Mario Carneiro]

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]

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]

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]

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