More basic theorems about surreal ≤

Changes

1 changed files (+84/-29)

• Surreal.lean
  • @@ -18,7 +18,7 @@ decreasing_by
    @[grind] def SurBase.valid (x : SurBase) := - (∀ a ∈ x.l, ∀ b ∈ x.r, a.le b) ∧ (x.l.Nodup ∧ ∀ a ∈ x.l, a.valid) ∧ (x.r.Nodup ∧ ∀ b ∈ x.r, b.valid) + (∀ a ∈ x.l, ∀ b ∈ x.r, ¬b.le a) ∧ (x.l.Nodup ∧ ∀ a ∈ x.l, a.valid) ∧ (x.r.Nodup ∧ ∀ b ∈ x.r, b.valid) decreasing_by all_goals expose_names
  • @@ -47,12 +47,12 @@ lemma sur_in_l {a x : Sur} : a ∈ x.l ↔ a.val ∈ x.val.l := by
    use a.val, h rfl - lemma sur_in_r {a x : Sur} : a ∈ x.r ↔ a.val ∈ x.val.r := by + lemma sur_in_r {b x : Sur} : b ∈ x.r ↔ b.val ∈ x.val.r := by simp [Sur.r] constructor · grind · intro h - use a.val, h + use b.val, h rfl noncomputable instance : SizeOf Sur where
  • @@ -135,9 +135,12 @@ decreasing_by
    cases _ : y.val grind [SurBase.mk.sizeOf_spec] - lemma sur_valid (x : Sur) : ∀ a ∈ x.l, ∀ b ∈ x.r, a ≤ b := by + lemma sur_valid (x : Sur) : ∀ a ∈ x.l, ∀ b ∈ x.r, ¬b ≤ a := by intro a ha b hb - exact sur_le_eq_surbase_le.mp <| x.valid.1 a.val (sur_in_l.mp ha) b.val (sur_in_r.mp hb) + by_contra h + apply sur_le_eq_surbase_le.mpr at h + have := x.valid.1 a.val (sur_in_l.mp ha) b.val (sur_in_r.mp hb) + grind abbrev Sur.Zero : Sur := ⟨⟨[], []⟩, by grind⟩
  • @@ -161,17 +164,17 @@ example : Sur.One ≤ Sur.One := by
    rw [← sur_le_eq_surbase_le] grind - theorem sur_trans (x y z : Sur) (hxy : x ≤ y) (hyz : y ≤ z) : x ≤ z := by + theorem sur_trans {x y z : Sur} (hxy : x ≤ y) (hyz : y ≤ z) : x ≤ z := by by_contra hxz rw [sur_le, Sur.le] at hxy hyz hxz simp at hxz by_cases h : ∀ a ∈ x.l, ¬z ≤ a · obtain ⟨k, hk⟩ := hxz h - have := sur_trans k x y + have := @sur_trans k x y grind · simp at h obtain ⟨k, hk⟩ := h - have := sur_trans y z k + have := @sur_trans y z k grind termination_by sizeOf x + sizeOf y + sizeOf z decreasing_by
  • @@ -179,31 +182,83 @@ decreasing_by
    have := List.sizeOf_lt_of_mem hk.1 grind - lemma sur_sandwich (x : Sur) : ∀ a ∈ x.val.l, a.le l - - lemma Sur.refl (x : Sur) : x ≤ x := by - by_contra hx - rw [sur_le, SurBase.le] at hx - simp at hx - by_cases h : ∀ a ∈ x.val.l, ¬x.val.le a - · obtain ⟨k, hk⟩ := hx h - - - - + theorem sur_sandwich (x : Sur) : (∀ a ∈ x.l, a ≤ x) ∧ (∀ b ∈ x.r, x ≤ b) := by + constructor + · by_contra h + simp at h + obtain ⟨a, ha, h⟩ := h + have := sur_valid x + have : ∃ aa ∈ a.l, x ≤ aa := by grind + obtain ⟨aa, haa, haa'⟩ := this + have := sur_trans haa' <| sur_sandwich a |>.1 aa haa + have := sur_sandwich a grind - · simp at h - obtain ⟨k, hk⟩ := h - + · by_contra h + simp at h + obtain ⟨b, hb, h⟩ := h + have := sur_valid x + have : ∃ bb ∈ b.r, bb ≤ x := by grind + obtain ⟨bb, hbb, hbb'⟩ := this + have := sur_trans (sur_sandwich b |>.2 bb hbb) hbb' + have := sur_sandwich b + grind + decreasing_by + · have := List.sizeOf_lt_of_mem ha + grind + · have := List.sizeOf_lt_of_mem hb grind + theorem sur_refl (x : Sur) : x ≤ x := by + rw [sur_le, Sur.le] + constructor + · by_contra h + simp at h + obtain ⟨a, ha, h⟩ := h + have := sur_refl a + grind + · by_contra h + simp at h + obtain ⟨b, hb, h⟩ := h + have := sur_refl b + grind + decreasing_by + · have := List.sizeOf_lt_of_mem ha + grind + · have := List.sizeOf_lt_of_mem hb + grind - -- have := x.property - -- unfold SurBase.correct at this - -- unfold SurBase.le - -- grind - - + theorem sur_antisymm {x y : Sur} (h : ¬x ≤ y) : y ≤ x := by + rw [sur_le, Sur.le] at h + simp at h + by_cases h' : ∀ a ∈ x.l, ¬y ≤ a + · obtain ⟨k, hk, hkk⟩ := h h' + have := sur_sandwich y |>.2 k hk + exact sur_trans this hkk + · simp at h' + obtain ⟨k, hk, hkk⟩ := h' + have := sur_sandwich x |>.1 k hk + exact sur_trans hkk this + + instance : LT Sur where + lt x y := ¬y ≤ x + + @[grind, simp] + lemma sur_lt {x y : Sur} : LT.lt x y ↔ ¬y ≤ x := by rfl + + theorem sur_trans' {x y z : Sur} (hxy : x ≤ y) (hyz : y < z) : x < z := by + contrapose hyz + simp at hyz ⊢ + exact sur_trans hyz hxy + + theorem sur_trans'' {x y z : Sur} (hxy : x < y) (hyz : y ≤ z) : x < z := by + contrapose hxy + simp at hxy ⊢ + exact sur_trans hyz hxy + + -- instance : PartialOrder Sur where + -- le_trans := sur_trans + -- le_refl := sur_refl + -- le_antisymm := sur_antisymm -- abbrev SurBase.correct (x : SurBase) := -- ∀ a ∈ x.l, ∀ b ∈ x.r, a.le b