Agda子类型反演引理证明中subst相关终止检查失败问询

误区澄清 #

你初步判断subst调用是导致终止检查失败的核心原因，这个结论并不准确。
终止检查失败的本质诱因是当前子类型定义中无约束的传递规则，叠加Agda结构递归检查的固有特性：

• 你的_<:_定义里，s-trans是独立的顶层构造子，Agda的终止检查器只会识别“递归传入的参数是当前匹配构造子的直接字段”这种严格的结构递减关系，没法通过逻辑推导判断“拆分传递规则后的两步推导，比完整的传递规则推导结构更小”。
• 代码里的subst只是进一步放大了这个问题：它会把原本清晰的项结构包上一层等价性证明的外壳，让检查器完全看不到传入递归函数的参数本质上是s-trans构造子里的字段，直接失去了终止性判断的依据。
  从数学逻辑上讲，你写的证明本身是成立的：对传递规则分支做归纳拆分的路径完全符合子类型推导树的归纳原理，只是Agda的检查器没法自动追踪这种逻辑上的大小关系。

可落地的解决方案 #

• 优先方案：切换到算法子类型定义
  去掉声明性定义里的s-trans规则，重新定义结构化的算法子类型关系（保留反射、Top对任意类型、箭头协变逆变这三个核心规则，不额外添加传递构造子）。这种定义下的所有规则都是严格结构化的，你要证明的反向引理根本不需要处理传递分支，自然不会出现终止检查问题，这也是《Types and Programming Languages》中证明这类引理的标准路径。后续只需要额外证明算法子类型和原声明性子类型的等价性，就可以安全迁移所有证明结论。
• 次选方案：为推导关系绑定高度测度，做有界递归
  如果必须保留原有的声明性子类型定义，可以给每个_<:_推导项添加一个自然数高度字段，明确每个构造子生成的推导高度严格大于其入参的高度。证明反向引理时沿着高度做归纳，而不是直接对推导项做结构递归——此时检查器可以通过“递归传入的推导高度严格小于当前推导高度”的证据，判断递归的收敛性，subst的存在也不会干扰判断。
• 不推荐的临时方案
  不建议直接用{-# TERMINATING #-}标注函数来绕过检查，这种方式会完全丢失终止性保障，一旦证明逻辑有漏洞，很容易引入逻辑不一致的风险。

代码优化提示 #

你当前代码里用&做嵌套合取的写法可以替换为原生的依赖对类型，减少不必要的语法依赖；处理传递分支时，可以直接调用_<:_的原生归纳原理完成证明，不需要手动逐分支匹配构造子，大幅减少手写递归带来的检查负担。 #

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