Mutually recursive functions over product type

Question

(Beginner Coq question)

Related to Defining recursive function over product type, I'm trying to define a recursive function over a product type. The difference here is there's a mutually recursive definition. I keep running into this error:

Recursive definition of printObjItem is ill-formed.

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

Conceptually it seems the recursion should go through since val is a subterm of item, is a subterm of items, is a subterm of x. I understand Coq is struggling with that first assertion but I'm not sure how to resolve. Is there a straightforward way without an explicit well-foundedness proof?

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

One solution could be to make printObjItem a local definition:

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.