Взаимная рекурсивная функция и проверка завершения в Coq

Question

РЕДАКТИРОВАТЬ

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

Answer 1

Взаимная рекурсия должна использоваться либо с одним индуктивным типом данных, либо с различными индуктивными типами данных, которые были определены вместе в одном индуктивном определении. В вашем случае вы используете полиморфные типы данных prod (тип пар), список и опцию, которые уже были определены до dpProof.

Вложенный подход с фиксированной точкой не имеет ограничений.