list - Agda：std-lib：列表：除了最后一个元素之外的所有元素与 snoc

Question

我是这样定义allButLast的：

allButLast : ∀ {a} {A : Set a} → List A → List A
allButLast l.[] = l.[]
allButLast list = l.reverse (tail' (l.reverse list))

并想证明以下陈述：

allButLast-∷ʳ :
  ∀ {a} {A : Set a} →
    (list : List A) →
      (y : A) →
        allButLast (list ∷ʳ y) ≡ list
allButLast-∷ʳ []       y = refl
allButLast-∷ʳ (x ∷ []) y = refl
allButLast-∷ʳ (x ∷ xs) y =
  begin
    allButLast ((x ∷ xs) ++ [ y ])
  ≡⟨⟩
    reverse (tail' (reverse ((x ∷ xs) ∷ʳ y)))
  ≡⟨ ? ⟩
    reverse (tail' (y ∷ reverse (x ∷ xs)))
  ≡⟨⟩
    reverse (reverse (x ∷ xs))
  ≡⟨ reverse-involutive (x ∷ xs) ⟩
    (x ∷ xs)
  ∎

我需要在哪里找到要替换?的内容。

我定义：

reverse-∷ʳ :
  ∀ {a} {A : Set a} →
    (list : List A) →
      (n : A) →
        reverse (list ∷ʳ n) ≡ n ∷ reverse list

我能够证明这一点。

我想用它reverse-∷ʳ (x ∷ xs) y来替换?但是，我收到以下错误：

x ∷ [] != [] of type List A
when checking that the expression reverse-∷ʳ (x ∷ xs) y has type
reverse (tail' (reverse ((x ∷ xs) ∷ʳ y))) ≡
reverse (tail' (y ∷ reverse (x ∷ xs)))

我不确定如何解释它。这是因为我在x ∷ []申请时没有涵盖此案reverse-∷ʳ (x ∷ xs) y吗？

标签： listagdaagda-stdlib

Answer 1

我建议以下解决方案：

allButLast : ∀ {a} {A : Set a} → List A → List A
allButLast [] = []
allButLast (_ ∷ []) = []
allButLast (x ∷ x₁ ∷ l) = x ∷ (allButLast (x₁ ∷ l))

allButLast-∷ʳ : ∀ {a} {A : Set a} {l : List A} {x} → allButLast (l ∷ʳ x) ≡ l
allButLast-∷ʳ {l = []} = refl
allButLast-∷ʳ {l = _ ∷ []} = refl
allButLast-∷ʳ {l = x ∷ x₁ ∷ l} = cong (x ∷_) (allButLast-∷ʳ {l = x₁ ∷ l})

---

一段时间以来，您在#Agda 中问了很多问题，这完全没问题。但是，不要采取错误的方式，您绝对应该尝试了解您在做什么，而不是一次又一次地问类似的问题。在我看来，您似乎不太了解如何在 Agda 中编写定义或证明，仅仅是因为您没有花足够的时间来尝试了解所有这些工作的原理。例如，您的先例问题表明您还不太了解函数和构造函数之间的区别，以及模式匹配。此外，您总是尝试使用链式等式来证明您的目标，即使在大多数情况下，对您正在处理的数据（主要是列表和向量）进行简单的案例拆分就足以解决您的问题。你倾向于把事情复杂化，相信我，这不是你在 Agda 或其他证明助手中开发时想要做的，因为证明本身往往很快就会变得非常复杂。我可以看到你渴望学习和提高你的 Agda 技能，所以这里有一些建议，从长远来看，这些建议比以不正确的方式定义和证明随机概念和属性更有用：

• 从你的定义和证明中退后一步
• 如果它足够简单可以理解，请花一些时间来弄清楚证明可能是什么。
• 尝试理解 Agda 的基本机制，如大小写，而不是更高级的机制，如相等推理。
• 确保您不能通过对其输入的简单递归而不是更复杂/耗时的方式来证明您的引理。
• 遵循一些您可以在网上找到的教程，其中大部分都在以下 wiki 页面中重新组合https://agda.readthedocs.io/en/v2.6.0.1/getting-started/tutorial-list.html
• 尝试并理解（并可能自己复制）作为您在此处提出的问题的答案的证明，因为您的许多新问题实际上可以以类似的方式得到回答/解决。
• 在定义数量时，尝试尽可能简单地定义它们，例如查看我的allButLast定义，而不是你的定义，它使用其他复杂函数，而不是仅仅在其输入上递归定义。
• 通过编写一些简单的测试用例并使用它们来评估它们，CTRL-C CTRL-N或者通过证明它们的一些非常简单的属性来确保您的定义确实符合您的意图，例如。您之前的定义allButLast，可以在您之前的问题中找到，实际上是列表上的标识函数，因为您总是准确地返回输入，通过一些测试和退一步可以很容易地看到。

总而言之，花点时间试着真正理解你在做什么，因为如果你不这样做，你将无法在 Agda 中开发任何重要的东西。我希望这些建议对您有所帮助，并且您不会误以为是。可能还有更多，但这是我可以直接想到的那些的简要概述。