search

leanprover-community / NNG4

Natural Number Game
https://adam.math.hhu.de
Apache License 2.0
85 stars 31 forks source link

"takes longer" #58

Closed jariji closed 3 months ago

jariji commented 3 months ago

https://github.com/leanprover-community/NNG4/blob/18e0aec41dc63b71c774a40fbb551cedd7b209dc/Game/Levels/Multiplication/L07mul_add.lean#L49-L56

induction b with b hb
rw [zero_add, mul_zero, zero_add]
rfl
rw [succ_add, mul_succ, mul_succ, add_right_comm, hb]
rfl

Doesn't seem to take longer.

joneugster commented 3 months ago

changed to "might take longer".

I think in a historic version not all of the reversed statements (zero_add, etc.) or add_right_comm might have not been available. The pedagogical thought here was that one should always start induction on the last variable because + is defined inductively on the second variable.