-- Homework 6
--
-- Math 4680/5680, "Topics in Logic and Computation"
-- Fall 2026
--
-- Due: November 3, 2026
--
-- Group members (up to 3):
-- _______________________
-- _______________________
-- _______________________
--
-- ============================================================
-- This homework is based on the first three pages of Chapter 1 from
-- Hungerford's "Algebra" (pp. 24-26).
--
-- Thomas W. Hungerford. "Algebra", 1974. Springer Graduate Texts
-- in Mathematics 73.
--
-- Note that this is not the same as his "Abstract Algebra" book. A
-- PDF with these pages is posted on Brightspace.
--
-- ============================================================

set_option autoImplicit false
set_option linter.unusedVariables false

namespace Semigroup

-- ============================================================
-- Below we provide types of semigroups, monoids, and groups by
-- starting with a structure `Semigroup` and extending to `Monoid` and
-- `Group`.

--  Definition 1.1.i
--
structure Semigroup where
  carrier : Type
  nonempty : Nonempty carrier
  mul : carrier → carrier → carrier
  mul_assoc : ∀ a b c, mul (mul a b) c = mul a (mul b c)

-- We provide some notations: `|S|` for the carrier, and `•` (type it
-- as `\bu`) for multiplication.

-- The `atomic`/`noWs` business means `|S|` must be written without
-- spaces, so that `|` is still available for `match` alternatives.
-- As a result, `|S|` will work but `| S |` will not.

macro:max atomic("|" noWs) S:term noWs "|" : term => `(Semigroup.carrier $S)

-- `a • b` is notation for multiplication. The `_` is the semigroup,
-- which Lean infers from the types of `a` and `b`.

infixl:70 " • " => Semigroup.mul _

-- The following is a neat trick you have not seen yet. This
-- "coercion" lets us write `x : S` as an abbreviation for `x : |S|`,
-- i.e., Lean inserts the carrier for us when a semigroup is used
-- where a type is expected.

instance : CoeSort Semigroup Type := ⟨Semigroup.carrier⟩

-- ============================================================
--  Definition 1.1.ii

structure Monoid extends Semigroup where
  one : carrier
  one_mul : ∀ a, mul one a = a
  mul_one : ∀ a, mul a one = a

-- The same notations work for monoids, via these coercions.

instance : CoeSort Monoid Type := ⟨fun M => M.carrier⟩
instance : Coe Monoid Semigroup := ⟨Monoid.toSemigroup⟩

def IsMonoid (S : Semigroup) : Prop :=
  ∃ e : S,
    (∀ a, e • a = a) ∧
    (∀ a, a • e = a)

--  [Foundations] Sanity check.

theorem monoid_is_monoid (M : Monoid) : IsMonoid M.toSemigroup := by
  sorry

-- ============================================================
--  Definition 1.1.iii

structure Group extends Monoid where
  inv : carrier → carrier
  inv_mul : ∀ a, mul (inv a) a = one
  mul_inv : ∀ a, mul a (inv a) = one

instance : CoeSort Group Type := ⟨fun G => G.carrier⟩
instance : Coe Group Semigroup := ⟨fun G => G.toMonoid.toSemigroup⟩

-- `a⁻¹` (type it as `\inv` or `\-1`) is a notation for the inverse.

postfix:max "⁻¹" => Group.inv _

def IsGroup (S : Semigroup) : Prop :=
  ∃ e : S,
    (∀ a, e • a = a) ∧
    (∀ a, a • e = a) ∧
    (∀ a, ∃ b, b • a = e ∧ a • b = e)


-- ============================================================
--  Definition 1.1.iv

--  [Foundations] Now define the type `Ab` of abelian groups in a
--  similar way.

structure Ab extends Group where
-- your code goes here

def IsAbelian (S : Semigroup) : Prop :=
  ∀ a b : S, a • b = b • a

-- ============================================================
--  [Foundations] Theorem 1.2

theorem one_unique (M : Monoid) (e : M)
    (hleft : ∀ a, e • a = a)
    (hright : ∀ a, a • e = a) : e = M.one := by
  sorry

namespace Group

variable (G : Group)

--  [Proficiency] Theorem 1.2.i

theorem idemp_eq_one (c : G) (h : c • c = c) :
    c = G.one := by
  sorry

--  [Proficiency] Theorem 1.2.ii

theorem left_cancel (a b c : G) (h : a • b = a • c) :
    b = c := by
  sorry

theorem right_cancel (a b c : G) (h : b • a = c • a) :
    b = c := by
  sorry

--  [Proficiency] Theorem 1.2.iii

theorem inv_unique (a b : G)
    (hleft : b • a = G.one) (hright : a • b = G.one) :
    b = a⁻¹ := by
  sorry

--  [Proficiency] Theorem 1.2.iv

theorem inv_inv (a : G) : (a⁻¹)⁻¹ = a := by
  sorry

--  [Proficiency] Theorem 1.2.v

theorem inv_product (a b : G) :
    (a • b)⁻¹ = b⁻¹ • a⁻¹ := by
  sorry

-- ============================================================
--  [Mastery] Theorem 1.2.vi
--
theorem mul_eq_iff (a b x : G) :
    a • x = b ↔ x = a⁻¹ • b := by
  sorry

theorem eq_mul_iff (a b y : G) :
    y • a = b ↔ y = b • a⁻¹ := by
  sorry

end Group

--  [Mastery] Proposition 1.3

theorem group_has_left_identity (S : Semigroup) (h : IsGroup S) :
    ∃ e : S, ∀ a, e • a = a := by
  sorry

theorem group_has_left_inverses (S : Semigroup) (h : IsGroup S)
    (e : S) (hleft : ∀ a, e • a = a) :
    ∀ a, ∃ b, b • a = e := by
  sorry

theorem group_of_left_axioms (S : Semigroup) (e : S)
    (hleft : ∀ a, e • a = a)
    (hinv : ∀ a, ∃ b, b • a = e) : IsGroup S := by
  sorry

--  [Mastery] Remark following Proposition 1.3

theorem group_has_right_identity (S : Semigroup) (h : IsGroup S) :
    ∃ e : S, ∀ a, a • e = a := by
  sorry

theorem group_has_right_inverses (S : Semigroup) (h : IsGroup S)
    (e : S) (hright : ∀ a, a • e = a) :
    ∀ a, ∃ b, a • b = e := by
  sorry

theorem group_of_right_axioms (S : Semigroup) (e : S)
    (hright : ∀ a, a • e = a)
    (hinv : ∀ a, ∃ b, a • b = e) : IsGroup S := by
  sorry

--  [Mastery] Proposition 1.4

theorem group_has_mul_solutions (S : Semigroup) (h : IsGroup S)
    (a b : S) : ∃ x, a • x = b := by
  sorry

theorem group_has_solutions_mul (S : Semigroup) (h : IsGroup S)
    (a b : S) : ∃ y, y • a = b := by
  sorry

-- Nonemptiness is essential in the following: an empty carrier would
-- satisfy both hypotheses, but it shouldn't be a group.
theorem group_of_solutions (S : Semigroup)
    (hmul_left : ∀ a b : S, ∃ x, a • x = b)
    (hmul_right : ∀ a b : S, ∃ y, y • a = b) :
    IsGroup S := by
  sorry


-- ============================================================
--
-- Instead of the first examples from Hungerford, we will use the
-- semigroup of positive natural numbers (which is not a monoid), the
-- monoid of natural numbers (which is not a group), and the group of
-- integers (which is abelian).
--
-- Hungerford notes that an operation written additively has identity
-- `0` and inverse `-a`. Our notation is multiplicative throughout, so
-- in these three examples `•` is addition, `one` is 0, and `inv` is
-- negation.
--
--  [Foundations] The natural numbers under addition form a monoid.

def MyNat : Monoid where
  carrier := Nat
  nonempty := by sorry
  mul := Nat.add
  mul_assoc := by sorry
  one := sorry
  one_mul := by sorry
  mul_one := by sorry

--  [Proficiency] Show that this monoid is not a group.

theorem mynat_is_not_group : ¬ IsGroup MyNat.toSemigroup := by
  sorry

-- ============================================================
--  [Proficiency] Positive naturals under addition: a semigroup need
--  not be a monoid.

inductive Pos : Nat → Prop where
  | base : Pos 1
  | step : ∀ {n : Nat}, Pos n → Pos (n + 1)

structure PosNat where
  val : Nat
  positive : Pos val

def posNatAdd (a b : PosNat) : PosNat :=
  ⟨a.val + b.val, by sorry⟩

def MyPosNat : Semigroup where
  carrier := PosNat
  nonempty := by sorry
  mul := posNatAdd
  mul_assoc := by sorry

theorem myposnat_is_not_monoid : ¬ IsMonoid MyPosNat := by
  sorry

-- ============================================================
--  [Foundations] The integers under addition form an abelian group.

def MyInt : Group where
  carrier := Int
  nonempty := by sorry
  mul := Int.add
  mul_assoc := by sorry
  one := sorry
  one_mul := by sorry
  mul_one := by sorry
  inv := sorry
  inv_mul := by sorry
  mul_inv := by sorry

theorem myint_is_abelian : IsAbelian MyInt.toSemigroup := by
  sorry

-- ============================================================
--
-- Both investigations are about the second example in Hungerford: the
-- group of symmetries of the square, a nonabelian group of order 8. In
-- Investigation A, the vertices of the square are treated as an
-- inductive type. In Investigation B, they are a structure built from
-- the structure `Point` from Lecture 11 (repeated below). Choose your
-- poison.
--
-- ============================================================
-- Investigation A: square symmetries with inductive vertices
-- ------------------------------------------------------------

namespace Square

-- Vertices 1, 2, 3, 4 run clockwise from the top left.
inductive Vertex where
  | v1 | v2 | v3 | v4

structure Map where
  image1 : Vertex
  image2 : Vertex
  image3 : Vertex
  image4 : Vertex

def act (m : Map) : Vertex → Vertex
  | .v1 => m.image1
  | .v2 => m.image2
  | .v3 => m.image3
  | .v4 => m.image4

def identityMap : Map := ⟨.v1, .v2, .v3, .v4⟩

-- `compose s t` applies `t` first, then `s`.
def compose (s t : Map) : Map :=
  ⟨act s t.image1, act s t.image2, act s t.image3, act s t.image4⟩

def opposite : Vertex → Vertex
  | .v1 => .v3
  | .v2 => .v4
  | .v3 => .v1
  | .v4 => .v2

-- Symmetries are invertible maps preserving opposite vertices.
structure Symmetry where
  map : Map
  inverse : Map
  left_inv : compose inverse map = identityMap
  right_inv : compose map inverse = identityMap
  preserves_opposites : ∀ v, act map (opposite v) = opposite (act map v)

-- A counterclockwise quarter-turn and a reflection across the `x`-axis.
def rot90 : Symmetry where
  map := sorry
  inverse := sorry
  left_inv := by sorry
  right_inv := by sorry
  preserves_opposites := by sorry

def reflectX : Symmetry where
  map := sorry
  inverse := sorry
  left_inv := by sorry
  right_inv := by sorry
  preserves_opposites := by sorry

def D4 : Group where
  carrier := Symmetry
  nonempty := by sorry
  mul := sorry
  mul_assoc := by sorry
  one := sorry
  one_mul := by sorry
  mul_one := by sorry
  inv := sorry
  inv_mul := by sorry
  mul_inv := by sorry

theorem rotation_four :
    D4.mul rot90 (D4.mul rot90 (D4.mul rot90 rot90)) = D4.one := by
  sorry

theorem reflection_square : D4.mul reflectX reflectX = D4.one := by
  sorry

theorem not_commutative :
    D4.mul rot90 reflectX ≠ D4.mul reflectX rot90 := by
  sorry

-- REPORT:

end Square

-- ============================================================
-- Investigation B: square symmetries with Point
-- ------------------------------------------------------------

-- Repeat Investigation A using coordinates for the four vertices.

namespace SquarePoints

structure Point where
  x : Nat
  y : Nat

structure Vertex extends Point where
  x_valid : x = 0 ∨ x = 1
  y_valid : y = 0 ∨ y = 1

def v1 : Vertex := ⟨⟨0, 1⟩, Or.inl rfl, Or.inr rfl⟩
def v2 : Vertex := ⟨⟨1, 1⟩, Or.inr rfl, Or.inr rfl⟩
def v3 : Vertex := ⟨⟨1, 0⟩, Or.inr rfl, Or.inl rfl⟩
def v4 : Vertex := ⟨⟨0, 0⟩, Or.inl rfl, Or.inl rfl⟩

def fromInductive : Square.Vertex → Vertex :=
  sorry

def toInductive : Vertex → Square.Vertex :=
  sorry

theorem toInductive_fromInductive (v : Square.Vertex) :
    toInductive (fromInductive v) = v := by
  sorry

theorem fromInductive_toInductive (v : Vertex) :
    fromInductive (toInductive v) = v := by
  sorry

structure Map where
  image1 : Vertex
  image2 : Vertex
  image3 : Vertex
  image4 : Vertex

def act (m : Map) (v : Vertex) : Vertex :=
  match v.x, v.y with
  | 0, 1 => m.image1
  | 1, 1 => m.image2
  | 1, 0 => m.image3
  | _, _ => m.image4

def identityMap : Map := ⟨v1, v2, v3, v4⟩

-- `compose s t` applies `t` first, then `s`.
def compose (s t : Map) : Map :=
  ⟨act s t.image1, act s t.image2, act s t.image3, act s t.image4⟩

def opposite (v : Vertex) : Vertex :=
  match v.x, v.y with
  | 0, 1 => v3
  | 1, 1 => v4
  | 1, 0 => v1
  | _, _ => v2

theorem fromInductive_opposite (v : Square.Vertex) :
    fromInductive (Square.opposite v) = opposite (fromInductive v) := by
  sorry

-- Symmetries are invertible maps preserving opposite vertices.
structure Symmetry where
  map : Map
  inverse : Map
  left_inv : compose inverse map = identityMap
  right_inv : compose map inverse = identityMap
  preserves_opposites : ∀ v, act map (opposite v) = opposite (act map v)

-- A counterclockwise quarter-turn and a reflection across the `x`-axis.
-- Hungerford centers the square at the origin, but our square has its
-- corners at (0,0) and (1,1), so `reflectX` is really the reflection
-- across the horizontal line through the center of the square.
def rot90 : Symmetry where
  map := sorry
  inverse := sorry
  left_inv := by sorry
  right_inv := by sorry
  preserves_opposites := by sorry

def reflectX : Symmetry where
  map := sorry
  inverse := sorry
  left_inv := by sorry
  right_inv := by sorry
  preserves_opposites := by sorry

def D4 : Group where
  carrier := Symmetry
  nonempty := by sorry
  mul := sorry
  mul_assoc := by sorry
  one := sorry
  one_mul := by sorry
  mul_one := by sorry
  inv := sorry
  inv_mul := by sorry
  mul_inv := by sorry

theorem rotation_four :
    D4.mul rot90 (D4.mul rot90 (D4.mul rot90 rot90)) = D4.one := by
  sorry

theorem reflection_square : D4.mul reflectX reflectX = D4.one := by
  sorry

theorem not_commutative :
    D4.mul rot90 reflectX ≠ D4.mul reflectX rot90 := by
  sorry

-- REPORT:

end SquarePoints

-- ============================================================

--  [Bonus] Give an example of a group that is not abelian.

def MyGroup : Group := sorry

theorem mygroup_is_not_abelian : ¬ IsAbelian MyGroup.toSemigroup := by
  sorry

end Semigroup

-- ============================================================

--  [Bonus] A type `A : Type` is finite if there exists a list
--  containing each element `a : A`.

namespace Finiteness

open Semigroup

def IsFinite (A : Type) : Prop :=
  ∃ xs : List A, ∀ a : A, a ∈ xs

-- Show that `Bool` is finite. Hint: `cases`, `List.Mem.head`,
-- `List.Mem.tail`.

theorem bool_is_finite : IsFinite Bool := by
  sorry

--  [Bonus] Turn `Bool` into a group: your first finite group (or your
--  second, if you did one of the investigations).

def boolGroup : Group := sorry

theorem boolGroup_is_finite : IsFinite |boolGroup| := by
  sorry

end Finiteness