リストにCoq変数があります

Question

リストに存在する変数を証明することに問題があります。

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. 

私は別の質問があります。リスト内の値に対してケース分析を行うには（リストのこの部分に存在するかどうか）これが私が証明している主題です。すべてのヘルプ感謝：a = bとあなたは置き換えることができ、またはa <> bとあなたのどちらか：

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. 

おかげで、最初のもののために

Answer 1

あなたの最初の補題は当てはまりそうではありません.がb \in [a]となるようにbが存在することがわかります。しかし、b \in [a]が成立しているかどうかは分かりませんので、証明するのは難しいようです。

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

その後、それはすぐにa = bことに従っていません：としてあなたは多分あなたの文を参照してくださいすることができます。あなたの2番目の質問については

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. 

、私は完全にあなたの補題の意図を理解していないです：あなたは補題のような場合があります。

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

が、これは補題in_decを参照してください、xの種類以上の平等のための決定可能性を必要とする：通常、一つは持っていたいです。

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

場合の推論を可能にする：あなたはl1, l2にリストlを分割した場合、ということになります。

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

{ x & P x}がexists x, P xのTypeバージョンである：より興味深い施設は便利な方法で推定することができます数学-COMPのpath.v、で与えられます。

Answer 2

は、私はあなたにもX上の平等が決定可能であるという事実が必要になる場合がありますでしょうね矛盾を起こしますが、そのようなケース分析を実行できる必要があります。

a :: l <> []部分を削除することができます。これは常に真であり、何も与えません。そして、私はあなたにも決定的な平等が必要であると確信しています（同じ理由で）。