Мягкое введение в 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 — это всего лишь тайпчекер, который выводит типы термов. Пользователь может модифицировать алгоритм вывода с помощью тактик.