Strong induction world

[kbuzzard]

I have a strong induction world in the lean 3 version of NNG but I never got around to putting it online. It's here. This needs to be broken up into bite-sized pieces, translated into Lean 4, and added as a new world.

[ndcroos]

Hi, I'd like to work on this issue. Can this be assigned it to me please?

[kbuzzard]

Sure!

For reviewing purposes, can you start by just adding a few levels? It seems to me that some of the levels I suggest in the route above are already in NNG4, or should not be in strong induction world. So some design decisions need to be made here. One possibility is that you start with a proof of strong induction and work back to see exactly which facts you need about <, and then basically make a new world which is basically < world with a proof of strong induction at the end.

[kbuzzard]

@ndcroos someone else has asked about this -- did you make any progress on it? The first step is to translate the Lean 3 code into Lean 4.

[ndcroos]

Hi, I am sorry, I could not work on this issue earlier due to other duties. But I am now going to start working on this. It still seems to me a nice project.

[kvanvels]

@ndcroos, I am not the "someone else" that Kevin mentioned earlier, but I have started working on this. I have a good amount of the world sketched and in decent shape. I will be polishing this up and making a pull request here tomorrow. Then we can work together.

[ndcroos]

@kvanvels Thanks! I'll keep an eye out for your PR. Let me know if I can do anything to help once the PR is made. (I am looking at this moment at your work in your NNG4 fork.)

[kvanvels]

@ndcroos Please don't judge the code too harshly. :) I was just trying to get stuff down. I doubt it even runs now in the browser.

[kvanvels]

@ndcroos, Have a look at the repo I set up. I forked the NNG, and have a local branch named kvv_lt, I am working on the introductions, conclusions and the hints. I have levels one through six in pretty good shape.

Be patient with me with interacting on github because I am still getting the hang of it.

Thanks,
Kent Van Vels