Зависимый тип как аргумент функции в Coq

Я новичок в Coq. Я пытаюсь поэкспериментировать с зависимыми типами Coq. Я просто хочу передать функции четное число. Например, в псевдокоде:

def next_even(n: {n: Integer | n is even}) :=
{
  add n 2
}

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

next_even(1)    // Coq should show an error
next_even(4)    // Coq should compute 6

Итак, в Coq я хочу сделать следующее:

Compute (next_even 1).
Compute (next_even 4).

Как я могу это построить?


function dependent-type coq
person arnobpl    schedule 14.11.2019    source источник

Ответы (1)


arrow_upward
1
arrow_downward

Вот прямой перевод вашей функции в Coq:

From Coq Require Import Arith.

Definition add_two_even (n : {n : nat | Nat.even n = true}) : nat :=
  proj1_sig n + 1.

Обратите внимание, что вам нужна функция proj1_sig для извлечения n из типа подмножества {n : nat | Nat.even n = true}. Чтобы использовать add_two_even, вам также нужно пойти другим путем: перейти от числа к элементу {n | Nat.even n = true}. В Coq это требует ручного доказательства. Для конкретных значений n это просто:

(* The next command fails with a type checking error *)
Fail Compute add_two_even (exist _ 1 eq_refl).
(* The next command succeeds *)
Compute add_two_even (exist _ 4 eq_refl).

Конструктор exist обертывает значение x с доказательством P x, создавая элемент типа подмножества {x | P x}. Термин eq_refl является доказательством x = x для любого значения x. Когда n - конкретное число, Coq может оценить Nat.even n и определить, является ли eq_refl действительным доказательством Nat.even n = true. Когда n равен 1, Nat.even n = false и проверка не выполняется, что приводит к первому сообщению об ошибке. Когда n равно 4, проверка завершается успешно.

Ситуация усложняется, когда n не константа, а произвольное выражение. Доказательство того, что Nat.even n = true может потребовать подробных рассуждений, которыми должен руководствоваться пользователь. Например, мы знаем, что Nat.even (n + n) = true для любого значения n, но Coq не знает. Таким образом, чтобы вызвать add_two_even что-то в форме n + n, нам нужно показать лемму.

Lemma add_n_n_even n : Nat.even (n + n) = true.
Proof.
induction n as [|n IH]; trivial.
now simpl; rewrite <- plus_n_Sm, IH.
Qed.

Definition foo (n : nat) :=
  add_two_even (exist _ (n + n) (add_n_n_even n)).

Есть некоторые инструменты для облегчения этого стиля программирования, такие как плагин уравнений, но общий Сообщество Coq считает, что вам следует избегать подмножеств типов для таких функций, как add_two_even, где ограничения существенно не упрощают свойства функции.

Вы можете найти множество примеров правильного использования подмножеств типов в библиотеках Mathematical Components. Например, библиотеки используют типы подмножества для определения типа n.-tuple T списков длины n и типа 'I_n целых чисел, ограниченных n. Это позволяет нам определить общую функцию доступа tnth (t : n.-tuple T) (i : 'I_n) : T, которая извлекает i-й элемент списка t. Если мы определяем этот метод доступа для произвольных списков и целых чисел, нам нужно передать значение по умолчанию функции, чтобы она возвращалась, когда индекс выходит за границы, или изменить подпись функции так, чтобы вместо этого она возвращала значение типа option T, указывая, что функция может не вернуть значение. Это изменение усложняет определение свойств функции доступа. Например, рассмотрим лемму eq_from_tnth, в которой говорится, что два списка равны, если все их элементы равны:

eq_from_tnth:
  forall (n : nat) (T : Type) (t1 t2 : n.-tuple T),
    (forall i : 'I_n, tnth t1 i = tnth t2 i) -> t1 = t2

Формулировка этой леммы для произвольных списков усложняется, потому что нам нужно дополнительное предположение о том, что два списка имеют одинаковый размер. (Здесь x0 - значение по умолчанию.)

eq_from_nth:
  forall (T : Type) (x0 : T) (s1 s2 : list T),
  size s1 = size s2 ->
  (forall i : nat, i < size s1 -> nth x0 s1 i = nth x0 s2 i) -> s1 = s2
person Arthur Azevedo De Amorim    schedule 14.11.2019
comment
Что вы имеете в виду, что общая мудрость состоит в том, чтобы не использовать типы подмножества? Что тогда использовать? Я думаю, что в mathcomp используются подмножества типов, и по уважительным причинам ими легче манипулировать, чем индексированно-индуктивными типами. - person Théo Winterhalter; 14.11.2019
comment
Да, библиотеки mathcomp предоставляют хороший образец использования для типов подмножеств. Я имел в виду, что, как правило, использование подмножества типа для такой функции, как add_two_even, - плохая идея, где добавленные ограничения на подпись, вероятно, не упростят свойства этой функции. Я постараюсь лучше объяснить это в своем ответе. - person Arthur Azevedo De Amorim; 14.11.2019