{-# OPTIONS --safe #-}
module Cubical.Algebra.Group.Instances.IntMod where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Equiv

open import Cubical.Relation.Nullary

open import Cubical.Data.Empty as 
open import Cubical.Data.Unit
open import Cubical.Data.Bool hiding (isProp≤)
open import Cubical.Data.Nat renaming (_+_ to _+ℕ_)
open import Cubical.Data.Nat.Mod
open import Cubical.Data.Nat.Order
open import Cubical.Data.Int renaming (_+_ to _+ℤ_)
open import Cubical.Data.Fin
open import Cubical.Data.Fin.Arithmetic
open import Cubical.Data.Sigma

open import Cubical.Algebra.Monoid.Base
open import Cubical.Algebra.Semigroup.Base
open import Cubical.Algebra.Group.Base
open import Cubical.Algebra.Group.MorphismProperties
open import Cubical.Algebra.Group.Morphisms
open import Cubical.Algebra.Group.Properties
open import Cubical.Algebra.Group.Instances.Unit
open import Cubical.Algebra.Group.Instances.Bool
open import Cubical.Algebra.Group.Instances.Int

open GroupStr
open IsGroup
open IsMonoid


ℤGroup/_ :   Group₀
ℤGroup/ zero = ℤGroup
fst (ℤGroup/ suc n) = Fin (suc n)
1g (snd (ℤGroup/ suc n)) = 0
GroupStr._·_ (snd (ℤGroup/ suc n)) = _+ₘ_
inv (snd (ℤGroup/ suc n)) = -ₘ_
isGroup (snd (ℤGroup/ suc n)) = makeIsGroup
                                isSetFin
                                 x y z  sym (+ₘ-assoc x y z))
                                +ₘ-rUnit
                                +ₘ-lUnit
                                +ₘ-rCancel
                                +ₘ-lCancel

ℤGroup/1≅Unit : GroupIso (ℤGroup/ 1) UnitGroup₀
ℤGroup/1≅Unit = contrGroupIsoUnit isContrFin1

Bool≅ℤGroup/2 : GroupIso BoolGroup (ℤGroup/ 2)
Iso.fun (fst Bool≅ℤGroup/2) false = 1
Iso.fun (fst Bool≅ℤGroup/2) true = 0
Iso.inv (fst Bool≅ℤGroup/2) (zero , p) = true
Iso.inv (fst Bool≅ℤGroup/2) (suc zero , p) = false
Iso.inv (fst Bool≅ℤGroup/2) (suc (suc x) , p) =
  ⊥.rec (¬-<-zero (predℕ-≤-predℕ (predℕ-≤-predℕ p)))
Iso.rightInv (fst Bool≅ℤGroup/2) (zero , p) =
  Σ≡Prop  _  isProp≤) refl
Iso.rightInv (fst Bool≅ℤGroup/2) (suc zero , p) =
  Σ≡Prop  _  isProp≤) refl
Iso.rightInv (fst Bool≅ℤGroup/2) (suc (suc x) , p) =
  ⊥.rec (¬-<-zero (predℕ-≤-predℕ (predℕ-≤-predℕ p)))
Iso.leftInv (fst Bool≅ℤGroup/2) false = refl
Iso.leftInv (fst Bool≅ℤGroup/2) true = refl
snd Bool≅ℤGroup/2 =
  makeIsGroupHom λ { false false  refl
                   ; false true  refl
                   ; true false  refl
                   ; true true  refl}

ℤGroup/2≅Bool : GroupIso (ℤGroup/ 2) BoolGroup
ℤGroup/2≅Bool = invGroupIso Bool≅ℤGroup/2

-- Definition of the quotient map homomorphism ℤ → ℤGroup/ (suc n)
-- as a group homomorphism.
ℤ→Fin : (n : )    Fin (suc n)
ℤ→Fin n (pos x) = x mod (suc n) , mod< n x
ℤ→Fin n (negsuc x) = -ₘ (suc x mod suc n , mod< n (suc x))

ℤ→Fin-presinv : (n : ) (x : )  ℤ→Fin n (- x)  -ₘ ℤ→Fin n x
ℤ→Fin-presinv n (pos zero) =
  Σ≡Prop  _  isProp≤) ((λ _  zero)  sym (cong fst help))
  where
  help : (-ₘ_ {n = n} 0)  0
  help = GroupTheory.inv1g (ℤGroup/ (suc n))
ℤ→Fin-presinv n (pos (suc x)) = Σ≡Prop  _  isProp≤) refl
ℤ→Fin-presinv n (negsuc x) =
  sym (GroupTheory.invInv (ℤGroup/ (suc n)) _)


-ₘ1-id : (n : )
       Path (Fin (suc n)) (-ₘ (1 mod (suc n) , mod< n 1))
                            (n mod (suc n) , mod< n n)
-ₘ1-id zero = refl
-ₘ1-id (suc n) =
     cong -ₘ_ (FinPathℕ ((1 mod suc (suc n)) , mod< (suc n) 1) 1
                (modIndBase (suc n) 1 (n , +-comm n 2)) .snd)
    Σ≡Prop  _  isProp≤)
      ((+inductionBase (suc n) _
         x _  ((suc (suc n))  x) mod (suc (suc n))) λ _ x  x) 1
        (n , (+-comm n 2)))

suc-ₘ1 : (n y : )
   ((suc y mod suc n) , mod< n (suc y)) -ₘ (1 mod (suc n) , mod< n 1)
    (y mod suc n , mod< n y)
suc-ₘ1 zero y =
  isContr→isProp
    (isOfHLevelRetractFromIso 0 (fst ℤGroup/1≅Unit) isContrUnit) _ _
suc-ₘ1 (suc n) y =
      i  ((suc y mod suc (suc n)) , mod< (suc n) (suc y))
         +ₘ (-ₘ1-id (suc n) i))
    Σ≡Prop  _  isProp≤)
      (cong (_mod (2 +ℕ n))
         (cong (_+ℕ (suc n) mod (2 +ℕ n))
           (mod+mod≡mod (suc (suc n)) 1 y))
      ∙∙ sym (mod+mod≡mod (suc (suc n))
             ((1 mod suc (suc n))
              +ℕ (y mod suc (suc n))) (suc n))
      ∙∙ (mod-rCancel (suc (suc n)) ((1 mod suc (suc n))
                                     +ℕ (y mod suc (suc n))) (suc n)
           cong (_mod (suc (suc n)))
           (cong (_+ℕ (suc n mod suc (suc n)))
                 (+-comm (1 mod suc (suc n)) (y mod suc (suc n)))
            sym (+-assoc (y mod suc (suc n))
                  (1 mod suc (suc n)) (suc n mod suc (suc n))))
      ∙∙ mod-rCancel (suc (suc n)) (y mod suc (suc n))
            ((1 mod suc (suc n)) +ℕ (suc n mod suc (suc n)))
      ∙∙ (cong (_mod (2 +ℕ n))
            (cong ((y mod suc (suc n)) +ℕ_)
                    (sym (mod+mod≡mod (suc (suc n)) 1 (suc n))
                   zero-charac (suc (suc n)))
                   +-comm _ 0)
        mod-idempotent y)))

1-ₘsuc : (n y : )
       ((1 mod (suc n) , mod< n 1)
     +ₘ (-ₘ (((suc y mod suc n) , mod< n (suc y)))))
        -ₘ ((y mod suc n) , mod< n y)
1-ₘsuc n y =
     sym (GroupTheory.invInv (ℤGroup/ (suc n)) _)
    cong -ₘ_
      (GroupTheory.invDistr (ℤGroup/ (suc n))
        (modInd n 1 , mod< n 1) (-ₘ (modInd n (suc y) , mod< n (suc y)))
       cong (_-ₘ (modInd n 1 , mod< n 1))
       (GroupTheory.invInv (ℤGroup/ (suc n)) (modInd n (suc y) , mod< n (suc y)))
        suc-ₘ1 n y)

isHomℤ→Fin : (n : )  IsGroupHom (snd ℤGroup) (ℤ→Fin n) (snd (ℤGroup/ (suc n)))
isHomℤ→Fin n =
  makeIsGroupHom
    λ { (pos x) y  pos+case x y
      ; (negsuc x) (pos y) 
             cong (ℤ→Fin n) (+Comm (negsuc x) (pos y))
          ∙∙ pos+case y (negsuc x)
          ∙∙ +ₘ-comm (ℤ→Fin n (pos y)) (ℤ→Fin n (negsuc x))
      ; (negsuc x) (negsuc y) 
           sym (cong (ℤ→Fin n) (-Dist+ (pos (suc x)) (pos (suc y))))
        ∙∙ ℤ→Fin-presinv n (pos (suc x) +ℤ (pos (suc y)))
        ∙∙ cong -ₘ_ (pos+case (suc x) (pos (suc y)))
        ∙∙ GroupTheory.invDistr (ℤGroup/ (suc n))
             (modInd n (suc x)
            , mod< n (suc x)) (modInd n (suc y) , mod< n (suc y))
        ∙∙ +ₘ-comm (ℤ→Fin n (negsuc y)) (ℤ→Fin n (negsuc x))}
  where
  +1case :  (y : )  ℤ→Fin n (1 +ℤ y)  ℤ→Fin n 1 +ₘ ℤ→Fin n y
  +1case (pos zero) = sym (GroupStr.·IdR (snd (ℤGroup/ (suc n))) _)
  +1case (pos (suc y)) =
       cong (ℤ→Fin n) (+Comm 1 (pos (suc y)))
      Σ≡Prop  _  isProp≤) (mod+mod≡mod (suc n) 1 (suc y))
  +1case (negsuc zero) =
      Σ≡Prop  _  isProp≤) refl
     sym (GroupStr.·InvR (snd (ℤGroup/ (suc n))) (modInd n 1 , mod< n 1))
  +1case (negsuc (suc y)) =
    Σ≡Prop  _  isProp≤)
      (cong fst (cong (ℤ→Fin n) (+Comm 1 (negsuc (suc y))))
      ∙∙ cong fst (cong -ₘ_ (refl {x = suc y mod suc n , mod< n (suc y)}))
      ∙∙ cong fst (sym (1-ₘsuc n (suc y)))
        λ i  fst ((1 mod (suc n) , mod< n 1)
         +ₘ (-ₘ (((suc (suc y) mod suc n) , mod< n (suc (suc y)))))))

  pos+case : (x : ) (y : )
     ℤ→Fin n (pos x +ℤ y)  ℤ→Fin n (pos x) +ₘ ℤ→Fin n y
  pos+case zero y =
      cong (ℤ→Fin n) (+Comm 0 y)
     sym (GroupStr.·IdL (snd (ℤGroup/ (suc n))) (ℤ→Fin n y))
  pos+case (suc zero) y = +1case y
  pos+case (suc (suc x)) y =
       cong (ℤ→Fin n) (cong (_+ℤ y) (+Comm (pos (suc x)) 1)
                      sym (+Assoc 1 (pos (suc x)) y))
    ∙∙ +1case (pos (suc x) +ℤ y)
    ∙∙ (cong ((modInd n 1 , mod< n 1) +ₘ_) (pos+case (suc x) y)
     ∙∙ sym (+ₘ-assoc (modInd n 1 , mod< n 1)
              (modInd n (suc x) , mod< n (suc x)) (ℤ→Fin n y))
     ∙∙ cong (_+ₘ ℤ→Fin n y) (lem x))
    where
    lem : (x : )
       (modInd n 1 , mod< n 1) +ₘ (modInd n (suc x) , mod< n (suc x))
         ℤ→Fin n (pos (suc (suc x)))
    lem x =
      Σ≡Prop  _  isProp≤) (sym (mod+mod≡mod (suc n) 1 (suc x)))

-- ℤ/2 lemmas
ℤ/2-elim :  {} {A : Fin 2  Type }  A 0  A 1  (x : _)  A x
ℤ/2-elim {A = A} a₀ a₁ (zero , p) = subst  p  A (zero , p)) (isProp≤ (0 .snd) p) a₀
ℤ/2-elim {A = A} a₀ a₁ (suc zero , p) = subst  p  A (1 , p)) (isProp≤ (1 .snd) p) a₁
ℤ/2-elim {A = A} a₀ a₁ (suc (suc x) , p) =
  ⊥.rec (snotz (cong  x  predℕ (predℕ x)) (+-comm (3 +ℕ x) (fst p)  snd p)))

ℤ/2-rec :  {} {A : Type }  A  A  Fin 2  A
ℤ/2-rec {A = A} a₀ a₁ (zero , p) = a₀
ℤ/2-rec {A = A} a₀ a₁ (suc zero , p) = a₁
ℤ/2-rec {A = A} a₀ a₁ (suc (suc x) , p) =
  ⊥.rec (snotz (cong  x  predℕ (predℕ x)) (+-comm (3 +ℕ x) (fst p)  snd p)))

-Const-ℤ/2 : (x : fst (ℤGroup/ 2))  -ₘ x  x
-Const-ℤ/2 = ℤ/2-elim refl refl

pres0→GroupIsoℤ/2 :  {} {G : Group } (f : fst G  (ℤGroup/ 2) .fst)
   fst f (GroupStr.1g (snd G))  fzero
   IsGroupHom (snd G) (fst f) ((ℤGroup/ 2) .snd)
pres0→GroupIsoℤ/2 {G = G} f fp = isGroupHomInv ((invEquiv f) , main)
  where
  one = invEq f fone

  f⁻∙ : invEq f fzero  GroupStr.1g (snd G)
  f⁻∙ = sym (cong (invEq f) fp)  retEq f _

  f⁻1 : GroupStr._·_ (snd G) (invEq f fone) (invEq f fone)
       GroupStr.1g (snd G)
  f⁻1 = sym (retEq f (GroupStr._·_ (snd G) (invEq f fone) (invEq f fone)))
    ∙∙ cong (invEq f) (mainlem _ refl  sym fp)
    ∙∙ retEq f (GroupStr.1g (snd G))
    where
    l : ¬ (fst f (GroupStr._·_ (snd G) (invEq f fone) (invEq f fone))
                 fone)
    l p = snotz (cong fst q)
      where
      q : fone  fzero
      q = (sym (secEq f fone)
         cong (fst f)
            ((sym (GroupStr.·IdL (snd G) one)
             cong  x  GroupStr._·_ (snd G) x one) (sym (GroupStr.·InvL (snd G) one)))
             sym (GroupStr.·Assoc (snd G) (GroupStr.inv (snd G) one) one one)))
         cong (fst f) (cong (GroupStr._·_ (snd G) (GroupStr.inv (snd G) (invEq f fone)))
                ((sym (retEq f _)  cong (invEq f) p)))
         cong (fst f) (GroupStr.·InvL (snd G) _)
         fp


    mainlem : (x : _)
       fst f (GroupStr._·_ (snd G) (invEq f fone) (invEq f fone))  x
       f .fst ((snd G GroupStr.· invEq f fone) (invEq f fone))  fzero
    mainlem = ℤ/2-elim
       p  p)
      λ p  ⊥.rec (l p)


  main : IsGroupHom ((ℤGroup/ 2) .snd) (invEq f) (snd G)
  main =
    makeIsGroupHom
      (ℤ/2-elim
        (ℤ/2-elim (f⁻∙  sym (GroupStr.·IdR (snd G) (GroupStr.1g (snd G)))
                        cong  x  snd G .GroupStr._·_ x x) (sym f⁻∙))
                  (sym (GroupStr.·IdL (snd G) one)
                   cong  x  snd G .GroupStr._·_ x one) (sym f⁻∙)))
        (ℤ/2-elim (sym (GroupStr.·IdR (snd G) one)
                   cong (snd G .GroupStr._·_ (invEq f fone)) (sym f⁻∙))
                  (f⁻∙  sym f⁻1)))