(* Simple inductive types and recursive definitions. *)
(* For the module G54DTP, Dependently Typed Programming. *)
(* Venanzio Capretta, February 2011. *)
(* The notation for the lambda abstraction (lambda x. t)
in Coq is: fun x => t.
*)
Definition my_fun : nat -> nat := fun x => x*x*x + 1.
Eval compute in (my_fun 3).
(* Alternatively, you can put the argument as a parameter. *)
Definition my_fun2 (x:nat) : nat := x*x*x + 1.
Eval compute in (my_fun2 3).
Check my_fun2.
(* The "constructor notation" for natural numbers uses
O for zero, S for successor (adding one).
Decimal numerals are defined as a convenient notation.
*)
Check (S (S O)).
(* Recursive functions are defined using the instruction "Fixpoint".
The "match" construct performs a case analysis on its argument:
every case consists in a pattern, the arrow => and the result term.
recursive calls must be performed on a subterm of the pattern.
*)
Fixpoint factorial (n:nat) : nat :=
match n with
O => 1
| (S n') => n*(factorial n')
end.
Eval compute in (factorial 4).
(* We can have nested pattern matching. *)
Fixpoint fibonacci (n:nat) : nat :=
match n with
O => 1
| (S n') =>
match n' with
O => 1
| (S n'') => (fibonacci n'') + (fibonacci n')
end
end.
Eval compute in (fibonacci 7).
(* Importing the library for integer numbers. *)
Require Import ZArith.
(* Specifying that special notations (numerals, infix operators for
addition and multiplication) must be interpreted in the integers.
*)
Open Scope Z_scope.
(* Opening a section: it allows us to declare local variables. *)
Section Lucas.
(* These variables are local:
they will be abstracted when we close the section.
*)
Variables (x0 x1:Z)(c0 c1:Z).
(* Lucas sequences are a generalization of the Fibonacci numbers.
The two first elements of the sequence are arbitrary: x0 and x1.
successive elements are obtained by the recursive equation:
lucas (n+2) = c0*(lucas n) + c1*(lucas (n+1)).
*)
Fixpoint lucas (n:nat) : Z :=
match n with
O => x0
| (S n') =>
match n' with
O => x1
| (S n'') => c0*(lucas n'') + c1*(lucas n')
end
end.
Check lucas.
(* Closing the section. *)
End Lucas.
(* Now the section variables have been abstracted and become
arguments of the function "lucas".
*)
Check lucas.
(* Fibonacci numbers are a special case of lucas numbers. *)
Definition fib := lucas 1 1 1 1.
Eval compute in (fib 20).
Eval compute in (fibonacci 20).
(* The natural numbers form an inductive type.
Here is an equivalent definition.
*)
Inductive Natural : Set :=
zero : Natural
| succ : Natural -> Natural.
(* We can define addition by recursion and pattern matching. *)
Fixpoint NatPlus (n m:Natural) : Natural :=
match m with
zero => n
| (succ m') => succ (NatPlus n m')
end.
(* Similarly for multiplication. *)
Fixpoint NatTimes (n m:Natural) : Natural :=
match m with
zero => zero
| (succ m') => NatPlus (NatTimes n m') n
end.
(* Fibonacci function on our set of naturals. *)
Fixpoint NatFib (n:Natural) : Natural :=
match n with
zero => (succ zero)
| (succ n') =>
match n' with
zero => (succ zero)
| (succ n'') => NatPlus (NatFib n'') (NatFib n')
end
end.
Eval compute in (NatFib (succ (succ (succ (succ zero))))).
(* Similarly, we can define a type of lists of integers.
Lists can be constructed in two ways:
"empty" is a list
"newhead" is a function that takes a number and a list
as arguments and returns the list with the number
as first element and the given list as continuation.
*)
Inductive ZList : Set :=
empty : ZList
| newhead : Z -> ZList -> ZList.
(* The length of a list, defined recursively. *)
Fixpoint zllength (l:ZList) : nat :=
match l with
empty => O
| (newhead x l') => S (zllength l')
end.
Eval compute in (zllength (newhead (-2) (newhead 1 (newhead 7 empty)))).
(* There is already a library for lists of any type. *)
Require Export List.
(* Use "Print" to see the definition of any object. *)
Print list.
Print length.
(* There is a function to compare two integers to see if the
first is smaller/equal or greater than the second.
*)
Check Z_le_gt_dec.
(* We will explain its type later.
For now it is enough that we can use the if_then_else
construct to branch according to the result.
*)
(* Insertion of a number in a list. If the list is ordered,
the number is inserted in the correct place.
*)
Fixpoint insert (x:Z)(l:list Z): list Z :=
match l with
nil => x::l
| (cons y l') => if (Z_le_gt_dec x y)
then (x::l)
else (y::(insert x l'))
end.
(* Now we can define the insertion sort algorithm
by recursion on the structure of lists.
*)
Fixpoint insertion_sort (l:list Z): list Z :=
match l with
nil => nil
| (cons x l') => insert x (insertion_sort l')
end.
Eval compute in (insertion_sort (2::6::1::3::9::7::0::nil)).