Soft introduction to Coq: data structures and higher-order functions

Tutorial

Pairs and Lists

In the previous parts, we learned how to set new data types, define functions above them, and prove their correctness using common tactics. It is time to define some data structures and higher-order functions (hereinafter FWP) above them.

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

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

should read like this: there is only one way to build a pair of numbers - apply the constructor pairto two arguments of typenat

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

Coq has a mechanism for injecting syntactic sugar using a command Notation. 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 definitions of functions and statement 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 also 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 universally in functional programming languages. But what if we want to use a generalized definition to construct a list of integers, a list of logical values? Coq has a mechanism for defining polymorphic inductive types:

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

niland conshere they play the role of polymorphic constructors. Similarly, we can define polymorphic functions.

FVP

Filter

In many modern programming languages, a function can either accept 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, a function filterfilters 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 mapapplies 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, the question was asked about how the interpretation of evidence by machine occurs.

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