Int.normalize

-- the canonical representative: strip successors pairwise

import Natural (+, plusZeroId, plusSucId, zeroPlusId)
import Int (Int)

normPair : ℕ → ℕ → ℕ × ℕ
normPair = λa. ℕ-elim (λb. Z, b) (n ih. λb. ℕ-elim (S n, Z) (m ihb. ih m) b) a

-- the three defining equations of normPair, in folded vocabulary, so
-- they can fire as rewrite rules without unfolding normPair in goals
normPairZero : (b : ℕ) → normPair Z b ≡ (Z, b) using (Int.normalize.normPair.eq)
normPairZero = λb. ⋆

normPairSucZero : (n : ℕ) → normPair (S n) Z ≡ (S n, Z) using (Int.normalize.normPair.eq)
normPairSucZero = λn. ⋆

normPairSucSuc : (n m : ℕ) → normPair (S n) (S m) ≡ normPair n m using (Int.normalize.normPair.eq)
normPairSucSuc = λn m. ⋆

-- normPair a b is R-related to (a, b)
normSound : (a b : ℕ) → normPair a b .π₁ + b ≡ normPair a b .π₂ + a
  using (hyp.rw,
    normPairZero,
    normPairZero.rw,
    normPairSucZero,
    normPairSucZero.rw,
    normPairSucSuc,
    normPairSucSuc.rw,
    plusSucId,
    plusSucId.rw,
    plusZeroId,
    plusZeroId.rw,
    zeroPlusId,
    zeroPlusId.rw)
normSound = λa. ℕ-elim (λb. ⋆) (n ih. λb. ℕ-elim ⋆ (m ihb. ⋆) b) a

-- at the quotient, normalization is invisible
normClass : (a b : ℕ) → class (normPair a b) ≡ class (a, b) ∈ Int using (Int.Int.unfold, normSound)
normClass = λa b. ⋆

intNormalize : Int → Int using (hyp.rw, Int.Int.unfold, normClass, normClass.rw)
intNormalize = λz. quot-elim (rep. class (normPair (rep .π₁) (rep .π₂))) z

intNormalizeTest1 : intNormalize (class (S Z, Z)) ≡ class (S Z, Z)
  using (Int.Int.unfold, Int.normalize.intNormalize.eq, Int.normalize.normPair.eq)
intNormalizeTest1 = ⋆

intNormalizeTest2 : intNormalize (class (S Z, 2)) ≡ class (Z, S Z)
  using (Int.Int.unfold, Int.normalize.intNormalize.eq, Int.normalize.normPair.eq)
intNormalizeTest2 = ⋆