Agdaで加法の交換法則

Agdaのインストールについては
Agdaのインストール | righ1113のブログ
を参照ください。

Agda 入門
を参考にしながら、というか写しで書いてみた。

module plus where

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

-- natural number
data Nat : Set where
  O : Nat
  S : Nat → Nat

-- plus operator
_+_ : Nat → Nat → Nat
x + O = x
x + (S y) = S (x + y)

left-increment : (x y : Nat) -> (S x) + y ≡ S (x + y)
left-increment x O = refl
left-increment x (S y) = cong S (left-increment x y)
-- add-sym
add-sym : (x y : Nat)  -> x + y ≡ y + x
add-sym    O     O  = refl
add-sym    O  (S y) = cong S (add-sym O y)
add-sym (S x)    O  = cong S (add-sym x O)
add-sym (S x) (S y) = begin
    (S x) + (S y)
  ≡⟨ refl ⟩
    S ((S x) + y)
  ≡⟨ cong S (add-sym (S x) y) ⟩
    S (y + (S x))
  ≡⟨ (sym (left-increment y (S x))) ⟩
    (S y) + (S x)
  ∎
  where open PropEq.≡-Reasoning

＆#10216;は⟨で、＆#10217;は⟩で、＆#8718;は∎です。
解説は……できない……