问题标签 [coq]

我正在寻找一种工具（首选 GUI，但 CLI 可以），它允许我输入数学表达式，然后对它们执行操作，但将我限制为仅在数学上有效的操作。此外，该工具必须能够保存会话并稍后证明给定的一组已保存操作是有效的。

注意：我不是在寻找生成证明的系统，只是检查我手动指定的步骤是否有效。

我已经将ACL2用于类似的操作，并且在某些情况下效果很好，但在其他所有情况下都很难使用。

这个小项目是我的动力。它是一种 D 模板类型，允许求解方程。给定这个等式：

任何一个符号都可以设置为未知，并且评估该表达式将导致对该变量的赋值。它的工作原理是将表达式树构建到类型中，然后使用重写规则将其转换为可以为未知类型触发的东西。

我需要的是某种方法来验证重写规则。它们可以通过测试一个断言来验证，即给定一些关系是真的，另一个也是真的。

我正在尝试 Coq，但我不完全确定我在做什么。是：

相当于：

编辑：我认为他们是。

如何在 Coq 中证明 (forall x, P x /\ Q x) -> (forall x, P x)？已经尝试了几个小时，但无法弄清楚如何将先行词分解为 Coq 可以消化的东西。（我是新手，显然:)

有谁知道以下任何例子？

1. 证明助手（例如Coq ）中关于正则表达式（可能通过反向引用扩展）的证明开发。
2. 关于正则表达式的依赖类型语言（例如Agda ）的程序。

我如何在 coq 中证明一个f接受 booltrue|false并返回 bool的函数true|false（如下所示），当两次应用于单个 bool 时，true|false将始终返回相同的值true|false：

例如函数f只能做 4 件事，让我们调用函数的输入b：

• 总是返回true
• 总是返回false
• 返回b（即如果 b 为真，则返回真，反之亦然）
• 返回not b（即如果 b 为真则返回假，反之亦然）

因此，如果函数始终返回 true：

如果函数总是返回 false，我们会得到：

对于其他情况，让我们假设函数返回not b

在这两种可能的输入情况下，我们总是以原始输入结束。如果我们假设函数返回，情况也是如此b。

那么你将如何在 coq 中证明这一点？

我试图在 Coq 中证明以下内容：

目标 (forall x:X, P(x) /\ Q(x)) -> ((forall x:X, P (x)) /\ (forall x:X, Q (x)))。

有人可以帮忙吗？我不确定是否要拆分，做出假设等。

我很抱歉成为一个完整的菜鸟

我有定义的归纳类型：

现在我必须证明该归纳类型的一系列属性，但我一直卡住。

有人可以帮助我前进。

由于那里有非图灵完整的语言，并且鉴于我没有在大学学习 Comp Sci，有人可以解释一下图灵不完整的语言（如Coq）无法做到的事情吗？

还是没有真正的实际兴趣的完整性/不完整性（即在实践中没有太大区别）？

编辑-我正在寻找一个答案，由于 X 或类似的原因，您无法用非图灵完备的语言构建哈希表！

我在Coq中定义了以下归纳类型。

natlist 基本上是一个自然数列表（类似于 Python 中的列表）。我正在尝试使用下面的定义找到两个 natlist 的联合。

Definition union_of_lists : natlist -> natlist -> natlist

即 Eval simpl in (union_of_lists [1,2,3] [1,4,1]) 应该返回 [1,2,3,1,4,1]

我有以下疑问。

• 由于这个定义没有参数，我如何实际获取输入并处理它们？
• union_of_lists 的定义究竟返回了什么？它只是一个natlist吗？

非常感谢任何帮助或提示。

我试图（经典地）证明

在考克。我想要做的是相反地证明它：

我的问题是第 (2) 和 (5) 行。我不知道如何选择 U 的任意元素，证明一些关于它的东西，并得出结论。

有什么建议（我不致力于使用对立）？