0

我对使用 Isabelle/Isar 编写既可读又机器检查的证明很感兴趣，我希望改进我的风格并简化我的证明。

prog-prove有以下练习：

练习 4.6。定义一个递归函数elems :: 'a list ⇒ 'a set并证明x ∈ elems xs ⟹ ∃ ys zs. xs = ys @ x # zs ∧ x ∉ elems ys。

模仿类似于我用笔和纸写的东西，我的解决方案是

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

fun takeUntil :: "('a ⇒ bool) ⇒ 'a list ⇒ 'a list" where
"takeUntil f [] = []" |
"takeUntil f (x # xs) = (case (f x) of False ⇒ x # takeUntil f xs | True ⇒ [])"

theorem "x ∈ elems xs ⟹ ∃ ys zs. xs = ys @ x # zs ∧ x ∉ elems ys"
proof -
  assume 1: "x ∈ elems xs"
  let ?ys = "takeUntil (λ z. z = x) xs"
  let ?zs = "drop (length ?ys + 1) xs"
  have "xs = ?ys @ x # ?zs ∧ x ∉ elems ?ys"
  proof
    have 2: "x ∉ elems ?ys"
    proof (induction xs)
      case Nil
      thus ?case by simp
    next
      case (Cons a xs)
      thus ?case
      proof -
        {
          assume "a = x"
          hence "takeUntil (λz. z = x) (a # xs) = []" by simp
          hence A: ?thesis by simp
        }
        note eq = this
        {
          assume "a ≠ x"
          hence "takeUntil (λz. z = x) (a # xs) = a # takeUntil (λz. z = x) xs" by simp
          hence ?thesis using Cons.IH by auto
        }
        note noteq = this
        have "a = x ∨ a ≠ x" by simp
        thus ?thesis using eq noteq by blast
      qed
    qed

    from 1 have "xs = ?ys @ x # ?zs"
    proof (induction xs)
      case Nil
      hence False by simp
      thus ?case by simp
    next
      case (Cons a xs)
      {
        assume 1: "a = x"
        hence 2: "takeUntil (λz. z = x) (a # xs) = []" by simp
        hence "length (takeUntil (λz. z = x) (a # xs)) + 1 = 1" by simp
        hence 3: "drop (length (takeUntil (λz. z = x) (a # xs)) + 1) (a # xs) = xs" by simp
        from 1 2 3 have ?case by simp
      }
      note eq = this
      {
        assume 1: "a ≠ x"
        with Cons.prems have "x ∈ elems xs" by simp
        with Cons.IH
         have IH: "xs = takeUntil (λz. z = x) xs @ x # drop (length (takeUntil (λz. z = x) xs) + 1) xs" by simp
        from 1 have 2: "takeUntil (λz. z = x) (a # xs) = a # takeUntil (λz. z = x) (xs)" by simp
        from 1 have "drop (length (takeUntil (λz. z = x) (a # xs)) + 1) (a # xs) = drop (length (takeUntil (λz. z = x) xs) + 1) xs" by simp
        hence ?case using IH 2 by simp
      }
      note noteq = this
      have "a = x ∨ a ≠ x" by simp
      thus ?case using eq noteq by blast
    qed
    with 2 have 3: ?thesis by blast
    thus "xs = takeUntil (λz. z = x) xs @ x # drop (length (takeUntil (λz. z = x) xs) + 1) xs" by simp
    from 3 show "x ∉ elems (takeUntil (λz. z = x) xs)" by simp
  qed
  thus ?thesis by blast
qed

但它似乎相当长。特别是，我觉得在这里调用排中律比较麻烦，我觉得应该有一些方便的示意图变量?goal，比如可以引用当前目标什么的。

我怎样才能在不牺牲清晰度的情况下缩短这个证明？

4

2 回答 2

1

并不是您的具体问题的真正答案，但我仍然想指出，更简洁的证明仍然可以理解。

lemma "x ∈ elems xs ⟹ ∃ ys zs. xs = ys @ x # zs ∧ x ∉ elems ys"
proof (induction)
  case (Cons l ls)
  thus ?case
  proof (cases "x ≠ l")
    case True
    hence "∃ys zs. ls = ys @ x # zs ∧ x ∉ elems ys" using Cons by simp
    thus ?thesis using ‹x ≠ l› Cons_eq_appendI by fastforce
  qed (fastforce)
qed (simp)
于 2018-07-17T16:02:01.750 回答
0

这是另一个比你自己的更短的证明：

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

lemma elems_prefix_suffix:
  assumes ‹x ∈ elems xs›
  shows ‹∃pre suf. xs = pre @ [x] @ suf ∧ x ∉ elems pre›
using assms proof(induction xs)
  fix y ys
  assume *: ‹x ∈ elems (y#ys)›
    and IH: ‹x ∈ elems ys ⟹ ∃pre suf. ys = pre @ [x] @ suf ∧ x ∉ elems pre›
  {
    assume ‹x = y›
    from this have ‹∃pre suf. y#ys = pre @ [x] @ suf ∧ x ∉ elems pre›
      using * by fastforce
  }
  note L = this
  {
    assume ‹x ≠ y› and ‹x ∈ elems ys›
    moreover from this obtain pre and suf where ‹ys = pre @ [x] @ suf› and ‹x ∉ elems pre›
      using IH by auto
    moreover have ‹y#ys = y#pre @ [x] @ suf› and ‹x ∉ elems (y#pre)›
      by(simp add: calculation)+
    ultimately have ‹∃pre suf. y#ys = pre @ [x] @ suf ∧ x ∉ elems pre›
      by(metis append_Cons)
  }
  from this and L show ‹∃pre suf. y#ys = pre @ [x] @ suf ∧ x ∉ elems pre›
    using * by auto
qed auto ― ‹Base case trivial›

我使用了 Isar 的一些特性来压缩证明：

  1. 大括号内的块{...}允许您执行假设推理。
  2. 事实可以使用明确命名note。
  3. 关键字启动一个计算，当moreover它们被建立时隐含地“携带”事实。计算“来到头”与ultimately关键字。这种风格可以显着减少在证明过程中需要引入的明确命名的事实的数量。
  4. 通过应用于所有剩余的子目标来qed auto完成证明。auto评论指出，剩余的子目标是归纳的基本情况，这是微不足道的。
于 2018-07-31T07:58:50.097 回答