title: Agda 入門
author: Yasutaka Higa
cover:
lang: Japanese


# このセミナーの目的
* 証明支援系の言語である Agda の入門を目的としています
* 具体的には
  * Agda による証明の方法を知る
  * 実際に自然数に対する演算の証明を追う
* ことをしていきます


# Agda とはどういう言語なのか
* 証明支援系と呼ばれる分野の言語です
  * 他には Coq などがあります
* Haskell で実装されています
* dependent type の言語 です
  * 型を第一級オブジェクトとして扱える
  * X -> X, f x, a == b のような型を扱うことができます


# 型と証明との対応 : Curry-Howard Isomorphism
* Agda における証明は
  * 証明したい命題 == 関数の型
  * 命題の証明     == 関数の定義
* として定義します
* 関数と命題の対応を Curry-Howard Isomorphism と言います


# Agda をはじめよう
* emacs に agda-mode があります
* module filename where
* を先頭に書く必要があります
* 証明を定義していく
* C-c C-l で型チェック(証明チェック)ができます


# 自然数の定義 : Peano Arithmetic
* 自然数 0 が存在する
* 任意の自然数 a にはその後続数 suc(a) が存在する
* 0 より前の自然数は存在しない
* 異なる自然数は異なる後続数を持つ
    * a != b のとき suc(a) != suc(b) となる
* 0 が性質を満たし、a も性質を満たせばその後続数も性質を満たすとき、すべての自然数はその性質を満たす


# Agda における自然数の定義
* data 型を使います

```
  data Int : Set where
    O : Int
    S : Int -> Int
```
* Int は O か、 Int に S がかかったもののみ
* Set は組込みで存在する型です。「成り立つ」と考えてもらえれば良いです。


# 自然数の例
* 0 = O
* 1 = S O
* 2 = S (S O)
* 5 = S (S (S (S (S O))))


# 自然数に対する演算の定義
* x と y の加算 : x にかかっている S の分だけ S を b に適用する
* x と y の乗算 : x にかかっている S の分だけ y を 0 に加算する

* Agda tips : 不明な項を ? と書くこともできます。 goal と呼びます
* その状態で C-c C-l するとその項の型が分かります


# Agda における自然数に対する演算の定義
```
  infixl 30 _+_
  _+_ : Int -> Int -> Int
  x + O     = x
  x + (S y) = S (x + y)
```

* Agda tips : C-c C-n すると式を評価することができます
* (S O) + (S (S O)) などしてみましょう


# Agda における関数定義のSyntax
* Agda において、関数は
  * 関数名                      : 型
  * 関数名 引数はスペース区切り = 関数の定義や値
* のように定義します
* 中置関数は _ で挟みます


# Agda で複数の引数がある関数の型
* func : A -> (A -> B) -> B

* 引数の型 -> 返り値の型
* -> の結合は右結合です。なので括弧を付けると以下のようになります
  * A -> ((A -> B) -> B)
* 右結合のため、A を受けとって ((A -> B) -> B) を返す、とも読めます


# パターンマッチ
* Agda においてはデータ型は引数で分解することができます
* ある型に続している値が、どのコンストラクタにおいて構成されたかをパターンで示せます
* Int は O か Int に S が付いたもの、でした
  * double : Int -> Int
  * double O     = O
  * double (S x) = S (S (double x))
* 関数名 (引数のパターン) = 定義


# もういちど : 自然数に対する演算の定義
```
  infixl 30 _+_
  _+_ : Int -> Int -> Int
  x + O     = x
  x + (S y) = S (x + y)
```
* 中置、関数、パターンマッチが使われています
* infixl は左結合を意味します。数値は結合強度です


# これから証明していきたいこと
* 加法の交換法則 : (x + y) = (y + x)
* 加法の結合法則 : (x + y) + z = x + (y + z) <- 目標ライン

* 乗法の交換法則 : (x * y) = (y * x)

# '等しい' ということ
* '等しい'という型 _ ≡ _ を定義する
  * refl  : x ≡ x
  * sym   : x ≡ y -> y ≡ x
  * cong  : (f : A -> B) -> x ≡ y -> f x ≡ f y
  * trans : x ≡ y -> y ≡ z -> y ≡ z
* defined : Relation.Binary.PropositionalEquality in Standard Library
* Agda tips : 記号は \ の後に文字列を入れると出てきます。 '≡' は "\ =="


# '同じもの'とは
* 項なら同じ項
  * term : (A : Set) -> (a : Set) -> a ≡ a
  * term A a = refl
* 関数なら normal form が同じなら同じ
  * lambda-term : (A : Set)  -> (\(x : A) -> x) ≡ (\(y : A) -> y)
  * lambda-term A = refl
* 関数による式変形は等しいものとして扱います


# 交換法則を型として定義する
* ≡を用いて
  * (x : Int) -> (y : Int) -> x + y ≡ y + x
* 引数は (名前 : 型) として名前付けできます


# 交換法則を証明していく
```
  sum-sym : (x y : Int)  -> x + y ≡ y + x
  sum-sym    O     O  = refl
  sum-sym    O  (S y) = cong S (sum-sym O y)
  sum-sym (S x)    O  = cong S (sum-sym x O)
  sum-sym (S x) (S y) = ?
```

# trans による等式変形
* sum-sym (S x) (S y) の時は1つの関数のみで等しさを証明できない
* 等しさを保ったまま式を変形していくことが必要になります

* sum-sym (S x) (S y) = trans (a ≡ b) (b ≡ c)
  * trans (refl) ?
  * trans (trans refl (cong S (left-add-one x y)) ?


# ≡-reasoning による等式変形
* trans が何段もネストしていくと分かりづらい
* ≡-reasoning という等式変形の拡張構文が Standard Library にあります

```
  begin
    変換前の式
      ≡⟨ 変換する関数 ⟩
    変換後の式
  ∎
```


# ≡-reasoning による最初の定義

```
  sum-sym (S x) (S y) = begin
      (S x) + (S y)
    ≡⟨ ? ⟩
      (S y) + (S x)
    ∎
```


# 交換法則の証明 : + の定義による変形
* 上から + の定義により変形

```
  sum-sym (S x) (S y) = begin
      (S x) + (S y)
    ≡⟨ refl ⟩
      S (S x + y)
    ≡⟨ ? ⟩
      (S y) + (S x)
    ∎
```


# cong と sum-sym を使って交換
* S が1つ取れたのでsum-symで交換できる
* sum-sym で交換した後に cong で S がかかる

```
    S ((S x) + y)
  ≡⟨ cong S (sum-sym (S x) y) ⟩
    S ((y + (S x)))
```


# 加法の時に左側からSを移動させられない

* 加法の定義は
  * x + (S y) = S (x + y)
* left-operand にかかっている S を移動させる方法が無い
* たしかに
  * S (y + S x) ≡ S y + S x
* にあてはまるものを入れてくれ、と出てきている


# left-operand からSを操作する証明を定義
```
  left-increment : (x y : Int) -> (S x) + y ≡ S (x + y)
  left-increment x y = ?
```

* Agda tips : goal の上で C-c C-c で引数のパターン分け
  * 例えば y にのみ適用してみる
* Agda tips : goal の上で C-c C-a で証明を探してくれる


# left-operand からSを移動させる
* left-increment は (S x) + y ≡ S (x + y) なので逆にして使う

```
    ...
    S ((S x) + y)
      ≡⟨ sym (left-increment x (S y)) ⟩
    (S y) + (S x)
  ∎
```


# 加法の交換法則 : (x + y) = (y + x)
```
  sum-sym (S x) (S y) = begin
      (S x) + (S y)
    ≡⟨ refl ⟩
      S ((S x) + y)
    ≡⟨ cong S (sum-sym (S x) y) ⟩
      S (y + (S x))
    ≡⟨ (sym (left-increment y (S x))) ⟩
      (S y) + (S x)
    ∎
```


# 加法の結合法則 : (x + y) + z = x + (y + z)
* 次に結合法則を証明します
* 手順は同じです
  * ≡ で証明したい式を定義
  * 定義に証明を書く
  * 必要ならば等式を変形していく
* ちなみに x + y + z は infixl なので ((x + y) + z) となります


# Agda による証明方法のまとめ
* 関数の型を命題、関数の定義を証明とする
* 等しさを証明するには等しいという型を定義する
* 等しさを保ったまま式を変形していくことにより等価性を証明できる
    * trans, reasoning
* C-c C-l により型のチェックが成功すれば証明終了


# 乗法の定義
```
  infixl 40 _*_
  _*_ : Int -> Int -> Int
  n *    O  = O
  n * (S O) = n
  n * (S m) = n + (n * m)
```

* _+_ よりも結合強度を上げるといわゆる自然数の演算


# 乗法の交換法則 : (x * y) = (y * x)
```
  mult-sym : (x y : Int) -> x * y ≡ y * x
```

途中で

```
  (x y : Int) -> (S x) * y ≡ y + (x * y)
```

が必要になることが分かる


# Agdaにおいて何ができるのか
* 証明の正しさを対話的に教えてくれる
  * それに必要な証明が結果的に分かることもある
* 今回は Int に対する演算だった
  * lambda-term に落とせれば Agda で証明していける
* 他にも命題論理の証明などがある
* プログラミング言語そのものに対するアプローチ
  * lambda-term の等価性によってリファクタリングなど


<!-- vim: set filetype=markdown.slide: -->