coq - 積の種類に対する相互再帰関数

Question

(Coq の初歩的な質問)

製品タイプに対する再帰関数の定義に関連して、製品タイプに対する再帰関数を定義しようとしています。ここでの違いは、相互に再帰的な定義があることです。私はこのエラーに遭遇し続けます:

printObjItem の再帰的な定義の形式が正しくありません。

printJson への再帰呼び出しには、「item」のサブタームではなく、「val」に等しい主要な引数があります。

概念的には、 は のサブ項であり、 は のサブ項であり、 は のサブ項であるため、再帰を実行する必要が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).