如何在"Isabelle/HOL中的编程和证明"的练习4.6中证明引理?

问题描述

我正在尝试解决"Isabelle/HOL中的编程和证明"中的练习4.6.它要求定义一个将列表转换为集合的函数elems :: "'a list ⇒ 'a set"，并证明引理"x ∈ elems xs ⟹ ∃ ys zs . xs = ys @ x # zs ∧ x ∉ elems ys".到目前为止，我已经走到了这么远:

I am trying to solve Exercise 4.6 in "Programming and Proving in Isabelle/HOL". It asks to define a function elems :: "'a list ⇒ 'a set" that converts a list into a set, and to prove the lemma "x ∈ elems xs ⟹ ∃ ys zs . xs = ys @ x # zs ∧ x ∉ elems ys". Until now, I have come that far:

fun elems :: "'a list ⇒ 'a set" where
  "elems [] = {}" |
  "elems (x # xs) = {x} ∪ elems xs"

lemma first_occ: "x ∈ elems xs ⟹ ∃ ys zs . xs = ys @ x # zs ∧ x ∉ elems ys"
proof (induction xs)
  case Nil
  thus ?case by simp
next
  case (Cons u us)
  show ?case
  proof cases
    assume "x = u"
    thus ?case
    proof
    ⟨…⟩

这时，我收到错误消息无法应用初始证明方法".这很奇怪，因为目标?case是命题∃ ys zs . u # us = ys @ x # zs ∧ x ∉ elems ys，并且应该有可能通过在特定证人的∃下显示命题来证明存在命题.

At this point, I get the error message "Failed to apply initial proof method". This is strange, since the goal, ?case, is the proposition ∃ ys zs . u # us = ys @ x # zs ∧ x ∉ elems ys, and it should be possible to prove existential propositions by showing the proposition under the ∃ for a specific witness.

推荐答案

您的行proof的问题在于，它proof是要应用一些默认规则的.在以上证明中，Isabelle无法确定您要执行存在性引入.因此，您可能想明确地告诉系统要这样做，例如，继续执行proof (intro exI)之类的方法.

the problem with your line proof is that it proof is meant to apply some default rule. In the above proof, Isabelle is not able to figure out that you want to perform existential introduction. So, you probably want to explicitly tell the system to do so, e.g., by continue with something like proof (intro exI).

我希望这会有所帮助，雷内(René)

I hope, this helps, René

这篇关于如何在"Isabelle/HOL中的编程和证明"的练习4.6中证明引理?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！