Coq中的非空列表追加定理

Question

我正在尝试在Coq中证明以下引理：

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

目前我的策略是在a上执行destruct操作，拆开析取式(disjunction)，然后理想情况下我可以声明如果a <> []，那么a ++ b也必须是<>[]...这就是计划，但是我似乎无法通过类似第一个"a ++ b <> []"的子目标，即使我的上下文明确声明了" b <> []"。有什么建议吗？

我还查阅了很多现有的列表定理，除了一些子目标的app_nil_l和app_nil_r之外，没有找到什么特别有帮助的东西。

- Akhil

---

"应用 app_eq_nil 应该很有用。当你有一个目标“a <> b”时，你可以使用“intro”来展示“a = b”会导致矛盾。" - Boris

请问您能否展示一下您目前所拥有的证明脚本？ - Julien

Answer 1

从 destruct a 开始是一个很好的主意。

对于 a 是 Nil 的情况，你应该解构 (a <> [] \/ b <> []) 假设。有两种情况：

• 右侧假设 [] <> [] 是一个 矛盾，
• 左侧假设 b <> [] 是你的目标（因为 a = []）

对于 a 是 a :: a0 的情况，你应该像 Julien 说的那样使用 discriminate。

- Bruno

Answer 2

你以 destruct a 的方式开始是正确的。

你最终应该得到 a0::a++b<>0。它类似于 a++b<>0，但由于有一个 cons 存在，因此 discriminate 知道它与 nil 不同。

- Julien

Answer 3

首先，我不确定您使用的Coq版本是哪个，语法看起来确实很奇怪。其次，如果您不展示目前为止的证明，我们很难提供帮助。我应该说，您的策略似乎是正确的，您应该破坏两个列表，但最好先检查or以查看哪个列表不为空。

另一个选项是使用计算来展示您的引理，在这种情况下，相等性会进行计算，因此您将得到比较的结果。在这种情况下，仅需销毁一个列表即可，由于参数的顺序：

From mathcomp Require Import all_ssreflect.

Lemma not_empty (A : eqType) (a b : seq A) :
  [|| a != [::] | b != [::]] -> a ++ b != [::].
Proof. by case: a. Qed.

- ejgallego