我正在用 PLFA 在 Agda 中做一个代码练习，以实现“一个列表的反转附加到另一个列表上，就是第二个列表的反转附加到第一个列表的反转上”的证明。
reverse-++-distrib : ∀ {A : Set} → (xs ys : List A) → reverse (xs ++ ys) ≡ reverse ys ++ reverse xs
我能够毫无问题地完成前两种归纳情况：
reverse-++-distrib {A} [] ys
reverse-++-distrib xs []
但是第三步出现“终止检查失败”错误，我猜这意味着归纳步骤没有正确完成。
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))
∎
有问题的调用显然是这样的：
反向-++-分布 {A} (x :: []) xs
对我来说这看起来不错，因为第一个参数的长度是 1，小于或等于 x :: xs 的长度。并且只有当 xs 是空列表时才相等，在这种情况下它应该进入第二个模式匹配。那么为什么 agda 对此定义有问题呢？
Agda还远远不能凭空猜出这种参数。终止检查器仅确保函数的参数在每次调用时在结构上变得更小（一旦按适当的字典顺序排列），但您的函数不满足该要求，因为在
x ∷ []结构上并不小于x ∷ xs（如您所注意到的，它可以相等）。您可能认为这是限制性的，但它通常揭示了一种更自然的方式来构建程序和证明：例如，在这里，您可以通过将其转换
reverse-++-distrib [ x ] xs为单独的引理来解决这个问题reverse-∷-distrib x xs : reverse (x ∷ xs) ≡ reverse xs ++ [ x ]。PS：您的最后一步只是
refl，因为[] ++ xs = xs根据定义。