From 8d590fb25f47cf1538e5e2d04df24bb4a7f8764a Mon Sep 17 00:00:00 2001
From: Denis Buzdalov <public@buzden.ru>
Date: Mon, 2 Dec 2019 01:09:57 +0300
Subject: [PATCH 1/3] Double not disappearing property was added for `Bool`s.

---
 libs/prelude/Prelude/Bool.idr | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/libs/prelude/Prelude/Bool.idr b/libs/prelude/Prelude/Bool.idr
index c5bda68f17..212ab5a980 100644
--- a/libs/prelude/Prelude/Bool.idr
+++ b/libs/prelude/Prelude/Bool.idr
@@ -45,3 +45,9 @@ Uninhabited (True = False) where
 
 Uninhabited (False = True) where
   uninhabited Refl impossible
+
+-- Not
+
+total doubleNotDisappears : (b : Bool) -> not (not b) = b
+doubleNotDisappears True  = Refl
+doubleNotDisappears False = Refl

From 503b590801de512f44537085fe4262294f77c831 Mon Sep 17 00:00:00 2001
From: Denis Buzdalov <public@buzden.ru>
Date: Mon, 2 Dec 2019 01:52:25 +0300
Subject: [PATCH 2/3] Conjunction and disjunction properties were added.

---
 libs/prelude/Prelude/Bool.idr | 52 +++++++++++++++++++++++++++++++++++
 1 file changed, 52 insertions(+)

diff --git a/libs/prelude/Prelude/Bool.idr b/libs/prelude/Prelude/Bool.idr
index 212ab5a980..abd6b6c6bf 100644
--- a/libs/prelude/Prelude/Bool.idr
+++ b/libs/prelude/Prelude/Bool.idr
@@ -51,3 +51,55 @@ Uninhabited (False = True) where
 total doubleNotDisappears : (b : Bool) -> not (not b) = b
 doubleNotDisappears True  = Refl
 doubleNotDisappears False = Refl
+
+-- Conjunction
+
+total conjTrueRightNeutral : (b : Bool) -> b && True = b
+conjTrueRightNeutral False = Refl
+conjTrueRightNeutral True  = Refl
+
+total conjTrueLeftNeutral : (b : Bool) -> True && b = b
+conjTrueLeftNeutral _ = Refl
+
+total conjFalseRightAbsorbs : (b : Bool) -> b && False = False
+conjFalseRightAbsorbs False = Refl
+conjFalseRightAbsorbs True  = Refl
+
+total conjFalseLeftAbsorbs : (b : Bool) -> False && b = False
+conjFalseLeftAbsorbs _ = Refl
+
+total conjCommutative : (b : Bool) -> (c : Bool) -> b && c = c && b
+conjCommutative False False = Refl
+conjCommutative False True  = Refl
+conjCommutative True  False = Refl
+conjCommutative True  True  = Refl
+
+total conjNotFalse : (b : Bool) -> b && not b = False
+conjNotFalse False = Refl
+conjNotFalse True  = Refl
+
+-- Disjunction
+
+total disjFalseRightNeutral : (b : Bool) -> b || False = b
+disjFalseRightNeutral False = Refl
+disjFalseRightNeutral True  = Refl
+
+total disjFalseLeftNeutral : (b : Bool) -> False || b = b
+disjFalseLeftNeutral _ = Refl
+
+total disjTrueRightAbsorbs : (b : Bool) -> b || True = True
+disjTrueRightAbsorbs False = Refl
+disjTrueRightAbsorbs True  = Refl
+
+total disjTrueLeftAbsorbs : (b : Bool) -> True || b = True
+disjTrueLeftAbsorbs _ = Refl
+
+total disjCommutative : (b : Bool) -> (c : Bool) -> b || c = c || b
+disjCommutative False False = Refl
+disjCommutative False True  = Refl
+disjCommutative True  False = Refl
+disjCommutative True  True  = Refl
+
+total disjNotTrue : (b : Bool) -> b || not b = True
+disjNotTrue False = Refl
+disjNotTrue True  = Refl

From 660cba72620926255aa2f5783e0a84849ffa9dc6 Mon Sep 17 00:00:00 2001
From: Denis Buzdalov <public@buzden.ru>
Date: Mon, 2 Dec 2019 02:34:15 +0300
Subject: [PATCH 3/3] De Morgan's laws were added as `Bool`'s properties.

---
 libs/prelude/Prelude/Bool.idr | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/libs/prelude/Prelude/Bool.idr b/libs/prelude/Prelude/Bool.idr
index abd6b6c6bf..88bf243941 100644
--- a/libs/prelude/Prelude/Bool.idr
+++ b/libs/prelude/Prelude/Bool.idr
@@ -103,3 +103,13 @@ disjCommutative True  True  = Refl
 total disjNotTrue : (b : Bool) -> b || not b = True
 disjNotTrue False = Refl
 disjNotTrue True  = Refl
+
+-- De Morgan's Laws
+
+total conjDeMorgan : (b : Bool) -> (c : Bool) -> not (b && c) = not b || not c
+conjDeMorgan False _ = Refl
+conjDeMorgan True  _ = Refl
+
+total disjDeMorgan : (b : Bool) -> (c : Bool) -> not (b || c) = not b && not c
+disjDeMorgan False _ = Refl
+disjDeMorgan True  _ = Refl