自然数

module natural-number where

open import identity-type
open import bottom-type
open import unit-type
open import negation
open import sum-type
open import sigma-type

定義

data ℕ : Set where
  zero : ℕ
  suc : ℕ → ℕ

`suc`の単射性

前者関数を定義する:

predℕ : ℕ → ℕ
predℕ zero = zero
predℕ (suc n) = n

定義より、predℕはsucの左逆写像となる。

pred-suc-id : ∀ n → predℕ (suc n) ＝ n
pred-suc-id _ = refl

前者関数を用いることで、sucが単射であることを示せる:

suc-injective : ∀ {m n : ℕ} → suc m ＝ suc n → m ＝ n
suc-injective e = cong predℕ e

`zero`と`suc`は異なる

zeroとsuc nが異なることは、Agdaのパターンマッチによって示すことができる:

zero-not-equal-to-suc : ∀ {n} → zero ＝ suc n → ⊥
zero-not-equal-to-suc ()

transportを用いた証明を以下に記す:

zero-not-equal-to-suc′ : ∀ {n} → zero ＝ suc n → ⊥
zero-not-equal-to-suc′ e = transport P e unit
  where
    P : ℕ → Set
    P zero = Unit
    P (suc _) = ⊥

加法

加法を第一引数に対して帰納的に定義する。

infixl 60 _+ℕ_
_+ℕ_ : ℕ → ℕ → ℕ
zero +ℕ n = n
suc m +ℕ n = suc (m +ℕ n)

加法が左単位元と右単位元を持つことを示す:

left-unit-+ℕ : ∀ n → zero +ℕ n ＝ n
left-unit-+ℕ _ = refl

right-unit-+ℕ : ∀ n → n +ℕ zero ＝ n
right-unit-+ℕ zero = refl
right-unit-+ℕ (suc n) = cong suc (right-unit-+ℕ n)

このように、+ℕの定義よりzeroが左単位元であることは即座に分かる。すなわち、nに対するパターンマッチを行わずにそのままreflを使うことでzero +ℕ n ＝ nを示すことができる。一方、zeroが+ℕの右単位元であることを示すには帰納法を使う必要がある。

加法が結合的であることを示す:

assoc-+ℕ : ∀ x y z → (x +ℕ y) +ℕ z ＝ x +ℕ (y +ℕ z)
assoc-+ℕ zero y z = refl
assoc-+ℕ (suc x) y z = cong suc (assoc-+ℕ x y z)

これもxに対する帰納法を用いて証明している。

定義より、suc m +ℕ nがsuc (m +ℕ n)と等しいことは分かっている。しかし、m +ℕ suc nがsuc (m +ℕ n)と等しいことは帰納法を用いて証明する必要がある:

+ℕ-suc : ∀ m n → m +ℕ suc n ＝ suc (m +ℕ n)
+ℕ-suc zero n = refl
+ℕ-suc (suc m) n = cong suc (+ℕ-suc m n)

この+ℕ-sucを使うことで、加法が可換であることを示せる:

comm-+ℕ : ∀ m n → m +ℕ n ＝ n +ℕ m
comm-+ℕ zero zero = refl
comm-+ℕ zero (suc n) = cong suc (sym (right-unit-+ℕ n))
comm-+ℕ (suc m) zero = cong suc (right-unit-+ℕ m)
comm-+ℕ (suc m) (suc n) = cong suc e
  where
    e : m +ℕ suc n ＝ n +ℕ suc m
    e =
        m +ℕ suc n
      ＝⟨ +ℕ-suc m n ⟩
        suc (m +ℕ n)
      ＝⟨ cong suc (comm-+ℕ m n) ⟩
        suc (n +ℕ m)
      ＝⟨ sym (+ℕ-suc n m) ⟩
        n +ℕ suc m
      ∎

以下の3つの定理は、上記で証明した結合性と可換性を組み合わせただけのものであるが、形式的に行う数学（すなわち、どんな「当たり前」のことでもちゃんと証明を書かなくてはならないような状況）では意外と便利である。

swap-left-+ℕ : ∀ x y z → x +ℕ (y +ℕ z) ＝ y +ℕ (x +ℕ z)
swap-left-+ℕ x y z =
    x +ℕ (y +ℕ z)
  ＝⟨ sym (assoc-+ℕ x y z) ⟩
    (x +ℕ y) +ℕ z
  ＝⟨ cong (_+ℕ z) (comm-+ℕ x y) ⟩
    (y +ℕ x) +ℕ z
  ＝⟨ assoc-+ℕ y x z ⟩
    y +ℕ (x +ℕ z)
  ∎

swap-right-+ℕ : ∀ x y z → (x +ℕ y) +ℕ z ＝ (x +ℕ z) +ℕ y
swap-right-+ℕ x y z =
    (x +ℕ y) +ℕ z
  ＝⟨ assoc-+ℕ x y z ⟩
    x +ℕ (y +ℕ z)
  ＝⟨ cong (x +ℕ_) (comm-+ℕ y z) ⟩
    x +ℕ (z +ℕ y)
  ＝⟨ sym (assoc-+ℕ x z y) ⟩
    (x +ℕ z) +ℕ y
  ∎

swap-center-+ℕ : ∀ w x y z → (w +ℕ x) +ℕ (y +ℕ z) ＝ (w +ℕ y) +ℕ (x +ℕ z)
swap-center-+ℕ w x y z =
  (w +ℕ x) +ℕ (y +ℕ z)
    ＝⟨ assoc-+ℕ w x (y +ℕ z) ⟩
  w +ℕ (x +ℕ (y +ℕ z))
    ＝⟨ cong (w +ℕ_) (sym (assoc-+ℕ x y z)) ⟩
  w +ℕ ((x +ℕ y) +ℕ z)
    ＝⟨ cong (w +ℕ_) (cong (_+ℕ z) (comm-+ℕ x y)) ⟩
  w +ℕ ((y +ℕ x) +ℕ z)
    ＝⟨ cong (w +ℕ_) (assoc-+ℕ y x z) ⟩
  w +ℕ (y +ℕ (x +ℕ z))
    ＝⟨ sym (assoc-+ℕ w y (x +ℕ z)) ⟩
  (w +ℕ y) +ℕ (x +ℕ z)
    ∎

cancel-left-+ℕ : ∀ x {a b} → x +ℕ a ＝ x +ℕ b → a ＝ b
cancel-left-+ℕ zero    e = e
cancel-left-+ℕ (suc x) e = cancel-left-+ℕ x (suc-injective e)

cancel-right-+ℕ : ∀ x {a b} → a +ℕ x ＝ b +ℕ x → a ＝ b
cancel-right-+ℕ x {a} {b} e = cancel-left-+ℕ x
  (
    x +ℕ a
        ＝⟨ comm-+ℕ x a ⟩
    a +ℕ x
        ＝⟨ e ⟩
    b +ℕ x
        ＝⟨ comm-+ℕ b x ⟩
    x +ℕ b
        ∎
  )

乗法

乗法を定義する。

infixl 70 _*ℕ_
_*ℕ_ : ℕ → ℕ → ℕ
zero  *ℕ n = zero
suc m *ℕ n = n +ℕ m *ℕ n

zeroとn : ℕの積はzeroとなる:

0*ℕ : ∀ n → zero *ℕ n ＝ zero
0*ℕ _ = refl

*ℕ0 : ∀ n → n *ℕ zero ＝ zero
*ℕ0 zero    = refl
*ℕ0 (suc n) = *ℕ0 n

suc m *ℕ n ＝ n +ℕ m *ℕ nであることは定義より分かる。一方、m *ℕ suc n ＝ m +ℕ m *ℕ nは帰納法によって証明される:

*ℕ-suc : ∀ m n → m *ℕ suc n ＝ m +ℕ m *ℕ n
*ℕ-suc zero    n = refl
*ℕ-suc (suc m) n = cong suc (trans k (swap-left-+ℕ n m (m *ℕ n)))
  where
    k : n +ℕ m *ℕ suc n ＝ n +ℕ (m +ℕ m *ℕ n)
    k = cong (n +ℕ_) (*ℕ-suc m n)

これにより、乗法が可換であることを示せる:

comm-*ℕ : ∀ m n → m *ℕ n ＝ n *ℕ m
comm-*ℕ zero    zero    = refl
comm-*ℕ zero    (suc n) = sym (*ℕ0 n)
comm-*ℕ (suc m) zero    = *ℕ0 m
comm-*ℕ (suc m) (suc n) = cong suc e
  where
    e : n +ℕ m *ℕ suc n ＝ m +ℕ n *ℕ suc m
    e =
      n +ℕ m *ℕ suc n     ＝⟨ cong (n +ℕ_) (*ℕ-suc m n) ⟩
      n +ℕ (m +ℕ m *ℕ n)  ＝⟨ swap-left-+ℕ n m (m *ℕ n) ⟩
      m +ℕ (n +ℕ m *ℕ n)  ＝⟨ cong (λ a → m +ℕ (n +ℕ a)) (comm-*ℕ m n) ⟩
      m +ℕ (n +ℕ n *ℕ m)  ＝⟨ cong (m +ℕ_) (sym (*ℕ-suc n m)) ⟩
      m +ℕ n *ℕ suc m     ∎

乗法は加法に分配する:

*ℕ-distrib-left-+ℕ : ∀ x a b → x *ℕ (a +ℕ b) ＝ x *ℕ a +ℕ x *ℕ b
*ℕ-distrib-left-+ℕ zero    a b = refl
*ℕ-distrib-left-+ℕ (suc x) a b =
  (a +ℕ b) +ℕ x *ℕ (a +ℕ b)
      ＝⟨ cong (λ r → a +ℕ b +ℕ r) (*ℕ-distrib-left-+ℕ x a b) ⟩
  (a +ℕ b) +ℕ (x *ℕ a +ℕ x *ℕ b)
      ＝⟨ swap-center-+ℕ a b (x *ℕ a) (x *ℕ b) ⟩
  (a +ℕ x *ℕ a) +ℕ (b +ℕ x *ℕ b)
      ∎

*ℕ-distrib-right-+ℕ : ∀ x a b → (a +ℕ b) *ℕ x ＝ a *ℕ x +ℕ b *ℕ x
*ℕ-distrib-right-+ℕ x a b =
  (a +ℕ b) *ℕ x
      ＝⟨ comm-*ℕ (a +ℕ b) x ⟩
  x *ℕ (a +ℕ b)
      ＝⟨ *ℕ-distrib-left-+ℕ x a b ⟩
  x *ℕ a +ℕ x *ℕ b
      ＝⟨ cong₂ _+ℕ_ (comm-*ℕ x a) (comm-*ℕ x b) ⟩
  a *ℕ x +ℕ b *ℕ x
      ∎

乗法が結合的であることを示す:

assoc-*ℕ : ∀ x y z → (x *ℕ y) *ℕ z ＝ x *ℕ (y *ℕ z)
assoc-*ℕ zero    y z = refl
assoc-*ℕ (suc x) y z =
  (y +ℕ x *ℕ y) *ℕ z
      ＝⟨ *ℕ-distrib-right-+ℕ z y (x *ℕ y) ⟩
  y *ℕ z +ℕ (x *ℕ y) *ℕ z
      ＝⟨ cong (y *ℕ z +ℕ_) (assoc-*ℕ x y z) ⟩
  y *ℕ z +ℕ x *ℕ (y *ℕ z)
      ∎

自然数の等価性は決定可能である

任意の2つの自然数が与えられたとき、それらが等しいかどうかは決定可能である:

Discrete-ℕ : Discrete ℕ
Discrete-ℕ zero zero = inl refl
Discrete-ℕ zero (suc n) = inr zero-not-equal-to-suc
Discrete-ℕ (suc m) zero = inr λ e → zero-not-equal-to-suc (sym e)
Discrete-ℕ (suc m) (suc n) with Discrete-ℕ m n
... | inl e = inl (cong suc e)
... | inr f = inr (λ e → f (suc-injective e))

偶数と奇数

data isEven : ℕ → Set where
  isEven-z : isEven zero
  isEven-ss : ∀ {n} → isEven n → isEven (suc (suc n))

data isOdd : ℕ → Set where
  isOdd-o : isOdd (suc zero)
  isOdd-ss : ∀ {n} → isOdd n → isOdd (suc (suc n))

任意の自然数は偶数か奇数である

任意の自然数について、それが偶数であるか奇数であるか、判定することができる:

even-or-odd : ∀ n → isEven n + isOdd n
even-or-odd zero = inl isEven-z
even-or-odd (suc zero) = inr isOdd-o
even-or-odd (suc (suc n)) with even-or-odd n
... | inl e = inl (isEven-ss e)
... | inr o = inr (isOdd-ss o)

偶数でない自然数は奇数であり、奇数でない自然数は偶数である:

¬isEven→isOdd : ∀ n → ¬ isEven n → isOdd n
¬isEven→isOdd n x with even-or-odd n
... | inl e = absurd (x e)
... | inr o = o

¬isOdd→isEven : ∀ n → ¬ isOdd n → isEven n
¬isOdd→isEven n x with even-or-odd n
... | inl e = e
... | inr o = absurd (x o)

偶数かつ奇数であるような自然数は存在しない

ある自然数nが偶数であるとき、その前者の前者もまた偶数である:

isEven-pp : ∀ {n} → isEven n → isEven (predℕ (predℕ n))
isEven-pp isEven-z = isEven-z
isEven-pp (isEven-ss e) = e

ある自然数nが奇数であるとき、それは1であるか、nの前者の前者もまた奇数となる:

isOdd-pp : ∀ {n} → isOdd n → (n ＝ suc zero) + isOdd (predℕ (predℕ n))
isOdd-pp isOdd-o = inl refl
isOdd-pp (isOdd-ss o) = inr o

偶数かつ奇数であるような自然数が与えられたとき、矛盾が生じる:

not-both-even-and-odd : ∀ n → isEven n → isOdd n → ⊥
not-both-even-and-odd zero _ ()
not-both-even-and-odd (suc zero) ()
not-both-even-and-odd (suc (suc n)) e o with isOdd-pp o
... | inl x = absurd (zero-not-equal-to-suc (sym (suc-injective x)))
... | inr o′ = not-both-even-and-odd n (isEven-pp e) o′

not-both-even-and-oddと¬isEven→isOdd、そして¬isOdd→isEvenによって、「偶数である」と「奇数ではない」は論理的同値となり、「奇数である」と「偶数ではない」は論理的同値となる。

偶数と奇数の決定可能性

したがって、「偶数である」ことと「奇数である」ことはどちらも決定可能である:

Decidable-isEven : ∀ n → Decidable (isEven n)
Decidable-isEven n with even-or-odd n
... | inl e = inl e
... | inr o = inr (λ e → not-both-even-and-odd n e o)

Decidable-isOdd : ∀ n → Decidable (isOdd n)
Decidable-isOdd n with even-or-odd n
... | inl e = inr (λ o → not-both-even-and-odd n e o)
... | inr o = inl o

順序

data _≤ℕ_ : ℕ → ℕ → Set where
  z≤n : ∀ n → zero ≤ℕ n
  s≤s : ∀ {m n} → m ≤ℕ n → suc m ≤ℕ suc n

_<ℕ_ : ℕ → ℕ → Set
m <ℕ n = suc m ≤ℕ n

refl-≤ℕ : ∀ n → n ≤ℕ n
refl-≤ℕ zero = z≤n zero
refl-≤ℕ (suc n) = s≤s (refl-≤ℕ n)

n≤s : ∀ {m n} → m ≤ℕ n → m ≤ℕ suc n
n≤s (z≤n n)   = z≤n (suc n)
n≤s (s≤s m≤n) = s≤s (n≤s m≤n)

¬-s≤z : ∀ n → ¬ (suc n ≤ℕ zero)
¬-s≤z n ()

p≤p : ∀ {m n} → m ≤ℕ n → predℕ m ≤ℕ predℕ n
p≤p (z≤n n) = z≤n (predℕ n)
p≤p (s≤s x) = x

順序は決定可能である:

Decidable-≤ℕ : ∀ m n → Decidable (m ≤ℕ n)
Decidable-≤ℕ zero    n    = inl (z≤n n)
Decidable-≤ℕ (suc m) zero = inr (¬-s≤z m)
Decidable-≤ℕ (suc m) (suc n) with Decidable-≤ℕ m n
... | inl m≤n = inl (s≤s m≤n)
... | inr f   = inr (λ x → f (p≤p x))

m ≤ℕ nでないならばn <ℕ mである:

¬≤→< : ∀ m n → ¬ (m ≤ℕ n) → n <ℕ m
¬≤→< zero    n       f = absurd (f (z≤n n))
¬≤→< (suc m) zero    f = s≤s (z≤n m)
¬≤→< (suc m) (suc n) f = s≤s (¬≤→< m n (λ z → f (s≤s z)))

そして、その逆も成り立つ:

<→¬≤ : ∀ m n → n <ℕ m → m ≤ℕ n → ⊥
<→¬≤ _ _ n<m (z≤n x)   = ¬-s≤z x n<m
<→¬≤ _ _ n<m (s≤s m≤n) = <→¬≤ _ _ (p≤p n<m) m≤n

また、m ≤ℕ nと「m ＝ nまたはm <ℕ n」は論理的同値である。

≤→＝+< : ∀ {m n} → m ≤ℕ n → (m ＝ n) + (m <ℕ n)
≤→＝+< (z≤n zero)    = inl refl
≤→＝+< (z≤n (suc n)) = inr (s≤s (z≤n n))
≤→＝+< (s≤s m≤n)     with ≤→＝+< m≤n
... | inl e   = inl (cong suc e)
... | inr m<n = inr (s≤s m<n)

＝+<→≤ : ∀ {m n} → (m ＝ n) + (m <ℕ n) → m ≤ℕ n
＝+<→≤ {m} (inl e)   = transport (m ≤ℕ_) e (refl-≤ℕ m)
＝+<→≤     (inr m<n) = p≤p (n≤s m<n)

<→≤ : ∀ {m n} → m <ℕ n → m ≤ℕ n
<→≤ m<n = ＝+<→≤ (inr m<n)

decide-≤-or-> : ∀ m n → (m ≤ℕ n) + (n <ℕ m)
decide-≤-or-> m n with Decidable-≤ℕ m n
... | inl m≤n = inl m≤n
... | inr ¬m≤n = inr (¬≤→< m n ¬m≤n)

+ℕ-resp-≤ℕ-left : ∀ x {a b} → a ≤ℕ b → x +ℕ a ≤ℕ x +ℕ b
+ℕ-resp-≤ℕ-left zero    a≤b = a≤b
+ℕ-resp-≤ℕ-left (suc x) a≤b = s≤s (+ℕ-resp-≤ℕ-left x a≤b)

+ℕ-resp-≤ℕ-right : ∀ x {a b} → a ≤ℕ b → a +ℕ x ≤ℕ b +ℕ x
+ℕ-resp-≤ℕ-right x {a} {b} a≤b =
  transport
    (λ v → (a +ℕ x) ≤ℕ v)
    (comm-+ℕ x b)
    (transport (λ v → v ≤ℕ (x +ℕ b)) (comm-+ℕ x a) (+ℕ-resp-≤ℕ-left x a≤b))

帰納法

recℕ : (P : Set) → P → (ℕ → P → P) → ℕ → P
recℕ P P0 Pstep zero = P0
recℕ P P0 Pstep (suc n) = Pstep n (recℕ P P0 Pstep n)

indℕ : (P : ℕ → Set)
  → P zero
  → (∀ n → P n → P (suc n))
  → (n : ℕ)
  → P n
indℕ P P0 Pstep zero = P0
indℕ P P0 Pstep (suc n) = Pstep n (indℕ P P0 Pstep n)

data _≤′ℕ_ : ℕ → ℕ → Set where
  n≤′n : ∀ n → n ≤′ℕ n
  n≤′s : ∀ {m n} → m ≤′ℕ n → m ≤′ℕ suc n

_<′ℕ_ : ℕ → ℕ → Set
m <′ℕ n = suc m ≤′ℕ n

z≤′n : ∀ n → zero ≤′ℕ n
z≤′n zero = n≤′n zero
z≤′n (suc n) = n≤′s (z≤′n n)

s≤′s : ∀ {m n} → m ≤′ℕ n → suc m ≤′ℕ suc n
s≤′s (n≤′n n)   = n≤′n (suc n)
s≤′s (n≤′s m≤n) = n≤′s (s≤′s m≤n)

≤→≤′ : ∀ {m n} → m ≤ℕ n → m ≤′ℕ n
≤→≤′ (z≤n n)   = z≤′n n
≤→≤′ (s≤s m≤n) = s≤′s (≤→≤′ m≤n)

≤′→≤ : ∀ {m n} → m ≤′ℕ n → m ≤ℕ n
≤′→≤ (n≤′n n)   = refl-≤ℕ n
≤′→≤ (n≤′s m≤n) = n≤s (≤′→≤ m≤n)

p≤′p-helper : ∀ m n → m ≤′ℕ n → predℕ m ≤′ℕ n
p≤′p        : ∀ m n → m ≤′ℕ n → predℕ m ≤′ℕ predℕ n

p≤′p-helper zero    _       x = x
p≤′p-helper (suc m) (suc n) x = n≤′s (p≤′p (suc m) (suc n) x)

p≤′p m       _ (n≤′n _) = n≤′n (predℕ m)
p≤′p zero    _ (n≤′s x) = x
p≤′p (suc m) _ (n≤′s x) = p≤′p-helper (suc m) _ x

module _ (P : ℕ → Set) (f : ∀ n → (∀ m → m <′ℕ n → P m) → P n) where
  comp-indℕ        : (n : ℕ) → P n
  comp-indℕ-helper : (m : ℕ) → (n : ℕ) → m ≤′ℕ n → P m

  comp-indℕ zero    = f zero (λ m ())
  comp-indℕ (suc n) =
    f (suc n) λ m x → comp-indℕ-helper m n (p≤′p (suc m) (suc n) x)

  comp-indℕ-helper m n       (n≤′n _) = comp-indℕ n
  comp-indℕ-helper m (suc n) (n≤′s x) = comp-indℕ-helper m n x

減法

subℕ : ∀ {m n} → m ≤ℕ n → Σ[ d ∈ ℕ ] (m +ℕ d ＝ n)
subℕ (z≤n n)   = n , refl
subℕ (s≤s m≤n) with subℕ m≤n
... | d , e = d , cong suc e

≤+→≤ : ∀ {m n} → Σ[ d ∈ ℕ ] (m +ℕ d ＝ n) → m ≤ℕ n
≤+→≤ {m = zero}  {n = n}     _       = z≤n n
≤+→≤ {m = suc m} {n = suc n} (d , e) = s≤s (≤+→≤ (d , suc-injective e))

除法

divℕ : ∀ m n → zero <ℕ n → Σ[ q ∈ ℕ ] Σ[ r ∈ ℕ ] (m ＝ q *ℕ n +ℕ r) × (r <ℕ n)
divℕ m′ n 0<n = comp-indℕ P f m′
  where
    P : ℕ → Set
    P m = Σ[ q ∈ ℕ ] Σ[ r ∈ ℕ ] (m ＝ q *ℕ n +ℕ r) × (r <ℕ n)

    f : ∀ m → (∀ p → p <′ℕ m → P p) → P m
    f m prev with decide-≤-or-> n m
    ... | inr m<n = zero , m , refl , m<n
    ... | inl n≤m = suc (k .fst) , k .snd .fst ,
                    ( m
                        ＝⟨ sym e ⟩
                      n +ℕ d
                        ＝⟨ cong (n +ℕ_) (k .snd .snd .fst) ⟩
                      n +ℕ (k .fst *ℕ n +ℕ k .snd .fst)
                        ＝⟨ sym (assoc-+ℕ n _ _) ⟩
                      (n +ℕ k .fst *ℕ n) +ℕ k .snd .fst
                        ＝⟨ refl ⟩
                      suc (k .fst) *ℕ n +ℕ k .snd .fst
                        ∎
                    ) , k .snd .snd .snd
      where
        d : ℕ
        d = subℕ n≤m .fst

        e : n +ℕ d ＝ m
        e = subℕ n≤m .snd

        d<m : d <ℕ m
        d<m = transport (d <ℕ_) e (+ℕ-resp-≤ℕ-right d 0<n)

        k = prev d (≤→≤′ d<m)

最大値と最小値

maxℕ : ℕ → ℕ → ℕ
maxℕ zero    n       = n
maxℕ (suc m) zero    = suc m
maxℕ (suc m) (suc n) = suc (maxℕ m n)

minℕ : ℕ → ℕ → ℕ
minℕ zero    _       = zero
minℕ (suc m) zero    = zero
minℕ (suc m) (suc n) = suc (minℕ m n)

≤→max-ℕ : ∀ {m n} → m ≤ℕ n → maxℕ m n ＝ n
≤→max-ℕ (z≤n _)   = refl
≤→max-ℕ (s≤s m≤n) = cong suc (≤→max-ℕ m≤n)

≤→min-ℕ : ∀ {m n} → m ≤ℕ n → minℕ m n ＝ m
≤→min-ℕ (z≤n _)   = refl
≤→min-ℕ (s≤s m≤n) = cong suc (≤→min-ℕ m≤n)

max→≤-ℕ : ∀ {m n} → maxℕ m n ＝ n → m ≤ℕ n
max→≤-ℕ {zero}  {n}     _ = z≤n n
max→≤-ℕ {suc m} {suc n} e = s≤s (max→≤-ℕ (suc-injective e))

min→≤-ℕ : ∀ {m n} → minℕ m n ＝ m → m ≤ℕ n
min→≤-ℕ {zero}  {n}     _ = z≤n n
min→≤-ℕ {suc m} {suc n} e = s≤s (min→≤-ℕ (suc-injective e))

comm-maxℕ : ∀ m n → maxℕ m n ＝ maxℕ n m
comm-maxℕ zero    zero    = refl
comm-maxℕ zero    (suc _) = refl
comm-maxℕ (suc _) zero    = refl
comm-maxℕ (suc m) (suc n) = cong suc (comm-maxℕ m n)

comm-minℕ : ∀ m n → minℕ m n ＝ minℕ n m
comm-minℕ zero    zero    = refl
comm-minℕ zero    (suc _) = refl
comm-minℕ (suc _) zero    = refl
comm-minℕ (suc m) (suc n) = cong suc (comm-minℕ m n)

idemp-maxℕ : ∀ n → maxℕ n n ＝ n
idemp-maxℕ n = ≤→max-ℕ (refl-≤ℕ n)

idemp-minℕ : ∀ n → minℕ n n ＝ n
idemp-minℕ n = ≤→min-ℕ (refl-≤ℕ n)

either-maxℕ : ∀ m n → (maxℕ m n ＝ m) + (maxℕ m n ＝ n)
either-maxℕ m n with decide-≤-or-> m n
... | inl m≤n = inr (≤→max-ℕ m≤n)
... | inr n<m = inl (comm-maxℕ m n ∙ ≤→max-ℕ (<→≤ n<m))

either-minℕ : ∀ m n → (minℕ m n ＝ m) + (minℕ m n ＝ n)
either-minℕ m n with decide-≤-or-> m n
... | inl m≤n = inl (≤→min-ℕ m≤n)
... | inr n<m = inr (comm-minℕ m n ∙ ≤→min-ℕ (<→≤ n<m))

left-unit-maxℕ : ∀ n → maxℕ zero n ＝ n
left-unit-maxℕ _ = refl

right-unit-maxℕ : ∀ n → maxℕ n zero ＝ n
right-unit-maxℕ n = comm-maxℕ n zero ∙ ≤→max-ℕ (z≤n n)

（right-unit-maxℕはパターンマッチでも簡単に示すことができる。）

assoc-maxℕ : ∀ x y z → maxℕ (maxℕ x y) z ＝ maxℕ x (maxℕ y z)
assoc-maxℕ zero    _       _       = refl
assoc-maxℕ (suc _) zero    _       = refl
assoc-maxℕ (suc _) (suc _) zero    = refl
assoc-maxℕ (suc x) (suc y) (suc z) = cong suc (assoc-maxℕ x y z)

maxℕ-is-upper-bound-left : ∀ m n → m ≤ℕ maxℕ m n
maxℕ-is-upper-bound-left m n with either-maxℕ m n
... | inl e = transport (m ≤ℕ_) (sym e) (refl-≤ℕ m)
... | inr e = transport (m ≤ℕ_) (sym e) (max→≤-ℕ e)

自然数

定義

sucの単射性

zeroとsucは異なる

加法

乗法