Natural Numbers Game: Proof works in game, not in lean

Stream: new members

[Peter B]

Hi!

I've been using the Natural Number Game at https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/ as an excuse to learn a little lean. What I've done is set up a Lean environment, and then for each level, I copy the lemma over into my editor, solve it in my local environment, and then bring the solution back into the game. Works great.

My problem is on the add_mul level I seem to have found a solution that works fine in the game but not in my lean 3 install.

In-game code:

begin
induction t with t ht,
repeat {rw mul_zero},
repeat {rw mul_succ},
refl,
simp,
rw ht,
refl,
end

In my local lean 3 install, simp says it can't simplify the expression any further. Is this just an artifact of the game not using the 'real' natural number support in Lean, and it's own custom class instead?

[Peter B]

(At this point, the goal is:

case nat.succ
abt: ℕ
ht: (a + b) * t = a * t + b * t
⊢ (a + b) * t + (a + b) = a * t + a + (b * t + b)

[Julian Berman]

The game is indeed quite different from "real Lean" (even though it's amazing and a great way to learn). But copying back and forth like that you'll find lots of differences.

[Julian Berman]

The version of Lean is different (older), some tactics are changed for pedagogical purposes (to be weaker but easier to understand)

[Julian Berman]

For this specific case if you're curious could you perhaps share a #mwe including the theorem statement, or at least the specific link to the level?

[Julian Berman]

actually I guess the only think I was unsure of was which variable was t but your goal state answers that, so it's just

lemma add_mul' {a b t : ℕ} : (a + b) * t = a * t + b * t := begin
  induction t with t ht,
  repeat {rw mul_zero},
  repeat {rw mul_succ},
  refl,
  simp,
  rw ht,
  refl,
end

and now I can indeed reproduce.

[Peter B]

Oh gosh, I thought I included the lemma - my bad

[Peter B]

My Lean 3 version of this is:

lemma add_mul (a b t : nat) : (a + b) * t = a * t + b * t :=
begin
induction t with t ht,
repeat {rw mul_zero},
repeat {rw mul_succ},
rw add_comm,
rw add_assoc, -- close
sorry,
end

and the proof state at the "--close" comment is:

case nat.succ
abt: ℕ
ht: (a + b) * t = a * t + b * t
⊢ a + (b + (a + b) * t) = a * t + a + (b * t + b)

...which has the left of the equality looking similar to the state in the web app post-simp, but the right is pretty far away. I'm not yet quite adept enough at rewriting, honestly.

[Julian Berman]

No worries -- I'm honestly not 100% sure what precise changes are responsible, someone else may come along and know.

For reference, here's a proof that works on "real Lean":

lemma add_mul' {a b t : ℕ} : (a + b) * t = a * t + b * t := begin
  induction t with t ht,
  { repeat {rw mul_zero}, refl },
  { simp [nat.mul_succ, ht, nat.add_comm, nat.add_assoc, ←nat.add_assoc (a * t) _] }
end

where I looked at what simp was confused about and taught it not to rewrite so it gets stuck

As I say someone may know which precise changes are responsible, but in general like I was trying to mention, things do differ as lean evolves -- in particular I suspect some glossary#simp-lemma s have changed. Also whether rw automatically runs refl afterwards is a thing that's often confusing when transitioning between NNG and "real Lean" -- in fact I notice in my code above, the refl is only needed if I don't import tactic, which is even more confusing.

[Julian Berman]

(Also by the way it's good to use the curly braces so you only have one goal focused at a time)

As for:

I'm not yet quite adept enough at rewriting, honestly.

don't worry about it, NNG by the end will make you quite adept I think.

[Kevin Buzzard]

nat (the lean version) and mynat (the natural number game version) are different types with different simp lemmas so it doesn't surprise me that simp behaves differently on analogous goals involving the two types.

[Jon Eugster]

simp in the natural number game seems to use commutativity and associativity to reorder the terms and get some kind of "normal form", the real simp doesn't do that, but there is the tactic ring (or ring_nf) which does exactly that:

import tactic.ring

example (a b t : ℕ) : (a + b) * t = a * t + b * t :=
begin
  induction t with t ht,
  repeat{rw mul_zero},
  ring
end

[Kevin Buzzard]

Of course you can prove all the lemmas with ring if you're using the inbuilt naturals ;-) nat has got a huge amount of infrastructure attached to it already, mynat has nothing so it wouldn't surprise me at all if they behaved very differently when using tactics like simp. If you want to play the levels in VS Code then it might just be easier to install the repo locally with leanproject get ImperialCollegeLondon/natural_number_game and then just open up the files in the various levels in src/game/worldX and solve them. Another advantage of this approach is that you get access to the "lost levels" here, this is a proof of strong induction which I never got around to making web pages for.

[Peter B]

@Kevin Buzzard Maybe this is a little silly, but I was so charmed by your and @Mohammad Pedramfar's work on the Natural Number game I did a "Let's Play" (of sorts) of the Tutorial and Addition World. Enjoy. https://youtu.be/e26V91LmhzY

[Peter B]

Have you ever played/looked at Joachim Breitner's _Incredible Proof Machine_? http://incredible.pm

[Eric Rodriguez]

he's also on the server :)