functional-programming - Coq：使用“重写”或“应用”将 (negb (neqb true) 简化为 true？

Question

在证明中，我想简化(negb (negb true))为true（同样使用false）。

我知道 Coq 的negb_involutive程序，但由于我的教科书没有介绍它，我认为我应该设法仅使用rewriteor来模仿它的功能apply。

Answer 1

正如 Anton 所说，解决此目标的典型程序是使用reflexivity或其较低级别的版本apply eq_refl。

回想一下，Coq 是基于一种编程语言的，在这种情况下，确实~~ (~~ true)可以很容易地看到的执行true（我缩写~~ x = negb x），就像它true在 Python 或 C 中返回的方式一样。

apply eq_refl将解决目标，因为 Coq 将尝试“计算”或“减少”项，以使事物匹配。eq_reflis的类型forall x, x = x，因此 when~~ (~~ true)减少到true您的目标现在变成true = true并且可以解决。在这种情况下，simpl只会减少您看到它的目标，但在证明中技术上不需要它。

在您的情况下应用并不习惯，negb_involutive当参数为变量时，此引理很有用negb，例如 in ~~ (~~ (~~ x)) = ~~ x。

你会发现自己rewrite在大多数涉及平等的目标中使用。