产品类型的相互递归函数

Question

（初学者 Coq 问题）

与有关，我正在尝试定义一个产品类型的递归函数。这里的区别在于有一个相互递归的定义。我一直运行进入这个错误：

Recursive definition of printObjItem is ill-formed.

Recursive call to printJson has principal argument equal to "val" instead of a subterm of "item".

从概念上讲，递归似乎应该通过，因为 val 是 item 的子项，是 items 的子项，是 x 的子项。我知道 Coq 正在为第一个断言而苦苦挣扎，但我不确定如何解决。有没有明确的充分依据证明的直接方法？

Require Import List.
Require Import String.
Import ListNotations.

Inductive Json :=
  | Atom : Json
  | String : string -> Json
  | Array : nat -> list Json -> Json
  | Object : list (string * Json) -> Json.

Fixpoint printJson (x : Json) :=
  match x with
  | Atom => "atom"
  | String n => "'" ++ n ++ "'"
  | Array _ els => "[" ++ (String.concat ", " (map printJson els)) ++ "]"
  | Object items => "{" ++ (String.concat ", " (map printObjItem items)) ++ "}"
  end%string
with printObjItem (item : string * Json) :=
       let (key, val) := item in key ++ ": " ++ (printJson val).

Answer 1

一个解决方案是使 printObjItem 成为本地定义：

Fixpoint printJson (x : Json) :=
  let printObjItem (item : string * Json) :=
    (let (key, val) := item in key ++ ": " ++ (printJson val))%string
  in
  match x with
  | Atom => "atom"
  | String n => "'" ++ n ++ "'"
  | Array _ els => "[" ++ (String.concat ", " (map printJson els)) ++ "]"
  | Object items => "{" ++ (String.concat ", " (map printObjItem items)) ++ "}"
  end%string.

产品类型的相互递归函数

Mutually recursive functions over product type

coq

mutual-recursion