search

leanprover-community / lean4game

Server to host lean games.
https://adam.math.hhu.de
GNU General Public License v3.0
199 stars 35 forks source link

Statement used to prove itself #117

Closed joneugster closed 1 year ago

joneugster commented 1 year ago

There are at least two issues concerning structural recursion of exercises:

  1. Once a statement is proven, it can be used in previous levels. E.g. proof add_comm then go back two levels and now you can use add_comm to proof e.g. zero_mul. Is the (only?) solution to disable the storage of "known theorems" in local storage?
  2. One should never be able to do any such structural recursive proofs. Usually, Lean would catch this, but the way we proof a new statement with everything imported makes this very hard to check, I believe.
joneugster commented 1 year ago

Partially fixed: we check now that a theorem cannot be used to prove itself.

You can still do trickery like proving add_comm using zero_add and then reproving zero_add using add_comm. Closing this latter issue as "wont fix"