勒柯克：？使用 “改写” 或 “应用”

在证明，我想简化(negb (negb true))到true（同样与false）简化（negb（neqb真）为true勒柯克：？使用 “改写” 或 “应用”

我知道勒柯克的negb_involutive程序，但因为我的书还没有出台，我认为我应该以某种方式管理使用仅rewrite或apply模仿它的功能。

来源

2016-11-14 Shuzheng

你不允许使用'simpl.'？此外，'negb（negb true）= true'可以通过'反身性'来证明，因为左边和右边的定义是相等的。 –

之前没有使用过“简单”，但也许我应该考虑一下。 – Shuzheng

我觉得现在应该已经足够了。还有一个更强大的策略'计算'，但它可能会创造更大的条件。你可能想看看这个不错的[cheatsheet]（http://adam.chlipala.net/itp/tactic-reference.html）。 –

安东说，要解决这一目标的典型程序是使用reflexivity，或其低级版本apply eq_refl。

回想一下，勒柯克是基于一种编程语言，在这种情况下，确实~~ (~~ true)执行很容易看出是true（其中我缩写~~ x = negb x），以同样的方式，将在Python或C.

返回trueapply eq_refl将解决这个目标，因为Coq在绑定时会尝试“计算”或“减少”条件以使匹配成功。 eq_refl的类型是forall x, x = x，因此当~~ (~~ true)减少到true时，您的目标现在变为true = true并且可以解决。在这种情况下，simpl只会降低您看到它的目标，但在技术上不需要证明。

在你的案例中应用negb_involutive不是惯用的，当negb的参数是一个变量时，这个引理是有用的，就像在~~ (~~ (~~ x)) = ~~ x中一样。

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

来源

2016-11-14 17:54:12 ejgallego

勒柯克：？使用 “改写” 或 “应用”

回答

相关问题