-- Bundled groups: a group as one structure of its carrier, operation, unit,
-- and inverse, the laws of a group under their standard names, and the
-- group rewrite set
-- 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.Basic
import Core

-- A group is a structure of its carrier, its operation graph, its unit, and
-- its inverse graph, built by Group.mk(A, m, e, i) and read back by the
-- projections G.carrier, G.mul, G.one, and G.inv. The operation applies to
-- two arguments, G.mul(x, y), and the inverse as a function, G.inv(x).
-- Group(G) says that G is such a structure whose data satisfy the laws
-- below, under their standard names; Group.Data(G) is the shape alone, and
-- Group.intro builds a group from its four pieces and the laws.
structure Group
  | carrier : Set
  | mul : carrier × carrier → carrier
  | one : carrier
  | inv : carrier → carrier
  where
    mul_assoc : ∀ a b c ∈ carrier, mul(mul(a, b), c) = mul(a, mul(b, c))
    one_mul : ∀ a ∈ carrier, mul(one, a) = a
    mul_one : ∀ a ∈ carrier, mul(a, one) = a
    inv_mul : ∀ a ∈ carrier, mul(inv(a), a) = one
    mul_inv : ∀ a ∈ carrier, mul(a, inv(a)) = one

-- The projection laws of a constructed group as one rewrite set.
tactic group_projections := simp [Group.mk.carrier, Group.mk.mul, Group.mk.one, Group.mk.inv]

-- The monoid and the abelian group as properties of the same structure:
-- Monoid(G) is the unbundled monoid at the projections, and AbelianGroup(G)
-- is a group whose operation commutes. IsMonoid(A, m, e), IsGroup(A, m, e, i),
-- and IsAbelianGroup(A, m, e, i) remain the forms over separate pieces.
predicate Monoid (G : Set) := Group.Data(G) ∧ IsMonoid(G.carrier, G.mul, G.one)
predicate AbelianGroup (G : Set) := Group(G) ∧ Commutative(G.carrier, G.mul)

-- The operation is written a * b and the inverse a⁻¹ wherever a hypothesis
-- in scope supplies the group; the operands' membership in G.carrier
-- selects the group when several are in scope. Under the same hypotheses a
-- binder (a : G) is a set variable with a ∈ G.carrier.
notation infixl 70 "*" => call2(G.mul, _, _) via hypothesis Monoid(G) for G.carrier
notation infixl 70 "*" => call2(G.mul, _, _) via hypothesis Group(G) for G.carrier
notation infixl 70 "*" => call2(G.mul, _, _) via hypothesis AbelianGroup(G) for G.carrier
notation postfix 90 "⁻¹" => apply(G.inv, _) via hypothesis Group(G) for G.carrier
notation postfix 90 "⁻¹" => apply(G.inv, _) via hypothesis AbelianGroup(G) for G.carrier

-- Bridges between the structure and the forms over separate pieces.
theorem Group.parts (G : Set)
  requires group : Group(G)
  shows IsGroup(G.carrier, G.mul, G.one, G.inv)
proof
  obtain ⟨shape, mulF, oneIn, invF, assoc, oneMul, mulOne, invMul, mulInv⟩ := group
  unfold IsGroup
  constructor
  . unfold IsMonoid
    constructor
    . unfold IsSemigroup
      constructor
      . exact mulF
      . unfold Associative
        exact assoc
    . unfold Identity
      refine ⟨oneIn, ?_⟩
      intros x xIn
      have left := oneMul with x, xIn
      have right := mulOne with x, xIn
      exact ⟨left, right⟩
  . unfold Inverse
    refine ⟨invF, ?_⟩
    intros x xIn
    have left := invMul with x, xIn
    have right := mulInv with x, xIn
    exact ⟨left, right⟩

theorem Group.of_parts (A m e i : Set)
  requires group : IsGroup(A, m, e, i)
  shows Group(Group.mk(A, m, e, i))
proof
  have monoid := IsGroup.monoid with group
  have mulF := IsGroup.magma with group
  have assoc := IsMonoid.associative with monoid
  have oneIn := IsMonoid.unit_in_carrier with monoid
  obtain ⟨invF, inverses⟩ := IsGroup.inverse with group
  apply Group.intro
  . exact mulF
  . exact oneIn
  . exact invF
  . unfold Associative at assoc
    exact assoc
  . intros x xIn
    exact IsMonoid.left_identity with monoid, xIn
  . intros x xIn
    exact IsMonoid.right_identity with monoid, xIn
  . intros x xIn
    have both := inverses with x, xIn
    exact both.left
  . intros x xIn
    have both := inverses with x, xIn
    exact both.right

theorem Monoid.parts (G : Set)
  requires monoid : Monoid(G)
  shows IsMonoid(G.carrier, G.mul, G.one)
proof
  obtain ⟨shape, laws⟩ := monoid
  exact laws

theorem Monoid.of_parts (A m e i : Set)
  requires monoid : IsMonoid(A, m, e)
  shows Monoid(Group.mk(A, m, e, i))
proof
  have shape := Group.mk.data at A, m, e, i
  unfold Monoid
  group_projections

theorem AbelianGroup.parts (G : Set)
  requires abelian : AbelianGroup(G)
  shows IsAbelianGroup(G.carrier, G.mul, G.one, G.inv)
proof
  obtain ⟨group, commutative⟩ := abelian
  have parts := Group.parts with group
  unfold IsAbelianGroup
  exact ⟨parts, commutative⟩

theorem AbelianGroup.of_parts (A m e i : Set)
  requires abelian : IsAbelianGroup(A, m, e, i)
  shows AbelianGroup(Group.mk(A, m, e, i))
proof
  have group := Group.of_parts with (IsAbelianGroup.group with abelian)
  have commutative := IsAbelianGroup.commutative with abelian
  unfold AbelianGroup
  group_projections

theorem Group.to_monoid (G : Set)
  requires group : Group(G)
  shows Monoid(G)
proof
  obtain ⟨shape, rest⟩ := group
  have parts := Group.parts with group
  unfold Monoid
  exact ⟨shape, IsGroup.monoid with parts⟩

theorem AbelianGroup.to_group (G : Set)
  requires abelian : AbelianGroup(G)
  shows Group(G)
proof
  obtain ⟨group, commutative⟩ := abelian
  exact group

-- A group is the constructor applied to its projections.
theorem Group.eta_of_group (G : Set)
  requires group : Group(G)
  shows G = Group.mk(G.carrier, G.mul, G.one, G.inv)
proof
  obtain ⟨shape, rest⟩ := group
  exact Group.eta with shape

section GroupLaws
variable (G : Set)
hypothesis group : Group(G)

-- Closure: the operation, unit, and inverse stay in the carrier. These are
-- instances, so the membership of a compound term is synthesized.
instance Group.mul_mem (a b : G)
  shows a * b ∈ G
proof
  have monoid := IsGroup.monoid with (Group.parts with group)
  exact IsMonoid.closed with monoid, *

instance Group.one_mem
  shows G.one ∈ G
proof
  have monoid := IsGroup.monoid with (Group.parts with group)
  exact IsMonoid.unit_in_carrier with monoid

instance Group.inv_mem (a : G)
  shows a⁻¹ ∈ G
proof
  have parts := Group.parts with group
  exact IsGroup.inverse_closed with parts, *

theorem Group.operation_function
  shows G.mul : G.carrier × G.carrier → G.carrier
proof
  have monoid := IsGroup.monoid with (Group.parts with group)
  have semigroup := IsMonoid.semigroup with monoid
  exact IsSemigroup.magma with semigroup

theorem Group.inverse_function
  shows G.inv : G.carrier → G.carrier
proof
  obtain ⟨function, laws⟩ := IsGroup.inverse with (Group.parts with group)
  exact function

-- The laws, under their standard names: the familiar underscore names, and
-- the dotted Group.inv_mul, Group.mul_inv, and Group.inv_involutive.
theorem mul_assoc (a b c : G)
  shows a * b * c = a * (b * c)
proof
  have monoid := IsGroup.monoid with (Group.parts with group)
  have associative := IsMonoid.associative with monoid
  exact Associative.law with associative, *

theorem one_mul (a : G)
  shows G.one * a = a
proof
  have monoid := IsGroup.monoid with (Group.parts with group)
  exact IsMonoid.left_identity with monoid, *

theorem mul_one (a : G)
  shows a * G.one = a
proof
  have monoid := IsGroup.monoid with (Group.parts with group)
  exact IsMonoid.right_identity with monoid, *

theorem Group.inv_mul (a : G)
  shows a⁻¹ * a = G.one
proof
  have parts := Group.parts with group
  exact IsGroup.inverse_left with parts, *

theorem Group.mul_inv (a : G)
  shows a * a⁻¹ = G.one
proof
  have parts := Group.parts with group
  exact IsGroup.inverse_right with parts, *

theorem inv_mul_cancel_left (a b : G)
  shows a⁻¹ * (a * b) = b
proof
  rw [← mul_assoc, Group.inv_mul, one_mul]
  rfl

theorem mul_inv_cancel_left (a b : G)
  shows a * (a⁻¹ * b) = b
proof
  rw [← mul_assoc, Group.mul_inv, one_mul]
  rfl

theorem mul_inv_cancel_right (a b : G)
  shows a * b * b⁻¹ = a
proof
  rw [mul_assoc, Group.mul_inv, mul_one]
  rfl

theorem inv_mul_cancel_right (a b : G)
  shows a * b⁻¹ * b = a
proof
  rw [mul_assoc, Group.inv_mul, mul_one]
  rfl

theorem mul_left_cancel (a b c : G)
  requires equal : a * b = a * c
  shows b = c
proof
  calc
    b = a⁻¹ * (a * b) := by rw inv_mul_cancel_left
    _ = a⁻¹ * (a * c) := by rw equal
    _ = c := by rw inv_mul_cancel_left

theorem mul_right_cancel (a b c : G)
  requires equal : a * b = c * b
  shows a = c
proof
  calc
    a = a * b * b⁻¹ := by rw mul_inv_cancel_right
    _ = c * b * b⁻¹ := by rw equal
    _ = c := by rw mul_inv_cancel_right

theorem mul_right_inj (a b c : G)
  shows a * b = a * c ↔ b = c
proof
  constructor
  . intro equal
    exact mul_left_cancel with *
  . intro equal
    rw equal
    rfl

theorem mul_left_inj (a b c : G)
  shows a * b = c * b ↔ a = c
proof
  constructor
  . intro equal
    exact mul_right_cancel with *
  . intro equal
    rw equal
    rfl

theorem inv_one
  shows G.one⁻¹ = G.one
proof
  have cancel : G.one⁻¹ * G.one = G.one := Group.inv_mul with *
  rwa mul_one at cancel

theorem eq_inv_of_mul_eq_one_left (a b : G)
  requires equal : a * b = G.one
  shows a = b⁻¹
proof
  calc
    a = a * b * b⁻¹ := by rw mul_inv_cancel_right
    _ = b⁻¹ := by rw [equal, one_mul]

theorem eq_inv_of_mul_eq_one_right (a b : G)
  requires equal : a * b = G.one
  shows b = a⁻¹
proof
  calc
    b = a⁻¹ * (a * b) := by rw inv_mul_cancel_left
    _ = a⁻¹ := by rw [equal, mul_one]

theorem inv_eq_of_mul_eq_one_right (a b : G)
  requires equal : a * b = G.one
  shows a⁻¹ = b
proof
  symm
  exact eq_inv_of_mul_eq_one_right with *

theorem inv_inv (a : G)
  shows (a⁻¹)⁻¹ = a
proof
  have cancel : a⁻¹ * a = G.one := Group.inv_mul with *
  exact inv_eq_of_mul_eq_one_right with *

theorem Group.inv_involutive (a : G)
  shows (a⁻¹)⁻¹ = a
proof
  exact inv_inv with *

theorem mul_inv_rev (a b : G)
  shows (a * b)⁻¹ = b⁻¹ * a⁻¹
proof
  have product : a * b * (b⁻¹ * a⁻¹) = G.one
    rw [mul_assoc, mul_inv_cancel_left, Group.mul_inv]
    rfl
  exact inv_eq_of_mul_eq_one_right with *

theorem mul_eq_one_iff_eq_inv (a b : G)
  shows a * b = G.one ↔ a = b⁻¹
proof
  constructor
  . intro equal
    exact eq_inv_of_mul_eq_one_left with *
  . intro equal
    rw [equal, Group.inv_mul]
    rfl

theorem mul_eq_one_iff_inv_eq (a b : G)
  shows a * b = G.one ↔ a⁻¹ = b
proof
  constructor
  . intro equal
    exact inv_eq_of_mul_eq_one_right with *
  . intro equal
    rw [← equal, Group.mul_inv]
    rfl

theorem inv_mul_eq_one (a b : G)
  shows a⁻¹ * b = G.one ↔ a = b
proof
  have criterion : a⁻¹ * b = G.one ↔ (a⁻¹)⁻¹ = b := mul_eq_one_iff_inv_eq with *
  rwa inv_inv at criterion

theorem mul_inv_eq_one (a b : G)
  shows a * b⁻¹ = G.one ↔ a = b
proof
  have criterion : a * b⁻¹ = G.one ↔ a = (b⁻¹)⁻¹ := mul_eq_one_iff_eq_inv with *
  rwa inv_inv at criterion

theorem inv_inj (a b : G)
  shows a⁻¹ = b⁻¹ ↔ a = b
proof
  constructor
  . intro equal
    have twiceA : (a⁻¹)⁻¹ = a := inv_inv with *
    have twiceB : (b⁻¹)⁻¹ = b := inv_inv with *
    cc
  . intro equal
    rw equal
    rfl

theorem inv_eq_one (a : G)
  shows a⁻¹ = G.one ↔ a = G.one
proof
  have criterion : a⁻¹ = G.one⁻¹ ↔ a = G.one := inv_inj with *
  rwa inv_one at criterion

theorem mul_self_eq_self (a : G)
  shows a * a = a ↔ a = G.one
proof
  constructor
  . intro idempotent
    calc
      a = a⁻¹ * (a * a) := by rw inv_mul_cancel_left
      _ = G.one := by rw [idempotent, Group.inv_mul]
  . intro equal
    rw [equal, one_mul]
    rfl

theorem mul_inv_eq_iff_eq_mul (a b c : G)
  shows a * b⁻¹ = c ↔ a = c * b
proof
  constructor
  . intro equal
    rw [← equal, inv_mul_cancel_right]
    rfl
  . intro equal
    rw [equal, mul_inv_cancel_right]
    rfl

theorem eq_inv_mul_iff_mul_eq (a b c : G)
  shows a = b⁻¹ * c ↔ b * a = c
proof
  constructor
  . intro equal
    rw [equal, mul_inv_cancel_left]
    rfl
  . intro equal
    rw [← equal, inv_mul_cancel_left]
    rfl

theorem inv_mul_eq_iff_eq_mul (a b c : G)
  shows a⁻¹ * b = c ↔ b = a * c
proof
  constructor
  . intro equal
    rw [← equal, mul_inv_cancel_left]
    rfl
  . intro equal
    rw [equal, inv_mul_cancel_left]
    rfl

theorem eq_mul_inv_iff_mul_eq (a b c : G)
  shows a = b * c⁻¹ ↔ a * c = b
proof
  constructor
  . intro equal
    rw [equal, inv_mul_cancel_right]
    rfl
  . intro equal
    rw [← equal, mul_inv_cancel_right]
    rfl

end GroupLaws

-- The group rewrite set: associativity to the right, the unit and inverse
-- cancellations, each applied where its operands are in the carrier.
tactic group_simp := simp [mul_assoc, one_mul, mul_one, Group.inv_mul, Group.mul_inv, inv_inv, inv_one, mul_inv_rev, inv_mul_cancel_left, mul_inv_cancel_left, mul_inv_cancel_right, inv_mul_cancel_right]

section AbelianLaws
variable (G : Set)
hypothesis abelian : AbelianGroup(G)

theorem mul_comm (a b : G)
  shows a * b = b * a
proof
  have commutative := IsAbelianGroup.commutative with (AbelianGroup.parts with abelian)
  exact Commutative.law with commutative, *

theorem mul_left_comm (a b c : G)
  shows a * (b * c) = b * (a * c)
proof
  have group := AbelianGroup.to_group with abelian
  have swap : a * b = b * a := mul_comm with *
  rw [← mul_assoc, swap, mul_assoc]
  rfl

theorem mul_right_comm (a b c : G)
  shows a * b * c = a * c * b
proof
  have group := AbelianGroup.to_group with abelian
  have swap : b * c = c * b := mul_comm with *
  rw [mul_assoc, swap, ← mul_assoc]
  rfl

theorem mul_mul_mul_comm (a b c d : G)
  shows a * b * (c * d) = a * c * (b * d)
proof
  have group := AbelianGroup.to_group with abelian
  have swap : b * (c * d) = c * (b * d) := mul_left_comm with *
  rw [mul_assoc, swap, ← mul_assoc]
  rfl

theorem mul_inv (a b : G)
  shows (a * b)⁻¹ = a⁻¹ * b⁻¹
proof
  have group := AbelianGroup.to_group with abelian
  have swap : b⁻¹ * a⁻¹ = a⁻¹ * b⁻¹ := mul_comm with *
  rw [mul_inv_rev, swap]
  rfl

end AbelianLaws