{-# OPTIONS --cubical --safe #-}
module Cubical.Data.Nat.Mod where

open import Cubical.Foundations.Prelude
open import Cubical.Data.Nat
open import Cubical.Data.Nat.Order
open import Cubical.Data.Empty

-- Defining x mod 0 to be 0. This way all the theorems below are true
-- for n : ℕ instead of n : ℕ₊₁.

------ Preliminary definitions ------
modInd : (n : )    
modInd n = +induction n  _  )  x _  x) λ _ x  x

modIndBase : (n m : )  m < suc n  modInd n m  m
modIndBase n = +inductionBase n  _  )  x _  x)  _ x  x)

modIndStep : (n m : )  modInd n (suc n + m)  modInd n m
modIndStep n = +inductionStep n  _  )  x _  x)  _ x  x)
-------------------------------------

_mod_ : (x n : )  
x mod zero = 0
x mod (suc n) = modInd n x

mod< : (n x : )  x mod (suc n) < (suc n)
mod< n =
  +induction n
     x  x mod (suc n) < suc n)
     x base  fst base
               , (cong  x  fst base + suc x)
                       (modIndBase n x base)
                 snd base))
     λ x ind  fst ind
              , cong  x  fst ind + suc x)
                     (modIndStep n x)  snd ind

mod-rUnit : (n x : )  x mod n  ((x + n) mod n)
mod-rUnit zero x = refl
mod-rUnit (suc n) x =
    sym (modIndStep n x)
   cong (modInd n) (+-comm (suc n) x)

mod-lUnit : (n x : )  x mod n  ((n + x) mod n)
mod-lUnit zero _ = refl
mod-lUnit (suc n) x = sym (modIndStep n x)

mod+mod≡mod : (n x y : )
   (x + y) mod n  (((x mod n) + (y mod n)) mod n)
mod+mod≡mod zero _ _ = refl
mod+mod≡mod (suc n) =
  +induction n
     z  (x : )
          ((z + x) mod (suc n))
          (((z mod (suc n)) + (x mod (suc n))) mod (suc n)))
     x p 
      +induction n _
         y q  cong (modInd n)
                       (sym (cong₂  _+_ (modIndBase n x p)
                       (modIndBase n y q))))
        λ y ind  cong (modInd n)
                        (cong (x +_) (+-comm (suc n) y)
                                    (+-assoc x y (suc n)))
                     ∙∙ sym (mod-rUnit (suc n) (x + y))
                     ∙∙ ind
                       cong  z  modInd n
                                    ((modInd n x + z)))
                             (mod-rUnit (suc n) y
                              cong (modInd n) (+-comm y (suc n))))
    λ x p y 
      cong (modInd n) (cong suc (sym (+-assoc n x y)))
        ∙∙ sym (mod-lUnit (suc n) (x + y))
        ∙∙ p y
          sym (cong (modInd n)
                (cong (_+ modInd n y)
                 (cong (modInd n)
                  (+-comm (suc n) x)  sym (mod-rUnit (suc n) x))))

mod-idempotent : {n : } (x : )  (x mod n) mod n  x mod n
mod-idempotent {n = zero} _ = refl
mod-idempotent {n = suc n} =
  +induction n  x  (x mod suc n) mod (suc n)  x mod (suc n))
              x p  cong (_mod (suc n))
                            (modIndBase n x p))
              λ x p  cong (_mod (suc n))
                            (modIndStep n x)
                          ∙∙ p
                          ∙∙ mod-rUnit (suc n) x
                            (cong (_mod (suc n)) (+-comm x (suc n)))

zero-charac : (n : )  n mod n  0
zero-charac zero = refl
zero-charac (suc n) = cong (_mod suc n) (+-comm 0 (suc n))
                  ∙∙ modIndStep n 0
                  ∙∙ modIndBase n 0 (n , (+-comm n 1))

zero-charac-gen : (n x : )  ((x · n) mod n)  0
zero-charac-gen zero x = refl
zero-charac-gen (suc n) zero = refl
zero-charac-gen (suc n) (suc x) =
  modIndStep n (x · (suc n))  zero-charac-gen (suc n) x

mod·mod≡mod : (n x y : )
   (x · y) mod n  (((x mod n) · (y mod n)) mod n)
mod·mod≡mod zero _ _ = refl
mod·mod≡mod (suc n) =
  +induction n _
     x p  +induction n _
       y q
         cong (modInd n)
            (cong₂ _·_ (sym (modIndBase n x p)) (sym (modIndBase n y q))))
      λ y p 
           cong (modInd n) (sym (·-distribˡ  x (suc n) y))
        ∙∙ mod+mod≡mod (suc n) (x · suc n) (x · y)
        ∙∙ cong  z  modInd n (z + modInd n (x · y)))
                (zero-charac-gen (suc n) x)
        ∙∙ mod-idempotent (x · y)
        ∙∙ p
          cong (_mod (suc n)) (cong (x mod (suc n) ·_)
                (sym (mod-idempotent y)
                ∙∙  i  modInd n (mod-rUnit (suc n) 0 i + modInd n y))
                ∙∙ sym (mod+mod≡mod (suc n) (suc n) y))))
    λ x p y 
         (sym (cong (_mod (suc n)) (·-distribʳ (suc n) x y))
       ∙∙ mod+mod≡mod (suc n) (suc n · y) (x · y)
       ∙∙  i  modInd n ((cong (_mod (suc n))
             (·-comm (suc n) y)  zero-charac-gen (suc n) y) i
             + modInd n (x · y)))
         mod-idempotent (x · y))
      ∙∙ p y
      ∙∙ cong (_mod (suc n)) (cong ( y mod (suc n))
              ((sym (mod-idempotent x)
               cong  z  (z + x mod (suc n)) mod (suc n))
                     (mod-rUnit (suc n) 0))
               sym (mod+mod≡mod (suc n) (suc n) x)))

mod-rCancel : (n x y : )  (x + y) mod n  (x + y mod n) mod n
mod-rCancel zero x y = refl
mod-rCancel (suc n) x =
  +induction n _
     y p  cong  z  (x + z) mod (suc n))
                   (sym (modIndBase n y p)))
     λ y p  cong (_mod suc n) (+-assoc x (suc n) y
                             ∙∙ (cong (_+ y) (+-comm x (suc n)))
                             ∙∙ sym (+-assoc (suc n) x y))
          ∙∙ sym (mod-lUnit (suc n) (x + y))
          ∙∙ (p  cong  z  (x + z) mod suc n) (mod-lUnit (suc n) y))

mod-lCancel : (n x y : )  (x + y) mod n  (x mod n + y) mod n
mod-lCancel n x y =
     cong (_mod n) (+-comm x y)
  ∙∙ mod-rCancel n y x
  ∙∙ cong (_mod n) (+-comm y (x mod n))

-- remainder and quotient after division by n
-- Again, allowing for 0-division to get nicer syntax
remainder_/_ : (x n : )  
remainder x / zero = x
remainder x / suc n = x mod (suc n)

quotient_/_ : (x n : )  
quotient x / zero = 0
quotient x / suc n =
  +induction n  _  )  _ _  0)  _  suc) x

≡remainder+quotient : (n x : )
   (remainder x / n) + n · (quotient x / n)  x
≡remainder+quotient zero x = +-comm x 0
≡remainder+quotient (suc n) =
  +induction n
     x  (remainder x / (suc n)) + (suc n)
          · (quotient x / (suc n))  x)
     x base  cong₂ _+_ (modIndBase n x base)
                           (cong ((suc n) ·_)
                           (+inductionBase n _ _ _ x base))
              ∙∙ cong (x +_) (·-comm n 0)
              ∙∙ +-comm x 0)
     λ x ind  cong₂ _+_ (modIndStep n x)
                        (cong ((suc n) ·_) (+inductionStep n _ _ _ x))
          ∙∙ cong (modInd n x +_)
                  (·-suc (suc n) (+induction n _ _ _ x))
          ∙∙ cong (modInd n x +_)
                  (+-comm (suc n) ((suc n) · (+induction n _ _ _ x)))
          ∙∙ +-assoc (modInd n x) ((suc n) · +induction n _ _ _ x) (suc n)
          ∙∙ cong (_+ suc n) ind
            +-comm x (suc n)

private
  test₀ : 100 mod 81  19
  test₀ = refl

  test₁ : ((11 + (10 mod 3)) mod 3)  0
  test₁ = refl