4

Isabelle/HOL で自己定義add関数の可換性を証明しようとしています。私は結合性を証明することができましたが、私はこれにこだわっています。

の定義add:

fun add :: "nat ⇒ nat ⇒ nat" where
"add 0 n = n" |
"add (Suc m) n = Suc(add m n)"

結合性の証明:

lemma add_Associative: "add(add k m) z = add k (add m z)"
apply(induction k)
apply(auto)
done

可換性の証明:

theorem add_commutativity: "add k m = add m k"
apply(induction k)
apply(induction m)
apply(auto)

次の目標を達成します。

goal (3 subgoals):
1. add 0 0 = add 0 0
2. ⋀m. add 0 m = add m 0 ⟹
     add 0 (Suc m) = add (Suc m) 0
3. ⋀k. add k m = add m k ⟹
     add (Suc k) m = add m (Suc k)

auto を適用すると、サブゴール 3 だけが残ります。

3. ⋀k. add k m = add m k ⟹
     add (Suc k) m = add m (Suc k)

編集：私は正しい方向へのプッシュとして、答えを探しているわけではありません。これらは Concrete Sementics という本からの演習です。

4

2 に答える 2

8

証明を可能な限りモジュール化することをお勧めします (つまり、後で可換性証明を解くのに役立つ中間レンマを証明します)。この目的のために、induct(あなたの のような)完全な自動化を適用する前に、によって導入されたサブゴールについて熟考することは、多くの場合、より有益apply (auto)です。

lemma add_comm:
  "add k m = add m k"
  apply (induct k)

この時点でのサブゴールは次のとおりです。

 goal (2 subgoals):
  1. add 0 m = add m 0
  2. ⋀k. add k m = add m k ⟹ add (Suc k) m = add m (Suc k)

それらを別々に見てみましょう。

  1. の定義を使用するaddと、左辺、つまり のみを単純化できadd 0 m = mます。次に、問題はどのように証明するかadd m 0 = mです。これを主な証明の一部として行いました。次の別の補題を証明することで可読性が向上すると私は主張します

    lemma add_0 [simp]:
  "add m 0 = m"
  by (induct m) simp_all

    simpを使用して自動化ツール (や などauto)に追加し[simp]ます。この時点で、最初のサブゴールは解決できsimp、2 番目のサブゴールだけが残ります。

  2. の定義とadd帰納仮説 ( add k m = add m k) を適用した後、 を証明する必要がありSuc (add m k) = add m (Suc k)ます。これは、 の元の定義の 2 番目の方程式に非常によく似ていますがadd、引数が入れ替わっているだけです。(その観点から、最初のサブゴールに対して証明しなければならなかったことは、 with swapped arguments の定義の最初の方程式に対応していましたadd。) さて、先に進むために、一般的な補題を証明することをお勧めしadd m (Suc n) = Suc (add m n)ます。

于 2014-07-18T11:39:59.930 に答える
3

私はクリスの答えのコメントでRainyCatsの質問に答えます：「イザベルはどのように証明するか」. addIsar で、手動と段階的の両方の結合性の詳細な証明を行います。

結合性のために手動で、k の帰納法によって:

  • for k=0を証明する必要がありadd (add 0 m) z = add 0 (add m z)ます。

    の定義で書き直しますadd。

    • add (add 0 m) z⇢add m z
    • add 0 (add m z)⇢add m z

    次に、ゴールは の再帰性によって証明され=ます。

  • k=のためにSuc k'

    • 想定してadd (add k' m) z = add k' (add m z)います。
    • 証明する必要がありadd (add (Suc k') m) z = add (Suc k') (add m z)ます。

    の定義で書き直しますadd。

    • add (add (Suc k') m) z⇢ add (Suc (add k' m)) z⇢Suc (add (add k' m) z)
    • add (Suc k') (add m z)⇢Suc (add k' (add m z))

    帰納仮説による：Suc (add (add k' m) z)⇢Suc (add k' (add m z))

    そして、ゴールは の再帰性によって証明され=ます。

この詳細レベルの Isar では、次のようになります。

lemma add_Associative: "add(add k m) z = add k (add m z)"
proof (induction k)
  case 0
    have "add (add 0 m) z = add m z" by (subst add.simps, intro refl)
    moreover have "add 0 (add m z) = add m z" by (subst add.simps, intro refl)
    ultimately show ?case by (elim ssubst, intro refl)
next
  case (Suc k')
    have "add (add (Suc k') m) z = add (Suc (add k' m)) z" by (subst add.simps, intro refl)
    also have "… = Suc (add (add k' m) z)" by (subst add.simps, intro refl)
    also have "… = Suc (add k' (add m z))" by (subst Suc, intro refl)
    moreover have "add (Suc k') (add m z) = Suc (add k' (add m z))" by (subst add.simps, intro refl)
    ultimately show ?case by (elim ssubst, intro refl)
qed

可能な限り最小のステップを作成し、すべてby ...をby simp.

于 2014-07-19T21:25:49.233 に答える