/Surreal.lean at 210c8f5a0c3b908aceaff0ac4aad69ae862c39a4

import Mathlib

structure SurBase where
  l : List SurBase
  r : List SurBase

@[grind]
def SurBase.le (x 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]

@[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)
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.valid }

def Sur.valid (x : Sur) := by
  have := x.property
  unfold SurBase.valid at this
  exact this

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

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

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

lemma sur_in_r {a x : Sur} : a ∈ x.r ↔ a.val ∈ x.val.r := by
  simp [Sur.r]
  constructor
  · grind
  · intro h
    use a.val, h
    rfl

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

@[grind]
lemma sur_sizeOf {x : Sur} : 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 sur_l_size {x : Sur} : sizeOf x.val.l = sizeOf x.l := by
  simp [Sur.l, list_sizeOf, sur_sizeOf]

lemma sur_r_size {x : Sur} : sizeOf x.val.r = sizeOf x.r := by
  simp [Sur.r, list_sizeOf, sur_sizeOf]

@[grind]
lemma sur_sizeOf_spec {x : Sur} : sizeOf x = 1 + sizeOf x.l + sizeOf x.r := by
  cases _ : x.val
  grind [SurBase.mk.sizeOf_spec, sur_l_size, sur_r_size]

@[grind]
def Sur.le (x y : Sur) :=
  (∀ 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 Sur where
  le x y := x.le y

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

lemma sur_le_eq_surbase_le {x y : Sur} : x.val.le y.val ↔ x ≤ y := by
  rw [sur_le, Sur.le, SurBase.le]
  constructor
  · intro h
    constructor
    · intro a ha
      have := h.1 a.val (sur_in_l.mp ha)
      contrapose this
      rw [not_not] at this ⊢
      exact sur_le_eq_surbase_le.mpr this
    · intro b hb
      have := h.2 b.val (sur_in_r.mp hb)
      contrapose this
      rw [not_not] at this ⊢
      exact sur_le_eq_surbase_le.mpr this
  · intro h
    constructor
    · intro a ha
      have := h.1 ⟨a, x.valid.2.1.2 a ha⟩ (sur_in_l.mpr ha)
      contrapose this
      rw [not_not] at this ⊢
      exact sur_le_eq_surbase_le.mp this
    · intro b hb
      have := h.2 ⟨b, y.valid.2.2.2 b hb⟩ (sur_in_r.mpr hb)
      contrapose this
      rw [not_not] at this ⊢
      exact sur_le_eq_surbase_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 [sur_sizeOf]
    cases _ : x.val
    grind [SurBase.mk.sizeOf_spec]
  · have := List.sizeOf_lt_of_mem hb
    simp [sur_sizeOf]
    cases _ : y.val
    grind [SurBase.mk.sizeOf_spec]

lemma sur_valid (x : Sur) : ∀ a ∈ x.l, ∀ b ∈ x.r, a ≤ b := 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)

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

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

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

example : Sur.Zero ≤ Sur.One := by
  rw [← sur_le_eq_surbase_le]
  grind

example : Sur.NegOne ≤ Sur.One := by
  rw [← sur_le_eq_surbase_le]
  grind

example : Sur.Zero ≤ Sur.Zero := by
  rw [← sur_le_eq_surbase_le]
  grind

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
  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
    grind
  · simp at h
    obtain ⟨k, hk⟩ := h
    have := sur_trans y z k
    grind
termination_by sizeOf x + sizeOf y + sizeOf z
decreasing_by
  all_goals
    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




    grind
  · simp at h
    obtain ⟨k, hk⟩ := h

    grind


  -- have := x.property
  -- unfold SurBase.correct at this
  -- unfold SurBase.le
  -- grind



-- abbrev SurBase.correct (x : SurBase) :=
--   ∀ a ∈ x.l, ∀ b ∈ x.r, a.le b

-- instance : LE SurBase where
--   le := SurBase.le

-- structure Sur extends SurBase where
--   h : SurBase.mk l r |>.correct
--    hl : ∀ x ∈ l, x.correct
--   hr : ∀ x ∈ r, x.correct


-- inductive Sur : SurBase → Prop where
--   | zero : Sur ⟨[], []⟩
--   | step : ∀ x, ∀ a ∈ x.l, ∀ b ∈ x.r, Sur a → Sur b → a ≤ b → Sur x


-- #print SurBase

--   structure le (x y : SurBase) where
--     blah : Prop := fun x y ↦ (∀ a ∈ x.l, ¬le y a) ∧ (∀ b ∈ y.r, ¬le b x)
-- end
  -- 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⟩))





-- structure Sur where
--   l : List Sur
--   r : List Sur
--   h : ∀ x ∈ l, ∀ y ∈ r, @SurBase.le [show SurBase Sur by grind] x y




-- import Mathlib

-- structure SurBase where
--   l : List SurBase
--   r : List SurBase

-- @[grind]
-- def SurBase.le (x 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]

-- @[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)
-- 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.valid }

-- noncomputable instance : SizeOf Sur where
--   sizeOf x := sizeOf x.val

-- lemma sur_sizeOf {x : Sur} : sizeOf x = sizeOf x.val := by rfl

-- noncomputable instance : SizeOf (Finset Sur) where
--   sizeOf f := sizeOf f.toList

-- lemma finset_sur_sizeOf (f : Finset Sur) : sizeOf f = sizeOf f.toList := by rfl

-- def Sur.valid (x : Sur) := by
--   have := x.property
--   unfold SurBase.valid at this
--   exact this

-- def Sur.l (x : Sur) : Finset Sur :=
--   @Finset.mk SurBase x.val.l x.valid.2.1.1 |>.attach.map
--     ⟨fun ⟨a, b⟩ ↦ ⟨a, x.valid.2.1.2 a b⟩, by grind [Function.Injective]⟩

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

-- example (x : Sur) : x.val.l = x.l.toList.map (·.val) := by
--   simp [Sur.l]
--   -- apply?


-- -- example (x : Sur) : x.val.l = x.l := by
-- --   simp [Sur.l, finset_sur_sizeOf, finset_sur_sizeOf]
-- --   have := x.valid.2.1.1
-- --   grind

-- def Sur.r (x : Sur) : Finset Sur :=
--   @Finset.mk SurBase x.val.r x.valid.2.2.1 |>.attach.map
--     ⟨fun ⟨a, b⟩ ↦ ⟨a, x.valid.2.2.2 a b⟩, by grind [Function.Injective]⟩

-- lemma sur_in_r {a x : Sur} : a ∈ x.r ↔ a.val ∈ x.val.r := by
--   simp [Sur.r]
--   constructor
--   · grind
--   · intro h
--     use a.val, h
--     rfl

-- lemma sur_sizeOf_spec (x : Sur) : sizeOf x = 1 + sizeOf x.l + sizeOf x.r := by
--   rw [sur_sizeOf]
--   cases _ : x.val
--   rw [SurBase.mk.sizeOf_spec]
--   sorry


-- #check SurBase.mk.sizeOf_spec

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

--     --simp only [sur_sizeOf]
--     -- rename_i h
--     -- apply sur_in_l at h
--     sorry



--   · sorry
--   -- all_goals
--     -- expose_names
--     -- cases x
--     -- cases y
--     -- have := List.sizeOf_lt_of_mem h
--     -- grind [SurBase.mk.sizeOf_spec]

-- instance : LE Sur where
--   le x y := x.le y

-- @[grind]
-- lemma sur_le {x y : Sur} : LE.le x y ↔ x.le y := by rfl

-- lemma sur_le_eq_surbase_le {x y : Sur} : x.val.le y.val ↔ x ≤ y := by
--   rw [sur_le, Sur.le, SurBase.le]
--   constructor
--   · intro h
--     constructor
--     · intro a ha
--       have := h.1 a.val (sur_in_l.mp ha)
--       contrapose this
--       rw [not_not] at this ⊢
--       exact sur_le_eq_surbase_le.mpr this
--     · intro b hb
--       have := h.2 b.val (sur_in_r.mp hb)
--       contrapose this
--       rw [not_not] at this ⊢
--       exact sur_le_eq_surbase_le.mpr this
--   · intro h
--     constructor
--     · intro a ha
--       have := h.1 ⟨a, x.valid.2.1.2 a ha⟩ (sur_in_l.mpr ha)
--       contrapose this
--       rw [not_not] at this ⊢
--       exact sur_le_eq_surbase_le.mp this
--     · intro b hb
--       have := h.2 ⟨b, y.valid.2.2.2 b hb⟩ (sur_in_r.mpr hb)
--       contrapose this
--       rw [not_not] at this ⊢
--       exact sur_le_eq_surbase_le.mp this
-- termination_by sizeOf x + sizeOf y
-- decreasing_by
--   sorry


-- lemma sur_valid (x : Sur) : ∀ a ∈ x.l, ∀ b ∈ x.r, a ≤ b := 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)




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

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

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

-- example : Sur.Zero ≤ Sur.One := by grind

-- example : Sur.NegOne ≤ Sur.One := by grind

-- example : Sur.Zero ≤ Sur.Zero := by grind

-- example : Sur.One ≤ Sur.One := by grind

-- lemma 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, _⟩ := hxz h
--     have := sur_trans k x y
--     grind
--   · simp at h
--     obtain ⟨k, _⟩ := h
--     have := sur_trans y z k
--     grind
-- termination_by sizeOf x + sizeOf y + sizeOf z
-- decreasing_by
--   all_goals
--     sorry
--     -- cases _ : x.val
--     -- cases _ : z.val
--     -- have := List.sizeOf_lt_of_mem hk.1
--     -- grind [SurBase.mk.sizeOf_spec]

-- 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




--     grind
--   · simp at h
--     obtain ⟨k, hk⟩ := h

--     grind


--   -- have := x.property
--   -- unfold SurBase.correct at this
--   -- unfold SurBase.le
--   -- grind



-- -- abbrev SurBase.correct (x : SurBase) :=
-- --   ∀ a ∈ x.l, ∀ b ∈ x.r, a.le b

-- -- instance : LE SurBase where
-- --   le := SurBase.le

-- -- structure Sur extends SurBase where
-- --   h : SurBase.mk l r |>.correct
-- --    hl : ∀ x ∈ l, x.correct
-- --   hr : ∀ x ∈ r, x.correct


-- -- inductive Sur : SurBase → Prop where
-- --   | zero : Sur ⟨[], []⟩
-- --   | step : ∀ x, ∀ a ∈ x.l, ∀ b ∈ x.r, Sur a → Sur b → a ≤ b → Sur x


-- -- #print SurBase

-- --   structure le (x y : SurBase) where
-- --     blah : Prop := fun x y ↦ (∀ a ∈ x.l, ¬le y a) ∧ (∀ b ∈ y.r, ¬le b x)
-- -- end
--   -- 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⟩))





-- -- structure Sur where
-- --   l : List Sur
-- --   r : List Sur
-- --   h : ∀ x ∈ l, ∀ y ∈ r, @SurBase.le [show SurBase Sur by grind] x y