Solution to SO question

AB.agda

-- https://stackoverflow.com/questions/52244800/how-to-normalize-rewrite-rules-that-always-decrease-the-inputs-size/52246261#52246261

open import Relation.Binary.PropositionalEquality
open import Data.Nat
open import Relation.Nullary
open import Data.Empty
open import Data.Star

data AB : Set where
  A : AB -> AB
  B : AB -> AB
  C : AB

-- 1-step rewrite
infix 3 _~>_
data _~>_ : AB → AB → Set where
  BA : ∀ {x} → B (A x) ~> x
  A  : ∀ {x y} → x ~> y → A x ~> A y
  B  : ∀ {x y} → x ~> y → B x ~> B y

-- reflexive-transitive closure
infix 3 _~>*_
_~>*_ : AB → AB → Set
_~>*_ = Star _~>_

normal : AB → Set
normal ab = ∀ {ab'} → ¬ (ab ~> ab')

consBs : ℕ → AB → AB
consBs zero    ab = ab
consBs (suc n) ab = B (consBs n ab)

reduce : AB -> ℕ -> AB
reduce (A ab) (suc n) = reduce ab n
reduce (A ab) zero    = A (reduce ab zero)
reduce (B ab) n       = reduce ab (suc n)
reduce C      n       = consBs n C

consBsB : ∀ n ab → B (consBs n ab) ≡ consBs n (B ab)
consBsB zero    ab = refl
consBsB (suc n) ab = cong B (consBsB n ab)

consBsA : ∀ n ab → B (consBs n (A ab)) ~> consBs n ab
consBsA zero    ab = BA
consBsA (suc n) ab = B (consBsA n ab)

lem : ∀ ab n → consBs n ab ~>* reduce ab n
lem (A ab) zero    = gmap A A (lem ab zero)
lem (A ab) (suc n) = consBsA n ab ◅ lem ab n
lem (B ab) n       = subst  (_~>* reduce ab (suc n)) (consBsB n ab) (lem ab (suc n))
lem C      n       = ε

reduceSound : ∀ ab → ab ~>* reduce ab 0
reduceSound ab = lem ab 0

lem2 : ∀ ab n → normal (reduce ab n)
lem2 (A ab) (suc n)       p      = lem2 ab n p
lem2 (A ab) zero          (A p)  = lem2 ab 0 p
lem2 (B ab) n             p      = lem2 ab (suc n) p
lem2 C      zero          ()
lem2 C      (suc zero)    (B ())
lem2 C      (suc (suc n)) (B p)  = lem2 (B C) n p

reduceNormal : ∀ ab → normal (reduce ab 0)
reduceNormal ab = lem2 ab 0