Роль пруфов в извлечении Coq
Я пытаюсь понять, какова роль доказательств в извлечении Coq.
У меня есть следующий пример целочисленного деления пола на два, взятый из здесь. Для моей первой попытки я использовал ключевое слово Admitted:
(*********************)
(* div_2_even_number *)
(*********************)
Definition div_2_even_number: forall n,
(Nat.Even n) -> {p:nat | n=p+p}.
Proof.
Admitted.
(*************)
(* test_even *)
(*************)
Definition test_even: forall n,
{Nat.Even n}+{Nat.Even (pred n)}.
Proof.
Admitted.
(********************)
(* div_2_any_number *)
(********************)
Definition div_2_any_number (n:nat):
{p:nat | n = p+p}+{p:nat | (pred n) = p+p} :=
match (test_even n) with
| left h => inl _ (div_2_even_number n h)
| right h' => inr _ (div_2_even_number (pred n) h')
end.
(***************************)
(* Extract to Haskell file *)
(***************************)
Extraction "/home/oren/some_file.hs" div_2_any_number.
Когда я изучаю получившийся файл Haskell, я вижу, что он действительно отсутствует:
div_2_even_number :: Prelude.Integer -> Prelude.Integer
div_2_even_number =
Prelude.error "AXIOM TO BE REALIZED"
test_even :: Prelude.Integer -> Prelude.Bool
test_even =
Prelude.error "AXIOM TO BE REALIZED"
div_2_any_number :: Prelude.Integer -> Prelude.Either Prelude.Integer
Prelude.Integer
div_2_any_number n =
case test_even n of {
Prelude.True -> Prelude.Left (div_2_even_number n);
Prelude.False -> Prelude.Right (div_2_even_number (pred n))}
Итак, я подумал, хорошо, давайте докажем div_2_even_number:
(*********************)
(* div_2_even_number *)
(*********************)
Definition div_2_even_number: forall n,
(Nat.Even n) -> {p:nat | n=p+p}.
Proof.
intros n0 H.
unfold Nat.Even in H.
destruct H as [m0].
exists m0.
Qed.
Но я получаю следующую ошибку:
Error: Case analysis on sort Set is not allowed for inductive definition ex.
Что тут происходит? Я явно что-то здесь упускаю.
Ответы 2
Вы работаете с типами разных видов.
> Check (Nat.Even 8).
Nat.Even 8
: Prop
> Check {p:nat | 8=p+p}.
{p : nat | 8 = p + p}
: Set
Особенностью системы типов Coq является то, что вы не можете исключить значение, тип которого находится в Prop, чтобы получить что-то, чей тип не находится в Prop (грубо говоря, Coq делает некоторые исключения для Prop типов, которые не несут информации, таких как True и False, но мы не в том случае). Грубо говоря, вы не можете использовать доказательство предложения ни для чего, кроме как для доказательства другого предложения.
Это ограничение, к сожалению, необходимо, чтобы Prop было непредикативным (мы хотим, чтобы forall P: Prop, P->P был типом в сортировке Prop) и соответствовало закону исключенного третьего. У нас не может быть всего, иначе мы столкнемся с парадоксом Берарди.
@luqui Я не могу вспомнить, но я думаю, что Coq действительно делает исключение для индуктивных типов, имеющих ноль или один тривиальный конструктор, поскольку они не несут «данных». Быстрый эксперимент, кажется, подтверждает это.
Я все еще немного запутался, значит ли это, что div_2_even_number можно доказать нет? есть ли способ определить (и извлечь) div_2_any_number?
@OrenIshShalom, как определяется Nat.Even?
div_2_even_number можно доказать, но не напрямую из Nat.Even предположения. Подумайте, во что она будет извлечена: если вы удалите доказательства (Nat.Even и n = p + p), у вас останется функция nat -> nat, которая должна отображать четные числа в их половины и которая никогда не будет применяться к нечетным числам (потому что у них нет доказательства Nat.Even на исходном языке). Следовательно, div_2_even_number должен выполнить как минимум столько же вычислений, сколько и деление на два, чтобы получить результат p : nat, плюс, возможно, дополнительную работу по построению доказательного термина для n = p + p.
@chi верен, если ожидаемый тип имеет вид Type, вы можете разрушить только неинформативные термины доказательства, и это позволяет вам разрушить доказательства False в «невозможных случаях».
@luqui вот оно: Nat.Even = fun n : nat => exists m : nat, n = 2 * m : nat -> Prop
Хотя то, что сказал Чи, верно, в этом случае вы действительно можете извлечь свидетеля p из доказательства существования. Когда у вас есть логический предикат P : nat -> bool, если exists p, P p = true, вы можете вычислить некоторое p, которое удовлетворяет предикату, запустив следующую функцию из 0:
find p := if P p then p else find (S p)
Вы не можете написать эту функцию непосредственно в Coq, но это можно сделать, создав специальное индуктивное предложение. Этот паттерн реализован в модуль выбора библиотеки математических компонентов:
From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype choice.
(* == is the boolean equality test *)
Definition even n := exists p, (n == 2 * p) = true.
Definition div_2_even_number n (nP : even n) : {p | (n == 2 * p) = true} :=
Sub (xchoose nP) (xchooseP nP).
Функция xchoose : (exists n, P n = true) -> nat выполняет описанный выше поиск, а xchooseP показывает, что ее результат удовлетворяет логическому предикату. (Настоящие типы более общие, но при создании экземпляра в nat они дают эту подпись.) Я использовал логический оператор равенства для упрощения кода, но вместо него можно было бы использовать =.
При этом, если вы заботитесь о запуске своего кода, программирование таким образом ужасно неэффективно: вам нужно выполнять n / 2nat сравнения, чтобы проверить деление n. Гораздо лучше написать просто типизированную версию функции деления:
Fixpoint div2 n :=
match n with
| 0 | 1 => 0
| S (S n) => S (div2 n)
end.
Разве вы не можете, например, использовать информацию
Prop, чтобы показать, что случай, которого вы достигли, невозможен при построенииType?