-- Uncountability of the Dedekind reals - Digits
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Cumulus.Real.Uncountable.Digits
import Nat.Pow
import Set

-- The membership bit of n in X, represented as a von Neumann natural. The
-- bounded separation is either {1} or empty, so its union is respectively
-- 1 or 0, so the construction stays inside set theory.
def binaryDigitSet (X n : Set) : Set :=
  { d ∈ {1} | n ∈ X }
def binaryDigitRaw (X n : Set) : Set := ⋃(binaryDigitSet(X, n))

theorem binaryDigitRaw.one (X n : Set)
  requires member : n ∈ X
  shows binaryDigitRaw(X, n) = 1
proof
  unfold binaryDigitRaw
  ext x
  simp [set.union, binaryDigitSet, singleton.membership, member]

theorem binaryDigitRaw.zero (X n : Set)
  requires missing : ¬(n ∈ X)
  shows binaryDigitRaw(X, n) = 0
proof
  unfold binaryDigitRaw
  ext x
  simp [set.union, binaryDigitSet, singleton.membership, missing, nat.zero, set.empty]

theorem binaryDigitRaw.cases (X n : Set)
  shows binaryDigitRaw(X, n) = 0 ∨ binaryDigitRaw(X, n) = 1
proof
  have membershipCases : n ∈ X ∨ ¬(n ∈ X) by tauto
  cases membershipCases with member | missing
  . right
    exact binaryDigitRaw.one with member
  . left
    exact binaryDigitRaw.zero with missing

instance binaryDigitRaw.natural (X n : Set)
  shows Nat(binaryDigitRaw(X, n))
proof
  have cases := binaryDigitRaw.cases at X, n
  cases cases with zero | one
  . rw zero
    exact Naturals.constructor.zero
  . rw one
    typecheck

def binaryDigit (X n : Set) : Nat := binaryDigitRaw(X, n)

theorem binaryDigit.zero (X n : Set)
  requires missing : ¬(n ∈ X)
  shows binaryDigit(X, n) = 0
proof
  unfold binaryDigit
  exact binaryDigitRaw.zero with missing

theorem binaryDigit.one (X n : Set)
  requires member : n ∈ X
  shows binaryDigit(X, n) = 1
proof
  unfold binaryDigit
  exact binaryDigitRaw.one with member

theorem binaryDigit.cases (X n : Set)
  shows binaryDigit(X, n) = 0 ∨ binaryDigit(X, n) = 1
proof
  have cases := binaryDigitRaw.cases at X, n
  cases cases with zero | one
  . left
    simp [binaryDigit]
  . right
    simp [binaryDigit]

theorem binaryDigit.natural (X n : Set)
  shows Nat(binaryDigit(X, n))
proof
  unfold binaryDigit
  exact binaryDigitRaw.natural

-- Base-four prefixes with digits 0 and 2. The gap between those digits is
-- what makes the eventual real recover every membership bit uniquely.
def cantorPrefix (X : Set, n : Nat) → Nat
  | X, zero => 0
  | X, succ(n) => 4 * cantorPrefix(X, n) + 2 * binaryDigit(X, n)

theorem cantorPrefix.zero (X : Set)
  shows cantorPrefix(X, 0) = 0
proof
  simp [cantorPrefix]

theorem cantorPrefix.succ (X : Set, n : Nat)
  shows cantorPrefix(X, succ(n)) =
    4 * cantorPrefix(X, n) + 2 * binaryDigit(X, n)
proof
  simp [cantorPrefix]

theorem cantorPrefix.natural (X : Set, n : Nat)
  shows Nat(cantorPrefix(X, n))
proof
  induction n
  | zero =>
    have shape := cantorPrefix.zero at X
    rw shape
    typecheck
  | succ(k) using ih =>
    have shape := cantorPrefix.succ at X, k
    rw shape
    have digitNatural := binaryDigit.natural at X, k
    have rightNatural := mul.closed at binaryDigit(X, k), 2 with digitNatural
    exact add.closed with rightNatural

theorem pow.four_nonzero (n : Nat)
  shows 4 ^ n ≠ 0
proof
  induction n
  | zero =>
    have shape := pow.zero at 4
    rw shape
    intro equal
    have impossible := Naturals.disjoint.zero.succ at 0
    apply impossible
    rw equal
    rfl
  | succ(k) using ih =>
    have shape := pow.succ at 4, k
    rw shape
    have fourNonzero : 4 ≠ 0
      intro fourZero
      have zeroFour : 0 = 4
        rw fourZero
        rfl
      have impossible := Naturals.disjoint.zero.succ at 3
      exact impossible with zeroFour
    exact mul.nonzero with fourNonzero, ih

theorem natural.four_nonzero
  shows 4 ≠ 0
proof
  intro fourZero
  have zeroFour : 0 = 4
    rw fourZero
    rfl
  have impossible := Naturals.disjoint.zero.succ at 3
  exact impossible with zeroFour