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

2016-11-14 98 views 1 likes

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

相關問題

11. 分型在勒柯克
12. 勒柯克「護航模式」
13. 串地圖和勒柯克
14. 勒柯克：替代和依賴類型
15. 消除與命題案件勒柯克
16. 勒柯克實數-lexing和解析3.14
17. 勒柯克 - 證明涉及bigops在Ssreflect
18. 勒柯克：找不到庫Jessie_memory_model在loadpath
19. 如何使用來定義勒柯克符號格式{
20. 幫助與勒柯克證明了亞
21. 如何編譯Logic.v在勒柯克
22. 通過勒柯克困惑進口
23. 在勒柯克，如何構建「SIG」型
24. 奇lambda語法在勒柯克
25. 雷亞爾和定理勒柯克
26. 轉換NAT在勒柯克提取big_int到Ocaml程序編寫
27. 獲得更強的感應原理在勒柯克
28. 在勒柯克（安全第n個功能）使用相關類型
29. 如何使用勒柯克GenericMinMax來證明事實有關雷亞爾
30. 勒柯克的測算風格的雙條件鏈

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

回答

相關問題

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