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 : Prop.Equal Bool (Orb Bool.true Bool.false) Bool.true
TestOrb1 = Prop.Equal.refl
TestOrb2 : Prop.Equal Bool (Orb Bool.false Bool.false) Bool.false
TestOrb2 = Prop.Equal.refl
TestOrb3 : Prop.Equal Bool (Orb Bool.false Bool.true) Bool.true
TestOrb3 = Prop.Equal.refl
TestOrb4 : Prop.Equal Bool (Orb Bool.true Bool.true) Bool.true
TestOrb4 = Prop.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 : Prop.Equal Bool (Nandb Bool.true Bool.false) Bool.true
Test_nandb1 = ?
Test_nandb2 : Prop.Equal Bool (Nandb Bool.false Bool.false) Bool.true
Test_nandb2 = ?
Test_nandb3 : Prop.Equal Bool (Nandb Bool.false Bool.true) Bool.true
Test_nandb3 = ?
Test_nandb4 : Prop.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 Prop.Equal Bool (Andb3 Bool.true Bool.true Bool.true) Bool.true
Test_andb3_1 = ?
Test_andb3_2 Prop.Equal Bool (Andb3 Bool.false Bool.true Bool.true) Bool.false
Test_andb3_2 = ?
Test_andb3_3 Prop.Equal Bool (Andb3 Bool.true Bool.false Bool.true) Bool.false
Test_andb3_3 = ?
Test_andb3_4 Prop.Equal Bool (Andb3 Bool.true Bool.true Bool.false) Bool.false
Test_andb3_4 = ?