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

问题描述

我试图将code_pred用于在语言环境中定义的归纳谓词。我碰到了email，它显示了如何完成此操作：

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 ())

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

有人知道如何解决吗？

解决方法

我不完全了解这里发生的情况，但是代码生成器已经在内部使用了单位，因此您的示例中的策略（对应于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)