/Surreal.lean at de561bac1e084cb34e5dca970c3e5b6fd992e3d6

import Mathlib

-- Based on Knuth's book "Surreal Numbers"
-- https://github.com/oersted/lean-surreal-numbers is incomplete but has some helpful stuff
-- https://leanprover-community.github.io/archive/stream/113489-new-members/topic/defining.20surreal.20numbers.html
-- https://leanprover-community.github.io/archive/stream/217875-Is-there-code-for-X%3F/topic/Surreal.20numbers.html
-- Also, mathlib4 and https://github.com/vihdzp/combinatorial-games/ both have implementations of surreal numbers

-- Apparently using Set instead of List here can cause paradoxes
-- Which is a bit sad since this definition can't have infinite lists
structure PseudoNumber where
  l : List PseudoNumber
  r : List PseudoNumber

@[grind]
def PseudoNumber.le (x y : PseudoNumber) :=
  (∀ a ∈ x.l, ¬le y a) ∧ (∀ b ∈ y.r, ¬le b x)
termination_by sizeOf x + sizeOf y
decreasing_by
  all_goals
    expose_names
    cases x
    cases y
    have := List.sizeOf_lt_of_mem h
    grind [PseudoNumber.mk.sizeOf_spec]

instance : LE PseudoNumber where
  le x y := x.le y

@[grind]
lemma pseudonumber_le {x y : PseudoNumber} : LE.le x y ↔ x.le y := by rfl

@[grind]
def PseudoNumber.valid (x : PseudoNumber) :=
  (∀ a ∈ x.l, ∀ b ∈ x.r, ¬b ≤ a) ∧ (∀ a ∈ x.l, a.valid) ∧ (∀ b ∈ x.r, b.valid)
decreasing_by
  all_goals
    expose_names
    cases x
    have := List.sizeOf_lt_of_mem h
    grind [PseudoNumber.mk.sizeOf_spec]

def Number := { x : PseudoNumber // x.valid }

def Number.valid (x : Number) := by
  have := x.property
  unfold PseudoNumber.valid at this
  exact this

def Number.l (x : Number) : List Number :=
  x.val.l.attach.map fun ⟨a, b⟩ ↦ ⟨a, x.valid.2.1 a b⟩

def Number.r (x : Number) : List Number :=
  x.val.r.attach.map fun ⟨a, b⟩ ↦ ⟨a, x.valid.2.2 a b⟩

lemma number_in_l {a x : Number} : a ∈ x.l ↔ a.val ∈ x.val.l := by
  simp [Number.l]
  constructor
  · grind
  · intro h
    use a.val, h
    rfl

lemma number_in_r {b x : Number} : b ∈ x.r ↔ b.val ∈ x.val.r := by
  simp [Number.r]
  constructor
  · grind
  · intro h
    use b.val, h
    rfl

noncomputable instance : SizeOf Number where
  sizeOf x := sizeOf x.val

@[grind]
lemma number_sizeOf {x : Number} : sizeOf x = sizeOf x.val := by rfl

lemma list_sizeOf [SizeOf α] (l : List α) : sizeOf l = 1 + (l.map (1 + sizeOf ·)).sum := by
  induction l
  · trivial
  · grind [List.cons.sizeOf_spec]

lemma number_l_size {x : Number} : sizeOf x.val.l = sizeOf x.l := by
  simp [Number.l, list_sizeOf, number_sizeOf]

lemma number_r_size {x : Number} : sizeOf x.val.r = sizeOf x.r := by
  simp [Number.r, list_sizeOf, number_sizeOf]

@[grind]
lemma number_sizeOf_spec {x : Number} : sizeOf x = 1 + sizeOf x.l + sizeOf x.r := by
  cases _ : x.val
  grind [PseudoNumber.mk.sizeOf_spec, number_l_size, number_r_size]

@[grind]
def Number.le (x y : Number) :=
  (∀ a ∈ x.l, ¬le y a) ∧ (∀ b ∈ y.r, ¬le b x)
termination_by sizeOf x + sizeOf y
decreasing_by
  all_goals
    rename_i h
    have := List.sizeOf_lt_of_mem h
    grind

instance : LE Number where
  le x y := x.le y

@[grind]
lemma number_le {x y : Number} : LE.le x y ↔ x.le y := by rfl

lemma number_le_eq_pseudonumber_le {x y : Number} : x.val ≤ y.val ↔ x ≤ y := by
  rw [number_le, Number.le, pseudonumber_le, PseudoNumber.le]
  constructor
  · intro h
    constructor
    · intro a ha
      have := h.1 a.val (number_in_l.mp ha)
      contrapose this
      rw [not_not] at this ⊢
      exact number_le_eq_pseudonumber_le.mpr this
    · intro b hb
      have := h.2 b.val (number_in_r.mp hb)
      contrapose this
      rw [not_not] at this ⊢
      exact number_le_eq_pseudonumber_le.mpr this
  · intro h
    constructor
    · intro a ha
      have := h.1 ⟨a, x.valid.2.1 a ha⟩ (number_in_l.mpr ha)
      contrapose this
      rw [not_not] at this ⊢
      exact number_le_eq_pseudonumber_le.mp this
    · intro b hb
      have := h.2 ⟨b, y.valid.2.2 b hb⟩ (number_in_r.mpr hb)
      contrapose this
      rw [not_not] at this ⊢
      exact number_le_eq_pseudonumber_le.mp this
termination_by sizeOf x + sizeOf y
decreasing_by
  · have := List.sizeOf_lt_of_mem ha
    grind
  · have := List.sizeOf_lt_of_mem hb
    grind
  · have := List.sizeOf_lt_of_mem ha
    simp [number_sizeOf]
    cases _ : x.val
    grind [PseudoNumber.mk.sizeOf_spec]
  · have := List.sizeOf_lt_of_mem hb
    simp [number_sizeOf]
    cases _ : y.val
    grind [PseudoNumber.mk.sizeOf_spec]

lemma number_valid (x : Number) : ∀ a ∈ x.l, ∀ b ∈ x.r, ¬b ≤ a := by
  intro a ha b hb
  by_contra h
  apply number_le_eq_pseudonumber_le.mpr at h
  have := x.valid.1 a.val (number_in_l.mp ha) b.val (number_in_r.mp hb)
  grind

abbrev Number.Zero : Number := ⟨⟨[], []⟩, by grind⟩

abbrev Number.One : Number := ⟨⟨[Number.Zero.val], []⟩, by grind⟩

abbrev Number.NegOne : Number := ⟨⟨[], [Number.Zero.val]⟩, by grind⟩

example : Number.Zero ≤ Number.One := by
  rw [← number_le_eq_pseudonumber_le]
  grind

example : Number.NegOne ≤ Number.One := by
  rw [← number_le_eq_pseudonumber_le]
  grind

example : Number.Zero ≤ Number.Zero := by
  rw [← number_le_eq_pseudonumber_le]
  grind

example : Number.One ≤ Number.One := by
  rw [← number_le_eq_pseudonumber_le]
  grind

/-- T1 -/
theorem pseudonumber_trans {x y z : PseudoNumber} (hxy : x ≤ y) (hyz : y ≤ z) : x ≤ z := by
  by_contra hxz
  rw [pseudonumber_le, PseudoNumber.le] at hxy hyz hxz
  simp at hxz
  by_cases h : ∀ a ∈ x.l, ¬z ≤ a
  · obtain ⟨k, hk⟩ := hxz h
    have := @pseudonumber_trans k x y
    grind
  · simp at h
    obtain ⟨k, hk⟩ := h
    have := @pseudonumber_trans y z k
    grind
termination_by sizeOf x + sizeOf y + sizeOf z
decreasing_by
  all_goals
    cases _ : x
    cases _ : z
    have := List.sizeOf_lt_of_mem hk.1
    grind [PseudoNumber.mk.sizeOf_spec]

theorem number_trans {x y z : Number} (hxy : x ≤ y) (hyz : y ≤ z) : x ≤ z := by
  rw [← number_le_eq_pseudonumber_le] at hxy hyz ⊢
  exact pseudonumber_trans hxy hyz

/-- T2 -/
theorem number_sandwich (x : Number) : (∀ a ∈ x.l, a ≤ x) ∧ (∀ b ∈ x.r, x ≤ b) := by
  constructor
  · by_contra h
    simp at h
    obtain ⟨a, ha, h⟩ := h
    have := number_valid x
    have : ∃ aa ∈ a.l, x ≤ aa := by grind
    obtain ⟨aa, haa, haa'⟩ := this
    have := number_trans haa' <| number_sandwich a |>.1 aa haa
    have := number_sandwich a
    grind
  · by_contra h
    simp at h
    obtain ⟨b, hb, h⟩ := h
    have := number_valid x
    have : ∃ bb ∈ b.r, bb ≤ x := by grind
    obtain ⟨bb, hbb, hbb'⟩ := this
    have := number_trans (number_sandwich b |>.2 bb hbb) hbb'
    have := number_sandwich b
    grind
decreasing_by
  all_goals
    try have := List.sizeOf_lt_of_mem ha
    try have := List.sizeOf_lt_of_mem hb
    grind

/-- T3 -/
theorem pseudonumber_refl (x : PseudoNumber) : x ≤ x := by
  rw [pseudonumber_le, PseudoNumber.le]
  constructor
  · by_contra h
    simp at h
    obtain ⟨a, ha, h⟩ := h
    have := pseudonumber_refl a
    grind
  · by_contra h
    simp at h
    obtain ⟨b, hb, h⟩ := h
    have := pseudonumber_refl b
    grind
decreasing_by
  all_goals
    try have := List.sizeOf_lt_of_mem ha
    try have := List.sizeOf_lt_of_mem hb
    cases x
    grind [PseudoNumber.mk.sizeOf_spec]

/-- T4 -/
theorem number_antisymm {x y : Number} (h : ¬x ≤ y) : y ≤ x := by
  rw [number_le, Number.le] at h
  simp at h
  by_cases h' : ∀ a ∈ x.l, ¬y ≤ a
  · obtain ⟨k, hk, hkk⟩ := h h'
    exact number_trans (number_sandwich y |>.2 k hk) hkk
  · simp at h'
    obtain ⟨k, hk, hkk⟩ := h'
    exact number_trans hkk <| number_sandwich x |>.1 k hk

instance : LT Number where
  lt x y := ¬y ≤ x

@[grind, simp]
lemma number_lt {x y : Number} : LT.lt x y ↔ ¬y ≤ x := by rfl

/-- T5 -/
theorem number_trans' {x y z : Number} (hxy : x ≤ y) (hyz : y < z) : x < z := by
  contrapose hyz
  simp at hyz ⊢
  exact number_trans hyz hxy

/-- T6 -/
theorem number_trans'' {x y z : Number} (hxy : x < y) (hyz : y ≤ z) : x < z := by
  contrapose hxy
  simp at hxy ⊢
  exact number_trans hyz hxy

theorem number_trans''' {x y z : Number} (hxy : x < y) (hyz : y < z) : x < z := by
  by_contra hxz
  simp at hxz
  have := number_antisymm <| number_trans'' hyz hxz
  grind

abbrev Number.equiv (x y : Number) := x ≤ y ∧ y ≤ x

abbrev List.pseudoify (l : List Number) := l.map (·.val)

abbrev number_list_merge (x : Number) (yl yr : List Number) (hl : ∀ a ∈ yl, a < x) (hr : ∀ b ∈ yr, x < b) : Number := ⟨⟨x.val.l ++ yl.pseudoify, x.val.r ++ yr.pseudoify⟩, by
  rw [PseudoNumber.valid]
  and_intros
  · simp
    intro a ha b hb
    obtain h₁|h₂ := ha <;> obtain h₃|h₄ := hb
    · exact x.valid.1 a h₁ b h₃
    · obtain ⟨c, hc, hc'⟩ := h₄
      have := number_trans' (number_sandwich x |>.1 ⟨a, x.valid.2.1 a h₁⟩ <| number_in_l.mpr h₁) <| hr c hc
      contrapose this
      simp at this ⊢
      exact number_le_eq_pseudonumber_le.mp <| hc' ▸ this
    · obtain ⟨d, hd, hd'⟩ := h₂
      have := number_trans'' (hl d hd) <| number_sandwich x |>.2 ⟨b, x.valid.2.2 b h₃⟩ <| number_in_r.mpr h₃
      contrapose this
      simp at this ⊢
      exact number_le_eq_pseudonumber_le.mp <| hd' ▸ this
    · obtain ⟨c, hc, hc'⟩ := h₄
      obtain ⟨d, hd, hd'⟩ := h₂
      have := number_lt.mp <| number_trans''' (hl d hd) (hr c hc)
      contrapose this
      simp at this ⊢
      exact number_le_eq_pseudonumber_le.mp <| hc' ▸ (hd' ▸ this)
  · simp
    intro a ha
    obtain h₁|h₂ := ha
    · exact x.valid.2.1 a h₁
    · obtain ⟨aa, _, haa⟩ := h₂
      exact haa ▸ aa.property
  · simp
    intro b hb
    obtain h₁|h₂ := hb
    · exact x.valid.2.2 b h₁
    · obtain ⟨bb, _, hbb⟩ := h₂
      exact hbb ▸ bb.property⟩

lemma number_list_merge_l {x : Number} {yl yr : List Number} (hl : ∀ a ∈ yl, a < x) (hr : ∀ b ∈ yr, x < b) : (number_list_merge x yl yr hl hr).l = x.l ++ yl := by
  simp [number_list_merge, Number.l, List.pseudoify]
  sorry

lemma number_list_merge_r {x : Number} {yl yr : List Number} (hl : ∀ a ∈ yl, a < x) (hr : ∀ b ∈ yr, x < b) : (number_list_merge x yl yr hl hr).r = x.r ++ yr := by
  simp [number_list_merge, Number.r, List.pseudoify]
  sorry

theorem number_list_merge_equiv {x : Number} {yl yr : List Number} (hl : ∀ a ∈ yl, a < x) (hr : ∀ b ∈ yr, x < b) : x.equiv (number_list_merge x yl yr hl hr) := by
  rw [Number.equiv, number_le, Number.le, number_le, Number.le, number_list_merge_l hl hr, number_list_merge_r hl hr]
  and_intros
  ·
    intro a ha
    have := number_sandwich x |>.1
    sorry
    -- rw [Number.le]
    -- simp
  · intro b hb
    simp [List.mem_append] at hb
    obtain h₁|h₂ := hb
    · have := number_sandwich x |>.2 b h₁




      -- have := number_antisymm
    · exact hr b h₂
      -- have : b = b'' := by


      --   rw [← hb']
      --   rw [← hb.2]






  · sorry
  · sorry



def PseudoNumber.add (x y : PseudoNumber) : PseudoNumber :=
  ⟨x.l.map y.add ++ y.l.map x.add, x.r.map y.add ++ y.r.map x.add⟩
termination_by sizeOf x + sizeOf y
decreasing_by
  all_goals
    expose_names
    cases x
    cases y
    have := List.sizeOf_lt_of_mem h
    grind [PseudoNumber.mk.sizeOf_spec]

def Number.add (x y : Number) : Number :=
  ⟨x.val.add y.val, by
    rw [PseudoNumber.valid]
    and_intros
    · intro a ha b hb
    · intro a ha

  ⟩