俺整数が加法に対してアーベル群をなす事の証明を洗練させてみた。
全体的に、reflで整数から自然数の組に展開させて、
congで自然数の法則を使って、
symで自然数の組から整数に戻す、ということをやっている。
仮定(postulate)したのは
・自然数の結合法則
・自然数の交換法則
・整数のI x x ≡ O
です。
module integer6 where import Relation.Binary.PropositionalEquality as PropEq open PropEq using (_≡_; refl; sym; cong; cong₂; trans) -- nat data ℕ : Set where zero : ℕ succ : ℕ → ℕ -- plus _+_ : ℕ → ℕ → ℕ zero + zero = zero zero + succ y = succ y succ x + zero = succ x succ x + succ y = succ (x + (succ y)) postulate add-sym : (x y : ℕ) → x + y ≡ y + x add-assoc : (x y z : ℕ) → (x + y) + z ≡ x + (y + z) -- integer data ℤ : Set where O : ℤ I : ℕ → ℕ → ℤ postulate zeroZ : (x : ℕ) → I x x ≡ O -- plusZ _+ℤ_ : ℤ → ℤ → ℤ O +ℤ O = O O +ℤ I x y = I x y I x y +ℤ O = I x y I x y +ℤ I z w = I (x + z) (y + w) -- inv negposZ : ℤ → ℤ negposZ O = O negposZ (I x y) = I y x -- proof of abelian group -- 1.Closure -> OK, because type -- 2.Associativity add-assocZ : (i j k : ℤ) → (i +ℤ j) +ℤ k ≡ i +ℤ (j +ℤ k) add-assocZ O O O = refl add-assocZ O O (I u v) = refl add-assocZ O (I z w) O = refl add-assocZ O (I z w) (I u v) = refl add-assocZ (I x y) O O = refl add-assocZ (I x y) O (I u v) = refl add-assocZ (I x y) (I z w) O = refl add-assocZ (I x y) (I z w) (I u v) = begin ((I x y) +ℤ (I z w)) +ℤ (I u v) ≡⟨ refl ⟩ (I (x + z) (y + w)) +ℤ (I u v) ≡⟨ refl ⟩ I ((x + z) + u) ((y + w) + v) ≡⟨ cong₂ I (add-assoc x z u) (add-assoc y w v) ⟩ I (x + (z + u)) (y + (w + v)) ≡⟨ sym (lem1 x y z w u v) ⟩ (I x y) +ℤ (I (z + u) (w + v)) ≡⟨ sym (lem2 x y z w u v) ⟩ (I x y) +ℤ ((I z w) +ℤ (I u v)) ∎ where open PropEq.≡-Reasoning lem1 : (x y z w u v : ℕ) → (I x y) +ℤ (I (z + u) (w + v)) ≡ I (x + (z + u)) (y + (w + v)) lem1 x y z w u v = refl lem2 : (x y z w u v : ℕ) → (I x y) +ℤ ((I z w) +ℤ (I u v)) ≡ (I x y) +ℤ (I (z + u) (w + v)) lem2 x y z w u v = refl -- 3.Commutativity add-symZ : (i j : ℤ) → i +ℤ j ≡ j +ℤ i add-symZ O O = refl add-symZ O (I z w) = refl add-symZ (I x y) O = refl add-symZ (I x y) (I z w) = begin I (x + z) (y + w) ≡⟨ cong₂ I (add-sym x z) (add-sym y w) ⟩ I (z + x) (w + y) ≡⟨ sym (lem x y z w) ⟩ I z w +ℤ I x y ∎ where open PropEq.≡-Reasoning lem : (x y z w : ℕ) → (I z w) +ℤ (I x y) ≡ I (z + x) (w + y) lem x y z w = refl -- 4.Existence of an identity element zero-elemZ : (i : ℤ) → i +ℤ O ≡ i zero-elemZ O = refl zero-elemZ (I x y) = refl -- 5.Existence of inverse elements inv-elemZ : (i : ℤ) → i +ℤ (negposZ i) ≡ O inv-elemZ O = refl inv-elemZ (I x y) = begin (I x y) +ℤ (I y x) ≡⟨ refl ⟩ I (x + y) (y + x) ≡⟨ cong₂ I (id x y) (add-sym y x) ⟩ I (x + y) (x + y) ≡⟨ zeroZ (x + y) ⟩ O ∎ where open PropEq.≡-Reasoning id : (x y : ℕ) → x + y ≡ x + y id x y = refl
