`rewrite decide_True` does not work with ssreflect rewritintg
Code says it all:
Lemma bar : (if decide (0 = 0) then 0 else 0) = 0.
Proof.
Succeed by rewrite ->decide_True.
Fail rewrite decide_True.
[...]
Because of issues like this, @msammler @Blaisorblade and me now have a general suspicion against decide
and prefer bool_decide
wherever possible.
With bool_decide P
one cannot do destruct
and get a proof of P
/¬P
, but the case_bool_decide
tactic handles that situation nicely. I never ran into situations where I wished I would have used decide
instead of bool_decide
. Hypothetically, if there are 2 bool_decide
in the goal, case_bool_decide
does not provide enough control to figure out which one to destruct, but one could imagine a case_bool_deice pat
that pattern-matches P
against pat
to solve this problem.
So that leaves the question:
- Can we fix
rewrite decide_True
? - Should we replace
decide
bybool_decide
entirely / wherever possible, to steer people towards the more reliable option? It is very rare that you actually need the proof term, so arguably the version that returnsbool
should be the default.
Edited by Ralf Jung