勒柯克：？使用「改寫」或「應用」

在證明，我想簡化(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

勒柯克：？使用 「改寫」 或 「應用」

回答

相關問題

勒柯克：？使用「改寫」或「應用」