Numbers

The types we have defined so far are examples of enumerated types: their definitions explicitly enumerate a finite set of elements. A more interesting way to define a type is to establish a collection of inductive rules describing its elements. For example, we can define natural numbers as follows:

type Nat {
  zero
  succ (pred: Nat)
}

This definition can be read as:

• Nat.zero is a natural number;
• Nat.succ is a constructor that takes a natural number, constructing another natural number;
  • That is, if n is a natural number, then (Nat.succ n) will also be.

Every type defined inductively (such as Nat, Bool ou Day) is a set of expressions. The definition of Nat says how expressions of type Nat can be constructed:

• The expression Nat.zero belongs to the set of Nat;
• If n is an expression in the set of Nat, then (Nat.succ n) is also an expression in the set of Nat;
• Expressions formed in these two ways are the only ones that belong to Nat.

The same rules apply to our definitions of Day and Bool. The annotations we used for them are analogous to the Nat.zero constructor, indicating that they do not receive any arguments.

These three conditions demonstrate the power of inductive declarations. They imply that the expression Nat.zero, the expression (Nat.succ Nat.zero), the expression (Nat.succ (Nat.succ Nat.zero)) and so on, are of the Nat set, while other expressions such as Bool.true, (Andb Bool.true Bool.false), and (Nat.succ (Nat.succ Bool.false)) are not.

We can write simple functions using pattern matching on natural numbers in the same way we did above - for example, the predecessor function:

Pred (n: Nat) : Nat
// Since natural numbers are strictly non-negative,
// we use as a convention that anything that would be
// less than 0 returns 0
Pred  Nat.zero    = Nat.zero
Pred (Nat.succ k) = k

The second pattern can be read as: "if n has the form (Nat.succ k) for some k, return k."

MinusTwo (n: Nat) : Nat
MinusTwo  Nat.zero               = Nat.zero
MinusTwo (Nat.succ  Nat.zero)    = Nat.zero
MinusTwo (Nat.succ (Nat.succ k)) = k

To avoid having to write a sequence of Nat.succ every time you want a Nat, you can use the n suffix at the end of any number, for example o 5n, which takes a number written in the primitive type U60 plus the n suffix and returns the corresponding Nat. {...}

Test : Equal/ Nat 6n (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ Nat.zero))))))
Test = Equal/refl

The Nat.succ constructor has type Nat -> Nat, as do the functions MinusTwo and Pred. They are all things that, when applied to a Nat, return a Nat. The essential difference between Nat.succ and the other two, however, is that functions come with reduction rules - for example, Pred (Nat.succ Nat.zero) is reducible to Nat.zero - while Nat.succ does not. Although it is a function applicable to an argument, it does not compute anything.

For most number function definitions, pattern matching alone is not enough: we will also need recursion. For example, to check whether a number n is even, we can recursively check whether n-2 is even.

Evenb (n: Nat) : Bool/
Evenb  Nat.zero               = Bool/true
Evenb (Nat.succ  Nat.zero)    = Bool/false
Evenb (Nat.succ (Nat.succ k)) = Evenb k

We can define Oddb (a function to check if a number is odd) with a similar recursive declaration, but we also have a simpler and somewhat easier to work with definition:

Oddb (n: Nat) : Bool/
Oddb n = Notb (Evenb n)

TestOddb1 : Equal/ Bool/ (Oddb 1n) Bool/true
TestOddb1 = Equal/refl

TestOddb2 : Equal/ Bool/ (Oddb 4n) Bool/false
TestOddb2 = Equal/refl

Naturally, we can also define functions with multiple arguments by recursion.

Plus (n: Nat) (m: Nat) : Nat
Plus  Nat.zero    m = m
Plus (Nat.succ k) m = Nat.succ (Plus k m)

Adding 3n and 2n will return 5n as expected. The simplification that Kind performs to arrive at this value can be visualized as follows:

Plus (Nat.succ (Nat.succ (Nat.succ Nat.zero))) (Nat.succ (Nat.succ Nat.zero))

> Nat.succ (Plus (Nat.succ (Nat.succ Nat.zero)) (Nat.succ (Nat.succ Nat.zero)))
by the second rule of Plus

> Nat.succ (Nat.succ (Plus (Nat.succ Nat.zero)) (Nat.succ (Nat.succ Nat.zero)))
by the second rule of Plus

> Nat.succ (Nat.succ (Nat.succ (Plus Nat.zero (Nat.succ (Nat.succ Nat.zero)))))
by the second rule of Plus

> Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ Nat.zero))))
by the first rule of Plus

Multiplication can be defined using the definition of Plus, as follows:

Mult (n: Nat) (m: Nat) : Nat
Mult  Nat.zero    m = Nat.zero
Mult (Nat.succ k) m = Plus m (Mult k m)

TestMult1 : Equal/ Nat (Mult 3n 3n) 9n
TestMult1 = Equal/refl

You can also use pattern matching on two expressions at the same time:

Minus (n: Nat) (m: Nat) : Nat
Minus  Nat.zero     m           = Nat.zero
Minus  n            Nat.zero    = n
Minus (Nat.succ k) (Nat.succ j) = Minus k j

The Exp function can be defined using Mult (analogous to how Mult is defined using Plus):

Exp (base: Nat) (power: Nat) : Nat
Exp base  Nat.zero    = Nat.succ Nat.zero
Exp base (Nat.succ k) = Mult base (Exp base k)

Factorial

Recall the basic mathematical definition of factorial:

\[\mathrm Factorial(n) = \begin{cases} \text{if $n$} = 0\,& 1 \
\\ \text{else} & n * Factorial(n-1) \end{cases} \]

\[ f(x)=\begin{cases}x&(x = 1)\\x f(x-1)&(x\gt 1)\end{cases} , x\in \Bbb{N} \]

Translate the factorial function into Kind2:

Factorial (n: Nat) : Nat
Factorial n = ?

TestFactorial1 : Equal/ Nat (Factorial 3n ) 6n
TestFactorial1 = ?

TestFactorial2 : Equal/ Nat (Factorial 5n) 120n
TestFactorial2 = ?

The Eql function tests equality between Naturals, returning a boolean.

Eql (n: Nat) (m: Nat) : Bool/
Eql  Nat.zero     Nat.zero    = Bool/true
Eql  Nat.zero    (Nat.succ j) = Bool/false
Eql (Nat.succ k)  Nat.zero    = Bool/false
Eql (Nat.succ k) (Nat.succ j) = Eql k j

TheLte function tests if the first argument is less than or equal to the second, returning a boolean.

Lte (n: Nat) (m: Nat) : Bool/
Lte  Nat.zero     m           = Bool/true
Lte (Nat.succ k)  Nat.zero    = Bool/false
Lte (Nat.succ k) (Nat.succ j) = Lte k j

TestLte1 : Equal/ Bool/ (Lte 2n 2n) Bool/true
TestLte1 = Equal/refl

TestLte2 : Equal/ Bool/ (Lte 2n 4n) Bool/true
TestLte2 = Equal/refl

TestLte3 : Equal/ Bool/ (Lte 4n 2n) Bool/false
TestLte3 = Equal/refl

Blt_nat

The Blt_natfunction tests the "less than" relationship in natural numbers. Instead of creating a new recursive function, define it using previously defined functions.

Blt_nat (n: Nat) (m: Nat) : Bool/
Blt_nat n m = ?

Test_blt_nat_1 : Equal/ Bool/ (Blt_nat 2n 2n) Bool/false
Test_blt_nat_1 = ?

Test_blt_nat_2 : Equal/ Bool/ (Blt_nat 2n 4n) Bool/true
Test_blt_nat_2 = ?

Test_blt_nat_3 : Equal/ Bool/ (Blt_nat 4n 2n) Bool/false
Test_blt_nat_3 = ?