# Mathcomp Book 読書会メモ
これは隔週でやってるcoqtokyo勉強会が作成しているメモです。subsectionごとに3行まとめをメモしたいです。
https://math-comp.github.io/
日本語訳
https://drive.google.com/drive/folders/12dZMyTx0Ky4tTrCwn0lLkWGY2atL-8Ol
### 自己紹介 (2023.02.17)
https://hackmd.io/KqGQD2tIQ_qi8zuT1i95lw
### はじめに
#### 本の構成
- 第1部: 形式言語を記述するための言語
- Gallina: Coqで数学を表現するために使用されている。Calculus of Inductive Constructionsという型理論の一種が元になっている
- SSReflect (Small Scale Reflection): boolean reflectionとも呼ばれる形式化手法の名前で、四色定理の証明のために考案された。MathCompライブラリの柱であり、奇数定理の形式的証明の柱となった
- 第2部: フォーマルなライブラリを作る
- 型推論による自動化。canonical structureを与える宣言的なプログラムで拡張を行う
##### 奇数定理とは?
[Feit-Thompsonの定理](https://en.wikipedia.org/wiki/Feit%E2%80%93Thompson_theorem)とも呼ばれる。
ガロア理論と関連。「すべての奇数位数の有限群は[可解群](https://ja.wikipedia.org/wiki/%E5%8F%AF%E8%A7%A3%E7%BE%A4)である」
affeldtさんの初学者向けssreflect [カラテCoq](https://www.math.nagoya-u.ac.jp/~garrigue/lecture/2022_affeldt/karate-coq-nagoya2022.pdf)
### Coqの動作環境
- `coqide`
- Emacs + Proof General
- VSCode + `vscoq` 拡張
- ブラウザ(jsCoqや[coqban](https://proof-ninja.github.io/coqban/)): [こちら](https://math-comp.github.io/mcb/snippets/)から本書のコードをjsCoqにより動かせる
## 1. 関数と計算
### 1.1. 関数 (2023.02.21)
印象に残ったこと
- カリー化
- 高階関数の説明
- 結合の仕方
```coq=
Definition f (n : nat) : nat := n + 1.
(* Definition f := fun n => n + 1. *)
About f. (* fの型を説明 *)
Print f. (* 型とbodyを表示 *)
Check f 3. (* 型チェック *)
Compute f 3. (* 評価結果の値を表示?(もっと奥深そう) *)
Definition g (n m : nat) : nat := n + m * 2. (* 複数の引数を持つ関数 *)
Check g 3. (* 複数の引数を持つ関数はカリー化される。部分適用もできる *)
(* 高階関数。関数を引数に取る関数の例 *)
Definition repeat_twice (g : nat -> nat) : nat -> nat :=
fun x => g (g x).
```
### 1.2 Data型と最初の例 (2023.03.14)
* 帰納的定義による簡単なデータ型の定義の方法
* bool型,nat型の紹介
* Fixpointを使った簡単な再帰的定義の紹介
### 1.3 コンテナ (2023.04.11)
* list, pair, option型
* Record型の使い方
* Ninjaパターンマッチ
### 1.4 `Section` と `Variables`と`Implicit Type`
* `Section`の中で宣言した`Variables`は`Section`の外側からは単なる引数になって見えるぞ
* (より凝った抽象化を設計したいときは型クラスとかモジュールとかを使え)
* `Implicit Type`で型注釈を省略できる
### 1.5 式のシンボリック評価
* 変数が含まれる式の計算には `Compute` コマンドよりも `Eval simpl` がいいぞ！
### 1.6 イテレータと数学的表記法 (2023.04.25)
* `foldr`と`iota`を用いた有限和等の定義方法
* Texの記法にインスパイアされた`Notation`がある: `\sum_ ( m <= i < n ) F`
* `foldr`だと証明しやすかったり、`bigop`に一般化しやすい
### 1.7 表記・略記 (Notations, abbreviations)
* `Notations`コマンドはCoqの式を読みやすくするために使う。優先順位と結合方向を指定できる。
* 主なNotationの表は以下にあります。
https://coq.inria.fr/refman/language/coq-library.html
* `(only parsing)` を指定すると、入力だけに使用され、Goalなどを表示するときには使われません。
* MathCompでは、Notationのシンボルにネーミングルールがあり、ここで紹介されています。
## 2. 形式証明の最初の一歩 (2023.05.16)
### 2.1. 正式なステートメント(Formal statements)
* Lemma のステートメントの初出
* Lemma の後には Prop 型の式しか書けないが、 MathComp では bool 型を暗黙的に(= true をつけて) Prop 型にしてくれる
* Prop と bool を混同しないように注意が必要
* About や Check など Coq の大文字から始まるコマンドのことを vernacular(現地語) コマンドと呼ぶ
### 2.2. 形式的な証明 p.45 (2023.05.30-06.13)
2.2.1 Proofs by computation
2.2.2 Case analysis
2.2.3 Rewriting
* 形式的な証明は、計算による証明(by [])、場合分けによる証明(case)、書き換えによる証明(rewrite)がある。
* 計算による証明は、関数の定義に基づいて簡約をおこない、=の左辺と右辺が一致したら、証明終わりとする。
* 場合分けによる証明は、caseタクティクをつかって、boolをtrueとfalseに分ける、natを0と非ゼロ(_.+1)に分けることで証明を進める。
* 書き換えによる証明は、rewriteたくティクを使って、補題の左辺から右辺への書き換えをおこなう。
* 命名規則については、2.5節で説明する。
### 2.3 量化子 (p.53, 2023.06.27-07.11)
* 2.3.1 forallが冠頭(prenex)にあるときと無いときの例
* 2.3.2 Section を使うと Variables, Hypothesis で宣言したものがSectionの外で量化される
* 2.3.3 forallがあるlemmaがapplyされる時にパラメータを推測してくれる
* 2.3.4 elimを使った帰納法による証明
### 2.4 rewriteは十徳ナイフ〜 p.62 (2023.07.11-07.18)
rewriteの色んな使い方について
* 書き換え回数の指定。 ?で0回以上 !で1回以上
* パターンを指定してrewriteする。[in RHS]
* /でunfold(定義の展開)。 -/ でfold
* change tacticのような使い方 -[n1]/(0 + n1)
* 0 + x を x にするのがsimplify。change tacticはその逆
* 前提の削除 rewrite -{}IHn
### 2.5 図書館を検索する
注意: 現在のSearchコマンドはSSReflect提供のものではなく、Coq自体に備わっているものが使われる。微妙に仕様が違う
https://coq.inria.fr/refman/proof-engine/vernacular-commands.html#coq:cmd.Search
* 2.5.1 パターンから検索する
* 訂正: 現在の `Search concl:(odd _).` に相当する
* 2.5.2 名前から検索する
* MathCompの補題には、命名規則があり、それを知っていると検索がしやすい
* 接尾辞などのまとめが、2.5.2にあるため、必要に応じて参照すること
## 3. 依存型理論
### 3.1 Propositions as types, proofs as programs
- Typing judgementの初出
- Curry-howardの初出
### 3.2 Terms, types, sorts
- `Set` とか `Prop` などの上位の型を sort と呼ぶ
- `Type : Type` となるが内部にindexを持っていて実は同じものではない
- 値に依存する型を「依存型」と呼ぶ
### 3.3 ならばとforall
- 「AならばB」の証明は「fun x:A => ...」の形になる
- 「forall x:A, B」の証明も「fun x:A => ...」の形
- `apply` タクティックはゴールの形を見て賢くパラメータを推論するぜ
### 3.4 Conversion
* 型のβリダクション
* Coqでは型式の中に1+2とか出てきうるが、型チェックのときに計算して等しいものは同一視される
* 変数が混ざっている式でもシンボリックに計算される
### 3.5 Inductive型 (2023.10.03)
* コンストラクタは単射(injective)だよ
* 前提の等式からinjectiveを使うためには `case: ` タクティックでやる
* `Fixpoint` コマンドはInductiveコマンドでできた値のmatch式で取り出したサブタームにだけ再帰呼び出しできるfixのいちばん簡単な形
### 3.6 論理演算子もInductiveだぜ (2023.10.17)
* 連言 and (/\) の定義、conj、proj1、proj2
* 存在量化 ex (exists) の定義、ex_intro
* True,Falseだけじゃなくとかeqとかも言語組み込みじゃなくInductiveコマンドでライブラリ提供されているぜ
* (x=yが成り立つときにrewriteで書き換えられるのは内部では単にeq_ind(eq_ind_r)をapplyしているだけ、そのときの述語Pを裏で構成している)
### 3.7 帰納的推論
<blockquote class="twitter-tweet"><p lang="ja" dir="ltr">超元気農法! でてきました！ <a href="https://twitter.com/hashtag/coqtokyo?src=hash&ref_src=twsrc%5Etfw">#coqtokyo</a> <a href="https://twitter.com/hashtag/coq?src=hash&ref_src=twsrc%5Etfw">#coq</a> <a href="https://t.co/oEqNbzxAr6">pic.twitter.com/oEqNbzxAr6</a></p>— Yoshihiro Imai (@yoshihiro503) <a href="https://twitter.com/yoshihiro503/status/1714238050048651731?ref_src=twsrc%5Etfw">October 17, 2023</a></blockquote> <script async src="https://platform.twitter.com/widgets.js" charset="utf-8"></script>
* nat_ind を手で書いてみる。
* strong_nat_ind を証明する。elim/strong_nat_ind で使う。
* MathComp ではイデオムを通して使う。
* 最近では ubnP を使う （karate-coq p.44)。
## 4 形式証明のための証明言語
ここから本格的に証明を書いていく予感...
### 4.1 スタックとしてのゴール操作
```coq=
========
forall x: nat, P x -> Q x
```
というゴールは
|x: nat|
|----|
|P x|
|Q x|
みたいなスタックになっていると考える。
* スタック操作やcase分析はbookkeepingだから冗長に書きたくないから接尾辞とかで
* `=>` がpull, `:` がpush
* `=>` の変数名で `[...]` 使うことで分解しながらpullできる、明らかなパターンのときはブラケット内に `//` 書いて `=> [//|z]`みたいに書ける
* `intro _.` はssreflectだと `move=> {foo}.`
* `clear foo.` は `move: {foo}.`
* `case E: ...`とかくと `case_eq` できる
### 4.2 証明の構造化
読みやすい証明の書き方のススメ
* ``have m1_gt1: 1 < m`! + 1.`` みたいにすると途中でも好きなこと証明できる
* 自然言語で考えたときの変数名の付け方や順番を意識するとよいぞ
* 「一般性を失わず〇〇」みたいなやつは `have` とか `wlog` タクティックを使いましょう
### 4.3 証明のメンテナンス
保守しやすい証明の書き方のあれこれ
* 紙の証明の粒度と順番で書くとよい
* `?lem` の書き方は注意だぞ
* 前提の名前のシャドウイング
* 細かく分けれない大きな証明は `have` とかを使うぞ
## 5. 帰納的仕様
(mathcompとかでは Inductive Propを自作することはあまりない. この章はおそらくreflectionとかviewの話がメインだろう)
### 5.1 Reflection views
reflection viewの話
* bool式とPropの同値性を関連付ける補題のことを「reflection view」と呼ぶぜ、それは `P` で終わる名前だぜ (`andP` とか)
* reflection viewは `move/ ` で使いがちだぞ
* `elimT` によるコアーションによりbool版からProp版へのならばと同一視できるぞ
(ssreflect で => の右に [....] みたいなの書いた場合2パターンの意味があるぞという話: https://twitter.com/yoshihiro503/status/1749741071557603527)
### 5.2 Advaced, practical statements
* 単純なreflect型以外の xxxP の補題もあるぞ
* ifPとかleqPとかboolPとか
* こういうやつを `spec` と呼ぶぞ
### 5.3 natのStrong inductionをmathcompでやる方法
* `move: {-2}m (leqnn m).` する方法
* `case: (ubnPgeq m)` する方法（↑よりいいぞ）
* (最新のssreflectだと `ltn_ind` を使えるからこれが一番良さそう)
### 5.4 ユークリットの割り算の事例
* これまでのいろいろなタクティックとかを使ってユークリッドの除法を形式化するぞ
* akiraさんによる一部説明の提案: :thumbsup: https://github.com/math-comp/mcb/issues/148
### 5.5 使用の表記
* Coercionによってbool式はPropになるぞ
### 6.1, 6.2 型推論と高階単一化と例
* `(f _)` のように `_` で与えられる省略された引数の推論の話
* `{}` で囲ったら暗黙的な引数になるぞ
* `Argument` コマンドによって自動的に暗黙的な引数にしてくれるぞ
### 6.3 関係としてのRecord
* Record型を使って型クラス的なことができるよ
* Eqクラスの例の紹介
* ペアのeqみたいなパラメタライズしたやつも推論できるぜ
### 6.4 ファーストクラスインターフェイスとしてのRecord
* 6.3のEqクラスにaxiomフィールドを入れて満たすべき公理を入れたぞ
* ModuleにくるんでStructureとRecordを組み合わせにしたぜ(継承のため?)
* コアーションでnat_eqTypeとnat型を同一視するぜ
### 6.5 より一般的なeqTypeの話
* ペアみたいに型パラメータ持つやつのeqTypeもいけるぞ
* `A`,`B`それぞれの型がeqTypeなら `(A, B)` もeqTypeにさせるぞ
### 6.6 EqTypeとリスト
* EqTypeのTを要素持つリストの話
* リストのmem判定や重複削除がboolでできるぞ
* さらにリスト自体もEqTypeになるぞ
### 6.7 bigop
* 数列の $\sum$ とかはbigopというより一般的なカタチで用意されるがこれは実態はfoldrなんだぜ
* いろいろな補題の一部は 演算子が Monoid であることだけ要求するんだ
* オレオレモノイドを使いたいときは `Canonical addn_monoid := Monoid.Law addnA add0n addn0.` のようにしてね
* Searchするときは `\sum_` だと見つからないから `"big" "eq"` とかでSearchせよ
### 6.8 bigopのためのnotation
* bigopはNotationをうまくやる都合でBigBodyみたいなやつを返す感じになってるから注意しようぜ
実験
```NotationFun.v
(* 表示するときに一意にならなそうな記法 *)
Definition ff (g1 g2 : nat -> nat) := 0.
Notation "\FF i [ A ] [ B ]" := (ff (fun i => A) (fun i => B)) (at level 99).
Check \FF i [ i ] [ i + 1 ].
Check ff (fun i => i) (fun i => i + 1).
Check ff (fun x => x+1) (fun k => k+2).
Check ff (fun _ => 1) (fun k => k+2).
Check ff (fun _ => 1) (fun _ => 2).
```
### 6.9
* (Coqで「overload」というと `eq_op` をいろんなデータで使えるやつのことをいうようだ)
* `simpl` は unfoldやらないので注意してね
* `bigop` 関連の証明だと `simpl` しないとごちゃごちゃになりすぎるときあるぜ
### 6.10 アドホック多相
自動翻訳: https://hackmd.io/efPSsS8cRuujMIn2UVvh0g
* Coqの幽霊型(Phantom Types) はこんな感じだぜ
## 7 サブタイピング！
### 7.1 リストに長さをつけた $n$`-tuple` を考える
<blockquote class="twitter-tweet"><p lang="ja" dir="ltr">mathcomp では tupleは長さ付きリストみたいなやつなので、よくプログラミング言語で使われているタプル型とは違うものなので注意ぞ！<a href="https://twitter.com/hashtag/Coq?src=hash&ref_src=twsrc%5Etfw">#Coq</a> <a href="https://twitter.com/hashtag/ssreflect?src=hash&ref_src=twsrc%5Etfw">#ssreflect</a> <a href="https://twitter.com/hashtag/mathcomp?src=hash&ref_src=twsrc%5Etfw">#mathcomp</a> <a href="https://twitter.com/hashtag/tuple?src=hash&ref_src=twsrc%5Etfw">#tuple</a> <a href="https://twitter.com/hashtag/vector?src=hash&ref_src=twsrc%5Etfw">#vector</a></p>— Yoshihiro Imai (@yoshihiro503) <a href="https://twitter.com/yoshihiro503/status/1815694591393255548?ref_src=twsrc%5Etfw">July 23, 2024</a></blockquote> <script async src="https://platform.twitter.com/widgets.js" charset="utf-8"></script>
* 長さ付きの `seq` 型、 `n.-tuple` 型というのがあるぞ
* seq操作のrev, map, consなどが tupleでも便利にできたいのでオペレータごとにCaonoical Structureが定まっているぞ (tupleをseqとして操作して最後にtupleに戻す)
* これはサブタイピングというよりも型推論をがんばっているということなんじゃないか?(型チェッカは普通のことしかやっていない)
## 7.2 型変換で便利で統一的な sub-type kit
* オレオレ型で `Structure ore := Ore { tval :> T; _ : 制約}` みたいに作っておくと, `ore` 型と `T` 型の変換をうまくやる方法がある
* `Canonical ore_subType := [subType for tval]` みたいにやっとくといい感じに subtype kitが使える
* `val` で `Ore -> T` への変換、 `Sub` で `T -> 制約 -> Ore` の変換がいろんなSubTypeで使えるぜ
## 7.3 有限型とその定理
* 有限型とは、その型の要素を一個ずつ並べた seq表現が存在すること
* sum_とかの bigopは有限集合使えるようになってるぜ
## 7.4 ordinalのsubtype
* `'I_` $n$ みたいな書き方で ordinal型(順序数型)が表現される
* Subtyp kitによって natのsubTypeになる
* $n$ `.-tuple` の nth を安全に定義できる
## 7.5 Finite function 有限関数 (ffum)
* `{ffun A -> B}` で定義できる有限関数
* 有限関数は定義域(domain) `A` が `finType` の場合の関数で、実態は`B`の要素の n.-tupleだぜ
* 値域(codomain) `B` も finTypeのときは関数全体も finTypeになるんぜ
### Coq豆知識
```coq
Definition f (x : T) := ...
```
を省略して
```coq
Definition f of T := ...
```
と書けるぞ
`Eval hnf` の `hnf` は head normal form 略だよ
### 7.6 有限集合
台集合 `T` を固定して、そのいろんな部分集合を考えたいときがある。
そのいろんな部分集合同士の要素を気軽に比較したかったりする。
そういうときは、finTypeそのままじゃなくて有限集合型 `A : {set T}` がある。
* `{set T}` と書くとTの部分集合全体の型
* `T` はfinTypeじゃないとだめという制約あり
* `D:{set T}`を使って `powerset D` と書くと `D` の部分集合全体が得られるぞ
* `{set T}`の元は型にはならないからそういう用途には使えない
### 7.7 Permutations
(`opam install coq-mathcomp-fingroup` が必要だぜ)
* finType `T` の要素の順番だけ入れ替えた `{perm T}` という型があるぜ
### 7.8 行列
* `'M[R]_(m, n)` というシンタックスで要素が型`K`の `m` x `n` 行列の型
* `'M[R]_ n` のように書くと `n` x `n` の正方行列を表す
* 行列型の具体的な値は `\matrix_ (i, j) (iとjを使った式)` のように書くと得られるがこれは実際に有限関数ffunから行列への変換が起きている
* 一般の行列の掛け算はringじゃないので特別な中置記法 `*m` が用意されている
* 証明の中で行列を関数のように評価したかったら`mxE` が便利かも
ここで証明Tips
* `have` タクティックの代わりに `gen have`とするとforallをなるだけつけた
#### 7.8.3 行列みたいなリッチな型のときの苦しみ
* 行列の掛け算 `A *m B` は Aの列数とBの行数が一致しないと型エラーだが、それがCoqから明らかにわからない場合はすんなり通らない苦しみがある
* 行列同士の比較 `=` もそう
* そういう場合は `let cast := (erefl m, 証明項) in` を作って(苦しい)、`castmx` 使って変換を入れ込むことをして型を合わせる
## 8. Organizing Theories
(この章はもしかしたら古い情報かも)
数学の構造で、体、環とかでいれことなる構造が出てくるけど、そういう話をする
### 8.1 構造のインターフェイス
* ssralg では整数$\mathbb{Z}$から体までの代数構造を定めている
* 基本的にはStructureとCanonicalでHaskellの型クラス的な風に実装している
* 剰余環 $\mathbb{Z}/p$ を作って `RingType`とか `ComRingType` にする例を説明する
* Mixinには名前をつけた方がパフォーマンスのために良いぞ
### 8.2 テレスコープ(望遠鏡)
テレスコープは簡単で便利だけど型チェックがめちゃめちゃ非効率になりがち→packed classという解決があるぞ
Packed Classのお作法
* `mixin_of` は追加するオペレーターや公理
* `class_of`
* こういう階層構造をつくる方法はPacked Class以外に、テレスコープっていうやりかたがあるぞ
* 参考: https://inria.hal.science/inria-00368403v1/document
* mathcomp 1時点での古いやり方かも？
* `eqtype` `chocie` `fintype` `ssarg` などでは使っていないが `Monoid.law` とかで使っている
### 8.3 Packed class
* ssrargのRingTypeは数え上げ可能を意味する choiceTypeを仮定していてヤバそう(？)
* Packed classを使って ComRingとかUnitRingとか定義するぜ
(math-comp 2以上だと Hierarchy Builder使うからちょっと違う感じかも)
### 8.4 Parameters and constructors
`pair_ringType int_ringType rat_ringType` みたいなのを明示的に書かないといけなくなったときこれはめんどいですよね。
Phantom Typeを使ってうまいこと型推論を納得させる方法があるんです。
(math-comp 2以上だと使われない方法かも)
### 8.5 自分の定義した型をfinTypeとかにする方法
```
Inductive windrose := N | S | E | W.
```
みたいな4値の型を `finType` にする簡単な方法
* 全単射をつくればよいっていう方法がある
* `windrose -> 'I_4` と `'I_4 -> option windrose` 関数を定義して `pcancel` を示す
* `pcancel` があれば、そこから eqTypeとか choiceTypeとか finTypeにできるぜ
* さらに `predArgType` 型としてInductiveしておくと `#| _ |` とかもできるようになるぜ
Sign in with Wallet
Connect another wallet