coq - 产品类型上的相互递归函数
问题描述
(初学者 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).
解决方案
一种解决方案可能是进行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.
推荐阅读
- php - 表格未显示动态值
- cmake - 如何为 yocto poky 添加库?
- jwt - 无法使用从 AzureKeyVault 读取的证书写入 JWTToken
- events - 如何将点击/点击事件添加到 AmCharts 4 Range?(ValueAxisDataItem)
- rust - rust 寿命问题,为什么第一次调用没有编译错误?
- ansible - 如何使用 Ansible 获取主机 IP 和主机名
- elasticsearch - 如何过滤top hits聚合结果
- css - 有没有办法在 JavaFX 中实现这个 CSS 动画?
- python-3.x - 当我在 settings.py 中关闭调试模式时,它返回一个错误的请求(400)
- android - 如何通过凌空传递整数或双精度值