Skip to content

Instantly share code, notes, and snippets.

@kbuzzard

kbuzzard/myint.lean

Created Jan 6, 2020
Embed
What would you like to do?
integers the maths way
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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment