feat: detailed feedback on decide tactic failure
#4674
Conversation
When the `decide` tactic fails, it can try to give hints about the failure: - It tells you which `Decidable` instances it unfolded, by making use of the diagnostics feature. - If it encounters `Eq.rec`, it gives you a hint that one of these instances was likely defined using tactics. - If it encounters `Classical.choice`, it hints that you might have classical instances in scope. This idea comes from discussion with Heather Macbeth [on Zulip](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Decidable.20with.20structures/near/449409870).
github-actions
bot
added
the
toolchain-available
|
Mathlib CI status (docs):
|
|
@david-christiansen Would you mind taking a look at the wordings of the error messages in the test files? One thing that might be confusing is that the expression it reports as being to blame might not be the original instance — that's by design since we want to diagnose where whnf got stuck. We can't use the word "subexpression" here because it's only a subexpression after enough reduction. Instead, I went for being slightly vague with the phrase "reduction got stuck at". |
tests/lean/run/decideTactic.lean
Outdated
| Hint: Reduction got stuck on '▸' (Eq.rec), which suggests that one of the decidability instances is | ||
| defined using tactics such as 'rw' or 'simp'. Use definitions such as inferInstanceAs or | ||
| decidable_of_decidable_of_iff to alter a proposition. |
There was a problem hiding this comment.
| Hint: Reduction got stuck on '▸' (Eq.rec), which suggests that one of the decidability instances is | |
| defined using tactics such as 'rw' or 'simp'. Use definitions such as inferInstanceAs or | |
| decidable_of_decidable_of_iff to alter a proposition. | |
| Hint: Reduction got stuck on '▸' (Eq.rec), which suggests that one of the 'Decidable' instances is | |
| defined using tactics such as 'rw' or 'simp'. Instead of these tactics, use functions such as 'inferInstanceAs' or | |
| 'decidable_of_decidable_of_iff' to alter a proposition. |
I'm not too happy with the term "function" here, but I think it's better than "definitions" (as the definition is not what's being used, really). Perhaps "operator"?
Thanks for being careful about making them all clickable :)
There was a problem hiding this comment.
How about "declarations"? Something I want to be clear about here is that these are plain old definitions that you could have written yourself, and I worry that "operator" would suggest that they're in a special category of their own.
If "declaration" is no good, "function" works too.
There was a problem hiding this comment.
For me, "declaration" and "definition" have the same downside: a declaration/definition is that which results in a name being given a meaning, but not the name nor the meaning itself. User's aren't expected to stick def ... here, they're expected to invoke something that was previously defined.
This is indeed a bit nitpicky, and I think the risk of someone being misled is fairly low.
"function", then?
There was a problem hiding this comment.
Imagine if these were theorems instead of definitions. Would you have the same objection to "Instead of these tactics, use theorems such as 'thm1' or 'thm2'"? Definitions and theorems are fundamental notions that we need to refer to somehow (both of which are kind of declarations).
Is the analogy "definition is to function/constant as theorem is to theorem"?
|
I have only nitpicks. This is a great improvement! |
| 'Nat.decEq', reduction got stuck at the 'Decidable' instance | ||
| match h : (((mul 4 1).mul 1).mul 1).num.beq 4 with | ||
| | true => isTrue ⋯ | ||
| | false => isFalse ⋯ |
There was a problem hiding this comment.
Possible future addition: add another "Hint" covering this situation (one of the definitions is marked as irreducible)?
There was a problem hiding this comment.
It would be nice to have a more general system to diagnose reduction issues! Right now, I'm a little worried that this reduction blamer might mis-blame match discriminants. At least every Decidable instance that appears should be reducible, so it should be harmless. With arbitrary discriminants, there's more risk of being wrong, unless perhaps we report each discriminant that doesn't reduce to a constructor.
(Somewhat related, today on Zulip I was thinking about this problem for diagnosing type mismatches. It's a bit different, since it's for isDefEq, but isDefEq depends on whnf.)
leanprover-community-mathlib4-bot
added
the
builds-mathlib
When the
decidetactic fails, it can try to give hints about the failure:Decidableinstances it unfolded, by making use of the diagnostics feature.Eq.rec, it gives you a hint that one of these instances was likely defined using tactics.Classical.choice, it hints that you might have classical instances in scope.Decidable.recs and matchers to pin blame on a particular instance that failed to reduce.This idea comes from discussion with Heather Macbeth on Zulip.