module Project3 where

-- In this project, we'll explore some elementary group theory. By
-- "elementary", I mean that we will explore some basic element-based
-- concepts of groups, but not set-based concepts like cosets and
-- quotients (which are harder to formalize in Agda).

open import Logic
open import Equality
open import Nat
open import Bool
open import Decidable

-- ----------------------------------------------------------------------
-- * Definition of a group

-- We define what it means to be a group structure on a set A,
-- similarly to what we did with monoids in class. Please note that
-- you can type \cdot to get the symbol ·, and \^-\^1 to get ⁻¹.
-- 
-- A group structure consists of 3 operations and 3 laws. By
-- "operation", I means multiplication (which is a binary operation),
-- inverse (which is a unary operation), and the identity (which is a
-- nullary operation, also called a constant).

record Group (A : Set) : Set where
  field
    -- Operations:
    _·_ : A -> A -> A
    e : A
    _⁻¹ : A -> A

    -- Laws:
    associativity-law : ∀ {x y z : A} -> (x · y) · z == x · (y · z)
    left-unit-law : ∀ {x : A} -> e · x == x
    left-inverse-law : ∀ {x : A} -> x ⁻¹ · x == e
    
  infix 7 _·_

open Group {{...}} 

-- For equational reasoning in groups, it is convenient to define the
-- following functions, which are special cases of "context". See the
-- next proof for an example of how they can be used.
on-left : ∀ {A} {{G : Group A}} {x y z : A} -> x == y -> x · z == y · z
on-left {x = x} {y} {z} hyp = context (λ c → c · z) hyp

on-right : ∀ {A} {{G : Group A}} {x y z : A} -> x == y -> z · x == z · y
on-right {x = x} {y} {z} hyp = context (λ c → z · c) hyp

-- ----------------------------------------------------------------------
-- * Some properties of the group operations

-- Did you know that the right inverse law follows from the left
-- inverse law, the left unit law, and associativity? In case you
-- didn't, here is a proof.
right-inverse-law : ∀ {A} {{G : Group A}} {x : A} -> x · x ⁻¹ == e
right-inverse-law {x = x} =
  equational x · x ⁻¹
          by symm left-unit-law
      equals e · (x · x ⁻¹)
          by on-left (symm left-inverse-law)
      equals ((x ⁻¹) ⁻¹ · x ⁻¹) · (x · x ⁻¹)
          by associativity-law
      equals (x ⁻¹) ⁻¹ · (x ⁻¹ · (x · x ⁻¹))
          by on-right (symm associativity-law)
      equals (x ⁻¹) ⁻¹ · ((x ⁻¹ · x) · x ⁻¹)
          by on-right (on-left left-inverse-law)
      equals (x ⁻¹) ⁻¹ · (e · x ⁻¹)
          by on-right left-unit-law
      equals (x ⁻¹) ⁻¹ · x ⁻¹
          by left-inverse-law
      equals e

-- 1. Similarly, the right unit law follows from the other laws. Prove
-- it. Hint: for the pencil-and-paper proof, simplify a · a ⁻¹ · a in
-- two different ways.
right-unit-law : ∀ {A} {{G : Group A}} {x : A} -> x · e == x
right-unit-law = {!!}

-- 2. Show that the right identity of a group is unique.
unique-right-unit : {A : Set} ->  {{G : Group A}} -> (x y : A) -> x · y == x -> y == e
unique-right-unit = {!!}

-- 3. Show that every right identity is a left identity.
unit-symm : {A : Set} ->  {{G : Group A}} -> (x y : A) -> x · y == x -> y · x == x
unit-symm = {!!}

-- 4. Show that x · y == e implies that x ⁻¹ == y.
right-inverse : {A : Set} ->  {{G : Group A}} -> (x y : A) -> x · y == e -> x ⁻¹ == y
right-inverse = {!!}

-- 5. Prove that the inverse operation is involutive.
involutive-inverse : {A : Set} ->  {{G : Group A}} -> (x : A) -> (x ⁻¹) ⁻¹ == x
involutive-inverse = {!!}

-- 6. Show that x · y == e implies y ⁻¹ == x
left-inverse : {A : Set} ->  {{G : Group A}} -> (x y : A) -> x · y == e -> y ⁻¹ == x
left-inverse = {!!}

-- 7. Show that (x · y) ⁻¹ == y ⁻¹ · x ⁻¹.
inverse-of-product : {A : Set} ->  {{G : Group A}} -> (x y : A) -> (x · y) ⁻¹ == y ⁻¹ · x ⁻¹
inverse-of-product = {!!}
    
-- ----------------------------------------------------------------------
-- * Group homomorphisms

-- If A and B are groups and f : A -> B is a function, we say that f
-- is a _group homomorphism_ if ∀ x y -> f (x · y) == f x · f y.
--
-- In Agda, we express this by saying that f is equipped with a "group
-- homomorphism structure", which is defined by a record similarly to
-- how we defined monoids or groups.

record GroupHom {A B : Set} {{G : Group A}} {{G' : Group B}} (f : A -> B) : Set where
  field
    groupHom : (x y : A) -> f (x · y) == f x · f y

open GroupHom {{...}}

-- 8. Prove that group homomorphisms preserve the identity. Hint: for
-- the pencil-and-paper proof, simplify f (e · e) in two different
-- ways. Then translate into Agda.
preserveUnit : {A B : Set} -> {{G : Group A}} -> {{G' : Group B}} -> (f : A -> B) -> {{r : GroupHom f}} -> f e == e
preserveUnit = {!!}

-- 9. Prove that group homomorphisms respect inverses.
preserveInverse : {A B : Set} -> {{G : Group A}} -> {{G' : Group B}} -> (f : A -> B) -> {{r : GroupHom f}} -> (a : A) -> f (a ⁻¹) == (f a) ⁻¹
preserveInverse = {!!}

-- ----------------------------------------------------------------------
-- * Group action on a set

-- If A is a group and X is a set, a function ● : A × X -> X
-- is called a _left action_ if ∀ g h x -> (g · h) ● x == g ● (h ● x).
--
-- In Agda, we can also express this as a record. A LeftAction is
-- given by three things: one operation and two laws.
--
-- Please note that you can type \cib to get the symbol ●. Here, "cib"
-- is short for "circle black".
record LeftAction (A X : Set) {{G : Group A}} : Set where
  field
    _●_ : A -> X -> X

    action-unit : {x : X} -> e ● x == x
    action-product : {g h : A} -> {x : X} -> (g · h) ● x == g ● (h ● x)

  infix 7 _●_

open LeftAction {{...}}

-- The following are similar to on-left and on-right, but work for ●.
dot-left : ∀ {A X} {{G : Group A}} {{act : LeftAction A X}} {g h : A} {x : X} -> g == h -> g ● x == h ● x
dot-left {g = g} {h} {x} hyp = context (λ c → c ● x) hyp

dot-right : ∀ {A X} {{G : Group A}} {{act : LeftAction A X}} {g : A} {x y : X} -> x == y -> g ● x == g ● y
dot-right {g = g} {x} {y} hyp = context (λ c → g ● c) hyp

-- ----------------------------------------------------------------------
-- * Some properties of group actions.

-- 10. Show that for any left action, g ● x == y iff g ⁻¹ ● y == x.
action-inverse : ∀ {A X : Set} -> {{G : Group A}} -> {{act : LeftAction A X}} -> ∀ (g : A) (x y : X) -> (g ● x == y <-> g ⁻¹ ● y == x)
action-inverse = {!!}

-- 11. For every group A, define the left action of A on itself by
-- conjugation. We have given the definition of the action; you need
-- to prove the laws.
instance
  self-action :  {A : Set} -> {{G : Group A}} -> LeftAction A A
  _●_ {{self-action}} g x = (g · x) · g ⁻¹
  action-unit {{self-action}} {x} = {!!}
  action-product {{self-action}} {g} {h} {x} = {!!}

-- ----------------------------------------------------------------------
-- * Orbits

-- If a group A acts on a set X, we say that x and y are in the same
-- _orbit_, written x ~ y, if there exists some g ∈ A such that
-- g ● x == y.

_~_ :  {A X : Set} -> {{G : Group A}} -> {{act : LeftAction A X}} -> X -> X -> Set
_~_ {A} {X} x y = ∃ \ (h : A) -> x == h ● y

-- Prove the next three propositions, which state that ~ is an
-- equivalence relation.

-- 12. Reflexivity.
act-refl : {A X : Set} -> {{G : Group A}} -> {{act : LeftAction A X}} -> (x : X) -> x ~ x
act-refl = {!!}

-- 13. Symmetry.
act-symm : {A X : Set} -> {{G : Group A}} -> {{act : LeftAction A X}} -> (x y : X) -> x ~ y ->  y ~ x
act-symm = {!!}
  
-- 14. Transitivity.
act-trans : {A X : Set} -> {{G : Group A}} -> {{act : LeftAction A X}} -> (x y z : X) -> x ~ y ->  y ~ z -> x ~ z
act-trans = {!!}

-- ----------------------------------------------------------------------
-- * The group structure on ℤ

module Integer where

  open Nat
  open Logic

  -- We will define the set of integers Int = {..., -2, -1, 0, 1, 2 ...}
  -- as follows:
  --
  -- * for all n : ℕ, let "pos n" denote the number n (regarded as an integer).
  --
  -- * for all n : ℕ, let "negsucc n" denote the number -1-n, i.e.,
  --   the negative of the successor of n.
  --
  -- Examples:
  --
  -- 0 = pos zero
  -- 1 = pos (succ zero)
  -- 2 = pos (succ (succ zero))
  -- -1 = negsucc zero
  -- -2 = negsucc (succ zero)

  -- For n : ℕ, the constructor pos n represents the integer n, and
  -- negsucc n represents -1-n.
  data Int : Set where
    pos : ℕ -> Int
    negsucc : ℕ -> Int
  
  -- The integer 0. We write it is "izero" to distinguish is from
  -- "zero", which is a natural number.
  izero : Int
  izero = pos 0
  
  -- The integer 1.
  ione : Int
  ione = pos 1
  
  -- The integer 2.
  itwo : Int
  itwo = pos 2
  
  -- The integer -1.
  iminusone : Int
  iminusone = negsucc 0

  -- The integer -2.
  iminustwo : Int
  iminustwo = negsucc 1
  
  -- 15. Define the successor function on the integers.
  isucc : Int -> Int
  isucc = {!!}

  -- 16. Define the predecessor function on the integers.
  ipred : Int -> Int
  ipred = {!!}
  
  -- 17. Define addition of integers.
  add : Int -> Int -> Int
  add = {!!}

  -- 18. Define negation of integers.
  negate : Int -> Int
  negate = {!!}

  module Tests where

    -- Your definitions should pass the following tests.
    test1 : isucc izero == ione
    test1 = {!refl!}

    test2 : isucc ione == itwo
    test2 = {!refl!}

    test3 : isucc iminusone == izero
    test3 = {!refl!}

    test4 : ipred izero == iminusone
    test4 = {!refl!}

    test5 : ipred ione == izero
    test5 = {!refl!}

    test6 : ipred iminusone == iminustwo
    test6 = {!refl!}

    test7 : add ione ione == itwo
    test7 = {!refl!}

    test8 : add ione iminustwo == iminusone
    test8 = {!refl!}

    test9 : add itwo iminusone == ione
    test9 = {!refl!}

    test10 : negate izero == izero
    test10 = {!refl!}

    test11 : negate ione == iminusone
    test11 = {!refl!}

    test12 : negate iminustwo == itwo
    test12 = {!refl!}

  -- The following lemmas are suggested. You do not have to prove
  -- them, but you do have to prove the theorems that follow, and
  -- these lemmas might turn out to be useful.

  lemma-isucc-ipred : ∀ x -> isucc (ipred x) == x
  lemma-isucc-ipred = {!!}

  lemma-ipred-isucc : ∀ x -> ipred (isucc x) == x
  lemma-ipred-isucc = {!!}

  lemma-isucc-add : ∀ x y -> add (isucc x) y == isucc (add x y)
  lemma-isucc-add = {!!}

  lemma-ipred-add : ∀ x y -> add (ipred x) y == ipred (add x y)
  lemma-ipred-add = {!!}

  lemma-add-ipred : ∀ x y -> add x (ipred y) == ipred (add x y)
  lemma-add-ipred = {!!}
  
  lemma-add-isucc : ∀ x y -> add x (isucc y) == isucc (add x y)
  lemma-add-isucc = {!!}

  lemma-negsucc-add : ∀ x -> add (negsucc x) (pos (succ x)) == pos zero
  lemma-negsucc-add = {!!}

  lemma-add-negsucc : ∀ x -> add (pos x) (negsucc x) == iminusone
  lemma-add-negsucc = {!!}

  -- 19. Prove associativity of addition.
  theorem-assoc : ∀ (x y z : Int) -> add (add x y) z == add x (add y z)
  theorem-assoc = {!!}

  -- 20. Prove the left inverse law of addition.
  theorem-left-inverse : ∀ x -> add (negate x) x == pos zero
  theorem-left-inverse = {!!}

  -- 21. Prove the left unit law of addition.
  theorem-left-unit : ∀ x -> add (pos zero) x == x
  theorem-left-unit = {!!}

  -- ----------------------------------------------------------------------
  -- * Finally, we can make Int into a group.

  -- 22. Make Int into a group.
  instance
    Group-Int : Group Int
    Group-Int = {!!}