Skip to content
Mathematics in Agda

整数

module integer where

open import identity-type
open import natural-number
open import sigma-type

record Equiv (A : Set) : Set₁ where
 field
   _≈_ : A → A → Set
   refl-≈ : ∀ x → x ≈ x
   sym-≈ : ∀ {x y} → x ≈ y → y ≈ x
   trans-≈ : ∀ {x y z} → x ≈ y → y ≈ z → x ≈ z

open Equiv ⦃ ... ⦄ public

ℤ : Set
ℤ = ℕ × ℕ

instance
  Equivℤ : Equiv ℤ
  _≈_ ⦃ Equivℤ ⦄ m n = fst m +ℕ snd n ＝ fst n +ℕ snd m
  refl-≈ ⦃ Equivℤ ⦄ x = refl
  sym-≈ ⦃ Equivℤ ⦄ e = sym e
  trans-≈ ⦃ Equivℤ ⦄ {x = x} {y = y} {z = z} e₁ e₂ = cancel-right-+ℕ (snd y)
    (
      (fst x +ℕ snd z) +ℕ snd y
          ＝⟨ swap-right-+ℕ (fst x) (snd z) (snd y) ⟩
      (fst x +ℕ snd y) +ℕ snd z
          ＝⟨ cong (_+ℕ snd z) e₁ ⟩
      (fst y +ℕ snd x) +ℕ snd z
          ＝⟨ swap-right-+ℕ (fst y) (snd x) (snd z) ⟩
      (fst y +ℕ snd z) +ℕ snd x
          ＝⟨ cong (_+ℕ snd x) e₂ ⟩
      (fst z +ℕ snd y) +ℕ snd x
          ＝⟨ swap-right-+ℕ (fst z) (snd y) (snd x) ⟩
      (fst z +ℕ snd x) +ℕ snd y
          ∎
    )

加法

infixl 60 _+ℤ_
_+ℤ_ : ℤ → ℤ → ℤ
m +ℤ n = (fst m +ℕ fst n , snd m +ℕ snd n)

+ℤ-resp-≈ : ∀ m n p q → m ≈ p → n ≈ q → m +ℤ n ≈ p +ℤ q
+ℤ-resp-≈ (x , x₁) (x₂ , x₃) (x₄ , x₅) (x₆ , x₇) m≈p n≈q =
  (x +ℕ x₂) +ℕ (x₅ +ℕ x₇)
      ＝⟨ swap-center-+ℕ x x₂ x₅ x₇ ⟩
  (x +ℕ x₅) +ℕ (x₂ +ℕ x₇)
      ＝⟨ cong₂ _+ℕ_ m≈p n≈q ⟩
  (x₄ +ℕ x₁) +ℕ (x₆ +ℕ x₃)
      ＝⟨ swap-center-+ℕ x₄ x₁ x₆ x₃ ⟩
  (x₄ +ℕ x₆) +ℕ (x₁ +ℕ x₃)
      ∎

整数の0を定義する:

0ℤ : ℤ
0ℤ = zero , zero

0ℤは+ℤの単位元となる:

left-unit-+ℤ : ∀ n → 0ℤ +ℤ n ≈ n
left-unit-+ℤ n = refl

right-unit-+ℤ : ∀ n → n +ℤ 0ℤ ≈ n
right-unit-+ℤ (a , b) =
  (a +ℕ zero) +ℕ b
      ＝⟨ assoc-+ℕ a _ _ ⟩
  a +ℕ (zero +ℕ b)
      ＝⟨ cong (a +ℕ_) (comm-+ℕ zero _) ⟩
  a +ℕ (b +ℕ zero)
      ∎

乗法

infixl 70 _*ℤ_
_*ℤ_ : ℤ → ℤ → ℤ
m *ℤ n = (fst m *ℕ fst n +ℕ snd m *ℕ snd n)
       , (snd m *ℕ fst n +ℕ fst m *ℕ snd n)

*ℤ-resp-≈ : ∀ m n p q → m ≈ p → n ≈ q → m *ℤ n ≈ p *ℤ q
*ℤ-resp-≈ (m₁ , m₂) (n₁ , n₂) (p₁ , p₂) (q₁ , q₂) m≈p n≈q = cancel-right-+ℕ (p₂ *ℕ n₂ +ℕ p₁ *ℕ n₁) (cancel-left-+ℕ (p₂ *ℕ n₁ +ℕ p₁ *ℕ n₂) (
  (p₂ *ℕ n₁ +ℕ p₁ *ℕ n₂) +ℕ (((m₁ *ℕ n₁ +ℕ m₂ *ℕ n₂) +ℕ (p₂ *ℕ q₁ +ℕ p₁ *ℕ q₂)) +ℕ (p₂ *ℕ n₂ +ℕ p₁ *ℕ n₁))
      ＝⟨ cong (p₂ *ℕ n₁ +ℕ p₁ *ℕ n₂ +ℕ_) (assoc-+ℕ (m₁ *ℕ n₁ +ℕ m₂ *ℕ n₂) _ _) ⟩
  (p₂ *ℕ n₁ +ℕ p₁ *ℕ n₂) +ℕ ((m₁ *ℕ n₁ +ℕ m₂ *ℕ n₂) +ℕ ((p₂ *ℕ q₁ +ℕ p₁ *ℕ q₂) +ℕ (p₂ *ℕ n₂ +ℕ p₁ *ℕ n₁)))
      ＝⟨ cong (p₂ *ℕ n₁ +ℕ p₁ *ℕ n₂ +ℕ_) (cong (m₁ *ℕ n₁ +ℕ m₂ *ℕ n₂ +ℕ_) (swap-center-+ℕ (p₂ *ℕ q₁) _ _ _)) ⟩
  (p₂ *ℕ n₁ +ℕ p₁ *ℕ n₂) +ℕ ((m₁ *ℕ n₁ +ℕ m₂ *ℕ n₂) +ℕ ((p₂ *ℕ q₁ +ℕ p₂ *ℕ n₂) +ℕ (p₁ *ℕ q₂ +ℕ p₁ *ℕ n₁)))
      ＝⟨ cong (p₂ *ℕ n₁ +ℕ p₁ *ℕ n₂ +ℕ_) (cong (m₁ *ℕ n₁ +ℕ m₂ *ℕ n₂ +ℕ_) (sym (cong₂ _+ℕ_ (*ℕ-distrib-left-+ℕ p₂ q₁ n₂) (*ℕ-distrib-left-+ℕ p₁ q₂ n₁)))) ⟩
  (p₂ *ℕ n₁ +ℕ p₁ *ℕ n₂) +ℕ ((m₁ *ℕ n₁ +ℕ m₂ *ℕ n₂) +ℕ ((p₂ *ℕ (q₁ +ℕ n₂)) +ℕ (p₁ *ℕ (q₂ +ℕ n₁))))
      ＝⟨ cong (p₂ *ℕ n₁ +ℕ p₁ *ℕ n₂ +ℕ_) (cong (m₁ *ℕ n₁ +ℕ m₂ *ℕ n₂ +ℕ_) (sym (cong₂ _+ℕ_ (cong (p₂ *ℕ_) n≈q) (cong (p₁ *ℕ_) (sym n≈q ∙ (comm-+ℕ n₁ _)))))) ⟩
  (p₂ *ℕ n₁ +ℕ p₁ *ℕ n₂) +ℕ ((m₁ *ℕ n₁ +ℕ m₂ *ℕ n₂) +ℕ ((p₂ *ℕ (n₁ +ℕ q₂)) +ℕ (p₁ *ℕ (q₁ +ℕ n₂))))
      ＝⟨ sym (assoc-+ℕ (p₂ *ℕ n₁ +ℕ p₁ *ℕ n₂) _ _) ⟩
  ((p₂ *ℕ n₁ +ℕ p₁ *ℕ n₂) +ℕ (m₁ *ℕ n₁ +ℕ m₂ *ℕ n₂)) +ℕ ((p₂ *ℕ (n₁ +ℕ q₂)) +ℕ (p₁ *ℕ (q₁ +ℕ n₂)))
      ＝⟨ cong (_+ℕ (p₂ *ℕ (n₁ +ℕ q₂) +ℕ p₁ *ℕ (q₁ +ℕ n₂))) (swap-center-+ℕ (p₂ *ℕ n₁) _ _ _) ⟩
  ((p₂ *ℕ n₁ +ℕ m₁ *ℕ n₁) +ℕ (p₁ *ℕ n₂ +ℕ m₂ *ℕ n₂)) +ℕ ((p₂ *ℕ (n₁ +ℕ q₂)) +ℕ (p₁ *ℕ (q₁ +ℕ n₂)))
      ＝⟨ cong (_+ℕ (p₂ *ℕ (n₁ +ℕ q₂) +ℕ p₁ *ℕ (q₁ +ℕ n₂))) (sym (cong₂ _+ℕ_ (*ℕ-distrib-right-+ℕ n₁ p₂ m₁) (*ℕ-distrib-right-+ℕ n₂ p₁ m₂))) ⟩
  (((p₂ +ℕ m₁) *ℕ n₁) +ℕ ((p₁ +ℕ m₂) *ℕ n₂)) +ℕ ((p₂ *ℕ (n₁ +ℕ q₂)) +ℕ (p₁ *ℕ (q₁ +ℕ n₂)))
      ＝⟨ cong (_+ℕ (p₂ *ℕ (n₁ +ℕ q₂) +ℕ p₁ *ℕ (q₁ +ℕ n₂))) (cong₂ _+ℕ_ (cong (_*ℕ n₁) (comm-+ℕ p₂ m₁ ∙ m≈p)) (cong (_*ℕ n₂) (sym m≈p))) ⟩
  (((p₁ +ℕ m₂) *ℕ n₁) +ℕ ((m₁ +ℕ p₂) *ℕ n₂)) +ℕ ((p₂ *ℕ (n₁ +ℕ q₂)) +ℕ (p₁ *ℕ (q₁ +ℕ n₂)))
      ＝⟨ cong (_+ℕ (p₂ *ℕ (n₁ +ℕ q₂) +ℕ p₁ *ℕ (q₁ +ℕ n₂))) (cong₂ _+ℕ_ (*ℕ-distrib-right-+ℕ n₁ p₁ m₂) (*ℕ-distrib-right-+ℕ n₂ m₁ p₂)) ⟩
  ((p₁ *ℕ n₁ +ℕ m₂ *ℕ n₁) +ℕ (m₁ *ℕ n₂ +ℕ p₂ *ℕ n₂)) +ℕ ((p₂ *ℕ (n₁ +ℕ q₂)) +ℕ (p₁ *ℕ (q₁ +ℕ n₂)))
      ＝⟨ cong (p₁ *ℕ n₁ +ℕ m₂ *ℕ n₁ +ℕ (m₁ *ℕ n₂ +ℕ p₂ *ℕ n₂) +ℕ_) (cong₂ _+ℕ_ (*ℕ-distrib-left-+ℕ p₂ n₁ q₂) (*ℕ-distrib-left-+ℕ p₁ q₁ n₂)) ⟩
  ((p₁ *ℕ n₁ +ℕ m₂ *ℕ n₁) +ℕ (m₁ *ℕ n₂ +ℕ p₂ *ℕ n₂)) +ℕ ((p₂ *ℕ n₁ +ℕ p₂ *ℕ q₂) +ℕ (p₁ *ℕ q₁ +ℕ p₁ *ℕ n₂))
      ＝⟨ swap-center-+ℕ (p₁ *ℕ n₁ +ℕ m₂ *ℕ n₁) _ _ _ ⟩
  ((p₁ *ℕ n₁ +ℕ m₂ *ℕ n₁) +ℕ (p₂ *ℕ n₁ +ℕ p₂ *ℕ q₂)) +ℕ ((m₁ *ℕ n₂ +ℕ p₂ *ℕ n₂) +ℕ (p₁ *ℕ q₁ +ℕ p₁ *ℕ n₂))
      ＝⟨ cong (_+ℕ (m₁ *ℕ n₂ +ℕ p₂ *ℕ n₂ +ℕ (p₁ *ℕ q₁ +ℕ p₁ *ℕ n₂))) (swap-center-+ℕ (p₁ *ℕ n₁) _ _ _) ⟩
  ((p₁ *ℕ n₁ +ℕ p₂ *ℕ n₁) +ℕ (m₂ *ℕ n₁ +ℕ p₂ *ℕ q₂)) +ℕ ((m₁ *ℕ n₂ +ℕ p₂ *ℕ n₂) +ℕ (p₁ *ℕ q₁ +ℕ p₁ *ℕ n₂))
      ＝⟨ cong (_+ℕ (m₁ *ℕ n₂ +ℕ p₂ *ℕ n₂ +ℕ (p₁ *ℕ q₁ +ℕ p₁ *ℕ n₂))) (cong₂ _+ℕ_ (comm-+ℕ (p₁ *ℕ n₁) _) (comm-+ℕ (m₂ *ℕ n₁) _)) ⟩
  ((p₂ *ℕ n₁ +ℕ p₁ *ℕ n₁) +ℕ (p₂ *ℕ q₂ +ℕ m₂ *ℕ n₁)) +ℕ ((m₁ *ℕ n₂ +ℕ p₂ *ℕ n₂) +ℕ (p₁ *ℕ q₁ +ℕ p₁ *ℕ n₂))
      ＝⟨ cong (_+ℕ (m₁ *ℕ n₂ +ℕ p₂ *ℕ n₂ +ℕ (p₁ *ℕ q₁ +ℕ p₁ *ℕ n₂))) (swap-center-+ℕ (p₂ *ℕ n₁) _ _ _) ⟩
  ((p₂ *ℕ n₁ +ℕ p₂ *ℕ q₂) +ℕ (p₁ *ℕ n₁ +ℕ m₂ *ℕ n₁)) +ℕ ((m₁ *ℕ n₂ +ℕ p₂ *ℕ n₂) +ℕ (p₁ *ℕ q₁ +ℕ p₁ *ℕ n₂))
      ＝⟨ cong (p₂ *ℕ n₁ +ℕ p₂ *ℕ q₂ +ℕ (p₁ *ℕ n₁ +ℕ m₂ *ℕ n₁) +ℕ_) (comm-+ℕ (m₁ *ℕ n₂ +ℕ p₂ *ℕ n₂) _) ⟩
  ((p₂ *ℕ n₁ +ℕ p₂ *ℕ q₂) +ℕ (p₁ *ℕ n₁ +ℕ m₂ *ℕ n₁)) +ℕ ((p₁ *ℕ q₁ +ℕ p₁ *ℕ n₂) +ℕ (m₁ *ℕ n₂ +ℕ p₂ *ℕ n₂))
      ＝⟨ swap-center-+ℕ ((p₂ *ℕ n₁ +ℕ p₂ *ℕ q₂)) _ _ _ ⟩
  ((p₂ *ℕ n₁ +ℕ p₂ *ℕ q₂) +ℕ (p₁ *ℕ q₁ +ℕ p₁ *ℕ n₂)) +ℕ ((p₁ *ℕ n₁ +ℕ m₂ *ℕ n₁) +ℕ (m₁ *ℕ n₂ +ℕ p₂ *ℕ n₂))
      ＝⟨ cong₂ _+ℕ_ (cong (p₂ *ℕ n₁ +ℕ p₂ *ℕ q₂ +ℕ_) (comm-+ℕ (p₁ *ℕ q₁) _)) (cong (_+ℕ (m₁ *ℕ n₂ +ℕ p₂ *ℕ n₂)) (comm-+ℕ (p₁ *ℕ n₁) _)) ⟩
  ((p₂ *ℕ n₁ +ℕ p₂ *ℕ q₂) +ℕ (p₁ *ℕ n₂ +ℕ p₁ *ℕ q₁)) +ℕ ((m₂ *ℕ n₁ +ℕ p₁ *ℕ n₁) +ℕ (m₁ *ℕ n₂ +ℕ p₂ *ℕ n₂))
      ＝⟨ cong₂ _+ℕ_ (swap-center-+ℕ (p₂ *ℕ n₁) _ _ _) (swap-center-+ℕ (m₂ *ℕ n₁) _ _ _) ⟩
  ((p₂ *ℕ n₁ +ℕ p₁ *ℕ n₂) +ℕ (p₂ *ℕ q₂ +ℕ p₁ *ℕ q₁)) +ℕ ((m₂ *ℕ n₁ +ℕ m₁ *ℕ n₂) +ℕ (p₁ *ℕ n₁ +ℕ p₂ *ℕ n₂))
      ＝⟨ cong₂ _+ℕ_ (cong (p₂ *ℕ n₁ +ℕ p₁ *ℕ n₂ +ℕ_) (comm-+ℕ (p₂ *ℕ q₂) _)) (cong (m₂ *ℕ n₁ +ℕ m₁ *ℕ n₂ +ℕ_) (comm-+ℕ (p₁ *ℕ n₁) _)) ⟩
  ((p₂ *ℕ n₁ +ℕ p₁ *ℕ n₂) +ℕ (p₁ *ℕ q₁ +ℕ p₂ *ℕ q₂)) +ℕ ((m₂ *ℕ n₁ +ℕ m₁ *ℕ n₂) +ℕ (p₂ *ℕ n₂ +ℕ p₁ *ℕ n₁))
      ＝⟨ assoc-+ℕ ((p₂ *ℕ n₁ +ℕ p₁ *ℕ n₂)) _ _ ⟩
  (p₂ *ℕ n₁ +ℕ p₁ *ℕ n₂) +ℕ ((p₁ *ℕ q₁ +ℕ p₂ *ℕ q₂) +ℕ ((m₂ *ℕ n₁ +ℕ m₁ *ℕ n₂) +ℕ (p₂ *ℕ n₂ +ℕ p₁ *ℕ n₁)))
      ＝⟨ cong (p₂ *ℕ n₁ +ℕ p₁ *ℕ n₂ +ℕ_) (sym (assoc-+ℕ ((p₁ *ℕ q₁ +ℕ p₂ *ℕ q₂)) _ _)) ⟩
  (p₂ *ℕ n₁ +ℕ p₁ *ℕ n₂) +ℕ (((p₁ *ℕ q₁ +ℕ p₂ *ℕ q₂) +ℕ (m₂ *ℕ n₁ +ℕ m₁ *ℕ n₂)) +ℕ (p₂ *ℕ n₂ +ℕ p₁ *ℕ n₁))
      ∎))