NNG syntax different from Lean's

Stream: new members

[Jason Rute]

@Kevin Buzzard (or whomever runs NNG) I just want to point you to this PA.SE where a user was very confused about Lean syntax since it was very different from the NNG. See the answer and comment. https://proofassistants.stackexchange.com/questions/2587/what-do-i-need-to-import-from-mathlib-to-make-induction-a-with-d-hd-work/2589#2589

Yeah it's definitely very confusing to play a game specifically to learn lean, and then it sets a series of traps that mean what you learn is different from actually using lean.

I don't know the full answer. Maybe it would be good to use rewrite instead of rw, use induction' or just adopt the new induction syntax, etc. Or if you do keep it separate, maybe some accessible note stating all the differences. Anyway, food for thought.

[Kevin Buzzard]

I don't think that mathematicians can see the point of the ascii art so I don't want to switch to Lean induction. Switching to induction' and rewrite is probably what I want to do, but these are so long to type. Is there any way that we can somehow integrate "click on tactic to make it magically appear in infoview" or have some drop-down menu for choosing a tactic or something? I think that something like this would be a nice solution. @Alexander Bentkamp ?

[Alexander Bentkamp]

@Jon Eugster

[Alexander Bentkamp]

I agree that point and click for tactics would be nice. But it really does not save a lot of time because you would probably still have to switch back to the keyboard to enter the arguments of the tactic.

[Alexander Bentkamp]

Maybe the error message when typing induction ... with... could be improved to point to induction'?

[Johan Commelin]

Pretty soon, Lean core will fix induction so that it is doing the nice thing.

[Johan Commelin]

@Kevin Buzzard How about a final world, in which people learn the differences between NNG-tactics and "real-world-Lean" tactics?

[Jon Eugster]

Kevin Buzzard said:

Is there any way that we can somehow integrate "click on tactic to make it magically appear in infoview" or have some drop-down menu for choosing a tactic or something? I think that something like this would be a nice solution.

We discussed something similar once and decided this wouldn't be a feature we'd want to invest the time to implement. However, the code is open-source and I'm very happy to help anybody interested in navigating the code base :)

[Jon Eugster]

FWIW, I think I once added paragraphs to some in-game-tactic-docs explaining the changes NNG makes, but I see that it only survived for rfl.

[Anand Rao Tadipatri]

I have been working on point-and-click tactics for Lean and would be interested in adding them to the NNG once they are polished enough. For tactics that require arguments, a drop-down list with suggestions (as demonstrated in the third gif) could be used to avoid the back and forth between the textbox and the user interface. (I noticed that sub-expression selection by shift-clicking doesn't work currently in the NNG, but perhaps this has something to do with the LocationsContext?)

[Jon Eugster]

That would certainly be cool! Once they are for example in Std, I assume it should be easy to add. If the selection already doesn't work at https://live.lean-lang.org (or lean.math.hhu.de) then that should be fixed in lean4web, which is used in the games. I never selected subexpressions, so I'm not sure how to test this - I also don't observe anything happening shift-clicking an a random file in vscode. If you write a issue for this bug at lean4web, I'll look at it eventually.

[Anand Rao Tadipatri]

I tested a bit more and it looks like sub-expression selection works on the Lean Web Editor after all, it's just that the highlighting doesn't persist in the way that I'm used to (which is fine).

[Craig Gidney]

I'm the person who was confused. I did manage to get past the issue. I tried to dump a bunch of beginner questions onto the proof assistant stack exchange as I went, to make the path a bit more obvious. Anyways, the NNG and the stack exchange were enough to get me to the point where I can prove the CHSH inequality over random strategies ( https://gist.github.com/Strilanc/2e9778537f810df54063e2b79685642c ). It's not an elegant proof, but it passes.

Something maybe interesting is that I wanted to use Rat for the probabilities, but found it impossible to prove basic things with Rat because of the GCD monster that appears when operating on them. I ended up defining my own un-normalized Odds struct instead, despite the fact it required me to prove transitive ordering on that class which was very difficult for me.

An obstacle I still keep running into is that there is a lot of variation in what methods are present for the various types. A particular annoyance is methods that are unnecessarily one-way instead of two-way. For example, Nat.succ_le_succ could work with rewrite, but instead its inverse direction has a different name Nat.le_of_succ_le_succ .

[Mario Carneiro]

why would GCD appear when proving things using Rat?

[Mario Carneiro]

you shouldn't be unfolding the definitions

[Yaël Dillies]

Also there's docs#Nat.succ_le_succ_iff

[Craig Gidney]

The GCD appears when I use induction on them and it pulls apart the definition, revealing the normalization. I completely buy that I'm doing it wrong.

Thanks for pointing out the method. I did look for it but did not find it. I was looking in the files that visual studio code's go-to-definition sent me into, instead of on the website, though.

[Ruben Van de Velde]

Yeah, using induction on a rational doesn't seem like it has useful behavior. Probably there are other ways to achieve what you were doing with it

[Craig Gidney]

The proof slowly improves as I find things in mathlib. nlinarith seems to solve most of the trivial stuff that was tripping me up with rationals. Down from 500 lines to 200 lines: https://gist.github.com/Strilanc/a4ee34e3a93db5dcb420a03517253491

[Alex Meiburg]

I'm curious Craig, why did you want to do induction on rationals, and what would you ideally have had? In the sense of -- what proof 'ideas', in English, would have led to induction on rationals?

[Alex Meiburg]

Maybe there's a good alternative induction theorem to define on rationals that would capture what you want :)

[Kevin Buzzard]

Why do you make <= Bool-valued? You're proving theorems so your life would be much easier if it were Prop-valued; you are constantly coercing from Bool to Prop this way. And why is probability Q-valued rather than R-valued?