情報証明論 第2章 証明の実行

第1節 もう少し証明らしい証明

目次


第1節 もう少し証明らしい証明

第2節 型の宣言や変換

第3節 変数の同等な型

第4節 型の階層


テスト

Logをみる

Back
 

第2章 証明の実行 第1節 もう少し証明らしい証明

 実は前章第6節の定理の例は、証明をつけなくても自明なものなのです。

証明部を全部削除し、

 theorem (x^2 = 1 implies x=1 or x=-1) implies
       (x^3 = 1 & x^2 =1 implies x=1 or x=-1);

としてチェックしてみます(環境部やreserve ...の部分はそのままで)。

 すると、エラーが0であることが分かります。つまりこの定理は、命題論理式として恒真命題に帰着できるものなのです。人がそれを知るには論理式を変形したり、真理値表を書いたりして苦労するのですが、Mizarのチェックプログラムは一瞬にしてそれを恒真であると判断するのです。

 そこでもう少し証明のいる例を示しましょう。x^3=x*x*x であることの証明です。

−−−
   theorem x^3=x*x*x
   proof
     thus x^3=x^2*x by POLYEQ_3:def 4 .=x*x*x by SQUARE_1:def 3;
   end;
−−−

 ここで 

  a= b .= d;

と = が繋がった部分は

  a=b ; then
b=d ;

を省略したものです。

 上の定理はどうでしょうか? 環境部を前のままでチェックしてみましょう。すると

−−−
theorem x^3=x*x*x
::>          *103
 proof
  thus x^3=x^2*x by POLYEQ_3:def 4 .=x*x*x by SQUARE_1:def 3;
::>           *103         *144,330
 end;

::>
::> 103: Unknown functor
::> 144: Unknown label
::> 330: Unexpected end of an item (perhaps ";" missing)
−−−

といくつもエラーが出てしまいます。エラーがたくさん出てもびっくりせずに(これらのエラーはかなりやっかいなものですが...)順に原因を考えてゆくようにします。

 まず *103 のエラーですが乗算が認識されていません。Element of COMPLEX について検索ページで検索してみると COMPLEX1に次のように定義されていることが分かります。

−−−
definition let z1,z2;
 redefine func z1 * z2 -> Element of COMPLEX equals
:: COMPLEX1:def 10
  [* Re z1 * Re z2 - Im z1 * Im z2, Re z1 * Im z2 + Re z2 * Im z1 *];
end;
−−−
そこでnotationにCOMPLEX1を加えます。またPOLYEQ_3がtheoremsに無いのでそれをtheorems部に加えます。そして再度チェックすると

−−−
theorem x^3=x*x*x
::>          *103
 proof
  thus x^3=x^2*x by POLYEQ_3:def 4 .=x*x*x by SQUARE_1:def 3;
::>           *103               *190 *103           *144,330
 end;

::>
::> 103: Unknown functor
::> 144: Unknown label
::> 190: Inaccessible theorem
::> 330: Unexpected end of an item (perhaps ";" missing)
−−−

 それでも *103 のエラーは消えていません。これはCOMPLEX1の定義が有効に働いていないためと思われますのでconstructors部にもCOMPLEX1を加えます。また新たにSQUARE_1の引用が認識されていないようなのでtheorems部にSQUARE_1も加えます。

 すると

−−−
theorem x^3=x*x*x
 proof
  thus x^3=x^2*x by POLYEQ_3:def 4 .=x*x*x by SQUARE_1:def 3;
::>                                         *4
 end;

::>
::> 4: This inference is not accepted
−−−

エラーは一気に減りました。*4 という推論に関するエラーだけがひとつ残りました。

 これはなぜでしょうか?