Mutualy recursive function and termination checker in Coq

Question

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'.

There are quite a lot of undeclared identifiers in your code snippet, and it does not contain any occurrence of p2 which is mentioned in your error message. Could you provide an example that leads exactly to said message? — Virgile
This time I edited and test the code combined and provide the error. Thank you for your patient. — Quyen

Yves Yves · Accepted Answer · 2012-11-08T12:13:31

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.

Mutualy recursive function and termination checker in Coq

1 Answers