Replace recursive definitions of algebraic operations with axioms

[kbuzzard]

I get annoyed when I see solutions to NNG levels in the wild which rely on definitional equality. We get confused people reporting bugs in NNG3 because they accidentally proved x + 0 = x by rfl and it worked. I tried to get around this by getting Jon/Alex to weaken rfl so that it wasn't solving stuff like this and 2 + 2 = 4, but apply and exact still manage to unify x and x + 0.

I decided that one approach to this could be to redefine addition, multiplication and exponentiation via opaque constants obeying axioms. All worlds apart from Algorithm World worked fine after the refactor, but this approach broke decide, which was no longer able to put 2 + 2 into a normal form. We have worked around this by making a custom simp set which knows the axioms defining + * and ^ and with another rule which makes numerals greater than 0 reduce to MyNat.succ (MyNat.succ ... (MyNat.succ 0))..); MyDecide applies this simp set and then runs decide. Thanks to all on the Zulip thread for suggestions.

Before:

(and user then shows up on Zulip confused about a "bug".)

After:

[Madjosz]

Maybe it is also possible to weaken tauto since it can solve Algorithm world 6,8 and tutorial world completely?

[kbuzzard]

OK, it took me two weeks to find the time to push this over the line, but I think now it's ready. I modified the the decide tactic so that it runs a custom simp set to reduce MyNat numerals and expressions like 1 + 1 to a reduced normal form (MyNat.succ (MyNat.succ ... MyNat.zero))..., which is perfectly fine for what we're trying to do here. The diff looks acceptable to me, and users should not notice any difference with the game.

Unrelated: I also changed myNatFromNat to MyNat.ofNat and natFromMyNat to MyNat.toNat (because an initial version of this idea used reduction to Nat), and I also fixed the (unique) linter warning that we get when compiling. Let me know if you want me to extract these out.

[kbuzzard]

PS happy to squash-merge (but don't really know what I'm talking about)

[kbuzzard]

Maybe it is also possible to weaken tauto since it can solve Algorithm world 6,8 and tutorial world completely?

This approach automatically weakens tauto too because a + 0 = a is no longer a tautology (it's an axiom, not true by definition).