Well-founded recursion by repeated division

Suppose I have some natural numbers d ≥ 2 and n > 0; in this case, I can split off the d's from n and get n = m * d^k, where m is not divisible by d.

I'd like to use this repeated removal of the d-divisible parts as a recursion scheme; so I thought I'd make a datatype for the Steps leading to m:

import Data.Nat.DivMod

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)

and write a recursive function that computes the Steps for a given pair of d and n:

total lemma: x * y `GT` 0 -> x `GT` 0
lemma {x = Z} LTEZero impossible
lemma {x = Z} (LTESucc _) impossible
lemma {x = (S k)} prf = LTESucc LTEZero

steps : (d : Nat) -> {auto dValid: d `GTE` 2} -> (n : Nat) -> {auto nValid: n `GT` 0} -> Steps d {dValid} n
steps Z {dValid = LTEZero} _ impossible
steps Z {dValid = (LTESucc _)} _ impossible
steps (S d) {dValid} n {nValid} with (divMod n d)
  steps (S d) (q * S d) {nValid} | MkDivMod q Z _ = Step (steps (S d) {dValid} q {nValid = lemma nValid})
  steps (S d) (S rem + q * S d) | MkDivMod q (S rem) remSmall = Base (S rem) (LTESucc LTEZero) remSmall q

However, steps is not accepted as total since there's no apparent reason why the recursive call is well-founded (there's no structural relationship between q and n).

But I also have a function

total wf : (S x) `LT` (S x) * S (S y)

with a boring proof.

Can I use wf in the definition of steps to explain to Idris that steps is total?

Solution

Here is one way of using well-founded recursion to do what you're asking. I'm sure though, that there is a better way. In what follows I'm going to use the standard LT function, which allows us to achieve our goal, but there some obstacles we will need to work around.

Unfortunately, LT is a function, not a type constructor or a data constructor, which means we cannot define an implementation of the WellFounded typeclass for LT. The following code is a workaround for this situation:

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)

We are going to need some helper lemmas dealing with the less than relation, the lemmas can be found in this gist (Order module). It's a subset of my personal library which I recently started. I'm sure the proofs of the helper lemmas can be minimized, but it wasn't my goal here.

After importing the Order module, we can solve the problem (I slightly modified the original code, it's not difficult to change it or write a wrapper to have the original type):

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)

I modeled steps after the divMod function from the contrib/Data/Nat/DivMod/IteratedSubtraction.idr module.

Full code is available here.

Warning: the totality checker (as of Idris 0.99, release version) does not accept steps as total. It has been recently fixed and works for our problem (I tested it with Idris 0.99-git:17f0899c).