产品类型的相互递归函数

Felipe 发表于 Dev

费利佩

（初学者Coq问题）

与在产品类型上定义递归函数有关，我正在尝试在产品类型上定义递归函数。这里的区别是存在一个相互递归的定义。我一直遇到这个错误：

printObjItem的递归定义格式不正确。

递归调用printJson的主参数等于“ val”，而不是“ 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).

安东·特鲁诺夫（Anton Trunov）

一种解决方案可能是进行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.

本文收集自互联网，转载请注明来源。

如有侵权，请联系 [email protected] 删除。