Zulip Chat Archive

Stream: new members

Topic: VSCode - show more suggestions

Trevor Fancher (Sep 10 2021 at 19:21):

When in tactic mode and I type convert mul_lt my VSCode automatically suggests many good options, but also misses many. For example mul_lt_mul and mul_lt_mul' show up, but not the double and triple prime options. Many times I have missed important lemmas because of this. Now, if I go ahead and type convert mul_lt_mul then hit ctrl+space I do get all the options. So I believe either VSCode or the Lean extension is pruning suggestions falling under a common prefix, which probably makes sense most the time. But sometimes I want to tell VSCode to just show all the damn matches and to let me deal with it. I've dug through VSCode settings and googled around for help on how to do this with VSCode generally, but I'm stuck. Any help is appreciated.

Kevin Buzzard (Sep 10 2021 at 19:44):

I get the double and triple primed options, but perhaps I have less imported than you. I think it cuts off after 100 suggestions?

Trevor Fancher (Sep 10 2021 at 19:59):

I'm working through your Formalising Maths workshop exercises, so I don't think I have any weird imports (only data.real.basis and tactic in the file week_3/Part_A_limits.lean). I've attached a screen shot of what happens when I type convert mul_lt (no ctrl+space, just auto suggestions). tmp.png

Kevin Buzzard (Sep 10 2021 at 20:01):

Try hitting Esc and then ctrl-space again. Do you get far far more?

Trevor Fancher (Sep 10 2021 at 20:02):

I was a little frustrated after I finished my proof and then looked at your nice use of convert mul_lt_mul'' ... I thought, "How did I miss that one" and after I figured out how I missed it I came here to start this thread.

Trevor Fancher (Sep 10 2021 at 20:04):

Yes. I do get all (or, at least, more) suggestions then. But I'd prefer to not always have to do that. Do I now always just have to Esc then ctrl-space when I think there might be more suggestions. Not a huge deal, but, in my (newbie) opinion, its a bit of a pain point for exploration.

Trevor Fancher (Sep 10 2021 at 20:05):

I was hoping there was either a Lean extension (or a general VSCode) option to just show everything.

Kevin Buzzard (Sep 10 2021 at 20:06):

When I was writing proofs I would typically just write something which was comprehensible to, but perhaps not findable by, the student. I guess my personal thought process was: "there is bound to be a lemma of the form 0<=a<c and 0<=b<d implies ab<cd, so let's just find it". I totally agree about the weird Esc then ctrl-space thing, I've never known why you sometimes need to do this to get far more options, it's just a trick I've picked up. I think I've mentioned it before but nobody ever explained what was going on (which is surprising because usually people are good at explaining everything here).

Kevin Buzzard (Sep 10 2021 at 20:06):

In the mean time, do you know this trick? Exit your proof completely and try

example (a b c d : ) (ha : 0  a) (hab : a < b) (hc : 0  c) (hd : c < d) :
  a * c < b * d := by library_search

Kevin Buzzard (Sep 10 2021 at 20:07):

This is a trick I use fairly often, as well as the "guess the name" trick (which you seem to have picked up, apart from the additional Esc trick to make it work more often :-) )

Trevor Fancher (Sep 10 2021 at 20:09):

I do know that trick. I guess it didn't help in this case because I was searching for something too specific (along the lines of

lemma mul_le_left {a b : } (ha : 0  a) (hb : 0  b) (hb1 : b < 1)  : a * b  a

which is the lemma I ended up proving to finish of the exercise. Btw, I came up with that name so its perhaps not the best).

Trevor Fancher (Sep 10 2021 at 20:11):

I guess the Esc then ctrl+space trick is something I'll remember from now on. Thanks :)

Kevin Buzzard (Sep 10 2021 at 20:12):

Your mul_le_left won't be in the library because it's somehow suboptimal: you can get away with the weaker hypothesis b<=1

Trevor Fancher (Sep 10 2021 at 20:13):

Yes, I noticed that after posting it here. For some reason I didn't notice when in the heat of battle :)

Kevin Buzzard (Sep 10 2021 at 20:13):

lemma mul_le_left {a b : } (ha : 0  a) (hb : 0  b) (hb1 : b  1)  :
  a * b  a := mul_le_of_le_one_right ha hb1 -- thanks library_search

Trevor Fancher (Sep 10 2021 at 20:14):

Ok, wow. I missed that one. Nice.

Trevor Fancher (Sep 10 2021 at 20:22):

Btw, library_search fails for my first version (I guess because the b<1 hypothesis is too strong). Perhaps that is also what sent me off track. I'm definitely learning a lot here. The moral here seems to be to make sure to state the most general example in order to help library_search succeed.

Kevin Buzzard (Sep 10 2021 at 20:24):

Just to be clear -- library_search only finds things which are explicitly stated in mathlib, as opposed to e.g. things which can be trivially deduced by composing two theorems in mathlib, so you have to get it exactly right. One thing I didn't understand for a while was which theorems go into mathlib and which don't -- the idea is basically that clean and useful theorems go in, and random true statements which probably aren't useful in general don't.

Trevor Fancher (Sep 10 2021 at 20:29):

Ya. But dropping a factor thats less that one from an inequality is so common in analysis that I just knew it had to be there. I spent way too much time trying to find it. But many lessons learned along the way, so overall worth the effort (is what I keep telling myself :)

Kevin Buzzard (Sep 10 2021 at 20:43):

Formalising is hard! After a while you begin to find your way around the library. By the way, another possibility is the "non-linear inequality tactic" nlinarith:

lemma mul_le_left {a b : } (ha : 0  a) (hb : 0  b) (hb1 : b < 1)  :
  a * b  a := by nlinarith

Trevor Fancher (Sep 10 2021 at 20:50):

Ah, yes. I forgot about nlinarith. After doing so many of the basic exercises from the first couple weeks, I sometimes find myself doing stuff the tedious way out of habit rather than reaching for the more high powered tactics. It's probably time I start familiarizing myself with more tactics.

Kevin Buzzard (Sep 10 2021 at 21:00):

The tedious way is fun and satisfying :-) But when you want to make progress more quickly e.g. because you're making some theory of your own, you just want to get goals out of the way!

Scott Morrison (Sep 12 2021 at 02:01):

Remember you can also use suggest as well as library_search. It returns many results, even if they don't close the goal.

Scott Morrison (Sep 12 2021 at 02:01):

suggest using h only returns results which make some use of the hypothesis h. It is really useful!

Phillip (Sep 12 2021 at 05:38):

Scott Morrison said:

suggest using h only returns results which make some use of the hypothesis h. It is really useful!

Is there an equivalent in Lean4?

Scott Morrison (Sep 12 2021 at 05:58):

It's on my todo list, but don't hold your breath. :-)

Last updated: Dec 20 2023 at 11:08 UTC