Agdaで整数

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
上手くいってる、のかな？

さてこの俺整数、正しさをどうやって証明したら良いのだろう？