Proof that Z-set and additive merge form an abelian group

zset_abelian.lean

variable {α : Type} [DecidableEq α]

-- Define our own minimal abelian group structure (no mathlib)
structure AbelianGroup (G : Type) where
  add : G → G → G
  zero : G
  neg : G → G
  add_assoc : ∀ a b c : G, add (add a b) c = add a (add b c)
  add_zero : ∀ a : G, add a zero = a
  zero_add : ∀ a : G, add zero a = a
  add_inv : ∀ a : G, add a (neg a) = zero
  add_comm : ∀ a b : G, add a b = add b a

-- Example that integers form our minimal abelian group:
example : AbelianGroup Int := {
  add := fun a b => a + b,
  zero := 0,
  neg := fun a => -a,
  add_assoc := Int.add_assoc,
  add_comm := Int.add_comm
  add_zero := Int.add_zero,
  zero_add := Int.zero_add,
  add_inv := Int.add_right_neg,
}


-- ZSet is a function from elements to integers (coefficients)
def ZSet (α : Type) : Type :=
  α → Int

-- Register extensionaltiy theorem for ZSet
-- This tells Lean: "To prove two ZSets are equal, show they're equal pointwise"
@[ext]
theorem ZSet.ext {α : Type} (f g : ZSet α) : (∀ x, f x  = g x) -> f = g :=
  funext

-- empty ZSet (all coefs are 0)
def ZSet.empty {α : Type} : ZSet α :=
  fun _ => 0

-- Add an element with coefficient
def ZSet.single (a : α) (n : Int) : ZSet α :=
  fun x => if x = a then n else 0

-- Additive merge: add coefficients pointwise
def ZSet.add {α : Type} (zs1 zs2 : ZSet α) : ZSet α :=
  fun x => zs1 x + zs2 x
-- Enable `+` notation for ZSets
instance {α : Type} : Add (ZSet α) where
  add := ZSet.add

-- Additive inverse: negate all coefficients
def ZSet.neg {α : Type} (zs : ZSet α) : ZSet α :=
  fun x => -(zs x)
-- Enable `-` unary operator for ZSets
instance {α : Type} : Neg (ZSet α) where
  neg := ZSet.neg

-- Proof that ZSet under additive merge form an abelian group
instance : AbelianGroup (ZSet α)
where
  add := ZSet.add
  zero := ZSet.empty
  neg := ZSet.neg

  -- (a + b) + c = a + (b + c)
  add_assoc := by
    intro a b c
    ext x
    simp [ZSet.add, Int.add_assoc]

  -- a + b = b + a
  add_comm := by
    intro a b
    ext x
    simp [ZSet.add, Int.add_comm]

  -- a + 0 = a
  add_zero := by
    intro a
    ext x
    simp [ZSet.add, ZSet.empty]

  -- 0 + a = a
  zero_add := by
    intro a
    ext x
    simp [ZSet.add, ZSet.empty]

  -- a + (-a) = 0
  add_inv := by
    intro a
    ext x
    simp [ZSet.add, ZSet.neg, ZSet.empty]
    rw [Int.add_right_neg]

example : (ZSet.single "a" 3 + ZSet.single "b" 2) "a" = 3 := by rfl

example : (ZSet.single "a" 3 + ZSet.single "a" 2) "a" = 5 := by rfl

example : (ZSet.single "a" (-3) + ZSet.single "a" 2) "a" = -1 := by rfl

example : ZSet.neg (ZSet.single "a" 3) "a" = (-3) := by rfl