问题标签 [coq]

我希望这是我的问题的正确位置。实际上我是 coq 用户，我正在尝试在“Mac OS X Lion 10.7.4”下使用 ocaml 实现一种新策略。我已经安装了我可能需要的所有库。编译我的 ocaml 文件并尝试在 coq 中导入它时（我使用 Proofgenral 和 Aquamacs）我收到此错误错误：不支持动态链接。经过长时间的搜索，我发现这是链接库的问题，但我还没有找到解决方法。

有人可以给我一个简单的 Coq 中存在实例化和存在泛化的例子吗？当我想证明，使用的一些exists x, P在哪里时，我经常想命名（例如），并操纵 P。这可以是 Coq 中的一个吗？PPropxxx0

我有一个定理，我证明存在满足某些属性的对象。我通过构造对象证明了这个定理。然后，在另一个证明中，我想在第二个定理的陈述中引用第一个定理中定义的对象。我知道如果我使用 Defined 而不是 Qed 关闭我的证明，该对象应该是可访问的，但我不知道如何访问它。例如：

定理 T1：存在 x，P x。证明。... 定义。

定理 T2：对于在 T1 中构造的相同 x，Q x \/ R x。证明。... Qed。

我如何在 Coq 中表达这一点？

我正在尝试在证明检查器 coq 中定义一个域。我该怎么做呢？

我正在尝试做相当于V in [0,10].

我已经尝试过这样做Definition V := forall v in R, 0 <= v /\ v <= 10.，但这会导致常量出现问题，例如根据 Coq0不在其中。V

在我的证明中，我偶然发现了A /\ B /\ C假设中存在的问题，我需要证明(A /\ B) /\ C. 这些在逻辑上是完全一样的，但是 coq 不会用assumption..

我一直在通过应用公理来解决这些问题，但是有没有更优雅（和正确）的方法来处理这个问题？

我必须证明一些正式的东西。有两个函数，获取一些字符串和字符串数组，比较是否匹配，并返回 bool。我想在引理中测试它们，并验证它。在编程中，函数如下所示。

我想在 Coq 中声明一个引理，如果两个函数都返回 true 并证明它，它应该为 true。喜欢

问题：

1）如何定义这些功能？这些不是归纳函数或递归函数（我认为）。他们应该像以下或任何其他选项吗？

2）如何处理子集？比如我该如何处理世界和欧洲的一组国家？请记住，我的要求是该函数获取一个名称和一个字符串数组。

3）Countryname、World、Name、Student这四个元素的类型应该是什么？

我很想获得帮助我在 Coq 中解决此类问题的材料的参考。

谢谢，

维拉亚特

我想证明下面的引理。我正在尝试使用“破坏”策略，但我无法证明这一点。请任何人指导我如何证明这样的引理。我可以为 EmptyString 证明它，但不能为变量 s1 和 s2 证明。谢谢

我试图证明关于 Prop 的替换定理，但我失败了。下面的定理能否在 coq 中被证明，如果不能，为什么不能。

关键是，在逻辑上，证明将是归纳法。据我所知，道具不是归纳定义的。如何在 Coq 中证明这样的定理？

我有一个场景，我想证明一个引理，包括许多字符串和列表变量。可能，它需要“归纳”，但任何人都可以帮助我证明下面给出的引理。如果需要其余代码，我也可以提供。

试图证明元素插入函数到 bst 中的正确性，我被困在试图证明一个看似微不足道的引理中。到目前为止我的尝试：

显然，如果树中的所有内容都小于n并且n <= m所有内容都小于m，但我似乎无法让 coq 相信我。我该如何继续？