add inverses of bool_decide_{true,false}
Merge request reports
Activity
I don't really like the names of these lemmas, the
_2suggests there's also a_1lemma, and the one without suffix is a biimplication.So, ideally, the names I would you are:
Lemma bool_decide_true (P : Prop) `{Decision P} : bool_decide P = true ↔ P. Lemma bool_decide_true_1 (P : Prop) `{Decision P} : bool_decide P = true → P. Lemma bool_decide_true_2 (P : Prop) `{Decision P} : P → bool_decide P = true. Lemma bool_decide_false (P : Prop) `{Decision P} : bool_decide P = false ↔ ¬P. Lemma bool_decide_false_1 (P : Prop) `{Decision P} : bool_decide P = false → ¬P. Lemma bool_decide_false_2 (P : Prop) `{Decision P} : ¬P → bool_decide P = false.The problem is this change is not backwards compatible. So, if we wish to keep backwards compatibility, maybe we should add the above set of lemmas with some other prefix than
bool_decide_{true,false}and keepbool_decide_{true,false}for backwards compatibility reasons?Edited by Robbert Krebbers
I don't really like the names of these lemmas, the
_2suggests there's also a_1lemma, and the one without suffix is a biimplication.Agreed. I used
bool_decide_true'first, but that didn't feel right either.maybe we should add the above set of lemmas with some other prefix than
bool_decide_{true,false}and keepbool_decide_{true,false}for backwards compatibility reasons?bool_decide_eq_{true,false}?mentioned in commit 02687b13
