はじめに

Agda あるいは一般に定理照明器を触るにあたって基本的な数学を"実装"してみようというのはおそらく自然な欲求だと思う、みょんさんみたいに米田の補題とかためしてみるのとかクールだと思う。
圏論をためしてみるの良いよと河野先生もおっしゃってくれてるのでいずれ挑戦しようと思ってます。

てなわけで、Agda Tutorialを上から写経していこうと思い立ったのでまずは第一弾、集合。

Modules.Basic

Agda のモジュールはmodule header が必要、とのこと。
（単なるAgda ファイルならどうなんだろう？）
Emacs にロードさせて（解釈させて）シンタックスハイライトさせるためにはC-c C-lと打ちましょう。

Sets.Enumerated

列挙ですね、外延的なのかな？

The Bool set

Haskell に似て非なるBoolean

data Bool : Set where
  true : Bool
  false : Bool

これは¹

Bool は Set の"要素”
true とfalse は Bool の"要素"

なお後述（される予定）のようにRussel のパラドクス回避のために

Setᵢ : Setᵢ₊₁

のように再帰的に型が定義されます。

Special finite sets

Boolean の他に大事な有限集合として、空集合と一点集合（シングルトン）があります：

data ⊥ : Set where

data ⊤ : Set where
  tt : ⊤

空集合はその名前から明らかなようにコンストラクターが不在です。

Types vs. sets

型と集合の違い

-ある要素に対して、型はユニークに決まるがその要素が属する集合は一つとは限らない
-型は要素を集めたものではない、それはどちらかと言うと集合

Sets.Recursive

再帰というとリストとか二分木とかですね。

Import List

module Sets.Recursive where

open import Sets.Enumerated using (Bool; true; false)

open import はその作用としてはBool 型の定義をこの場所に展開するのと等しいらしい。

Definition of ℕ

いわゆるペアノ数と呼ばれる再帰的な自然数の定義

data ℕ : Set where
  zero :     ℕ
  suc  : ℕ → ℕ

これによって十進法で言うところの0 をzero で、1 をsuc zero で、2 をsuc (suc zero)で、というふうに表していけることになる。

Type-checking of expressions

Emacs 上でC-c C-d (deduce) と打つとAgda による型チェックを行うことが出来る。
例えば、C-c C-d と打ってからsuc (suc zero) と打つとこれはℕ だよと教えてくれるわけだ。

Binary representation of ℕ

ペアノ数はいわば一進法に相当するわけで、二進法のもある、もちろん同型であるわけだが証明が必要。

data ℕ⁺ : Set where
  one      :      ℕ⁺
  double   : ℕ⁺ → ℕ⁺
  double+1 : ℕ⁺ → ℕ⁺

data ℕ₂ : Set where
  zero :      ℕ₂
  id   : ℕ⁺ → ℕ₂

Binary trees

二分木の構造だけ、データは入っていない。

data BinTree : Set where
  leaf : BinTree
  node : BinTree → BinTree → BinTree

Constants

Import List

module Constants where

open import Sets.Enumerated using (Bool; true; false)
open import Sets.Recursive using (ℕ; zero; suc)

Constant definitions

ちょっとだけプログラミングらしくなるところ。

nine : ℕ
nine = suc (suc (suc (suc (suc (suc (suc (suc (suc zero))))))))

ten : ℕ
ten = suc nine

Haskell のそれとは異なり型宣言は必須、とのこと。
一回用意したものを再利用（ten の中で使われてるnine）可能。

Normal form

C-c C-n (normal)と押してten と叩くとそれはsuc (suc (suc (suc (suc (suc (suc (suc (suc (suc zero))))))))) と教えてくれる、これをnormal form と呼ぶ、日本語だと正規形だろうか？それとも標準形？

Syntax.Decimal_Naturals

、、、要はペアノ数と普段使ってる十進法の間に組み込みの対応を用意してますよーとのこと。

Syntax.Infix

module Syntax.Infix where

open import Sets.Enumerated using (Bool; true; false)

Infix notation

_をプレースホルダーとして使うのがややややこしいかもしれない。
なお適応順はおそらく左端から。

data BinTree' : Set where
  x : BinTree'
  _+_ : BinTree' → BinTree' → BinTree'

この定義からは以下のような二分木型が作れます。

BinTree' : Set
x : BinTree'
x + x : BinTree'
(x + x) + x : BinTree'
x + (x + x) : BinTree'
(x + x) + (x + x) : BinTree'

右結合か左結合かを明示的に宣言できます、数値は作用素としての強さですね

infixr 3 _+_

こう宣言することで

x + x + x   : BinTree'
x + (x + x) : BinTree'

の２つは同じになります、すなわち右結合。

Sets.Mutual

module Sets.Mutual where

open import Sets.Enumerated using (Bool; true; false)
open import Syntax.Decimal_Naturals using (ℕ; zero; suc)

Mutual definitions

mutual definitions のためには先にdata で（型）宣言をする必要があります：

data L : Set
data M : Set

data L where
  nil : L
  _∷_ : ℕ → M → L

data M where
  _∷_ : Bool → L → M

Sets.Parametric

module Sets.Parametric where
open import Data.Nat

Definition of List

さてリストの定義、糖衣構文を剥がしたHaskell のそれとそっくりですね。

data List (A : Set) : Set where
  []  : List A
  _∷_ : A → List A → List A

infixr 5 _∷_

A : Set の仮定の下、List A : Set となり、このときA をリストのパラメタと呼びます。
従ってList Bool 型の要素は例えば

[]  
true  ∷ []  
false ∷ []
true  ∷ true  ∷ []  
false ∷ true  ∷ []  
true  ∷ false ∷ []  
false ∷ false ∷ []  
...

となります。

×: Cartesian Product

デカルト積です。

data _×_ (A B : Set) : Set where
  _,_ : A → B → A × B

infixr 4 _,_
infixr 2 _×_

型とそのインスタンスは少々ややこしいですが、例えば Bool × Bool 型は全部列挙できて

true , true 
true , false
false , true
false , false

というわけです。

⊎: Disjoint Union (Sum)

今度は直和です。

data _⊎_ (A B : Set) : Set where
  inj₁ : A → A ⊎ B
  inj₂ : B → A ⊎ B

infixr 1 _⊎_

Sets.Indexed

module Sets.Indexed where

open import Data.Empty    using (⊥)
open import Data.Unit     using (⊤; tt)
open import Data.Sum      using (_⊎_; inj₁; inj₂)
open import Data.Bool     using (Bool; true; false)
open import Data.Nat      using (ℕ; zero; suc)

Fin, family of finite sets

ℕ でインデックスされた集合族を考えます、つまりFin n は要素がn 個の集合です。
このとき、明らかに数が等しいので

Fin 0 ~ ⊥
Fin 1 ~ ⊤ ~ Maybe ⊥ ~ ⊤ ⊎ ⊥
Fin 2 ~ Bool ~ Maybe ⊤ ~ Maybe (Maybe ⊥) ~ ⊤ ⊎ ⊤ ⊎ ⊥
Fin 3 ~ Maybe Bool ~ Maybe (Maybe (Maybe ⊥)) ~ ⊤ ⊎ ⊤ ⊎ ⊤ ⊎ ⊥
Fin 4 ~ Maybe (Maybe (Maybe (Maybe ⊥))) ~ ⊤ ⊎ ⊤ ⊎ ⊤ ⊎ ⊤ ⊎ ⊥

などの同型関係があります。

Definition of Fin

data Fin : ℕ → Set where
  zero : (n : ℕ) → Fin (suc n)
  suc  : (n : ℕ) → Fin n → Fin (suc n)

Vec A n ~ Aⁿ

data Vec (A : Set) : ℕ → Set where
  []  : Vec A zero
  cons : (n : ℕ) → A → Vec A n → Vec A (suc n)

Term_Inference

Import.agda

module Term_Inference where

open import Data.Empty    using (⊥)
open import Data.Unit     using (⊤; tt)
open import Data.Sum      using (_⊎_; inj₁; inj₂)
open import Data.Nat      using (ℕ; zero; suc)

Term inference

アンダースコア(_) が置かれた項をAgda のコンパイラは推論してくれます。
例えばn はsuc の引数なのでℕ 型だというわけです。

data Fin′ : ℕ → Set where
  zero : (n : _) → Fin′ (suc n)            -- ℕ is inferred
  suc  : (n : _) → Fin′ n → Fin′ (suc n)   -- ℕ is inferred

x : Fin′ 3
x = suc _ (zero _)                         -- 2 and 1 are inferred

Implicit arguments

アンダースコアは隠すこともできます、とのこと。
引数を"暗示的に”扱う際は{}を使いなさい、とのこと。

data Fin : ℕ → Set where
  zero : {n : _} → Fin (suc n)
  suc  : {n : _} → Fin n → Fin (suc n)

このとき

x′ : Fin 3
x′ = suc {_} (zero {_}) 
{_} can be deleted:

とかけるそうですが、さらに{_} も消去できて

x″ : Fin 3
x″ = suc zero

となりますが、これが普通の書き方な気がするなぁ、、、
と思いましたが、この定義だとzero やsuc なども暗示的に要素数n を持っているのでいちいち書かなくても型宣言の時一回のみで良いというのが利点ですね。

Syntactic abbreviations

明示的に書く場合は以下のように書けます。

data Fin′ : ℕ → Set where
  zero : (n : _) → Fin′ (suc n)
  suc  : (n : _) → Fin′ n → Fin′ (suc n)

data Fin′ : ℕ → Set where
  zero : ∀ n → Fin′ (suc n)
  suc  : ∀ n → Fin′ n → Fin′ (suc n)

同様に

data Fin : ℕ → Set where
  zero : {n : _} → Fin (suc n)
  suc  : {n : _} → Fin n → Fin (suc n)

data Fin : ℕ → Set where
  zero : ∀ {n} → Fin (suc n)
  suc  : ∀ {n} → Fin n → Fin (suc n)

Sets.Propositions

module Sets.Propositions where

open import Data.Nat using (ℕ; zero; suc)

Proofs as data

Agda のキモである証明について。

真である命題の証明

いわゆる終対象である一点集合をもって真なる命題の証明を表します、すなわち

data ⊤ : Set where
  tt : ⊤

なるほど、だからttなのか。

偽である命題の証明

こんどは始対象に相当する空集合ですね、すなわち偽なる命題は証明を持たないので

data ⊥ : Set where

論理積あるいはAND

A, B を命題としてそれらの論理積を型A × B で表す。

data _×_ (A B : Set) : Set where
  _,_ : A → B → A × B

infixr 4 _,_
infixr 2 _×_

a を命題A の証明だとする、同様にb をB の証明だとする。
このとき型A × B はa , b なる証明を持つことになる、というわけです。

論理和あるいはOR

論理積の双対ですね。

data _⊎_ (A B : Set) : Set where
  inj₁ : A → A ⊎ B
  inj₂ : B → A ⊎ B

infixr 1 _⊎_

すなわちA ⊎ B はinj₁ a あるいはinj₂ b という証明がありますよ、ということです。

≤: Less-or-equal predicate

n ≤ m (n, m = 0, 1, ...)なる命題の証明を考えます。
以下のようにm, n でインデックスされた集合を定義します。

data  _≤_ : ℕ → ℕ → Set where
  z≤n : {n : ℕ} →                       zero  ≤ n
  s≤s : {m : ℕ} → {n : ℕ} →   m ≤ n  →  suc m ≤ suc n

infix 4 _≤_

この定義によって以下の様な命題とその証明が生成されることになります。

z≤n {0} : 0 ≤ 0
z≤n {1} : 0 ≤ 1
z≤n {2} : 0 ≤ 2
...
s≤s (z≤n {0}) : 1 ≤ 1
s≤s (z≤n {1}) : 1 ≤ 2
s≤s (z≤n {2}) : 1 ≤ 3
...
s≤s (s≤s (z≤n {0})) : 2 ≤ 2
s≤s (s≤s (z≤n {1})) : 2 ≤ 3
s≤s (s≤s (z≤n {2})) : 2 ≤ 4
...

型を整理すると

0 ≤ 0
0 ≤ 1,  1 ≤ 1
0 ≤ 2,  1 ≤ 2,  2 ≤ 2
0 ≤ 3,  1 ≤ 3,  2 ≤ 3,  3 ≤ 3
...

となり、これらの命題（型）を持つ命題はその証明を得たことになります。

1 ≤ 0

上記に載ってない1 ≤ 0 なども空集合があるという意味では正しい命題です、もちろん偽なので証明はありません。
これはAgda においては1 ≤ 0 なる型の要素はありません、と表現されます。

Proving emptiness

要は再帰を遡っていって直接空であることを示せるところまで降りたら良い、ということみたいですね。
すなわち、例えば型7 ≤ 3 を考えてみます。

これが空で無ければ、あるx : 6 ≤ 2 があって、 s≤s x : 7 ≤ 3 となります。
再帰的にこれは結局4 ≤ 0 という型まで降りてくるわけですが、これが以下のように空であることが分かるので7 ≤ 3 は偽だと証明出来るわけです。

4 ≤ 0

z≤n の定義より、0 ≤ 0, 0 ≤ 1, 0 ≤ 2, .. は存在しますが、この左辺は4 には成り得ないのでここには4 ≤ 0 は存在しません。
s≤s の定義より、z≤n で作られた0 ≤ n から始まってm ≤ (n + m) は存在しますが、やはりここには4 ≤ 0 は存在しません。
従って型4 ≤ 0 は空であることが示せました。

のちほど

上記で省略した”再帰的に”のくだりをAgda では

7≰3 : 7 ≤ 3 → ⊥
7≰3 (s≤s (s≤s (s≤s ())))

と表すことが出来るそうです。
ここで() は空集合の"値"を表しているそうです、Haskell ではユニットと呼ばれるやはり特殊な値に使われている記号ですね。
読み方としては"関数"7≰3が"入力"の型7 ≤ 3 に対して"空"()なる型⊥を返すことで、7 ≤ 3が偽であることが示される、という感じですかね。

また、一旦空集合であることが示せたら他の証明でも使えます。

8≰4 : 8 ≤ 4 → ⊥
8≰4 (s≤s x) = 7≰3 x

Alternative representation

違うやり方。

data _≤′_ : ℕ → ℕ → Set where
  ≤′-refl : {m : ℕ} →                       m ≤′ m
  ≤′-step : {m : ℕ} → {n : ℕ} →  m ≤′ n  →  m ≤′ suc n

infix 4 _≤′_

これによって

≤′-refl : 0 ≤ 0
≤′-step ≤′-refl : 0 ≤ 1
≤′-step (≤′-step ≤′-refl) : 0 ≤ 2
...
≤′-refl : 1 ≤ 1
≤′-step ≤′-refl : 1 ≤ 2
≤′-step (≤′-step ≤′-refl) : 1 ≤ 3
...
≤′-refl : 2 ≤ 2
≤′-step ≤′-refl : 2 ≤ 3
≤′-step (≤′-step ≤′-refl) : 2 ≤ 4
...

が生成されます。
もちろん作り方が異なるのでm ≤ n とm ≤′ n は異なるわけですが、考える問題によってどっちが良いかが決まります。
人間の脳コンパイラはこの辺を吸収して自動的によろしい方を選択するわけですね、なんと賢い。

Syntactic abbreviations

以下のコードはすべて正しいコードとなります、どれが良い書き方なんでしょうかね？
個人的にはふたつ目のはあまり美しくない気がする、好みなのはやはり最初か最後かな。

data  _≤_ : ℕ → ℕ → Set where
  z≤n : {n : ℕ} →                       zero  ≤ n
  s≤s : {m : ℕ} → {n : ℕ} →   m ≤ n  →  suc m ≤ suc n

data  _≤_ : ℕ → ℕ → Set where
  z≤n : {n : ℕ} →                     zero  ≤ n
  s≤s : {m : ℕ} {n : ℕ} →   m ≤ n  →  suc m ≤ suc n

data  _≤_ : ℕ → ℕ → Set where
  z≤n : {n : ℕ} →               zero  ≤ n
  s≤s : {m n : ℕ} →   m ≤ n  →  suc m ≤ suc n

data  _≤_ : ℕ → ℕ → Set where
  z≤n : {n : _} →               zero  ≤ n
  s≤s : {m n : _} →   m ≤ n  →  suc m ≤ suc n

data  _≤_ : ℕ → ℕ → Set where
  z≤n : ∀ {n} →               zero  ≤ n
  s≤s : ∀ {m n} →   m ≤ n  →  suc m ≤ suc n

_+≡: Addition predicate

m + n ≡ k の形の命題の証明を考えます。

方針としてはm + n ≡ k という型の集合を考え、それが空か否かを判定するということになります。
従って2 + 2 ≡ 5 は空集合という意味で正しくて、m + n ≡ k なる集合が空集合でない必要十分条件はn + m = k となります。

Definition of _+≡

DefinitionOfAdditionPredicate.agda

data _+_≡_ : ℕ → ℕ → ℕ → Set where
  znn : ∀ {n} → zero + n ≡ n
  sns : ∀ {m n k} → m + n ≡ k → suc m + n ≡ suc k

これは以下のコードと同値です。

data _+_≡_ : ℕ → ℕ → ℕ → Set where
  znn : {n : ℕ} → zero + n ≡ n
  sns : {m : ℕ} → {n : ℕ} → m + n ≡ k → suc m + n ≡ suc k

これらはsuc を使うことで一刻みに網羅する方針。

Definition reuse

さらにあるいは

data _≤″_ : ℕ → ℕ → Set where
  ≤+ : ∀ {m n k} → m + n ≡ k → m ≤″ k

と定義することによって任意のn について網羅することが出来ます。

Sets.Parameters_vs_Indices

open import Data.Nat using (ℕ; zero; suc; _≤_; z≤n; s≤s)
open import Data.List using (List; []; _∷_)

Parameters vs. indices

（型とインスタンスの）引数の位置が対応していればパラメータとして書き下せるそうです、以下がもとの文章です。

The first index can be turned into a new parameter if each constructor has the same variable on the first index position (in the result type).

これは例を見たほうがわかりやすいと思います。

例１

以下の２つは”似ている”そうです。

data _≤′_ : ℕ → ℕ → Set where
  ≤′-refl : {m : ℕ} →                       m ≤′ m
  ≤′-step : {m : ℕ} → {n : ℕ} →  m ≤′ n  →  m ≤′ suc n

data _≤′_ (m : ℕ) : ℕ → Set where
  ≤′-refl :                       m ≤′ m
  ≤′-step : {n : ℕ} →  m ≤′ n  →  m ≤′ suc n

例２

このみっつも似ているそうです。

data _≤″_ : ℕ → ℕ → Set where
  ≤+ : ∀ {m n k} → m + n ≡ k → m ≤″ k

data _≤″_ (m : ℕ) : ℕ → Set where
  ≤+ : ∀ {n k} → m + n ≡ k → m ≤″ k

data _≤″_ (m : ℕ) (k : ℕ) : Set where
  ≤+ : ∀ {n} → m + n ≡ k → m ≤″ k

Design decision

まだ書き直す前の定義の方がわかりやすく感じるのですが、パラメータを使うというのは選択肢として良いらしいです。

-集合の構造について多く記載することによって、Agda コンパイラが推測できる性質が増える。
-コンストラクタの引数が減るのでわかりやすくなる。

例えばパラメータを一つ固定するだけで

data 10≤′ : ℕ → Set where
  10≤′-refl :                       10≤′ 10
  10≤′-step : {n : ℕ} →  10≤′ n  →  10≤′ suc n

という形で簡単に定義が可能になります。

General equality: ≡

data  _≡_ {A : Set} (x : A) : A → Set  where
  refl : x ≡ x

infix 4 _≡_

集合A を暗に固定しておいて、x をパラメータとした定義ですね。

∈ proposition

data _∈_ {A : Set}(x : A) : List A → Set where
  first : ∀ {xs} → x ∈ x ∷ xs
  later : ∀ {y xs} → x ∈ xs → x ∈ y ∷ xs

infix 4 _∈_

これもx をパラメータとした定義ですね。

おわり

とりあえずAgda による集合の扱いに触ってみた、という段階です。
Haskell のようでHaskell でないAgda 、なかなかおもしろそうです。
カリー化された型定義と数学の作法に似た定義をそのまま書ける感じはおそらくHaskell ゆずりなんでしょう、冬休みの間にもう少し理解が進むと良いですね。

コードを書き下す際に、lang:FileName.agdaと書くとプレビューではシンタックスハイライトされずにすべてagda としたのでやや参照しづらいですね、これは投稿したら実は上手くなってたりするのだろうか、というわけで以下は実験。

In.agda

data _∈_ {A : Set}(x : A) : List A → Set where
  first : ∀ {xs} → x ∈ x ∷ xs
  later : ∀ {y xs} → x ∈ xs → x ∈ y ∷ xs

infix 4 _∈_

この部分は英語の方が文法的に良く出来ていて例えば Bool is a Set. のように表現されます。 ↩