leanprover-community/NNG4

Strong induction world

Opened this issue · 2 comments

kbuzzard commented

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 commented

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

kbuzzard commented

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.