rational.lean

import tactic

/-
I define ℤ⁺ to use for denominators, so that no proofs are required to construct rationals.
-/

/-- Strictly positive integers -/
inductive posint : Type
  | one : posint
  | succ : posint → posint

notation `ℤ⁺` := posint

namespace posint

  open posint

  private def add : ℤ⁺ → ℤ⁺ → ℤ⁺
    | one y := y.succ
    | (succ x) y := (x.add y).succ
  private def mul : ℤ⁺ → ℤ⁺ → ℤ⁺
    | one y := y
    | (succ x) y := add y (x.mul y)

  instance : has_one ℤ⁺ := ⟨one⟩
  instance : has_add ℤ⁺ := ⟨add⟩
  instance : has_mul ℤ⁺ := ⟨mul⟩

  variables x y z : ℤ⁺

  @[simp] lemma one_add : one + y = y.succ := rfl
  @[simp] lemma succ_add : x.succ + y = (x + y).succ := rfl
  @[simp] lemma one_mul : one * y = y := rfl
  @[simp] lemma succ_mul : x.succ * y = y + x * y := rfl

  lemma add_comm : x + y = y + x :=
  begin
    revert y,
    induction x with x,
    {
      intros y,
      induction y with y,
      {
        refl,
      },
      simpa,
    },
    intros y,
    induction y with y,
    {
      simp *,
    },
    simp [x_ih, y_ih.symm],
  end

  lemma add_assoc : x + (y + z) = x + y + z :=
  begin
    induction x with x,
    {
      refl,
    },
    simpa,
  end

  lemma add_swap₃ : x + y + z = x + z + y :=
  begin
    rw [← add_assoc, add_comm y, add_assoc],
  end

  @[simp]
  lemma mul_one : x * one = x :=
  begin
    induction x with x,
    {
      refl,
    },
    simpa,
  end

  lemma mul_distrib_left : x * (y + z) = x * y + x * z :=
  begin
    induction x with x,
    {
      refl,
    },
    simp [add_assoc, add_swap₃, *],
  end

  lemma mul_comm : x * y = y * x :=
  begin
    revert y,
    induction x with x,
    {
      simp,
    },
    intros y,
    induction y with y,
    {
      simp,
    },
    simp [y_ih.symm, x_ih, add_assoc],
    simp only [add_comm],
  end

  lemma right_distrib : (y + z) * x = y * x + z * x :=
  begin
    simp [mul_distrib_left, mul_comm],
  end

  lemma mul_assoc : x * (y * z) = x * y * z :=
  begin
    induction x with x,
    {
      simp,
    },
    simp [right_distrib, *],
  end

  private def to_int : ℤ⁺ → ℤ
    | one := 1
    | (succ x) := x.to_int + 1

  instance coe_int : has_coe ℤ⁺ ℤ := ⟨to_int⟩

  @[simp] lemma coe_int_one : @coe _ ℤ _ one = 1 := rfl
  @[simp] lemma coe_int_succ : @coe _ ℤ _ x.succ = ↑x + 1 := rfl
  @[simp] lemma coe_int_one₂ : @coe ℤ⁺ ℤ _ 1 = 1 := rfl

  lemma coe_int_pos : 0 < @coe _ ℤ _ x :=
  begin
    induction x with x,
    {
      simp,
    },
    dsimp,
    apply add_pos,
    {
      apply x_ih,
    },
    {
      simp,
    },
  end

  lemma coe_int_sign : int.sign x = 1 :=
  begin
    apply (int.sign_eq_one_iff_pos _).mpr,
    apply coe_int_pos,
  end

  lemma add_respects_coe_int : @coe _ ℤ _ (x + y) = ↑x + ↑y :=
  begin
    induction x with x,
    {
      simp [int.add_comm],
    },
    simp *,
    ring,
  end

  lemma mul_respects_coe_int : @coe _ ℤ _ (x * y) = ↑x * ↑y :=
  begin
    induction x with x,
    {
      simp,
    },
    simp [add_respects_coe_int, *],
    ring,
  end

  private def to_nat : ℤ⁺ → ℕ
    | one := 1
    | (succ x) := x.to_nat.succ

  instance coe_nat : has_coe ℤ⁺ ℕ := ⟨to_nat⟩

  @[simp] lemma coe_nat_one : @coe _ ℕ _ one = 1 := rfl
  @[simp] lemma coe_nat_succ : @coe _ ℕ _ (x.succ) = (@coe _ ℕ _ x).succ := rfl

  lemma coe_nat_pos : 0 < @coe _ ℕ _ x :=
  begin
    induction x with x,
    {
      simp,
    },
    dsimp,
    apply nat.zero_lt_succ,
  end

  lemma coe_int_nat_abs : int.nat_abs x = x :=
  begin
    induction x with x,
    {
      refl,
    },
    dsimp,
    rw int.nat_abs_add_nonneg,
    {
      rw x_ih,
      refl,
    },
    {
      apply le_of_lt,
      apply coe_int_pos,
    },
    {
      simp,
    },
  end

  instance : inhabited ℤ⁺ := ⟨37⟩

  /-- Conversion from nat -/
  def of_nat_plus_one : ℕ → ℤ⁺
    | nat.zero := one
    | (nat.succ x) := succ (of_nat_plus_one x)

  @[simp] lemma of_nat_plus_one_succ (x : ℕ) : of_nat_plus_one x.succ = succ (of_nat_plus_one x) := rfl

  lemma coe_of_nat_plus_one (x : ℕ) : @coe _ ℤ _ (of_nat_plus_one x) = x + 1 :=
  begin
    induction x with x,
    {
      refl,
    },
    {
      simp *,
    },
  end

end posint

/-
I define the internal representation of rational numbers as ℤ ⨯ ℤ⁺ and an equivalence on them.
-/

/-- Internal representation of rational numbers -/
structure rat.rep : Type := mk :: (num : ℤ) (denom : ℤ⁺)

namespace rat.rep

  variables x y : rat.rep

  private def add : rat.rep := ⟨x.num * y.denom + y.num * x.denom, x.denom * y.denom⟩
  private def neg : rat.rep := ⟨-x.num, x.denom⟩
  private def mul : rat.rep := ⟨x.num * y.num, x.denom * y.denom⟩
  private def inv : rat.rep → rat.rep
    | ⟨int.of_nat nat.zero, denom⟩ := ⟨0, denom⟩
    | ⟨int.of_nat (nat.succ num), denom⟩ := ⟨denom, posint.of_nat_plus_one num⟩
    | ⟨int.neg_succ_of_nat num, denom⟩ := ⟨-denom, posint.of_nat_plus_one num⟩
  private def equiv : Prop := x.num * y.denom = y.num * x.denom

  instance : has_one rat.rep := ⟨⟨1, 1⟩⟩
  instance : has_add rat.rep := ⟨add⟩
  instance : has_neg rat.rep := ⟨neg⟩
  instance : has_mul rat.rep := ⟨mul⟩
  instance : has_inv rat.rep := ⟨inv⟩
  instance : has_equiv rat.rep := ⟨equiv⟩

  @[simp] lemma one_num : num 1 = 1 := rfl
  @[simp] lemma one_denom : denom 1 = 1 := rfl
  @[simp] lemma add_def : x + y = ⟨x.num * y.denom + y.num * x.denom, x.denom * y.denom⟩ := rfl
  @[simp] lemma mul_def : x * y = ⟨x.num * y.num, x.denom * y.denom⟩ := rfl
  @[simp] lemma neg_def : -x = ⟨-x.num, x.denom⟩ := rfl
  @[simp] lemma inv_zero (d : ℤ⁺) : (⟨0, d⟩ : rat.rep)⁻¹ = ⟨0, d⟩ := rfl
  @[simp] lemma inv_pos (n : ℕ) (d : ℤ⁺) : (⟨n + 1, d⟩ : rat.rep)⁻¹ = ⟨d, posint.of_nat_plus_one n⟩ := rfl
  @[simp] lemma inv_neg (n : ℕ) (d : ℤ⁺) : (⟨int.neg_succ_of_nat n, d⟩ : rat.rep)⁻¹ = ⟨-d, posint.of_nat_plus_one n⟩ := rfl
  @[simp] lemma equiv_def : x ≈ y = (x.num * y.denom = y.num * x.denom) := rfl

  lemma equiv_equivalence : equivalence (@has_equiv.equiv rat.rep _) :=
  begin
    split,
    {
      intros x,
      simp,
    },
    split,
    {
      intros x y x_eq_y,
      simp * at *,
    },
    {
      intros x y z x_eq_y y_eq_z,
      dsimp at *,
      have y_denom_nonzero : @coe _ ℤ _ y.denom ≠ 0 := ne_of_gt (posint.coe_int_pos _),
      rw ← @int.mul_div_cancel (x.num * _) y.denom y_denom_nonzero,
      rw ← @int.mul_div_cancel (z.num * _) y.denom y_denom_nonzero,
      apply congr_arg2 _ _ rfl,
      rw [mul_assoc x.num, int.mul_comm z.denom, ← mul_assoc, x_eq_y],
      rw [mul_assoc z.num, int.mul_comm x.denom, ← mul_assoc, ← y_eq_z],
      rw mul_right_comm,
    },
  end

  instance rat.setoid : setoid rat.rep := ⟨equiv, equiv_equivalence⟩

  instance : inhabited rat.rep := ⟨37⟩

end rat.rep

/-
I define rational numbers as a quotient type on ℤ ⨯ ℤ⁺.
-/

namespace myrat

  open rat.rep

  /-- Rational numbers -/
  def rat := quotient rat.setoid

  notation `ℚ'` := rat

  lemma add_respects : (@has_equiv.equiv rat.rep _ ⇒ (≈) ⇒ (≈)) (+) (+) :=
  begin
    intros x z x_eq_z y w y_eq_w,
    dsimp at *,
    simp only [posint.mul_respects_coe_int, right_distrib],
    rw [mul_assoc x.num, int.mul_comm y.denom, ← mul_assoc x.num, ← mul_assoc x.num, x_eq_z],
    rw [int.mul_comm z.denom, mul_assoc y.num, int.mul_comm x.denom, ← mul_assoc y.num, ← mul_assoc y.num, y_eq_w],
    ring,
  end

  lemma neg_respects : (@has_equiv.equiv rat.rep _ ⇒ (≈)) has_neg.neg has_neg.neg :=
  begin
    intros x y x_eq_y,
    dsimp at *,
    rw [← neg_mul_eq_neg_mul, ← neg_mul_eq_neg_mul, x_eq_y],
  end

  lemma mul_respects : (@has_equiv.equiv rat.rep _ ⇒ (≈) ⇒ (≈)) (*) (*) :=
  begin
    intros x z x_eq_z y w y_eq_w,
    dsimp at *,
    simp only [posint.mul_respects_coe_int],
    rw [int.mul_comm z.denom, mul_assoc x.num, ← mul_assoc y.num, y_eq_w],
    rw [mul_comm z.num, mul_assoc _ z.num, ← mul_assoc z.num, ← x_eq_z],
    ring,
  end

  lemma int.coe_plus_one_mul_eq_zero {x : ℕ} {y : ℤ} : (↑x + 1) * y = 0 → y = 0 :=
  begin
    intros h,
    have := int.eq_zero_or_eq_zero_of_mul_eq_zero h,
    cases this,
    {
      exfalso,
      revert this,
      apply ne_of_gt,
      apply int.add_pos_of_nonneg_of_pos,
      {
        apply int.coe_zero_le,
      },
      {
        apply int.one_pos,
      },
    },
    {
      apply this,
    },
  end

  lemma int.neg_plus_one_mul_eq_zero {x : ℕ} {y : ℤ} : -[1+ x] * y = 0 → y = 0 :=
  begin
    intros h,
    have := int.eq_zero_or_eq_zero_of_mul_eq_zero h,
    cases this,
    {
      contradiction,
    },
    {
      apply this,
    },
  end

  lemma inv_respects : (@has_equiv.equiv rat.rep _ ⇒ (≈)) has_inv.inv has_inv.inv :=
  begin
    intros x y x_eq_y,
    dsimp at *,
    cases x,
    cases x_num,
    cases x_num,
    all_goals
    {
      cases y,
      cases y_num,
      cases y_num,
      all_goals { dsimp at * },
    },
    {
      apply x_eq_y,
    },
    {
      rw [zero_mul, int.coe_plus_one_mul_eq_zero x_eq_y.symm] at *,
      simp,
    },
    {
      rw [zero_mul, int.neg_plus_one_mul_eq_zero x_eq_y.symm] at *,
      simp,
    },
    {
      rw [zero_mul, int.coe_plus_one_mul_eq_zero x_eq_y] at *,
      simp,
    },
    {
      rw [posint.coe_of_nat_plus_one, posint.coe_of_nat_plus_one, mul_comm, ← x_eq_y, mul_comm],
    },
    {
      rw [posint.coe_of_nat_plus_one, posint.coe_of_nat_plus_one, ← neg_mul_eq_neg_mul, mul_comm (coe y_denom), x_eq_y],
      ring,
    },
    {
      rw [zero_mul, int.neg_plus_one_mul_eq_zero x_eq_y] at *,
      simp,
    },
    {
      rw [int.neg_succ_of_nat_eq] at x_eq_y,
      rw [posint.coe_of_nat_plus_one, posint.coe_of_nat_plus_one, ← neg_mul_eq_neg_mul, mul_comm, ← x_eq_y],
      ring,
    },
    {
      rw [int.neg_succ_of_nat_eq, int.neg_succ_of_nat_eq] at x_eq_y,
      rw [posint.coe_of_nat_plus_one, posint.coe_of_nat_plus_one, neg_mul_comm, neg_mul_comm, mul_comm, ← x_eq_y, mul_comm],
    },
  end

  private def canonical_repr : ℚ' → ℤ × ℕ × ℕ :=
  begin
    intros x,
    apply quotient.lift_on x,
    swap,
    {
      clear x,
      intros x,
      let gcd := nat.gcd x.num.nat_abs x.denom,
      exact (x.num.sign, x.num.nat_abs / gcd, x.denom / gcd),
    },
    clear x,
    intros x y x_eq_y,
    apply prod.ext_iff.mpr,
    dsimp at *,
    split,
    {
      apply_fun int.sign at x_eq_y,
      rw [int.sign_mul, int.sign_mul, posint.coe_int_sign, posint.coe_int_sign, int.mul_one, int.mul_one] at x_eq_y,
      apply x_eq_y,
    },
    apply prod.ext_iff.mpr,
    apply_fun int.nat_abs at x_eq_y,
    rw [int.nat_abs_mul, posint.coe_int_nat_abs, int.nat_abs_mul, posint.coe_int_nat_abs] at x_eq_y,
    dsimp at *,
    have lowest_terms_unique : ∀ {a b c d : ℕ}, a * d = c * b → 0 < a ∨ 0 < b → 0 < c ∨ 0 < d → a / a.gcd b = c / c.gcd d :=
    begin
      intros a b c d h fst_pos snd_pos,
      apply nat.div_eq_of_eq_mul_left,
      {
        cases fst_pos,
        {
          apply nat.gcd_pos_of_pos_left,
          apply fst_pos,
        },
        {
          apply nat.gcd_pos_of_pos_right,
          apply fst_pos,
        },
      },
      rw [nat.mul_comm, ← nat.mul_div_assoc],
      swap,
      {
        apply nat.gcd_dvd_left,
      },
      symmetry,
      apply nat.div_eq_of_eq_mul_left,
      {
        cases snd_pos,
        {
          apply nat.gcd_pos_of_pos_left,
          apply snd_pos,
        },
        {
          apply nat.gcd_pos_of_pos_right,
          apply snd_pos,
        },
      },
      rw [← nat.gcd_mul_left, ← nat.gcd_mul_right],
      simp [h, nat.mul_comm],
    end,
    split,
    {
      apply lowest_terms_unique x_eq_y; right; apply posint.coe_nat_pos,
    },
    {
      rw [← nat.gcd_comm x.denom, ← nat.gcd_comm y.denom],
      symmetry' at x_eq_y,
      rw [← nat.mul_comm x.denom, ← nat.mul_comm y.denom] at x_eq_y,
      apply lowest_terms_unique x_eq_y; left; apply posint.coe_nat_pos,
    },
  end

  private def repr (x : ℚ') := let (s, n, d) := canonical_repr x in (s * n).repr ++ "/" ++ d.repr

  instance : has_repr ℚ' := ⟨repr⟩

  private def add := quotient.map₂ (+) add_respects
  private def mul := quotient.map₂ (*) mul_respects
  private def neg := quotient.map has_neg.neg neg_respects
  private def inv := quotient.map has_inv.inv inv_respects

  instance : has_zero ℚ' := ⟨⟦⟨0, 1⟩⟧⟩
  instance : has_one ℚ' := ⟨⟦1⟧⟩
  instance : has_add ℚ' := ⟨add⟩
  instance : has_mul ℚ' := ⟨mul⟩
  instance : has_neg ℚ' := ⟨neg⟩
  instance : has_inv ℚ' := ⟨inv⟩

  variables x y z : ℚ'

  lemma add_assoc : x + y + z = x + (y + z) :=
  begin
    apply quotient.induction_on₃ x y z,
    clear x y z,
    intros x y z,
    apply quotient.sound,
    dsimp,
    repeat { rw posint.mul_respects_coe_int },
    ring,
  end

  lemma zero_add : 0 + x = x :=
  begin
    apply quotient.induction_on x,
    clear x,
    intros x,
    apply quotient.sound,
    dsimp,
    rw posint.mul_respects_coe_int,
    ring,
  end

  lemma add_zero : x + 0 = x :=
  begin
    apply quotient.induction_on x,
    clear x,
    intros x,
    apply quotient.sound,
    dsimp,
    rw posint.mul_respects_coe_int,
    ring,
  end

  lemma add_left_neg : -x + x = 0 :=
  begin
    apply quotient.induction_on x,
    clear x,
    intros x,
    apply quotient.sound,
    dsimp,
    rw posint.mul_respects_coe_int,
    ring,
  end

  lemma add_comm : x + y = y + x :=
  begin
    apply quotient.induction_on₂ x y,
    clear x y,
    intros x y,
    apply quotient.sound,
    dsimp,
    repeat { rw posint.mul_respects_coe_int },
    ring,
  end

  lemma mul_assoc : x * y * z = x * (y * z) :=
  begin
    apply quotient.induction_on₃ x y z,
    clear x y z,
    intros x y z,
    apply quotient.sound,
    dsimp,
    repeat { rw posint.mul_respects_coe_int },
    ring,
  end

  lemma one_mul : 1 * x = x :=
  begin
    apply quotient.induction_on x,
    clear x,
    intros x,
    apply quotient.sound,
    dsimp,
    rw posint.mul_respects_coe_int,
    ring,
  end

  lemma mul_one : x * 1 = x :=
  begin
    apply quotient.induction_on x,
    clear x,
    intros x,
    apply quotient.sound,
    dsimp,
    rw posint.mul_respects_coe_int,
    ring,
  end

  lemma left_distrib : x * (y + z) = x * y + x * z :=
  begin
    apply quotient.induction_on₃ x y z,
    clear x y z,
    intros x y z,
    apply quotient.sound,
    dsimp,
    repeat { rw posint.mul_respects_coe_int },
    ring,
  end

  lemma right_distrib : (x + y) * z = x * z + y * z :=
  begin
    apply quotient.induction_on₃ x y z,
    clear x y z,
    intros x y z,
    apply quotient.sound,
    dsimp,
    repeat { rw posint.mul_respects_coe_int },
    ring,
  end

  lemma mul_comm : x * y = y * x :=
  begin
    apply quotient.induction_on₂ x y,
    clear x y,
    intros x y,
    apply quotient.sound,
    dsimp,
    repeat { rw posint.mul_respects_coe_int },
    ring,
  end

  lemma exists_pair_ne : ∃ x y : ℚ', x ≠ y :=
  begin
    refine ⟨0, 1, _⟩,
    refine _ ∘ quotient.exact,
    simp,
  end

  lemma mul_inv_cancel : x ≠ 0 → x * x⁻¹ = 1 :=
  begin
    apply quotient.induction_on x,
    clear x,
    intros x x_nonzero,
    apply quotient.sound,
    dsimp,
    rw posint.mul_respects_coe_int,
    cases x,
    cases x_num,
    cases x_num,
    {
      exfalso,
      apply x_nonzero,
      apply quotient.sound,
      simp,
    },
    {
      dsimp,
      rw posint.coe_of_nat_plus_one,
      ring,
    },
    {
      dsimp,
      rw [posint.coe_of_nat_plus_one, int.neg_succ_of_nat_coe'],
      ring,
    },
  end

  lemma inv_zero : 0⁻¹ = (0 : ℚ') := rfl

  instance : field ℚ' :=
  ⟨
    (+),
    add_assoc,
    0,
    zero_add,
    add_zero,
    has_neg.neg,
    add_left_neg,
    add_comm,
    (*),
    mul_assoc,
    1,
    one_mul,
    mul_one,
    left_distrib,
    right_distrib,
    mul_comm,
    has_inv.inv,
    exists_pair_ne,
    mul_inv_cancel,
    inv_zero,
  ⟩

  instance : inhabited ℚ' := ⟨37⟩

end myrat

#eval ((99/70)^2 /2 : ℚ')

#eval (1/2 + 1/3 + 1/4 + 1/5 + 1/6 : ℚ')

#lint-