Agdaで俺整数を定義してみた。
Natから符号を付けてIntを定義する方法も考えたけど、ゴチャゴチャしてやめた。
0と、+1を表すPと、-1を表すMで構成した。
module integer2 where import Relation.Binary.PropositionalEquality as PropEq open PropEq using (_≡_; refl; sym; cong; trans) -- integer data Int : Set where O : Int P : Int → Int M : Int → Int -- plus operator _+_ : Int → Int → Int x + O = x x + (P y) = P (x + y) x + (M y) = M (x + y) -- minus operator _-_ : Int → Int → Int x - O = x x - (P y) = M (x - y) x - (M y) = P (x - y) -- cancellative operator cancellative : Int → Int cancellative O = O cancellative (P O) = P O cancellative (M O) = M O cancellative (P (P (M x))) = (cancellative x) + (P O) cancellative (P (M (P x))) = (cancellative x) + (P O) cancellative (M (P (M x))) = (cancellative x) + (M O) cancellative (M (M (P x))) = (cancellative x) + (M O) cancellative (P (P x)) = (cancellative x) + (P (P O)) cancellative (M (M x)) = (cancellative x) + (M (M O)) cancellative (P (M x)) = cancellative x cancellative (M (P x)) = cancellative x -- plus' operator _+'_ : Int → Int → Int x +' y = cancellative (cancellative (x + y)) -- minus' operator _-'_ : Int → Int → Int x -' y = cancellative (cancellative (x - y))
C-c C-nで評価してみよう。
(P (P O)) +' (P (P (P O))) => P (P (P (P (P O))))
(P (P O)) -' (P (P (P O))) => M O
(P (P O)) -' (P (P O)) => O
上手くいってる、のかな?
さてこの俺整数、正しさをどうやって証明したら良いのだろう?