search

ImperialCollegeLondon / natural_number_game

Building the natural numbers in Lean 3. The original natural number game, now frozen. See README for Lean 4 information.
Apache License 2.0
292 stars 73 forks source link

nat versus mynat issue with literal zeros #74

Closed gjm11 closed 4 years ago

gjm11 commented 4 years ago

(I am a total newb so there may be wrong assumptions etc. baked into this bug report.)

I'm looking at Advanced Multiplication level 1. For some reason my browser forgot stuff when I last restarted my computer, so I haven't (in this session) actually done any earlier levels, but e.g. all the necessary tactics and theorems are present in the left sidebar.

I do

intro a0,
intro b0,
cases a with n,

so now I have to get a contradiction out of 0 ≠ 0. Obviously I can do that by introducing a new goal 0 = 0 and proving it with refl, right?

have zz : 0=0,
refl,
exfalso,

... so far so good ...

exact a0(zz)

but now I get

type mismatch at application
  a0 zz
term
  zz
has type
  @eq nat 0 0
but is expected to have type
  @eq mynat 0 0

This goes away if I explicitly say have zz : (0:mynat)=(0:mynat) but I don't think players are supposed to have to do that.

May be related to #1?

kbuzzard commented 4 years ago

I think there's nothing i can do about this. If you start talking about 0 without saying what its type is then Lean by default assumes that it is 0 : nat, which is Lean's inbuilt naturals. I'm not sure this can be fixed without changes to core Lean which I am not competent to make.

PS I knew someone whose email address was gjm11@something 30 years ago...

gjm11 commented 4 years ago

Hmm, that's a shame. I wonder whether there's a way to identify that this might be happening and give a friendly warning message suggesting what the user ought to be doing instead.

(And yes, same gjm11.)