前回の記事 Agdaで自然数
やったこと
Agdaで整数を定義し, 基本的な性質を証明しました.
ソースコード
整数の構成
整数全体の集合$\mathbb{Z}$とは$\mathbb{N}\times\mathbb{N}$を次の同値関係$\equiv$で割った集合$\mathbb{N}\times\mathbb{N}/\equiv$のことです.
$$
(a, b) \equiv (c, d) \Leftrightarrow a + d = b + c
$$
$\mathbb{Z}$上の和と積は次のように定義できます. この和と積の定義は同値類の代表元によりません(ソースコードの+ℤ-lUniv, +ℤ-rUniv, *ℤ-lUniv, *ℤ-rUniv).
\begin{align}
(a, b) + (c, d) &= (a + c, b + d) \\
(a, b) \times (c, d) &= (a \times c + b \times d , a \times d + b \times c)
\end{align}
このとき和の単位元は$(0, 0)$で積の単位元は$(1, 0)$になり, 整数$(a, b)$の逆元は$(b, a)$です.
また, $+$と$\times$は交換法則と結合法則, 分配法則を見たすので$\mathbb{Z}$は可換環をなします.
整数の重要な性質として自然数を含むことが挙げられますが, 実際に$\mathbb{Z}$から$(m, 0)$なる要素を全て取り出すと自然数をなします. すなわち, $(m, 0)$なる要素が正の整数であり, $(0, m)$なる要素が負の整数です.
整数での順序は次のように定義できます.
$$
a \leq b \Leftrightarrow \exists m \in \mathbb{N}. a + (m,0) = b
$$
この順序関係は全順序になります.
まとめ
Setoidを用いて$\mathbb{Z}$を定義しましたが、Setoid上の射を定義する方法がわからず、結局は台集合上の射として和と積を定義し、Setoidに触れることなく緒性質を証明しました。 また、上で定義した同値関係でReasoningをする方法がわからず、同値関係の定義を展開して証明するような形になってしまいました。