Agda中reverse-++-distrib练习终止检查失败问题求助

我正在完成PLFA中的Agda代码练习，需要证明两个列表拼接后的反转等于第二个列表反转后拼接第一个列表反转，对应定理的类型签名为：

reverse-++-distrib : ∀ {A : Set} → (xs ys : List A) → reverse (xs ++ ys) ≡ reverse ys ++ reverse xs

我已经顺利完成前两个归纳case：

reverse-++-distrib {A} [] ys

reverse-++-distrib xs []

但在第三个归纳步骤（(x :: xs)的情况）中出现了Termination checking failed错误，推测是归纳调用的逻辑有误。相关代码如下：

reverse-++-distrib {A} (x :: xs) ys =
  begin
    reverse ((x :: xs) ++ ys)
  ≡⟨⟩
    reverse (x :: (xs ++ ys))
  ≡⟨⟩
    reverse (xs ++ ys) ++ [ x ]
  ≡⟨ cong (_++ [ x ]) (reverse-++-distrib xs ys) ⟩
    (reverse ys ++ reverse xs) ++ [ x ]
  ≡⟨ ++-assoc (reverse ys) (reverse xs) [ x ] ⟩
    reverse ys ++ (reverse xs ++ [ x ])
  ≡⟨ cong ((reverse ys) ++_) (cong ((reverse xs) ++_) (sym (reverse-++-fixed-point {A} x))) ⟩
    (reverse ys) ++ (reverse xs ++ (reverse [ x ]))
  ≡⟨ cong ((reverse ys) ++_) (sym (reverse-++-distrib {A} (x :: []) xs)) ⟩
    (reverse ys) ++ (reverse ([ x ] ++ xs))
  ≡⟨⟩
    (reverse ys) ++ (reverse (x :: ([] ++ xs)))
  ≡⟨ cong ((reverse ys) ++_) (cong reverse (cong (x ::_) (++-identityˡ xs))) ⟩
    (reverse ys) ++ (reverse (x :: xs))
  ∎

问题出在这一行调用：

reverse-++-distrib {A} (x :: []) xs

我原本认为这个调用的第一个参数长度为1，小于等于x :: xs的长度，只有当xs为空时两者长度才相等，此时应该匹配到第二个已完成的case，但Agda仍然判定终止检查失败，这是为什么？

原因分析 #

Agda的终止检查器不会基于参数的“长度”这类语义属性判断调用是否递减，它只看参数的语法结构是否是当前递归参数的直接子项。

当前递归的参数是(x :: xs)和ys，而你调用的reverse-++-distrib (x :: []) xs中：第一个参数(x :: [])并不是(x :: xs)的直接子项（(x :: xs)的直接子项只有x和xs），第二个参数xs虽然符合子项要求，但第一个参数的语法结构不满足终止检查器的规则。哪怕(x :: [])长度更短，终止检查器也不会“计算长度”验证，只认语法上的子项关系。当xs不为空时，(x :: [])和(x :: xs)没有语法子项关联，检查器无法确认调用一定会终止，因此报错。

正确的归纳步骤 #

你完全不需要绕到reverse-++-distrib (x :: []) xs这一步——因为reverse xs ++ [x]本身就是reverse (x :: xs)的定义（假设你的reverse实现为reverse [] = []，reverse (x :: xs) = reverse xs ++ [x]）。

修正后的证明链可以直接跳过多余步骤，简化为：

reverse-++-distrib {A} (x :: xs) ys =
  begin
    reverse ((x :: xs) ++ ys)
  ≡⟨⟩
    reverse (x :: (xs ++ ys))
  ≡⟨⟩
    reverse (xs ++ ys) ++ [ x ]
  ≡⟨ cong (_++ [ x ]) (reverse-++-distrib xs ys) ⟩
    (reverse ys ++ reverse xs) ++ [ x ]
  ≡⟨ ++-assoc (reverse ys) (reverse xs) [ x ] ⟩
    reverse ys ++ (reverse xs ++ [ x ])
  ≡⟨ cong (reverse ys ++_) (sym (reverse-cons {A} x xs)) ⟩
    reverse ys ++ reverse (x :: xs)
  ∎

其中reverse-cons是对应reverse (x :: xs) ≡ reverse xs ++ [x]的引理（如果reverse是按上述方式定义的，这个等式可以直接用refl或一个极简引理）。

内容的提问来源于stack exchange，提问作者Werner Germán Busch