More surreal stuff

Changes

1 changed files (+432/-42)

• Surreal.lean
  • @@ -4,14 +4,8 @@ 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) := + 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
  • @@ -22,14 +16,9 @@ decreasing_by
    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) + 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
  • @@ -37,66 +26,171 @@ decreasing_by
    have := List.sizeOf_lt_of_mem h grind [SurBase.mk.sizeOf_spec] - def Sur := { x : SurBase // x.correct } + 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] - def SurZero : Sur := ⟨⟨[], []⟩, by 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] - def SurOne : Sur := ⟨⟨[SurZero.val], []⟩, by 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 SurNegOne : Sur := ⟨⟨[], [SurZero.val]⟩, by 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] - example : SurZero.val.le SurOne.val := by + 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 : SurNegOne.val.le SurOne.val := by + example : Sur.NegOne ≤ Sur.One := by + rw [← sur_le_eq_surbase_le] grind - example : SurZero.val.le SurZero.val := by + example : Sur.Zero ≤ Sur.Zero := by + rw [← sur_le_eq_surbase_le] grind - example : SurOne.val.le SurOne.val := by + example : Sur.One ≤ Sur.One := by + rw [← sur_le_eq_surbase_le] 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 + theorem sur_trans (x y z : Sur) (hxy : x ≤ y) (hyz : y ≤ z) : x ≤ z := by by_contra hxz - unfold SurBase.le at hxy hyz hxz + rw [sur_le, Sur.le] at hxy hyz hxz simp at hxz - by_cases h : ∀ a ∈ x.val.l, ¬z.val.le a + by_cases h : ∀ a ∈ x.l, ¬z ≤ 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 + have := sur_trans k 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⟩ + have := sur_trans y z k grind - termination_by sizeOf x.val + sizeOf y.val + sizeOf z.val + termination_by sizeOf x + sizeOf y + sizeOf z 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 + all_goals have := List.sizeOf_lt_of_mem hk.1 - grind [SurBase.mk.sizeOf_spec] + grind + lemma sur_sandwich (x : Sur) : ∀ a ∈ x.val.l, a.le l - lemma Sur_refl (x : Sur) : x.val.le x.val := by + lemma Sur.refl (x : Sur) : x ≤ x := by by_contra hx - unfold SurBase.le at 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
  • @@ -108,3 +202,299 @@ lemma Sur_refl (x : Sur) : x.val.le x.val := by
    -- 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