Search code examples
coq

disjunction of empty and non-empty list in coq

I'm new in Coq. How can I prove the disjunction of empty and non-empty list is true?

l = [] \/ l <> []

This is the lemma I'm working on:

Lemma in_list: forall (X : Type) (a : X) l (P : X -> Prop),
        (a :: l <> [] /\ exists b : X, In b (a :: l) -> P b) ->

  (P a /\ l = [] \/
P a /\ l <> [] \/ ~ P a /\ l <> [] /\ (exists b : X, In b l -> P b))

So for proving the lemma one way seems to be considering two cases:

if l = [] or l <> []

Then

if l = [], P a holds

and

if l <> [], ~ P a /\ l <> [] /\ (exists b : X, In b l -> P b) holds

I can prove the lemma this way but I don't know how to go this way. I have done something similar for Prop type (not a list) like this for Variable R of type Prop which considers two cases of True or False. I'm not sure if I can do something similar for list.

destruct (classic R) as [r | rn].

Thanks,

Solution

  • You already know about:

    destruct (classic R) as [r | rn].

    It can be used with any R : Prop and it relies internally on the excluded-middle axiom.

    One simpler version exists where no axiom is needed because you already know that the object can be only of several forms:

    destruct l.

    where l is your list here, but it could be a natural number as well or a proof of a disjunction...