时间戳

首页 > 解决方案 > 为什么 Isabelle/HOL 2018 显示错误而没有错误消息？

isabelle - 为什么 Isabelle/HOL 2018 显示错误而没有错误消息？

问题描述

对于一个 uni 项目，我正在使用 Iabelle/HOL 2018 进行证明。应用明显结果时出现错误。但是，此错误并未说明发生了什么问题。

起初我认为这是一个统一的问题。但是当我简化它时，结果证明这是一种我完全不理解的行为。

我有一个最小的例子，如下所示：

我将命题公式定义为 type1，然后我有一个尾递归函数，它简单地收集每个子公式。可能有更好的方法来做到这一点。我只是试图以最简单的方式复制错误。然后我想展示一个简单的等式（我已经在我的代码中证明了这一点，在这里我只是简化为“对不起”）然后我想在其他一些证明中使用这个事实，但是它似乎并没有应用已证明的事实，即使我将它添加到 simp 集中。甚至，直接应用它对我也不起作用。

这是代码：

theory test
  imports Main
begin

datatype 'a type1 = 
    Bot
    | Atm 'a
    | Neg "'a type1"
    | Imp "'a type1" "'a type1"

fun func :: "'a type1 ⇒ ('a type1) list list ⇒ ('a type1) list list"
  where
    "func Bot acc = acc"
  | "func (Atm p) acc = acc"
  | "func (Neg p) acc = func p ([Neg p] # acc)"
  | "func (Imp p q) acc = func q (func p ([Imp p q] # acc))"

lemma lemma1 [simp]:
  "func p acc = func p [] @ acc"
  sorry

lemma lemma2:
  "func p acc = func p acc"
proof -
  have "func p acc = func p [] @ acc" by auto
  show ?thesis sorry
qed

end

在我看来，这应该没有问题。但是，在 lemma2 证明的第一行中，我得到了一个错误。但是对于“未能完成证明”或类似的错误没有任何解释。

有谁知道我做错了什么？或者有没有人有类似的问题或行为？

标签： isabelle

解决方案

引用《高阶逻辑的证明助手》一书：“在最基本的形式中，简化意味着从左到右重复应用方程......只有真正简化的方程，如rev (rev xs) = xs和xs @ [] = xs，应声明为默认简化规则。” （还有其他有价值的资源可以解释这个问题，例如官方 Isabelle/Isar 参考手册或教科书 'Concrete Semantics with Isabelle/HOL'）。因此，lemma1对于默认简化规则来说，这不是一个好的选择，并且将其添加到 simpset 可能会导致不终止，如您的示例所示。

如果您想lemma1在另一个证明中使用，也许，您可以使用类似于

have "func p acc = func p [] @ acc by (rule lemma1)"

或仅将 simp 规则重写为

func p [] @ acc = func p acc.

但是，一般来说，在引入新的 simp 规则时需要非常小心，尤其是在全局理论背景下。

推荐阅读