From 64bedf4ca9583aa486805cd24450cb60c273bc6d Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 21 Aug 2013 14:46:37 +0200
Subject: [PATCH] Two basic De Morgan like laws for decidable propositions.

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

diff --git a/theories/decidable.v b/theories/decidable.v
index e8dd5172..b61c6e79 100644
--- a/theories/decidable.v
+++ b/theories/decidable.v
@@ -171,3 +171,9 @@ Instance uncurry_dec `(P_dec : ∀ (p : A * B), Decision (P p)) x y :
 Instance sig_eq_dec `(P : A → Prop) `{∀ x, ProofIrrel (P x)}
   `{∀ x y : A, Decision (x = y)} (x y : sig P) : Decision (x = y).
 Proof. refine (cast_if (decide (`x = `y))); by rewrite sig_eq_pi. Defined.
+
+(** Some laws for decidable propositions *)
+Lemma not_and_l {P Q : Prop} `{Decision P} : ¬(P ∧ Q) ↔ ¬P ∨ (¬Q ∧ P).
+Proof. destruct (decide P); tauto. Qed.
+Lemma not_and_r {P Q : Prop} `{Decision Q} : ¬(P ∧ Q) ↔ (¬P ∧ Q) ∨ ¬Q.
+Proof. destruct (decide Q); tauto. Qed.
-- 
GitLab