a proof of finitely suppported zset is an abelian group

finite_support_zset_abelian.lean

-- Lean v4.23.0-rc2

import Std

open Std

variable {α : Type} [DecidableEq α]

/- ------------------------------------------------------------
   0) Your minimal abelian group structure (unchanged)
------------------------------------------------------------ -/

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 : 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,
}

/- ------------------------------------------------------------
   1) Finite support, but using List

   FiniteSupport f := ∃ s : List α, outside s, f is 0.

   This is the only place we encode “finite-ness”.
------------------------------------------------------------ -/

def FiniteSupport {α : Type} (f : α → Int) : Prop :=
  ∃ s : List α, ∀ x : α, x ∉ s → f x = 0

/-- Finitely-supported Z-set = function + proof it has finite support. -/
def FZSet (α : Type) : Type :=
  { f : α → Int // FiniteSupport f }

/- Extensionality for FZSet: equality is pointwise equality of the function. -/
@[ext]
theorem FZSet.ext {α : Type} (f g : FZSet α) : (∀ x, f.1 x = g.1 x) → f = g := by
  intro h
  apply Subtype.ext
  funext x
  exact h x

/- ------------------------------------------------------------
   2) Constructors: empty and single (now with List witnesses)
------------------------------------------------------------ -/

def FZSet.empty {α : Type} : FZSet α :=
  ⟨(fun _ => 0), by
    refine ⟨([] : List α), ?_⟩
    intro x hx
    rfl⟩

def FZSet.single (a : α) (n : Int) : FZSet α :=
  ⟨(fun x => if x = a then n else 0), by
    refine ⟨([a] : List α), ?_⟩
    intro x hx
    -- From x ∉ [a], we get x ≠ a
    have hne : x ≠ a := by
      intro hxa
      -- If x = a then x ∈ [a], contradiction
      have : x ∈ ([a] : List α) := by
        -- [a] is a :: [], so membership is by head equality
        simp [List.mem_cons, hxa]
      exact hx this
    -- So the if-expression takes the "else" branch
    simp [hne]⟩

/- ------------------------------------------------------------
   3) Operations: add and neg, with closure proofs via List witnesses
------------------------------------------------------------ -/

def FZSet.add {α : Type} (zs1 zs2 : FZSet α) : FZSet α :=
  ⟨(fun x => zs1.1 x + zs2.1 x), by
    rcases zs1.2 with ⟨s1, hs1⟩
    rcases zs2.2 with ⟨s2, hs2⟩
    -- Witness for sum support is s1 ++ s2
    refine ⟨s1 ++ s2, ?_⟩
    intro x hx

    -- If x ∉ s1 ++ s2 then x ∉ s1 and x ∉ s2
    have hx1 : x ∉ s1 := by
      intro hx1'
      have : x ∈ s1 ++ s2 := by
        exact List.mem_append.mpr (Or.inl hx1')
      exact hx this

    have hx2 : x ∉ s2 := by
      intro hx2'
      have : x ∈ s1 ++ s2 := by
        exact List.mem_append.mpr (Or.inr hx2')
      exact hx this

    -- Outside both supports, both are zero
    simp [hs1 x hx1, hs2 x hx2]⟩

instance {α : Type} : Add (FZSet α) where
  add := FZSet.add

def FZSet.neg {α : Type} (zs : FZSet α) : FZSet α :=
  ⟨(fun x => -(zs.1 x)), by
    rcases zs.2 with ⟨s, hs⟩
    refine ⟨s, ?_⟩
    intro x hx
    simp [hs x hx]⟩

instance {α : Type} : Neg (FZSet α) where
  neg := FZSet.neg

/- ------------------------------------------------------------
   4) Abelian group instance

   Exactly the same ext+simp shape as your original proof,
   because the algebraic laws are still pointwise Int laws.
------------------------------------------------------------ -/

instance : AbelianGroup (FZSet α)
where
  add := FZSet.add
  zero := FZSet.empty
  neg := FZSet.neg

  add_assoc := by
    intro a b c
    ext x
    simp [FZSet.add, Int.add_assoc]

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

  add_zero := by
    intro a
    ext x
    simp [FZSet.add, FZSet.empty]

  zero_add := by
    intro a
    ext x
    simp [FZSet.add, FZSet.empty]

  add_inv := by
    intro a
    ext x
    simp [FZSet.add, FZSet.neg, FZSet.empty, Int.add_right_neg]

/- ------------------------------------------------------------
   5) Examples (note: underlying function is `.1`)
------------------------------------------------------------ -/

example : (FZSet.single "a" 3 + FZSet.single "b" 2).1 "a" = 3 := by rfl
example : (FZSet.single "a" 3 + FZSet.single "a" 2).1 "a" = 5 := by rfl
example : (FZSet.single "a" (-3) + FZSet.single "a" 2).1 "a" = -1 := by rfl
example : (FZSet.neg (FZSet.single "a" 3)).1 "a" = (-3) := by rfl