Agda 终止检查对于反向-++-分布练习失败

Question

我正在 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))
  ∎

有问题的调用显然是这样的：

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

对我来说这看起来很好，因为第一个参数的长度是 1，它小于或等于 x :: xs 的长度。仅当 xs 为空列表时它才相等，在这种情况下它应该进入第二个模式匹配。那么为什么 agda 这个定义有问题呢？

Answer 1

对我来说这看起来很好，因为第一个参数的长度是 1，它小于或等于 x :: xs 的长度。仅当 xs 为空列表时它才相等，在这种情况下它应该进入第二个模式匹配。那么为什么 agda 这个定义有问题呢？

Agda 相当远不能凭空猜出这种论点。终止检查器仅确保每次调用时函数的参数在结构上变得更小（一旦按字典顺序适当排序），但您的函数不满足该要求，因为 x ∷ [] 在结构上并不小于

x ∷ xs

（它可以正如您所注意到的，是平等的）。您可能认为这是限制性的，但它通常揭示了一种更自然的方式来构造程序和证明：例如，在这里，您可以通过将

reverse-++-distrib [ x ] xs

变成单独的引理

reverse-∷-distrib x xs : reverse (x ∷ xs) ≡ reverse xs ++ [ x ]

来解决这个问题。P.S.：你的最后一步只是

refl

，因为根据定义

[] ++ xs = xs

。