Mutualy recursive function and termination checker in Coq
coq, totality
Solution
Mutual recursion is to be used either with a single inductive data-type or with different inductive data-types that have been defined together in a single inductive definition. In your case, you are using polymorphic data-types prod (the type of pairs), list, and option which were already defined before dpProof.
The nested fixpoint approach does not have the restriction.
Problem
EDIT ``` 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. ``` I got an error message saying that: Recursive call to dpProof has principal argument equal to ``` "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". ``` If I do not use the mutual recursive and use the nested fixpoint, it will combine and pass the checker of termination. Here is the code that successfully combined. ``` 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. ``` I would like to understand deeper about the reason why it cannot pass the termination checker? Is it because they cannot guess the argument descreasing? Is there any way that I can use the mutually recursive to express my function `dpGraphProc`? Also How can I write the function `dpGraphProc` that check in the whole list? Here I do not know how to use the argument `cs'`.