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

Question

当尝试在 Idris 上实现 mod : Nat -> (m : Nat) -> Fin m 函数时，我注意到明显的算法不起作用，因为在循环和增加时结果， 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 函数。我也很难实现它。当查看 mod 的 Agda 标准库实现时，我注意到它首先证明了 mod-lemma : (acc d n : ℕ) → let s = acc + n in mod-helper acc s d n ≤ s ，然后，使用 Fin.fromℕ≤″ 实现 mod。那看起来很重。有没有其他方法可以在不增加索引的情况下增加 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 转换成它的 Church 表示(一个函数重复任何内函数一定次数)。因此:

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