Norm.agda

module Norm where

open import Data.Empty
open import Data.Nat
open import Data.Product
open import Data.Sum
open import Function
open import Relation.Binary.PropositionalEquality

data Int : Set where
  s : Int → Int
  p : Int → Int
  z : Int

norm : Int → Int
norm (s x) with norm x
... | p y = y
... | y = s y
norm (p x) with norm x
... | s y = y
... | y = p y
norm z = z

app : ∀ {a} {A : Set a} → ℕ → (A → A) → A → A
app zero    f = id
app (suc n) f = f ∘ app n f

-- The main lemma about normals forms.
--
-- norm x returns either s (s (s ... z)) for some number of 's's, or
-- p (p (p ... z)) for some number of 'p's.
nform : ∀ x → ∃ λ n → norm x ≡ app n s z ⊎ norm x ≡ app n p z
nform (s x) with nform x
nform (s x) | _     , inj₁ _ with norm x
nform (s _) | n     , inj₁ q  | s _ = 1 + n , inj₁ (cong s q)
nform (s _) | zero  , inj₁ () | p _
nform (s _) | suc _ , inj₁ () | p _
nform (s _) | _     , inj₁ _  | z   = 1 , inj₁ refl
nform (s x) | _     , inj₂ _ with norm x
nform (s _) | zero  , inj₂ () | s _
nform (s _) | suc _ , inj₂ () | s _
nform (s _) | zero  , inj₂ () | p _
nform (s _) | suc n , inj₂ q  | p _ = n , inj₂ (cong (λ {(p x) → x; x → x}) q)
nform (s _) | _     , inj₂ _  | z   = 1 , inj₁ refl

nform (p x) with nform x
nform (p x) | _     , inj₁ _ with norm x
nform (p _) | zero  , inj₁ () | s _
nform (p _) | suc n , inj₁ q  | s _ = n , inj₁ (cong (λ {(s x) → x; x → x}) q)
nform (p _) | zero  , inj₁ () | p _
nform (p _) | suc _ , inj₁ () | p _
nform (p _) | _     , inj₁ _  | z   = 1 , inj₂ refl
nform (p x) | _     , inj₂ _ with norm x
nform (p _) | zero  , inj₂ () | s _
nform (p _) | suc _ , inj₂ () | s _
nform (p _) | n     , inj₂ q  | p _ = 1 + n , inj₂ (cong p q)
nform (p _) | _     , inj₂ _  | z   = 1 , inj₂ refl

nform z = 0 , inj₁ refl

bad-+ : ∀ n {x} → p x ≢ app n s z
bad-+ zero    ()
bad-+ (suc _) ()

-- Normalizing a positive number already in normal form
-- does nothing.
norm+ : ∀ n → norm (app n s z) ≡ app n s z
norm+ zero = refl
norm+ (suc n) with norm (app n s z) | norm+ n
... | s r | q = cong s q
... | p r | q = ⊥-elim (bad-+ n q)
... | z   | q = cong s q

bad-- : ∀ n {x} → s x ≢ app n p z
bad-- zero    ()
bad-- (suc _) ()

-- Normalizing a negative number already in normal form
-- does nothing as well.
norm- : ∀ n → norm (app n p z) ≡ app n p z
norm- zero = refl
norm- (suc n) with norm (app n p z) | norm- n
... | s r | q = ⊥-elim (bad-- n q)
... | p r | q = cong p q
... | z   | q = cong p q

open ≡-Reasoning

-- Figure out whether 'norm x' is positive or negative
-- and then apply previous lemmas.
idem : ∀ x → norm (norm x) ≡ norm x
idem x with nform x
idem x | n , inj₁ q = begin
    norm (norm x)     ≡⟨ cong norm q ⟩
    norm (app n s z)  ≡⟨ norm+ n ⟩
    app n s z         ≡⟨ sym q ⟩
    norm x            ∎
idem x | n , inj₂ q = begin
    norm (norm x)     ≡⟨ cong norm q ⟩
    norm (app n p z)  ≡⟨ norm- n ⟩
    app n p z         ≡⟨ sym q ⟩
    norm x            ∎