Роль доказательств в извлечении Coq

Question

Я пытаюсь понять, какова роль доказательств в извлечении 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.

Что здесь происходит? Я явно что-то здесь упускаю.

Answer 1

Хотя то, что сказал Чи, верно, в этом случае вы действительно можете извлечь свидетеля 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 / 2 nat сравнений, чтобы проверить деление n.Гораздо лучше написать просто напечатанную версию функции деления:

Fixpoint div2 n :=
  match n with
  | 0 | 1 => 0
  | S (S n) => S (div2 n)
  end.

Answer 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) и соответствовать закону исключенного среднего. У нас не может быть всего, или мы встречаемся с парадоксом Берарди.