リスト内のすべての要素を証明する

Question

リストのすべての要素でHと目標が同じであることを証明するにはどうすればよいですか？

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 

二つの文~ (In n l /\ ~ P n)とIn b l -> P bは等しいです。私はapply imply_to_orを単純化することを目標に試みましたが、統一できませんでした。 "後方"

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

我々の理由目標に補題を適用する：

おかげで、すべての

Answer 1

まず、我々はいくつかの輸入を必要とします。 これは、結果として暗黙の意味を持つ補題が必要であることを意味します。ではなく、 premissです。

我々はそれのためSearch (~ ?p \/ ?c -> ?p -> ?c).ことができ、これは取得しますあなた：

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

上記の補題は動作しますが、私たちは少しでも良いの操作を行うことができます、あなたを私たちはtauto戦術を利用することができ、出来上がり

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.