VSCode - show more suggestions

Stream: new members

[Trevor Fancher]

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]

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]

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]

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

[Trevor Fancher]

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]

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]

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

[Kevin Buzzard]

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]

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]

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]

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]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

Ok, wow. I missed that one. Nice.

[Trevor Fancher]

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]

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]

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]

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]

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]

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]

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]

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

[Phillip]

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]

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