Surreal number experiments

Changes

1 changed files (+110/-0)

• Surreal.lean (new)
  • @@ -0,0 +1,110 @@
    + import Mathlib + + structure SurBase where + l : List SurBase + r : List SurBase + + -- h : ∀ x ∈ l, ∀ y ∈ r, + + --match a, b with + -- | SurBase.mk xl xr _, ⟨yl, yr, _⟩ => + -- (∀ a ∈ xl, ¬le ⟨yl, yr⟩ a) ∧ (∀ b ∈ yr, ¬le b ⟨xl, xr⟩)) + + @[grind] + def SurBase.le (x : SurBase) (y : SurBase) := + (∀ 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 [SurBase.mk.sizeOf_spec] + + -- structure Sur where + -- l : List Sur + -- r : List Sur + -- h : ∀ x ∈ l, ∀ y ∈ r, SurBase.le ⟨x.l, x.r⟩ ⟨y.l, y.r⟩ + + @[grind] + def SurBase.correct (x : SurBase) := + (∀ a ∈ x.l, ∀ b ∈ x.r, a.le b) ∧ (∀ a ∈ x.l, a.correct) ∧ (∀ b ∈ x.r, b.correct) + decreasing_by + all_goals + expose_names + cases x + have := List.sizeOf_lt_of_mem h + grind [SurBase.mk.sizeOf_spec] + + def Sur := { x : SurBase // x.correct } + + @[grind] + def SurZero : Sur := ⟨⟨[], []⟩, by grind⟩ + + @[grind] + def SurOne : Sur := ⟨⟨[SurZero.val], []⟩, by grind⟩ + + @[grind] + def SurNegOne : Sur := ⟨⟨[], [SurZero.val]⟩, by grind⟩ + + example : SurZero.val.le SurOne.val := by + grind + + example : SurNegOne.val.le SurOne.val := by + grind + + example : SurZero.val.le SurZero.val := by + grind + + example : SurOne.val.le SurOne.val := by + grind + + lemma Sur_trans (x y z : Sur) (hxy : x.val.le y.val) (hyz : y.val.le z.val) : x.val.le z.val := by + by_contra hxz + unfold SurBase.le at hxy hyz hxz + simp at hxz + by_cases h : ∀ a ∈ x.val.l, ¬z.val.le a + · obtain ⟨k, hk⟩ := hxz h + have := Sur_trans ⟨k, by + have := z.property + unfold SurBase.correct at this + exact this.2.2 k hk.1⟩ x y + grind + · simp at h + obtain ⟨k, hk⟩ := h + have := Sur_trans y z ⟨k, by + have := x.property + unfold SurBase.correct at this + exact this.2.1 k hk.1⟩ + grind + termination_by sizeOf x.val + sizeOf y.val + sizeOf z.val + decreasing_by + all_goals expose_names + · cases _ : z.val + have := List.sizeOf_lt_of_mem hk.1 + grind [SurBase.mk.sizeOf_spec] + · cases _ : x.val + have := List.sizeOf_lt_of_mem hk.1 + grind [SurBase.mk.sizeOf_spec] + + + lemma Sur_refl (x : Sur) : x.val.le x.val := by + by_contra hx + unfold SurBase.le at hx + simp at hx + by_cases h : ∀ a ∈ x.val.l, ¬x.val.le a + · obtain ⟨k, hk⟩ := hx h + + + grind + · simp at h + obtain ⟨k, hk⟩ := h + + grind + + + -- have := x.property + -- unfold SurBase.correct at this + -- unfold SurBase.le + -- grind