From 516090f6084dcbc8a276dfe8f46b3787db4665ff Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 6 Dec 2021 15:09:41 -0500
Subject: [PATCH] swap lemma directions and adjust names; add and/or versions

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

diff --git a/theories/decidable.v b/theories/decidable.v
index f149b0b2..c3d94f5f 100644
--- a/theories/decidable.v
+++ b/theories/decidable.v
@@ -192,8 +192,6 @@ 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_negb P `{Decision P} : negb (bool_decide P) = bool_decide (not P).
-Proof. repeat case_bool_decide; intuition. Qed.
 
 Lemma bool_decide_eq_true_1 P `{!Decision P}: bool_decide P = true → P.
 Proof. apply bool_decide_eq_true. Qed.
@@ -205,6 +203,16 @@ 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_not P `{Decision P} :
+  bool_decide (¬ P) = negb (bool_decide P).
+Proof. repeat case_bool_decide; intuition. Qed.
+Lemma bool_decide_or 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_and P Q `{Decision P, Decision Q} :
+  bool_decide (P ∧ Q) = 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.
 - Goals that compute to [True] or [x = x].
-- 
GitLab