问题标签 [theorem-proving]
For questions regarding programming in ECMAScript (JavaScript/JS) and its various dialects/implementations (excluding ActionScript). Note JavaScript is NOT the same as Java! Please include all relevant tags on your question; e.g., [node.js], [jquery], [json], [reactjs], [angular], [ember.js], [vue.js], [typescript], [svelte], etc.
isabelle - 如何生成伊莎贝尔理论的html版本
我有一个 Isabelle 理论文件,名为John.thy
. 我想把它展示给我的朋友,但我的朋友没有 Isabelle,而且原始.thy
文件不太容易阅读。我在 Isabelle 库中看到了一些网页(例如:http: //isabelle.in.tum.de/library/HOL/Finite_Set.html),它们具有漂亮的语法突出显示,我希望我的理论看起来像那样。
那么我该怎么做John.html
呢?我查看了文档,所有的构建文件和制作文件等看起来都相当可怕和困难。某个善良的灵魂可以解释最简单的方法吗?
isabelle - 确定记录类型属于给定类
我创建了一个名为 的记录类型graph
,并定义了一个合适的“是”关系的子图。我想表明一组图与子图关系形成一个顺序,即是ord
类的一个实例。但我无法让它工作。这是我的最小工作示例:
我得到错误:
Type unification failed: No type arity graph_ext :: ord"
我尝试输入诸如instantiation graph :: ord
and之类的内容instantiation graph_ext :: ord
,但似乎没有任何效果。有任何想法吗?
isabelle - 生成 Isabelle HTML 文档 *无需证明*
我希望为 Isabelle 理论(例如 HOL 会话)生成 HTML 文档,但不包括证明。
也就是说,我想制作像http://isabelle.in.tum.de/library/HOL/Nat.html这样的页面 ,而不是,例如,
我只想看
原因是我使用 HTML 页面来查看可用的定理,但在这种情况下,证明只会分散注意力。(我知道在生成 PDF 时可以省略证明,但我对 HTML 文档特别感兴趣。)
theorem-proving - 在 Agda 中证明类型为空
我试图在 agda 中证明 2*3!=5。为此,我将定义一个带有签名 2 * 3 ≡ 5 → ⊥ 的函数。
利用我对乘法的定义
我已经证明
和
但是当我试图证明:
编译器吐出这个关于 x 的错误
对不起,如果这是一个愚蠢的问题。提前致谢。
max - Isabelle 琐碎问题:“Max (S::nat set) = 0”意味着 S 的所有元素都为零
我试图证明以下含义:
我认为这将是相当微不足道的,这就是为什么我尝试使用大锤来证明。不幸的是,这失败了。要么我的定义是错误的,要么涉及像 Max 这样的大运营商的自动证明存在一些困难。
我试图通过查看它们的定义以及我能找到的任何文档来更好地理解 Max 和 max。正如我之前遇到过 Isabelle 的一个问题,尽管它看起来微不足道(“为什么 Isabelle 不简化我的“if _ then _ else”构造的主体? ”),但最终结果证明它需要大量经验,我决定在这里发布这个问题。
solver - 如何使用 solve_direct 建议的规则?(按(规则……)并不总是有效)
有时<statement> solve_direct
(我通常通过 调用<statement> try
)列出许多库定理并说“当前目标可以直接解决:……”。
设<theorem>
为 的一个搜索结果solve_direct
,那么在大多数情况下我都可以证明<statement> by (rule theorem)
。
但是,有时这样的证明不被接受,导致错误消息“无法应用初始证明方法”。
是否有一种通用的、不同的技术来重用由 找到的定理solve_direct
?
还是取决于个人情况?我可以尝试制定一个最小的示例并将其附加到这个问题上。
polynomial-math - 多项式的次数小于一个数
我正在研究一个引理,该引理表明,n
如果每个单项式的指数小于或等于 ,则单项式之和的次数总是小于或等于n
。
到目前为止,我要做的如下(请注意,我是 Isabelle 的初学者):
这就是问题所在,我不明白为什么以下引理不足以完成证明。特别是,我希望最后一部分(抱歉的地方)足够简单,让大锤找到证据:
.
布赖恩霍夫曼出色回答的解决方案:
。
coq - Coq:如何证明“a=b -> nat_compare ab = Eq.”?
为了了解 Coq 是什么,我最终遇到了一种情况,我基本上需要证明a=b -> nat_compare a b = Eq
.
我可以通过以下方式轻松开始:
这给了我:
第一个是微不足道的:
但下一个目标难倒我:
我可以
这使:
(我也可以通过 到达这个确切的点simpl
,这似乎更有意义。)
现在,用笔和纸,我只是声称这是我的归纳证明..
我是否以正确的方式处理这个问题?我在哪里可以最好地学习如何正确地做到这一点?
theory - 证明冒泡排序是由引理排序的
我已经尝试证明乐趣bubble_main
是有序的,但似乎没有任何方法有效。有人可以帮我证明引理吗is_ordered (bubble_main L)
?
我只是删除了我以前所有的引理,因为似乎没有一个可以帮助Isabelle找到证据。这是我的代码/理论:
coq - Coq - 消除 OR 时出错
我不知道为什么,但是在 Coq 中,当试图证明程序规范时,在试图消除 OR 假设时会出错:
这是我要证明的定理:
这是发生错误时的目标和上下文:
在这个定理之前,我有这个定义和这些导入:
当我尝试使用这种策略时,我得到了之前的错误:
我真的不知道可能是什么原因造成的。