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 <> [])假说.将有两种情况:

• 正确的假设[] <> []是contradiction,
• 左边的,假设b <> []是你的目标(因为a = [])

对于这里的情况a是a :: a0,你应该使用discriminate的朱利安说.

Answer 2

你以正确的方式开始了 destruct a.

你应该在某个时候结束a0::a++b<>0.它具有重复性,a++b<>0但它与你在cons 这里完全不同,因此discriminate 知道它与之不同nil.