定理証明と検証(全17回)

開発深知」から定理証明と検証の講義動画を紹介します。動画をご覧になるには、開発深知の会員登録(無料)が必要です。

講義概要

本講義では、強力な仕様記述能力を持ち,また証明を支援する機構を備えている定理証明器「Coq」をとりあげます。

Coqをプログラムの検証ツールとして捉え、次のことができることを目標にします。

  • Coqで基本的なプログラムを記述する
  • Coqでプログラムの満たすべき性質を記述する
  • Coqでそれを証明する

01_講義の目標

Coq入門として学習することが可能です。本講義は動画と小テストの構成になっております。

講義は、こちらから登録することができます。
定理証明と検証 | 開発深知
また、動画をご覧になる場合には、開発深知の会員登録(無料)が必要です。
開発深知登録方法について | 開発深知ブログ

本講義の構成

その1:証明支援器Coqとは
定理証明器(自動定理証明器、対話的定理証明器)、仕様記述言語、対話的定理証明器の例(Coq、Agda、Isabell/HOL)、CoIC(Calculus of Inductive Constructions)、Coqの利用事例、Coqの導入、Extractionの対象となる言語について解説します。
その2:プログラム検証の流れ
EmacsのProofGeneralという環境を使って、実際にCoqのプログラムやプログラム検証の流れを見ていきます。
その3:Coqの基本
Coqを操作するコマンド(Vernacularコマンド、タクティック)、Coqの式(プログラムの式、プログラムの型、仕様(論理式)、証明)、型付け関係、プログラミング言語としての式、仕様記述言語としての式、Coqの原理(Prop型)、型の階層構造、Coqの式のおおよその分類、Coqにおける証明について解説します。
その4:Vernacularコマンド
Coqを操作するVernacularコマンド(Definition、Require Import、Open Scope、Check、Print、Compute、Theorem、Lemma、Proof、Qed、Admitted、Section、Variable(s)、Hypothesis(es)、Locate、Infix、Notation、SearchPattern、SerchRewrite、Extraction)について解説し、Vernacularコマンドの調べ方について紹介します。
その5:プログラミング言語としてのCoq(1)
Coqでの関数プログラミングの基本について学んでいきます。関数プログラミング、準備、値の例、変数定義、関数定義、関数適用、条件分岐、場合分け、基本のパターン(パターンマッチ)、その他の基本データ(タプル、オプション)、局所的な変数、関数の定義について解説します。
その6:プログラミング言語としてのCoq(2)
高階関数、高階関数の例、無名関数、関数の型、複数引数を取る関数の型、部分適用、多相性(polymorphism)について解説します。
その7:Induvtiveデータ型(1)
Coqで非常に良く使うInduvtiveなデータ型の定義や値の扱い、再帰関数の定義について学んでいきます。列挙型としてのInduvtive型、パターンマッチ、パメラータ付き列挙型、多相的なInduvtive型、自然数の定義、自然数の例、再帰的な関数について解説します。
その8:Induvtiveデータ型(2)
リスト型の定義、リストオブジェクトの例、リストを扱う関数、リストの記法、再帰関数と停止性について解説します。また、Coqと他のプログラミングとの大きな違いとして、停止しない関数をかくことができない点について紹介します。
その9:仕様記述言語としてのCoq(1)
3回にわたって、論理式のCoqの構文による形式化、基本的なタクティックを用いた論理式の証明、帰納法を使った証明でリストに関する性質の証明について学んでいきます。Coqでの仕様記述、Coqでの証明、Theoremコマンド、introタクティック、applyタクティック、証明モードの終了、∧(かつ)の証明(∧が前提にあるとき)、論理演算子に関するタクティック早見表、タクティックの調べ方について解説します。
その10:仕様記述言語としてのCoq(2)
等式の証明(ゴールに等式があるとき、前提に等式があるとき)、simleタクティック、unfoldタクティック、場合分けによる証明について解説します。
その11:仕様記述言語としてのCoq(3)
帰納法による証明、inductionタクティック、リストに関する帰納法、reverse関数の性質について解説します。
その12:証明付きデータ型
証明付きデータ型(symbol型、sig型、制約付きオブジェクト)のsumbool型について学んでいきます。sumbookと証明、sumbool型を返す判定関数の定義、タクティックによる関数定義、refineタクティック、その他の判定関数、その他の証明付きデータ型について解説していきます。
その13:再帰関数と停止性
トランプシャッフルの例を元に再帰関数と停止性について学んでいきます。上手く行かない例、Functionコマンドによる再帰関数の定義、停止性の証明、Functionによる再帰関数、shuffle関数の使い方、shuffle関数の実態、shuffle関数の使い方、shuffle_equation、shuffleに関する帰納法について解説します。
その14:CoInductiveデータ型
無限の要素を持つデータ型を表現するためのCoInductiveデータ型について学んでいきます。Stream型の定義、CoInductiveなデータ型に対する再帰、CoFixpointとFixpoint、Fixpointの例、CoFixpointの例(再帰関数)、どちらにも該当する場合について解説します。
その15:既存のプログラムとの連携
Extraction機能、連携できるプログラミング言語(OCaml、Haskell、Schemeなど)、Extractionの実行とソースコードの生成(OCaml)、OCamlからの呼び出しコード、OCamlプログラムのコンパイル、Extract Inductiveコマンド、Extract Constantコマンド、OCamlへのExtractionのための便利なライブラリについて解説していきます。
その16:タクティカル
タクティックを修飾したり、結合したりするためのタクティカルについて学んでいきます。タクティックの合成、;の例、;タクティカル、制御構造、repeatタクティックの使用例、tryタクティックの使用例、タクティックのいろいろな役割、その他の基礎的なタクティック、solveタクティックの使用例について解説していきます。
その17:証明の自動化
自動証明と対話証明、証明の自動化(自明なゴールを自動で証明するタクティック)、autoで証明できる例、autoのアルゴリズム、auto用の仮定の追加、ringタクティック、omegaタクティック、自動証明支援器とタクティックについて解説します。

講師

有限会社 ITプランニング
今井宜洋先生
※講座内容や講師の所属に関しましては、収録時の情報を掲載しております。変更になっている場合がございますので、ご了承いただきますようお願いします。

小テストの例

本講義では、各講義動画と合わせて小テストを設定しております。小テストの解答については、定理証明と検証 | 開発深知の講義でご確認ください。
スクリーンショット 2015-03-31 12.07.34

定理証明と検証のダイジェスト動画

本講義は、トップエスイーの講義動画のダイジェスト版です。
開発深知で公開している最新版とは内容が多少異なっております。講義内容を把握するための参考としてご覧ください。

講義スライド

定理証明と検証の講義からスライドをピックアップしてご紹介します。

仕様記述言語

02_仕様記述言語

  • 多くの検証ツールでは検証したいことを記述するための、仕様記述言語がある
  • 仕様記述言語は形式的仕様を数学の論理式で表現することが多い
  • 論理式と言ってもいろいろな論理体系があり、ツールによって異なる
  • 使っている論理体系によって、仕様記述言語の表現力は大きく異なる

定理証明器

03_定理証明器

自動定理証明器
・全自動で証明を構築
・仕様記述言語の表現力が低い
対話的定理証明器
・手動で証明を作成
・仕様記述言語の表現力が高い

つまり、対話的定理証明器は、強力な仕様記述の表現力を持つというメリットがある一方、手間がかかるというデメリットがあるというツールである。

対話的定理証明器の例

04_対話的定理証明器の例

Coq
本講座で扱う検証器、半自動証明を実現するための卓ティックという機能を備え、部分的な自動証明が可能。OCaml、Haskell、Schemeなどのプログラミング言語と連携。
Agda
Haskellで書かれた仕様記述言語兼プログラミング言語。Coqとよく似た理論をベースに持つ。プログラミング言語としての特徴が強く、それ自身がコンパイラとしても振舞う。
Isabelle/HOL
Standerd MLで書かれた老舗の証明支援器。高階論理を使って形式的証明を行う。lserという証明言語を使って証明を構築する。

Coqを操作するコマンド

01_Coqを操作するコマンド
Coqを操作するための次の種類のコマンドがある。いずれもピリオドでコマンドの終了を示す。

  • Vernacularコマンド:単にコマンドとも言う、コマンド名は大文字で始める
  • タクティック:証明作成用コマンド、コマンド名は小文字で始まる

Coqの式

02_Coqの式
Coqの式は表現力が非常に強い。次の全てはCoqでは単に式として表現される。

  • プログラムの式:(1+2, “hello”, (fun x => x+1))など。
  • プログラムの型:(bool, list nat)など
  • 仕様(論理式):(formal x, x=0 -> x+x=0 ∧ x*x=0)
  • 証明

その正体は単なる式である。

仕様記述言語としての式

03_仕様記述言語としての式
命題を表す式はProp型を持つ。
Check (2+1 = 3).
2 + 1 = 3 : Prop
Check Prop.
Prop : Type
「=」はProp型の式を構成する演算子。

関数プログラミング

146004_関数プログラミング
Coqの式は純粋関数型言語である:

  • 代入ではなく、変数の値があとで変更されることはない
  • 全ての関数の戻り値は、入力によってのみ決定し、同じ引数を渡せば、いつでも同じように振る舞う
  • 全てのデータ型は不変データ構造である
  • 関数を組み合わせて、プログラミングを行う

これによって次のようなメリットがある

  • プログラムの依存関係が明確になる
  • 暗黙の状態などがなくなり、見通しが良くなる
  • 全ての関数を数学的な対象として扱うことができ、証明など検証しやすい

多相性

146005_多相性
多相性(polymorphism)はJavaやC#ではジェネリクスなどとも呼ばれ、多くの静的型付き言語が持つ機能である。
多相性を使う最も単純な例は恒等関数であろう。プログラミング言語で記述例を記載する。

ソースコード3:OCamlの例
(* id : 'a -> 'a *)
let id x = x

ソースコード4:Haskellの例
id :: a -> a
id x = x

ソースコード5:Javaの例
public static final <A> A id(final A x){
return x;
}

Inductiveなデータ型

146006_Inductiveなデータ型

Inductive型は帰納型とも呼び、非常によく使われる機能である。Coqではほとんどのデータ型がInductive型である。

この節の目標:

  • Inductiveコマンドによるデータ型の定義
  • パターンマッチを使ったIncuctive型の値の扱い
  • 再帰関数の定義

Inductive型はJavaやC#などの列挙型、MLやHaskellなどにおける代数的データ型、GADTなどによく似ているが、それら以上の強力な表現力を持つ。

再帰関数と停止性

146007_再帰関数と停止性

  • Coqでは停止しない関数を書くことはできない
  • Curry-Howard対応により、停止しない関数を書けることは論理体系の矛盾を意味する
  • 今回定義したlength関数などは、再帰呼び出しの度に引数が「小さく」なっていたので停止することは自明
  • より複雑な再帰関数については後の講義で扱う

Coqでの仕様記述

146008_Coqでの仕様記述

等式の証明

146009_等式の証明

Coqでは a = b のような等式はProp型の式となる。

Compute (0 = 0). をしてもTrueは得られない。その代わり、証明(その型を持つ式)を与えることによってその正しさを保証する。

帰納法による証明

146010_帰納法による証明

自然数natに関する帰納法

  • 数学的帰納法:任意の自然数nについてPnが成り立つのは以下のとき
     ・n = 0のときPnが成り立つ
     ・Pkが成り立つと仮定したときにP(k+1)が成り立つ

証明付きデータ型

146011_証明付きデータ型

これまでは、プログラムと証明を分けて扱っていた。しかし、データ型には何らかの性質を満たすための証明を含めることができる。証明付きデータ型は次のような例がある。

  • sumbool型
  • sig型
  • 制限付きオブジェクト

Functionコマンドによる再帰関数の定義

146012_Functionコマンドによる再帰関数の定義

Functionコマンドではより複雑な再帰関数が定義できる。Functionコマンドを便利に使うためにはRecdefモジュールが必要である。

Require Import Recdef.
【構文】Functionコマンドによる再帰関数
Function関数名 引数1...引数n{減少に関するアノテーション}:=関数本体.
停止性の証明

「減少に関するアノテーション」の部分は、再帰呼び出しがどういう意味で減少するかを指定できる。いくつかの指定方法があるが、今回はmeasureによる指定方法を説明する。

【構文】measureアノテーション
{mesure 大きさを測る関数 引数名}

CoInductive:無限のデータ構造

146013_CoInductive:無限のデータ構造

無限の要素を持つデータ型を表現するためのCoInductiveデータ型を紹介する。CoInductiveデータ型はCoInductiveというコマンドで、Inductive型と同様に定義できる。

【構文】CoInductiveコマンド
CoInductive型名 型引数:型:=
|コンストラクタ名:コンストラクタの型
|コンストラクタ名:コンストラクタの型
...

連携できるプログラミング言語

146014_連携できるプログラミング言語

Coqがデフォルトでサポートしているターゲット言語

  • OCaml
  • Haskell
  • Scheme

その他の言語との連携のための拡張への挑戦

  • Coq2Scara(*1,2)
  • Coq Ruby(*3)
  • Coq Clojure ext(*4)

*1 http://proofcafe.org/wiki/Coq2Scala
*2 http://github.com/hemmi/coq2scala
*3 http://github.com/mzp/coq-ruby
*4 http://patch-tag.org/r/leque/coq-clojure-ext/home

タクティカルとは

146015_タクティカルとは

  • タクティカルとはタクティックを修飾したり、結合したりするものである
  • タクティカルを使うことで、よりシンプルでわかりやすい証明の記述ができる

証明の自動化

146016_証明の自動化

自明なゴールを自動で証明するタクティックをいくつか紹介する。

  • 探索による自動証明:可能な補題と仮定を適用することにより証明を試みる方法:autoタクティック等
  • 決定手続きによる証明:特定分野の問題を証明するためのアルゴリズム:omega、ring、タクティック等

スライドの詳細な説明については、定理証明と検証 | 開発深知の講義動画をご覧ください。
また、講義動画は開発深知の会員登録(無料)を行う必要がございます。

関連講義

定理証明と検証の関連講義について紹介します。

Coqで学ぶ定理証明入門
対話的定理証明器や自動定理証明器、Coqを使った関数型プログラミングのテクニック、CoqIde、タクティックを使った証明の技法について解説します。
MindStormで学ぶ、UPPAALによる時間制約の検証
時間制約を扱えるモデル検査ツールUPPAALを使って、時間に関する情報をUPPAALでモデル化し、時間制約を検証する手法について解説します。

参考リンク

トップエスイー | サイエンスによる知的ものづくり教育プログラム
NPO法人トップエスイー教育センター
トップエスイーチャンネル(TopSE Channel)

ソフトウェア開発者のための学習サイト「開発深知」については、開発深知とはをご覧ください。