Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
-- 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)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment