Coq中的非空列表附加定理

Question

我试图证明Coq中的以下引理：

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

现在，我目前的策略是对进行析取，在打破析取之后，我可以理想地声明，如果<>[]则a++b也必须是<>[]。。。这就是我的计划，但我似乎无法通过一个类似于第一个"a++b<>[]"的子目标，即使我的上下文明确表示"b<>[]"。有什么建议吗？

我还研究了很多预先存在的列表定理，没有发现任何特别有用的东西(对于一些子目标，减去app_nil_l和app_nil_r(。

Answer 1

从destruct a开始确实是个好主意。

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

• 右边的假设CCD_ 5是CCD_
• 左边的假设b <> []是你的目标(因为a = [](

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

Answer 2

您以正确的方式开始使用destruct a。

您应该在某个时刻使用a0::a++b<>0。它重新汇编了a++b<>0，但它非常不同，因为这里有一个cons，因此discriminate知道它与nil不同。

Answer 3

首先，我不确定您使用的是哪个Coq版本，语法看起来肯定很奇怪。几秒钟后，如果你不向我们展示你迄今为止的证据，我们很难提供帮助。我应该说，事实上，你的策略似乎是正确的，你应该销毁这两个列表，但最好先检查或看看哪个列表不是空的。

另一种选择是使用计算来显示引理，在这种情况下，等式将进行计算，因此您将得到比较的结果。在这种情况下，由于顺序或参数的原因，只销毁一个列表就足够了：

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