User:Hakerh400/Proof 002

This is a proof that the algorithm described in User:Hakerh400/Bijection between reals and the powerset of naturals is incorrect. In particular, real number $-0.75$ cannot be represented as a sequence of binary digits using the algorithm.

Definitions

A bit is either $0$ or $1$.

A natural number is either zero, or a successor of a natural number.

A real number is a 3-tuple $(S,N,F)$ where $S$ is a bit, $N$ is a natural number and $F$ is a countably infinite sequence of bits. There are two constraints:

• $F$ does not end with infinitely many $1$s (for each natural number $n$, there exists a natural number $k\geq n$ such that $k$-th bit of $F$ is $0$).
• If $F$ consists only of $0$s and $N$ is zero, then $S$ is $0$.

Informally, $S$ represents the sign of the real number ($0$ - nonnegative, $1$ - negative), $N$ represents the absolute value of the integral part, $F$ represents the binary expansion of the fractional part.

Referencing bits in sequences of bits is 0-indexed.

Function bits_to_real maps countably infinite sequences of bits to real numbers. It is defined in the following way. Given sequence of bits $f$. There are two cases:

• $f$ ends with infnitely many same bits. $S$ is that bit. Let $i$ be the index of the first of the ending bits (the first index such that from that index on, all bits are equal to that bit). Let $f'$ be $f$ with all bits starting from $i+1$ replaced with $0$. $N$ is the index of the first $0$ in $f'$. $F$ is $f'$ without the first $N+1$ bits.
• $f$ does not end with infinitely many same bits. $S$ is the first bit. Let $f'$ be $f$ without the first bit. $N$ is the index of the first $0$ in $f'$. $F$ is $f'$ without the first $N+1$ bits.

Theorem

Function bits_to_real between countably infinite sequences of bits and real numbers in injective, but not surjective, and therefore not bijective.

Proof

-- Lean: v3.35.1
-- Mathlib: d856bf9b

import tactic
import data.nat.lattice

open nat
open function
open classical

open_locale classical

namespace real

noncomputable theory

def ends_with (b : Prop) (f : ℕ → Prop) : Prop :=
∃ (i : ℕ), ∀ {n : ℕ}, i ≤ n → f n = b

structure Real :=
(neg : Prop)
(n : ℕ)
(f : ℕ → Prop)
(h₁ : ¬ends_with true f)
(h₂ : (∀ (n : ℕ), ¬f n) → n = 0 → ¬neg)

def slice (k : ℕ) (f : ℕ → Prop) (n : ℕ) : Prop :=
f (n + k)

class preserves_end (F : (ℕ → Prop) → ℕ → Prop) : Prop :=
(pe: ∀ {f : ℕ → Prop} {b : Prop}, ends_with b (F f) = ends_with b f)

lemma pr_end {F : (ℕ → Prop) → ℕ → Prop} [preserves_end F] :
∀ {f : ℕ → Prop} {b : Prop}, ends_with b (F f) = ends_with b f
:= by apply preserves_end.pe

instance {k : ℕ} : preserves_end (slice k) := begin
  split, rintro f b, ext, split; rintro ⟨i, h⟩,
  { use i + k, rintro n h₁,
    obtain ⟨n, rfl⟩ := exists_eq_add_of_le h₁, clear h₁,
    unfold slice at h, rw [add_assoc, add_comm k, ←add_assoc],
    apply h, apply le_add_right (le_refl _) },
  { use i, rintro n h₁, apply h, apply le_add_right h₁ },
end

def n_aux (f : ℕ → Prop) : ℕ := Inf {i | ¬f i}

def get_nf (f : ℕ → Prop) : ℕ × (ℕ → Prop) :=
⟨n_aux f, slice (n_aux f + 1) f⟩

def real_from_nf
  (neg : Prop)
  (snf : ℕ × (ℕ → Prop))
  (h₁ : ¬ends_with true snf.2)
  (h₂ : (∀ (n : ℕ), ¬snf.2 n) → snf.1 = 0 → ¬neg)
  : Real := ⟨neg, snf.1, snf.2, h₁, h₂⟩

def min_end (b : Prop) (f : ℕ → Prop) : ℕ :=
Inf {i | ∀ (n : ℕ), i ≤ n → f n = b }

def bits_to_real (f : ℕ → Prop) : Real :=
if h : ∃ {b : Prop}, ends_with b f
  then real_from_nf (some h) (get_nf
      (λn, n < min_end (some h) f + 1 ∧ f n))
    begin
      simp_rw [ends_with, get_nf, slice],
      generalize_proofs, push_neg, intro i,
      use max i (min_end (some h) f + 1), split,
      { apply le_max_left },
      { rw [ne, eq_true], apply not_and_of_not_left,
        push_neg, apply le_add_right, apply le_max_right },
    end
    begin
      intro F_all_0s,
      intro N_is_0,
      intro h₁,
      revert F_all_0s N_is_0,
      have f_ends_with_1s := some_spec h,
      rw ←@eq_true (some h) at h₁, rw h₁ at *, clear h₁,
      generalize f'_def : (λ (n : ℕ), n < min_end true f + 1 ∧ f n) = f',
      generalize F_def : (get_nf f').snd = F,
      intro F_all_0s,
      intro N_is_0,
      have f'_ends_with_0s : ends_with false f',
      { use min_end true f + 1, rintro i h₁,
        rw ←f'_def, dsimp only, rw eq_false,
        apply not_and_of_not_left, push_neg, exact h₁ },
      have f'_has_0 : ∃ (n : ℕ), ¬f' n,
      { obtain ⟨n, h₁⟩ := f'_ends_with_0s, use n,
        replace h₁ := @h₁ n (le_refl _),
        rw eq_false at h₁, exact h₁ },
      have f'_0_is_0 : ¬f' 0,
      { simp_rw [get_nf, n_aux, Inf] at N_is_0,
        split_ifs at N_is_0 with h₁,
        { letI := prop_decidable,
          exact (nat.find_eq_zero f'_has_0).mp N_is_0 },
        { obtain ⟨n, h₂⟩ := f'_has_0,
          push_neg at h₁, exfalso, exact h₁ n h₂ }},
      have f'_has_1 : ∃ (n : ℕ), f' n,
      { rw ←f'_def, use min_end true f, split,
        { apply lt_succ_self },
        { simp_rw [min_end, Inf], split_ifs with h₁,
          { exact eq_true.mp (nat.find_spec f_ends_with_1s (le_refl _)) },
          { obtain ⟨i, h₂⟩ := id f_ends_with_1s,
            exfalso, push_neg at h₁, apply h₁ i, assumption }}},
      have F_is_slice_1_f' : F = slice 1 f',
      { have h₁ := le_zero_iff.mp (@nat.Inf_le {i : ℕ | ¬f' i} _ f'_0_is_0),
        ext n, simp_rw [←F_def, get_nf, n_aux, h₁] },
      have F_has_1 : ∃ (n : ℕ), F n,
      { obtain ⟨n, h₁⟩ := f'_has_1, cases n,
        { exfalso, exact f'_0_is_0 h₁, },
        { use n, simp_rw [F_is_slice_1_f', slice], exact h₁ } },
      exact F_all_0s _ (some_spec F_has_1),
    end
  else real_from_nf (f 0) (get_nf (slice 1 f))
    begin
      push_neg at h, replace h := @h true,
      simp_rw [get_nf, pr_end], exact h,
    end
    begin
      push_neg at h, replace h := @h false,
      simp_rw [get_nf, n_aux],
      rintro h₁ h₂,
      rw [h₂, zero_add] at h₁, clear h₂,
      unfold slice at h₁,
      unfold ends_with at h,
      push_neg at h, exfalso,
      obtain ⟨n, ⟨h₁, h₂⟩⟩ := h 2, clear h,
      obtain ⟨n, rfl⟩ := exists_eq_add_of_lt h₁, clear h₁,
      rw [ne, eq_false, add_comm 1 n] at h₂,
      exact h₂ (h₁ n),
    end

lemma exi_end_iff {f : ℕ → Prop} :
  (∃ (b : Prop), ends_with b f) ↔
  (∃ (b : Prop), ends_with b (bits_to_real f).f) :=
begin
  split; intro h,
  { use false,
    simp_rw [bits_to_real, real_from_nf, get_nf],
    split_ifs with h₁,
    { clear h₁,
      generalize h₁ : n_aux
        (λ (n : ℕ), n < min_end (some h) f + 1 ∧ f n) + 1 = k₁,
      generalize h₂ : min_end (some h) f + 1 = k₂,
      use k₂, rintro n h₃, rw [eq_false, slice],
      apply not_and_of_not_left, push_neg,
      apply le_add_right h₃ },
    { contradiction }},
  { simp_rw [bits_to_real, real_from_nf, get_nf] at h,
    split_ifs at h with h₁,
    { exact h₁ },
    { simp_rw [pr_end] at h, contradiction }},
end

lemma eq_slice {f₁ f₂ : ℕ → Prop} (n : ℕ) :
  ((∀ (k : ℕ), k < n → f₁ k = f₂ k) ∧
    slice n f₁ = slice n f₂) ↔ f₁ = f₂ :=
begin
  split,
  { rintro ⟨h₁, h₂⟩, ext i,
    by_cases h₃ : i < n,
    { exact iff_of_eq (h₁ i h₃) },
    { push_neg at h₃,
      obtain ⟨i, rfl⟩ := exists_eq_add_of_le h₃,
      replace h₂ := congr_fun h₂ i,
      unfold slice at h₂, rw add_comm at h₂,
      exact iff_of_eq h₂ }},
  { intro h, subst h, split,
    { rintro k h, refl },
    { refl }},
end

lemma exi_bit {f : ℕ → Prop}
  (h : ∀ (b : Prop), ¬ends_with b f) :
  ∀ (b : Prop), ∃ (n : ℕ), f n = b :=
begin
  intro b,
  replace h := h ¬b,
  unfold ends_with at h,
  push_neg at h,
  obtain ⟨i, ⟨h₁, h₂⟩⟩ := h 0,
  use i, ext, tauto,
end

lemma exi_bit_slice {f : ℕ → Prop}
  (h : ∀ (b : Prop), ¬ends_with b f) :
  ∀ (b : Prop) (k : ℕ), ∃ (n : ℕ), slice k f n = b :=
begin
  rintro b k, unfold slice, apply exi_bit,
  clear b, intro b, replace h := h b,
  have h₁ := id h, rw ←@pr_end (slice k) at h₁, exact h₁,
end

lemma eq_of_n_aux {f₁ f₂ : ℕ → Prop}
  (h₄ : n_aux f₁ = n_aux f₂)
  (h₅ : slice (n_aux f₁ + 1) f₁ = slice (n_aux f₂ + 1) f₂)
  (h₁ : ∃ (n : ℕ), ¬f₁ n)
  (h₂ : ∃ (n : ℕ), ¬f₂ n) :
  f₁ = f₂ :=
begin
  rw h₄ at h₅,
  refine (eq_slice _).mp ⟨_, h₅⟩,
  rintro k h₆,
  replace h₆ := le_of_lt_succ h₆,
  rw [n_aux] at h₆,
  replace h₆ := le_iff_eq_or_lt.mp h₆,
  cases h₆,
  { have h₇ := h₆,
    unfold n_aux at h₄,
    rw ←h₄ at h₆,
    have h₈ := @nat.Inf_mem (λk, ¬f₁ k) h₁,
    have h₉ := @nat.Inf_mem (λk, ¬f₂ k) h₂,
    simp_rw ←eq_false at h₆ h₇ h₈ h₉,
    transitivity false,
    { rw h₆, exact h₈ },
    { rw h₇, exact eq.symm h₉ }},
  { have h₇ := h₆, unfold n_aux at h₄, rw ←h₄ at h₆,
    replace h₆ := not_not.mp (nat.not_mem_of_lt_Inf h₆),
    replace h₇ := not_not.mp (nat.not_mem_of_lt_Inf h₇),
    ext, tauto },
end

lemma min_end_eq {f : ℕ → Prop} {b : Prop}
  (h₁ : ends_with b f) :
  ∀ (k : ℕ), min_end b f ≤ k → f k = b :=
by rintro k h₂; exact @nat.Inf_mem _ h₁ k h₂

lemma m_wlog {f₁ f₂ : ℕ → Prop}
  (h' : bits_to_real f₁ = bits_to_real f₂)
  (h₁ : ∃ {b : Prop}, ends_with b f₁)
  (h₂ : ∃ {b : Prop}, ends_with b f₂) :
  let b : Prop := some h₁,
      m₁ : ℕ := min_end b f₁,
      m₂ : ℕ := min_end b f₂,
      F₁ : ℕ → Prop := λ (n : ℕ), n < m₁ + 1 ∧ f₁ n,
      F₂ : ℕ → Prop := λ (n : ℕ), n < m₂ + 1 ∧ f₂ n
  in b = some h₂ →
     ends_with b f₁ →
     ends_with b f₂ →
     n_aux F₁ = n_aux F₂ →
     (∀ (a : ℕ), F₁ a = F₂ a) →
     (∀ (a : ℕ),
        F₁ (a + (n_aux F₁ + 1)) = F₂ (a + (n_aux F₂ + 1))) →
     m₁ ≤ m₂ :=
begin
  intros b m₁ m₂ F₁ F₂ h₃ h₆ h₇ h₄ h₈ h₅,
  by_contra hm, push_neg at hm,
  by_cases hb : b,
  { rw ←@eq_true b at hb, rw hb at *,
    have hm₁ : ∀ (k : ℕ), m₁ < k → ¬F₁ k,
    { rintro k hk, simp_rw F₁, apply not_and_of_not_left,
      push_neg, apply succ_le_of_lt hk },
    have hm₂ : ∀ (k : ℕ), m₂ < k → ¬F₂ k,
    { rintro k hk, simp_rw F₂, apply not_and_of_not_left,
      push_neg, apply succ_le_of_lt hk },
    have hx : F₁ m₁,
    { simp_rw F₁, refine ⟨lt_succ_self _, _⟩,
      rw ←@eq_true (f₁ m₁), simp_rw [m₁, min_end, b],
      apply nat.Inf_mem h₆, simp_rw [←b, hb], apply le_refl },
    have hy : ¬F₂ m₁,
    { simp_rw F₂,
      apply not_and_of_not_left,
      push_neg,
      apply succ_le_of_lt hm },
    rw ←h₈ at hy, contradiction },
  { obtain ⟨d, hd⟩ := exists_eq_add_of_lt hm,
    rw ←eq_false at hb, rw hb at *,
    have hm₁ : ∀ (k : ℕ), m₁ ≤ k → ¬f₁ k,
    { rintro k hk,
      simp_rw [m₁, min_end, hb] at hk,
      exact eq_false.mp (@nat.Inf_mem _ h₆ _ hk) },
    have hx : F₁ (pred m₁),
    { have hm₂ : m₂ + d < m₁,
      { rw hd, apply lt_succ_self },
      simp_rw [m₁, min_end] at hm₂,
      have hm₃ : ¬∀ (n : ℕ), m₂ + d ≤ n → f₁ n = b,
      { exact nat.not_mem_of_lt_Inf hm₂ },
      push_neg at hm₃,
      simp_rw [hb, ne, eq_false, not_not] at hm₃,
      simp_rw [F₁, hd, pred],
      obtain ⟨n, ⟨hn₁, hn₂⟩⟩ := hm₃,
      split,
      { apply lt_succ_of_lt, apply lt_succ_self },
      { cases hn₁ with n hn₃,
        { exact hn₂ },
        { exfalso,
          refine hm₁ _ _ hn₂,
          rw hd,
          rw [add_one_le_iff, lt_succ_iff],
          exact hn₃ }}},
    have hy : ¬F₂ (pred m₁),
    { simp_rw [F₂, hd, pred],
      apply not_and_of_not_right,
      simp_rw ←eq_false,
      apply nat.Inf_mem h₇,
      simp_rw [m₂, min_end, hb],
      apply le_add_right (le_refl _) },
    rw ←h₈ at hy, contradiction },
end

lemma inj_bits_to_real : injective bits_to_real := begin
  rintro f₁ f₂ h,
  have h' := h,
  simp_rw [bits_to_real, real_from_nf, get_nf] at h,
  split_ifs at h with h₁ h₂ h₂,
  { rcases h with ⟨h₃, ⟨h₄, h₅⟩⟩,
    have h₆ := some_spec h₁,
    have h₇ := some_spec h₂,
    rw ←h₃ at *,
    have h₈ := eq_of_n_aux h₄ h₅ begin
      use min_end (some h₁) f₁ + 2,
      apply not_and_of_not_left,
      push_neg, apply le_succ,
    end
    begin
      use min_end (some h₁) f₂ + 2,
      apply not_and_of_not_left,
      push_neg, apply le_succ,
    end,
    have h₉ : min_end (some h₁) f₁ = min_end (some h₁) f₂,
    { revert h₃ h₄ h₅ h₆ h₇ h₈,
      generalize b_def : some h₁ = b,
      generalize m₁_def : min_end b f₁ = m₁,
      generalize m₂_def : min_end b f₂ = m₂,
      generalize F₁_def : (λ (n : ℕ), n < m₁ + 1 ∧ f₁ n) = F₁,
      generalize F₂_def : (λ (n : ℕ), n < m₂ + 1 ∧ f₂ n) = F₂,
      rintro h₃ h₄ h₅ h₆ h₇ h₈,
      replace h₅ := congr_fun h₅,
      replace h₈ := congr_fun h₈,
      unfold slice at h₅,
      apply le_antisymm,
      { subst_vars, apply m_wlog; assumption },
      { subst h₃,
        subst_vars, apply m_wlog;
          try {try {symmetry}, assumption},
        { intro a, exact eq.symm (h₈ a) },
        { intro a, exact eq.symm (h₅ a) }}},
    replace h₈ := congr_fun h₈, dsimp at h₈,
    rw ←h₉ at h₈,
    apply (eq_slice (min_end (some h₁) f₁ + 1)).mp, split,
    { rintro k h₁₀, ext, split; intro h,
      { exact ((iff_of_eq (h₈ k)).mp ⟨h₁₀, h⟩).2 },
      { exact ((iff_of_eq (h₈ k)).mpr ⟨h₁₀, h⟩).2 }},
    { apply funext, intro n, unfold slice,
      transitivity some h₁,
      { apply min_end_eq,
        { exact h₆ },
        { exact le_add_left (le_succ _) }},
      { symmetry, apply min_end_eq,
        { rw h₃, exact some_spec h₂ },
        { rw ←h₉, exact le_add_left (le_succ _) }}}},
  { rw exi_end_iff at h₁ h₂, rw h' at h₁, contradiction },
  { rw exi_end_iff at h₁ h₂, rw h' at h₁, contradiction },
  { push_neg at h₁ h₂,
    rcases h with ⟨h₃, ⟨h₄, h₅⟩⟩,
    apply (eq_slice 1).mp, split,
    { rintro k h₆, rw [lt_one_iff.mp h₆, h₃] },
    { apply eq_of_n_aux h₄ h₅; simp_rw ←eq_false;
        apply exi_bit_slice _ false 1; assumption }},
end

lemma not_surj_bits_to_real : ¬surjective bits_to_real := begin
  rintro surj,
  generalize F_def : (λ (n : ℕ), n < 2) = F,
  obtain ⟨f, h₁⟩ := surj
    { neg := true,
      n := 0,
      f := F,
      h₁ := begin
        unfold ends_with,
        push_neg,
        rintro i,
        use max i 2,
        refine ⟨le_max_left _ _, _⟩,
        rw [ne, eq_true],
        subst F_def,
        dsimp,
        push_neg,
        apply le_max_right,
      end,
      h₂ := begin
        rintro h₁ h₂,
        clear h₂,
        exfalso,
        subst F_def,
        replace h₁ := h₁ 0,
        dsimp at h₁,
        push_neg at h₁,
        exact absurd h₁ (not_succ_le_zero _),
      end },
  have hf₁ := (@exi_end_iff F).mp begin
    use false,
    subst F_def,
    use 2,
    rintro n hn,
    dsimp,
    rw eq_false,
    push_neg,
    assumption,
  end,
  simp_rw [bits_to_real, real_from_nf, get_nf] at h₁,
  split_ifs at h₁ with hi₁,
  { rcases h₁ with ⟨h₁, ⟨h₂, h₃⟩⟩,
    simp_rw h₁ at h₂ h₃,
    simp_rw [h₂, zero_add] at h₃,
    subst F_def,
    generalize m_def : min_end true f = m,
    clear hf₁,
    simp_rw m_def at h₂ h₃,
    replace h₃ : ∀ (n : ℕ), n < 2 ↔ n < m ∧ f (n + 1),
    { replace h₃ := congr_fun h₃,
      simp_rw slice at h₃,
      dsimp at h₃,
      rintro n,
      replace h₃ := h₃ n,
      symmetry' at h₃,
      rw add_lt_add_iff_right at h₃,
      exact iff_of_eq h₃ },
    have f_ends_with_1s : ends_with true f,
    { have h := some_spec hi₁,
      rw h₁ at h,
      exact h },
    have f_0_eq_0 : ¬f 0,
    { simp_rw [n_aux, Inf] at h₂,
      split_ifs at h₂,
      { rw nat.find_eq_iff at h₂,
        replace h₂ := h₂.1,
        dsimp at h₂,
        contrapose h₂,
        push_neg at h₂ ⊢,
        exact ⟨zero_lt_succ _, h₂⟩ },
      { exfalso,
        push_neg at h,
        replace h := h (m + 1),
        dsimp at h,
        push_neg at h,
        exact lt_irrefl _ h.1 }},
    have min_end_ne_zero : m ≠ 0,
    { simp_rw min_end at m_def,
      have hm := nat.Inf_mem f_ends_with_1s (le_refl _),
      rw eq_true at hm,
      intro h, subst h,
      change f (Inf {i : ℕ | ∀ (n : ℕ), i ≤ n → f n = true}) at hm,
      rw m_def at hm,
      contradiction },
    obtain ⟨x, hx⟩ := exists_eq_succ_of_ne_zero min_end_ne_zero,
    have f_x_succ_eq_1 : f x.succ,
    { simp_rw min_end at m_def,
      have hm := nat.Inf_mem f_ends_with_1s (le_refl _),
      rw [←hx, ←m_def],
      rw eq_true at hm,
      assumption },
    have min_end_ge_2 : 2 < m,
    { have h₄ : f 1 := ((h₃ 0).mp (zero_lt_succ _)).2,
      have h₅ : 1 < m := ((h₃ 1).mp (lt_succ_self _)).1,
      replace h₅ : 2 ≤ m := succ_le_of_lt h₅,
      rw le_iff_eq_or_lt at h₅,
      cases h₅,
      { exfalso,
        subst h₅,
        replace hx := succ.inj hx,
        subst hx,
        have he : ∀ (n : ℕ), 2 ≤ n → f n = true,
        { simp_rw [min_end, Inf] at m_def,
          split_ifs at m_def;
            rw nat.find_eq_iff at m_def; exact m_def.1 },
        have h : min_end true f = 1,
        { simp_rw [min_end, Inf],
          split_ifs,
          { rw nat.find_eq_iff,
            dsimp,
            split,
            { rintro n hn,
              rw le_iff_eq_or_lt at hn,
              cases hn,
              { rw eq_true,
                subst hn,
                assumption },
              { apply he _ (succ_le_of_lt hn) }},
            { rintro n hn,
              rw lt_one_iff at hn,
              subst hn,
              push_neg,
              use 0,
              refine ⟨le_refl _, _⟩,
              rw [ne, eq_true],
              assumption }},
          { exfalso,
            contrapose h,
            push_neg,
            use 2,
            assumption }},
        { linarith }},
      { assumption }},
    have not_x_lt_2 : ¬x < 2,
    { subst hx,
      push_neg,
      apply le_of_lt_succ,
      assumption },
    rw ←eq_false at not_x_lt_2,
    have h₄ := (h₃ x).mpr,
    rw not_x_lt_2 at h₄,
    change ¬(x < m ∧ f x.succ) at h₄,
    push_neg at h₄,
    rw hx at h₄,
    replace h₄ := h₄ (lt_succ_self _),
    contradiction },
  { rcases h₁ with ⟨h₁, ⟨h₂, h₃⟩⟩,
    simp_rw [←exi_end_iff, ←h₃, pr_end] at hf₁,
    contradiction },
end

lemma not_bij_bits_to_real : ¬bijective bits_to_real :=
not_and_of_not_right _ not_surj_bits_to_real

end real