やったこと

Agdaで自然数を定義して基本的な性質を示しました。

コード

自然数の定義

data ℕ : Set where
    zero : ℕ
    succ : ℕ → ℕ

_+_ : ℕ → ℕ → ℕ
zero + m = m
succ n + m = succ (n + m)

_*_ : ℕ → ℕ → ℕ
zero * _ = zero
succ n * m = m + (n * m)

_≤_ : ℕ → ℕ → Set
n ≤ m = Σ ℕ (λ l → n + l ≡ m)

今回は数学での流儀によせようとして順序を存在量化を用いて定義しましたが、以下の様に定義した方が証明しやすいでしょう。コードの最後で同値性を証明しているので論理的にはどちらを用いても問題ありません。

data _≲_ : ℕ → ℕ → Set where
    0≲n : {n : ℕ} → zero ≲ n
    s≲s : {n m : ℕ} → n ≲ m → succ n ≲ succ m

証明の例

例えば、+の可換性は以下の様に証明しています。Reasoningと数学的帰納法を乱用してます。

+-rUnit : (n : ℕ) → n + zero ≡ n
+-rUnit zero = refl
+-rUnit (succ n) = cong succ (+-rUnit n)

+-right : (n m : ℕ) → n + succ m ≡ succ (n + m)
+-right zero m = refl
+-right (succ n) m = cong succ (+-right n m)

+-comm : (m n : ℕ) → m + n ≡ n + m
+-comm zero n = sym (+-rUnit n)
+-comm (succ m) n = begin
        succ (m + n)
    ≡⟨ cong succ (+-comm m n) ⟩
        succ (n + m)
    ≡⟨ sym (+-right n m) ⟩
        n + succ m
    ∎

まとめ

このコードを書きながらReasoning(_≡⟨_⟩_で式変形を行なう技法)を理解したのですが、現在の式とGoalを確認しながら証明を進めることができて非常にやりやすいですね。
Agda初心者なので直和やReasoningについて調べながら書いたのですが、Agdaはライブラリを探しにくいですね。Hoogleみたいなものがあればいいのですが。

予定

今回定義した自然数を拡張して整数、有理数、実数と定義していきたいのですが、Agdaで商集合ってどうやってとるんですかね?簡単に調べたところSetoidとやらを使うらしいですが……
初心者なので調べつつ挑戦していきます。

参考文献

エルフに数学を装備するだけ (http://ncode.syosetu.com/n2185cj/)
Encyclopedia of P-adic Numbers (http://padic.wicurio.com/)
Agda Tutorial (http://people.inf.elte.hu/divip/AgdaTutorial/Index.html#general-information)