カントールの対関数

cantor_pairling.lean

import Mathlib.Tactic

-- `Nat.succ` を `x + 1` に変換するのが面倒なので導入
@[simp]
theorem nat_succ_eq_add_one {x : Nat} : Nat.succ x = x + 1 := by rfl

-- `Nat.zero` を `0` に変換するのが面倒なので導入
@[simp]
theorem nat_zero_eq_zero : Nat.zero = 0 := by rfl

/-- `0` から `n` までの自然数の和.
多項式として表現する必要はないので，返り値は自然数. -/
def sum (n : ℕ) : ℕ :=
  match n with
  | 0 => 0
  | n + 1 => (n + 1) + sum n

@[simp]
theorem summ_zero_iff_zero {n : ℕ} : sum n = 0 ↔ n = 0 := by
  constructor <;> intro h
  case mp =>
    induction' n with n _ih <;> simp at *
    simp [sum] at h
  case mpr =>
    rw [h, sum]

/-- カントールの対関数 -/
def pair : ℕ × ℕ → ℕ
  | (m, n) => sum (m + n) + m

@[simp]
theorem pair_zero : pair 0 = 0 := by rfl

/-- カントールの対関数の逆関数 -/
def unpair : ℕ → ℕ × ℕ
  | 0 => (0, 0)
  | x + 1 =>
    let (m, n) := unpair x
    if n = 0 then
      (0, m + 1)
    else
      (m + 1, n - 1)

@[simp]
theorem unpair_zero : unpair 0 = 0 := by rfl

theorem pair_unpair_eq_id (x : ℕ) : pair (unpair x) = x := by
  -- `x` に対する帰納法を使う
  match x with
  | 0 =>
    simp
  | x + 1 =>
    -- 帰納法の仮定
    have ih := pair_unpair_eq_id x

    -- まず `unpair` の定義を展開しよう．
    dsimp [unpair]
    split_ifs

    -- 見やすさのために `(m, n) := unpair x` とおく．
    all_goals
      set p := unpair x with ph
      set m := p.fst with mh
      set n := p.snd with nh

    -- `n = 0` の場合,
    case pos h =>
      -- 次を示せばよい．
      show pair (0, m + 1) = x + 1

      -- `pair` の定義を展開して，帰納法の仮定を利用すれば示せる.
      rw [pair, ←ih, pair]
      simp [←ph, ←mh, ←nh, h, sum]
      ac_rfl

    -- `n ≠ 0` の場合,
    case neg h =>
      -- 次を示せばよい．
      show pair (m + 1, n - 1) = x + 1

      -- `pair` の定義を展開して，帰納法の仮定を利用すれば示せる．
      rw [pair, ←ih, pair]
      simp [←ph, ←mh, ←nh]
      rw [show m + 1 + (n - 1) = m + n from by omega]
      ac_rfl

theorem unpair_pair_eq_id (m n : ℕ) : unpair (pair (m, n)) = (m, n) := by
  -- `x = pair (m, n)` として `x` に対する帰納法を利用する
  induction' h : pair (m, n) with x ih generalizing m n
  all_goals simp at *

  -- `pair (m, n) = 0` のとき
  case zero =>
    -- `pair` の定義から明らか．
    simp [pair] at h
    aesop

  -- `pair (m, n) = x + 1` のとき
  case succ =>
    -- `m` がゼロかそうでないかで場合分けする
    match m with

    -- `m = 0` のとき
    | 0 =>
      -- `pair (0, n) = x + 1` により `n > 0` が成り立つ.
      have npos : n > 0 := by
        by_contra!; simp at this
        simp [this] at h
        contradiction

      -- よって `n = (n - 1) + 1` であり，
      replace npos : n = (n - 1) + 1 := by omega
      have : sum n = sum (n - 1) + n := by
        nth_rw 1 [npos]
        dsimp [sum]
        omega

      -- `pair (n - 1, 0) = x` が成り立つ.
      replace : pair (n - 1, 0) = x := by
        dsimp [pair] at h ⊢
        simp at h
        rw [this] at h
        omega

      -- 後は帰納法の仮定から従う.
      specialize ih (n-1) 0 this
      simp [unpair, ih]
      symm; assumption

    -- `m = m' + 1` のとき
    | m' + 1 =>
      -- `pair` の定義から `pair (m', n + 1) = x` が成り立つ．
      have : pair (m', n + 1) = x := by
        simp [pair] at h ⊢
        rw [show m' + 1 + n = m' + (n + 1) from by ac_rfl] at h
        omega

      -- 後は帰納法の仮定から従う．
      specialize ih m' (n + 1) this
      simp [unpair, ih]