More random surreal stuff

Changes

1 changed files (+101/-6)

• Surreal.lean
  • @@ -1,5 +1,9 @@
    import Mathlib + -- Based on Knuth's book "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
  • @@ -79,7 +83,7 @@ lemma number_r_size {x : Number} : sizeOf x.val.r = sizeOf x.r := by
    simp [Number.r, list_sizeOf, number_sizeOf] @[grind] - lemma sur_sizeOf_spec {x : Number} : sizeOf x = 1 + sizeOf x.l + sizeOf x.r := by + 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]
  • @@ -170,6 +174,7 @@ 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
  • @@ -194,6 +199,7 @@ theorem number_trans {x y z : Number} (hxy : x ≤ y) (hyz : y ≤ z) : x ≤ z
    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
  • @@ -220,6 +226,7 @@ decreasing_by
    try have := List.sizeOf_lt_of_mem hb grind + /-- T3 -/ theorem pseudonumber_refl (x : PseudoNumber) : x ≤ x := by rw [pseudonumber_le, PseudoNumber.le] constructor
  • @@ -240,17 +247,16 @@ decreasing_by
    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' - have := number_sandwich y |>.2 k hk - exact number_trans this hkk + exact number_trans (number_sandwich y |>.2 k hk) hkk · simp at h' obtain ⟨k, hk, hkk⟩ := h' - have := number_sandwich x |>.1 k hk - exact number_trans hkk this + exact number_trans hkk <| number_sandwich x |>.1 k hk instance : LT Number where lt x y := ¬y ≤ x
  • @@ -258,17 +264,106 @@ instance : LT Number where
    @[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 - abbrev equiv (x y : Number) := x ≤ y ∧ y ≤ x + 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⟩