Zulip Chat Archive

Stream: lean4

Topic: Port NNG to Lean 4


Huỳnh Trần Khanh (Jan 28 2021 at 14:14):

Is it possible to port NNG to Lean 4? Will we do it?

Kevin Buzzard (Jan 28 2021 at 14:19):

I would imagine that porting the Lean code would be a very pleasant exercise, and indeed a few weeks ago someone posted to this Zulip a bunch of NNG stuff in Lean 4. I have no clue about how one turns Lean 4 code into a browser game though so cannot comment on that. It would probably be not unfair to say that this is not high priority for me right now (although of course if someone else wants to take it on I'm not going to be complaining!). However once we're at the stage where we are expecting newcomers to use Lean 4 rather than Lean 3 (and I have no clue about when this will happen, I am adopting a "wait and see" approach here because I have no idea about any of the subtleties involved) then I would imagine that this would become a much higher priority, because NNG seems to work as a way of attracting people with a mathematical interest to Lean.

Sebastian Ullrich (Jan 28 2021 at 14:24):

step 1: figure out how to compile Lean 4 to Wasm
step 2: figure out how to connect the Lean 4 server with a web editor
step 3: remove "and don't forget the comma"

Kevin Buzzard (Jan 28 2021 at 14:25):

you forgot all semicolons in your message

Reid Barton (Jan 28 2021 at 14:25):

I noticed rw doesn't like to apply refl rfl afterwards now, so Kevin will be happy about that!

Sebastian Ullrich (Jan 28 2021 at 14:26):

Kevin Buzzard said:

you forgot all semicolons in your message

I prefer whitespace sensitivity

Kevin Buzzard (Jan 28 2021 at 14:26):

So we see!

Matthew Ballard (Aug 05 2022 at 16:35):

(I also use it to tex and lean from my iPad)

Alexander Bentkamp (Aug 05 2022 at 20:39):

I had worked on the idea of running Lean on a server a while ago, and now I've worked on it a little more. Here is the result so far: https://lean-browser.herokuapp.com/. It may take a while to load because I am not paying for the server. As soon as you see a little "1" in the top left corner, write some Lean code. You can hover over anything that gets underlined. There is no info view yet... And the whole thing seems to collapse after some time of inactivity. But it definitely seems fast enough to work with, at least from Europe where the server is located.

Alexander Bentkamp (Aug 05 2022 at 20:43):

Oh, and I haven't worked out how to handle multiple users at once. So if you get output that doesn't seem to belong to you, somebody else is playing at the same time :grinning:

Alexander Bentkamp (Aug 05 2022 at 20:45):

Here is the source code: https://github.com/abentkamp/lean-browser

Patrick Massot (Aug 17 2022 at 20:58):

Alexander Bentkamp said:

Oh, and I haven't worked out how to handle multiple users at once. So if you get output that doesn't seem to belong to you, somebody else is playing at the same time :grinning:

I'm interested in playing a bit with this idea but I realize I have no idea how stateful web applications work. How can I tell my Apache server that whenever it gets a request on a certain url it should check whether this user already runs Lean and either talk to the corresponding Lean process or start one? Is that something that FastCGI can do? How does something like GitPod handles this? Then how does GitPod or a similar application decides to kill any process? Does it simply wait for a certain time after the last request?

Alexander Bentkamp (Aug 18 2022 at 07:00):

I've fixed this issue by now. I am using websockets, which is a protocol that can identify different clients much more easily than HTTP. I think Gitpod is using websockets, too. I don't know FastCGI.

Alexander Bentkamp (Aug 18 2022 at 07:01):

With HTTP, you would need to assign an identifier to each client that the client would include with each request. The identifier should be hard to guess so that you can't steal other people's identity.

Patrick Massot (Aug 18 2022 at 10:59):

@Alexander Bentkamp Do you have any documentation to recommend about all that?

Alexander Bentkamp (Aug 18 2022 at 11:21):

It depends on what you would like to use to implement the server. I used NodeJS. Here is a tutorial about that: https://dev.to/codesphere/getting-started-with-web-sockets-in-nodejs-49n0

Alexander Bentkamp (Aug 18 2022 at 11:22):

Here is documentation about the client side: https://developer.mozilla.org/de/docs/Web/API/WebSocket
And here documentation about the (NodeJS) server side: https://www.npmjs.com/package/ws

Patrick Massot (Aug 18 2022 at 11:37):

So NodeJS is directly taking connections from the outside world without going through Apache or Nginx or anything like that?

Patrick Massot (Aug 18 2022 at 11:38):

It's a pity that we can't do that directly in Lean 4 yet. But maybe František Silváši will tell us it actually can.

Alexander Bentkamp (Aug 18 2022 at 12:03):

You don't need Apache or Nginx. I also used express (https://www.npmjs.com/package/express) in the prototype above, although maybe that wasn't even necessary.

Alexander Bentkamp (Aug 18 2022 at 12:04):

Implementing the server directly in Lean would be nice :-)

Siddhartha Gadgil (Aug 18 2022 at 12:24):

I assume that will come when someone writes ffi bindings to something like https://github.com/cesanta/mongoose

Siddhartha Gadgil (Aug 18 2022 at 12:25):

Or maybe https://www.gnu.org/software/libmicrohttpd/ which seems smaller.

Alexander Bentkamp (Aug 18 2022 at 12:26):

I think @František Silváši is actually doing it the hard way and implements the protocol from scratch :-).

Siddhartha Gadgil (Aug 18 2022 at 12:26):

I am familiar with the JVM world so the specific libraries mentioned above are just from naive googleing.

Alexander Bentkamp (Aug 18 2022 at 12:28):

Anyway, for a usable Lean web interface, it's mostly the client side that needs more love. The server just forwards messages.

Alexander Bentkamp (Aug 18 2022 at 12:29):

And of course, there is the problem that someone would need to pay for the server.

Huỳnh Trần Khanh (Aug 18 2022 at 13:33):

This is just a proof of concept, isn't it? Because you didn't do security verification to prevent Lean from damaging the system, right?

Huỳnh Trần Khanh (Aug 18 2022 at 13:34):

It is possible to write programs in Lean. Programs in Lean can do anything programs in other languages can.

Alexander Bentkamp (Aug 18 2022 at 13:40):

Hm, yeah, good point. Any ideas how to prevent that?

Mario Carneiro (Aug 18 2022 at 13:43):

run lean in a container

Matthew Ballard (Aug 18 2022 at 13:43):

Is that enough?

Mario Carneiro (Aug 18 2022 at 13:44):

I think that's the standard approach for projects like tio.run and godbolt.org

Mario Carneiro (Aug 18 2022 at 13:44):

you also need resource limits

Arthur Paulino (Aug 18 2022 at 13:45):

This question has come up other times and the conclusion is often "run it in a VM/container". I don't have other ideas.

I have memories of someone mentioning that they were trying to build an inoffensive version of Lean 4 without IO

Mario Carneiro (Aug 18 2022 at 13:45):

yeah I strongly recommend against internal sandboxing here

Mario Carneiro (Aug 18 2022 at 13:46):

it's way too hard to get right and if you fail your server is hosed

Matthew Ballard (Aug 18 2022 at 13:46):

If it is not in the browser, then I would just make sure to have a kill switch and nothing of value on the machine.

Mario Carneiro (Aug 18 2022 at 13:47):

at the very least the machine has credentials to communicate with the website

Matthew Ballard (Aug 18 2022 at 14:06):

Source code for the playground at go.dev/play. In case anyone wants an example.

Patrick Massot (Oct 01 2022 at 09:18):

I'm pleased to announce that an early prototype of the first five levels of the natural number game is very temporarily available on http://pat.perso.ens-lyon.org/nng4/. I know that several things are missing (for instance you can easily type unicode characters if you want to right to left rewrite). This was mostly a learning project for me (Lean 4 programming of course but also React that I wanted to learn for future widget writing purposes). It is also a technological demo.

Patrick Massot (Oct 01 2022 at 09:19):

Note that, when you play the game, Lean runs on my home computer acting as a server. I won't keep this server running forever. So if you read the above message late and can't see anything but a circular loading icon in the middle of a webpage then it means the server is switched off.

EDIT: There is a small issue currently. If you see the circular loading thing forever when the server is meant to be running then you can open about:config in Firefox and toggle network.websocket.allowInsecureFromHTTPS to true.

Patrick Massot (Oct 01 2022 at 09:20):

Please see https://github.com/PatrickMassot/lean4-game-server, https://github.com/PatrickMassot/NNG4 and https://github.com/PatrickMassot/nng4-interface for a lot more details.

Johan Commelin (Oct 01 2022 at 09:21):

/me can't see anything but a circular loading icon in the middle of a webpage

Patrick Massot (Oct 01 2022 at 09:25):

This is extremely weird. Can you try reloading the page?

Patrick Massot (Oct 01 2022 at 09:25):

It worked yesterday evening with Kevin

Johan Commelin (Oct 01 2022 at 09:26):

Ctrl-F5 doesn't help

Riccardo Brasca (Oct 01 2022 at 09:29):

Same here.

Riccardo Brasca (Oct 01 2022 at 09:29):

Tried with firefox and chrome

Julian Berman (Oct 01 2022 at 09:39):

Firefox can’t establish a connection to the server at wss://pat.perso.ens-lyon.org:8765/.

Patrick Massot (Oct 01 2022 at 09:40):

I'll need to fix that but in the mean time you can open about:config in Firefox and toggle network.websocket.allowInsecureFromHTTPS

Julian Berman (Oct 01 2022 at 09:43):

It still seems to try to upgrade the connection, probably because of HTTPS-only mode... will try from another browser.

Patrick Massot (Oct 01 2022 at 09:43):

It now works for Johan

Patrick Massot (Oct 01 2022 at 09:45):

To be clear, what happens is that the website is running over https but it tries to talk to Lean through a non-secure websocket connection. I'll have to understand how to use a secure websocket connection.

Julian Berman (Oct 01 2022 at 09:49):

It still doesn't work here, (either because I'm on a newer version of FF beta than Johan or because my HTTPS-only mode is on the maximum security which I think isn't the default) but what does work is:

Screen-Shot-2022-10-01-at-10.48.23.png

i.e. just whitelisting your domain to allow non-HTTPS connections. And it's cool!

Johan Commelin (Oct 01 2022 at 09:50):

I really like the game-play. The way you get hints at a very granular level along the way is super nice!

Patrick Massot (Oct 01 2022 at 09:51):

That granularity was a very important target. It was one of main pains of the original NNG.

Patrick Massot (Oct 01 2022 at 09:52):

You can see how tactic-state-triggered messages are registered at https://github.com/PatrickMassot/NNG4/blob/main/NNG/Levels/Level2.lean#L31-L32 for instance.

Alexander Bentkamp (Oct 01 2022 at 10:59):

Wow, this is beautiful. Great work!

Do you have a way to get a server from your university? I assume I will get access to a university server next week. If you won't get one, I'd go ahead and host it there. It would be a pity to take it down, even if it's just a demo now.

Patrick Massot (Oct 01 2022 at 11:40):

It would make more sense to get a server from the Hoskinson center (cc @Jeremy Avigad ). But this is a bit premature. We need people to work a bit more on the interface (at least implementing unicode abbreviations and navigating the proof) and more people porting levels. Note that I stopped porting after the first level using induction.

Patrick Massot (Oct 01 2022 at 11:41):

Then before making wide announcements we would need someone who understand security to have a look at this.

Alexander Bentkamp (Oct 01 2022 at 11:48):

Ok, right, hosting it at the Hoskinson center would be even better.

It seems that security is not that much of an issue here because the interface to Lean is very restricted. You can just run a handful of tactics, not execute arbitrary Lean code. Anyway, sandboxing the Lean instances might still be a good idea, as Mario proposed above.

Patrick Massot (Oct 01 2022 at 11:50):

Sure, this is the main reason why I'm not allowing to run any tactic. I also prevents "cheating".

pcpthm (Oct 01 2022 at 12:58):

I found a way to cheat

Maybe the server should check the proof for axioms?

Patrick Massot (Oct 01 2022 at 13:28):

The tactic detection is indeed really basic. This is why I wrote this should be strengthened before advertising it more widely.

Alexander Bentkamp (Oct 02 2022 at 08:44):

I tried to build nng4-interface locally. I get:

$ npm run build

> nng_interface@0.1.0 build
> react-scripts build

Could not find a required file.
  Name: index.html
  Searched in: /Users/alex/Projects/nng4-interface/public

Alexander Bentkamp (Oct 02 2022 at 09:03):

Ok, got it to work using this standard React app index.html file: https://github.com/react-cosmos/create-react-app-example/blob/master/public/index.html

Patrick Massot (Oct 02 2022 at 10:59):

Oops, I forgot the public folder. Indeed I don't think I touched anything in that folder since launching the react app creation script. I just pushed it, sorry about the inconvenience.

Alexander Bentkamp (Oct 02 2022 at 16:35):

No problem, thanks!

Patrick Massot (Oct 03 2022 at 20:40):

Could anyone have a look at whether https://pat.perso.ens-lyon.org/nng4ssl/ works without switching off any security thing?

Adam Topaz (Oct 03 2022 at 20:40):

It seems to work fine for me

Patrick Massot (Oct 03 2022 at 20:41):

And did you test the previous version?

Adam Topaz (Oct 03 2022 at 20:41):

No :-/

Patrick Massot (Oct 03 2022 at 20:41):

Ok, it's still useful information but it would be even better to have someone who had to change something to get the previous version.

Patrick Massot (Oct 03 2022 at 20:42):

The issue is that it depends on web browser paranoia setting.

Adam Topaz (Oct 03 2022 at 20:42):

I'll try again with https everywhere turned on

Patrick Massot (Oct 03 2022 at 20:42):

On Saturday night Kevin had no trouble accessing the non-secure version but on Sunday morning Johan, Julian and Riccardo couldn't.

Matthew Ballard (Oct 03 2022 at 20:42):

Works for me also (Safari).

Matthew Ballard (Oct 03 2022 at 20:43):

Also did not test the previous version.

Adam Topaz (Oct 03 2022 at 20:43):

Adam Topaz said:

I'll try again with https everywhere turned on

https everywhere on and it still works

Adam Topaz (Oct 03 2022 at 20:45):

So now I have all the default paranoid settings from firefox turned on (https everywhere, full tracker blocking) as well as ublock origin turned on, and things still look good!

Matthew Ballard (Oct 03 2022 at 20:48):

I tried it on iPadOS Safari and it works there. In my experience, iPadOS has the most stringent security defaults.

Patrick Massot (Oct 03 2022 at 20:55):

Nice. For people interested in hosting their own game, I pushed a sample https://github.com/PatrickMassot/NNG4/blob/main/gameserver_ssl.py creating a wss server talking to Lean.

Patrick Massot (Oct 03 2022 at 20:57):

By the way @Frantisek Silvasi the above 50 lines of python are the only non-Lean piece of the Lean 4 NNG prototype. If your planned WebSocket lib in Lean can do that then we could have a 100% Lean setup.

Patrick Massot (Oct 03 2022 at 21:00):

I would be interested if any real Lean 4 programmer could have a look at what I did at https://github.com/PatrickMassot/lean4-game-server. It was a nice exercise to do this myself (with help of answers to my questions here of course), but now I would be very happy to see the official textbook solution.

František Silváši 🦉 (Oct 04 2022 at 09:10):

The project's being worked on, albeit slowly - I'll be happy to open source this mid-development if someone's interested, although maybe this is a good time to ping @Xubai Wang to see if they're willing to put some license on: https://github.com/xubaiw/BaseN.lean/ :).

Nevertheless, the current state of affairs is such that one can handshake/negotiate a WebSocket connection and I am in the process of finishing/debugging the basic frame structure that this connection requires. I can make few promises wrt. timelines here as this is very much a 'weekend evening' project, but it's not dead.

Patrick Massot (Oct 04 2022 at 09:27):

It's not really blocking anything, but it would be nice for Leo's talks to be able to say that Lean 4 goes all the way from checking proofs in the game to serving websocket connections.

Sebastian Ullrich (Oct 04 2022 at 10:20):

We should not abandon the goal of making all this work without a server either though :) . In fact a custom UI like this should make that quite a bit easier since replicating the LSP editor interface always seemed like the biggest hurdle.

Patrick Massot (Oct 04 2022 at 11:30):

What do you mean by "without a server"? Do you mean running Lean directly in the browser?

Sebastian Ullrich (Oct 04 2022 at 11:35):

Yes. You're not using the language server, so "export these specific Lean functions to (single-threaded) JS/WASM" is all you need, right?

Sebastian Ullrich (Oct 04 2022 at 11:35):

Plus "load this restricted set of imports from bundled .olean files". The size of .olean files (Init+Lean) was another in-browser worry, but that shouldn't be an issue for your case I assume.

Andrés Goens (Oct 04 2022 at 12:26):

Patrick Massot said:

Ok, it's still useful information but it would be even better to have someone who had to change something to get the previous version.

this works for me and the previous version didn't! (and it's really cool)

Arthur Paulino (Oct 04 2022 at 12:33):

I love the geeky RPG vibes of this version. Well done!

Patrick Massot (Oct 04 2022 at 14:02):

Sebastian Ullrich said:

Yes. You're not using the language server, so "export these specific Lean functions to (single-threaded) JS/WASM" is all you need, right?

I don't really know. What I I think I need is exactly what is in https://github.com/PatrickMassot/lean4-game-server

Patrick Massot (Oct 04 2022 at 14:04):

Arthur Paulino said:

I love the geeky RPG vibes of this version. Well done!

Some of it is already in the original NNG, but I wanted to emphasize that Lean 4 meta programming allows to use Lean in a way that doesn't look like Lean, and this is part of it. As explained in https://github.com/PatrickMassot/NNG4#some-game-play-choices, this is completely specific to NNG and not baked in the game server.

Chris Lovett (Oct 05 2022 at 04:23):

I'm also interested in doing the nng as a lean4 sample that runs in vscode (or in gitpod), see https://github.com/leanprover/lean4-samples/tree/clovett/NaturalNumberGame/NaturalNumberGame.

Patrick Massot (Oct 05 2022 at 07:27):

What is the motivation for that version?

Chris Lovett (Oct 05 2022 at 19:18):

mostly trying to decouple from the problem of "web hosting" so we can make progress on the actual content, and providing a place for the code to be checked in so multiple folks can work on it... I saw you posted this link http://pat.perso.ens-lyon.org/nng4/ but the web page you posted didn't respond. Ah, but now I see you have a repo already at https://github.com/PatrickMassot/NNG4 so I'll check that out. Ignore my branch then, unless you want to make this an official lean4-sample. My branch has more of additional world too I think. Should I port that to your repo? are you actively working on this or should I continue with my branch? Your TacticDocs stuff is interesting... I see you are also working on https://github.com/PatrickMassot/lean4-game-server, so I'll check that out also...

Patrick Massot (Oct 05 2022 at 19:55):

You can try http://pat.perso.ens-lyon.org/nng4ssl/ that has less SSL issues.

Patrick Massot (Oct 05 2022 at 19:57):

And indeed contributing more levels to https://github.com/PatrickMassot/NNG4 is very welcome. I stopped at the first inductive proof because I was interested in building the framework, not porting levels. I hope Kevin will easily find people interested in porting levels. Also the game server currently does not put levels into worlds. This refinement would be very easy to add, but doing it from the beginning would have been a distraction only.

Chris Lovett (Oct 05 2022 at 20:16):

ha ha, it works, that's pretty fun, thanks. I found that the rfl after rewrite was unnecessary because rewrite now does a rfl automatically, but your version of the game still acts like the rfl is needed... also the instructions talk about typing "\l" to get a left arrow, but that doesn't work in your Invocation box...

Mario Carneiro (Oct 05 2022 at 20:20):

removing the rfl after rw is one of the changes that was made in the original NNG to make it more orthogonal for teaching purposes

Chris Lovett (Oct 05 2022 at 20:30):

and I take it level 5 is not complete yet? It doesn't let me "cast an induction spell"...
image.png

Patrick Massot (Oct 05 2022 at 20:31):

That's because you didn't read the explanation about how to cast that spell

Patrick Massot (Oct 05 2022 at 20:32):

The game server is really meant for single line tactics. The new-style induction tactic is completely orthogonal to that, so I wrote a custom induction tactic. And for that game in particular induction won't work anyway because the natural numbers that are used are not an inductive type, see the discussion at https://github.com/PatrickMassot/NNG4#some-game-play-choices

Mario Carneiro (Oct 05 2022 at 20:41):

The blurb at the end of level 3 mentions rewrite ← h which is problematic both because of the lack of unicode and the missing brackets

Patrick Massot (Oct 05 2022 at 20:43):

:sad: I tried to find all those missing brackets but obviously they were everywhere since you would never put them for a single rewrite in Lean 3.

Mario Carneiro (Oct 05 2022 at 20:44):

why not have the NNG version be just rw h with no brackets and no option for multiple rewrite?

Mario Carneiro (Oct 05 2022 at 20:46):

in level 5 if you write induction_on n with n ih it gives an "unexpected end of input" error

Chris Lovett (Oct 05 2022 at 20:46):

rw h doesn't work for me in VS Code with latest lean4 ...? It seems I have to write rw [h]

Mario Carneiro (Oct 05 2022 at 20:47):

that's the lean 3 syntax

Mario Carneiro (Oct 05 2022 at 20:47):

you were allowed to omit the brackets if there was only one rewrite

Mario Carneiro (Oct 05 2022 at 20:47):

in lean 4 this was removed

Chris Lovett (Oct 05 2022 at 20:48):

That seems to go counter to your goal in lean4-game-server of "This discrepancy led to some issues down the road where people got confused by ways tactic have subtly different behaviors in NNG and regular Lean"

Patrick Massot (Oct 05 2022 at 20:48):

I fixed those issues (sorry for people who were playing, I restarted the server)

Patrick Massot (Oct 05 2022 at 20:48):

What goes counter to my goal?

Patrick Massot (Oct 05 2022 at 20:49):

Mario Carneiro said:

why not have the NNG version be just rw h with no brackets and no option for multiple rewrite?

I also considered doing that. But since rewrite already existed it was faster to simply use it. I also wasn't sure how to shadow the existing rw tactic.

Mario Carneiro (Oct 05 2022 at 20:49):

I assumed that's why you spelled your induction tactic induction_on as well

Patrick Massot (Oct 05 2022 at 20:49):

Yes

Mario Carneiro (Oct 05 2022 at 20:50):

I believe (priority := high) on the syntax should suffice

Chris Lovett (Oct 05 2022 at 20:50):

What goes counter to my goal?

teaching to tactics that you invented just for the game...

Anatole Dedecker (Oct 05 2022 at 20:51):

Chris Lovett said:

That seems to go counter to your goal in lean4-game-server of "This discrepancy led to some issues down the road where people got confused by ways tactic have subtly different behaviors in NNG and regular Lean"

I think you misunderstood the proposed solution here. Patrick's approach is not to better stick with Lean4, but on the contrary to make a clear distinction between the game and Lean4 so that there is no confusion possible

Patrick Massot (Oct 05 2022 at 20:51):

Renaming the induction tactic also helps if people want to switch to regular Lean. This way it's clear it's a different tactic.

Sebastian Ullrich (Oct 05 2022 at 20:52):

It might be easier to use a custom syntax category if you want to deviate from tactic in general

Chris Lovett (Oct 05 2022 at 20:54):

so do you plan to stick with single line input for the whole game? If so, perhaps my "vs code" version of NNG serves a different goal for folks who want to learn Lean while editing actual lean programs, doing the NNG levels (exercises) as they go with the power of the full lean editor at their finger tips - this is what I personally would prefer but perhaps this then is for a different audience. Question is though would this cause confusion having 2 versions? Should I rename my "lean4-sample" perhaps just call it "NaturalNumbers" or something... since it doesn't really have all the fun "game" elements that the online version has.

Patrick Massot (Oct 05 2022 at 20:56):

Indeed I think it's better to have a clear distinction between the game and more serious stuff. As I explained in the README, Kevin really wanted this to be a game from the beginning. It became a common first Lean learning step by accident.

Kevin Buzzard (Oct 05 2022 at 21:08):

Yes we were all surprised about how well it took off.

Chris Lovett (Oct 05 2022 at 23:51):

Ok, I've renamed the sample to just "Natural Numbers" and prepared it as a leanink style book (removing the game elements). See https://github.com/leanprover/lean4-samples/tree/main/NaturalNumbers. This can be hosted on a simple github pages site like this: https://lovettsoftware.com/NaturalNumbers/index.html

Chris Lovett (Oct 06 2022 at 00:42):

Now I'm running into an interesting bug in my version and I'm not sure why, I'm finding I need to add this theorem theorem zero_is_0 : MyNat.zero = 0 := by rfl and use it in some places like in Addition Level 4 and I'm not sure why. Is there something missing from MyNat definition that makes it so that I have to do this? I think I implemented OfNat properly because I can do this #eval (zero : MyNat) -- 0, so I'm confused why I need this hack?

Mario Carneiro (Oct 06 2022 at 00:50):

When you just apply the induction principle for Nat, you end up with the actual constructors of the type, unadorned with any OfNat wrapper. The original NNG had to deal with this as well

Mario Carneiro (Oct 06 2022 at 00:50):

this is part of why NNG overrides the implementation of induction to handle this

Mario Carneiro (Oct 06 2022 at 00:55):

the regular induction tactic has the same behavior:

example (x : Nat) : x = x := by
  induction x
-- case zero
-- ⊢ Nat.zero = Nat.zero
-- case succ
-- n✝: ℕ
-- : n✝ = n✝
-- ⊢ Nat.succ n✝ = Nat.succ n✝

Chris Lovett (Oct 06 2022 at 01:32):

Ok, so it sounds like my having to add rw [zero_is_0] is not a bug, but things are working normally then. If so, I will try and add some explanation for this. I also found that the simp example didn't work in Lean 4 with the Level 6 example of (((a+b)+c)+d)+e=(c+((b+e)+a))+d, is this because I have not completed the AddMonoid instances and does that somehow extend the power of simp?

Mario Carneiro (Oct 06 2022 at 01:37):

you need to simp with add_assoc, add_comm, add_left_comm either by passing them to the simp call or marking the lemmas as @[simp]

Chris Lovett (Oct 06 2022 at 01:40):

I already have this: attribute [simp] zero_add add_assoc add_comm succ_add add_succ succ_eq_add_one one_eq_succ_zero add_right_comm but there is no add_left_com in the original NNG?

Chris Lovett (Oct 06 2022 at 01:57):

But interestingly, when I got to multiplication level 9 that example worked:

example (a b c d e : MyNat) :
  (((a*b)*c)*d)*e=(c*((b*e)*a))*d := by
  simp

Chris Lovett (Oct 06 2022 at 02:01):

and this has a left_comm attribute [simp] mul_assoc mul_comm mul_left_comm so I went back to level6 and changed it to this, and now it works too :-)

attribute [simp] add_assoc add_comm add_left_comm

example (a b c d e : MyNat) :
  (((a+b)+c)+d)+e=(c+((b+e)+a))+d := by
  simp

Kevin Buzzard (Oct 06 2022 at 07:09):

Yeah, this was a problem in Lean 3 NNG; 0 is has_zero.zero whereas induction would spit out nat.zero which printed differently and confused users. here is where I change induction so that it does usual induction and then runs dsimp with a simp set including this which means that users don't ever see the problem.

Alexander Bentkamp (Oct 06 2022 at 12:11):

Sebastian Ullrich said:

Yes. You're not using the language server, so "export these specific Lean functions to (single-threaded) JS/WASM" is all you need, right?

Do you have some hints on how to do this?

Sebastian Ullrich (Oct 06 2022 at 12:18):

I think the most promising way to an official Emscripten build of Lean was last discussed in https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/wasm.20nix.20emscripten.20build/near/271113368. Though if someone is seriously considering completing that work, we should first chat with @Leonardo de Moura about .olean platform portability expectations.

Chris Lovett (Oct 06 2022 at 22:32):

I found this Lean 4 solution to Power World Level 8, not using "Ring", but is there a simpler one?

lemma add_squared (a b : MyNat) :
  (a + b) ^ two = a ^ two + b ^ two + 2 * a * b := by
  rw [two_eq_succ_one]
  rw [one_eq_succ_zero]
  repeat rw [pow_succ]
  repeat rw [pow_zero]
  repeat rw [one_mul]
  rw [mul_add]
  repeat rw [add_mul]
  rw [one_plus_one]
  repeat rw [add_mul]
  repeat rw [one_mul]
  simp

See lean ink version

I couldn't get Mathlib.Tactic.Ring to work here as shown in Lean 3 NNG.

Chris Lovett (Oct 14 2022 at 05:29):

I'm happy to report the entire NNG is now ported to lean4, here's the raw source code :

The effort was a great learning experience and I have to thank Mario Carneiro, Heather Macbeth for much help and guidance along the way.

Note that this is not a 1:1 port as some tactics are missing still, like cc so the port includes rewriting proofs so they do not depend on these missing tactics. I think cc was the only real big missing piece I ran into. I also did not use ring since it was more work to setup. But if someone wants to go back and put ring back in PR's are welcome.

TBD: the stuff about collectable "instances" of things that use your proofs is not implemented because some of that stuff is still missing from mathlib4. If you search the web page for BUGBUG you will see where those TBD work items exist.

Chris Lovett (Oct 14 2022 at 08:50):

Oh, and having gone through the whole thing with a fine tooth comb, I have to say huge thanks to Kevin Buzzard for the original content - it is definitely well thought out and presents things in a really clear and enjoyable way. I only found 1 typo: your your goal

Chris Lovett (Oct 14 2022 at 11:16):

This is a map of the tactics covered and where they are first introduced:

image.png

Kevin Buzzard (Oct 14 2022 at 12:17):

The reason I push for "naturals are a semiring" before starting on order theory is that to prove naturals are a semiring you only need to know three tactics! I found this extraordinary. I remember telling @Jeremy Avigad at the time and him replying "sure, it's just equational reasoning" and me not having a clue what that even meant.

Kevin Buzzard (Oct 14 2022 at 12:19):

It was conversations like this which made me realise that 25 years of being a professional number theorist doesn't teach you anything about how mathematics actually works

David Michael Roberts (Oct 14 2022 at 13:42):

In classic category theorist fashion, I guess I get to say "number theory is really just the study of the free semiring on one generator"...

More seriously, there is such impressive richness in our playground, even from humble origins.

Jeremy Avigad (Oct 14 2022 at 16:28):

What I had in mind was Birkhoff's theorem:
https://en.wikipedia.org/wiki/Variety_(universal_algebra)
It tells us that lots of interesting structures can be axiomatized by equations, and that consequences of those equations can be proved with just rw.
https://en.wikipedia.org/wiki/Birkhoff%27s_theorem_(equational_logic)

joaogui1 (he/him) (Oct 20 2022 at 01:20):

@Patrick Massot given that Chris Lovett ported the content to Lean4 are you just going to use his port for the content and keep working on the interface? What's your plan?

Patrick Massot (Oct 20 2022 at 14:07):

Chris's effort is completely orthogonal to what is needed for the game. He wanted a set of Lean files to edit normally in VSCode, using an inductive type for natural numbers and Lean regular tactics. Also, in the game version, a lot of the work is to update the explanations from the Lean 3 game to remove unneeded parts and, much more importantly, to give explanations in response to tactic states.

joaogui1 (he/him) (Oct 20 2022 at 16:00):

Got it!


Last updated: Dec 20 2023 at 11:08 UTC