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).

Repatriate

"apply app_eq_nil" should be useful. When you have a goal "a <> b" you can use "intro" to show that "a = b" lead to a contradiction. – Pernik

Could you please show us the proof script you have so far. – Easing

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.

Simonsimona

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.

Easing

Answer 3

first, I am not sure which Coq version you are using, the syntax certainly looks odd. Seconds, it is hard for us to help if you don't show us the proof you have so far. I should say that indeed your strategy seems correct, you should destruct both lists, tho it is better if you first inspect the or to see which list is not empty.

Another option is to use computation to show your lemma, in this case, equality will compute and thus you will get the result of the comparison. It suffices to destroy only one list in this case due the order or arguments:

From mathcomp Require Import all_ssreflect.

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

Hark