如何在不增加索引的情况下增加`Fin n`的值？

Question

当试图mod : Nat -> (m : Nat) -> Fin m在 Idris上实现一个函数时，我注意到明显的算法不起作用，因为当循环和增加结果时，Idris 不会相信它仍在范围内。这段代码解释了这个问题：

-- (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

为了实现modAux，似乎我们需要一个suc : Fin n -> Fin n循环的函数。我也很难实现。在查看 Agda 的标准库实现时mod，我注意到它首先证明mod-lemma : (acc d n : ?) ? let s = acc + n in mod-helper acc s d n ? s了 ，然后，mod通过使用实现Fin.from???。那看起来很重 有没有其他方法可以在Fin n不增加索引的情况下增加值？

Answer 1

Data.Fin.strengthen 可以做繁重的工作。

-- Data.Fin.strengthen : Fin (S n) -> Either (Fin (S n)) (Fin n)
-- conceptually
-- strengthen Data.Fin.last = Left last
-- strengthen n = Right n

我个人不喜欢这个功能，因为它的输出“太大”；它通常不会使用Left它所说的可以返回的所有值，但它在标准库中并且可以工作。

rotateUp : Fin n -> Fin n
rotateUp {n = Z} _ impossible
rotateUp {n = S k} f = either (const FZ) FS $ strengthen f

不建议modAux直接写。我宁愿mod用这个函数来表达，它更通用：

toChurchNat : Nat -> (a -> a) -> (a -> a)
toChurchNat Z _ x = x
toChurchNat (S n) f x = toChurchNat n f (f x)

Nat它将a转换为其 Church 表示（一种重复任何内函数多次的函数）。因此：

mod : Nat -> (divisor : Nat) -> {auto prf : IsSucc divisor} -> Fin divisor
mod dividend (S divisor') = toChurchNat dividend rotateUp FZ