Skip to content

Instantly share code, notes, and snippets.

@qnighy

qnighy/hott-coq-oboegaki.md

Last active April 22, 2023 04:27
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save qnighy/bfb53e54d3ffcbbd0e84 to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save qnighy/bfb53e54d3ffcbbd0e84 to your computer and use it in GitHub Desktop.
Download ZIP
HoTT/Coq 覚書
Raw
hott-coq-oboegaki.md

はじめに

HoTT(ホモトピー型理論) はホモトピー論や∞圏論を型システムの上で展開しようという考え方である。この体系は既にCoqで形式化が進んでいる。これはその使い方の覚書である。

HoTTの参考資料

まず、HoTT/Coqではなく、HoTT全般に関係する資料について述べる。

  • HoTTの本家サイト http://homotopytypetheory.org/ に情報がたくさんある。この分野は数学の他分野に比べて、インターネット上に情報がより集約されているという特徴がある。
  • HoTTについて紙面で勉強するならば、上のサイトにあるHoTT Bookを読むのが最も適切である。
  • HoTTに関連するコードは主に https://github.com/HoTT/ に集約されている。
  • HoTTに限らず、圏論や∞圏論に関係する事柄は nLab http://ncatlab.org/ に充実している。辞典として用いるのに便利である。ただし、積極的にカテゴリカルな記述をするなど先鋭的であり慣れていないとわかりづらい場合があるので、書籍やWikipediaなどの他の資料と併用するとよいかもしれない。
  • HoTTについて書かれているブログの例 http://d.hatena.ne.jp/m-a-o/ http://d.hatena.ne.jp/m-hiyama/

HoTT/Coqの準備

HoTT/Coqは次の二つからなる。

  1. HoTT用にカスタマイズされたCoq
  2. 上のCoqで動作する証明ライブラリ

1のみのパッケージは https://github.com/HoTT/coq/ から入手できる。使い方は通常のCoqとほぼ同じである。特徴として、HIT(高階帰納型)を擬似的に実現するためのPrivate Inductive命令が使えることと、宇宙多相性に対応していることが挙げられる。

宇宙多相性は適当なオプションをつければ有効化できるので、「8.5が待てない、今すぐ宇宙多相性が使いたい」という人も使ってみる価値があるかもしれない。

2のパッケージ https://github.com/HoTT/HoTT/ には git submoduleの形で1のパッケージが同梱されている。したがってHoTTをCoqで始めたい人はこれを使えばよい。

インストール方法はREADMEを読め (Ubuntu等のLinuxに入れるのがオススメ)

HoTT/Coqのcoqdoc

HoTT/Coqのcoqdocは http://hott.github.io/HoTT/coqdoc-html/toc.html にある。

coqdocではなくproviolaを用いたものは http://hott.github.io/HoTT/proviola-html/toc.html にある。

これらのファイルの実体は https://github.com/HoTT/HoTT/tree/gh-pages にあり、これはHoTTが更新されるたびにTravis-CIで自動でビルド＆デプロイされている。

HoTT/Coqで証明を行うときのテンプレート

HoTT/Coqのライブラリを全てロードする

Require Import HoTT.

HoTT/Coqライブラリは非常に軽量であり、全てのライブラリをロードしても一瞬で終わる。

HoTT/Coqの一部のライブラリをロードする

Require Import Overture PathGroupoids Equivalences Trunc HProp HSet.
Require Import types.Unit types.Paths types.Sigma types.Forall types.Arrow.
Require Import types.Bool types.Universe Misc.
Require Import hit.Circle.
Local Open Scope path_scope.
Local Open Scope equiv_scope.

特に、HoTT/Coqのライブラリ内では Require Import HoTT. を実行してはいけないので注意すること。

圏論ライブラリを全てロードする

Require Import categories.

Set Universe Polymorphism.
Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.

HoTT/Coq本体とは異なり、圏論ライブラリの全てのライブラリをロードするのはそれなりの時間がかかる。

圏論ライブラリを全てロードし、UTF-8記法を有効化する

Require Import categories.
Require Import categories.Utf8.

Set Universe Polymorphism.
Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.

HoTTに限らず基本的な型

伝統的なCoqと異なり、命題と集合は区別せず、Propは使わない。

  • Unit … 0項直積 (tt 唯一の元)
  • Empty … 0項直和
  • A * B … 2項直積 (pair 唯一のコンストラクタ)
  • A + B … 2項直和 (inl, inr 左右のコンストラクタ)
  • forall x, P x … 依存直積 / 依存関数空間 (fun λ式)
  • A -> B … 非依存直積 / 関数空間 (fun λ式)
  • sig P または { x : _ & P x } … 依存直和 / ファイブレーション (exist 唯一のコンストラクタ / sig_rect 除去関数)
  • Bool … 2点集合 (true, false 左右のコンストラクタ / ifが使える)

HoTTの型

  • x = y … xからyへの道空間
  • x = y :> A … xやyが空間Aの点であることを明示
  • f == g … 関数fとgの間の各点道からなる空間 (Funext はこれがf = gと見なせるということを主張する)
  • A <~> B … 空間AとBの間のホモトピー同値からなる空間 (Univalence はこれがA = Bと見なせるということを主張する)
  • Contr A … Aは可縮空間である (Unitとホモトピー同値)
  • IsHProp A … Aは命題である (EmptyまたはUnitとホモトピー同値)
  • IsHSet A … Aは集合である (離散空間とホモトピー同値)
  • IsTrunc n A … Aはn-Truncatedである (nがminus_twoのときContr, nがminus_oneのときIsHProp, nが0のときIsHSet)
  • IsEquiv f … fはホモトピー同値写像

<~>, Contr, IsHProp, IsHSet, IsTrunc, IsEquiv は型クラスである。つまりインスタンスを用意しておけば勝手に補充してくれる。

また、HIT(高階帰納型)として定義される次の型についても把握しておこう。

  • minus1Trunc A … Aは非空である(という命題) / (-1)-truncationあるいはinhabitedとも呼ぶ。
  • quotient R … 関係Rによる商空間
  • Susp A … Aの懸垂 (ただし、Aが空のときはSusp Aは2点集合となるので注意)
  • S1 … 円周S1

HoTTのよく使う構成

  • 1 あるいはidpath x … xの恒等道 (=のコンストラクタ)
  • p @ q あるいは concat p q … 道pとqの合成
  • p ^ … 道pの逆道
  • ap f p … 道pを関数fで写す。f : A -> B, p : x = yのとき、ap f p : f x = f y。 fのpへの適用(application)または道への作用(action on path)
  • transport P p z あるいは p # z … 値zを道pに沿って輸送する。複素積分と同様に、輸送する道が異なると輸送した結果は異なる可能性がある。p:x=yのときにtransport P p : P x -> P y
  • apD01とか色々 … apの亜種(一般化)
  • transportD … transportの亜種(一般化)
  • s @@ t … 2次元道の水平合成
  • whiskerL p t … 2次元道を左からずらす
  • whiskerR s q … 2次元道を右からずらす
  • cancelL, cancelR … whiskerLとwhiskerRの逆
  • f ^-1 … fがホモトピー同値写像であることがわかっているとき、その逆写像

HoTTのよく使う定理

定理だと思って書いていたらゴールにこれらの名前が出てくるなんてこともよくあるから実際には一概に「定理」とは言えない。

  • concat_p_ppとかconcat_pp_p … 結合法則 (名前から性質を読み取れるようにせよ)
  • concat_1pとかconcat_p1 … 左および右から恒等道を合成しても変わらない
  • concat_pVとかconcat_Vp … 左および右から逆道を合成すると消える
  • inv_pp … 合成の逆は逆の合成
  • ap_1 … ap _ 1は1
  • ap_pp … 合成への作用は作用したものの合成
  • ap_const … 恒等関数を作用させると1になる
  • transport_const … transport (fun _ => Const) を見つけたら大体これによる書き換えが正解
  • transport_arrow … transport (fun x => A x -> B x) を見つけたら大体これ
  • transport_forall … transport (fun x => forall y:A x, B x y) を見つけたら大体これ
  • transport_hoge … transport (fun x => hoge) を見つけたら大体これ (適当)

たぶんOvertureとPathGroupoidsとtypes.Pathsの定義や定理は最終的には全部覚えないといけないんじゃないかという気がする。(もちろん最初から暗記する必要はない)

HoTTでよく使う証明

まずHoTTでは、Coqの通常の証明モードの使い方

Lemma FooBar : forall X, BarBaz.
Proof.
  yokini.
  hakaratte.
Qed.

の他に、定義をするための証明モードの使い方

Definition FooBar : forall X, BarBaz.
Proof.
  nanka.
  tsukuru.
Defined.

をよく使う。(QedではなくDefinedを使っていることがポイント。)また、ここでDefinitionをInstanceに変えたものもよく使う。

よく使うタクティック

  • refine … 値を直接与える。ただし、空欄補充に失敗したらそれを次のゴールにする。
  • refine (foobar @ _) … 等式の証明で左側を書き換えていくときに結構使う。
  • rewrite H … 通常のCoqのrewriteと全く同じ。HoTTの=でも使えるということ。
  • simpl … HoTTでも重要。simplを実行しても見た目が変わっていない場合でも、表示されていない項がこっそり変化して使いやすくなっていることがある。
  • hott_simpl … HoTT特有のめんどくさい書き換えのうち、自明なものをやってくれる。
  • change … 項の形のせいで進まないタクティックを力技で何とかする。
  • unfold … HoTTでも重要

よく使う戦略

  • transpose (fun _ => _) を見つけて、funの中身が特定の形をしていたら、それを分解するための定理を使って書き換えるとうまくいくことがある。
  • x = yの形をしているある道pについて、destruct pは成功したり失敗したりする(たいてい失敗する)。複雑な式が、このタクティック一本で単純化されることもある。しかし、適切な場所で適切なものをdestructするには慣れが必要。
  • Definition thm ... Definedで作ったものの中身がゴールに出てくると、thmが巨大だと悲惨。定義したものは細かく分ける必要が出てくることがある。
  • 透明な定義にするか、不透明な証明にするかの判断は重要。その型がIsHPropだったら不透明な証明にしてもだいたい問題ない。そうでなかったら、透明である必要があることが多い。

HoTTの公理

HoTTは将来的に全てのコードが実行可能となることが期待されているが、現在は実行できないものがいくつかある。それは

  • 関数外延性 (Funext)
  • 単葉性 (Univalence)
  • 高階帰納型 (HIT)

また、HoTT/Coqのライブラリには無いようだが、例えば次のような公理を導入することができる。

  • 命題に対する排中律、命題に対する二重否定除去則
  • 集合でインデックスされた集合族に対する選択公理
  • 集合でインデックスされた型の族に対する選択公理

高階帰納型 (HIT)

Higher Inductive Typeは例えば次のように定義できることが期待されている。

Inductive S1 : Type :=
  | base : S1
  | loop : base = base.

Definition S1_rect(P : S1 -> Type) (b : P base) (l : loop # b = b) (x : S1) : P x :=
  match x return P x with
  | base => b
  | loop => l
  end.

そして、S1_rect P b l baseはbaseに、apD (S1_rect P b l) loopはlに簡約されることが期待されている。

現在はこれをPrivate Inductiveという仕組みとAxiomを使って擬似的に実現している。 (Circle.v参照)

このとき、S1_rect P b l baseはbaseに簡約されるが、apD (S1_rect P b l) loopはlに簡約されない。代わりにこの2つが等しいことを示す公理がある。

単葉性と関数外延性

UnivalenceとFunextは、どこで仮定しているかがわかるように型クラスの形で持ち回している。

これらの公理を使うには、例えば

Definition foo `{Univalence} (P:Type) ... := ... .

とか、

Section AssumeUnivalence.
Context `{Univalence}.

...

End AssumeUnivalence.

とか書く。

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment