时间戳

首页 > 解决方案 > 语言环境：使用单元实例化时 Codegen 失败（code_pred：“战术失败”）

isabelle - 语言环境：使用单元实例化时 Codegen 失败（code_pred：“战术失败”）

问题描述

我正在尝试code_pred用于在语言环境中定义的归纳谓词。我遇到了这封电子邮件，其中显示了如何做到这一点：

locale l = fixes x :: 'a assumes "x = x"
inductive (in l) is_x where "is_x x"
global_interpretation i: l "0 :: nat" defines i_is_x = "i.is_x" by unfold_locales simp

declare i.is_x.intros[code_pred_intro]
code_pred i_is_x by(rule i.is_x.cases)

但是，当我将 更改global_interpretation为使用() :: unit而不是 时0 :: nat，将code_pred失败并显示以下消息：

Tactic failed
The error(s) above occurred for the goal statement⌂:
i_is_x_i x = Predicate.bind (Predicate.single x) (λx. case x of () ⇒ Predicate.single ())

我尝试手动进行证明，但在某些时候我得到了同样的错误。

有谁知道如何解决这个问题？

标签： isabelle

解决方案

我不完全理解这里发生了什么，但是代码生成器已经在内部使用了 unit 并且策略（对应于before single intro rule）在您的示例中失败了。

错误不是来自证明，而是来自done零件内部完成的证明。所以改变证明并不会改变问题（你甚至会很抱歉地看到）。

一种可能的解决方法：使用与单元同构的类型：

datatype myunit = MyUnit
locale l = fixes x :: 'a assumes "x = x"
inductive (in l) is_x where "is_x x"
definition X where ‹X = ()›
global_interpretation i: l "MyUnit :: myunit" defines i_is_x = "i.is_x" by unfold_locales simp

declare i.is_x.intros[code_pred_intro]

code_pred  i_is_x
  by (rule i.is_x.cases)

推荐阅读