dedekind.lean

import algebra.archimedean
import tactic

open_locale classical
noncomputable theory

/-!

# Definition of the Reals, as cuts of the rationals

Source: Appendix of Baby Rudin

-/

section
variables {α : Type*}

namespace set

lemma ne_univ_iff_exists_not_mem {s : set α} : s ≠ set.univ ↔ ∃ (a : α), a ∉ s :=
begin
  split,
  { intro h,
    rcases exists_of_ssubset (or.resolve_left 
            (set.eq_or_ssubset_of_subset (set.subset_univ s)) h) with ⟨x, hx1, hx2⟩,
    use [x, hx2] },
  { rintro ⟨x, hx⟩ rfl,
    apply hx,
    exact mem_univ _ }
end

end set
end

-- A cut is
@[ext] structure cut :=
-- a subset of ℚ
(c : set ℚ)
-- which is nonempty
(hnonempty : c.nonempty)
-- and is not equal to ℚ itself
(hneuniv : c ≠ set.univ)
-- and satisfies
(h1 : ∀ p ∈ c, ∀ q : ℚ, q < p → q ∈ c)
(h2 : ∀ p ∈ c, ∃ r ∈ c, p < r)

namespace cut

-- The reals are the Type of all cuts
notation `ℝ` := cut

lemma lt_of_mem_of_not_mem {α : ℝ} {p q : ℚ} (hpα : p ∈ α.c) (hqα : ¬ q ∈ α.c) : p < q :=
begin
  by_contra,
  rw [not_lt, le_iff_lt_or_eq] at h,
  cases h,
  { apply hqα,
    apply α.h1 p hpα _ h },
  { apply hqα,
    rwa h }
end

lemma not_mem_of_lt_of_not_mem (α : ℝ) (p q : ℚ) (hpα : ¬ p ∈ α.c) (hpq : p < q) : ¬ q ∈ α.c :=
begin
  intro h,
  apply hpα,
  apply α.h1 _ h _ hpq,
end

-- We say α < β if α ⊂ β
def lt (α β : ℝ) : Prop := α.c ⊂ β.c

-- and α ≤ β if α ⊆ β
def le (α β : ℝ) : Prop := α.c ⊆ β.c

-- Then ℝ is a linear order
instance : linear_order ℝ :=
{ le := le,
  lt := lt,
  -- Clearly, we have that α ≤ α
  le_refl := λ α, set.subset.refl α.c,
  -- and that if α ≤ β, and β ≤ γ, then α ≤ γ
  le_trans := λ α β γ, set.subset.trans,
  -- and by definition, we have that α < β ↔ α ≤ β ∧ α ≠ β
  lt_iff_le_not_le := λ α β, iff.rfl,
  -- and that if α ≤ β and β ≤ α, we get that α = β
  le_antisymm := λ α β h1 h2, cut.ext _ _ $ set.subset.antisymm h1 h2,
  -- Now, we need to show that for all α β, at least one of α ≤ β and β ≤ α holds.
  le_total := begin
    intros α β,
    -- Suffices to show that if α is not less that β, then β is less than α
    suffices : (¬le α β → le β α),
    { tauto },
    -- If ¬ α ≤ β, then there exists p ∈ α such that p ∉ β
    rintro (h : ¬α.c ⊆ β.c),
    rw set.not_subset at h,
    rcases h with ⟨p, hpα, hpβ⟩,
    -- Now for any q ∈ β,
    intros q hq,
    -- using the definition of a cut, if q < p, we get that q ∈ β
    apply α.h1 p hpα,
    apply lt_of_mem_of_not_mem hq hpβ,
  end,
  decidable_le := classical.dec_rel _,
  decidable_eq := classical.dec_rel _,
  decidable_lt := classical.dec_rel _ }

-- The Sup, but we haven't proven it's ths Sup yet
def foo (S : set ℝ) (hS : S.nonempty) (hS2 : bdd_above S) : ℝ := {
    c := ⋃ s ∈ S, cut.c s,
    hnonempty := begin
      rcases hS with ⟨x, hx⟩,
      cases x.hnonempty with t ht,
      use t,
      rw set.mem_bUnion_iff,
      use [x, hx, ht]
    end,
    hneuniv := begin
      cases hS2 with γ hγ,
      rw mem_upper_bounds at hγ,
      suffices : (⋃ s ∈ S, cut.c s) ⊆ γ.c,
      { have hγuniv : γ.c ⊂ set.univ,
        { apply or.resolve_left (set.eq_or_ssubset_of_subset (set.subset_univ _)) _,
          exact γ.hneuniv },
        apply ne_of_lt,
        change _ < _ at hγuniv, -- apparently not defeq enough for `apply`?
        apply lt_of_le_of_lt _ hγuniv,
        convert this },
      apply set.bUnion_subset,
      exact hγ,
    end,
    h1 := begin
      intros p hp q hqp,
      rw set.mem_bUnion_iff at hp ⊢,
      rcases hp with ⟨x, hxS, hx⟩,
      use [x, hxS],
      apply x.h1 p hx _ hqp,
    end,
    h2 := begin
      intros p hp,
      rw set.mem_bUnion_iff at hp,
      rcases hp with ⟨x, hxS, hx⟩,
      rcases x.h2 p hx with ⟨q, hq, hpq⟩,
      use q,
      split,
      { rw set.mem_bUnion_iff,
        use [x, hxS, hq] },
      { exact hpq }
    end }

-- The LUB property
example (S : set ℝ) (hS : S.nonempty) (hS2 : bdd_above S) : ∃ B, is_lub S B :=
begin
  set γ : ℝ := foo S hS hS2,
  use γ,
  split,
  { intros x hx,
    change x.c ⊆ (foo S hS hS2).c,
    unfold foo,
    dsimp only,
    apply set.subset_bUnion_of_mem hx },
  { intros β hβ,
    by_contra h,
    change ¬γ.c ⊆ β.c at h,
    rw set.not_subset at h,
    rcases h with ⟨a, haγ, haβ⟩,
    change a ∈ (foo S hS hS2).c at haγ,
    dsimp [foo] at haγ,
    rw set.mem_bUnion_iff at haγ,
    rcases haγ with ⟨x, hxS, hax⟩,
    specialize hβ hxS,
    apply haβ,
    apply hβ,
    exact hax }
end

def add (α β : ℝ) : ℝ :=
{ c := {z : ℚ | ∃ (x ∈ α.c) (y ∈ β.c), x + y = z},
  hnonempty := begin
    cases α.hnonempty with x hx,
    cases β.hnonempty with y hy,
    use [x + y, x, hx, y, hy],
  end,
  hneuniv := begin
    rcases set.ne_univ_iff_exists_not_mem.mp α.hneuniv with ⟨x, hx⟩,
    rcases set.ne_univ_iff_exists_not_mem.mp β.hneuniv with ⟨y, hy⟩,
    rw set.ne_univ_iff_exists_not_mem,
    use x + y,
    intro h,
    rcases h with ⟨p, hp, q, hq, h⟩,
    have h1 : p < x,
    { apply lt_of_mem_of_not_mem hp hx },
    have h2 : q < y,
    { apply lt_of_mem_of_not_mem hq hy },
    linarith,
  end,
  h1 := begin
    rintros p ⟨x, hx, y, hy, h⟩ q hq,
    refine ⟨x + (q - p),_, y, hy, _⟩,
    { apply α.h1 _ hx,
      linarith },
    { linarith }
  end,
  h2 := begin
    rintros p ⟨x, hx, y, hy, h⟩,
    rcases α.h2 x hx with ⟨r, hrα, hr⟩,
    rcases β.h2 y hy with ⟨s, hsβ, hs⟩,
    use [r + s,r,hrα,s,hsβ],
    linarith,
  end }

instance : has_add ℝ := ⟨add⟩

lemma add_comm (a b : ℝ) : a + b = b + a :=
begin
  ext,
  split;
  { rintro ⟨p, hp, q, hq, h⟩,
    use [q, hq, p, hp],
    rw [←h, add_comm] },
end

lemma add_assoc (a b c : ℝ) : (a + b) + c = a + (b + c) :=
begin
  ext,
  split,
  { rintro ⟨s, ⟨p, hp, q, ⟨hq, hqs⟩⟩, r, hr, h⟩,
    refine ⟨p, hp, q + r, ⟨q, hq, r, hr, rfl⟩, _⟩,
    linarith },
  { rintro ⟨p, hp, s, ⟨q, hq, r, ⟨hr, hrs⟩⟩, h⟩,
    refine ⟨p + q, ⟨p, hp, q, hq, rfl⟩, r, hr, _⟩,
    linarith }
end

def zero : ℝ := 
{ c := {q : ℚ | q < 0},
  hnonempty := ⟨-1, show (-1 : ℚ) < 0, by norm_num⟩,
  hneuniv := set.ne_univ_iff_exists_not_mem.mpr ⟨1, λ (h : 1 < 0), by linarith⟩,
  h1 := begin
    rintros p (hp : p < 0) q hq,
    change q < 0,
    linarith,
  end,
  h2 := begin
    rintros p (hp : p < 0),
    refine ⟨p/2, (_ : p/2 < 0), _⟩; 
      linarith
  end }

instance : has_zero ℝ := ⟨zero⟩

lemma zero_add (a : ℝ) : 0 + a = a :=
begin
  ext,
  split,
  { rintro ⟨p, (hp : p < 0), q, hq, h⟩,
    apply a.h1 _ hq,
    linarith },
  { intro h,
    rcases a.h2 x h with ⟨w, hw1, hw2⟩,
    refine ⟨x - w, (_ : x - w < 0), w, hw1, _⟩;
    linarith }
end

lemma add_zero (a : ℝ) : a + 0 = a :=
begin
  rw [add_comm, zero_add]
end

def neg (a : ℝ) : ℝ :=
{ c := { p : ℚ | ∃ r > 0, - p - r ∉ a.c },
  hnonempty := begin
    rcases set.ne_univ_iff_exists_not_mem.mp a.hneuniv with ⟨s, hs⟩,
    refine ⟨-s-1, 1, zero_lt_one, _⟩,
    convert hs,
    ring,
  end,
  hneuniv := begin
    cases a.hnonempty with p hp,
    rw set.ne_univ_iff_exists_not_mem,
    use -p,
    rintro ⟨r, hr, h⟩,
    apply h,
    apply a.h1 p hp,
    linarith,
  end,
  h1 := begin
    rintros p ⟨r, hr, h⟩ q hqp,
    use [r, hr],
    intro hqr,
    apply h,
    apply a.h1 _ hqr,
    linarith,
  end,
  h2 := begin
    rintros p ⟨r, hr, h⟩,
    refine ⟨p + r/2, ⟨r/2, half_pos hr, _⟩, _, _⟩,
    { convert h using 2,
      linarith },
    { linarith },
    { linarith }
  end }

instance : has_neg ℝ := ⟨neg⟩

-- name?
lemma c_bdd_above (a : ℝ) : bdd_above a.c :=
begin
  by_contra h,
  rw not_bdd_above_iff at h,
  rcases set.ne_univ_iff_exists_not_mem.mp a.hneuniv with ⟨s, hs⟩,
  rcases h s with ⟨x, hx1, hx2⟩,
  have := lt_of_mem_of_not_mem hx1 hs,
  linarith,
end

lemma archim {S : set ℚ} (hS : bdd_above S) (a : ℚ) (ha : 0 < a) : ∃ (n : ℤ), (n * a : ℚ) ∈ S ∧ ((n + 1) * a : ℚ) ∉ S :=
begin
  sorry,
end

lemma add_left_neg (a : ℝ) : -a + a = 0 :=
begin
  ext z,
  split,
  { rintro ⟨x, ⟨r, hr, hrx⟩, y, hy, h⟩,
    set s := - x - r with hs,
    have : y < s,
    { apply lt_of_mem_of_not_mem hy hrx },
    change z < 0,
    rw ←h,
    linarith },
  { rintros (hz : z < 0),
    set w := -z/2 with hw,
    have hwpos : 0 < w,
    { linarith },
    rcases archim (c_bdd_above a) w hwpos with ⟨n, hn1, hn2⟩,
    refine ⟨- (n + 2) * w, ⟨w, hwpos, _⟩, n * w, hn1, _⟩,
    { convert hn2,
      ring },
    { rw hw, linarith } }
end

instance : add_comm_group ℝ :=
{ add := add,
  add_assoc := add_assoc,
  zero := zero,
  zero_add := zero_add,
  add_zero := add_zero,
  neg := neg,
  add_left_neg := add_left_neg,
  add_comm := add_comm }

instance : linear_ordered_add_comm_group ℝ :=
{ add_le_add_left := begin
  rintro a b hab c p ⟨x, hx, y, hy, h⟩,
  specialize hab hy,
  use [x, hx, y, hab, h],
  end, ..cut.add_comm_group, ..cut.linear_order }

end cut

def preal := {x : ℝ // 0 < x}

notation `ℝ+` := preal

namespace preal

lemma exists_pos_rat (a : ℝ+) : ∃ (r : ℚ) (h : r > 0), r ∈ a.val.c :=
begin
  rcases a with ⟨a, ha⟩,
  change (0 : ℝ).c ⊂ a.c at ha,
  rcases set.exists_of_ssubset ha with ⟨r, hr, hr0⟩,
  change ¬r < 0 at hr0,
  rw not_lt at hr0,
  rcases le_iff_lt_or_eq.mp hr0 with (h|rfl),
  { use [r, h, hr] },
  { rcases a.h2 _ hr with ⟨t, ht, h⟩,
    use [t, h, ht] }
end

def mul (a b : ℝ+) : ℝ+ :=
⟨{ c := {x | ∃ (r ∈ a.val.c) (s ∈ b.val.c), 0 < r ∧ 0 < s ∧ x ≤ r * s},
  hnonempty := begin
    rcases exists_pos_rat a with ⟨r, hr0, hr⟩,
    rcases exists_pos_rat b with ⟨s, hs0, hs⟩,
    refine ⟨r*s, r, hr, s, hs, hr0, hs0, le_refl _⟩,
  end,
  hneuniv := begin
    rcases set.ne_univ_iff_exists_not_mem.mp a.1.hneuniv with ⟨t, ht⟩,
    rcases set.ne_univ_iff_exists_not_mem.mp b.1.hneuniv with ⟨u, hu⟩,
    rw set.ne_univ_iff_exists_not_mem,
    use u * t,
    rintro ⟨r, hr, s, hs, hr0, hs0, hrs⟩,
    have hsu : s < u := cut.lt_of_mem_of_not_mem hs hu,
    have hrt : r < t := cut.lt_of_mem_of_not_mem hr ht,
    nlinarith,
  end,
  h1 := begin
    rintros p ⟨r, hr, s, hs, hr0, hs0, hprs⟩ q hq,
    use [r, hr, s, hs, hr0, hs0],
    apply le_of_lt,
    apply lt_of_lt_of_le hq hprs,
  end,
  h2 := begin
    rintros p ⟨r, hr, s, hs, hr0, hs0, hrs⟩,
    rcases a.1.h2 _ hr with ⟨t, ht, hrt⟩,
    rcases b.1.h2 _ hs with ⟨u, hu, hsu⟩,
    refine ⟨t * u, ⟨t, ht, u, hu, _, _, le_refl _⟩, _⟩,
    { linarith },
    { linarith },
    apply lt_of_le_of_lt hrs,
    apply mul_lt_mul hrt (le_of_lt hsu) hs0 (le_of_lt (lt_trans hr0 hrt)),
  end },
  begin
    change _ ⊂ _,
    dsimp,
    rw set.ssubset_iff_of_subset,
    { use 0,
      rcases exists_pos_rat a with ⟨r, hr0, hr⟩,
      rcases exists_pos_rat b with ⟨s, hs0, hs⟩,
      split,
      { use [r, hr, s, hs, hr0, hs0],
        nlinarith },
      { rintro (h : (0 : ℚ) < 0),
        linarith } },
    { rintro x (hx : x < 0),
      rcases exists_pos_rat a with ⟨r, hr0, hr⟩,
      rcases exists_pos_rat b with ⟨s, hs0, hs⟩,
      use [r, hr, s, hs, hr0, hs0],
      nlinarith }
  end⟩

.

def one : ℝ+ := 
⟨{ c := {x | x < 1},
  hnonempty := ⟨0, show (0 : ℚ) < 1, by norm_num⟩,
  hneuniv := set.ne_univ_iff_exists_not_mem.mpr ⟨2, show ¬ (2 : ℚ) < 1, by norm_num⟩,
  h1 := begin
    rintros p (hp : p < 1) q hqp,
    change q < 1,
    linarith,
  end,
  h2 := begin
    rintros p (hp : p < 1),
    refine ⟨(p + 1)/2, (_ : (p + 1)/2 < 1), _⟩,
    { linarith },
    { linarith }
  end },
  begin
    change _ ⊂ _,
    dsimp,
    rw set.ssubset_iff_of_subset,
    { refine ⟨(1/2), (_ : 1/2 < 1), (_ : ¬ 1/2 < 0)⟩,
      { norm_num },
      { norm_num } },
    { rintro x (hx : x < 0),
      apply lt_trans hx zero_lt_one }
  end⟩

.

instance : has_mul ℝ+ := ⟨mul⟩
instance : has_one ℝ+ := ⟨one⟩

lemma mul_comm (a b : ℝ+) : a * b = b * a :=
begin
  ext,
  split;
  { rintros ⟨p, hp, q, hq, hp0, hq0, hpq⟩,
    refine ⟨q, hq, p, hp, hq0, hp0, _⟩,
    convert hpq using 1,
    rw mul_comm },
end

lemma mul_assoc (a b c : ℝ+) : a * b * c = a * (b * c) :=
begin
  ext,
  split,
  { rintro ⟨p, ⟨q, hq, s, hs, hq0, hs0, hqs⟩, t, ht, hp0, ht0, hpt⟩,
    refine ⟨q, hq, s * t, ⟨s, hs, t, ht, hs0, ht0, le_refl _⟩, hq0, _, _⟩;
    nlinarith },
  { rintro ⟨p, hp, q, ⟨s, hs, t, ht, hs0, ht0, hst⟩, hp0, hq0, hpq⟩,
    refine ⟨p * s, ⟨p, hp, s, hs, hp0, hs0, le_refl _⟩, t, ht, _, ht0, _⟩;
    nlinarith }
end

lemma one_mul (a b c : ℝ+) : 1 * a = a :=
begin
  ext,
  split,
  { rintro ⟨p, (hp : p < 1), q, hq, hp0, hq0, hpq⟩,
    apply a.1.h1 _ hq,
    nlinarith },
  { rintro h,
    rcases a.1.h2 _ h with ⟨x', hx', hx'x⟩,
    set y := x/x',
    refine ⟨y, (_ : y < 1), x', _, _, _, _⟩,
    all_goals { sorry },
   }
end

end preal