如何在Agda中提取统一重写逻辑优化ren-refl′的模式匹配？

解决方案：提取公共重写到主定义，用辅助函数处理分支 #

你可以通过将公共的keep*-refl重写统一放在主函数的头部，然后把模式匹配的分支逻辑放到一个where块的辅助函数中，这样既避免了重复写相同的rewrite，又不需要额外的cong操作，完全保留你最初实现的简洁性：

ren-refl′ : ∀ {Γ i t} (ts′ : List Ty) → (e : Tm {i} (Γ <> ts′) t) → ren (keep* ts′ reflᵣ) e ≡ e
ren-refl′ {Γ} ts′ e rewrite keep*-refl {Γ} ts′ = helper e
  where
    helper : ∀ {t} (e : Tm {i} (Γ <> ts′) t) → ren reflᵣ e ≡ e
    helper (var v) rewrite ren-var-refl v = refl
    helper (con e) rewrite ren-con-refl e = refl

为什么这个方案有效？ #

1. 统一处理公共重写：在主函数的rewrite语句会将keep* ts′ reflᵣ简化为reflᵣ，这样整个目标就从ren (keep* ts′ reflᵣ) e ≡ e变成了更简单的ren reflᵣ e ≡ e。
2. 保留分支的rewrite能力：辅助函数helper的类型已经是简化后的目标，所以你可以像最初的实现一样，对每个构造子使用rewrite来处理ren-var-refl和ren-con-refl，完全不需要cong——因为此时ren reflᵣ (var v)经过ren-var-refl v重写后直接等于var v，返回refl就足够了。
3. 避开lambda的限制：Agda确实不支持在lambda表达式内部使用rewrite，而用where块的辅助函数是Agda中提取重复逻辑、保持代码清晰的标准做法，完美适配你的需求。

这个方案既实现了你想要的“统一重写公共部分”的目标，又和你最初的实现逻辑保持一致，没有引入额外的复杂度。

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