Isabelle/HOL Isar中的假设证明

我试图证明一个引理,它在某个部分有一个错误的假设.在Coq,我曾经写过"一致",它会摆脱目标.但是,我不知道如何继续Isabelle Isar.我试图证明我的le功能的一个引理:

primrec le::"nat ? nat ? bool" where
"le 0 n = True" |
"le (Suc k) n = (case n of 0 ? False | Suc j ? le k j)"

lemma def_le: "le a b = True ? (?k. a + k = b)"
proof
  assume H:"le a b = True"
  show "?k. a + k = b"
  proof (induct a)
    case 0
    show "?k. 0 + k = b"
    proof -
      have "0 + b = b" by simp
      thus ?thesis by (rule exI)
    qed

    case Suc
    fix n::nat
    assume HI:"?k. n + k = b"
    show "?k. (Suc n) + k = b"
    proof (induct b)
      case 0
      show "?k. (Suc n) + k = 0"
      proof -
        have "le (Suc n) 0 = False" by simp
        oops

请注意,我的le功能是"更少或相等".在这一点上证明我发现我的假设H其中指出le a b = True,或在这种情况下le (Suc n) 0 = True这是假的.我该如何解决这个引理？

另一个小问题:我想写,have "le (Suc n) 0 = False" by (simp only:le.simps)但这不起作用.我似乎需要添加一些规则来减少案例表达式.我错过了什么？

非常感谢您的帮助.

问题不在于False伊莎贝尔很难摆脱假设.事实上,如果存在False假设,几乎所有Isabelle的证明方法都会立即证明.不,这里的问题是,在证据的那一点上,你没有你需要的假设,因为你没有将它们链接到归纳中.但首先,请允许我做一些小的评论,然后给出具体的建议来修正你的证据.

写作le a b = True或le a b = False在Isabelle中有点不合时宜.只是写le a b或¬le a b.

以方便的形式编写定义对于获得良好的自动化非常重要.当然,您的定义是有效的,但我建议使用以下内容,这可能更自然,并且会免费为您提供方便的归纳规则:

使用功能包:

fun le :: "nat ? nat ? bool" where
  "le 0 n             = True"
| "le (Suc k) 0       = False"
| "le (Suc k) (Suc n) = le k n"

存在性有时可以隐藏重要信息,并且它们易于自动化,因为自动化从未完全知道如何实例化它们.

如果您证明以下引理,则证明是完全自动的:

lemma def_le': "le a b ? a + (b - a) = b"
  by (induction a arbitrary: b) (simp_all split: nat.split)

使用我的函数定义,它是:

lemma def_le': "le a b ? (a + (b - a) = b)"
  by (induction a b rule: le.induct) simp_all

你的引理然后从那个简单的:

lemma def_le: "le a b ? (?k. a + k = b)"
  using def_le' by auto

这是因为存在主义使搜索空间爆炸.给自动化一些具体的东西可以帮助很多.

有很多问题.首先,你可能需要做的induct a arbitrary: b,因为b你的诱导过程中会发生变化(le (Suc a) b你将不得不做一个案例分析b,然后在情况下b = Suc b',你将去le (Suc a) (Suc b')到le a b').

第二,在最顶端,你有assume "le a b = True",但你没有把这个事实链接到归纳.如果您在Isabelle中进行归纳,则必须将包含归纳变量的所有必需假设链接到归纳命令中,否则它们将无法在归纳证明中使用.有问题的假设谈论a和b,但如果你做了归纳a,你将不得不推理一些a'与之无关的任意变量a.例如:

assume H:"le a b = True"
thus "?k. a + k = b"

(和第二次感应相同b)

第三,当您在Isar中有多个案例时(例如在归纳或案例分析期间),next如果他们有不同的假设,您必须将它们分开.在next本质上扔掉所有的固定变量和局部假设.随着我之前提到的变化,你需要一个next之前case Suc,或者Isabelle会抱怨.

第四,caseIsar中的命令可以修复变量.在您的Suc情况下,归纳变量a是固定的; 随着改变arbitrary: b,一个a和一个b是固定的.你应该给这些变量明确的名字; 否则,伊莎贝尔会发明它们,你必须希望它所提出的那些与你使用的相同.这不是好风格.所以写一下case (Suc a b).注意,你不会有固定的变量或使用时,承担的东西case.该case命令为您处理,并将局部假设存储在与案例同名的定理集合中,例如Suc此处.它们被归类为Suc.prems,Suc.IH,Suc.hyps.此外,当前案件的证明义务存储在?case(不是?thesis!)中.

有了这个(以及一点点清理),你的证明看起来像这样:

lemma def_le: "le a b ? (?k. a + k = b)"
proof
  assume "le a b"
  thus "?k. a + k = b"
  proof (induct a arbitrary: b)
    case 0
    show "?k. 0 + k = b" by simp
  next
    case (Suc a b)
    thus ?case
    proof (induct b)
      case 0
      thus ?case by simp
    next
      case (Suc b)
      thus ?case by simp
    qed
  qed
next

它可以浓缩为

lemma def_le: "le a b ? (?k. a + k = b)"
proof
  assume "le a b"
  thus "?k. a + k = b"
  proof (induct a arbitrary: b)
    case (Suc a b)
    thus ?case by (induct b) simp_all
  qed simp
next

但实际上,我建议你先简单地证明一个具体的结果le a b ? a + (b - a) = b,然后用它来证明存在主义的陈述.