ocaml - Coq 中的非空列表追加定理

Question

我试图在 Coq 中证明以下引理:

Require Import Lists.List.
Import ListNotations.
Lemma not_empty : forall (A : Type) (a b : list A),
    (a <> [] \/ b <> []) -> a ++ b <> [].

现在我目前的策略是在 a 上进行破坏，在打破分离之后，我可以理想地声明，如果 a <> [] 那么 a++ b 也必须是 <> []... 那是计划，但我似乎无法通过类似于第一个“a++ b <> []”的子目标，即使我的上下文明确指出“b <> []”。有什么建议吗？

我还查看了许多预先存在的列表定理，但没有发现任何特别有用的东西(对于某些子目标，减去 app_nil_l 和 app_nil_r)。

Answer 1

以 destruct a 开头确实是个好主意。

对于 a 的情况是 Nil ，您应该销毁 (a <> [] \/ b <> [])假设。会有两种情况:

正确的假设[] <> []是 contradiction ,

左一，假设b <> []是您的目标(自 a = [] 起)

对于 a 的情况是 a :: a0 ，你应该使用 discriminate正如朱利安所说。