Coq/SSReflect/MathComp による定理証明を読んで(1)

@aintek on Wed Sep 04 2019
2.1 min

目次

本書における命題、定理、補題、言明について

  • 命題とは: 論理的に真か偽かが定まる主張
  • 定理とは: 命題の内、真であるもの
  • 補題とは: 定理の別名
  • 言明とは: 命題の主張を表す文章や記号の列

形式化とは

私たちが普段使うような文章(言明)を、定理証明支援器(支援系)向けに変換すること。

Coqは、これらの言明の正しさをチェックする定理証明支援器の1つ。

どのように支援器は正しさを保証するか

定理証明支援器の根幹をなす、数学基礎論によって保証する。
これは定理証明支援器が数学基礎論を機械化(ソフトウェア化)したものであることから。

Coqは 型理論 と呼ばれる基礎論に基づいて実装されている。

型理論の基礎

型理論は、その名の通り という概念が根幹をなしている。

a : A

と書くと 「型Aの要素a」 という意味を表す。
これは集合でいうところの「集合Aのaという要素」と全く同じ意味である。

論理演算

形式論理 での論理和

A \/ B

A + B

と表す型に対応させる。A + Bは「AまたはBの型(の要素)で構成される型」という意味。

なお、A + BB + A は別の型を意味する。

形式論理 での論理積

A /\ B

は、型理論では、∑x: A, B を表す型に対応させる。これは、順序対(a,b)を要素に持つ型を意味する。

形式論理での含意

A --> B

は 型理論の Πx: A, B を表す型に対応させる。これは、関数 f: A --> B に相当する要素によって構成される型、すなわち A型からB型への写像を持つ関数という捉え方ができる。

最後に

なぜかMathJaxが動かない・・・
きれいな数式が書けない!!!書きたい!!!

日別に記事を見る