-- This module introduces the basic structure of an Agda program.
{- Every Agda file contains a single top-level module. To make it possible to
find the file corresponding to a particular module, the name of the file
should correspond to the name of the module. In this case the module
'Introduction.Basics' is defined in the file 'Introduction/Basics.agda'.
-}
module Introduction.Basics where
{- The top-level module contains a sequence of declarations, such as datatype
declarations and function definitions. The most common forms of declarations
are introduced below.
A module can also contain sub-modules, see 'Introduction.Modules.SubModules'
for more information.
-}
-- Agda can be used as a pure logical framework. The 'postulate' declaration
-- introduces new constants :
postulate
N : Set -- Set is the first universe
z : N
s : N -> N -- The independent function space is written A -> B
-- Using 'postulate' it is not possible to introduce new computation rules. A
-- better way is to introduce a datatype and define functions by pattern
-- matching on elements of the datatype.
-- A datatype is introduced with the 'data' keyword. All constructors of the
-- datatype are given with their types after the 'where'. Datatypes can be
-- parameterised (see 'Introduction.Data.Parameterised').
data Bool : Set where
false : Bool
true : Bool
data Nat : Set where
zero : Nat
suc : Nat -> Nat
-- Functions over datatypes can be defined by pattern matching.
plus : Nat -> Nat -> Nat
plus zero m = m
plus (suc n) m = suc (plus n m)
-- With this definition plus (suc zero) (suc zero) will reduce to suc (suc
-- zero).
-- Mutually recursive function can be defined inside a 'mutual' block.
mutual
even : Nat -> Bool
even zero = true
even (suc n) = odd n
odd : Nat -> Bool
odd zero = false
odd (suc n) = even n
-- Agda is a monomorphic, but dependently typed, language. This means that
-- polymorphism is simulated by having functions take type arguments. For
-- instance, the polymorphic identity function can be represented as follows :
id : (A : Set) -> A -> A -- the dependent function space is written (x : A) -> B
id A x = x
one : Nat
one = id Nat (suc zero) -- a silly use of the identity function
-- To faithfully simulate a polymorphic function we would like to omit the type
-- argument when using the function. See 'Introduction.Implicit' for
-- information on how to do this.
-- Agda is both a programming language and a formal proof language, so we
-- expect to be able to prove theorems about our programs. As an example we
-- prove the very simple theorem n + 0 == n.
-- First we introduce datatypes for truth (a singleton type) and falsity (an
-- empty type).
data True : Set where -- Here it would make sense to declare True to be a
tt : True -- Prop (the universe of propositions) rather than a
-- Set. See 'Introduction.Universes' for more
-- information.
data False : Set where -- see 'Introduction.Data.Empty' for more information
-- on empty types.
-- Second, we define what it means for two natural numbers to be equal. Infix
-- operators are declared by enclosing the operator in _. See
-- 'Introduction.Operators' for more information.
_==_ : Nat -> Nat -> Set
zero == zero = True
zero == suc m = False
suc n == zero = False
suc n == suc m = n == m
-- Now we are ready to state and prove our theorem. The proof is by induction
-- (i.e. recursion) on 'n'.
thmPlusZero : (n : Nat) -> plus n zero == n -- A function from a number n to
-- P n can be seen as the
-- proposition ∀ n. P n.
thmPlusZero zero = tt
thmPlusZero (suc n) = thmPlusZero n
{- In both branches the reduction makes the proof very simple. In the first
case the goal is
plus zero zero == zero which reduces to
zero == zero and
True
In the second case we have
plus (suc n) zero == suc n
suc (plus n zero) == suc n
plus n zero == n
so the induction hypothesis (the recursive call) is directly applicable.
-}