Zulip Chat Archive

Stream: new members

Topic: NNG syntax different from Lean's

Jason Rute (Dec 06 2023 at 00:03):

@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 (Dec 06 2023 at 00:11):

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 (Dec 06 2023 at 02:45):

@Jon Eugster

Alexander Bentkamp (Dec 06 2023 at 03:33):

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 (Dec 06 2023 at 03:36):

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

Johan Commelin (Dec 06 2023 at 08:28):

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

Johan Commelin (Dec 06 2023 at 08:29):

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

Jon Eugster (Dec 06 2023 at 10:11):

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 (Dec 06 2023 at 10:12):

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 (Dec 06 2023 at 10:38):

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 (Dec 06 2023 at 11:44):

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 (Dec 06 2023 at 15:24):

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 (Dec 06 2023 at 15:55):

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 (Dec 06 2023 at 15:56):

why would GCD appear when proving things using Rat?

Mario Carneiro (Dec 06 2023 at 15:56):

you shouldn't be unfolding the definitions

Yaël Dillies (Dec 06 2023 at 15:58):

Also there's docs#Nat.succ_le_succ_iff

Craig Gidney (Dec 06 2023 at 16:11):

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 (Dec 06 2023 at 16:23):

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 (Dec 10 2023 at 23:49):

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 (Dec 13 2023 at 17:44):

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 (Dec 13 2023 at 17:44):

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

Kevin Buzzard (Dec 14 2023 at 18:40):

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?

Last updated: Dec 20 2023 at 11:08 UTC