Zulip Chat Archive

Stream: maths

Topic: int is a ring


view this post on Zulip 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
  -- unfold it in your head
  change first a + second a = second a + first a,
  -- if you delete the line above, the line below still works
  apply add_comm,
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

instance : has_add 3 := add

@[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

instance : add_comm_group 3 :=
{ add := (+),
  add_assoc :=
  begin
    intros a b c,
    apply quotient.induction_on₃ a b c,
    intros,
    simp * at *,
    omega,
  end,
  zero := 0,
  zero_add :=
  begin
    intro a,
    apply quotient.induction_on a,
    intros,
    simp * at *,
    omega
  end,
  add_zero :=
  begin
    intro a,
    apply quotient.induction_on a,
    intros,
    simp * at *,
    omega
  end,
  neg := has_neg.neg,
  add_left_neg :=
  begin
    intro a,
    apply quotient.induction_on a,
    intros,
    simp * at *,
    omega
  end,
  add_comm :=
  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 [add_mul, add_mul] at h3,
  apply @nat.add_left_cancel (u * r),
  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 [h2, mul_add, mul_add],
  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,
  ..int3.add_comm_group
}

end int3

view this post on Zulip 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)⟧

view this post on Zulip 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,

view this post on Zulip Bhavik Mehta (Jun 28 2020 at 15:48):

This works

view this post on Zulip 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