主页 / coding / 问题 / 79010540
Accepted
Werner Germán Busch
Asked: 2024-09-22 06:11:29 +0800 CST

Agda 终止检查在反向-++-分布练习中失败

  • 772

我正在用 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

1 个回答

  1. Best Answer

    对我来说这看起来不错，因为第一个参数的长度是 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根据定义。

    • 1

相关问题