小编Akh*_*hil的帖子

我试图在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,对于某些子目标).