Modular arithmetics

ModArith.agda

-- adapted from https://gist.github.com/oisdk/037862acb385f30257a1c594fd5a616e

module ModArith where

open import Prelude

open import Data.Empty
open import Data.Nat
open import Data.Bool
open import Data.Reflects as Reflects
open import Data.Dec

module GTE where
  infix 4 _≥_
  data _≥_ (m : ℕ) : ℕ → 𝒰 where
    m≥m : m ≥ m
    m≥p : ∀ {n} → m ≥ suc n → m ≥ n

  s≥s : ∀ {n m} → n ≥ m → suc n ≥ suc m
  s≥s m≥m = m≥m
  s≥s (m≥p n≥m) = m≥p (s≥s n≥m)

  p≥p : ∀ {n m} → suc n ≥ suc m → n ≥ m
  p≥p m≥m = m≥m
  p≥p (m≥p n≥m) = m≥p (p≥p n≥m)

  ≥-trans : ∀ {n m l} → n ≥ m → m ≥ l → n ≥ l
  ≥-trans     m≥m     ml      = ml
  ≥-trans nm@(m≥p _)  m≥m     = nm
  ≥-trans nm@(m≥p _) (m≥p ml) = m≥p (≥-trans nm ml)

  =→≥ : ∀ {n m} → n ＝ m → n ≥ m
  =→≥ {n} {m} e = subst (n ≥_) e m≥m

  z≯n : ∀ {n} → zero ≥ suc n → ⊥
  z≯n (m≥p z≥sn) = z≯n z≥sn

  n≥z : ∀ {n} → n ≥ zero
  n≥z = go _ m≥m
    where
    go : ∀ {n} m → n ≥ m → n ≥ zero
    go zero n≥m = n≥m
    go (suc m) n≥m = go m (m≥p n≥m)

  _≥?_ : ℕ → ℕ → Bool
  zero  ≥? zero  = true
  zero  ≥? suc m = false
  suc n ≥? zero  = true
  suc n ≥? suc m = n ≥? m

  instance
    reflects-≥? : ∀ {n m} → Reflects (n ≥ m) (n ≥? m)
    reflects-≥? {n = zero}  {m = zero}  = ofʸ m≥m
    reflects-≥? {n = zero}  {m = suc m} = ofⁿ z≯n
    reflects-≥? {n = suc n} {m = zero}  = ofʸ n≥z
    reflects-≥? {n = suc n} {m = suc m} = Reflects.dmap s≥s (contra p≥p) (reflects-≥? {n = n} {m = m})

    dec-≥? : ∀ {n m} → Dec (n ≥ m)
    dec-≥? {n} {m} .does  = n ≥? m
    dec-≥? {n} {m} .proof = reflects-≥? {n = n} {m = m}

open GTE using (_≥_; m≥m; m≥p; ≥-trans; =→≥; _≥?_)

Mod : ℕ → 𝒰
Mod n = Σ[ m ꞉ ℕ ] (n ≥ m)

infixl 6 _+m_
_+m_ : ∀ {n} → Mod n → Mod n → Mod n
_+m_ (m , x) = go x
  where
  go : ∀ {n m} → n ≥ m → Mod n → Mod n
  go  m≥m     y          = y
  go (m≥p x) (zero , y)  = suc _ , x
  go (m≥p x) (suc s , y) = go x (s , m≥p y)

space : ∀ {n m} → n ≥ m → ℕ
space  m≥m      = zero
space (m≥p n≥m) = suc (space n≥m)

to-ℕ : ∀ {n} → Mod n → ℕ
to-ℕ = space ∘ snd

from-ℕ-= : ∀ {n} m
          → (@0 n≥m : n ≥ m)
          → Σ[ n-m ꞉ Mod n ] (m ＝ to-ℕ n-m)
from-ℕ-=  zero   n≥m = (_ , m≥m) , refl
from-ℕ-= (suc n) n≥m with from-ℕ-= n (m≥p n≥m)
... | (zero , x) , e  = absurd (ctra _ zero x (≥-trans n≥m (=→≥ $ ap suc e)))
  where
  n≱sk+n : ∀ n k {sk+n} → sk+n ＝ suc k + n → ¬ (n ≥ sk+n)
  n≱sk+n n k e  m≥m     = false! (e ∙ +-comm (suc k) n)
  n≱sk+n n k e (m≥p mm) = n≱sk+n n (suc k) (ap suc e) mm

  ctra : ∀ n m → (n≥m : n ≥ m) → ¬ (n ≥ suc (m + space n≥m))
  ctra n m  m≥m     n≥st = n≱sk+n n 0 (ap suc (+-zero-r m)) n≥st
  ctra n m (m≥p mm) n≥st = ctra n (suc m) mm (≥-trans n≥st (=→≥ $ ap suc $ +-suc-r m (space mm)))
... | (suc s , x) , e = (s , m≥p x) , (ap suc e)

mod-from-ℕ : ∀ {n} m → {@0 n≥m : ⌞ n ≥? m ⌟} → Mod n  -- why not n ≥ m ?
mod-from-ℕ m {n≥m} = fst $ from-ℕ-= m (so→true! n≥m)

instance
  From-ℕ-Mod : ∀ {n} → From-ℕ (Mod n)
  From-ℕ-Mod {n} .From-ℕ.Constraint m = ⌞ n ≥? m ⌟
  From-ℕ-Mod {n} .from-ℕ m ⦃ (n≥m) ⦄ = mod-from-ℕ m {n≥m = n≥m}

-_ : ∀ {n} → Mod n → Mod n
- (s , p) = mod-from-ℕ s {n≥m = true→so! p}

example : 4 +m 8 ＝ the (Mod 9) 2
example = refl