Agdaで整数 その2

前回作った俺整数の正しさを証明するために、
俺整数が加法に対してアーベル群をなす事を証明しようと思った。
加法の定義は少し変えた。
　

module integer4 where

import Relation.Binary.PropositionalEquality as PropEq
open PropEq using (_≡_; refl; sym; cong; cong₂; trans)

-- integer
data Int : Set where
  O : Int
  P : Int → Int
  M : Int → Int
-- plus operator
_+_ : Int → Int → Int
x + O = x
O + y = y
P x + P y = P ((P x) + y)
M x + P y = x + y
P x + M y = x + y
M x + M y = M ((M x) + y)
postulate
  npn : (x y z : Int) → (x + P y) + z ≡ (M x + P y) + P z
  nnn : (x y z : Int) → (x + y) + z ≡ (x + M y) + P z
  nmn : (x y z : Int) → (x + M y) + z ≡ (P x + M y) + M z
  nnn2 : (x y z : Int) → (x + y) + z ≡ (x + P y) + M z
  mp : (x : Int) → x ≡ M (P x)
  pm : (x : Int) → x ≡ P (M x)
  xx : (x : Int) → x ≡ x
-- inverse operator
negpos : Int → Int
negpos O = O
negpos (P x) = M (negpos x)
negpos (M x) = P (negpos x)

-- proof of abelian group
-- 1.Closure -> OK, because type

-- 2.Associativity
add-asso : (x y z : Int) → x + (y + z) ≡ (x + y) + z
add-asso x y O = refl
-- P z
add-asso _ O (P _) = refl
add-asso O (P _) (P _) = refl
add-asso (P x) (P y) (P z) = begin
    P x + (P y + P z)
  ≡⟨ refl ⟩
    P x + P (P y + z)
  ≡⟨ refl ⟩
    P (P x + (P y + z))
  ≡⟨ cong P (add-asso (P x) (P y) z) ⟩
    P ((P x + P y) + z)
  ∎
  where open PropEq.≡-Reasoning
add-asso (M x) (P y) (P z) = begin
    M x + (P y + P z)
  ≡⟨ refl ⟩
    M x + P (P y + z)
  ≡⟨ refl ⟩
    x + (P y + z)
  ≡⟨ add-asso x (P y) z ⟩
    (x + P y) + z
  ≡⟨ npn x y z ⟩
    (M x + P y) + P z
  ∎
  where open PropEq.≡-Reasoning
add-asso x (M y) (P z) = begin
    x + (M y + P z)
  ≡⟨ refl ⟩
    x + (y + z)
  ≡⟨ add-asso x y z ⟩
    (x + y) + z
  ≡⟨ nnn x y z ⟩
    (x + M y) + P z
  ∎
  where open PropEq.≡-Reasoning
-- M z
add-asso _ O (M _) = refl
add-asso O (M _) (M _) = refl
add-asso (M x) (M y) (M z) = begin
    M x + (M y + M z)
  ≡⟨ refl ⟩
    M x + M (M y + z)
  ≡⟨ refl ⟩
    M (M x + (M y + z))
  ≡⟨ cong M (add-asso (M x) (M y) z) ⟩
    M ((M x + M y) + z)
  ∎
  where open PropEq.≡-Reasoning
add-asso x (P y) (M z) = begin
    x + (P y + M z)
  ≡⟨ refl ⟩
    x + (y + z)
  ≡⟨ add-asso x y z ⟩
    (x + y) + z
  ≡⟨ nnn2 x y z ⟩
    (x + P y) + M z
  ∎
  where open PropEq.≡-Reasoning
add-asso (P x) (M y) (M z) = begin
    P x + (M y + M z)
  ≡⟨ refl ⟩
    P x + M (M y + z)
  ≡⟨ refl ⟩
    x + (M y + z)
  ≡⟨ add-asso x (M y) z ⟩
    (x + M y) + z
  ≡⟨ nmn x y z ⟩
    (P x + M y) + M z
  ∎
  where open PropEq.≡-Reasoning

-- 3.Commutativity
left-incrementP : (x y : Int) → (P x) + y ≡ P (x + y)
left-incrementP x O = refl
left-incrementP x (P y) = begin -- (P x + P y) ≡ P (x + P y)
    P x + P y
  ≡⟨ refl ⟩
    P (P x + y)
  ≡⟨ cong₂ (\ x y → P (P x + y)) (xx x) (mp y) ⟩
    P (P x + M (P y))
  ∎
  where open PropEq.≡-Reasoning
left-incrementP x (M y) = begin -- (P x + M y) ≡ P (x + M y)
    P x + M y
  ≡⟨ refl ⟩
    x + y
  ≡⟨ cong₂ (\ x y → x + y) (pm x) (pm y) ⟩
    P (M x) + P (M y)
  ≡⟨ refl ⟩
    P (P (M x) + M y)
  ≡⟨ cong₂ (\ x y → P (x + M y)) (sym (pm x)) (xx y) ⟩
    P (x + M y)
  ∎
  where open PropEq.≡-Reasoning
left-incrementM : (x y : Int) → (M x) + y ≡ M (x + y)
left-incrementM x O = refl
left-incrementM x (P y) = begin
    M x + P y
  ≡⟨ refl ⟩
    x + y
  ≡⟨ cong₂ (\ x y → x + y) (mp x) (mp y) ⟩
    M (P x) + M (P y)
  ≡⟨ refl ⟩
    M (M (P x) + P y)
  ≡⟨ cong₂ (\ x y → M (x + P y)) (sym (mp x)) (xx y) ⟩
    M (x + P y)
  ∎
  where open PropEq.≡-Reasoning
left-incrementM x (M y) = begin
    M x + M y
  ≡⟨ refl ⟩
    M (M x + y)
  ≡⟨ cong₂ (\ x y → M (M x + y)) (xx x) (pm y) ⟩
    M (M x + P (M y))
  ∎
  where open PropEq.≡-Reasoning
add-sym : (x y : Int) → x + y ≡ y + x
add-sym O O = refl
add-sym (P _) O = refl
add-sym (M _) O = refl
add-sym O (P _) = refl
add-sym O (M _) = refl
add-sym (P x) (P y)  = begin
    P x + P y
  ≡⟨ refl ⟩
    P ((P x) + y)
  ≡⟨ cong P (add-sym (P x) y) ⟩
    P (y + (P x))
  ≡⟨ sym (left-incrementP y (P x)) ⟩
    P y + P x
  ∎
  where open PropEq.≡-Reasoning
add-sym (M x) (P y) rewrite add-sym x y = refl
add-sym (P x) (M y) rewrite add-sym x y = refl
add-sym (M x) (M y) = begin
    M x + M y
  ≡⟨ refl ⟩
    M ((M x) + y)
  ≡⟨ cong M (add-sym (M x) y) ⟩
    M (y + (M x))
  ≡⟨ sym (left-incrementM y (M x)) ⟩
    M y + M x
  ∎
  where open PropEq.≡-Reasoning

-- 4.Existence of an identity element
zero-elem : (x : Int) → x + O ≡ x
zero-elem x = refl

-- 5.Existence of inverse elements
inv-elem : (x : Int) → x + (negpos x) ≡ O
inv-elem O = refl
inv-elem (P x) rewrite inv-elem x = refl
inv-elem (M x) rewrite inv-elem x = refl

　
少し解説を。
1.演算の閉性
これは問題ない。型が保証してくれる。

2.結合法則
いちばん苦労した。postulateを使っているから厳密には出来てない。
P x + (P y + P z) ≡ P ((P x + P y) + z)
を証明してなぜうまくいくのか分かっていない。

3.交換法則
これもpostulateを使っている。
でもx ≡ M (P x)だから罪悪感は少ない。

4.零元の存在
5.逆元の存在
これらはスマートにできた。

まあ、ここまでは出来ましたよ〜ってことで。