dk_bool.dk

#REQUIRE cc.

(; Bool ;)
(; Declaration ;)
bool : cc.uT.
Bool : Type.
[] cc.eT bool --> Bool.

(; Constructors ;)
true : Bool.
false : Bool.

(; Pattern-matching ;)
def match :
  P : (Bool -> cc.uT) ->
  cc.eT (P true) ->
  cc.eT (P false) ->
  b : Bool ->
  cc.eT (P b).
[P : Bool -> cc.uT,
 Ht : cc.eT (P true),
 Hf : cc.eT (P false) ]
    match P Ht Hf true --> Ht
[P : Bool -> cc.uT,
 Ht : cc.eT (P true),
 Hf : cc.eT (P false) ]
    match P Ht Hf false --> Hf.

(; Operations ;)
(; polymorphic if .. then .. else .. ;)
def ite :
  A : cc.uT ->
  Bool ->
  cc.eT A ->
  cc.eT A ->
  cc.eT A.
[ A : cc.uT,
  x : cc.eT A,
  y : cc.eT A,
  b : Bool ]
    ite A b x y
      -->
    match (b : Bool => A) x y b.

def match__true :
  Bool ->
  A : cc.uT ->
  cc.eT A ->
  cc.eT A ->
  cc.eT A.
[ A : cc.uT, b : Bool, t : cc.eT A, e : cc.eT A]
    match__true b A t e --> ite A b t e.

def match__false :
  Bool ->
  A : cc.uT ->
  cc.eT A ->
  cc.eT A ->
  cc.eT A.
[ A : cc.uT, b : Bool, t : cc.eT A, e : cc.eT A]
    match__false b A t e --> ite A b e t.

(; boolean if .. then .. else .. ;)
def iteb : Bool -> Bool -> Bool -> Bool
     := ite bool.

(; negation ;)
def not : Bool -> Bool.
[] not true --> false
[] not false --> true
[ b : Bool ] not (not b) --> b.

(; binary operators ;)
def and : Bool -> Bool -> Bool.
[ b : Bool ] and b true --> b
[ b : Bool ] and true b --> b
[ b : Bool ] and b false --> false
[ b : Bool ] and false b --> false.

def or : Bool -> Bool -> Bool.
[ b : Bool ] or b true --> true
[ b : Bool ] or true b --> true
[ b : Bool ] or b false --> b
[ b : Bool ] or false b --> b.

def xor : Bool -> Bool -> Bool.
[ b : Bool ] xor b true --> not b
[ b : Bool ] xor true b --> not b
[ b : Bool ] xor b false --> b
[ b : Bool ] xor false b --> b.

def imp : Bool -> Bool -> Bool.
[ b : Bool ] imp b true --> true
[ b : Bool ] imp true b --> b
[ b : Bool ] imp b false --> not b
[ b : Bool ] imp false b --> true.

def eqv : Bool -> Bool -> Bool.
[ b : Bool ] eqv b true --> b
[ b : Bool ] eqv true b --> b
[ b : Bool ] eqv b false --> not b
[ b : Bool ] eqv false b --> not b.

(; Associativity ;)
[ b1 : Bool, b2 : Bool, b3 : Bool ]
    and b1 (and b2 b3) --> and (and b1 b2) b3.
[ b1 : Bool, b2 : Bool, b3 : Bool ]
    or b1 (or b2 b3) --> or (or b1 b2) b3.
[ b1 : Bool, b2 : Bool, b3 : Bool ]
    xor b1 (xor b2 b3) --> xor (xor b1 b2) b3.

(; Distributivity ;)
[ b1 : Bool, b2 : Bool, b3 : Bool ]
    and b1 (or b2 b3) --> or (and b1 b2) (and b1 b3).
[ b1 : Bool, b2 : Bool, b3 : Bool ]
    and (or b1 b2) b3 --> or (and b1 b3) (and b2 b3).

[ b1 : Bool, b2 : Bool ]
    not (and b1 b2) --> or (not b1) (not b2).
[ b1 : Bool, b2 : Bool ]
    not (or b1 b2) --> and (not b1) (not b2).
[ b1 : Bool, b2 : Bool ]
    not (xor b1 b2) --> eqv (not b1) (not b2).
[ b1 : Bool, b2 : Bool ]
    not (eqv b1 b2) --> xor (not b1) (not b2).