theory - 证明冒泡排序是按引理排序的

Question

我已经尝试证明这很有趣 bubble_main已订购，但似乎没有任何方法有效。这里有人能帮我证明引理is_ordered (bubble_main L)请。

我只是删除了我以前的所有引理，因为似乎没有一个能帮助 Isabelle 找到证明。
这是我的代码/理论:

text{*check if the list is ordered ascendant*}
fun is_sorted :: "nat list ⇒ bool" where
"is_sorted (x1 # x2 # xs) = (x1 < x2 ∧ is_sorted (x2 # xs))" |
"is_sorted x = True"


fun bubble_once :: "nat list ⇒ nat list" where
"bubble_once (x1 # x2 # xs) = (if x1 < x2 
                     then x1 # bubble_once (x2 # xs) 
                     else x2 # bubble_once (x1 # xs))" |
"bubble_once xs = xs"

text{*calls fun bubble_once  *}
fun bubble_all where
"bubble_all 0 L = L"|
"bubble_all (Suc n) L = burbuja_all n (bubble_once L)"


text{*main function *}
fun bubble_main where
"bubble_main L = bubble_main (length L) L"

text{*-----prove by induction-----*}

lemma "is_sorted (bubble_main L)"
apply (induction L)
apply auto
quickcheck  
oops

Answer 1

首先，我会修复你的定义。例如，使用您的版本
的 is_sorted在某种意义上太严格了，[0,0] 没有排序。这
也可以通过快速检查来检测。

fun is_sorted :: "nat list ⇒ bool" where
  "is_sorted (x1 # x2 # xs) = (x1 <= x2 ∧ is_sorted (x2 # xs))" |
  "is_sorted x = True"

bubble_all必须递归地调用自己。

fun bubble_all where
  "bubble_all 0 L = L"|
  "bubble_all (Suc n) L = bubble_all n (bubble_once L)"

和 bubble_main必须调用 bubble_all .

fun bubble_main where
  "bubble_main L = bubble_all (length L) L"

然后需要几个辅助引理来证明结果。
我在这里列出了一些，其他人在 sorry 中可见的。

lemma length_bubble_once[simp]: "length (bubble_once L) = length L"
  by (induct rule: bubble_once.induct, auto)

lemma is_sorted_last: assumes "⋀ x. x ∈ set xs ⟹ x ≤ y"
  and "is_sorted xs"
  shows "is_sorted (xs @ [y])" sorry

当然，主要算法是 bubble_all ，所以你应该证明 bubble_all的属性(property)，不适用于 bubble_main感应地。
此外，对列表长度(或迭代次数)的归纳
在这里是有利的，因为列表由 bubble_all 更改在递归调用中。

lemma bubble_all_sorted: "n ≥ length L ⟹ is_sorted (bubble_all n L)"
proof (induct n arbitrary: L)
  case (0 L) thus ?case by auto
next
  case (Suc n L)
  show ?case
  proof (cases "L = []")
    case True
    from Suc(1)[of L] True
    show ?thesis by auto
  next
    case False
    let ?BL = "bubble_once L"
    from False have "length ?BL ≠ 0" by auto
    hence "?BL ≠ []" by (cases "?BL", auto)
    hence "?BL = butlast ?BL @ [last ?BL]" by auto
    then obtain xs x where BL: "?BL = xs @ [x]" ..
    from BL have x_large: "⋀ y. y ∈ set xs ⟹ y ≤ x" sorry 
    from Suc(2) have "length ?BL ≤ Suc n" by auto    
    with BL have "length xs ≤ n" by auto
    from Suc(1)[OF this] have sorted: "is_sorted (bubble_all n xs)" .
    from x_large have id: "bubble_all n (xs @ [x]) = bubble_all n xs @ [x]" sorry
    show ?thesis unfolding bubble_all.simps BL id
    proof (rule is_sorted_last[OF x_large sorted])
      fix x
      assume "x ∈ set (bubble_all n xs)"
      thus "x ∈ set xs" sorry
    qed
  qed
qed

最终的定理就很容易实现了。

lemma "is_sorted (bubble_main L)"
  using bubble_all_sorted by simp

我希望，这有助于了解所需的方向。