Non-empty list append theorem in Coq

Question

I am trying to prove the following lemma in Coq:

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

Right now my current strategy was to destruct on a, and after breaking the disjunction I could ideally just state that if a <> [] then a ++ b must also be <> []... That was the plan, but I can't seem to get past a subgoal that resembles the first " a ++ b <> []", even when my context clearly states that " b <> []". Any advice?

I've also looked through a lot of the pre-existing list theorems and haven't found anything particularly helpful (minus app_nil_l and app_nil_r, for some subgoals).

Answer 1

Starting with destruct a is a good idea indeed.

For the case where a is Nil, you should destruct the (a <> [] \/ b <> []) hypothesis. There will be two cases:

• the right one the hypothesis [] <> [] is a contradiction,
• the left one, the hypothesis b <> [] is your goal (since a = [])

For the case where a is a :: a0, you should use discriminate as Julien said.

Answer 2

You started the right way with your destruct a.

You should end up at some point with a0::a++b<>0. It ressembles a++b<>0 but it is quite different as you have a cons here, thus discriminate knows that it is different from nil.