Agda Tutorial よりSets

# はじめに

Agda あるいは一般に定理照明器を触るにあたって基本的な数学を"実装"してみようというのはおそらく自然な欲求だと思う、[みょんさん](https://gist.github.com/myuon/7deee7f90984cebcd34a)みたいに米田の補題とかためしてみるのとかクールだと思う。
圏論をためしてみるの良いよと[河野先生](https://www.google.co.jp/url?sa=t&rct=j&q=&esrc=s&source=web&cd=2&ved=0ahUKEwiBt9vayKHKAhXDW5QKHW-1CSEQFggpMAE&url=https%3A%2F%2Fipsj.ixsq.nii.ac.jp%2Fej%2Findex.php%3Faction%3Dpages_view_main%26active_action%3Drepository_action_common_download%26item_id%3D113012%26item_no%3D1%26attribute_id%3D1%26file_no%3D1%26page_id%3D13%26block_id%3D8&usg=AFQjCNE9a6jA6tvywlKXPe7l-B8CzxBNAg&sig2=oGL24-inFUkfb2ijzjP-dw&cad=rja)もおっしゃってくれてるのでいずれ挑戦しようと思ってます。

てなわけで、[Agda Tutorial](http://people.inf.elte.hu/divip/AgdaTutorial/Index.html)を上から写経していこうと思い立ったのでまずは第一弾、集合。

# [Modules.Basic](http://people.inf.elte.hu/divip/AgdaTutorial/Modules.Basic.html#1)
Agda のモジュールはmodule header が必要、とのこと。
（単なるAgda ファイルならどうなんだろう？）
Emacs にロードさせて（解釈させて）シンタックスハイライトさせるためにはC-c C-lと打ちましょう。

# [Sets.Enumerated](http://people.inf.elte.hu/divip/AgdaTutorial/Sets.Enumerated.html#1)
列挙ですね、外延的なのかな？

## The Bool set
Haskell に似て非なるBoolean

```agda
data Bool : Set where
  true : Bool
  false : Bool
```

これは[^1]
- Bool は Set の"要素”
- true とfalse は Bool の"要素"

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

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

```agda
Setᵢ : Setᵢ₊₁
```

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

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

```agda
data ⊥ : Set where

data ⊤ : Set where
  tt : ⊤
```

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

## Types vs. sets
型と集合の違い

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

# [Sets.Recursive](http://people.inf.elte.hu/divip/AgdaTutorial/Sets.Recursive.html#1)
再帰というとリストとか二分木とかですね。

## Import List

```agda
module Sets.Recursive where

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

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

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

```agda
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 ℕ
ペアノ数はいわば一進法に相当するわけで、二進法のもある、もちろん同型であるわけだが証明が必要。

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

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

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

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

# [Constants](http://people.inf.elte.hu/divip/AgdaTutorial/Constants.html#1)
## Import List

```agda
module Constants where

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

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

```agda
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](http://people.inf.elte.hu/divip/AgdaTutorial/Syntax.Decimal_Naturals.html#1)
、、、要はペアノ数と普段使ってる十進法の間に組み込みの対応を用意してますよーとのこと。

# [Syntax.Infix](http://people.inf.elte.hu/divip/AgdaTutorial/Syntax.Infix.html#1)
```agda
module Syntax.Infix where

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

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

```agda
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'

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

```agda
infixr 3 _+_
```

こう宣言することで

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

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

# [Sets.Mutual](http://people.inf.elte.hu/divip/AgdaTutorial/Sets.Mutual.html#1)

```agda
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 で（型）宣言をする必要があります：

```agda
data L : Set
data M : Set

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

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

# [Sets.Parametric](http://people.inf.elte.hu/divip/AgdaTutorial/Sets.Parametric.html#1)

```agda
module Sets.Parametric where
open import Data.Nat
```

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

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

infixr 5 _∷_
```

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

```agda
[]  
true  ∷ []  
false ∷ []
true  ∷ true  ∷ []  
false ∷ true  ∷ []  
true  ∷ false ∷ []  
false ∷ false ∷ []  
...
```

となります。

## _×_: Cartesian Product
デカルト積です。

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

infixr 4 _,_
infixr 2 _×_
```

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

```agda
true , true 
true , false
false , true
false , false
```

というわけです。

## _⊎_: Disjoint Union (Sum)
今度は直和です。

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

infixr 1 _⊎_
```

# [Sets.Indexed](http://people.inf.elte.hu/divip/AgdaTutorial/Sets.Indexed.html#1)

```agda
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 個の集合です。
このとき、明らかに数が等しいので

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

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

## Definition of Fin

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

## Vec A n ~ Aⁿ

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

# [Term_Inference](http://people.inf.elte.hu/divip/AgdaTutorial/Term_Inference.html#1)

```lang: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 の引数なのでℕ 型だというわけです。

```agda
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
アンダースコアは隠すこともできます、とのこと。
引数を"暗示的に”扱う際は{}を使いなさい、とのこと。

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

このとき

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

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

```agda
x″ : Fin 3
x″ = suc zero
```

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

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

```agda
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)
```

同様に

```agda
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](http://people.inf.elte.hu/divip/AgdaTutorial/Sets.Propositions.html#1)

```agda
module Sets.Propositions where

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

## Proofs as data
Agda のキモである証明について。

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

```agda
data ⊤ : Set where
  tt : ⊤
```

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

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

```agda
data ⊥ : Set where
```

### 論理積あるいはAND
A, B を命題としてそれらの論理積を型A × B で表す。

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

infixr 4 _,_
infixr 2 _×_
```

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

### 論理和あるいはOR
論理積の双対ですね。

```agda
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 でインデックスされた集合を定義します。

```agda
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 では

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

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

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

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

## Alternative representation
違うやり方。

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

```agda
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 _+_≡_

```lang:DefinitionOfAdditionPredicate.agda
data _+_≡_ : ℕ → ℕ → ℕ → Set where
  znn : ∀ {n} → zero + n ≡ n
  sns : ∀ {m n k} → m + n ≡ k → suc m + n ≡ suc k
```

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

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

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

## Definition reuse
さらにあるいは

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

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

# [Sets.Parameters_vs_Indices](http://people.inf.elte.hu/divip/AgdaTutorial/Sets.Parameters_vs_Indices.html#1)

```agda
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).


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

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

```agda
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
```

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

```agda
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 コンパイラが推測できる性質が増える。
-コンストラクタの引数が減るのでわかりやすくなる。

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

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

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

## General equality: _≡_

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

infix 4 _≡_
```

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

## _∈_ proposition

```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 _∈_
```

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

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

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

```lang: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 _∈_
```