Natural Number Type
Notation
Rules
Types are defined by their formation, term introduction, term eliminator and computation rules.
In order to avoid having a infinite number of constructors we can define Nat in terms of functions Z and S.
Nat Type 


formation rule N exists 


term introduction rules



term eliminator Proof by induction To prove property P (implemented as a type) we need to proove P(0) and P(x) implies P(sx) rec is recursor (see recursor section above) where: rec
nat
z_{0} z_{s} O
=
z_{0} where



computation rules 



Idris Code
Idris Code for Nat is here.
The formation and term introduction rules can be represented in Idris like this: 
data Nat = Z  S Nat 
The term eliminator can be implemented by the 'case' construct.  
computation and local completeness rules  ie 
Computer Implementation
How do we implement natural numbers in computer algebra and proof assistant programs? Some alternatives are:
 Define inductively from Zero and Successor as in Coq (Calculus of Inductive Constructions) .
 Define them as predicates in higher order logic.
 Define them axiomatically.
defined inductively  predicates in higher order logic  define them axiomatically  

advantages  Can automatically generate induction proof principle. Can define functions by wellfounded recursion. 
Keeps program simple Don't need to show each recursive definition represents a terminating algorithm, unique for each input. 

disadvantages  each function requires a proof. 
Idris
Elimination (pattern matching) is built in to Idris. 
data Nat =  Zero Z   Successor S Nat Eq Nat where Z == Z = True (S l) == (S r) = l == r _ == _ = False 
Coq
github  Inductive nat : Set :=  0 : nat  S : nat > nat. 
Enumeration Type
An enumerated type is any type given by a finite disjoint sum of unit types.
Can be thought of as a sum (1+1...) or as a degenerate form of an inductive type.
Inductive Types
Natural Number Type
Natural Number Type 


formation rule N exists 


term introduction rules



term eliminator Proof by induction To prove property P (implemented as a type) we need to proove P(0) and P(x) implies P(sx) rec is recursor (see recursor section above) where: rec
nat
z_{0} z_{s} O
=
z_{0} where



computation rules 



Next Steps
Other types are discussed on the following pages: