Мягкое введение в Coq: индуктивные определения

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

Ранее я сказал, что в Coq нет батареек. На самом деле я слукавил — в Coq есть стандартная библиотека, которая содержит множество полезных определений. Помимо стандартной библиотеки существуют и более специфические вещи, на которых мы пока не будем останавливаться.

В момент старта CoqIDE в фоновом режиме подругжаются некоторые библиотеки, список которых можно посмотреть с помощью команды Print Libraries:

Loaded and imported library files: 
  Coq.Init.Notations 
  Coq.Init.Logic 
  Coq.Init.Datatypes 
  Coq.Init.Specif 
  Coq.Init.Peano 
  Coq.Init.Wf 
  Coq.Init.Tactics 
  Coq.Init.Prelude 
  Coq.Init.Logic_Type

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

Как известно, ни одна вводная статья по функциональному программированию не обходится без вычисления факториала. Мы не будем отходить от этой традиции и напишем свой собственный факториал с индуктивными типами.

Натуральные числа

Индуктивные определения встречаются в математике повсеместно. Например, натуральные числа с позиции теории множеств вводятся следующим образом:



Аналогичным образом мы можем задать натуральные числа в Coq. Для того, чтобы не засорять пространство имен, воспользуемся системой модулей:

Module Test1. 

Inductive nat : Type := 
  | O : nat 
  | S : nat -> nat. 

Это объявление следует читать так:

1. O — натуральное число,
2. S — это конструктор, который принимает натуральное число, и возвращает еще одно натуральное число: если n ∈ N, то и S n ∈ N.

Пользуясь этим определением мы можем сконструировать любое натуральное число:

Eval simpl in (S O).
(* ==> 1 : nat *)
Eval simpl in (S (S O)).
(* ==> 2 : nat *)
Eval simpl in (S (S (S O))).
(* ==> 3 : nat *)

Теперь, когда у нас есть натуральные числа, самое время определить набор функций над этими числами:

Fixpoint plus (n : nat) (m : nat) : nat :=
  match n with
    | O => m
    | S n' => S (plus n' m)
  end.

Здесь мы определили рекурсивную (ключевое слово Fixpoint) функцию plus, которая принимает на вход два аргумента типа nat и возвращает результат типа nat. Убедиться в этом можно с помощью команды Check:

Check plus.
(* ==> plus : nat -> nat -> nat *)

Рассмотрим ее работу на конкретном примере. Вычислим значение выражения 3 + 2:

Eval simpl in (plus (S (S (S O))) (S (S O))).
(* ==> 5 : nat *)

Отлично! Все работает. Но как получается это результат?

(*  plus (S (S (S O))) (S (S O))    
==> S (plus (S (S O)) (S (S O))) второй клоз в определении
==> S (S (plus (S O) (S (S O)))) второй клоз в определении
==> S (S (S (plus O (S (S O))))) второй клоз в определении
==> S (S (S (S (S O))))          первый клоз в определении
*)

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

Fixpoint mult (n m : nat) : nat :=
  match n with
    | O => O
    | S n' => plus m (mult n' m)
  end.

Fixpoint factorial (n : nat) : nat :=
  match n with
    | O => S O
    | S n' => mult n (factorial n')
  end.

Eval simpl in (factorial (S (S (S (S (S O)))))).
(* ==> 120 : nat *)

Заключение

Для закрепления материала я настоятельно рекомендую читателю запустить все примеры в CoqIDE. В следующей части рассмотрим работу с базовыми тактиками Coq.

Продолжение.