Coq error: Unable to unify "true" with "is_true (0 < a - b - 3)"

Question

不确定我做错了什么，但我认为 reflexivity 应该在下面工作，但事实并非如此。

a, b : nat
H : (1 <=? a - b - 3) = true
______________________________________(1/7)
is_true (0 < a - b - 3)

我也尝试 apply leb_complete in H. 结果是：

a, b : nat
H : (1 <= a - b - 3)%coq_nat
______________________________________(1/7)
is_true (0 < a - b - 3)

但在这两种情况下，Coq 都会给我一个错误提示 Unable to unify "true" with "is_true (0 < a - b - 3)"

应该没那么复杂吧？我在这里遗漏了什么吗？

Answer 1

首先，“它不应该很复杂”是错误的问题。

reflexivity 是一种从不使用假设的策略，它试图以非常具体的方式证明目标。对于“简单”的纯数字目标 p，您可以使用 lia。

它只能证明目标可转换为形状 R a1 a2 其中 R 是自反关系（如相等）并且 a1 和 a2 是可转换的。如果将两个项简化为标准形式给出“相同”的结果（模数 eta-expansion 的一些并发症），则两个项是可转换的。

例如，自反性可以证明2 + 2 + 0 = 4，或者0 + n = n。但是不能证明n+0=n（可以用lia证明），因为n+0是范式

coq