用Coq中归纳谓词的递归定义函数

问题是,您需要在证明中包含信息来构建树。具体来说,你需要一些拆分 (s1, s2) 因此 s1 ++ s2 = s /\ s1 <<- e1 /\ s2 <<- e2 . 该分割必须通过计算来定义,而不是从证明中提取适当的分割 H: s1 <<- e1 @ e2 .

解决此问题的最简单方法是 in_regex 在里面 Type ,以匹配Agda开发的工作方式。这意味着 in\u regex 必须通过计算构建,因此您可以自由匹配。

Inductive in_regex : string -> regex -> Type

使用 not 在里面 empty_in_regex_inv 休息,但你可以写 s <<- #0 -> False .

感谢Ben Sherman指出了这个解决方案!

也可以保持 in\u regex 在里面 Prop ,但您需要一种单独的匹配正则表达式的计算方法来计算拆分,然后需要一个将此函数与 in\u regex .