我正在尝试在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之外,没有找到什么特别有帮助的东西。