Мягкое введение в Coq: структуры данных и функции высших порядков

Пары и списки

В предыдущих частях мы научились задавать новые типы данных, определять функции над ними и доказывать их корректность с помощью распространенных тактик. Настало время определить некоторые структуры данных и функции высших порядков (далее ФВП) над ними.


В индуктивном определении каждый конструктор может содержать произвольное число параметров, например определение

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

следует читать так: существует единственный способ построить пару чисел – применить конструктор pair к двумя аргументам типа nat

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

В Coq существует механизм для введения синтаксического сахара с помощью команды Notation. Например, мы можем избавиться от префиксной формы и определять пары чисел так:

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

Эта новая нотация теперь может быть широко использована в выражениях и в определениях функций и формулировках теорем:

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 (a b : nat), 
 (a,b) = (fst (a,b), snd (a,b)). 
Proof. reflexivity. Qed.

Обобщив определение пары мы можем описать и списки чисел:

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

С помощью введенных синтаксических правил, мы можем определять списки несколькими способами:

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

Списки применяются в функциональных языках программирования повсеместно. Но что делать, если мы хотим использовать обобщенное определение для конструирования списка целых чисел, списка логических значений? В Coq существует механизм для определения полиморфных индуктивных типов:

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

nil и cons здесь играют роль полиморфных конструкторов. Аналогичным образом мы можем определять и полиморфные функции.

ФВП

Filter

Во многих современных языках программирования функция может как принимать в качестве аргумента другую функцию, так и возвращать ее в качестве результата. Такие функции называются функциями высшего порядка и широко используются в математике (например, оператор вычисления производной) и программировании (например, функция filter фильтрует элементы множества по предикату):

Fixpoint evenb (n:nat) : bool :=
  match n with
  | O        => true
  | S O      => 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

ФВП map применяет данную функцию к каждому элементу списка, возвращая список результатов:

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

Лирическое отступление

В комментариях к одной из предыдущих статей был задан вопрос о том, как происходит интерпретация доказательств машиной.

Как известно, изоморфизм Карри-Говарда определяет соответствие между доказательствами и программами. Мы можем построить некоторые аналогии:

• теоремы — типы
• доказательства — термы
• проверка доказательства — проверка типа терма

Таким образом, Coq — это всего лишь тайпчекер, который выводит типы термов. Пользователь может модифицировать алгоритм вывода с помощью тактик.