module Data.Mod where

open import Data.Nat renaming (_+_ to _ℕ+_)
open import Data.Nat.Properties
open import Data.Integer hiding (_*_; _≤_) renaming (suc to ℤsuc; pred to ℤpred)
open import Data.Integer.Properties
open import Data.Nat.Divisibility
open import Quotient -- http://www.cs.nott.ac.uk/~txa/AIMXV/Quotient.html/Quotient.html
open import Function using (_∘_)

open import Relation.Binary
open import Relation.Binary.PropositionalEquality hiding ([_])
open ≡-Reasoning

open import Algebra
import Data.Nat.Properties as Nat
private
  module ℕ-CS = CommutativeSemiring Nat.commutativeSemiring
import Data.Integer.Properties as Integer
private
  module ℤ-CR = CommutativeRing Integer.commutativeRing
private
  module ℕ-Ord = StrictTotalOrder Nat.strictTotalOrder
import Algebra.RingSolver.AlmostCommutativeRing as ACR
private
  module ℤ-ACR = ACR.AlmostCommutativeRing (ACR.fromCommutativeRing Integer.commutativeRing)
open import Data.Product

private
  open import Relation.Binary.PropositionalEquality as PropEq
    using (_≡_; refl; sym; cong; cong₂)
  open PropEq.≡-Reasoning

  neg-minus-pos : (x y : )  -[1+ x ] - (+ y)  -[1+ (y ℕ+ x) ]
  neg-minus-pos x zero = refl
  neg-minus-pos zero (suc y) = cong (-[1+_]  suc) (sym (proj₂ ℕ-CS.+-identity y))
  neg-minus-pos (suc x) (suc y) = cong (-[1+_]  suc) (ℕ-CS.+-comm (suc x) y)

  flip-suc :  x y  x ℕ+ suc y  suc x ℕ+ y
  flip-suc zero y = refl
  flip-suc (suc x) y = cong suc (flip-suc x y)

  flip-⊖ : (x y : )  x  y  - (y  x)
  flip-⊖ zero     zero    = refl
  flip-⊖ zero     (suc y) = refl
  flip-⊖ (suc x)  zero    = refl
  flip-⊖ (suc x)  (suc y) = flip-⊖ x y

  telescope : (x y z : )  (x - y) + (y - z)  x - z
  telescope x y z =
    begin
      (x - y) + (y - z)
    ≡⟨ ℤ-CR.+-assoc x (- y) (y - z) 
      x + ((- y) + (y - z))
    ≡⟨ cong (_+_ x) (sym (ℤ-CR.+-assoc (- y) y (- z))) 
      x + ((- y + y) - z)
    ≡⟨ sym (ℤ-CR.+-assoc x (- y + y) (- z)) 
      x + (- y + y) - z
    ≡⟨ cong  a  x + a - z) (proj₁ ℤ-CR.-‿inverse y) 
      x + (+ 0) - z
    ≡⟨ cong  a  a - z) (proj₂ ℤ-CR.+-identity x) 
      x - z
    

  abs-⊖-comm : (x y : )   x  y    y  x 
  abs-⊖-comm zero zero = refl
  abs-⊖-comm zero (suc _) = refl
  abs-⊖-comm (suc _) zero = refl
  abs-⊖-comm (suc x) (suc y) = abs-⊖-comm x y

  ∸-*-distrib : {n : }  (p q : )  p * n  q * n  (p  q) * n
  ∸-*-distrib zero zero = refl
  ∸-*-distrib {n} zero (suc q) = 0∸n≡0 (n ℕ+ q * n)
  ∸-*-distrib (suc p) zero = refl
  ∸-*-distrib {n} (suc p) (suc q) =
    begin
      (n ℕ+ p * n)  (n ℕ+ q * n)
    ≡⟨ [i+j]∸[i+k]≡j∸k n (p * n) (q * n) 
      p * n  q * n
    ≡⟨ ∸-*-distrib p q 
      (p  q) * n
    

  abs-flip : (x y : )   x - y    y - x 
  abs-flip -[1+ x ] -[1+ y ] = abs-⊖-comm y x
  abs-flip -[1+ x ] (+ y) =
    begin
       -[1+ x ] - (+ y) 
    ≡⟨ cong ∣_∣ (neg-minus-pos x y) 
      suc (y ℕ+ x)
    ≡⟨ cong suc (ℕ-CS.+-comm y x)
      suc (x ℕ+ y)
    ≡⟨ ℕ-CS.+-comm (suc x) y 
      y ℕ+ suc x
    
  abs-flip (+ x) -[1+ y ] =
    begin
      x ℕ+ suc y
    ≡⟨ ℕ-CS.+-comm x (suc y) 
      suc (y ℕ+ x)
    ≡⟨ cong suc (ℕ-CS.+-comm y x) 
      suc (x ℕ+ y)
    ≡⟨ cong ∣_∣ (sym (neg-minus-pos y x)) 
       -[1+ y ] + - (+ x) 
    
  abs-flip (+ x) (+ y) =
    begin
       (+ x) - (+ y) 
    ≡⟨ cong ∣_∣ (lem x y) 
       x  y 
    ≡⟨ abs-⊖-comm x y 
       y  x 
    ≡⟨ cong ∣_∣ (sym (lem y x)) 
       (+ y) - (+ x) 
    
    where
    lem : (x y : )  (+ x) - (+ y)  x  y
    lem zero zero = refl
    lem zero (suc y) = refl
    lem (suc x) zero = cong (+_  suc) (proj₂ ℕ-CS.+-identity x)
    lem (suc x) (suc y) = refl

  diff-x<y :  {x y} (x<y : x < y)  y  suc x  + (y  suc x)
  diff-x<y (s≤s z≤n) = refl
  diff-x<y (s≤s (s≤s y≤n)) = diff-x<y (s≤s y≤n)

  diff-x≥y :  {x y} (x≥y : x  y)  y  suc x  -[1+ (x  y) ]
  diff-x≥y z≤n = refl
  diff-x≥y (s≤s m≤n) = diff-x≥y m≤n

  >-weaken :  {n m}  n > m  n  m
  >-weaken (s≤s z≤n) = z≤n
  >-weaken (s≤s (s≤s m≤n)) = s≤s (>-weaken (s≤s m≤n))

  ≡-weaken :  {n m}  n  m  n  m
  ≡-weaken {zero} refl = z≤n
  ≡-weaken {suc n} refl = s≤s (≡-weaken refl)

  suc-∸ :  {x y} (y≤x : y  x)  suc (x  y)  suc x  y
  suc-∸ {x} {zero} z≤n = refl
  suc-∸ {suc x} {suc y} (s≤s y≤x) = suc-∸ y≤x
  suc-∸ {zero} {suc y} ()

  div-diff :  {n : }  {x y : }  n  suc x  n  y  n   y  suc x 
  div-diff {n} {x} {y} (divides q eq) (divides r eq′) = dispatch
    where
    lem-x<y : (x<y : x < y)  n   y  suc x 
    lem-x<y x<y = divides (r  q) eq″
      where
      eq″ :  y  suc x   (r  q) * n
      eq″ =
        begin
           y  suc x 
        ≡⟨ cong ∣_∣ (diff-x<y x<y) 
          y  suc x
        ≡⟨ cong₂ _∸_ eq′ eq 
          r * n  q * n
        ≡⟨ ∸-*-distrib r q 
          (r  q) * n
        

    lem-x≥y : (x≥y : x  y)  n   y  suc x 
    lem-x≥y x≥y = divides (q  r) eq″
      where
      eq″ :  y  suc x   (q  r) * n
      eq″ =
        begin
           y  suc x 
        ≡⟨ cong ∣_∣ (diff-x≥y x≥y) 
          suc (x  y)
        ≡⟨ suc-∸ x≥y 
          suc x  y
        ≡⟨ cong₂ _∸_ eq eq′ 
          q * n  r * n
        ≡⟨ ∸-*-distrib q r 
          (q  r) * n
        

    dispatch : n   y  suc x 
    dispatch with ℕ-Ord.compare x y
    dispatch | tri< x<y  _    _    = lem-x<y x<y
    dispatch | tri≈ _    x≡y  _    = lem-x≥y (≡-weaken x≡y)
    dispatch | tri> _    _    x>y  = lem-x≥y (>-weaken x>y)


  ∣-abs-+ :  {n : }  (x y : )  n   x   n   y   n   x + y 
  ∣-abs-+ {n} (+ x) (+ y) (divides q eq) (divides r eq′) = divides (q ℕ+ r) lem
    where
    lem : x ℕ+ y  (q ℕ+ r) * n
    lem =
      begin
        x ℕ+ y
      ≡⟨ cong₂ _ℕ+_ eq eq′ 
        q * n ℕ+ r * n
      ≡⟨ sym (proj₂ ℕ-CS.distrib n q r) 
        (q ℕ+ r) * n
      
  ∣-abs-+ {n} -[1+ x ] -[1+ y ] (divides q eq) (divides r eq′) = divides (q ℕ+ r) lem
    where
    lem : suc (suc (x ℕ+ y))  (q ℕ+ r) * n
    lem =
      begin
        suc ((suc x) ℕ+ y)
      ≡⟨ cong suc (ℕ-CS.+-comm (suc x) y) 
        suc y ℕ+ suc x
      ≡⟨ ℕ-CS.+-comm (suc y) (suc x) 
        suc x ℕ+ suc y
      ≡⟨ cong₂ _ℕ+_ eq eq′ 
        q * n ℕ+ r * n
      ≡⟨ sym (proj₂ ℕ-CS.distrib n q r) 
        (q ℕ+ r) * n
      
  ∣-abs-+ {n} -[1+ x ] (+ y) d d′ = div-diff d d′
  ∣-abs-+ {n} (+ x) -[1+ y ] d d′ = div-diff d′ d



Mod₀ :   Setoid _ _
Mod₀ n = record
  { Carrier = 
  ; _≈_ = _∼_
  ; isEquivalence = record
    { refl = λ {x}  reflexive {x}
    ; sym = λ {x} {y}  symmetric {x} {y}
    ; trans = λ {x} {y} {z}  transitive {x} {y} {z}
    }
  }

  where
    _∼_ : Rel  _
    x  y = n   x - y 

    reflexive : Reflexive _∼_
    reflexive {x} = divides zero (cong ∣_∣ (proj₂ ℤ-CR.-‿inverse x))

    symmetric : Symmetric _∼_
    symmetric {x} {y} (divides q eq) = divides q (trans (abs-flip y x) eq)

    transitive : Transitive _∼_
    transitive {x} {y} {z} d d′ = subst (_∣_ n) (cong ∣_∣ (telescope x y z)) (∣-abs-+ (x - y) (y - z) d d′)

Mod :   Set
Mod n = Quotient (Mod₀ n)



open import Quotient.Product

plus :  {n}  Mod n  Mod n  Mod n
plus {n} = lift₂ _+_  {x} {y} {t} {u}  proof {x} {y} {t} {u})
  where
  proof :  {x y t u}  (n   x - y )  (n   t - u )  n   (x + t) - (y + u) 
  proof {x} {y} {t} {u} x∼y t∼u = subst ((_∣_ n)  ∣_∣) (sym (eq x y t u)) (∣-abs-+ (x - y) (t - u) x∼y t∼u)
    where
    eq :  a b c d  (a + c) - (b + d)  (a - b) + (c - d)
    eq a b c d =
      begin
        (a + c) - (b + d)
      ≡⟨ cong (_-_ (a + c)) (ℤ-CR.+-comm b d) 
        (a + c) - (d + b)
      ≡⟨ ℤ-CR.+-assoc a c (- (d + b)) 
        a + (c - (d + b))
      ≡⟨ cong (_+_ a  _+_ c) (sym (ℤ-ACR.-‿+-comm d b)) 
        a + (c + (- d + - b))
      ≡⟨ cong (_+_ a) (sym (ℤ-CR.+-assoc c (- d) (- b))) 
        a + ((c - d) - b)
      ≡⟨ sym (ℤ-CR.+-assoc a (c - d) (- b)) 
        (a + (c - d)) - b
      ≡⟨ cong  x  x - b) (ℤ-CR.+-comm a (c - d)) 
        ((c - d) + a) - b
      ≡⟨ ℤ-CR.+-assoc (c - d) a (- b) 
        (c - d) + (a - b)
      ≡⟨ ℤ-CR.+-comm (c - d) (a - b) 
        (a - b) + (c - d)
      



_+1 :  {n}  Mod n  Mod n
_+1 = plus [ + 1 ]

_-1 :  {n}  Mod n  Mod n
_-1 = plus [ - (+ 1) ]

+1-1 :  {n}  (x : Mod n)  x +1 -1  x
+1-1 {n} = elim _  x  [ proof x ]-cong)  x∼y  proof-irrelevance _ _)
  where
  pred-suc :  x  ℤpred (ℤsuc x)  x
  pred-suc -[1+ zero ] = refl
  pred-suc -[1+ suc _ ] = refl
  pred-suc (+ _) = refl

  proof :  x  n   ℤpred (ℤsuc x) - x 
  proof x = divides 0 (cong ∣_∣ (lem x))
    where
    lem :  x  ℤpred (ℤsuc x) - x  + 0
    lem x = trans (cong  a  a - x) (pred-suc x)) (proj₂ ℤ-CR.-‿inverse x)