如何不增大索引提升`Fin n`的值？Idris中mod函数实现难题

1. 如何在不增大索引的情况下提升Fin n的值？ #

首先得明确：Fin n的本质是小于n的自然数，附带类型层面的范围证明。要提升它的值（数值+1）同时保持索引n不变，必须满足一个前提：当前值加1后仍然小于n——也就是当前值不能是Fin n里的最后一个元素（数值等于n-1的那个元素）。

这里有两种实用的实现方式：

方式一：用Maybe处理边界情况 #

如果不确定当前元素是不是最后一个，可以用Maybe封装结果，成功时返回新值，失败时返回Nothing：

-- 判断是否是Fin n的最后一个元素
isLast : Fin n -> Bool
isLast {n = S Z} FZ = True
isLast {n = S (S m)} FZ = False
isLast {n = S (S m)} (FS k) = isLast k

-- 安全提升Fin值的函数
succFin : Fin n -> Maybe (Fin n)
succFin k = if isLast k 
            then Nothing 
            else Just (strengthen (FS k))

这里的strengthen是Idris自带的函数，它能把Fin (S m)转换为Fin n，前提是S m <=n——而我们已经通过isLast k排除了k是最后一个元素的情况，所以FS k对应的数值k+1 <n，完全满足转换条件。

方式二：用依赖类型证明保证合法性 #

如果能提前证明当前元素不是最后一个，可以写一个无需Maybe的总函数：

-- 定义类型，表示当前元素不是Fin n的最后一个
data NotLast : Fin n -> Type where
    NotLastFZ : NotLast {n = S (S m)} FZ
    NotLastFS : NotLast k -> NotLast (FS k)

-- 带证明的安全递增函数
succFin : (k : Fin n) -> NotLast k -> Fin n
succFin FZ NotLastFZ = FS FZ
succFin (FS k) (NotLastFS prf) = FS (succFin k prf)

这个函数要求调用者提供NotLast k的证明，确保k+1仍在Fin n范围内，类型检查器会完全保证操作的安全性。

2. 实现mod : Nat -> (m : Nat) -> Fin m时的递归范围问题 #

你遇到的是Idris类型检查的典型痛点：它不会自动推断递归过程中结果的范围，尤其是当你通过递增结果实现模运算时，无法确认递增后的结果仍然小于模数m。

问题根源 #

如果直接递归递增结果r，FS r的类型是Fin (S (pred (index of r)))，而我们需要的是Fin m——当r是last m（数值等于m-1）时，FS r的数值就是m，已经超出Fin m的范围，类型检查器自然报错。

解决方法：辅助函数处理边界重置 #

可以写一个辅助函数，每次递增前判断是否到达边界，到达就重置为0，否则安全递增：

-- 辅助函数：处理单步结果更新
nextResult : Fin m -> Fin m
nextResult {m = S Z} FZ = FZ  -- 模数为1时，结果只能是0
nextResult {m = S (S k)} FZ = FS FZ
nextResult {m = S (S k)} (FS r) = if isLast r then FZ else FS (nextResult r)

-- 最终的mod函数：从0开始递归更新结果
mod : Nat -> (m : Nat) -> {auto prf : m /= Z} -> Fin m
mod Z _ = FZ
mod (S n) m = nextResult (mod n m)

这里用isLast判断边界，重置为0避免超出范围，类型检查器能顺利通过。

更简洁的实现：用减法代替递增 #

其实模运算更直观的实现是用减法，类型检查器更容易推断范围：

-- 把小于m的Nat转换为Fin m（自动推断范围证明）
fromNatLT : (n : Nat) -> {auto prf : LT n m} -> Fin m
fromNatLT {m = S k} Z = FZ
fromNatLT {m = S k} (S n) = FS (fromNatLT n)

-- 最终的mod函数
mod : Nat -> (m : Nat) -> {auto prf : m /= Z} -> Fin m
mod n m = if n < m 
          then fromNatLT n 
          else mod (n - m) m

这个版本利用Idris的自动证明搜索，当n <m时自动生成LT n m的证明，把n转换成Fin m；否则递归减去m，直到结果小于m。

内容的提问来源于stack exchange，提问作者MaiaVictor