search

djvelleman / STG4

Set Theory Game
7 stars 8 forks source link

'apply' not shown as available in level 6/6 in world 1 #6

Closed 9s-l-s9 closed 9 months ago

9s-l-s9 commented 9 months ago

As the title says, the apply tactic is not shown to be available (greyed out) but is needed to solve the problem. (if it is not needed the user should also not be able to use it)

djvelleman commented 9 months ago

No, the apply tactic is not needed for this level. You should start by introducing an arbitrary object x : U and the assumption h3 : x ∈ A. Once you do that, you get a hint asking if your situation reminds you of a previous level. In fact, the situation now is exactly the same as level 3. In level 3, the hints suggested a two-step proof, using have in the first step and exact in the second step. There is no need for apply.

9s-l-s9 commented 9 months ago

Thanks for the explanation. In that case, the locked tactics (like apply in this case) should not be available.

It seems this is a bug on the side of the game engine, referenced in this issue as well: leanprover-community/lean4game#176

So we can close the issue here :)

joneugster commented 9 months ago

Testing with my local copy of the game engine and a local copy of STG4 (bumped to v4.4.0) it blocks apply correctly. I'm going to assume this is a problem that will be fixed when the updated versions are live.