Symbols_J:概要

Preface_J:前書き

• 前書き
• 概要
• 実際の学習について
  • 章間の依存関係
  • 学習者に要求される知識的前提
• Coqについて
  • 学習に必要なもの
  • 教材となるCoqファイルの入手方法
• 練習問題について
• 推奨書籍
• 教育関係者へ

Basics_J: 関数プログラミングとプログラムの証明

• 列挙型
  • 曜日の表し方
  • ブール型
  • 関数の型
  • 数値
• 簡約を用いた証明
• introsタクティック
• 書き換え（Rewriting）による証明
• Case分析
• Caseへのネーミング
• 帰納法
• 形式的証明と非形式的証明
• 証明の中で行う証明
• さらなる練習問題

Lists_J: 直積、リスト、オプション

• 数のペア
• 数のリスト
• リストを使ったバッグ
• リストに関する推論
  • お小言
  • リスト上の帰納法
  • SearchAbout
  • リストについての練習問題 (1)
  • リストについての練習問題 (2)
• オプション
• apply タクティック
• 帰納法の仮定を変更する
• 練習問題: 辞書

Poly_J: 多相性と高階関数

• ポリモルフィズム（多相性）
  • 多相的なリスト
    • 型推論
    • 引数の同化（Synthesys）
    • 暗黙の引数
    • 練習問題:多相的なリスト
  • 多相的なペア
  • 多相的なオプション
• データとしての関数
  • 高階関数
  • 部分適用
  • 余談： カリー化
  • フィルター (Filter)関数
  • 無名（匿名）関数
  • マップ（Map）関数
  • 畳み込み（Fold）関数
  • 関数を作成する関数
• さらにCoqについて
  • unfoldタクティック
  • 反転（Inversion）
  • タクティックを仮定に使用する
  • destructを複合式で使う
  • rememberタクティック
  • apply ... with ...タクティック
• まとめ
• さらなる練習問題

Gen_J: 帰納法の仮定の一般化

Prop_J: 命題と根拠

• 命題によるプログラミング
• 根拠
  • 帰納的に定義された命題
  • 証明オブジェクト
  • カリー・ハワード対応
  • 含意
  • 帰納的に定義された型に対する帰納法の原理
  • 帰納法の仮定
  • 偶数について再び
  • 根拠に対する帰納法の推論
  • なぜ命題を帰納的に定義するのか?
• 全体像: Coqの2つの空間
  • 値
  • 帰納的定義
  • 型と種類 (kinds)
  • 命題 vs. ブール値
  • 関数 vs. 限量子
  • 関数 vs. 含意
• 非形式的な証明
  • 帰納法による非形式的な証明
    • 帰納的に定義された集合についての帰納法
    • 帰納的に定義された命題についての帰納法
• 選択課題
  • induction タクティックについてもう少し
  • Prop における帰納法の原理
• 追加練習問題

Logic_J: Coqにおける論理

• 全称記号 と ならば
• 論理積、連言（Conjunction、AND）
  • Iff （両含意）
• 論理和、選言（Disjunction、OR）
  • ∧ 、 ∨ のandb 、orb への関連付け
• 偽であるということ
  • 真であるということ
• 否定
  • 不等であるということ
• 存在量化子
• 等しいということ（同値性）
  • Inversion 再び
• 命題としての関係
  • 少し脱線: <= と < についてのさらなる事実
• 選択課題
  • ∧ や ∨ のための帰納法の原理
  • 帰納法のための明白な証明オブジェクト
  • Coq の信頼できるコンピューティング基盤

Rel_J: 関係の性質

• 関係の基本性質
• 反射推移閉包

SfLib_J: Software Foundations ライブラリ

• Coq スタンダードライブラリから
• Basics.vから
• Props.vから
• Logic.vから
• 使い勝手のいいタクティックをいくつか

Imp_J: 単純な命令型プログラム

• Sflib
• 算術式とブール式
  • 構文
  • 評価
  • 最適化(Optimization)
• Coq の自動化
  • タクティカル(Tacticals)
    • tryタクティカル
    • ;タクティカル
  • 新しいタクティック記法を定義する
    • 場合分けを万全にする
  • omegaタクティック
  • 便利なタクティックをさらにいくつか
• 関係としての評価
  • 推論規則記法
• 変数を持つ式
  • 識別子
  • 状態
  • 構文
  • 評価
• コマンド
  • 構文
  • 例
• 評価
  • 評価関数
  • 関係としての評価
  • 関係による評価とステップ指数を利用した評価の等価性
  • 実行の決定性
• プログラムの検証
  • 基本的な例
  • プログラム正当性 (Optional)
• 追加の練習問題

ImpParser_J: Coqでの字句解析と構文解析

• 内部処理
  • 字句解析
  • 構文解析
    • Option と Error
    • シンボルテーブル
    • パーサ構築のための一般コンビネータ
    • Impの再帰下降パーサ
• 例

Equiv_J: プログラムの同値性

• 宿題割当てについての一般的アドバイス
• 振る舞い同値性
  • 定義
  • 例
• 振る舞い同値の性質
  • 振る舞い同値は同値関係である
  • 振る舞い同値は合同関係である
• ケーススタディ: 定数畳み込み
  • プログラム変換の健全性
  • 定数畳み込み変換
  • 定数畳み込みの健全性
  • (0 + n)の消去の健全性、再び
• プログラムが同値でないことを証明する
• 外延性を使わずに行う (Optional)
• さらなる練習問題

ImpList_J: Imp のリスト拡張

• リストを持つ Imp プログラム
  • 定義の繰り返し
  • 拡張
  • 定義の繰り返し

Hoare_J: ホーア論理

• ホーア論理
  • 表明
  • ホーアの三つ組
  • 最弱事前条件
  • 証明規則
    • 代入
    • 帰結
    • 余談: eapply タクティック
    • Skip
    • コマンド合成
    • 条件分岐
    • ループ
    • 練習問題: REPEATのホーア規則
    • 修飾付きプログラム
  • ホーア論理によるプログラムについての推論
    • 例: 遅い引き算
    • 練習問題: ゼロへの簡約
    • 練習問題: 遅い足し算
    • 例: パリティ
    • 例: 平方根の探索
    • 練習問題: 階乗
    • リストを扱うプログラムについての推論
  • 修飾付きプログラムの形式化
    • 構文
    • 検証条件の抽出
    • 例

HoareAsLogic_J: 論理としてのホーア論理

Smallstep_J: スモールステップ操作的意味論

• おもちゃの言語
  • 値
  • 強進行と正規形
  • 練習問題
• マルチステップ簡約
  • マルチステップ簡約
  • 正規形再び
  • ビッグステップ簡約とスモールステップ簡約の同値性
  • さらなる練習問題
• スモールステップ Imp
• 並列実行 Imp

Types_J: 型システム

• さらに自動化
  • auto と eauto タクティック
  • Proof with タクティック
  • solve by inversion タクティック
  • try solve タクティック
  • f_equal タクティック
  • normalize タクティック
• 型付きの算術式
  • 構文
  • スモールステップ簡約
  • 正規形と値
  • 型付け
  • 進行
  • 型保存
  • 型の健全性
  • 追加演習

Stlc_J: 単純型付きラムダ計算

• 単純型付きラムダ計算
  • 概観
  • 構文
    • 型
    • 項
  • 操作的意味論
    • 値
    • 自由変数と置換
    • 簡約
    • 例
  • 型付け
    • コンテキスト
    • 型付け関係
    • 例
  • 性質
    • 自由な出現
    • 置換
    • 保存
    • 進行
    • 型の一意性
  • さらなる練習問題
• 練習問題: 算術を持つSTLC
  • 構文と操作的意味

Typechecking_J: STLCの型チェッカ

• 型を比較する
• 型チェッカ
• 性質

MoreStlc_J: 単純型付きラムダ計算についてさらに

• STLCの単純な拡張
  • 数値
  • let束縛
  • 対
  • 直和
  • リスト
  • 一般再帰
  • レコードとバリアント (Optional)
    • Unit型
    • レコード
    • レコードのエンコード
    • バリアント
• 拡張を形式化する
  • 構文と操作的意味
  • 置換
  • 簡約
  • 型付け
  • 例
    • 準備
    • 数値
    • 直積
    • let
    • 直和
    • リスト
    • fix
  • 型付けの性質
    • 進行
    • コンテキスト不変性
    • 保存

Records_J: STLCにレコードを追加する

• レコードを追加する
• レコードを形式化する
  • 構文と操作的意味
  • Well-Formedness(正しい形をしていること、整式性)
  • 置換
  • 簡約
  • 型付け
  • 例
  • 型付けの性質
    • Well-Formedness
    • フィールドのルックアップ
    • 進行
    • コンテキスト不変性
    • 保存

References_J: 変更可能な参照の型付け

• 定義
• 構文
  • 型
  • 項
  • 型付け (プレビュー)
  • 値と置換
• プラグマティクス(語用論)
  • 副作用と順次処理
  • 参照と別名付け
  • 共有状態
  • オブジェクト
  • 参照と合成型
  • null参照
  • ガベージコレクション
• 操作的意味
  • 場所(Locations)
  • 記憶(Stores)
  • 簡約
• 型付け
  • 記憶の型付け
  • 型付け関係
• 性質
  • 型付けできる記憶
  • 記憶型付けを拡張する
  • 保存、最終的に
  • 置換補題
  • 代入は記憶型付けを保存する
  • 記憶についての弱化
  • 保存!
  • 進行
• 参照と非停止性
• さらなる練習問題

Subtyping_J: サブタイプ

• 概念
  • 動機付けのための例
  • サブタイプとオブジェクト指向言語
  • 包摂規則
  • サブタイプ関係
    • 直積型
    • 関数型
    • Top
    • 構造規則
    • レコード
    • 直積と Top によるレコード (optional)
• 中核部の定義
  • 構文
  • 包摂
  • 簡約
• サブタイプ
  • 定義
  • サブタイプの例と練習問題
• 型付け
  • 型付けの例
• 性質
  • サブタイプの反転補題(Inversion Lemmas)
  • 正準形(Canonical Forms)
  • 進行
  • 型付けの反転補題
  • コンテキスト不変性
  • 置換
  • 保存
  • 型付けの練習問題
• 練習問題: 直積の追加

RecordSub_J: レコードのサブタイプ

• 中核部の定義
  • 構文
  • Well-Formedness
  • 置換
  • 簡約
• サブタイプ
  • 定義
  • サブタイプの例と練習問題
  • サブタイプの性質
    • Well-Formedness
    • フィールド参照
    • 反転補題
• 型付け
  • 型付けの例
  • 型付けの性質
    • Well-Formedness
    • フィールド参照
    • 進行
    • 反転補題
    • コンテキスト不変性
    • 保存
  • 型付けの練習問題

Norm_J: STLCの正規化

• 言語
  • 構文と操作的意味
  • 置換
  • 簡約
  • 型付け
  • コンテキスト不変性
  • 保存
  • 決定性
• 正規化
  • R_T の要素であるか否かは評価によって変化しない
  • R_Tに含まれる型Tの項の閉じたインスタンス
    • 多重置換、多重拡張、インスタンス化
    • 置換についてのさらなる事実
    • 多重置換の性質
    • 多重拡張の性質
    • インスタンス化の性質
    • stepmany(⇒*)についての合同補題
    • R補題
    • 正規化定理

UseTactics_J: Coq用タクティックライブラリのご紹介

• 導入と場合分けについてのタクティック
  • タクティックintrov
  • タクティックinverts
  • タクティックcasesとcases_if
• n-引数論理演算のためのタクティック
  • タクティック splits
  • タクティック branch
  • タクティック ∃
• 等式を扱うタクティック
  • タクティック asserts_rewrite と cuts_rewrite
  • タクティック substs
  • タクティック fequals
  • タクティック applys_eq
• 便利な略記法をいくつか
  • タクティック unfolds
  • タクティックfalseとtryfalse
  • タクティック gen
  • タクティックskip、skip_rewrite、skip_goal
  • タクティック sort
• 高度な補題具体化のためのタクティック
  • letsのはたらき
  • applys、forwards、specializesのはたらき
  • 具体化の例

UseAuto_J: Coqの証明自動化の理論と実際

• 証明探索の基本性質
  • 証明探索の強さ
  • 基本
  • 連言
  • 選言
  • 存在限量
  • 否定
  • 等式
• 証明探索はどのようにはたらくか
  • 探索の深さ
  • バックトラック
  • ヒントを追加する
  • タクティックへの自動証明の統合
• 自動化の使用例
  • 決定性
  • STLC の保存
  • STLC の前進
  • ビッグステップとスモールステップ
  • STLCRef の保存
  • STLCRef の前進
  • サブタイプ
• 証明探索の進んだ話題
  • 補題を正しい方法で記述する
  • 証明検索中で定義を展開する
  • 不合理なゴールの証明の自動化
  • 推移性補題についての自動化
• 決定手続き
  • Omega
  • Ring(環)
  • Congruence(合同)

LibTactics_J: 使いやすい汎用タクティックのコレクション

• Coqのための追加の記法
  • N変数の存在限量
• Ltacによるプログラミングのための道具類
  • 等価継続
  • タクティックの型付けされない引数
  • タクティックのオプショナルな引数
  • タクティックのワイルドカード引数
  • ポジションマーカ
  • タクティックの引数のリスト
  • 補題のデータベース
  • その場での仮定の除去
  • 引数としての数値
  • タクティックをテストする
  • ゴールにやり残しがないことのチェック
  • 仮定のタグ付け
  • 仮定のタグ付け
  • 項を解体する
  • 出現場所でのアクションと出現場所以外でのアクション
  • eqの別名
• 後方/前方連鎖
  • 適用(Application)
  • 表明(Assertions)
  • 具体化と前方連鎖
  • 適用(application)の実験的タクティック
  • 仮定を追加する
  • トートロジーの適用
  • 等式を法とした適用
• 導入と一般化
  • 導入(Introduction)
  • 一般化(Generalization)
  • 名前付け(Naming)
• 書き換え
  • 書き換え(Rewriting)
  • 置き換え(Replace)
  • 名前変え(リネーム、Renaming)
  • 定義の展開(Unfolding)
  • 単純化(Simplification)
  • 評価(Evaluation)
  • 置換(Substitution)
  • proof irrelevance を扱うタクティック
  • 等式を証明する
• 反転(Inversion)
  • 基本反転(Basic inversion)
  • 置換(substitution)を伴う反転(inversion)
  • 置換を伴う注入(Injection)
  • 置換を伴う反転と注入 -- おおざっぱな実装
  • 場合分け
• 帰納法(Induction)
• 決定可能な等式
• 同値(Equivalence)
• N個の連言と選言
• タイプクラスのインスタンスを証明するためのタクティック
• 自動化起動のタクティック
  • jauto, 新しい自動化タクティック
  • 自動化タクティックの定義
  • コンパチビリティを構文解析するための定義
  • 軽い自動化の構文解析
  • 強力な自動化の構文解析
• 証明コンテキストを整理するためのタクティック
  • 仮定の隠蔽
  • 仮定のソーティング
  • 仮定のクリア
• 開発目的のタクティック
  • サブゴールのスキップ
• 標準ライブラリとのコンパチビリティ

PE_J: 部分評価

• 定数畳み込みを一般化する
  • 部分状態
  • 算術式
  • ブール式
• ループ以外のコマンドの部分評価
  • 代入
  • 条件分岐
  • 部分評価関係
  • 例
  • 部分評価の正しさ
• ループの部分評価
  • 例
  • 正しさ
• フローチャートプログラムの部分評価
  • 基本ブロック
  • フローチャートプログラム
  • 基本ブロックとフローチャートプログラムの部分評価

Postscript_J: あとがき

• ふりかえり...
• さらなる読み物