-- Uncountability of the Dedekind reals - Encoding
-- 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.Encoding
import Separation

theorem cantorPrefix.eq_of_real_eq (X Y : Set, n : Nat)
  requires same : cantorReal(X) = cantorReal(Y)
  shows cantorPrefix(X, n) = cantorPrefix(Y, n)
proof
  induction n
  | zero =>
    have right : 0 = cantorPrefix(Y, 0)
      have rightShape := cantorPrefix.zero at Y
      rw rightShape
      rfl
    calc
      cantorPrefix(X, 0) = 0 := cantorPrefix.zero at X
      _ = cantorPrefix(Y, 0) := right
  | succ(k) using ih =>
    have leftShape := cantorPrefix.succ at X, k
    have rightShape := cantorPrefix.succ at Y, k
    rw [leftShape, rightShape, ih]
    have xCases := binaryDigit.cases at X, k
    have yCases := binaryDigit.cases at Y, k
    cases xCases with xZero | xOne
    . cases yCases with yZero | yOne
      . rw [xZero, yZero]
        rfl
      . exfalso
        have yMember : k ∈ Y
          by_contra yMissing
          have zeroAtY := binaryDigit.zero with yMissing
          rw yOne at zeroAtY
          have zeroNotOne := Naturals.disjoint.zero.succ at 0
          apply zeroNotOne
          rw zeroAtY
          rfl
        have xMissing : ¬(k ∈ X)
          intro xMember
          have oneAtX := binaryDigit.one with xMember
          rw xZero at oneAtX
          exact Naturals.disjoint.zero.succ at 0 with oneAtX
        have bitY : k ∈ Y ↔ cantorMid(Y, k) ∈ cantorReal(Y) by apply cantorReal.bit
        have yMid := bitY.forward with yMember
        have midsEqual : cantorMid(X, k) = cantorMid(Y, k) by simp [cantorMid, ih]
        rw [← midsEqual, ← same] at yMid
        exact cantorMid.not_mem_of_missing with xMissing, yMid
    . cases yCases with yZero | yOne
      . exfalso
        have xMember : k ∈ X
          by_contra xMissing
          have zeroAtX := binaryDigit.zero with xMissing
          rw xOne at zeroAtX
          have zeroNotOne := Naturals.disjoint.zero.succ at 0
          apply zeroNotOne
          rw zeroAtX
          rfl
        have yMissing : ¬(k ∈ Y)
          intro yMember
          have oneAtY := binaryDigit.one with yMember
          rw yZero at oneAtY
          exact Naturals.disjoint.zero.succ at 0 with oneAtY
        have bitX : k ∈ X ↔ cantorMid(X, k) ∈ cantorReal(X) by apply cantorReal.bit
        have xMid := bitX.forward with xMember
        have midsEqual : cantorMid(X, k) = cantorMid(Y, k) by simp [cantorMid, ih]
        rw [midsEqual, same] at xMid
        exact cantorMid.not_mem_of_missing with yMissing, xMid
      . rw [xOne, yOne]
        rfl

theorem cantorReal.injective (X Y : Set)
  requires subsetX : X ⊆ ℕ
  requires subsetY : Y ⊆ ℕ
  requires same : cantorReal(X) = cantorReal(Y)
  shows X = Y
proof
  ext n
  constructor
  . intro memberX
    have nInOmega := subsetX with n, memberX
    have nNatural := nat.omega.backward with nInOmega
    have bitX : n ∈ X ↔ cantorMid(X, n) ∈ cantorReal(X) by apply cantorReal.bit
    have midpoint := bitX.forward with memberX
    have prefixesEqual := cantorPrefix.eq_of_real_eq with same
    have midsEqual : cantorMid(X, n) = cantorMid(Y, n) by simp [cantorMid, prefixesEqual]
    rw [midsEqual, same] at midpoint
    have bitY : n ∈ Y ↔ cantorMid(Y, n) ∈ cantorReal(Y) by apply cantorReal.bit
    exact bitY.backward with midpoint
  . intro memberY
    have nInOmega := subsetY with n, memberY
    have nNatural := nat.omega.backward with nInOmega
    have bitY : n ∈ Y ↔ cantorMid(Y, n) ∈ cantorReal(Y) by apply cantorReal.bit
    have midpoint := bitY.forward with memberY
    have prefixesEqual := cantorPrefix.eq_of_real_eq with same
    have midsEqual : cantorMid(X, n) = cantorMid(Y, n) by simp [cantorMid, prefixesEqual]
    rw [← midsEqual, ← same] at midpoint
    have bitX : n ∈ X ↔ cantorMid(X, n) ∈ cantorReal(X) by apply cantorReal.bit
    exact bitX.backward with midpoint