編集
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'
。