integers the maths way

myint.lean

import tactic

-- need to teach pairs

-- (3, 6) : ℕ × ℕ
-- x.1 is first element of x, x.2 is second

/-- The equivalence relation on ℕ² such that equivalence classes are ℤ -/
def nat2.R (a b : ℕ × ℕ) : Prop :=
a.1 + b.2 = b.1 + a.2

instance : has_equiv (ℕ × ℕ) := ⟨nat2.R⟩

lemma equiv_def {i j k l : ℕ} : (i, j) ≈ (k, l) ↔ i + l = k + j := iff.rfl

-- BUG:
-- #print notation  ≈ -- Type ≈ using ~~ or \approx or \thickapprox
-- this should say \~~

namespace nat2.R

-- teach change, or modded equiv?
lemma practice : (3, 5) ≈ (4, 6) :=
begin
  rw equiv_def, -- need modded equiv
  -- refl

  -- or

--  change 3 + 6 = 4 + 5,
--  change 9 = 9,
--  refl,
end

-- teach rintro
lemma reflexive : ∀ x : ℕ × ℕ, x ≈ x :=
begin
  rintro ⟨i, j⟩,
  rw equiv_def,
  -- refl

  -- or

  -- change i + j = i + j,
  -- refl,
end

lemma symmetric : ∀ x y : ℕ × ℕ, (x ≈ y) → (y ≈ x) :=
begin
  rintro ⟨i, j⟩ ⟨k, l⟩ h,
  rw equiv_def at h ⊢,
  symmetry,
  assumption,
end

-- teach calc; teach P → Q → R
lemma transitive : ∀ x y z : ℕ × ℕ, (x ≈ y) → (y ≈ z) → (x ≈ z) :=
begin
  rintro ⟨i, j⟩ ⟨k, l⟩ ⟨m, n⟩,
  intros h1 h2,
  rw equiv_def at h1 h2 ⊢,
  suffices : (i + n) + (l + k) = (m + j) + (l + k),
    exact add_right_cancel this,
  exact calc i + n + (l + k) = (i + l) + (k + n) : by ring
  ...                        = (k + j) + (m + l) : by rw [h1, h2]
  ...                        = (m + j) + (l + k) : by ring
end

instance setoid : setoid (ℕ × ℕ) :=
{ r := nat2.R,
  iseqv := ⟨reflexive, symmetric, transitive⟩ }

end nat2.R

def myint := quotient nat2.R.setoid

namespace myint 

-- def mk : ℕ × ℕ → myint := quotient.mk -- never used

def add_aux (x y : ℕ × ℕ) : myint := ⟦(x.1 + y.1, x.2 + y.2)⟧

lemma add_aux_def (i j k l : ℕ) : add_aux (i, j) (k, l) = ⟦(i + k, j + l)⟧ :=
begin
  refl
end

lemma add_aux_lemma : ∀ x₁ x₂ y₁ y₂ : ℕ × ℕ,
(x₁ ≈ y₁) → (x₂ ≈ y₂) → add_aux x₁ x₂ = add_aux y₁ y₂ :=
begin
  rintro ⟨i, j⟩ ⟨k, l⟩ ⟨m, n⟩ ⟨p, q⟩ h1 h2,
  rw add_aux_def,
  rw add_aux_def,
  apply quotient.sound,
  rw equiv_def at h1 h2 ⊢,
  exact calc i + k + (n + q) = (i + n) + (k + q) : by simp
  ...                        = (m + j) + (p + l) : by rw [h1, h2]
  ...                        = m + p + (j + l) : by simp
end

def add : myint → myint → myint :=
quotient.lift₂ add_aux add_aux_lemma

instance : has_add myint := ⟨add⟩

lemma add_def (i j k l : ℕ) : (⟦(i, j)⟧ + ⟦(k, l)⟧ : myint) = ⟦(i + k, j + l)⟧ := rfl

lemma add_assoc (x y z : myint) : (x + y) + z = x + (y + z) :=
begin
  apply quotient.induction_on₃ x y z,
  rintro ⟨i, j⟩ ⟨k, l⟩ ⟨m, n⟩,
  rw add_def,
  rw add_def,
  rw add_def,
  rw add_def,
  apply quotient.sound,
  rw equiv_def,
  simp,
end

instance : add_semigroup myint :=
{ add := add,
  add_assoc := add_assoc }

def zero := ⟦(⟨0, 0⟩ : ℕ × ℕ)⟧

instance : has_zero myint := ⟨myint.zero⟩

lemma zero_def : (0 : myint) = ⟦(0, 0)⟧ := rfl

lemma zero_add (x : myint) : 0 + x = x :=
begin
  apply quotient.induction_on x,
  rintro ⟨i, j⟩,
  rw zero_def,
  rw add_def,
  apply quotient.sound,
  rw equiv_def,
  simp,  
end

lemma add_zero (x : myint) : x + 0 = x :=
begin
  apply quotient.induction_on x,
  rintro ⟨i, j⟩,
  rw zero_def,
  rw add_def,
  apply quotient.sound,
  rw equiv_def,
  simp,  
end

instance : add_monoid myint :=
by refine_struct { add_zero := add_zero, zero_add := zero_add, ..myint.add_semigroup, ..myint.has_zero}

lemma add_comm (x y : myint) : x + y = y + x :=
begin
  apply quotient.induction_on₂ x y,
  rintro ⟨i, j⟩ ⟨k, l⟩,
  rw add_def,
  rw add_def,
  apply quotient.sound,
  rw equiv_def,
  simp,
end

instance : add_comm_monoid myint :=
by refine_struct {add_comm := add_comm, ..myint.add_monoid}

def neg_aux (x : ℕ × ℕ) : myint := ⟦(x.2, x.1)⟧

lemma neg_aux_def (i j : ℕ) : neg_aux (i, j) = ⟦(j, i)⟧ := rfl

lemma neg_aux_lemma : ∀ x y : ℕ × ℕ, x ≈ y → neg_aux x = neg_aux y :=
begin
  rintro ⟨i, j⟩ ⟨k, l⟩,
  intro h,
  rw neg_aux_def,
  rw neg_aux_def,
  apply quotient.sound,
  rw equiv_def at h ⊢,
  rw nat.add_comm,
  rw ←h,
  apply nat.add_comm,
end

def neg : myint → myint :=
quotient.lift neg_aux neg_aux_lemma

instance : has_neg myint := ⟨neg⟩

lemma neg_def (i j : ℕ) : (-⟦(i, j)⟧ : myint) = ⟦(j, i)⟧ := rfl

lemma add_left_neg (x : myint) : -x + x = 0 :=
begin
  apply quotient.induction_on x,
  rintro ⟨i, j⟩,
  rw neg_def,
  rw add_def,
  apply quotient.sound,
  rw equiv_def,
  simp,
end

instance : add_group myint :=
by refine_struct {add_left_neg := add_left_neg, ..myint.add_monoid, ..myint.has_neg}; begin end

instance : add_comm_group myint :=
by refine_struct {..myint.add_comm_monoid, ..myint.add_group}

-- woohoo!

def mul_aux (x y : ℕ × ℕ) : myint := ⟦(x.1 * y.1 + x.2 * y.2, x.1 * y.2 + y.1 * x.2)⟧ -- 

lemma mul_aux_def (i j k l : ℕ) : mul_aux (i, j) (k, l) = ⟦(i * k + j * l, i * l + k * j)⟧ := rfl

-- proving multiplication is well-defined on int := ℕ^2/~

/-
1 goal
i j k l m n p q : ℕ,
h2 : k + q = p + l,
h1 : i + n = m + j
⊢ i * k + j * l + (m * q + p * n) = m * p + n * q + (i * l + k * j)
-/

lemma mul_aux_lemma : ∀ x₁ x₂ y₁ y₂ : ℕ × ℕ,
(x₁ ≈ y₁) → (x₂ ≈ y₂) → mul_aux x₁ x₂ = mul_aux y₁ y₂ :=
begin
  rintro ⟨i, j⟩ ⟨k, l⟩ ⟨m, n⟩ ⟨p, q⟩ h1 h2,
  rw mul_aux_def,
  rw mul_aux_def,
  apply quotient.sound,
  rw equiv_def at h1 h2 ⊢,
  rw ←add_left_inj (n * k + i * p + m * l),
  exact calc (n * k + i * p + m * l) + (i * k + j * l + (m * q + p * n))
        = (i + n) * (p + k) + j * l + m * q + m * l : by ring
  ...   = (m + j) * (p + k) + j * l + m * q + m * l : by rw h1
  ...   = (m + j) * (p + l) + j * k + m * (k + q) : by ring
  ...   = (i + n) * (p + l) + j * k + m * (p + l) : by rw [←h1, h2]
  ...   = (i + n) * (p + l) + m * p + k * j + m * l : by ring
  ...   = (i + n) * (k + q) + m * p + k * j + m * l : by rw ←h2
  ...   = i * (k + q) + n * k + m * p + n * q + k * j + m * l : by ring
  ...   = i * (p + l) + n * k + m * p + n * q + k * j + m * l : by rw h2
  ...   = (n * k + i * p + m * l) + (m * p + n * q + (i * l + k * j)) : by ring
end

-- !!

def mul : myint → myint → myint :=
quotient.lift₂ mul_aux mul_aux_lemma

instance : has_mul myint := ⟨mul⟩ 

lemma mul_def (i j k l : ℕ) : (⟦(i, j)⟧ * ⟦(k, l)⟧ : myint) = ⟦(i * k + j * l, i * l + k * j)⟧ := rfl

lemma mul_assoc (x y z : myint) : (x * y) * z = x * (y * z) :=
begin
  apply quotient.induction_on₃ x y z,
  rintro ⟨i, j⟩ ⟨k, l⟩ ⟨m, n⟩,
  repeat {rw mul_def},
  apply quotient.sound,
  rw equiv_def,
  ring
end

instance : semigroup myint := by refine_struct {mul := mul, mul_assoc := mul_assoc}

def one := ⟦(1, 0)⟧

instance : has_one myint := ⟨myint.one⟩

lemma one_def : (1 : myint) = ⟦(1, 0)⟧ := rfl

lemma one_mul (x : myint) : 1 * x = x :=
begin
  apply quotient.induction_on x,
  rintro ⟨i, j⟩,
  rw one_def,
  rw mul_def,
  apply quotient.sound,
  rw equiv_def,
  ring
end

lemma mul_one (x : myint) : x * 1 = x :=
begin
  apply quotient.induction_on x,
  rintro ⟨i, j⟩,
  rw one_def,
  rw mul_def,
  apply quotient.sound,
  rw equiv_def,
  ring
end

instance : monoid myint :=
by refine_struct { mul_one := mul_one, one_mul := one_mul, ..myint.semigroup, ..myint.has_one}

lemma mul_comm (x y : myint) : x * y = y * x :=
begin
  apply quotient.induction_on₂ x y,
  rintro ⟨i, j⟩ ⟨k, l⟩,
  repeat {rw mul_def},
  apply quotient.sound,
  rw equiv_def,
  ring,
end

instance : comm_monoid myint :=
by refine_struct {mul_comm := mul_comm, ..myint.monoid}

instance : comm_semigroup myint := by apply_instance

lemma mul_add (x y z : myint) : x * (y + z) = x * y + x * z :=
begin
  apply quotient.induction_on₃ x y z,
  rintro ⟨i, j⟩ ⟨k, l⟩ ⟨m, n⟩,
  repeat {rw mul_def},
  repeat {rw add_def},
  repeat {rw mul_def},
  apply quotient.sound,
  rw equiv_def,
  ring
end

lemma add_mul (x y z : myint) : (x + y) * z = x * z + y * z :=
begin
  apply quotient.induction_on₃ x y z,
  rintro ⟨i, j⟩ ⟨k, l⟩ ⟨m, n⟩,
  repeat {rw mul_def},
  repeat {rw add_def},
  repeat {rw mul_def},
  apply quotient.sound,
  rw equiv_def,
  ring
end

instance : distrib myint := by refine_struct {left_distrib := mul_add, right_distrib := add_mul, ..myint.has_add, ..myint.has_mul}
instance : ring myint := by refine_struct {..myint.add_comm_group, ..myint.monoid, ..myint.distrib}
instance : comm_ring myint := by refine_struct {..myint.ring, ..myint.comm_semigroup}

#eval (6 : myint) + 8 -- (#0 #14 #0)

end myint