How to increase the value of a `Fin n` without increasing its index?

When trying to implement a mod : Nat -> (m : Nat) -> Fin m function on Idris, I noticed the obvious algorithm wouldn't work because, when looping around and when increasing the result, Idris won't believe it is still within range. This snippet explains the problem:

-- (M : Nat) is the modulus, doesn't change
-- (r : Fin M) is the result, increases as you recurse
-- (n : Nat) is the dividend, the recursion stops when it is 0
-- (m : Nat) is the modulus index, when it is Zero, the result loops around
modAux : (M : Nat) -> (r : Fin M) -> (n : Nat) -> (m : Nat) -> Nat

-- When `n` is Zero, we're done, so, return result (works!)
modAux M r Z m = r

-- When `n > 0` but `m` iz zero, the result must loop around
-- Problem: `Z` is not a valid `Fin M`!
modAux M r (S n) Z = modAux M Z n M

-- when `n > 0` and `m > 0`, decrease both and increase the result
-- Problem: `(S r)` is not a valid `Fin M`!
modAux M r (S n) (S m) = modAux M (S r) n m

To implement modAux, it seems like we need a suc : Fin n -> Fin n function that loops around. I had trouble implementing that, too. When looking at Agda's standard lib implementation of mod, I noticed it first proves mod-lemma : (acc d n : ℕ) → let s = acc + n in mod-helper acc s d n ≤ s, to, then, implement mod by using Fin.fromℕ≤″. That looks heavy. Is there any alternative way to increase a Fin n value without increasing its index?

Solution

Here is a solution:

open import Function
open import Data.Nat
open import Data.Fin renaming (zero to fzero; suc to fsuc) using (Fin)

suc-around : ∀ {n} -> Fin n -> Fin n
suc-around {0}     ()
suc-around {suc _} i  = go id i where
  go : ∀ {n m} -> (Fin n -> Fin (suc m)) -> Fin n -> Fin (suc m)
  go {1}           k  fzero   = fzero
  go {suc (suc _)} k  fzero   = k (fsuc fzero)
  go               k (fsuc i) = go (k ∘ fsuc) i

The idea is that you need to decide whether to return Fin.suc i or Fin.zero in the very end of processing a Fin n. I.e. when you make recursive calls, you do not know whether the computation will result in an additional Fin.suc or Fin.zero will be returned. This choice can be made only in the base case where you know that the argument of type Fin is actually Fin.zero. This is what these two lines are responsible for:

  go {1}           k  fzero   = fzero
  go {suc (suc _)} k  fzero   = k (fsuc fzero)

If there is no room for another Fin.suc (i.e. the argument actually has the Fin 1 type), then simply return Fin.zero. But if it's possible to apply another Fin.suc without changing the type, then do it and also apply the continuation which consists of Fin.sucs collected so far while performing recursive calls:

  go               k (fsuc i) = go (k ∘ fsuc) i

So the main idea is that you need to choose what to return in the base case, hance in the recursive case you only make sure that you don't lose the information of how many Fin.sucs have been processed.

Regarding mod itself I like this implementation by András Kovács.