Рассмотрим следующую пару взаимно рекурсивных типов данных Coq, которые представляют Forest непустых Tree с.Каждый Branch из Tree содержит дополнительный логический флаг, который мы можем извлечь с помощью isOK.
Inductive Forest a : Type
:= Empty : Forest a
| WithTree : Tree a -> Forest a -> Forest a
with Tree a : Type
:= Branch : bool -> a -> Forest a -> Tree a.
Arguments Empty {_}.
Arguments WithTree {_} _ _.
Arguments Branch {_} _ _ _.
Definition isOK {a} (t : Tree a) : bool :=
match t with
| Branch ok _ _ => ok
end.
Теперь, если мы проигнорируем этот логический флаг, мы можем написать пару функций отображенияприменить функцию к каждому значению в Forest или Tree, и это прекрасно работает:
Fixpoint mapForest_always {a} (f : a -> a) (ts0 : Forest a) {struct ts0} : Forest a :=
match ts0 with
| Empty => Empty
| WithTree t ts => WithTree (mapTree_always f t) (mapForest_always f ts)
end
with mapTree_always {a} (f : a -> a) (t : Tree a) {struct t} : Tree a :=
match t with
| Branch ok x ts => Branch ok (f x) (mapForest_always f ts)
end.
Однако, предположим, что логическое значение представляет некоторую проверку достоверности, которая была бы более сложной в реальном коде,Таким образом, мы сначала проверяем логическое значение, и рекурсивно только в случае необходимости.Это означает, что у нас есть три взаимно рекурсивные функции, но одна из них просто передает работу.К сожалению, это не работает:
Fail Fixpoint mapForest_bad {a} (f : a -> a) (ts0 : Forest a) {struct ts0} : Forest a :=
match ts0 with
| Empty => Empty
| WithTree t ts => WithTree (mapTree_bad f t) (mapForest_bad f ts)
end
with mapTree_bad {a} (f : a -> a) (t : Tree a) {struct t} : Tree a :=
if isOK t
then mapOKTree_bad f t
else t
with mapOKTree_bad {a} (f : a -> a) (t : Tree a) {struct t} : Tree a :=
match t with
| Branch ok x ts => Branch ok (f x) (mapForest_bad f ts)
end.
Проблема в том, что mapTree_bad вызывает mapOKTree_bad с аргументом, который на самом деле не меньше.
За исключением ... всех mapOKTree_bad делает это дополнительный шаг после некоторой предварительной обработки.Это будет всегда завершаться, но Coq этого не видит.Чтобы убедить средство проверки завершения, мы можем вместо этого определить mapOKTree_good, который является тем же самым, но является локальной let -связью;затем средство проверки завершения проследит через привязку let и позволит нам определить mapForest_good и mapTree_good.Если мы хотим получить mapOKTree_good, мы можем просто использовать простое старое определение после того, как мы определили взаимно рекурсивные функции, которые имеют то же тело, что и привязка let:
Fixpoint mapForest_good {a} (f : a -> a) (ts0 : Forest a) {struct ts0} : Forest a :=
match ts0 with
| Empty => Empty
| WithTree t ts => WithTree (mapTree_good f t) (mapForest_good f ts)
end
with mapTree_good {a} (f : a -> a) (t : Tree a) {struct t} : Tree a :=
let mapOKTree_good {a} (f : a -> a) (t : Tree a) : Tree a :=
match t with
| Branch ok x ts => Branch ok (f x) (mapForest_good f ts)
end in
if isOK t
then mapOKTree_good f t
else t.
Definition mapOKTree_good {a} (f : a -> a) (t : Tree a) : Tree a :=
match t with
| Branch ok x ts => Branch ok (f x) (mapForest_good f ts)
end.
Это работает, но это не красиво.Есть ли способ убедить программу проверки завершения Coq принять варианты _bad, или трюк _good лучший из всех, что у меня есть?Команда, которая работает для меня, такая как Program Fixpoint или Function, также является вполне разумным решением.