insertion-sort - 使用 Isabelle 证明插入排序算法

我在 Isabelle/HOL 中实现了一些插入排序算法来生成代码(ML、Python 等)。我确信相应的函数工作正常，但我需要创建一些定理来证明它并且非常确定它工作正常。我的功能是这些:

(* The following functions are used to prove the algorithm works fine *)
fun menor_igual :: "nat ⇒ nat list ⇒ bool" where
"menor_igual n [] = True" |
"menor_igual n (x # xs) = (n ≤ x ∧ menor_igual n xs)"

fun ordenado :: "nat list ⇒ bool" where
"ordenado [] = True" |
"ordenado (x # xs) = (menor_igual x xs ∧ ordenado xs)"

fun cuantos :: "nat list ⇒ nat ⇒ nat" where
"cuantos [] num = 0" |
"cuantos (x # xs) num = (if x = num then Suc (cuantos xs num) else cuantos xs num)"


(* These functions make the algorithm itself *)
fun insertar:: "nat ⇒ nat list ⇒ nat list" where
"insertar num [] = [num]" |
"insertar num (x # xs) = (if (num ≤ x) then (num # x # xs) else x # insertar num xs)"

fun asc :: "nat list ⇒ nat list" where
"asc [] = []" |
"asc (x # xs) = insertar x (asc xs)"

问题是我不知道如何正确创建定理。我需要证明有序列表与原始列表的长度相同，并且两个列表具有相同的元素名称。我的第一个定理是:

theorem "ordenado (asc xs)"
apply (induction xs rule: asc.induct)
apply auto

theorem "cuantos (asc xs) x = cuantos xs x"
apply (induction xs rule: asc.induct)
apply auto

第一个定理试图证明列表是正确排序的，第二个定理试图证明两个列表具有相同的长度。

当我应用归纳和自动时，我希望得到 0 个子目标，这说明定理是正确的，算法工作正常，但在那之后我不知道如何删除子目标，我的意思是我不知道如何做简化规则( lemma [simp]: "" )来做到这一点，我会很感激你的帮助。

最佳答案

后

theorem "ordenado (asc xs)"
apply (induction xs rule: asc.induct)
apply auto

您仍然需要证明以下子目标:

1. ⋀x xs.
      ordenado (asc xs) ⟹
      ordenado (insertar x (asc xs))

即假设asc xs是有序的，你要证明insertar x (asc xs)是有序的。这建议首先证明关于 insertar 和 ordenado 之间交互的辅助引理

lemma ordenado_insertar [simp]:
  "ordenado (insertar x xs) = ordenado xs"
 ...

它指出当且仅当 insertar x xs 已经排序时，xs 才会排序。为了证明这个引理，你将再次需要辅助引理。这次是关于 menor_igual 以及 menor_igual 和 insertar 之间的交互。

lemma le_menor_igual [simp]:
  "y ≤ x ⟹ menor_igual x xs ⟹ menor_igual y xs"
  ...

lemma menor_igual_insertar [simp]:
  "menor_igual y (insertar x xs) ⟷ y ≤ x ∧ menor_igual y xs"
  ...

第一个指出，如果 y 小于等于 x 并且 x 小于等于 xs 的所有元素，那么 y 小于等于 xs 的所有元素，等等......

我把证明留作练习；)。

对于你的第二个定理，我建议遵循相同的配方。首先尝试 induct 后跟 auto(就像你已经做过的那样)，然后找出仍然缺少哪些属性，证明它们作为辅助引理并完成你的证明。

关于insertion-sort - 使用 Isabelle 证明插入排序算法，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/27085556/