Внимание! Эта упрощённая задача предназначена только для студентов, не специализирующихся по кафедре математической логики и теории алгоритмов.
Постановка задачи: доказать в Coq, что для любого конечного списка целых чисел a1, ..., an существует целое число M, которое, для любого i от 1 до n, не делится на ai, если |ai| > 1. Извлечь функциональный код программы, возвращающей число M с требуемым свойством по списку a1, ..., an.
Задача формализуется в Coq следующим образом (включая необходимые модули и определения):
Require Import ZArith.
Require Import Coq.Lists.List.
Open Scope Z_scope.
Definition div (x : Z) (y : Z) :=
exists z : Z, x = y * z.
Definition notdiv : forall L : list Z,
{ M : Z | forall a : Z, In a L -> a > 1 \/ a < -1 -> ~ div M a }.
Теперь нужно «доказать» определение notdiv, т.е.
построить объект (функцию) требуемого типа.
Примечание: список реализуется как объект индуктивного типа list Z (частный случай полиморфного типа списков list). Определение спискового типа и операций над ним см. в документации к стандартной библиотеке: Coq.Lists.List. В нашем определении используется предикат In, обозначающий принадлежность элемента списку.
Fixpoint listprod (L : list Z) := match L with | nil => 1 | a :: L' => a * (listprod L') end.Можно доказать (индукцией по списку L), что произведение всех элементов делится на каждый элемент:
Lemma divprodlist : forall L : list Z, forall a : Z, In a L -> div (listprod L) a.
Lemma ndivone : forall x y : Z, x > 1 -> div y x -> ~ div (y+1) x. Lemma ndivone2 : forall x y : Z, x > 1 \/ x < -1 -> div y x -> ~ div (y+1) x.
Доказательство леммы ndivone в Coq не совсем тривиально. Применяя red, intros и elim, мы получаем две гипотезы:
H2 : y = x * x0 H3 : y + 1 = x * x1откуда можно перейти (тактикой assert) к x * (x1 - x0) = 1.
Привести последнюю к противоречию (цель у нас — False) можно рассмотрением случаев с помощью Ztrichotomy (см. Coq.ZArith.Zorder), применённой к (x1 - x0) и нулю. Переход от условия «> 0» к «≥ 1» осуществляется применением Zgt_le_succ (см. там же), после чего можно использовать Zmult_lt_compat_l для перемножения неравенств.
Также следует пользоваться, где это возможно, автоматическими тактиками auto with zarith, ring и omega.
Извлечение функционального кода на языке OCaml осуществляется инструкцией Extraction (в новых версиях Coq нужно загрузить модуль Coq.extraction.Extraction):
Extraction "notdiv.ml" notdiv.Извлечённый таким образом код будет корректным кодом на языке OCaml, однако заставить его работать затруднительно: целые числа в нём представлены не в стандартном типе int, а посредством определения в OCaml Coq'овского типа Z (числа там представляются примерно так: Zpos (XI (XO (XI XH)))).
Самый простой способ получить код, использующий тип int, заключается в использовании модуля Coq.extraction.ExtrOcamlZInt, который подменяет тип Z на встроенный тип int, а также заменяет рекурсивные реализации арифметических операций, построенные в Coq для Z на эффективные встроенные реализации.
При использовании модуля Coq.extraction.ExtrOcamlZInt
Require Import Coq.extraction.ExtrOcamlZInt. Extraction "notdiv2.ml" notdiv.получается код, который можно непосредственно запустить (заметим, что при использовании этого модуля list также отобразился в «родной» списочный тип OCaml):
$ ocaml
OCaml version 4.05.0
# #use "notdiv2.ml";;
type 'a sig0 = 'a
module Pos :
sig
val succ : int -> int
val add : int -> int -> int
val add_carry : int -> int -> int
val pred_double : int -> int
val mul : int -> int -> int
end
module Z :
sig
val double : int -> int
val succ_double : int -> int
val pred_double : int -> int
val pos_sub : int -> int -> int
val add : int -> int -> int
val mul : int -> int -> int
end
val listprod : int list -> int = <fun>
val notdiv_list : int list -> int = <fun>
# notdiv_list [2;5;6];;
- : int = 61
# Control+D
$
(Полужирным выделено то, что вводит пользователь.)
Использование Coq.extraction.OcamlZInt в реальных приложениях, однако, не рекомендуется: что простая синтаксическая замена Z на int может приводить к конфликтам имён, а также арифметические операции, заменённые на встроенные, становятся несертифицированными (подробнее см. описание родственного модуля Coq.extraction.ExtrOcamlNatInt).
В этом необязательном разделе мы обсудим модуль Coq.extraction.ExtrOcamlIntConv для более аккуратной работы с целыми числами при извлечении кода в OCaml. Этот модуль разделяет типы int (встроенный в OCaml) и Z (рекурсивно определённый в Coq), и предоставляет интерфейсы между ними: int_of_z : Z -> int и z_of_int : int -> Z. При этом у нас сохраняется сертифицированность всех операций, производимых в типе Z, а условие на корректность формулируется также в терминах Z с помощью перевода:
Require Import Coq.extraction.ExtrOcamlIntConv.
Definition notdiv_int : forall L : list int,
{ M : int | forall a : int, In a L -> (z_of_int a) > 1 \/ (z_of_int a) < -1 -> ~ div (z_of_int M) (z_of_int a) }.
(Мы не можем написать условие в терминах int, потому что для машинно-реализованных целых чисел у нас нет никакой теории.)
Новый терм notdiv_int можно построить («доказать», Proof) с помощью ранее построенного notdiv, однако для этого понадобится постулировать дополнительный принцип:
Require Import Coq.extraction.ExtrOcamlIntConv.
Axiom zz : forall b : Z, z_of_int (int_of_z b) = b.
Definition notdiv_int : forall L : list int,
{ M : int | forall a : int, In a L -> (z_of_int a) > 1 \/ (z_of_int a) < -1 -> ~ div (z_of_int M) (z_of_int a) }.
Proof.
intros.
elim (notdiv (map z_of_int L)). intros.
exists (int_of_z x). intros.
rewrite (zz x). apply p.
apply in_map. assumption.
assumption.
Qed.
Аксиома zz говорит, что преобразование Z → int → Z даёт то же число. К сожалению,
доказать zz невозможно, потому что это утверждение попросту неверно: если число слишком большое, трансляция его
в int даст переполнение. Таким образом, здесь «дырка» в верификации стала явной, в отличие от ситуации с
Coq.extraction.ExtrOcamlZInt. Итак, notdiv_int верифицировано по модулю того, что аргументы и результат вычисления
удовлетворяют zz.
Теперь код можно извлечь:
Extraction "notdiv3.ml" notdiv_int.и запустить следующим образом:
$ ocaml
OCaml version 4.05.0
# #use "notdiv3.ml";;
type 'a list = Nil | Cons of 'a * 'a list
type 'a sig0 = 'a
type positive = XI of positive | XO of positive | XH
type z = Z0 | Zpos of positive | Zneg of positive
module Pos :
sig
val succ : positive -> positive
val add : positive -> positive -> positive
val add_carry : positive -> positive -> positive
val pred_double : positive -> positive
val mul : positive -> positive -> positive
end
module Z :
sig
val double : z -> z
val succ_double : z -> z
val pred_double : z -> z
val pos_sub : positive -> positive -> z
val add : z -> z -> z
val mul : z -> z -> z
end
val map : ('a -> 'b) -> 'a list -> 'b list = <fun>
val int_of_pos : positive -> int = <fun>
val int_of_z : z -> int = <fun>
val int_poslike_rec : 'a -> ('a -> 'a) -> ('a -> 'a) -> int -> 'a = <fun>
val pos_of_int : int -> positive = <fun>
val int_zlike_case : 'a -> (int -> 'a) -> (int -> 'a) -> int -> 'a = <fun>
val z_of_int : int -> z = <fun>
val listprod : z list -> z = <fun>
val notdiv_list : z list -> z = <fun>
val notdiv_int : int list -> int = <fun>
# let rec listwrapper = function
[] -> Nil
| x :: l -> Cons (x, listwrapper l);;
val listwrapper : 'a list -> 'a list = <fun>
# notdiv_int (listwrapper [2;3;4]);;
- : int = 25
# Control+D
$
Здесь функция listwrapper преобразует список из встроенного списочного типа OCaml в рекурсивно
определённый в Coq списочный тип. Объектами списка по-прежнему являются числа типа int: преобразование
в Z и обратно делается в Coq.