#recursion #coq
#рекурсия #coq
Вопрос:
Я создал следующие индуктивные типы данных и рекурсивные функции.
Require Coq.Lists.List.
Inductive PairTree : Type :=
| PTLeaf : PairTree
| PTBranch : (nat*nat) -> PairTree -> PairTree -> PairTree.
Fixpoint smush (r m : list nat) : list nat :=
match m with
| nil => r
| h :: t => smush (h :: r) t
end.
Я определил следующую функцию, используя их, со вспомогательным параметром «gas», чтобы правила завершения Coq легко выполнялись.
Fixpoint fueled_prefix_part (gas : nat) (r m : list nat) : PairTree :=
match gas with
| 0 => PTLeaf
| S gas' =>
match r with
| nil => PTLeaf
| f :: fs =>
match fs with
| nil => PTLeaf
| f' :: fs' =>
PTBranch (f, f')
(fueled_prefix_part gas' (smush fs' m) nil)
(fueled_prefix_part gas' (f :: fs') (f' :: m))
end
end
end.
Тем не менее, я хотел извлечь фактический код из этого и запустить его. Таким образом, вместо структурной рекурсии в gas я мог бы получить более приятный извлеченный код, если бы вместо этого я мог использовать следующий код, поскольку тогда я мог бы использовать какой-либо другой nat-подобный тип данных с < (например, целые числа Haskell).
Require Import Recdef.
Require Export Coq.omega.Omega.
Require Export Coq.Lists.List.
(* Insert definitions of PairTree and smush here. *)
Function fpp' (gas: nat) (r m: list nat) {measure (fun x => x) gas}: PairTree :=
match 0 <? gas with
| false => PTLeaf
| true =>
match r with
| nil => PTLeaf
| f :: fs =>
match fs with
| nil => PTLeaf
| f' :: fs' =>
let gas' := gas - 1 in
PTBranch (f, f')
(fpp' gas' (smush fs' m) nil)
(fpp' gas' (f :: fs') (f' :: m))
end
end
end.
Конечно, мы не можем на этом закончить; мы должны доказать, что это заканчивается. Следующее, по-видимому, доказывает завершение…
Proof.
intro gas. destruct gas; intros _ _ teq _ _ _ _ _ _.
inversion teq.
omega.
intro gas. destruct gas; intros _ _ teq _ _ _ _ _ _.
inversion teq.
omega.
На данный момент в ProofGeneral я не вижу целей на экране цели, а на экране ответа я вижу сообщение
No more subgoals.
(dependent evars:)
Итак, я ввожу
Defined.
и получите сообщение об ошибке
Toplevel input, characters 0-8:
Error: Attempt to save a proof with shelved goals (in proof fpp'_terminate)
Что, черт возьми, происходит? Если я наберу
Unshelve.
Defined.
Я получаю ту же ошибку.
Комментарии:
1. После небольшого расследования очень вероятно, что это ошибка Coq, не могли бы вы сообщить об этом в Coq bugzilla?