CODEWITHSUNDEEP
coq
saeed M
saeed M

Reputation: 21

Proving for all elements of a list in coq

How can I prove that H and my goal are same for all elements of the list?

X : Type
P : X -> Prop
l : list X
H : forall n : X, ~ (In n l /\ ~ P n)
______________________________________(1/1)
forall b : X, In b l -> P b

The two statements ~ (In n l /\ ~ P n) and In b l -> P b are equal. I tried apply imply_to_or on the goal to simplify but couldn't unify.

Thanks,

Upvotes: 0

Views: 1091

Answers (1)

Anton Trunov
Anton Trunov

Reputation: 15424

First of all, we need some imports:

Require Import Coq.Logic.Classical_Prop.
Require Import Coq.Lists.List.

We reason "backwards" when applying lemmas to the goal. This means you need a lemma that has implication as its consequent, not premiss.

We can Search (~ ?p \/ ?c -> ?p -> ?c). for it and this will get you:

or_to_imply: forall P Q : Prop, ~ P \/ Q -> P -> Q

The above lemma will work, but we can do a little bit better: we can make use of the tauto tactic, and voilà, you have a simple proof:

Goal forall (X : Type) (P : X -> Prop) (l : list X),
       (forall n, ~ (In n l /\ ~ P n)) ->
       forall b, In b l -> P b.
  intros X P l H b.
  specialize H with b.
  tauto.
Qed.

Upvotes: 2

Related Questions