fix multiple hint display using strict hints#129
Conversation
| " | ||
| -/ | ||
| Hint "It is clear which `b` can be used. Start with `use …` and continue with `lt_trichotomy` e.g. | ||
| Hint (strict := true) "It is clear which `b` can be used. Start with `use …` and continue with `lt_trichotomy` e.g. |
There was a problem hiding this comment.
Why is strict necessary here? Surely use will change the goal?
There was a problem hiding this comment.
i think i took a slightly different path in the proof which led to this hint appearing twice , ill look into this
There was a problem hiding this comment.
what i did to solve the level is first do obtain then do use which is why I saw the hint multiple times for every case.
I don't think it would hurt to mark as strict , the point of this hint is to appear and be read one anyways. If you wish to remove strict then I won't contest that and would remove it
There was a problem hiding this comment.
Sorry for taking a while to get back to you. I can see how the hint gets doubled in your solution:
obtain h | h | h := lt_trichotomy a c
use (a + c) / 2
left
constructor
linarith
linarith
…The initial hint appears a second time when the first subgoal created by have gets closed. But I don't understand why this is the case. The intended behaviour of Hints is documented very clearly, and states in particular that:
[…] identical (non-hidden) hints which where already present in the step before are omitted.
It would be super helpful if you could narrow down and replicate this behaviour. Can you come up with a "minimal non-working example" that shows how the actual behaviour is in conflict with the documented behaviour?
I would like to sort this out first before making any changes to the game.
There was a problem hiding this comment.
No need to apologize for late responses , I sometimes respond late as well.
However from my perspective, I thought this was normal i.e a hint before have then invoking have changing the goal and then when that secondary goal is closed and the proof state returns to the original goal then the same hint would appear again. I thought this was normal and it's been a habit of mine to add strict for these kinds of hints even without testing for my own game.
The above were my initial thoughts , I'll look into this more deeply and review my assumptions regarding how hints are supposed to work by reading the current version of the docs more carefully.
There was a problem hiding this comment.
It would be super helpful if you could narrow down and replicate this behaviour. Can you come up with a "minimal non-working example" that shows how the actual behaviour is in conflict with the documented behaviour?
Here are two examples which are the most minimal and much more simple than the hint in the game we were discussing:
Statement
: 2 = 2 := by
/-
if the user does `have : 1=1`(or any other subgoal)
then closes that subgoal , this hint would appear again
-/
Hint
"
use rfl
"
rfl
Statement
: 2 = 2 := by
/-
a hint instructing the user to use have , the user complies
and proves the subgoal. after that the hint appears again
-/
Hint
"
prove the subgoal 1=1 using have then close the goal
"
have : 1=1
rfl
rfl
Concerning the documentation and specifically when do hints show?,
If you read the first paragraph on its own
"
A hint will be displayed if the player's goal matches the one where the hint was placed in the sample solutions and the entire context from the sample solutions is present in the player's context. The player's context may contain additional items.
"
then the behavior displayed in the examples and in your last comment is normal.
Regarding the second paragraph,
"
This means if you have multiple identical subgoals, you should only place a single hint in one of them, and it will be displayed in all of them.
"
I think its misleading to emphasize 'subgoal' here because as far as I know the mechanism for displaying hints doesn't distinguish between the 'main goal' and 'subgoals' , it only sees the current goal and the type of that goal.
Regardless,
The second paragraph would suggest that for the given example
Statement
: 2 = 2 := by
Hint
"
triggering before have
"
have : 1=1
Hint
"
subgoal 1 eq 1 hint
"
rfl
rfl
and the user doing the following solution
have : 1=1
rfl
have : 1=1
rfl
rfl
then the hint "subgoal 1 eq 1 hint" would appear each time have is used(which is the case).
However, I think it suggests more than that. For the above example , it suggests that whenever the engine sees that the goal is 1=1 it would trigger the hint. This reasoning would apply to the hint before have as well placed for the 'main' goal `2=2.(which is the behavior you pointed out to be a bug/not intended)
The second paragraph from the above point of view would contradict the third paragraph,
"
However, identical (non-hidden) hints which where already present in the step before are omitted. This is to allow a player to add new assumptions to context, for example with have, without seeing the same hint over and over again. Hidden hints are not filtered.
"
I think that the third paragraph does not accurately describe how hints work.
From my perspective , the next thing to do is to remove the third paragraph and move on. But you're saying that this is behavior is a bug/not the intended behavior.
There was a problem hiding this comment.
Thanks! This is indeed very helpful. I think we agree on the analysis now, just that I would call it a bug rather than a misdocumentation. See leanprover-community/lean4game#532. Let's return here once that is resolved.
| -- Hint "**Du**: Aha. Eine Primzahl ist also eine natürlich Zahl größergleich `2`, die nur durch | ||
| -- `1` und sich selbst teilbar ist. Das klingt vertraut." | ||
| Hint "A prime number is a natural number greater or equal to `2`, which is only divisible by `1` | ||
| Hint (strict := true) "A prime number is a natural number greater or equal to `2`, which is only divisible by `1` |
There was a problem hiding this comment.
Again, unsure why strict would be needed here. The way obtain is used here, the hypothesis hp should disappear from the proof state.
There was a problem hiding this comment.
here's my solution
rw [prime_def] at hp
have := hp.right a ha
obtain this | this := this
rw [this] at h
contradiction
after contradiction the hint appears again.
non strict hints don't trigger based on the environment but based only on the goal , so what you mentioned regarding the hypothesis hp disappearing after using obtain is only relevant when using strict
There was a problem hiding this comment.
from the docs
"
If you use the attribute (strict := true) a hint is only shown if the entire context matches exactly the one where the hint is placed. With (strict := false), which is the default, it does not matter if additional assumptions are present in the player's context.
"
i guess the docs only mention additional assumptions , but this seems to hold true also for when an assumption is "consumed"
There was a problem hiding this comment.
As above, the docs are very clear on this. If an assumption is missing, Hints certainly should not trigger. If they do, it's a bug that we need to investigate.
There was a problem hiding this comment.
i found an alternative solution where the hint wouldn't appear twice
rw [prime_def] at hp
have := hp.right a ha
obtain this | this := this
omega
assumption
Co-authored-by: Marcus Zibrowius <marcus.zibrowius@cantab.net>
Co-authored-by: Marcus Zibrowius <marcus.zibrowius@cantab.net>
2 participants
No description provided.