-- Core group theory
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Cumulus.Algebra.Group.Core
import Defs
import Set.Function

theorem IsMagma.closed (A op x y : Set)
  requires magma : IsMagma(A, op)
  requires xInA : x ∈ A
  requires yInA : y ∈ A
  shows op(x, y) ∈ A
proof
  unfold IsMagma at magma
  unfold call2
  apply FunctionBetween.apply_closed with magma
  exact product.pair with xInA, yInA

theorem IsSemigroup.magma (A op : Set)
  requires h : IsSemigroup(A, op)
  shows IsMagma(A, op)
proof
  simp [IsSemigroup]

theorem IsSemigroup.associative (A op : Set)
  requires h : IsSemigroup(A, op)
  shows Associative(A, op)
proof
  simp [IsSemigroup]

theorem IsSemigroup.closed (A op x y : Set)
  requires semigroup : IsSemigroup(A, op)
  requires xInA : x ∈ A
  requires yInA : y ∈ A
  shows op(x, y) ∈ A
proof
  have magma := IsSemigroup.magma with semigroup
  exact IsMagma.closed with magma, xInA, yInA

theorem Associative.law (A op x y z : Set)
  requires associative : Associative(A, op)
  requires xInA : x ∈ A
  requires yInA : y ∈ A
  requires zInA : z ∈ A
  shows op(op(x, y), z) =
    op(x, op(y, z))
proof
  exact associative with x, xInA, y, yInA, z, zInA

theorem Commutative.law (A op x y : Set)
  requires commutative : Commutative(A, op)
  requires xInA : x ∈ A
  requires yInA : y ∈ A
  shows op(x, y) = op(y, x)
proof
  exact commutative with x, xInA, y, yInA

theorem IsMonoid.identity (A op unit : Set)
  requires h : IsMonoid(A, op, unit)
  shows Identity(A, op, unit)
proof
  simp [IsMonoid]

theorem IsMonoid.closed (A op unit x y : Set)
  requires monoid : IsMonoid(A, op, unit)
  requires xInA : x ∈ A
  requires yInA : y ∈ A
  shows op(x, y) ∈ A
proof
  have semigroup := IsMonoid.semigroup with monoid
  exact IsSemigroup.closed with semigroup, xInA, yInA

theorem IsMonoid.associative (A op unit : Set)
  requires monoid : IsMonoid(A, op, unit)
  shows Associative(A, op)
proof
  have semigroup := IsMonoid.semigroup with monoid
  exact IsSemigroup.associative with semigroup

theorem IsMonoid.unit_in_carrier (A op unit : Set)
  requires monoid : IsMonoid(A, op, unit)
  shows unit ∈ A
proof
  obtain ⟨unitInA, laws⟩ := IsMonoid.identity with monoid
  exact unitInA

theorem IsMonoid.left_identity (A op unit x : Set)
  requires monoid : IsMonoid(A, op, unit)
  requires xInA : x ∈ A
  shows op(unit, x) = x
proof
  obtain ⟨unitInA, laws⟩ := IsMonoid.identity with monoid
  obtain ⟨left, right⟩ := laws with x, xInA
  exact left

theorem IsMonoid.right_identity (A op unit x : Set)
  requires monoid : IsMonoid(A, op, unit)
  requires xInA : x ∈ A
  shows op(x, unit) = x
proof
  obtain ⟨unitInA, laws⟩ := IsMonoid.identity with monoid
  obtain ⟨left, right⟩ := laws with x, xInA
  exact right

theorem IsCommMonoid.monoid (A op unit : Set)
  requires h : IsCommMonoid(A, op, unit)
  shows IsMonoid(A, op, unit)
proof
  simp [IsCommMonoid]

theorem IsCommMonoid.commutative (A op unit : Set)
  requires h : IsCommMonoid(A, op, unit)
  shows Commutative(A, op)
proof
  simp [IsCommMonoid]

theorem IsGroup.magma (A op unit inv : Set)
  requires group : IsGroup(A, op, unit, inv)
  shows IsMagma(A, op)
proof
  have monoid := IsGroup.monoid with group
  have semigroup := IsMonoid.semigroup with monoid
  exact IsSemigroup.magma with semigroup

theorem IsGroup.inverse (A op unit inv : Set)
  requires h : IsGroup(A, op, unit, inv)
  shows Inverse(A, op, unit, inv)
proof
  simp [IsGroup]

theorem IsGroup.inverse_closed (A op unit inv x : Set)
  requires group : IsGroup(A, op, unit, inv)
  requires xInA : x ∈ A
  shows inv(x) ∈ A
proof
  obtain ⟨function, laws⟩ := IsGroup.inverse with group
  exact FunctionBetween.apply_closed with function, xInA

theorem IsGroup.inverse_left (A op unit inv x : Set)
  requires group : IsGroup(A, op, unit, inv)
  requires xInA : x ∈ A
  shows op(inv(x), x) = unit
proof
  obtain ⟨function, laws⟩ := IsGroup.inverse with group
  obtain ⟨left, right⟩ := laws with x, xInA
  exact left

theorem IsGroup.inverse_right (A op unit inv x : Set)
  requires group : IsGroup(A, op, unit, inv)
  requires xInA : x ∈ A
  shows op(x, inv(x)) = unit
proof
  obtain ⟨function, laws⟩ := IsGroup.inverse with group
  obtain ⟨left, right⟩ := laws with x, xInA
  exact right

theorem IsAbelianGroup.group (A op unit inv : Set)
  requires h : IsAbelianGroup(A, op, unit, inv)
  shows IsGroup(A, op, unit, inv)
proof
  simp [IsAbelianGroup]

theorem IsAbelianGroup.commutative (A op unit inv : Set)
  requires h : IsAbelianGroup(A, op, unit, inv)
  shows Commutative(A, op)
proof
  simp [IsAbelianGroup]

theorem Identity.in_carrier (A op unit : Set)
  requires h : Identity(A, op, unit)
  shows unit ∈ A
proof
  simp [Identity]

theorem Identity.unique (A op e f : Set)
  requires he : Identity(A, op, e)
  requires hf : Identity(A, op, f)
  shows e = f
proof
  rcases he with ⟨heA, heLaws⟩
  rcases hf with ⟨hfA, hfLaws⟩
  specialize heLaws with f, hfA
  rcases heLaws with ⟨hef, hfe⟩
  specialize hfLaws with e, heA
  rcases hfLaws with ⟨hfe2, hef2⟩
  rwa ← hef2

theorem IsInverse.unique (A op unit a b c : Set)
  requires monoid : IsMonoid(A, op, unit)
  requires hb : IsInverse(A, op, unit, a, b)
  requires hc : IsInverse(A, op, unit, a, c)
  shows b = c
proof
  have monoidStructure := monoid
  rcases monoid with ⟨semigroup, identity⟩
  rcases semigroup with ⟨magma, associative⟩
  rcases identity with ⟨unitA, identityLaws⟩
  rcases hb with ⟨aA, bA, hba, hab⟩
  rcases hc with ⟨aA2, cA, hca, hac⟩
  specialize identityLaws with b, bA
  rcases identityLaws with ⟨unitB, bUnit⟩
  obtain ⟨unitA2, identityLawsC⟩ := IsMonoid.identity with monoidStructure
  specialize identityLawsC with c, cA
  rcases identityLawsC with ⟨unitC, cUnit⟩
  specialize associative with b, bA, a, aA, c, cA
  rewrite ← bUnit
  rewrite ← hac
  rewrite ← associative
  rwa hba

theorem IsGroup.inverse_unit (A op unit inv : Set)
  requires group : IsGroup(A, op, unit, inv)
  shows inv(unit) = unit
proof
  have monoid := IsGroup.monoid with group
  have unitInA := IsMonoid.unit_in_carrier with monoid
  have inverseUnitInA := IsGroup.inverse_closed with group, unitInA
  have inverseEquation := IsGroup.inverse_left with group, unitInA
  have unitEquation := IsMonoid.right_identity with monoid, inverseUnitInA
  rwa unitEquation at inverseEquation

theorem IsGroup.inverse_involutive (A op unit inv x : Set)
  requires group : IsGroup(A, op, unit, inv)
  requires xInA : x ∈ A
  shows inv(inv(x)) = x
proof
  have monoid := IsGroup.monoid with group
  have inverseXInA := IsGroup.inverse_closed with group, xInA
  have inverseInverseXInA := IsGroup.inverse_closed with group, inverseXInA
  have inverseLeft := IsGroup.inverse_left with group, xInA
  have inverseRight := IsGroup.inverse_right with group, xInA
  have twiceLeft := IsGroup.inverse_left with group, inverseXInA
  have twiceRight := IsGroup.inverse_right with group, inverseXInA
  have first : IsInverse(A, op, unit, inv(x), x)
    unfold IsInverse
    refine ⟨inverseXInA, xInA, inverseRight, inverseLeft⟩
  have second : IsInverse(A, op, unit,
      inv(x), inv(inv(x)))
    unfold IsInverse
    refine ⟨inverseXInA, inverseInverseXInA, twiceLeft, twiceRight⟩
  have unique := IsInverse.unique with monoid, first, second
  cc

theorem IsAbelianGroup.four_shuffle (A op unit inv a b c d : Set)
  requires group : IsAbelianGroup(A, op, unit, inv)
  requires aInA : a ∈ A
  requires bInA : b ∈ A
  requires cInA : c ∈ A
  requires dInA : d ∈ A
  shows op(op(a, b), op(c, d)) =
    op(op(a, c), op(b, d))
proof
  have ordinary := IsAbelianGroup.group with group
  have monoid := IsGroup.monoid with ordinary
  have associative := IsMonoid.associative with monoid
  have commutative := IsAbelianGroup.commutative with group
  have cdInA := IsMonoid.closed with monoid, cInA, dInA
  have bdInA := IsMonoid.closed with monoid, bInA, dInA
  have outerLeft := Associative.law with associative, aInA, bInA, cdInA
  have middleLeft := Associative.law with associative, bInA, cInA, dInA
  have swap := commutative with b, bInA, c, cInA
  have middleRight := Associative.law with associative, cInA, bInA, dInA
  have outerRight := Associative.law with associative, aInA, cInA, bdInA
  cc

theorem IsAbelianGroup.inverse_op (A op unit inv x y : Set)
  requires group : IsAbelianGroup(A, op, unit, inv)
  requires xInA : x ∈ A
  requires yInA : y ∈ A
  shows inv(op(x, y)) =
    op(inv(x), inv(y))
proof
  have ordinary := IsAbelianGroup.group with group
  have monoid := IsGroup.monoid with ordinary
  have inverseXInA := IsGroup.inverse_closed with ordinary, xInA
  have inverseYInA := IsGroup.inverse_closed with ordinary, yInA
  have xyInA := IsMonoid.closed with monoid, xInA, yInA
  have inverseXYInA := IsGroup.inverse_closed with ordinary, xyInA
  have candidateInA := IsMonoid.closed with monoid, inverseXInA, inverseYInA
  have shuffle := IsAbelianGroup.four_shuffle with group, inverseXInA, inverseYInA, xInA, yInA
  have inverseX := IsGroup.inverse_left with ordinary, xInA
  have inverseY := IsGroup.inverse_left with ordinary, yInA
  have unitInA := IsMonoid.unit_in_carrier with monoid
  have unitUnit := IsMonoid.left_identity with monoid, unitInA
  have candidateLeft : call2(op,
      op(inv(x), inv(y)), op(x, y)) = unit
    rwa [shuffle, inverseX, inverseY]
  have commutative := IsAbelianGroup.commutative with group
  have candidateSwap := commutative with
    op(inv(x), inv(y)), candidateInA,
    op(x, y), xyInA
  have candidateRight : call2(op, call2(op, x, y),
      op(inv(x), inv(y))) = unit
    rwa ← candidateSwap
  have canonical : IsInverse(A, op, unit,
      op(x, y), inv(op(x, y)))
    unfold IsInverse
    refine ⟨xyInA, inverseXYInA, _, _⟩
    . exact IsGroup.inverse_left at
        A, op, unit, inv, op(x, y) with ordinary, xyInA
    . exact IsGroup.inverse_right at
        A, op, unit, inv, op(x, y) with ordinary, xyInA
  have candidate : IsInverse(A, op, unit,
      op(x, y), op(inv(x), inv(y)))
    unfold IsInverse
    refine ⟨xyInA, candidateInA, candidateLeft, candidateRight⟩
  exact IsInverse.unique with monoid, canonical, candidate

-- The inverse of a product reverses the factors.
theorem IsGroup.inverse_op (A op unit inv a b : Set)
  requires group : IsGroup(A, op, unit, inv)
  requires ha : a ∈ A
  requires hb : b ∈ A
  shows inv(op(a, b)) = op(inv(b), inv(a))
proof
  have monoid := group.left
  have associative := IsMonoid.associative with monoid
  have product := IsMonoid.closed with monoid, ha, hb
  have invA := IsGroup.inverse_closed with group, ha
  have invB := IsGroup.inverse_closed with group, hb
  have invProduct := IsGroup.inverse_closed with group, product
  have candidate := IsMonoid.closed with monoid, invB, invA
  have leftInverse := IsGroup.inverse_left with group, product
  have rearranged : op(op(inv(b), inv(a)), op(a, b)) = unit
    have step1 := Associative.law with associative, candidate, ha, hb
    have step2 := Associative.law with associative, invB, invA, ha
    have cancelA := IsGroup.inverse_left with group, ha
    have unitRight := IsMonoid.right_identity with monoid, invB
    have cancelB := IsGroup.inverse_left with group, hb
    rwa [← step1, step2, cancelA, unitRight]
  have equalProducts : op(inv(op(a, b)), op(a, b)) = op(op(inv(b), inv(a)), op(a, b))
    rw [leftInverse, rearranged]
    rfl
  have rightCancel : ∀ x ∈ A, ∀ y ∈ A, op(x, op(a, b)) = op(y, op(a, b)) → x = y
    intros x hx y hy equal
    have invProductIn := IsGroup.inverse_closed with group, product
    have cancelX : op(op(x, op(a, b)), inv(op(a, b))) = x
      have assoc := Associative.law with associative, hx, product, invProductIn
      have right := IsGroup.inverse_right with group, product
      have identity := IsMonoid.right_identity with monoid, hx
      rwa [assoc, right]
    have cancelY : op(op(y, op(a, b)), inv(op(a, b))) = y
      have assoc := Associative.law with associative, hy, product, invProductIn
      have right := IsGroup.inverse_right with group, product
      have identity := IsMonoid.right_identity with monoid, hy
      rwa [assoc, right]
    rw [equal, cancelY] at cancelX
    symm at cancelX
    exact cancelX
  have forX := rightCancel with invProduct
  have forXY := forX with candidate
  exact forXY with equalProducts