(* 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)).