与Coq相比,Isabelle/HOL证明助手是否有任何弱点和优势？
我看到了几个不同的研究小组,至少有一本关于使用Coq设计认证程序的书.关于认证计划的定义是什么,是否有共识？从我所知道的,它真正意味着该程序被证明是完整的并且类型正确.现在,程序的类型可能是非常奇特的东西,例如列表,其中包含非空的证明,排序,所有元素> = 5等等.但是,最终,是一个经过认证的程序,Coq显示的是总计和类型安全的程序,所有有趣的问题归结为最终类型中包含的内容？
根据wjedynak的回答,我看了Xavier Leroy的论文"现实编译器的形式验证",它在下面的答案中有所联系.我认为这包含一些很好的信息,但我认为这个研究序列中的信息量更多的信息可以在Sandrine Blazy和Xavier Leroy 的C语言的Clight子集的机械化语义学中找到.这是"形式验证"论文添加优化的语言.在其中,Blazy和Leroy介绍了Clight语言的语法和语义,然后在第5节讨论了这些语义的验证.在第5节中,列出了用于验证编译器的不同策略,这在某种意义上提供了概述创建认证计划的不同策略.这些是:
在任何情况下,可能会添加一些点,我当然希望听到更多.
回到我关于认证程序定义的原始问题,对我来说仍然有点不清楚.Wjedynak提供了一个答案,但Leroy的工作实际上涉及在Coq中创建编译器,然后在某种意义上证明它.从理论上讲,它现在可以证明C程序的内容,因为我们现在可以进行C-> Coq->证明.从这个意义上讲,似乎就是我们可以做到这一点
或者,我们可以在校对助手工具中创建程序规范,然后证明规范的属性,而不是程序本身.
无论如何,如果有人有这些定义,我仍然有兴趣听取其他定义.
在 Isabelle 中，命令print_state可以打印需要证明的当前目标。但是，我希望以其他易于处理的格式打印目标，例如 S 表达式和抽象语法树。
默认打印模式不包括这种格式，所以我想知道如何修改Isabelle内部的ML文件。或者更具体地说，当前目标如何通过打印。我很高兴它在 ML 文件中是 AST 格式，然后才被传递到打印，但我很难找到变量是如何传输的。有谁知道如何解决这个问题？
我已经看过很多关于Isabelle的语法和证明策略的文档.然而,我几乎找不到它的基础.我有几个问题,如果有人能抽出时间回答,我将非常感激:
为什么Isabelle/HOL不接受不终止的功能？许多其他语言(如Haskell)都承认非终止函数.
什么符号是伊莎贝尔的元语言的一部分？我读到在通用量化(/\)和暗示(==>)的元语言中有符号.但是,这些符号在对象级语言(∀和-->)中具有对应的符号.我知道这-->是一个类型的对象级函数bool => bool => bool.但是,∀和how是如何定义的？它们是对象级布尔函数吗？如果是这样,它们是不可计算的(考虑无限域).我注意到我能够在∀和ther中编写布尔函数,但它们不可计算.那么∀和what是什么？它们是对象级别的一部分吗？如果是这样,他们是如何定义的？
Isabelle定理只是布尔表达式吗？然后布尔是元语言的一部分？
据我所知,Isabelle是一种严格的编程语言.我怎样才能使用无限对象？比方说,无限列表.Isabelle/HOL有可能吗？
对不起,如果这些问题非常基础.我似乎没有找到关于伊莎贝尔元理论的好教程.我很乐意,如果有人可以推荐我这些主题的好教程.
非常感谢你.
如何使用Isabelle/HOL从源理论文件中自动生成LaTeX？
Isabelle/HOL tutorial.pdf非常漂亮.我将在LaTeX上写一篇论文,里面有很多Isabelle代码.
在Isabelle理论文件中,我可以编写简单的单行策略,如下所示:
apply (clarsimp simp: split_def split: prod.splits)
然而,我发现,当我开始编写ML代码来自动化证明,生成一个ML tactic对象时,这些单行变得相当冗长:
clarsimp_tac (Context.proof_map (
Simplifier.map_ss (fold Splitter.add_split @{thms prod.splits})
#> Simplifier.map_ss (fn ss => ss addsimps [@{thm split_def}]))
@{context}) 1
有没有更简单的方法来编写Isabelle/ML级别的简单单线战术？
例如,像反引语这样的东西:@{tactic "clarsimp simp: split_def split: prod.splits"}产生类型的函数context -> tactic,将是一个理想的解决方案.
我有一个Isabelle证据结构如下:
proof (cases "n = 0")
case True
(* lots of stuff here *)
show ?thesis sorry
next
case False
(* lots of stuff here too *)
show ?thesis sorry
qed
第一种情况实际上是几页长,所以在阅读第二种情况时,对于一个随意的读者,甚至对我自己来说,它False所指的不再是清楚的.(嗯,它实际上是,但不是来自阅读,只能在交互式环境中:例如,如果在Isabelle/jEdit中,您将光标置于其后case False,您将n ? 0在"输出"面板中的"this"下看到.)
那么是否有一种语法允许假设"假"情况明确,这样读者既不必与IDE交互,也不必向上滚动到proof关键字,但是可以正确看待假设？
我正在寻找一个工具(首选GUI但CLI可以工作),它允许我输入数学表达式,然后执行它们的操作,但限制我只有数学上有效的操作.此外,该工具必须能够保存会话,然后证明给定的已保存操作集是有效的.
注意:我不是在寻找一个生成校样的系统,只是检查我手动指定的步骤是否有效.
我已经使用ACL2进行类似的操作,并且它在某些情况下表现很好但是很难用于其他所有情况.
这个小项目是我的动力.它是一种D模板类型,允许求解方程.鉴于这个等式:
(A * B) = C + D / F;
可以将任何一个符号设置为未知,并评估该表达式将导致对该变量的赋值.它的工作原理是将表达式树构建到类型中,然后使用重写规则将其转换为可以针对未知类型进行事件处理的事物.
我需要的是一些验证重写规则的方法.可以通过测试给定某种关系为真的断言来验证它们,另一种也是.
通常我有问题sledgehammer找到证据,但是当我插入它时,它不会终止.我猜sledgehammer是Isabelle最重要的部分之一,但如果证据失败则会变得很烦人.
在Sledgehammer教程中,有一个小章节"为什么Metis无法重建证明？".
它列出:
isar_proofs选项以获得逐步的Isar证明,其中每个步骤都是正确的metis.由于步骤相当小,
metis因此更有可能重播它们.smt证明方法而不是metis.它通常更强大,但您需要使用Z3重放证明,信任SMT求解器或使用证书.blast或者auto证明方法,通过传递必要的事实unfolding,using,intro:,elim:,dest:,或simp:适当.问题是第一个选项使证明更加冗长,并且还涉及手动干预.第二种选择很少有效.
那么第三种选择呢？我可以使用任何易于遵循的启发式方法吗？
unfolding和之间有什么区别using？也有关于如何使用的最佳做法intro:,elim:以及dest:从失败的metis证明吗？
部分例子
proof-
have "(det (?lm)) = (det (transpose ?lm))" by (smt det_transpose)
then have "(det (?lm)) = [...][not shown]"
unfolding det_transpose transpose_mat_factor_col by auto
then show ?thesis [...][not …在一些Cedille源中使用以下Nats编码:
cNat : ?
cNat = ? X : ? . X ? (? R : ? . (R ? X) ? R ? X) ? X
cZ : cNat
cZ = ? X . ? z . ? s . z
cS : ? A : ? . (A ? cNat) ? A ? cNat
cS = ? A . ? e . ? d . ? X . ? z . ? s . s · A (? …