Отделение данных, которыми нужно манипулировать, от доказательств того, что манипуляции оправданы.

У меня есть тип списков, головы и хвосты которых должны быть в определенном смысле "совместимы":

Inductive tag := A | B. (* Just an example *)

Inductive element : tag -> tag -> Set :=
  | AA : element A A
  | AB : element A B
  | BB : element B B. (* Also just an example *)

Inductive estack : tag -> tag -> Set :=
  | ENil  : forall     t,                              estack t t
  | ECons : forall r s t, element r s -> estack s t -> estack r t.

Однако мне этот код не очень нравится по следующим причинам:

  1. Он не является модульным: конструкторы специальных списков данных неразрывно связаны с доказательствами совместимости орла и решки — тегами.
  2. Это не одобряет повторное использование кода: я вынужден переопределить обычные функции списка (например, конкатенацию списков) и повторно доказать обычные теоремы о списках (такие как ассоциативность конкатенации списков).

Я имею в виду другой подход, который состоит из трех шагов:

  1. Определение одного типа теговых элементов (в отличие от семейства теговых типов элементов):

    Inductive taggedElement := Tagged : forall t1 t2, element t1 t2 -> taggedElement.

  2. Определение типа произвольных (т. е. действительных или недействительных) списков тегированных элементов:

    Definition taggedElementStack := list taggedElement.

  3. Определение действительного списка помеченных элементов как кортежа, элементы которого являются произвольным списком помеченных элементов и доказательством того, что элементы совместимы с соседними.

    (* I have no idea how to do this in Coq, hence the question!
 * 
 * I am going to use pseudomathematical notation. I am not well versed in either
 * mathematics or theoretical computer science, so please do not beat me with a
 * stick if I say something that is completely bogus!
 * 
 * I want to construct the type
 * 
 *     (tes : taggedElementStack, b : proof that P(tes) holds)
 * 
 * where P(tes) is a predicate that is only true when, for every sublist of tes,
 * including tes itself, the heads and tails are compatible.
 *)

Как мне выполнить третий шаг в Coq?


coq
person pyon    schedule 11.09.2012    source источник

Ответы (1)


arrow_upward
2
arrow_downward

Посмотрите на свой estack, что он делает? Обобщай! element — это просто отношение (A -> A -> Set), tag — это просто Set. Что вы получаете?

Inductive RTList {I : Set} (X : Rel I) : Rel I :=
  | RTNil  : forall {i : I}, RTList X i i
  | RTCons : forall {i j k : I},    X i j -> RTList X j k -> RTList X i k.

(Rel — это просто определение с Rel I = I -> I -> Set.)

Рефлексивно-транзитивное замыкание! Это является общим, многоразовым и модульным. Или так вы думаете.

Единственная реализация, которую я нашел в библиотеках Coq, находится в Coq.Relations.Relation_Operators и называется clos_refl_trans, по-другому устроен и заперт в Prop (все по документам, не пробовал).

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

С другой вашей идеей, вероятно, будет сложнее справиться. Посмотрите на NoDup что-то похожее на ваше описание. возможность повторного использования шаблона. Если ты действительно этого хочешь. NoDup использует In — функция, проверяющая наличие элемента в списке. В прошлый раз, когда я пытался использовать его, мне было значительно труднее решать доказательства, включающие In. Вы не можете просто destruct, но должны применять вспомогательные леммы, вам нужно аккуратно развернуть ровно $n уровней, свернуть назад сложно и т. д. и т. д. Я бы посоветовал, если это действительно не необходимо, вам лучше придерживаться типов данных для Propс.

person nobody    schedule 13.09.2012