## Stream: maths

### Topic: int is a ring

#### Kevin Buzzard (Jun 28 2020 at 15:45):

I'm so nearly there. Those sorries should be done by automation. Kenny told me an earlier simp fix which made simp not get stuck in a hole in the proof of add_assoc, but it's stuck in another one with the distrib lemmas.

import tactic

-- Kenny tells me there's a missing simp lemma. Without this I get an
-- error on line 132; omega can't do add_assoc
@[simp] theorem quotient.lift_on_beta₂ {α : Type} {β : Type} [setoid α] (f : α → α → β) (h)
(x y : α) : ⟦x⟧.lift_on₂ ⟦y⟧ f h = f x y := rfl

namespace int3

notation ℕ² := ℕ × ℕ

namespace natsquared

notation first := prod.fst

notation second := prod.snd

@[ext] lemma ext {a b : ℕ²} : first a = first b → second a = second b → a = b :=
by tidy

lemma ext_iff (a b : ℕ²) : a = b ↔ first a = first b ∧ second a = second b :=
⟨λ h, by cases h; simp, λ ⟨p, q⟩, ext p q⟩

instance : has_zero ℕ² := ⟨(0, 0)⟩
@[simp] lemma first_zero : first (0 : ℕ²) = 0 := by refl
@[simp] lemma second_zero : second (0 : ℕ²) = 0 := by refl

def has_one : has_one ℕ² := ⟨(1, 0)⟩
local attribute [instance] has_one

@[simp] lemma first_one : first (1 : ℕ²) = 1 := by refl
@[simp] lemma second_one : second (1 : ℕ²) = 0 := by refl

def r (a b : ℕ²) := first a + second b = second a + first b

instance : has_equiv ℕ² := ⟨r⟩

namespace r
theorem refl (a : ℕ²) : a ≈ a :=
begin
change first a + second a = second a + first a,
-- if you delete the line above, the line below still works
end

theorem symm (a b : ℕ²) : a ≈ b → b ≈ a :=
begin
intro hab,
unfold has_equiv.equiv at *,
rw [r] at *,
omega,
end

theorem trans (a b c : ℕ²) : a ≈ b → b ≈ c → a ≈ c :=
begin
intro hab,
intro hbc,
unfold has_equiv.equiv at *,
rw [r] at *,
omega,
end

theorem equiv : equivalence r :=
⟨refl, symm, trans⟩

end r

instance : setoid ℕ² :=
{ r := r,
iseqv := r.equiv }

end natsquared

local attribute [instance] natsquared.has_one -- the canonical 1 is another one!

-- definition of int as quotient type
notation ℤ3 := quotient natsquared.setoid

-- theorem! It's a ring!

def zero : ℤ3 := ⟦0⟧
instance : has_zero ℤ3 := ⟨zero⟩
@[simp] lemma zero.thing0 : (0 : ℤ3) = ⟦0⟧ := rfl

def one : ℤ3 := ⟦1⟧
instance : has_one ℤ3 := ⟨one⟩
@[simp] lemma one.thing0 : (1 : ℤ3) = ⟦1⟧ := rfl

@[simp] lemma one.first : first (1 : ℕ²) = 1 := by refl
@[simp] lemma one.second : second (1 : ℕ²) = 0 := by refl

open natsquared

@[simp] lemma thing (a b : ℕ²) : a ≈ b ↔ first a + second b = second a + first b := iff.rfl

@[simp] def add (a b : ℤ3) : ℤ3 := quotient.lift_on₂ a b (λ z w,
⟦(first z + first w, second z + second w)⟧) begin
intros,
simp at *,
omega,
end

@[simp] lemma thing2 (a b : ℤ3) : a + b = add a b := rfl

@[simp] def neg (a : ℤ3) : ℤ3 := quotient.lift_on a (λ b, ⟦(second b, first b)⟧)
begin
intros,
simp at *,
omega
end

instance : has_neg ℤ3 := ⟨neg⟩

@[simp] lemma neg.thing0 (a : ℤ3) : -a = neg a := rfl

begin
intros a b c,
apply quotient.induction_on₃ a b c,
intros,
simp * at *,
omega,
end,
zero := 0,
begin
intro a,
apply quotient.induction_on a,
intros,
simp * at *,
omega
end,
begin
intro a,
apply quotient.induction_on a,
intros,
simp * at *,
omega
end,
neg := has_neg.neg,
begin
intro a,
apply quotient.induction_on a,
intros,
simp * at *,
omega
end,
begin
intros a b,
apply quotient.induction_on₂ a b,
intros,
simp * at *,
omega
end
}

theorem useful (p q r s t u v w : ℕ) (h1 : p + u = q + t) (h2 : r + w = s + v) :
p * r + q * s + (t * w + u * v) = p * s + q * r + (t * v + u * w) :=
begin
have h3 : (p + u) * r = (q + t) * r,
rw h1,
rw [show u * r + (p * r + q * s + (t * w + u * v)) = p * r + u * r + q * s + t * w + u * v, by ring],
rw h3,
rw [show q * r + t * r + q * s + t * w + u * v = t * (r + w) + q * s + u * v + q * r, by ring],
rw [show u * r + (p * s + q * r + (t * v + u * w)) = u * (r + w) + p * s + t * v + q * r, by ring],
rw [show t * s + t * v + q * s + u * v + q * r = t * s + q * s + t * v + u * v + q * r, by ring],
--uv cancels tv cancels qr cancels
suffices : t * s + q * s = (p + u) * s,
rw this, ring,
rw h1,
ring,
end

@[simp] def mul (a b : ℤ3) : ℤ3 := quotient.lift_on₂ a b (λ z w,
⟦(first z * first w + second z * second w, first z * second w + second z * first w)⟧)
-- why is this well-defined?
begin
intros,
simp at *,
apply useful _ _ _ _ _ _ _ _ a_1 a_2,
end

instance : has_mul ℤ3 := ⟨mul⟩

@[simp] lemma thing3 (a b : ℤ3) : a * b = mul a b := rfl

instance : comm_ring ℤ3 :=
{ mul := (*),
one := 1,
mul_assoc := begin
intros a b c,
apply quotient.induction_on₃ a b c,
intros,
simp,
ring
end,
one_mul := begin
intro a,
apply quotient.induction_on a,
intros,
simp,
ring,
end,
mul_one := begin
intro a,
apply quotient.induction_on a,
intros,
simp,
ring,
end,
left_distrib := begin
intros a b c,
apply quotient.induction_on₃ a b c,
intros,
simp,
ring,
sorry
end,
right_distrib := begin
intros a b c,
apply quotient.induction_on₃ a b c,
intros,
simp,
ring,
sorry
end,
mul_comm := begin
intros a b,
apply quotient.induction_on₂ a b,
intros,
simp,
ring,
end,
}

end int3


#### Kevin Buzzard (Jun 28 2020 at 15:47):

State after simp (when I want omega or ring to kick in) in left_distrib and right_distrib is

abc : ℤ3
a_1b_1c_1 : ℕ²
⊢ ⟦a_1⟧.lift_on₂ (add_comm_group.add ⟦b_1⟧ ⟦c_1⟧) (λ (z w : ℕ²), ⟦(z.fst * w.fst + z.snd * w.snd, z.fst * w.snd + z.snd * w.fst)⟧) mul._proof_1 = add_comm_group.add ⟦(a_1.fst * b_1.fst + a_1.snd * b_1.snd, a_1.fst * b_1.snd + a_1.snd * b_1.fst)⟧ ⟦(a_1.fst * c_1.fst + a_1.snd * c_1.snd, a_1.fst * c_1.snd + a_1.snd * c_1.fst)⟧


#### Bhavik Mehta (Jun 28 2020 at 15:48):

  left_distrib := begin
intros a b c,
apply quotient.induction_on₃ a b c,
intros,
apply quotient.sound,
simp,
ring,
end,


This works

#### Bhavik Mehta (Jun 28 2020 at 15:48):

I've found the trick for any of these is to use quotient.sound after the induction step

Last updated: May 09 2021 at 09:11 UTC