Coq-практикум: сортировка

В этой задаче мы реализуем простейший алгоритм сортировки списков натуральных чисел. При этом, если в исходном списке были повторы, они могут быть отождествлены (мы не накладываем требования сохранения количества вхождений).

I. Необходимые модули и определения

Require Import Coq.Lists.List.
Require Import Coq.Arith.Compare_dec.
Require Import Arith.


Fixpoint first (L : list nat) (d : nat) :=
match L with
nil => d |
a :: L1 => a
end.

Fixpoint sorted (L : list nat) :=
match L with
nil => True |
a :: L1 => sorted L1 /\ first L1 0 <= a
end.

Definition subset (L1 : list nat) (L : list nat) :=
forall a : nat, In a L1 -> In a L.

Definition is_sort (Ls : list nat) (L : list nat) :=
sorted Ls /\ subset Ls L /\ subset L Ls.

II. Технические леммы

Lemma triv_subset : forall L : list nat, subset L L.

Lemma triv_sort : forall L : list nat, sorted L -> is_sort L L.

Lemma sort_gap : forall L : list nat, forall a : nat, forall b : nat,
 sorted (a :: b :: L) -> sorted (a :: L).

Lemma sort_monotone : forall L : list nat, forall a : nat,
 sorted (a :: L) -> sorted L.

Lemma sort_deep : forall L : list nat, forall a : nat, 
 sorted (a :: L) -> forall b : nat, (In b L -> b <= a).

Lemma subset_trans : forall L1 L2 L3 : list nat,
 subset L1 L2 -> subset L2 L3 -> subset L1 L3.

Lemma subset_longer : forall L1 L2 : list nat, forall a : nat,
 subset L1 L2 -> subset (a :: L1) (a :: L2).

III. Основная часть

Definition SortAppend : forall Ls : list nat, forall a : nat, 
 sorted Ls -> { Lss : list nat | is_sort Lss (a :: Ls) }.

Definition Sort : forall L : list nat, 
 { Ls : list nat | is_sort Ls L }.

IV. Извлечение кода

Extraction "/tmp/sort.ml" Sort.

V. Запуск

$ ocaml
        OCaml version 4.02.3

# #use "sort.ml";;
type nat = O | S of nat
type 'a list = Nil | Cons of 'a * 'a list
type 'a sig0 = 'a
type sumbool = Left | Right
val le_lt_dec : nat -> nat -> sumbool = <fun>
val sortAppend : nat list -> nat -> nat list = <fun>
val sort : nat list -> nat list = <fun>
# #use "sort_wrapper.ml";;
val i2n : int -> nat = <fun>
val n2i : nat -> int = <fun>
val listwrapper : int list -> nat list = <fun>
val listunwrapper : nat list -> int list = <fun>
val sortlist : int list -> int list = <fun>
# sortlist [34;23;59;300;1;44];;
- : int list = [300; 59; 44; 34; 23; 1]
# Control+D
$

Подсказки

Полезно иметь под рукой документацию к используемым модулям стандартной библиотеки Coq. Напомним, что нам нужны модули Coq.Lists.List, Coq.Arith.Compare_dec и, конечно, Arith. Правила Coq запрещают разбирать индуктивно построенный объект (малый тип) типа Prop, если целевой объект сам не лежит в типе Prop (а то, что мы строим в SortAppend и Sort, лежит в Set, а не Prop). Поэтому вместо дизъюнкции приходится использовать конструкцию «булева сумма» и использовать леммы из Coq.Arith.Compare_dec вместо Arith.

Также полезно помнить про стандартные тактики: red раскрывает неиндуктивные определения, elim разбирает случаи индуктивного типа в посылке, simpl осуществляет упрощение выражений.