omniscience

Omniscient.lean

import Mathlib.Data.Set.Insert
import Mathlib.Logic.Embedding.Basic

universe u

def IsOmniscient (X : Type u) : Type u :=
  ∀ p : X → Bool, Decidable (∃ x : X, p x = false)

lemma isOmniscient_em {X : Type u} (hX : IsOmniscient X) (p : X → Bool) :
    (∃ x : X, p x = false) ∨ (∀ x : X, p x = true) :=
  match hX p with
  | isTrue h => Or.inl h
  | isFalse h => Or.inr fun _ ↦ eq_true_of_ne_false fun h' ↦ h ⟨_, h'⟩

variable {X : Type*} {ε : (X → Bool) → X}

def IsSelection (X : Type*) (ε : (X → Bool) → X) : Prop :=
    ∀ p : X → Bool, p (ε p) = true → ∀ x, p x = true

lemma isSelection_contra :
    IsSelection X ε → ∀ p : X → Bool, ¬ (∀ x, p x = true) → p (ε p) = false := by
  simp only [IsSelection, ← Bool.not_eq_true]
  intro h p h' h''
  exact h' (h p h'')

def IsSearchable (X : Type*) : Prop :=
  ∃ (ε : (X → Bool) → X), IsSelection X ε

def IsSelection.isOmniscient {X : Type*} {ε : (X → Bool) → X} (hε : IsSelection X ε) :
    IsOmniscient X := fun p ↦
  match hp : p (ε p) with
  | true => isFalse fun ⟨x, h⟩ ↦ by
      have := hε p hp x
      simp_all only [Bool.true_eq_false]
  | false => isTrue ⟨_, hp⟩

lemma IsSelection.exists_eq_false_iff {X : Type*} {ε : (X → Bool) → X}
    (hε : IsSelection X ε) (p : X → Bool) :
    (∃ x, p x = false) ↔ p (ε p) = false := by
  refine ⟨?_, fun h ↦ ⟨_, h⟩⟩
  rintro ⟨x, hx⟩
  rw [← Bool.not_eq_true]
  intro h
  rw [← Bool.not_eq_true] at hx
  exact hx (hε p h x)

def decideRoot (X : Type*) (ε : (X → Bool) → X) : (X → Bool) → Bool := fun p => p (ε p)

lemma IsSelection.decideRoot_eq_false_iff {X : Type*} {ε : (X → Bool) → X} (hε : IsSelection X ε)
    {p : X → Bool} :
    decideRoot X ε p = false ↔ ∃ x, p x = false :=
  (hε.exists_eq_false_iff p).symm

lemma IsSearchable.choice {X Y : Type*} (A : X → Y → Prop) [DecidableRel A] (hY : IsSearchable Y) :
    (∀ x, ∃ y, A x y) → ∃ f : X → Y, ∀ x, A x (f x) := by
  intro h
  obtain ⟨ε, hε⟩ := hY
  let f (x) := ε (fun y ↦ ¬ A x y)
  refine ⟨f, fun x ↦ ?_⟩
  dsimp [f]
  apply Decidable.of_not_not
  simp only [decide_not]
  intro h'
  have : _ = true → _ := hε (fun y ↦ ¬ A x y)
  simp only [decide_not, Bool.not_eq_eq_eq_not, Bool.not_true, decide_eq_false_iff_not] at this
  obtain ⟨y, hy⟩ := h x
  exact this h' y hy


def Ninfty : Set (ℕ → Bool) := {x : ℕ → Bool | ∀ i : ℕ, x (i + 1) ≤ x i}

notation "ℕ∞" => Ninfty

lemma antitone_of_mem_ninfty {a : ℕ → Bool} : a ∈ ℕ∞ → ∀ i j, i ≤ j → a j ≤ a i := by
  intro h i j hij
  induction j, hij using Nat.le_induction with
  | base => intro h; exact h
  | succ n hmn h' => exact h' ∘ h _

def ofNat : ℕ → ℕ∞ := fun n ↦ ⟨fun i ↦ n > i, fun i h ↦ by simp_all; omega⟩

@[simp] lemma ofNat_apply {n i : ℕ} : (ofNat n).1 i = decide (n > i) := rfl

lemma ofNat_injective : Function.Injective ofNat := by
  intro n m h
  have hn : (ofNat n).1 n = (ofNat m).1 n := by rw [h]
  have hm : (ofNat n).1 m = (ofNat m).1 m := by rw [h]
  simp only [ofNat_apply, gt_iff_lt, lt_self_iff_false, decide_false, false_eq_decide_iff, not_lt,
    decide_eq_false_iff_not] at hn hm
  exact Nat.le_antisymm hm hn

def nats : Set ℕ∞ := Set.range ofNat

def infty : ℕ∞ := ⟨fun _ => true, fun _ ↦ Bool.le_true _⟩

@[simp] lemma infty_apply {i : ℕ} : infty.1 i = true := rfl

def minUpTo_aux (a : ℕ → Bool) : ℕ → Bool
  | 0 => a 0
  | n + 1 => a (n + 1) && minUpTo_aux a n

def minUpTo (a : ℕ → Bool) : ℕ∞ := ⟨minUpTo_aux a, fun _ ↦ Bool.and_le_right _ _⟩

lemma minUpTo_zero (a : ℕ → Bool) : (minUpTo a).1 0 = a 0 := rfl
lemma minUpTo_succ (a : ℕ → Bool) (n : ℕ) :
    (minUpTo a).1 (n + 1) = (a (n + 1) && (minUpTo a).1 n) := rfl

lemma minUpTo_le_self {a : ℕ → Bool} {n : ℕ} : (minUpTo a).1 n ≤ a n :=
  match n with
  | 0 => id
  | _ + 1 => Bool.and_le_left _ _

lemma minUpTo_le {α : ℕ → Bool} {n k : ℕ} (hk : k ≤ n) : (minUpTo α).1 n ≤ α k := by
  induction n, hk using Nat.le_induction with
  | base => exact minUpTo_le_self
  | succ m hkm ih => exact ih ∘ Bool.and_le_right _ _

lemma exists_eq_minUpTo (a : ℕ → Bool) (n : ℕ) : ∃ i ≤ n, (minUpTo a).1 n = a i := by
  induction n with
  | zero => exact ⟨0, le_rfl, rfl⟩
  | succ n ih =>
      obtain ⟨i, hin, hi⟩ := ih
      rw [minUpTo_succ]
      cases h : a (n + 1) with
      | false => exact ⟨n + 1, le_rfl, by rw [h, Bool.false_and]⟩
      | true => exact ⟨i, hin.trans (Nat.le_succ _), by rwa [Bool.true_and]⟩

lemma minUpTo_eq_true_iff {a : ℕ → Bool} {n : ℕ} :
    (minUpTo a).1 n = true ↔ ∀ i ≤ n, a i = true := by
  constructor
  · intro h i hi
    apply minUpTo_le hi h
  · intro h
    obtain ⟨i, hi, hi'⟩ := exists_eq_minUpTo a n
    rw [hi', h _ hi]

lemma minUpTo_eq_false_iff {a : ℕ → Bool} {n : ℕ} :
    (minUpTo a).1 n = false ↔ ∃ i ≤ n, a i = false := by
  constructor
  · intro h
    obtain ⟨i, hi, hi'⟩ := exists_eq_minUpTo a n
    use i, hi
    rw [← hi', h]
  · rintro ⟨i, hi, hi'⟩
    rw [← Bool.not_eq_true] at hi' ⊢
    intro h
    exact hi' (minUpTo_le hi h)

lemma minUpTo_eq_of_mem (a : ℕ → Bool) (ha : a ∈ ℕ∞) : minUpTo a = a := by
  ext n
  rw [Bool.eq_iff_iff, minUpTo_eq_true_iff]
  constructor
  · intro h
    exact h _ le_rfl
  · intro h i hi
    exact antitone_of_mem_ninfty ha i n hi h

lemma minUpTo_surj : minUpTo.Surjective := by
  rintro ⟨a, ha⟩
  use minUpTo a
  apply Subtype.ext
  rw [minUpTo_eq_of_mem a ha, minUpTo_eq_of_mem _ ha]

def sumTo (a : ℕ → Bool) : ℕ → ℕ
  | 0 => 0
  | n + 1 => (a n).toNat + sumTo a n

lemma sumTo_eq_of {a : ℕ → Bool} (ha : a ∈ ℕ∞) {n : ℕ} (h : a n = true) :
    sumTo a n = n := by
  induction n with
  | zero => simp [sumTo]
  | succ n ih =>
      rw [sumTo]
      have hn : a n = true := ha n h
      rw [hn, Bool.toNat_true, Nat.add_comm, ih hn]

lemma ofNat_sumTo {a : ℕ → Bool} (ha : a ∈ ℕ∞) {n : ℕ} (h : a n = false) :
    ofNat (sumTo a n) = a := by
  ext i
  rw [ofNat, Subtype.coe_mk, Bool.eq_iff_iff, decide_eq_true_eq, gt_iff_lt]
  induction n generalizing i with
  | zero =>
      rw [sumTo]
      simp only [Nat.not_lt_zero, false_iff]
      intro hi
      rw [← Bool.not_eq_true] at h
      exact h (antitone_of_mem_ninfty ha 0 i (by omega) hi)
  | succ n ih =>
      rw [sumTo]
      match hn : a n with
      | false =>
          simp only [Bool.toNat_false, Nat.zero_add]
          apply ih hn
      | true =>
          rw [Bool.toNat_true, Nat.add_comm]
          constructor
          · intro h'
            suffices i ≤ n from antitone_of_mem_ninfty ha _ _ this hn
            rw [sumTo_eq_of ha hn] at h'
            omega
          · intro h'
            rw [Nat.lt_add_one_iff]
            have : i ≤ n := by
              by_contra!
              have : n + 1 ≤ i := by omega
              rw [← Bool.not_eq_true] at h
              exact h (antitone_of_mem_ninfty ha _ _ this h')
            exact this.trans_eq (sumTo_eq_of ha hn).symm

lemma eq_ofNat_of_eq_false {a : ℕ → Bool} (ha : a ∈ ℕ∞) {n : ℕ} (h : a n = false) :
    ∃ k, a = ofNat k := by
  refine ⟨sumTo a n, ?_⟩
  rw [ofNat_sumTo ha h]

def IsFull (S : Set X) : Prop := ∀ x, ¬ x ∉ S

lemma full_dense {X Y : Type*} [DecidableEq Y] {F : Set X} (hF : IsFull F)
    {f : X → Y} (y : Y) (hf : ∀ x ∈ F, f x = y) :
    ∀ x, f x = y := by
  intro x
  by_contra! this
  apply hF x
  intro hx
  exact this (hf x hx)

lemma eq_infty_of {a : ℕ∞} (ha : ∀ n, a ≠ ofNat n) : a = infty := by
  ext n
  simp only [infty]
  rw [← Bool.not_eq_false]
  intro h
  obtain ⟨k, hk⟩ := eq_ofNat_of_eq_false a.2 h
  apply ha k
  exact Subtype.ext hk

lemma eq_infty_of' {a : ℕ∞} (ha : a ∉ nats) : a = infty := eq_infty_of fun n h ↦ ha ⟨n, h.symm⟩

lemma insert_isFull : IsFull (insert infty nats) := by
  intro a ha
  rw [Set.mem_insert_iff] at ha
  have : a ∉ nats := mt .inr ha
  exact ha (Or.inl (eq_infty_of' this))

def select (p : ℕ∞ → Bool) : ℕ∞ := minUpTo fun n ↦ p (ofNat n)

lemma select_eq_false_iff (p : ℕ∞ → Bool) (n : ℕ) :
    (select p).1 n = false ↔ ∃ k ≤ n, p (ofNat k) = false := by
  rw [select, minUpTo_eq_false_iff]

lemma select_eq_true_iff (p : ℕ∞ → Bool) (n : ℕ) :
    (select p).1 n = true ↔ ∀ k ≤ n, p (ofNat k) = true := by
  rw [select, minUpTo_eq_true_iff]

lemma select_eq_ofNat_iff (p : ℕ∞ → Bool) (n : ℕ) :
    select p = ofNat n ↔ p (ofNat n) = false ∧ ∀ k < n, p (ofNat k) = true := by
  rw [Subtype.ext_iff, funext_iff]
  simp only [ofNat_apply, gt_iff_lt]
  constructor
  · intro h
    have : ∀ k < n, p (ofNat k) = true := by
      intro k hk
      specialize h k
      simp only [hk, decide_true, select_eq_true_iff] at h
      exact h _ le_rfl
    refine ⟨?_, this⟩
    specialize h n
    simp only [lt_self_iff_false, decide_false, select_eq_false_iff] at h
    obtain ⟨k, hk, hk'⟩ := h
    suffices ¬ k < n by
      have : k = n := by omega
      rwa [← this]
    intro h
    rw [← Bool.not_eq_true] at hk'
    apply hk'
    rw [this _ h]
  · rintro ⟨h₁, h₂⟩ x
    cases lt_or_ge x n with
    | inl h =>
        simp only [h, decide_true]
        rw [select_eq_true_iff]
        intro k hk
        apply h₂ _ (by omega)
    | inr h =>
        simp [h.not_gt]
        rw [select_eq_false_iff]
        refine ⟨n, h, h₁⟩

lemma select_eq_infty_iff (p : ℕ∞ → Bool) :
    select p = infty ↔ ∀ n, p (ofNat n) = true := by
  simp only [Subtype.ext_iff, funext_iff, infty_apply, select_eq_true_iff]
  aesop

lemma select_isSelection : IsSelection ℕ∞ select := by
  intro p hp
  have h₁ : ∀ n, select p ≠ ofNat n := by
    intro n hn
    have : p (ofNat n) = true := by rw [← hn, hp]
    rw [select_eq_ofNat_iff] at hn
    rw [← Bool.not_eq_false] at this
    exact this hn.1
  have h₂ : select p = infty := eq_infty_of h₁
  have h₃ : p infty = true := by
    rw [← h₂, hp]
  have h₄ : ∀ n, p (ofNat n) = true := by
    intro n
    rw [select_eq_infty_iff] at h₂
    apply h₂
  have h₅ : ∀ x ∈ insert infty nats, p x = true := by simp [nats, *]
  exact full_dense insert_isFull true h₅

def ninfty_isOmniscient : IsOmniscient ℕ∞ := select_isSelection.isOmniscient

def decidableEq_function {X : Type*} {Y : Type*} (hX : IsOmniscient X) [DecidableEq Y] :
    DecidableEq (X → Y) :=
  fun f g ↦
  match hX (fun x ↦ decide (f x = g x)) with
  | isTrue h => isFalse <| by
      obtain ⟨x, hx⟩ := h
      simp only [decide_eq_false_iff_not] at hx
      rintro rfl
      exact hx rfl
  | isFalse h => isTrue <| by
      simp only [decide_eq_false_iff_not, not_exists, Decidable.not_not] at h
      exact funext h

instance {Y : Type*} [DecidableEq Y] : DecidableEq (ℕ∞ → Y) :=
  decidableEq_function ninfty_isOmniscient

def witness {X Y : Type*} [DecidableEq Y] {ε : (X → Bool) → X} (hε : IsSelection X ε)
    (f g : X → Y) : {x // f x ≠ g x} ⊕' (∀ x, f x = g x) :=
  let p : X → Bool := fun x ↦ decide (f x = g x)
  match hp : p (ε p) with
  | true => .inr fun x ↦ decide_eq_true_iff.1 (hε p hp x)
  | false => .inl ⟨ε p, decide_eq_false_iff_not.1 hp⟩

def findDifference {Y : Type*} [DecidableEq Y] (f g : ℕ∞ → Y) : Option ℕ∞ :=
  match witness select_isSelection f g with
  | .inl x => some x
  | .inr _ => none

instance : Repr ℕ∞ where
  reprPrec r _ :=
    let N := 20
    "(sorry /- " ++
      Std.Format.joinSep ((List.range N).map <| repr ∘ Bool.toNat ∘ r.1) "" ++
      "... -/)"

def test : (X : Type) × DecidableEq (X → Bool) × (ℕ ↪ X) :=
  ⟨ℕ∞, inferInstance, ⟨ofNat, ofNat_injective⟩⟩

#print axioms test -- 'test' depends on axioms: [propext, Quot.sound]