module Project3-model 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 {A} {{g}} {x} =
  equational x · e
          by on-right (symm left-inverse-law)
      equals x · (x ⁻¹ · x)
          by symm associativity-law
      equals (x · x ⁻¹) · x
          by on-left right-inverse-law
      equals e · x
          by left-unit-law
      equals x

-- 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 x y h =
  equational y
          by symm left-unit-law
      equals e · y
          by on-left (symm left-inverse-law)
      equals (x ⁻¹ · x) · y 
          by associativity-law
      equals x ⁻¹ · (x · y)
          by on-right h
      equals x ⁻¹ · x
          by left-inverse-law
      equals e

-- 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 x y h =
  equational y · x
          by on-left (unique-right-unit x y h)
      equals e · x
          by left-unit-law
      equals x

-- 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 x y h =
  equational x ⁻¹
          by symm right-unit-law
      equals x ⁻¹ · e
          by on-right (symm h)
      equals x ⁻¹ · (x · y)
          by symm associativity-law
      equals (x ⁻¹ · x) · y
          by on-left left-inverse-law
      equals e · y
          by left-unit-law
      equals y

-- 5. Prove that the inverse operation is involutive.
involutive-inverse : {A : Set} ->  {{G : Group A}} -> (x : A) -> (x ⁻¹) ⁻¹ == x
involutive-inverse x =
  equational (x ⁻¹) ⁻¹
          by symm right-unit-law
      equals (x ⁻¹) ⁻¹ · e
          by on-right (symm left-inverse-law)
      equals (x ⁻¹) ⁻¹ · (x ⁻¹ · x)
          by symm associativity-law
      equals ((x ⁻¹) ⁻¹ · x ⁻¹) · x
          by on-left left-inverse-law
      equals e · x
          by left-unit-law
      equals x

-- 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 x y h =
  equational y ⁻¹
          by symm (context _⁻¹ (right-inverse x y h))
      equals ((x ⁻¹) ⁻¹)
          by involutive-inverse x 
      equals x

-- 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 x y = left-inverse (y ⁻¹ · x ⁻¹) (x · y) claim
  where
    claim : (y ⁻¹ · x ⁻¹) · (x · y) == e
    claim = 
      equational (y ⁻¹ · x ⁻¹) · (x · y)
              by associativity-law
          equals y ⁻¹ · (x ⁻¹ · (x · y))
              by on-right (symm associativity-law)
          equals y ⁻¹ · ((x ⁻¹ · x) · y)
              by on-right (on-left left-inverse-law)
          equals y ⁻¹ · (e · y)
              by on-right left-unit-law
          equals y ⁻¹ · y
              by left-inverse-law
          equals e
    
-- ----------------------------------------------------------------------
-- * 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 {A} {B} {{G}} {{G'}} f {{r}} =
  equational f e
          by symm left-unit-law
      equals e · f e
          by on-left (symm left-inverse-law)
      equals ((f e) ⁻¹ · f e) · f e
          by associativity-law
      equals (f e) ⁻¹ · (f e · f e)
          by on-right (symm claim)
      equals (f e) ⁻¹ · f e
          by left-inverse-law 
      equals e
  where
    claim : f e == f e · f e
    claim =
      equational f e
              by context f (symm left-unit-law)
          equals f (e · e)
              by groupHom e e
          equals f e · f e

-- 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 f a = symm (right-inverse (f a) (f (a ⁻¹)) claim)
  where
    claim : f a · f (a ⁻¹) == e
    claim =
      equational f a · f (a ⁻¹)
              by symm (groupHom a (a ⁻¹))
          equals f (a · a ⁻¹)
              by context f right-inverse-law
          equals f e
              by preserveUnit f
          equals e

-- ----------------------------------------------------------------------
-- * 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 g x y = (left-to-right , right-to-left)
  where
    left-to-right : g ● x == y -> g ⁻¹ ● y == x
    left-to-right hyp =
      equational g ⁻¹ ● y
              by dot-right (symm hyp)
          equals g ⁻¹ ● (g ● x)
              by symm action-product
          equals (g ⁻¹ · g) ● x
              by dot-left left-inverse-law
          equals e ● x
              by action-unit
          equals x

    right-to-left : g ⁻¹ ● y == x -> g ● x == y
    right-to-left hyp =
      equational g ● x
              by dot-right (symm hyp)
          equals g ● (g ⁻¹ ● y)
              by symm action-product
          equals (g · g ⁻¹) ● y
              by dot-left right-inverse-law
          equals e ● y
              by action-unit
          equals y

-- 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} =
    equational (e · x) · e ⁻¹
            by on-left left-unit-law
        equals x · e ⁻¹
            by on-right (left-inverse e e left-unit-law)
        equals x · e
            by right-unit-law
        equals x
  action-product {{self-action}} {g} {h} {x} =
    equational ((g · h) · x) · (g · h) ⁻¹
            by on-right (inverse-of-product g h)
        equals ((g · h) · x) · (h ⁻¹ · g ⁻¹)
            by symm associativity-law
        equals (((g · h) · x) · h ⁻¹) · g ⁻¹
            by on-left associativity-law
        equals ((g · h) · (x · h ⁻¹)) · g ⁻¹
            by on-left associativity-law
        equals (g · (h · (x · h ⁻¹))) · g ⁻¹
            by on-left (on-right (symm associativity-law))
        equals (g · ((h · x) · h ⁻¹)) · g ⁻¹

-- ----------------------------------------------------------------------
-- * 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 x = (e , symm action-unit)

-- 13. Symmetry.
act-symm : {A X : Set} -> {{G : Group A}} -> {{act : LeftAction A X}} -> (x y : X) -> x ~ y ->  y ~ x
act-symm x y (k , p) = (k ⁻¹ , claim)
 where
   claim : y == k ⁻¹ ● x
   claim = equational y
                   by symm action-unit
               equals (e ● y)
                   by dot-left (symm left-inverse-law)
               equals (k ⁻¹ · k) ● y
                   by action-product
               equals k ⁻¹ ● (k ● y)
                   by dot-right (symm p)
               equals (k ⁻¹ ● x)
  
-- 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 x y z (k1 , p1) (k2 , p2) = (k1 · k2 , claim)
  where
    claim : x == (k1 · k2) ● z
    claim = equational x
                    by p1
                equals k1 ● y
                    by dot-right p2
                equals k1 ● (k2 ● z)
                    by symm action-product
                equals (k1 · k2) ● z

-- ----------------------------------------------------------------------
-- * 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 (pos x) = pos (succ x)
  isucc (negsucc zero) = pos zero
  isucc (negsucc (succ x)) = negsucc x

  -- 16. Define the predecessor function on the integers.
  ipred : Int -> Int
  ipred (pos zero) = iminusone
  ipred (pos (succ x)) = pos x
  ipred (negsucc x) = negsucc (succ x)
  
  -- 17. Define addition of integers.
  add : Int -> Int -> Int
  add (pos zero) y = y
  add (pos (succ x)) y = isucc (add (pos x) y)
  add (negsucc zero) y = ipred y
  add (negsucc (succ x)) y = ipred (add (negsucc x) y)

  -- 18. Define negation of integers.
  negate : Int -> Int
  negate (pos zero) = pos zero
  negate (pos (succ x)) = negsucc x
  negate (negsucc x) = pos (succ x)

  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 (pos zero) = refl
  lemma-isucc-ipred (pos (succ x)) = refl
  lemma-isucc-ipred (negsucc x) = refl

  lemma-ipred-isucc : ∀ x -> ipred (isucc x) == x
  lemma-ipred-isucc (pos x) = refl
  lemma-ipred-isucc (negsucc zero) = refl
  lemma-ipred-isucc (negsucc (succ x)) = refl

  lemma-isucc-add : ∀ x y -> add (isucc x) y == isucc (add x y)
  lemma-isucc-add (pos x) y = refl
  lemma-isucc-add (negsucc zero) y = symm (lemma-isucc-ipred y)
  lemma-isucc-add (negsucc (succ x)) y = symm (lemma-isucc-ipred (add (negsucc x) y))

  lemma-ipred-add : ∀ x y -> add (ipred x) y == ipred (add x y)
  lemma-ipred-add (pos zero) y = refl
  lemma-ipred-add (pos (succ x)) y = symm (lemma-ipred-isucc (add (pos x) y))
  lemma-ipred-add (negsucc x) y = refl

  lemma-add-ipred : ∀ x y -> add x (ipred y) == ipred (add x y)
  lemma-add-ipred (pos zero) y = refl
  lemma-add-ipred (pos (succ x)) y =
    equational isucc (add (pos x) (ipred y))
            by context isucc (lemma-add-ipred (pos x) y)
        equals isucc (ipred (add (pos x) y))
            by lemma-isucc-ipred (add (pos x) y)
        equals add (pos x) y
            by symm (lemma-ipred-isucc (add (pos x) y))
        equals ipred (isucc (add (pos x) y))
  lemma-add-ipred (negsucc zero) y = refl
  lemma-add-ipred (negsucc (succ x)) y = context ipred (lemma-add-ipred (negsucc x) y)

  lemma-add-isucc : ∀ x y -> add x (isucc y) == isucc (add x y)
  lemma-add-isucc (pos zero) y = refl
  lemma-add-isucc (pos (succ x)) y = context isucc (lemma-add-isucc (pos x) y)
  lemma-add-isucc (negsucc zero) y = trans (lemma-ipred-isucc y) (symm (lemma-isucc-ipred y))
  lemma-add-isucc (negsucc (succ x)) y =
    equational ipred (add (negsucc x) (isucc y))
            by context ipred (lemma-add-isucc (negsucc x) y)
        equals ipred (isucc (add (negsucc x) y))
            by trans (lemma-ipred-isucc (add (negsucc x) y)) (symm (lemma-isucc-ipred (add (negsucc x) y)))
        equals isucc (ipred (add (negsucc x) y))

  lemma-negsucc-add : ∀ x -> add (negsucc x) (pos (succ x)) == pos zero
  lemma-negsucc-add zero = refl
  lemma-negsucc-add (succ x) =
    equational ipred (add (negsucc x) (pos (succ (succ x))))
            by definition
        equals ipred (add (negsucc x) (isucc (pos (succ x))))
            by context ipred (lemma-add-isucc (negsucc x) (pos (succ x)))
        equals ipred (isucc (add (negsucc x) (pos (succ x))))
            by lemma-ipred-isucc (add (negsucc x) (pos (succ x)))
        equals add (negsucc x) (pos (succ x))
            by lemma-negsucc-add x
        equals pos zero

  lemma-add-negsucc : ∀ x -> add (pos x) (negsucc x) == iminusone
  lemma-add-negsucc zero = refl
  lemma-add-negsucc (succ x) =
    equational isucc (add (pos x) (negsucc (succ x)))
            by definition
        equals isucc (add (pos x) (ipred (negsucc x)))
            by context isucc (lemma-add-ipred (pos x) (negsucc x))
        equals isucc (ipred (add (pos x) (negsucc x)))
            by lemma-isucc-ipred (add (pos x) (negsucc x))
        equals add (pos x) (negsucc x)
            by lemma-add-negsucc x
        equals iminusone

  -- 19. Prove associativity of addition.
  theorem-assoc : ∀ (x y z : Int) -> add (add x y) z == add x (add y z)
  theorem-assoc (pos zero) y z = refl
  theorem-assoc (pos (succ x)) y z =
    equational add (isucc (add (pos x) y)) z
            by lemma-isucc-add (add (pos x) y) z
        equals isucc (add (add (pos x) y) z)
            by context isucc (theorem-assoc (pos x) y z)
        equals isucc (add (pos x) (add y z))
  theorem-assoc (negsucc zero) y z = lemma-ipred-add y z
  theorem-assoc (negsucc (succ x)) y z =
    equational add (ipred (add (negsucc x) y)) z
            by lemma-ipred-add (add (negsucc x) y) z
        equals ipred (add (add (negsucc x) y) z)
            by context ipred (theorem-assoc (negsucc x) y z)
        equals ipred (add (negsucc x) (add y z))

  -- 20. Prove the left inverse law of addition.
  theorem-left-inverse : ∀ x -> add (negate x) x == pos zero
  theorem-left-inverse (pos zero) = refl
  theorem-left-inverse (pos (succ x)) = lemma-negsucc-add x
  theorem-left-inverse (negsucc x) =
    equational isucc (add (pos x) (negsucc x))
            by context isucc (lemma-add-negsucc x)
        equals isucc iminusone
            by definition
        equals pos zero

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

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

  -- 22. Make Int into a group.
  instance
    Group-Int : Group Int
    _·_ {{Group-Int}} = add
    e {{Group-Int}} = izero
    _⁻¹ {{Group-Int}} = negate
    associativity-law {{Group-Int}} {x} {y} {z} = theorem-assoc x y z
    left-unit-law {{Group-Int}} {x} = theorem-left-unit x
    left-inverse-law {{Group-Int}} {x} = theorem-left-inverse x