Coq variable exists in list

Question

I have problem with proving existential variable in list. How can I prove something like this:

Lemma exists_in_list_helper: forall (X : Type) (a : X) (P : X -> Prop),
        (exists b : X, In b [a] -> P b) ->
        P a.
Proof.
Admitted.

I have another question. How can I do case analysis over the values in a list (if it exists in this part of the list or not)? This is the main lemma I'm proving. Any help appreciated:

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 <> [] /\ exists b : X, In b l -> P b) \/
        (P a /\ l <> [] /\ forall b : X, In b l -> ~ P b) \/
        (~ P a /\ l <> [] /\ exists b : X, In b l -> P b).
Proof. 

Thanks,

Answer 1

your first lemma doesn't seem probable: we know that there exists a b such that P b holds iff b \in [a]. However, we don't know if b \in [a] holds, so it seems difficult to prove. You can maybe see your statement as:

Lemma exists_in_list_helper (X : Type) (a : X) (P : X -> Prop) :
        (exists b : X, a = b -> P b) ->
        P a.

Then, it doesn't immediately follow that a = b. You may want a lemma such as:

Lemma in1 T (x y : T) : In x [y] <-> x = y.
Proof.
split; intros H.
+ now apply in_inv in H; case H.
+ now rewrite H; constructor.
Qed.

Regarding your second question, I am not sure I fully understand the intent of your lemma. Usually, one wants to have:

forall x l, x \in l \/ x \notin l

but this requires decidability for the equality over the type of x, see Lemma in_dec. If you split a list l in l1, l2, then it follows that:

x \in l1 ++ l2 <-> x \in l1 \/ x \in l2

which allows for case reasoning. More interesting facilities are given by math-comp's path.v, which allows to deduce in a convenient way:

x \in l -> { l1, l2 & l = l1 ++ [x] ++ l2 }

where { x & P x} is the Type version of exists x, P x.

Answer 2

For the first one, I'd say you might also need the fact that equality on X is decidable: either a = b and you can substitute, or a <> b and you get a contradiction, but you need to be able to perform such case analysis.

For the second one, you can remove the a :: l <> [] part, it is always true and doesn't give you anything. And I'm pretty sure you also need decidable equality too (for the same reasons).