From 3db8e2f720b4733427d306d8660122d17b4b4c14 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sun, 30 Jun 2019 20:12:36 +0200
Subject: [PATCH] add invserses of bool_decide_{true,false}

---
 theories/decidable.v | 23 +++++++++++++++++++----
 1 file changed, 19 insertions(+), 4 deletions(-)

diff --git a/theories/decidable.v b/theories/decidable.v
index 42b5b615..925a6b86 100644
--- a/theories/decidable.v
+++ b/theories/decidable.v
@@ -112,14 +112,29 @@ Proof. rewrite bool_decide_spec; trivial. Qed.
 Lemma bool_decide_pack (P : Prop) {dec : Decision P} : P → bool_decide P.
 Proof. rewrite bool_decide_spec; trivial. Qed.
 Hint Resolve bool_decide_pack : core.
-Lemma bool_decide_true (P : Prop) `{Decision P} : P → bool_decide P = true.
-Proof. case_bool_decide; tauto. Qed.
-Lemma bool_decide_false (P : Prop) `{Decision P} : ¬P → bool_decide P = false.
-Proof. case_bool_decide; tauto. Qed.
+
+Lemma bool_decide_eq_true (P : Prop) `{Decision P} : bool_decide P = true ↔ P.
+Proof. case_bool_decide; intuition discriminate. Qed.
+Lemma bool_decide_eq_false (P : Prop) `{Decision P} : bool_decide P = false ↔ ¬P.
+Proof. case_bool_decide; intuition discriminate. Qed.
 Lemma bool_decide_iff (P Q : Prop) `{Decision P, Decision Q} :
   (P ↔ Q) → bool_decide P = bool_decide Q.
 Proof. repeat case_bool_decide; tauto. Qed.
 
+Lemma bool_decide_eq_true_1 P `{!Decision P}: bool_decide P = true → P.
+Proof. apply bool_decide_eq_true. Qed.
+Lemma bool_decide_eq_true_2 P `{!Decision P}: P → bool_decide P = true.
+Proof. apply bool_decide_eq_true. Qed.
+
+Lemma bool_decide_eq_false_1 P `{!Decision P}: bool_decide P = false → ¬P.
+Proof. apply bool_decide_eq_false. Qed.
+Lemma bool_decide_eq_false_2 P `{!Decision P}: ¬P → bool_decide P = false.
+Proof. apply bool_decide_eq_false. Qed.
+
+(** Backwards compatibility notations. *)
+Notation bool_decide_true := bool_decide_eq_true_2.
+Notation bool_decide_false := bool_decide_eq_false_2.
+
 (** * Decidable Sigma types *)
 (** Leibniz equality on Sigma types requires the equipped proofs to be
 equal as Coq does not support proof irrelevance. For decidable we
-- 
GitLab