Zulip Chat Archive

Stream: new members

Topic: Odd resolution of goal in natural numbers game

Michaël Maex (Nov 19 2021 at 22:57):

I'm a total newbie who's working their way through the natural numbers game.
During an attempt to solve level 4 of the advanced multiplication world I stumbled upon behaviour that struck me as odd and that I would like to understand.

The code looks like this

theorem mul_left_cancel (a b c : mynat) (ha : a  0) : a * b = a * c  b = c :=
cases a,
apply ha,
revert b,
induction c with n hn,
intro b,
intro h,
rw mul_zero at h,
rw mul_eq_zero_iff at h,
intro b,
cases b,
intro hf,
rw mul_zero at hf,

After the exfalso the context looks like

2 goals
a : mynat,
ha : succ a  0,
n : mynat,
hn :  (b : mynat), succ a * b = succ a * n  b = n,
hf : succ a * 0 = succ a * succ n

case mynat.succ
a : mynat,
ha : succ a  0,
n : mynat,
hn :  (b : mynat), succ a * b = succ a * n  b = n,
b : mynat
 succ a * succ b = succ a * succ n  succ b = succ n

After rw mul_zero at hf, the context suddenly looks like

case mynat.zero
a : mynat,
ha : succ a  0
  (b : mynat), succ a * b = succ a * zero  b = zero

Not only did one goal disappear or get resolved in a very non-trivial way. The other goal changed in a way that I find very odd.
Does anyone see what's going on? I'd love to know

Kevin Buzzard (Nov 20 2021 at 00:05):

lol it's the line 71 column 18 bug in NNG :-) Hit enter a couple of times and sanity will be restored!

Kevin Buzzard (Nov 20 2021 at 00:07):


Kevin Buzzard (Nov 20 2021 at 00:09):

This is a super-obscure bug whereby the actual goal is not correctly printed if the cursor is in a couple of extremely specific places. It is unlikely to ever be fixed in Lean 3 because we're moving to Lean 4 (and even if it was fixed in Lean 3 I'm unlikely to port the fix to NNG...)

Last updated: Dec 20 2023 at 11:08 UTC