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

Bug in first two levels of the Power World #104

Closed czAdamV closed 4 years ago

czAdamV commented 4 years ago

The first two levels can be completed using just a single refl without actually proving anything. I found this by accident when I did the following in the second level:

induction m,
rwa[pow_succ, pow_zero, mul_zero],

expecting only the base case to be proved, but finding out the game thinks the entire proof is already completed. It seems the refl tactic proves some goals of the form A = B in those two levels, even if A and B aren't the same thing.

czAdamV commented 4 years ago

Never mind, I just learned that refl is more powerful than described in the game, and this is expected behaviour.