-2
我不知道我必須使用什麼策略來證明該模板。 我嘗試了兩種方法，但我被困在了兩個。coq我應該使用什麼策略？答：Prop，A - > ~~ A
Lemma Exo17 : forall A : Prop, ~~(A \/ ~A).
Proof.
Methode 1
intro.
unfold not.
intro.
Methode 2
intro.
intro.
case H.
A
回答
7
這種情況最好的策略叫做「筆和紙」。事實上，你應該先嚐試手動建立證明[intuitionistic sequent calculus LJ應該爲此目的正常工作]。
一旦你清楚瞭解證明的工作方式，在Coq中編碼它將是微不足道的。
+3
鉛筆比筆更好，以防萬一出錯。 :-) –
+0
根據問題的標題，我不清楚提問者是否知道「微不足道」的策略。 –
+0
你好，我沒有看到我應該做直觀的LJ序列計算^^。我不知道這些戰術是否微不足道，在文檔中它說它解決了像X = X這樣的微小平等，但是我在哪裏可以在代碼中使用它。我在這個假設中遇到了A \ /（A - > False） - > False。 –
0
嘗試使用intuition來解決問題，然後Print Exo17找出解決方案是什麼。
+1
「直覺」經常產生次優的證明術語，這當然是可以理解的。我想人們必須親自去做這樣的任務才能更好地掌握這個主題。 –
+1
我接受了'直覺'的輸出，並將其削減直到我明白髮生了什麼。否則我不會考慮使用這個假設！ –
相關問題
- 1. 爲什麼我不能使用`Show a => [Something - > a]`類型？
- 2. 應該是什麼回聲++ $ A + $ A ++
- 3. 我該如何說服coq（A/\ B）/ \ C == A/\ B/\ C？
- 4. 我應該在F＃中使用Nullable <'a>還是Option <'a>？
- 5. 爲什麼fold會預期（a - > b - > a）而不是（b - > a - > a）？
- 6. 我該怎麼做<a href>?
- 7. Coq「本地應用策略」的正確用法是什麼？
- 8. 爲什麼`[1，「a」] :: [forall a。顯示a => a]`不允許？
- 9. Coq證明策略
- 10. 我應該使用什麼策略來加密web.config部分？
- 11. 爲什麼ghci輸出（Num a）=> a for：t 4而不是（Ord a）=> a？
- 12. Coq：如何證明「a = b - > nat_compare a b = Eq。」？
- 13. 爲什麼（。）頭的類型（（a - > [c]） - > a - > c）？
- 14. 這是什麼意思？公式一=> A - > [A] - >布爾
- 15. 什麼是後{a = 5; A = A ++; Syso（a）;}
- 16. A a有什麼區別？和A a（）;？
- 17. A = A〜= 0是做什麼的，我該如何指定它？
- 18. 什麼是Haskell`（ - >）a` monad？
- 19. 什麼是A＆B代表.Aggregate（（a，b）=>聲明w/a＆b）
- 20. 什麼是Haskell中的'（float a，Num（a - > a））'？
- 21. [a - > a] - >（a - > a）的最慣用的實現`
- 22. 什麼是ocaml類型'a。 'a - >'是什麼意思？
- 23. Haskell sequencelistIO [a - > IO a] - > a - > IO
- 24. <a></a><a></a>標籤
- 25. Monad m => a - > [a - > m a] - > m a
- 26. 爲什麼要在EmberJS中使用{{＃link-to}}而不是<a></a>？
- 27. ArrayList <Integer> a [];有什麼區別？和ArrayList <Integer> a ;?
- 28. href表達式<a href="javascript:;"></a>做什麼？
- 29. <a href="#">Click here</a>是什麼意思？
- 30. 什麼是<a href="?request=register"> Register</a>中的href？
這功課嗎？ –
我同意這看起來像作業。 – Yves