CODEWITHSUNDEEP
coq
saeed M
saeed M

Reputation: 21

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,

Upvotes: 0

Views: 864

Answers (2)

Zimm i48
Zimm i48

Reputation: 3081

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

Upvotes: 0

Vinz
Vinz

Reputation: 6057

This is a very basic question, which looks like question 1 of a home assignment, so I would advise you to:

  • think about it on paper: how would you prove that with pen & paper ?
  • what tactics do you know, which one could apply here ?
  • as @anton said, at least explain us what you tried and what failed

Upvotes: 1

Related Questions