Additions to Haskell.Law.Bool

.gitignore

@@ -1,3 +1,4 @@
+# Haskell
 _build
 dist
 dist-newstyle
@@ -7,6 +8,9 @@ docs/build/
 *.hi
 *.o
 
+# Agda
+*.agdai
+
 # For nix users
 .direnv/**
 .envrc

lib/Haskell/Law/Bool.agda

@@ -5,6 +5,184 @@ open import Haskell.Prim.Bool
 
 open import Haskell.Law.Equality
 
+{-----------------------------------------------------------------------------
+    Properties
+    Logical operations and constants
+------------------------------------------------------------------------------}
+--
+prop-x-&&-True
+  : ∀ (x : Bool)
+  → (x && True) ≡ x
+--
+prop-x-&&-True True = refl
+prop-x-&&-True False = refl
+
+--
+prop-x-&&-False
+  : ∀ (x : Bool)
+  → (x && False) ≡ False
+--
+prop-x-&&-False True = refl
+prop-x-&&-False False = refl
+
+--
+prop-x-||-True
+  : ∀ (x : Bool)
+  → (x || True) ≡ True
+--
+prop-x-||-True True = refl
+prop-x-||-True False = refl
+
+--
+prop-x-||-False
+  : ∀ (x : Bool)
+  → (x || False) ≡ x
+--
+prop-x-||-False True = refl
+prop-x-||-False False = refl
+
+{-----------------------------------------------------------------------------
+    Properties
+    Boolean algebra
+    https://en.wikipedia.org/wiki/Boolean_algebra_(structure)
+------------------------------------------------------------------------------}
+--
+prop-||-idem
+  : ∀ (a : Bool)
+  → (a || a) ≡ a
+--
+prop-||-idem False = refl
+prop-||-idem True = refl
+
+--
+prop-||-assoc
+  : ∀ (a b c : Bool)
+  → ((a || b) || c) ≡ (a || (b || c))
+--
+prop-||-assoc False b c = refl
+prop-||-assoc True b c = refl
+
+--
+prop-||-sym
+  : ∀ (a b : Bool)
+  → (a || b) ≡ (b || a)
+--
+prop-||-sym False False = refl
+prop-||-sym False True = refl
+prop-||-sym True False = refl
+prop-||-sym True True = refl
+
+--
+prop-||-absorb
+  : ∀ (a b : Bool)
+  → (a || (a && b)) ≡ a
+--
+prop-||-absorb False b = refl
+prop-||-absorb True b = refl
+
+--
+prop-||-identity
+  : ∀ (a : Bool)
+  → (a || False) ≡ a
+--
+prop-||-identity False = refl
+prop-||-identity True = refl
+
+--
+prop-||-&&-distribute
+  : ∀ (a b c : Bool)
+  → (a || (b && c)) ≡ ((a || b) && (a || c))
+--
+prop-||-&&-distribute False b c = refl
+prop-||-&&-distribute True b c = refl
+
+--
+prop-||-complement
+  : ∀ (a : Bool)
+  → (a || not a) ≡ True
+--
+prop-||-complement False = refl
+prop-||-complement True = refl
+
+--
+prop-&&-idem
+  : ∀ (a : Bool)
+  → (a && a) ≡ a
+--
+prop-&&-idem False = refl
+prop-&&-idem True = refl
+
+--
+prop-&&-assoc
+  : ∀ (a b c : Bool)
+  → ((a && b) && c) ≡ (a && (b && c))
+--
+prop-&&-assoc False b c = refl
+prop-&&-assoc True b c = refl
+
+--
+prop-&&-sym
+  : ∀ (a b : Bool)
+  → (a && b) ≡ (b && a)
+--
+prop-&&-sym False False = refl
+prop-&&-sym False True = refl
+prop-&&-sym True False = refl
+prop-&&-sym True True = refl
+
+--
+prop-&&-absorb
+  : ∀ (a b : Bool)
+  → (a && (a || b)) ≡ a
+--
+prop-&&-absorb False b = refl
+prop-&&-absorb True b = refl
+
+--
+prop-&&-identity
+  : ∀ (a : Bool)
+  → (a && True) ≡ a
+--
+prop-&&-identity False = refl
+prop-&&-identity True = refl
+
+--
+prop-&&-||-distribute
+  : ∀ (a b c : Bool)
+  → (a && (b || c)) ≡ ((a && b) || (a && c))
+--
+prop-&&-||-distribute False b c = refl
+prop-&&-||-distribute True b c = refl
+
+--
+prop-&&-complement
+  : ∀ (a : Bool)
+  → (a && not a) ≡ False
+--
+prop-&&-complement False = refl
+prop-&&-complement True = refl
+
+--
+prop-deMorgan-not-&&
+  : ∀ (a b : Bool)
+  → not (a && b) ≡ (not a || not b)
+--
+prop-deMorgan-not-&& False b = refl
+prop-deMorgan-not-&& True b = refl
+
+--
+prop-deMorgan-not-||
+  : ∀ (a b : Bool)
+  → not (a || b) ≡ (not a && not b)
+--
+prop-deMorgan-not-|| False b = refl
+prop-deMorgan-not-|| True b = refl
+
+{-----------------------------------------------------------------------------
+    Properties
+    Other
+------------------------------------------------------------------------------}
+
 --------------------------------------------------
 -- &&