mod-arith.agda

module Scratch where

open import Data.Nat as ℕ using (ℕ; suc; zero)
open import Data.Product
open import Function
open import Relation.Nullary
open import Relation.Nullary.Decidable
open import Data.Empty

module GTE where
  infix 4 _≥_
  data _≥_ (m : ℕ) : ℕ → Set 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)

  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)

  _≥?_ : ∀ n m → Dec (n ≥ m)
  zero ≥? zero = yes m≥m
  zero ≥? suc m = no (⊥-elim ∘ z≯n)
  suc n ≥? zero = yes n≥z
  suc n ≥? suc m with n ≥? m
  ... | yes p = yes (s≥s p)
  ... | no ¬p = no (¬p ∘ p≥p)
open GTE using (_≥_; m≥m; m≥p; _≥?_)

Mod : ℕ → Set
Mod = ∃ ∘ _≥_

infixl 6 _+_
_+_ : ∀ {n} → Mod n → Mod n → Mod n
_+_ (_ , x) = go x
  where
  go : ∀ {n m} → n ≥ m → Mod n → Mod n
  go m≥m y = y
  go (m≥p x) (zero  , y) = _ , 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)

toNat : ∀ {n} → Mod n → ℕ
toNat = space ∘ proj₂

open import Relation.Binary.PropositionalEquality
open import Data.Empty
import Data.Empty.Irrelevant as Irrel

fromNat-≡ : ∀ {n} m
          → .(n≥m : n ≥ m)
          →  Σ[ n-m ∈ Mod n ] m ≡ toNat n-m
fromNat-≡ zero    n≥m = ( _ , m≥m) , refl
fromNat-≡ (suc n) n≥m with fromNat-≡ n (m≥p n≥m)
... | (suc space , n-1), x≡m = (space , m≥p n-1), cong suc x≡m
... | (zero      , n≥0), x≡m rewrite x≡m = Irrel.⊥-elim (contra _ zero n≥0 n≥m)
  where
  import Data.Nat.Properties as Prop

  n≱sk+n : ∀ n k {sk+n} → sk+n ≡ suc k ℕ.+ n → n ≥ sk+n → ⊥
  n≱sk+n n k wit (m≥p n≥sk+n) = n≱sk+n n (suc k) (cong suc wit) n≥sk+n
  n≱sk+n n k wit m≥m with Prop.+-cancelʳ-≡ 0 (suc k) wit
  ... | ()

  contra : ∀ n m → (n≥m : n ≥ m) → n ≥ suc (m ℕ.+ space n≥m) → ⊥
  contra n m m≥m n≥st = n≱sk+n n zero (cong suc (Prop.+-identityʳ n)) n≥st
  contra n m (m≥p n≥m) n≥st =
    contra n (suc m) n≥m (subst (λ x → n ≥ suc x) (Prop.+-suc m (space n≥m)) n≥st)

modFromNat : ∀ {n} m → .{n≥m : True (n ≥? m)} → Mod n
modFromNat m {n≥m} = proj₁ (fromNat-≡ m (toWitness n≥m))

open import Agda.Builtin.FromNat

instance
  number : ∀ {n} → Number (Mod n)
  number {n} = record
    { Constraint = λ m → (True (n ≥? m))
    ; fromNat    = λ m ⦃ n≥m ⦄ → modFromNat m {n≥m} }

import Data.Nat.Literals as NatLit
instance
  numberNat : Number ℕ
  numberNat = NatLit.number

-_ : ∀ {n} → Mod n → Mod n
- (s , p) = modFromNat s { fromWitness p }

example : 4 + 8 ≡ (Mod 9 ∋ 2)
example = refl