3
1

Delete article

Deleted articles cannot be recovered.

Draft of this article would be also deleted.

Are you sure you want to delete this article?

More than 5 years have passed since last update.

Agdaで自然数

Posted at

やったこと

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
    0n : {n : }  zero  n
    ss : {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とやらを使うらしいですが……
初心者なので調べつつ挑戦していきます。

参考文献

3
1
0

Register as a new user and use Qiita more conveniently

  1. You get articles that match your needs
  2. You can efficiently read back useful information
  3. You can use dark theme
What you can do with signing up
3
1

Delete article

Deleted articles cannot be recovered.

Draft of this article would be also deleted.

Are you sure you want to delete this article?