coq - Require Import Omega 后 bool 和 Datatypes.bool 的混淆

Question

我正在研究软件基础并遇到错误。

错误：术语“true”的类型为“bool”，而预期的类型为“Datatypes.bool”

为下面的证明。

Theorem beq_nat_true : forall n m,
  beq_nat n m = true -> n = m.

我发现当我使用Require Import Omega. 对环境中引入
的内容有任何提示、建议或解释吗？Omega

Answer 1

该Omega模块间接导入了许多操纵自然数的标准库定义，其中一些最终影响了软件基础的部分内容。beq_nat功能就是其中之一。出现问题是因为标准库的版本beq_nat返回标准布尔值，而 SF 的版本返回其重新定义的布尔值。

我们前段时间注意到了这个问题，并且已经在当前版本中修复了它。如果您不想重新下载所有内容（或者如果您自己导入Omega了），您也可以beq_nat使用正确的版本。我的猜测是这Basics.beq_nat应该有效。