Hello and question about NNG online vs local install

Stream: new members

[Stephen Hicks]

Hello -
I'm a new member here, I'm interested learning more about lean prover, but it's just for fun for me. I am a retired EE.

I was excited to see the post about How To Prove it with Lean, and I had completed previously the natural number game in Lean 3, but thought since it was using Lean 4 I should go back and redo it in lean 4. I had been doing the online version at https://adam.math.hhu.de/ but had been having trouble completing Power World Level 6 mul power. So I tried the version from https://github.com/leanprover/lean4-samples installing locally. I was able to figure out that I could complete the proof using

simp only [mul_comm, mul_left_comm, mul_assoc]

but that was somewhat unsatisfying since I really wanted to understand how to do it with rw and I was having trouble with terms like a ^ n getting errors. I was able to at least get the steps using

  show_term {
    simp only [mul_comm, mul_left_comm, mul_assoc]
  }

in my local version on lean4 on my laptop. But trying to use that in the online version I ran into a couple of problems terms like

induction n with
  | zero =>
    repeat rw [zero_is_0]

but in the online version I needed to write it like

induction n with d hd
repeat rw [zero_is_0]
...

But more of an issue was when I got the part where I need use rewrites of the form

rw [mul_comm  (a ^ n * b ^ n) (a * b)]

I get and error on the induction line

Line 1, Character 0

declaration uses 'sorry'

for my purposed I'm fine using the local version installed on my machine but I thought the online version was so cool and I really got a lot out of using it with leanprover 3 I thought I would ask if anyone knows whats going on.

Sorry for the lenghty explanation and Thanks!
Stephen Hicks

[Kevin Buzzard]

NNG induction (used in NNG4) isn't the same as core Lean 4 induction (used in lean4-samples); we re-implement some tactics to make them more beginner-friendly, that probably explains the difference in behaviour. The other error I don't really know what's going on, can you maybe post your full proof script which generates the error?

[Stephen Hicks]

Thank you so much for the quick reply. Of course! I didn't do it because I was a bit worried about spoiling the game.

theorem MyNat.mul_pow ∀ (a b n : ℕ), (a * b) ^ n = a ^ n * b ^ n := by
induction n with d hd
repeat rw [pow_zero]
rw [mul_one]
rfl
repeat rw [pow_succ]
rw [hd]
rw [mul_comm  (a ^ n * b ^ n) (a * b)]
--    rw [mul_assoc a b (a ^ n * b ^ n)]
--    rw [mul_comm (a ^ n) a]
--    rw [mul_comm (b ^ n) b]
--    rw [mul_left_comm (a * a ^ n) b (b ^ n)]
--    rw [mul_assoc a (a ^ n) (b ^ n)]
--   rw [mul_left_comm b a (a ^ n * b ^ n)]
-- simp only [mul_comm, mul_assoc, mul_left_comm]

and the error is

Goal:
(a * b) ^ n = a ^ n * b ^ n
Line 1, Character 0

declaration uses 'sorry'

If I comment out the last rw and uncomment the simp only it completes the goal

[Kevin Buzzard]

The game is going to be completely rewritten this month because I want to expand it and then use the expanded version for teaching, which starts in early October. So don't worry about spoilers. The solutions are all in the source code on GitHub anyway so publically available

[Stephen Hicks]

Thank you for the quick reply. I'm happy to wait and retry on the new version when it comes out. Also happy to submit bugs if you do that kind of tracking.

[Kevin Buzzard]

The problem with your code is that the last line talks about n but there is no n in sight in the goal or context (it disappeared when you applied induction on it). The problem with the game is that it's giving you an extremely unhelpful error, but normal service is restored if you change those ns to d. Please feel free to open an issue, the repo is https://github.com/hhu-adam/NNG4

[Stephen Hicks]

Thanks so much! Duh! I will look closer next time. And thanks for the liink I will write up an issue for the message and also I have another place to look to see if it's already a known problem