help for Lean beginners in natural number game

Stream: new members

[Neil Immerman]

Dear Lean Experts,

Hi. I have a strong background in logic and theoretical computer science,
but I am new to Lean. I have been going through the Natural Number Game
and I have some questions. In particular I am here:
https://adam.math.hhu.de/#/g/leanprover-community/nng4/world/Multiplication/level/3,
i.e., level 3 out of 9 in the Multiplication World.

Our goal is to prove succ_mul which I write as ∀a b:N (succ a) * b = a * b + b)

Lean writes Goal: succ a * b = a*b + b

Now we already know the following two facts:

mul_succ: ∀x y:N (x * succ y = x * y + x)
mul_comm: ∀x y:N (x * y = y * x)

So it seems to me that this should be pretty straight forward.
The first thing I tried was "rw [mul_comm]" As I understand it,
this means match the first occurrence of x * y and replace it with y * x, right?

So this should have let x be succ a and y be b and thus the new
Goal would be b * succ a = a*b + b.

However Lean said no, this tactic failed. Why?

Furthermore, if it couldn't match x * y with succ a * b, then
surely it should have been able to match x * y with a*b. Why didn't
it do that.

What am I missing? Is there something I can read about how Lean chooses
to unify terms to do its substitutions?

Thanks for your help.

Best,
-- Neil

[Mark Fischer]

Could be a bug!

@Jon Eugster

I don't have mul_comm by that level, but if I unlock it I wind up with the mul_comm from Mathlib.Algebra.Group and

failed to synthesize instance
  CommMagma ℕ

if I try MyNat.mul_comm, then I get

unknown constant 'MyNat.mul_comm'

So I think there's something wrong with NNG4.

[Mark Fischer]

Neil Immerman said:

As I understand it,
this means match the first occurrence of x * y and replace it with y * x, right?

So this should have let x be succ a and y be b and thus the new
Goal would be b * succ a = a*b + b.

That's mostly right. This is what I get if I do this outside NNG4.

Instead of the first occurrence rw will actually replace every occurrence. Though perhaps a bit confusingly, if rw gets a proof like b → c = d, it will try to infer a value for b, then replace every occurrence of c with d.

In this case, either rw [mul_comm (succ a) b] or rw [mul_comm a b] would have worked, but lean chooses the first one. In either case, it would have re-written every occurrence if there were more than one.

[Yaël Dillies]

Dear Neil, nice seeing you here! I am reading your book at the moment.

[Yaël Dillies]

I agree with Treq's diagnosis. Something is up with NNG here.

[Jon Eugster]

Here's my 30sec diagnosis from my phone so that might be wrong. I'll look at it tomorrow in details.

If I play around a bit with mul_comm I get

failed to synthesize instance CommMagma ℕ

which makes me believe that mul_comm is in fact some statement from mathlib and not MyNat.mul_comm (note that ℕ means MyNat in the nng and not lean's Nat). And since the game uses MyNat instead of Nat it fails to find some some instances to use this mul_comm which applies to an arbitrary (comm.) magma.

I'll see if the NNG needs to be tweaked somehow to not import this mul_comm there, alternatively it might need to either add some instances to MyNat or disable the theorem until MyNat.mul_comm is defined and takes higher priority.

Btw Neil, some #backticks make your message much more readable:blush:

[Jon Eugster]

(oh and I didnt read Treq's message at all🤦🏻‍♂️:sweat_smile:)

[Kevin Buzzard]

I am a bit confused about Neil's claim that we "already know mul_comm" -- that theorem is level 4 and you're on level 3. So sure something's wrong but it doesn't surprise me at all that you can't get mul_comm to work; in some sense that should be a reasonable explanation of what's wrong. The issue is that the error message is bad.

[Jon Eugster]

Indeed, Im just a bit afraid that we might not be able to get rid of mathlibs mul_comm because it's not in any namespace but probably imported by some low-level tactic we're using.

[Kevin Buzzard]

I guess this adds more weight to the idea that mathlib stuff should be put in a mathlib namespace

[Jon Eugster]

I now pushed the updated game where we just removed a lot of mathlib tactics to avoid importing Mathlib.Algebra.Group.Defs.

That means now it should rather say "unknown identifier mul_comm" (or the obstruse rw-error message if one tries rw [nonexisting])

I haven't tested it completely, so lets see if anybody finds a tactic that's now missing or missfunctional because it was modified in mathlib...

[Kevin Buzzard]

Oh wow, I had not realised that my cavalier attitude of import tactic was the root cause of the problems! Many thanks!

[Kevin Buzzard]

Did you deploy? (I don't know how to tell). I'll find the time to play through the game after I've got this pile of marking off my desk

[Jon Eugster]

Yes I deployed (there's no good way for you to tell yet, but I guess redeploying is also not hurtfull)

well that works until you decide that it would be good to reintroduce ring to the game. Then we'd need to think about something different

[Kevin Buzzard]

If ring causes more problems than it solves then I'm happy to leave it out.