Isabelle Tutorial その14
5.15 Forward Proof: Transforming Theorems
ここまでは後ろ向きの証明を扱ってきましたが、前向きに証明を行うこともできます。前向きの証明は、一般的な定理から固有の定理を導くのに便利です。例えば最大公約数の分配法則を考えます。
k * gcd(m, n) = gcd(k * m, k * n)
m = 1とすると次の新しい定理が得られます。
k = gcd(k, k * n)
この新しい定理は左右を入れ替えると、単純化ルールとして便利そうです。左右を入れ替え、さらにn = 1とするとまた新たな定理が得られます。
gcd(k, k) = k
変数への値の代入が前向きの証明ステップとなっています。
5.15.1 Modifying a Theorem using of, where and THEN
3.5.3で関数gcdを定義しました。これを使用して、分配法則を証明します。次の定理からスタートします。
?k * gcd ?m ?n = gcd (?k * ?m) (?k * ?n) (gcd_mult_distrib2)
まず、?mを1で置き換えます。ofは式に含まれる変数を左から順に、指定した値に置き換えます。
lemmas gcd_mult_0 = gcd_mult_distrib2 [of k 1]
[of k 1]はgcd_mult_distrib2の?kをkに、?mを1に置き換えます。lemmasは導出された式を新しい定理として定義します。この結果、gcd_mult_0は次のように定義されます。
k * gcd 1 ?n = gcd (k * 1) (k * ?n) (gcd_mult_0)
置き換えたくない変数にはアンダースコア(_)を使用します。例えば次のようにすると、?mを1に置き換え、?kはそのまま残ります。
gcd_mult_distrib2 [of _ 1]
whereを使用しても同様のことができます。
gcd_mult_distrib2 [where m=1]
whereでは変数名と値を直接指定します。複数の変数を指定する場合はandで繋げます。
gcd_mult_0に戻ります。simplifiedは単純化した式を返します。
lemmas gcd_mult_1 = gcd_mult_0 [simplified]
gcd_mult_1は次のように定義されます*1。
k = gcd k (k * ?n) (gcd_mult_1)
定理の左右を入れ替えるために対称律を使用します。
?s = ?t ==> ?t = ?s (sym)
lemmas gcd_mult = gcd_mult_1 [THEN sym]
この結果、gcd_multは次のように定義されます。
gcd k (k * ?n) = k (gcd_mult)
THEN symは定理にsymを適用し結果を返します。一般的にTHENは破壊規則とともに使用します。例えばTHEN specはALL x. Pから全称限量子を取り除き、THEN mpはP --> QをP ==> Qに変形します。
ofやwhere、THENは一度に適用できます。gcd_multは次のようにも定義できます。
lemmas gcd_mult = gcd_mult_distrib2 [of k 1, simplified, THEN sym]
定理のこのような定義方法は読みづらいため、補題の証明形式で定義し、証明の中で前向き証明を使用する方がいいでしょう。gcd_multは次のようにも定義できます。
lemma gcd_mult [simp]: "gcd k (k * n) = k" by(rule gcd_mult_distrib2 [of k 1, simplified, THEN sym])
この節の最初に登場したgcd(k, k) = kは次のように定義できます。
lemma gcd_self [simp]: "gcd k k = k" by(rule gcd_mult [of k 1, simplified])
5.15.2 Modifying a Theorem using OF
OFは前提を指定することで新しい式を作成します。次の定義が証明済みであるとします。
[|gcd ?k ?n = 1; ?k dvd ?m * ?n|] ==> ?k dvd ?m (relprime_dvd_mult)
まず、前提の最初の式のインスタンスを証明します。
lemma relprime_20_81: "gcd 20 81 = 1" by(simp add: gcd.simps)
この補題をOFで使用します。
relprime_dvd_mult [OF relprime_20_81]
この式は次の定理を作成します。
20 dvd (?m * 81) ==> 20 dvd ?m
次の例を見てみます。整除性に関する次の定理を使用します。
[|?k dvd ?m; ?k dvd ?n|] ==> ?k dvd ?m + ?n (dvd_add) ?m dvd ?m (dvd_refl)
dvd_addの二つの前提にdvd_reflを適用してみます。
dvd_add [OF dvd_refl dvd_refl]
結果は次のようになります。
?k dvd (?k + ?k)
ofと同じように、_を使用することもできます。
dvd_add [OF _ dvd_refl]
?k dvd ?m ==> ?k dvd ?m + ?k
5.16 Forward Reasoning in a Backward Proof
メソッドdrule、frule、drule_tacなどでも、mpやspecを適用することで前向きに証明できることを既に見ました。他にも、次のようなルールも使えます。
?x = ?y ==> ?f ?x = ?f ?y (arg_cong) ?i <= ?j ==> ?i * ?k <= ?j * ?k (mult_le_mono1)
例を見てみます。
lemma "2 <= u ==> u * m ~= Suc (u * n)" apply(intro notI)
1. [| 2 <= u; u * m = Suc (u * n) |] ==> False
次に、u * m = Suc (u * n)の両辺にmod uを適用します。
apply(drule_tac f="% x. x mod u" in arg_cong)
1. [| 2 <= u; u * m mod u = Suc (u * n) mod u |] ==> False
定理mod_Sucを使用するとこのサブゴールを証明できます。
Suc ?m mod ?n = (if Suc (?m mod ?n) = ?n then 0 else Suc (?m mod ?n)) (mod_Suc)
ここからは、前向きの証明のための新たなメソッドを見ていきます。
5.16.1 The Method insert
メソッドinsertは指定した定理を全てのサブゴールの前提に追加します。定理にofやTHENを付けることもできます。
例を見てみます。まず、gcdの分配法則を追加します。
lemma relprime_dvd_mult: "[|gcd k n = 1; k dvd m * n|] ==> k dvd m" apply(insert gcd_mult_distrib2 [of m k n])
得られるサブゴールを見ると、定理が前提に追加されていることがわかります。
1. [| gcd k n = Suc 0; k dvd m * n; m = gcd (m * k) (m * n) |] ==> k dvd m
残りの証明は省略します。
insertで追加された定理に含まれるスキーム変数は、新しいサブゴールではメタ全称限量子で限量化されます。
5.16.2 The Method subgoal_tac
subgoal_tacは任意の式を前提に追加します。さらに、現在のサブゴールの前提からその式が証明できることを、別のサブゴールとして追加します。例を見てみます。
lemma "[|(z::int) < 37; 66 < 2*z; z*z ~= 1225; Q(34); Q(36)|] ==> Q(z)" apply(subgoal_tac "z = 34 | z = 36") apply(blast) apply(subgoal_tac "z ~= 35") apply(arith) apply(force) done
前提の最初の三つから、zは34または36であることがわかります。そこでそれをsubgoal_tacで前提に追加しました。追加した結果、次のサブゴールが得られます。
1. [| z < 37; 66 < 2 * z; z * z ~= 1225; Q 34; Q 36; z = 34 | z = 36 |] ==> Q z 2. [| z < 37; 66 < 2 * z; z * z ~= 1225; Q 34; Q 36 |] ==> z = 34 | z = 36
一つ目のサブゴールは前提の指定した式が追加されています。二つ目のサブゴールは、追加した前提が正しいことの証明です。一つ目のサブゴールはblastで証明が完了し、二つ目のサブゴールにはさらにzが35ではないことを追加しています。残りはarithとforceで証明が完了します。
*1:私の環境ではうまくいきませんでした。なぜ？？
