0

我试图在 Coq 中证明一个定理，但我无法解决出现的问题。我正在尝试解决：

 forall A B C: Prop, A\/(B\/C)->(A\/B)\/C.
Proof.
intros.
destruct H as [H1 | [H2 | H3 ]].
Case H1.
and in this last line I get the following error "Error: The reference Case was not found in the current environment."

我是 Coq 的新手，所以我不知道这到底意味着什么。我在互联网上做了一些研究，但我没有设法找到解决方案。有谁知道这个问题来自哪里？

4

2 回答 2

2

你已经破坏了假设，所以你已经在分析每个案例。

使用leftandright来操纵结论中的析取，assumption当假设和结论相同时。

于 2012-11-25T15:23:48.373 回答
1

编辑：嗯...我可能误解了您实际上在这里尝试做的事情...

您正在使用并且可能已经在Case其他地方看到使用的不是 Coq 构建的，而是一个在 Coq 生态系统中漂浮的库。

我可以在这里找到它的参考：http ://coq.inria.fr/cocorico/Case%20(tactic )

我个人也用过。要使用它，您需要将该链接中的定义复制到文件中的某个位置，或者复制到MyCaseModule.v您导入的另一个文件中：

Require Import MyCaseModule.

作为旁注，Coq 8.4 似乎提供了另一种使用项目符号构建证明的方法。我不知道具体细节，因为其他原因我一直使用 8.3。但是，您可能仍然更喜欢 Case/SCase/... 因为它能够为不同的案例命名。

于 2012-11-26T03:01:14.940 回答