我想用这种destruct策略来证明一个案例。我在网上阅读了几个例子，我很困惑。有人可以更好地解释吗？

这是一个小例子（还有其他方法可以解决它，但请尝试使用destruct）：

现在一些在线示例建议执行以下操作：

在这种情况下，我得到：

所以，我想证明前两种情况是不可能的。但是机器将它们列为子目标并希望我证明它们……这是不可能的。

摘要：如何准确丢弃不可能的情况？

我看过一些例子，inversion但我不明白这个过程。

最后，如果我的引理依赖于几种归纳类型并且我仍然想涵盖所有情况会发生什么？

我的 Coq 证明有问题，希望得到一些帮助和指导。我的部分定义如下：

我想说“组件术语必须是连接的客户端或服务器；但不能同时是两者。” 我在 Coq 中提出了以下内容作为上述内容的表示（基于我上面的定义）：

但是，我不确定这是否正确（是吗？），因为当我得到证明时，我陷入了困境

的类型HotelRes确实是组件（在这种情况下，HotelRes是连接的客户端），但是，由于这不在假设集中，我不能使用确切或自动策略之类的东西。

我怎么能继续这样的证明？

我在本地上下文中有一个假设，我们称其H为true=true -> conclusion. 我可以使用哪种策略来放弃前提而只保留结论？

我正在考虑在 Coq 中编写代码并提取此代码以用于大型 Haskell 项目。我想在 Coq 中构建一个模块，证明属性，然后使用 Haskell 的模块系统来防止违反这些属性（通过智能构造函数）。

我找不到任何迹象表明可以将 Coq 代码提取到具有显式导出列表的 Haskell 模块中。看来我必须手动修改提取的 Coq 代码，这没什么大不了的，但我想知道我是否有这个权利。有人有替代方案吗？

我在从 Coq 中的模块导入定义时遇到问题。我是 Coq 的新手，但无法使用该语言的参考手册或在线教程解决问题。我有一个模块，它定义了有限集的签名和公理，我打算在另一个模块中实现。还有更多，但它看起来像这样（作为参考，我正在密切关注 Filliatre 关于有限自动机的论文）：

我使用命令编译模块coqc并尝试将其加载到另一个模块中，例如FinSetListor 。当我尝试导入模块时，Coq（通过 Proof General）发出警告：FinSetRBTRequire Import FinSet

此外，我看不到FinSet. 如何将定义（在本例中为公理）从一个模块导入另一个模块？我基本上遵循了 Pierce 的“软件基础”讲座中概述的步骤。但是，他们不为我工作。

I'm working through the ListSet module from the Coq standard library. I'm unsure how to reason about conditionals in a proof. For instance, I am having trouble with the following proof. Definitions are provided for context.

The current proof state includes the inr of Aeq_dec as a hypothesis. I have discarded the base case of induction and the inductive case where the inl of Aeq_dec is true.

The only way for H to be true if a <> x is if set_mem xs is true. I should be able to apply the conditional in H to a <> x in order to obtain set_mem xs. However, I don't understand how to do this. How do I deal with, or decompose, or apply conditionals?

是.v为了验证吗？验证？瓦马诺斯？

为什么不使用.coq扩展程序？

[我不确定这是否适合堆栈溢出，但这里还有许多其他 Coq 问题，所以也许有人可以提供帮助。]

我正在从http://www.cis.upenn.edu/~bcpierce/sf/Basics.html#lab28完成以下工作（就在介绍案例的下方）。请注意，我在这方面是一个完整的初学者，并且正在家里工作——我不是学生。

我正在研究重写的作用：

然后rewrite <- H.应用：

并且很清楚证明将如何成功。

我可以看到如何以机械方式操纵符号来获得证明。没关系。但我对“意义”感到不安。特别是，我怎么能false = true在一个证明中间？

似乎我在提出某种矛盾的论点，但我不确定是什么。我觉得我一直在盲目地遵守规则，不知怎的已经到了我在胡说八道的地步。

我在上面做什么？

我希望这个问题很清楚。

我可以使用类型类在 Coq 中天真地构建代数结构的层次结构。我在查找有关 Coq 类型类的语法和语义的资源时遇到了一些麻烦。但是，我相信以下是半群、幺半群和交换幺半群的正确实现：

如果我理解正确，可以通过首先声明Monoid的实例Semigroup，然后参数化 on来添加其他参数（例如，幺半群的标识元素） id : A。但是，为 构建的记录中发生了一些奇怪的事情AbelianMonoid。

这发生在我试图为半组构建一个类时。我认为以下语法是正确的：

但是，我无法消除正确的运算符和标识元素的歧义。打印记录揭示了上述问题。所以我有两个问题：第一，如何正确声明类Monoid；第二，如何消除超类中的函数歧义？

我真正想要的是一个很好的资源，它清楚地解释了 Coq 的类型类，而没有过时的语法。例如，我认为 Hutton 的书清楚地解释了 Haskell 中的类型类。

我已经困惑了几个小时，我不知道如何证明

在考克。我真的需要你的帮助。有什么建议么？