A gentle introduction to Coq: data structures and higher order functions

Couples and Lists

In the previous parts, we learned how to define new data types, define functions on them and prove their correctness with the help of common tactics. It is time to determine some data structures and higher-order functions (hereinafter, FVP) above them.


In an inductive definition, each constructor can contain an arbitrary number of parameters, for example, the definition

 Inductive natprod: Type: = 
   pair: nat -> nat -> natprod.

should read like this: there is only one way to build a pair of numbers - use the pair constructor to the two arguments of the nat type
')

 Eval simpl in (pair 1 2).
 (* ==> pair 1 2: natprod *)

Coq has a mechanism for introducing syntax sugar using the Notation command. For example, we can get rid of the prefix form and define pairs of numbers like this:

 Notation "(x, y)": = (pair xy).

This new notation can now be widely used in expressions and in the definitions of functions and formulations of theorems:

 Definition fst (p: natprod): nat: = 
   match p with 
   |  (x, y) => x 
   end. 
 Definition snd (p: natprod): nat: = 
   match p with 
   |  (x, y) => y 
   end.
 Theorem test: forall (ab: nat), 
  (a, b) = (fst (a, b), snd (a, b)). 
 Proof.  reflexivity.  Qed.

Summarizing the definition of a pair, we can describe lists of numbers:

 Inductive natlist: Type: = 
   |  nil: natlist 
   |  cons: nat -> natlist -> natlist.
 Notation "h :: t": = (cons ht) (at level 60, right associativity). 
 Notation "[]": = nil. 
 Notation "[h, .., t]": = (cons h .. (cons t nil) ..).

Using the syntax rules introduced, we can define lists in several ways:

 Definition list1: = 1 :: (2 :: (3 :: nil)). 
 Definition list2: = [1,2,3].

Lists are used everywhere in functional programming languages. But what if we want to use a generic definition to construct a list of integers, a list of logical values? In Coq, there is a mechanism for determining polymorphic inductive types:

 Inductive list (X: Type): Type: = 
   |  nil: list X 
   |  cons: X -> list X -> list X.

nil and cons play the role of polymorphic constructors here. Similarly, we can define polymorphic functions.

Pvp

Filter

In many modern programming languages, a function can either take another function as an argument or return it as a result. Such functions are called higher order functions and are widely used in mathematics (for example, the derivative calculation operator) and programming (for example, the filter function filters the elements of a set by a predicate):

 Fixpoint evenb (n: nat): bool: =
   match n with
   |  O => true
   |  SO => false
   |  S (S n ') => evenb n'
   end.

 Fixpoint filter {X: Type} (test: X → bool) (l: list X)
                 : (list X): =
   match l with
   |  [] => []
   |  h :: t => if test h then h :: (filter test t)
                         else filter test t
   end.

 Example test: filter evenb [1,2,3,4,5] = [2,4].
 Proof.  reflexivity.  Qed.

Map

FVP map applies this function to each element of the list, returning a list of results:

 Fixpoint map {XY: Type} (f: X → Y) (l: list X)
              : (list Y): =
   match l with
   |  [] => []
   |  h :: t => (fh) :: (map ft)
   end.

Lyrical digression

In the comments to one of the previous articles, a question was asked about how the machine interprets the evidence.

As is known, the Curry-Howard isomorphism determines the correspondence between evidence and programs. We can build some analogies:

• theorems - types
• evidence - terms
• proof verification - term type verification

Thus, Coq is just a type check checker that derives term types. The user can modify the output algorithm using tactics.