Coq 错误：无法将“true”与“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 扩展的复杂性），则两个术语是可转换的。

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