ИЗМЕНИТЬ
Require Import Bool List ZArith.
Variable A: Type.
Inductive error :=
| Todo.
Inductive result (A : Type) : Type :=
Ok : A -> result A | Ko : error -> result A.
Variable bool_of_result : result A -> bool.
Variable rules : Type.
Variable boolean : Type.
Variable positiveInteger : Type.
Variable OK: result unit.
Definition dps := rules.
Inductive dpProof :=
| DpProof_depGraphProc : list
(dps * boolean * option (list positiveInteger) * option dpProof) -> dpProof.
Fixpoint dpProof' (R D: rules) (p: dpProof) {struct p}:=
match p with
| DpProof_depGraphProc cs => dpGraphProc R D cs
end
with dpGraphProc (R D: rules ) cs {struct cs} :=
match cs with
| nil => Ko unit Todo
| (_, _, _, op) :: cs' =>
match op with
| None => Ko unit Todo
| Some p2 => dpProof' R D p2
end
end.
Я получил сообщение об ошибке: Рекурсивный вызов dpProof имеет главный аргумент, равный
"p2" instead of "cs'".
Recursive definition is:
"fun (R D : rules)
(cs : list
(dps * boolean * option (list positiveInteger) *
option dpProof)) =>
match cs with
| nil => Ko unit Todo
| (_, _, _, Some p2) :: _ => dpProof' R D p2
| (_, _, _, None) :: _ => OK
end".
Если я не использую взаимную рекурсию и использую вложенную фиксированную точку, она объединится и пройдет проверку завершения. Вот код, который успешно скомбинирован.
Fixpoint dpProof' (R D: rules) (p: dpProof) {struct p}:=
match p with
| DpProof_depGraphProc cs =>
match cs with
| nil => Ko _ Todo
| (_, _, _, op) :: cs' =>
match op with
| None => Ko unit Todo
| Some p2 => dpProof' R D p2
end
end end.
Я хотел бы глубже понять причину, по которой он не может пройти проверку завершения? Это потому, что они не могут догадаться, что аргумент убывает? Есть ли способ использовать взаимно-рекурсивное выражение для выражения моей функции dpGraphProc
?
Также как я могу написать функцию dpGraphProc
, которая проверяет весь список? Здесь я не знаю, как использовать аргумент cs'
.
p2
, упомянутого в вашем сообщении об ошибке. Не могли бы вы привести пример, который ведет именно к указанному сообщению? - person Virgile   schedule 08.11.2012