无法使用 app_removelast_last 重写列表

Question

我有一个看起来像这样的环境：

P: list nat -> Prop
Hnil: P []
...
xs, xp: list nat
Hex: xp = a :: xs
Hnilcons: xp <> []
===================
P xp

我想将目标重写为

P ((removelast xp)++[last xp 0])

正如我在上下文中证明 xp 不是 nil 一样，我尝试使用 app_removelast_last：

Lemma app_removelast_last :
    forall l d, l <> [] -> l = removelast l ++ [last l d].

但是当我尝试

rewrite (app_removelast_last xp 0 Hnilcons).

我收到一条晦涩的错误消息：

The term "Hnilcons" has type
 "not (@eq (list nat) xp (@nil nat))"
while it is expected to have type
 "not
    (@eq (list (list nat)) ?l
       (@nil (list nat)))"
(cannot unify "list (list nat)" and
"list nat").

显然，我不明白如何使用列表不是 [] 的证明。

有人可以帮我澄清如何进行重写吗？

谢谢 ！！

Answer 1

您提供的参数不是 app_removelast_last 所期望的。你可以通过About 找到这个：

About app_removelast_last.
(*
app_removelast_last :
forall [A : Type] [l : list A] (d : A),
l <> [] -> l = removelast l ++ [last l d]

app_removelast_last is not universe polymorphic
Arguments app_removelast_last [A]%type_scope [l]%list_scope d _
*)

出现在方括号（或花括号，虽然这里没有）内的参数是implicit。这意味着 Coq 可以从显式参数中推断出它们。所以即使app_removelast_last 需要四个参数来达到相等（即A、l、d 和l <> [] 的证明），它也只期望其中两个（d 和一个证明l <> [])，因为可以从中推断出 A 和 l。或者换句话说，一旦你提供了d 和l <> [] 的证明，A 和l 只有一个可能的选择。

请注意，d 应该是提供给last 的默认值，以防列表为空。这里我们知道列表是非空的，所以我们选择哪个默认值完全无关紧要，但我们仍然必须选择一个。当您编写app_removelast_last xp Hnilcons 时，您是在说您希望xp 成为默认值（请记住，l 是隐含的！）。然后 Coq 推断，由于您的默认值具有类型 list nat，因此相关的 l 必须具有类型 list (list nat)，这就是您特别收到该错误消息的原因。

解决方案是使用例如app_removelast_last 0 Hnilcons 重写，因为0 是一个足够的默认值。

---

编辑：您也可以避免使用 @ 的隐式参数，如下所示：

@app_removelast_last nat xp 0 Hnilcons

但是，根据您的评论，您没有使用标准库版本的这个引理，而是Constant AlphaCode1_forward_c.app_removelast_last，它显然特定于自然数列表并且没有隐式参数，所以这可能不是导致问题的原因。