Agda PLFA量词章节练习题：2*m写法互递归函数终止检查失败

Agda 的终止检查仅基于语法层面的结构递归规则工作：它只会识别模式匹配时直接拆分出的构造器子项，判断递归调用的参数是否在构造器层级上严格小于原参数，不会对自定义算术运算的等式语义做任何逻辑推导。
对比两个版本的实现差异，核心原因在于：

• 可正常通过的 m*2 版本中，所有和参数大小相关的关系都是语法层面可直接识别的：odd 的约束等式为 1 + m * 2 ≡ n，其中 1 对应字面构造器 suc zero，因此 1 + m*2 等价于语法层面的 suc (m*2)，Agda 可以直接看到互递归过程中每个传入的 n 都比上一层少一个 suc 构造器，满足结构递减的要求。
• 报错的 2*m 版本中，所有大小关系（比如 2*suc m ≡ suc (2*m +1)、2*m +1 ≡ suc(2*m)）都是通过额外等式证明、rewrite 规则推导出来的，并非语法层面的直接构造器嵌套。终止检查器看不到这些语义上的递减关系，仅能观察到：
  • even 匹配 suc m 分支调用 odd 时，传入的 m 是 suc m 的直接子项，符合递减要求
  • odd 没有对自己的参数 m 做任何构造器匹配，直接将 m 原样传给 even，这一步没有任何语法层面的递减证据——Agda 无法证明 odd 收到的 m 是 even 拆分出的更小的 m，也无法识别 odd 调用 even 时传入的 n 实际比 odd 自身的 n 小一层，因此判定存在无限递归风险。

核心思路是让递归调用的结构递减关系变为语法层面可直接识别的，不要将大小关系隐藏在等式证明的语义中。具体调整点：

• 给 ∃-odd′ 增加对第一个分量 m 的构造器匹配，拆分为两个独立分支：
  • 匹配 ⟨ zero , eq ⟩ 分支：此时 2*zero +1 ≡ 1 ≡n，直接返回对应的 odd 构造值，不需要递归
  • 匹配 ⟨ suc m , refl ⟩ 分支：此时传入 even 的参数 m 是 suc m 的直接语法子项，Agda 可以直接识别这个构造器层级的递减
• 保留原有的等式证明逻辑，不需要修改互递归的参数传递结构，仅需要显式拆分 odd 的模式匹配分支，让终止检查器能看到每一步递归的参数都是从上层构造器中直接拆出的子项。

调整后的 odd 分支核心逻辑示例：

∃-odd′ ⟨ zero , refl ⟩ = odd-suc even-zero
∃-odd′ ⟨ suc m , refl ⟩ rewrite +-suc (2 * m) 0
                | +-identityʳ m
                | +-identityʳ (m + m)
                | dbl≡2* m
                = odd-suc (∃-even′ ⟨ m , refl ⟩)

这样调整后，Agda 可以直接识别到两个函数递归时传入的参数都是上层构造器拆分出的直接子项，整个互递归的构造器层级严格递减，即可通过终止检查。

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