A basic Boolean algebra written in Agda, supporting all typical logic gates plus converse implication, equality, and order relations.

BooleanAlgebra.agda

-- define boolean class
data Boolean : Set where
  true false : Boolean

{-
  truth table
                                                                      (a.k.a xnor)
  false | A and B | A < B | B | A > B | A | A xor B | A or B | A nor B | A == B | not A | A imply B | not B | A con B | A nand B | true 
  ------|---------|-------|---|-------|---|---------|--------|---------|--------|-------|-----------|-------|---------|----------|------
    0   |    0    |   0   | 0 |   0   | 0 |    0    |    0   |    1    |    1   |   1   |     1     |   1   |    1    |     1    |   1  
    0   |    0    |   0   | 0 |   1   | 1 |    1    |    1   |    0    |    0   |   0   |     0     |   1   |    1    |     1    |   1  
    0   |    0    |   1   | 1 |   0   | 0 |    1    |    1   |    0    |    0   |   1   |     1     |   0   |    0    |     1    |   1  
    0   |    1    |   0   | 1 |   0   | 1 |    0    |    1   |    0    |    1   |   0   |     1     |   0   |    1    |     0    |   1   
-}

-- nand is complete and is used to derive all other logic gates
_nand_ : Boolean -> Boolean -> Boolean
true nand true = false
_ nand _ = true

-- nand derives not
not_ : Boolean -> Boolean
not x = x nand x

-- not, nand derives and
_and_ : Boolean -> Boolean -> Boolean
x and y = not (x nand y)

-- not, nand derives or
_or_ : Boolean -> Boolean -> Boolean
x or y = (x nand y) and ((not x) nand (not y))

-- not, or derives nor
_nor_ : Boolean -> Boolean -> Boolean
x nor y = not (x or y)

-- not, or derives imply
_imply_ : Boolean -> Boolean -> Boolean
x imply y = (not x) or y

-- not, or derives converse imply
_con_ : Boolean -> Boolean -> Boolean
x con y = x or (not y)

-- nand, and, or derives xor
_xor_ : Boolean -> Boolean -> Boolean
x xor y = (x or y) and (x nand y)

-- not, xor derives equality relation
_==_ : Boolean -> Boolean -> Boolean
x == y = not (x xor y)

-- not, imply derives greater-than order relation
_>_ : Boolean -> Boolean -> Boolean
x > y = not (x imply y)

-- not, converse imply derives less-than order relation
_<_ : Boolean -> Boolean -> Boolean
x < y = not (x con y)