From ee01b088774638f58c763cb164f338ab50d5af54 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 7 Dec 2021 12:18:48 +0100
Subject: [PATCH] Add more properties of `bool_decide` w.r.t. logical
 connectives.

---
 theories/decidable.v | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/theories/decidable.v b/theories/decidable.v
index eb93b48f..39ccc1b4 100644
--- a/theories/decidable.v
+++ b/theories/decidable.v
@@ -203,6 +203,10 @@ 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.
 
+Lemma bool_decide_True : bool_decide True = true.
+Proof. reflexivity. Qed.
+Lemma bool_decide_False : bool_decide False = false.
+Proof. reflexivity. Qed.
 Lemma bool_decide_not P `{Decision P} :
   bool_decide (¬ P) = negb (bool_decide P).
 Proof. repeat case_bool_decide; intuition. Qed.
@@ -212,6 +216,12 @@ Proof. repeat case_bool_decide; intuition. Qed.
 Lemma bool_decide_and P Q `{Decision P, Decision Q} :
   bool_decide (P ∧ Q) = bool_decide P && bool_decide Q.
 Proof. repeat case_bool_decide; intuition. Qed.
+Lemma bool_decide_impl P Q `{Decision P, Decision Q} :
+  bool_decide (P → Q) = implb (bool_decide P) (bool_decide Q).
+Proof. repeat case_bool_decide; intuition. Qed.
+Lemma bool_decide_iff P Q `{Decision P, Decision Q} :
+  bool_decide (P ↔ Q) = eqb (bool_decide P) (bool_decide Q).
+Proof. repeat case_bool_decide; intuition. Qed.
 
 (** The tactic [compute_done] solves the following kinds of goals:
 - Goals [P] where [Decidable P] can be derived.
-- 
GitLab