WellFoundedStep.idr

-- http://stackoverflow.com/questions/40611744/well-founded-recursion-by-repeated-division

import Data.Nat.DivMod
import Order

data Steps: (d : Nat) -> {auto dValid: d `GTE` 2} -> (n : Nat) -> Type where
  Base: (rem: Nat) -> (rem `GT` 0) -> (rem `LT` d) -> (quot : Nat) -> Steps d {dValid} (rem + quot * d)
  Step: Steps d {dValid} n -> Steps d {dValid} (n * d)

total
accIndLt : {P : Nat -> Type} ->
         (step : (x : Nat) -> ((y : Nat) -> LT y x -> P y) -> P x) ->
         (z : Nat) -> Accessible LT z -> P z
accIndLt {P} step z (Access f) =
  step z $ \y, lt => accIndLt {P} step y (f y lt)

total
wfIndLt : {P : Nat -> Type} ->
        (step : (x : Nat) -> ((y : Nat) -> LT y x -> P y) -> P x) ->
        (x : Nat) -> P x
wfIndLt step x = accIndLt step x (ltAccessible x)


-- n = m * d^k, where m is not divisible by d
total
steps : (n : Nat) -> {auto nValid : 0 `LT` n} -> (d : Nat) -> Steps (S (S d)) n
steps n {nValid} d = wfIndLt {P = P} step n d nValid
  where
    P : (n : Nat) -> Type
    P n = (d : Nat) -> (nV : 0 `LT` n) -> Steps (S (S d)) n

    step : (n : Nat) -> (rec : (q : Nat) -> q `LT` n -> P q) -> P n
    step n rec d nV with (divMod n (S d))
      step (S r + q * S (S d)) rec d nV | (MkDivMod q (S r) prf) =
        Base (S r) (LTESucc LTEZero) prf q
      step (Z + q * S (S d))       rec d nV | (MkDivMod q Z     _) =
        let qGt0 = multLtNonZeroArgumentsLeft nV in
        let lt = multLtSelfRight (S (S d)) qGt0 (LTESucc (LTESucc LTEZero)) in
        Step (rec q lt d qGt0)