-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