У этой проблемы есть два сложных аспекта.
- Программирование с независимой типизацией с индексированными типами в Coq
- Вложенные рекурсивные типы
Программирование с независимой типизациейс индексированными типами в Coq
Под «индексированным типом» я имею в виду конкретно индуктивные типы, такие как Vector.t, где конструкторы уточняют некоторые аргументы типа.Эти аргументы называются индексами и должны появляться между : и := в сигнатуре типа:
Inductive Vector.t (A : Type) : nat (* <- index *) -> Type :=
| nil : Vector.t A 0
| cons : A -> forall n, Vector.t A n -> Vector.t A (S n).
Индексированные индуктивные типы очень полезны для определения предложений, где термины не имеют значения.Но для фактических данных короткая история здесь: не делайте этого.Это технически возможно, но это очень глубокая кроличья нора, и работать с ней в целом довольно сложно, во многом потому, что зависимое сопоставление с образцом в Coq является такой не интуитивной конструкцией.Например, см. Этот пост в блоге: https://homes.cs.washington.edu/~jrw12/dep-destruct.html
Менее экстремальное решение - отказаться от других «зависимо-типизированных» аспектов этой программы.Следующим кандидатом на рубку здесь является sumbool ({ _ } + { _ }).Если функции (и параметры) вместо этого возвращают bool, это делает их достаточно простыми для определения (* кашель *, см. Следующий раздел).Доказательство их правильности все еще является проблемой, но, по крайней мере, у вас есть что вычислить.
Две основные альтернативы индуктивным индексированным типам:
Просто используйте плоскую версию (list вместо vec), отказавшись от некоторых гарантий «по конструкции».
Сделайте тип функцией индексов как Definition (или Fixpoint)вместо Inductive.Здесь мы используем unit и prod в качестве строительных блоков для таких типов, но вам, возможно, придется придумать свои собственные для более сложных типов.Потребуется много зависимого сопоставления с образцом.
Fixpoint vec (A : Type) (n : nat) := match n with
| O => unit | S n => (A * vec n)%type
end.
Возможно, вы захотите пересмотреть представление языка, который вы хотите реализовать.Например, вы действительно хотите представлять арности так же явно, как функцию для символов?(Это, безусловно, может иметь место.) Например, не могли бы вы ограничить это символами арности 0, 1, 2?
Вложенные рекурсивные типы
Это рекурсивные типы, рекурсивные вхождения которыхвнутри других типов данных (которые могут быть рекурсивными).Чтобы упростить обсуждение, снять загромождение кода и из-за вышеупомянутых проблем с зависимыми типами в Coq, рассмотрите следующий тип, используя list вместо vec и с одним меньшим количеством конструктора:
Inductive LTree : Type :=
| funTerm : list LTree -> LTree.
Вы можете определить рекурсивные функции для такого типа с помощью Fixpoint, но вы должны быть особенно осторожны с тем, как рекурсивные вызовы вкладываются.Конечно, это действительно имеет значение для любого рекурсивного типа, но шаблон гораздо более естественный, когда рекурсия не является вложенной, поэтому проблема менее заметна.
Ниже показано, как мы можем определить равенство для LTree.Мы отказываемся от зависимого sumbool, возвращая вместо него bool.Определение dec_list является стандартным и общим.
Require Import List.
Import ListNotations.
Section List.
Context {A : Type} (decA : A -> A -> bool).
Fixpoint dec_list (l l' : list A) : bool :=
match l, l' ith
| [], [] => true
| a :: l0, a' :: l0' =>
decA a a' && dec_list l0 l0'
| _, _ => false
end.
End List.
Тогда равенство LTree выглядит невинным ...
Fixpoint decLTree (x y : LTree) : bool :=
match x, y with
| funTerm lx, funTerm ly =>
dec_list decLTree lx ly
end.
... но есть очень тонкие детали, которыенужно знать, чтобы убедить Coq в том, что рекурсия структурно уменьшается.
Правильность decLTree определенно очень тонко зависит от того, как dec_list использует свой аргумент decA, поэтомуdec_list должно быть прозрачным определением:
Он применяется только к подтерме первого списка (вы можете сделать его вторым, если хотите, с некоторыми аннотациями struct).
decA связан вне из Fixpoint dec_list.Функция decLTree не будет правильно сформирована, если вместо этой строки будет читать Fixpoint dec_list {A : Type} (decA : A -> A -> bool).
Также можно упаковать эти трюки, написав некоторые общие схемы рекурсии / индукции для LTree / VTree.