Booleans

Similarly, we can declare the Bool type for booleans:

type Bool {
 true
 false
}

We are declaring our own booleans just to demonstrate how to do everything from scratch. Kind has its own default implementation of booleans in the standard package (Wikind), along with many other structures and proofs.

In fact, at the time of writing, you need to be working within the Wikind folder to do proofs and the theorem resolution utilities are not built-in.

Functions that operate on booleans are defined in the same way as seen earlier:

// Negação lógica
Notb (b: Bool) : Bool
Notb Bool.true  = Bool.false
Notb Bool.false = Bool.true

// E lógico
Andb (b1: Bool) (b2: Bool) : Bool
Andb Bool.true  b2 = b2
Andb Bool.false b2 = Bool.false

// OU lógico
Orb (b1: Bool) (b2: Bool) : Bool
Orb Bool.true  b2 = Bool.true
Orb Bool.false b2 = b2

The last two functions demonstrate the syntax of Kind for multi-argument functions, and also show that it is possible to pattern match only on some of the variables of the function, not necessarily all.

The cases of the last function can be exhaustively tested (all possibilities) as shown below, creating the truth table of the logical operation.

TestOrb1 : Equal Bool (Orb Bool.true Bool.false) Bool.true
TestOrb1 = Equal.refl

TestOrb2 : Equal Bool (Orb Bool.false Bool.false) Bool.false
TestOrb2 = Equal.refl

TestOrb3 : Equal Bool (Orb Bool.false Bool.true) Bool.true
TestOrb3 = Equal.refl

TestOrb4 : Equal Bool (Orb Bool.true Bool.true) Bool.true
TestOrb4 = Equal.refl

Nandb

Replace the hole "?", completing the following function;

then check if it is correct using the following statements (Analogous to how it was done for the Orb function). The function returns Bool.true if any of its inputs is Bool.false.

Nandb (b1: Bool) (b2: Bool) : Bool
Nandb b1 b2 = ?

Test_nandb1 : Equal Bool (Nandb Bool.true Bool.false) Bool.true
Test_nandb1 = ?

Test_nandb2 : Equal Bool (Nandb Bool.false Bool.false) Bool.true
Test_nandb2 = ?

Test_nandb3 : Equal Bool (Nandb Bool.false Bool.true) Bool.true
Test_nandb3 = ?

Test_nandb4 : Equal Bool (Nandb Bool.true Bool.true) Bool.false
Test_nandb4 = ?

And3

Do the same for the Andb3 function below. This function should return Bool.true if all inputs are Bool.true, and Bool.false otherwise.

Andb3 (b1: Bool) (b2: Bool) (b3: Bool) : Bool
Andb3 b1 b2 b3 = ?

Test_andb3_1 Equal Bool (Andb3 Bool.true Bool.true Bool.true) Bool.true
Test_andb3_1 = ?

Test_andb3_2 Equal Bool (Andb3 Bool.false Bool.true Bool.true) Bool.false
Test_andb3_2 = ?

Test_andb3_3 Equal Bool (Andb3 Bool.true Bool.false Bool.true) Bool.false
Test_andb3_3 = ?

Test_andb3_4 Equal Bool (Andb3 Bool.true Bool.true Bool.false) Bool.false
Test_andb3_4 = ?