问题标签 [theorem-proving]

我有一个 Isabelle 理论文件，名为John.thy. 我想把它展示给我的朋友，但我的朋友没有 Isabelle，而且原始.thy文件不太容易阅读。我在 Isabelle 库中看到了一些网页（例如：http: //isabelle.in.tum.de/library/HOL/Finite_Set.html），它们具有漂亮的语法突出显示，我希望我的理论看起来像那样。

那么我该怎么做John.html呢？我查看了文档，所有的构建文件和制作文件等看起来都相当可怕和困难。某个善良的灵魂可以解释最简单的方法吗？

我创建了一个名为 的记录类型graph，并定义了一个合适的“是”关系的子图。我想表明一组图与子图关系形成一个顺序，即是ord类的一个实例。但我无法让它工作。这是我的最小工作示例：

我得到错误：

Type unification failed: No type arity graph_ext :: ord"

我尝试输入诸如instantiation graph :: ordand之类的内容instantiation graph_ext :: ord，但似乎没有任何效果。有任何想法吗？

我希望为 Isabelle 理论（例如 HOL 会话）生成 HTML 文档，但不包括证明。

也就是说，我想制作像http://isabelle.in.tum.de/library/HOL/Nat.html这样的页面 ，而不是，例如，

我只想看

原因是我使用 HTML 页面来查看可用的定理，但在这种情况下，证明只会分散注意力。（我知道在生成 PDF 时可以省略证明，但我对 HTML 文档特别感兴趣。）

我试图在 agda 中证明 2*3!=5。为此，我将定义一个带有签名 2 * 3 ≡ 5 → ⊥ 的函数。

利用我对乘法的定义

我已经证明

和

但是当我试图证明：

编译器吐出这个关于 x 的错误

对不起，如果这是一个愚蠢的问题。提前致谢。

我试图证明以下含义：

我认为这将是相当微不足道的，这就是为什么我尝试使用大锤来证明。不幸的是，这失败了。要么我的定义是错误的，要么涉及像 Max 这样的大运营商的自动证明存在一些困难。

我试图通过查看它们的定义以及我能找到的任何文档来更好地理解 Max 和 max。正如我之前遇到过 Isabelle 的一个问题，尽管它看起来微不足道（“为什么 Isabelle 不简化我的“if _ then _ else”构造的主体？ ”），但最终结果证明它需要大量经验，我决定在这里发布这个问题。

有时<statement> solve_direct（我通常通过 调用<statement> try）列出许多库定理并说“当前目标可以直接解决：……”。

设<theorem>为 的一个搜索结果solve_direct，那么在大多数情况下我都可以证明<statement> by (rule theorem)。

但是，有时这样的证明不被接受，导致错误消息“无法应用初始证明方法”。

是否有一种通用的、不同的技术来重用由 找到的定理solve_direct？

还是取决于个人情况？我可以尝试制定一个最小的示例并将其附加到这个问题上。

我正在研究一个引理，该引理表明，n如果每个单项式的指数小于或等于 ，则单项式之和的次数总是小于或等于n。

到目前为止，我要做的如下（请注意，我是 Isabelle 的初学者）：

这就是问题所在，我不明白为什么以下引理不足以完成证明。特别是，我希望最后一部分（抱歉的地方）足够简单，让大锤找到证据：

.
布赖恩霍夫曼出色回答的解决方案：
。

为了了解 Coq 是什么，我最终遇到了一种情况，我基本上需要证明a=b -> nat_compare a b = Eq.

我可以通过以下方式轻松开始：

这给了我：

第一个是微不足道的：

但下一个目标难倒我：

我可以

这使：

（我也可以通过 到达这个确切的点simpl，这似乎更有意义。）

现在，用笔和纸，我只是声称这是我的归纳证明..

我是否以正确的方式处理这个问题？我在哪里可以最好地学习如何正确地做到这一点？

我已经尝试证明乐趣bubble_main是有序的，但似乎没有任何方法有效。有人可以帮我证明引理吗is_ordered (bubble_main L)？

我只是删除了我以前所有的引理，因为似乎没有一个可以帮助Isabelle找到证据。这是我的代码/理论：

我不知道为什么，但是在 Coq 中，当试图证明程序规范时，在试图消除 OR 假设时会出错：

这是我要证明的定理：

这是发生错误时的目标和上下文：

在这个定理之前，我有这个定义和这些导入：

当我尝试使用这种策略时，我得到了之前的错误：

我真的不知道可能是什么原因造成的。