typeclass_example.lean

import tactic

class has_oplus (α : Type*) := (oplus : α → α → α)
class has_otimes (α : Type*) := (otimes : α → α → α)

instance : has_oplus ℤ := { oplus := int.add }
instance : has_otimes ℤ := { otimes := int.mul }

infixl ` ⊕ `:65  := has_oplus.oplus
infixl ` ⊗ `:70  := has_otimes.otimes

class oring (α : Type*) extends has_oplus α, has_otimes α :=
(o0 : α)
(o1 : α)
(oplus_assoc : ∀ (x y z : α), (x ⊕ y) ⊕ z = x ⊕ (y ⊕ z))
(oplus_zero : ∀ (x : α), x ⊕ o0 = x)
(zero_oplus : ∀ (x : α), o0 ⊕ x = x)
(has_neg : ∀ (x : α), ∃ (y : α), x ⊕ y = o0)
(otimes_assoc : ∀ (x y z : α), (x ⊗ y) ⊗ z = x ⊗ (y ⊗ z))
(otimes_one : ∀ (x : α), x ⊗ o1 = x)
(one_otimes : ∀ (x : α), o1 ⊗ x = x)
(left_distrib : ∀ (x y z : α), x ⊗ (y ⊕ z) = x ⊗ y ⊕ x ⊗ z)
(distrib_right : ∀ (x y z : α), (x ⊕ y) ⊗ z = x ⊗ z ⊕ y ⊗ z)
(zero_otimes : ∀ x : α, o0 ⊗ x = o0)
(otimes_zero : ∀ x : α, x ⊗ o0 = o0)

instance : oring ℤ := {
  o0 := int.zero,
  o1 := int.one,
  oplus_assoc := int.add_assoc,
  oplus_zero := int.add_zero,
  zero_oplus := int.zero_add,
  has_neg := by { intro x, existsi (- x), exact int.add_right_neg x },
  otimes_assoc := int.mul_assoc,
  otimes_one := int.mul_one,
  one_otimes := int.one_mul,
  left_distrib := int.distrib_left,
  distrib_right := int.distrib_right,
  zero_otimes := int.zero_mul,
  otimes_zero := int.mul_zero
}

def oring.neg_is_right_neg {R : Type*} [oring R]
  : ∀ (x y : R), x ⊕ y = oring.o0 → y ⊕ x = oring.o0 :=
begin
  intros x y h,
  obtain ⟨z, h'⟩ := oring.has_neg y,
  rw ← h',
  congr,
  transitivity x ⊕ oring.o0,
  { symmetry, apply oring.oplus_zero },
  { rw ← h',
    rw ← oring.oplus_assoc,
    rw h,
    apply oring.zero_oplus }
end

example : ∀ (x y : ℤ), x ⊕ y = oring.o0 → y ⊕ x = oring.o0
  := oring.neg_is_right_neg

-- Could do
def oring.hom {R S : Type*} [oring R] [oring S] (f : R → S) : Prop :=
  f oring.o1 = oring.o1
  ∧ ((∀ (x y : R), f (x ⊕ y) = f x ⊕ f y)
     ∧ (∀ (x y : R), f (x ⊗ y) = f x ⊗ f y))

lemma oring.hom_preserves_zero {R S : Type*} [oring R] [oring S] (f : R → S) (h : oring.hom f)
  : f oring.o0 = oring.o0 :=
begin
  rcases h with ⟨h1, h_add, h_mul⟩,
  have h1 : f oring.o0 ⊕ f oring.o0 = f oring.o0,
  { rw ← h_add,
    rw oring.zero_oplus }, 
  rcases oring.has_neg (f oring.o0),
  have h2 : (f oring.o0 ⊕ f oring.o0) ⊕ w = f oring.o0 ⊕ w,
  { congr, exact h1 },
  rw oring.oplus_assoc at h2,
  rw h at h2,
  rw oring.oplus_zero at h2,
  exact h2
end

-- Or
class oring.hom' {R S : Type*} [oring R] [oring S] (f : R → S) :=
(hom_one : f oring.o1 = oring.o1)
(hom_oplus : ∀ (x y : R), f (x ⊕ y) = f x ⊕ f y)
(hom_otimes : ∀ (x y : R), f (x ⊗ y) = f x ⊗ f y)

lemma oring.hom'_preserves_zero {R S : Type*} [oring R] [oring S] (f : R → S) [oring.hom' f]
  : f oring.o0 = oring.o0 :=
begin
  have h1 : f oring.o0 ⊕ f oring.o0 = f oring.o0,
  { rw ← oring.hom'.hom_oplus,
    rw oring.zero_oplus }, 
  rcases oring.has_neg (f oring.o0),
  have h2 : (f oring.o0 ⊕ f oring.o0) ⊕ w = f oring.o0 ⊕ w,
  { congr, exact h1 },
  rw oring.oplus_assoc at h2,
  rw h at h2,
  rw oring.oplus_zero at h2,
  exact h2
end