3

コード (ML、Python など) を生成するために、Isabelle/HOL で挿入ソート アルゴリズムを実装しました。対応する関数が正常に機能すると確信していますが、それを証明するためにいくつかの定理を作成し、それが確実に機能することを確認する必要があります。私の機能は次のとおりです。

(* 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

最初の定理はリストが正しく順序付けられていることを証明しようとし、2 番目の定理は両方のリストが同じ長さであることを証明しようとします。

誘導と自動を適用すると、サブゴールが0になると予想されます。これは、定理が正しく、アルゴリズムが正常に機能することを示していますが、その後、サブゴラスを削除する方法がわかりません。簡略化規則 ( lemma [simp]: "") を使用してください。よろしくお願いします。

4

1 に答える 1

2

後

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_igualinsertar

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小さいと等しい場合、のすべての要素が小さいと等しい、などと述べています。xxxsyxs

証明は演習として残しておきます ;)。

2 番目の定理については、同じレシピに従うことをお勧めします。最初inductに（すでに行ったように）続いて試しautoてから、まだ欠けているプロパティを見つけ、それらを補助補題として証明し、証明を完成させます。

于 2014-11-24T16:12:37.447 に答える