Idris 2中类似Agda rewrite且修改环境绑定类型的方法

假设我定义了如下定理：

foo : (n : _) -> (f : Fin (n + 0)) -> ...
foo n f = ?goal

我希望在需要Fin n的上下文中直接使用原术语f（而非replace (plusZeroRightNeutral n) f），需要借助引理同时改写目标类型和环境中f的类型。

在Agda中，直接用rewrite就能实现（它会展开为两个并行with抽象）：

foo : (n : _) -> (f : Fin (n + 0)) -> ...
foo n f rewrite plusZeroRightNeutral n = ?goal

但Idris 2的rewrite仅修改目标类型，不会影响作用域内绑定的类型。我尝试模仿Agda的实现写出了以下代码：

foo : (n : _) -> (f : Fin (n + 0)) -> ...
foo n f with (plusZeroRightNeutral n)
  _ | eq with (plus n 0)
    _ | _ = case eq of Refl => ?goal

这段代码先获取n + 0 = n的证明，但直接对证明模式匹配会报错Can't solve constraint between: ?n [no locals in scope] and plus ?n 0.，因此我对plus n 0做了with抽象，让它在f和eq的类型中成为单一术语，之后才能对eq模式匹配，此时goal的环境中f的类型变为Fin n。

但这种方式仅适用于单次改写，多次改写会嵌套繁琐。我尝试用Agda式的并行with（比如with (plus n 0, plusZeroRightNeutral n)），但要么语法错误，要么类型检查器异常。请问有没有更优的实现方式？

更优实现方式 #

1. 使用带proof的with构造（Idris 2推荐方式） #

Idris 2的with支持通过proof关键字显式绑定等式证明，同时抽象掉需要改写的项，避免嵌套：

foo : (n : Nat) -> (f : Fin (n + 0)) -> Fin n
foo n f with (n + 0) proof eq
  foo n f | n = case eq of Refl => f

这里with (n + 0) proof eq会同时将n + 0抽象为n，并把等式n + 0 = n绑定为eq，模式匹配Refl后，环境中f的类型会自动改写为Fin n，无需额外嵌套。

2. 封装通用改写辅助函数 #

如果需要多次改写，可以封装一个辅助函数来统一处理类型改写，避免重复代码：

rewriteVar : {a : Type} -> {b : Type} -> (eq : a = b) -> (x : a) -> b
rewriteVar Refl x = x

foo : (n : Nat) -> (f : Fin (n + 0)) -> Fin n
foo n f = rewriteVar (plusZeroRightNeutral n) f

这种方式虽然需要显式调用辅助函数，但代码简洁，多次改写时只需重复调用即可，且语义清晰。

3. 使用let绑定配合模式匹配 #

通过let直接绑定等式证明并模式匹配，也能实现环境类型的改写：

foo : (n : Nat) -> (f : Fin (n + 0)) -> Fin n
foo n f = let eq = plusZeroRightNeutral n in
          case eq of
            Refl => f

不过这种方式仅当等式两边的类型在类型检查器中能被直接统一时生效，对于复杂等式可能需要结合with抽象。

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