Coq變量存在於列表中

-3

我在驗證列表中的存在變量時遇到了問題。我怎麼能證明這樣的事情：Coq變量存在於列表中

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.

我還有一個問題。我如何對列表中的值進行個案分析（如果它存在於列表的這部分中）？這是我證明的主要引理。任何幫助表示讚賞：

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.

感謝，

來源

2016-09-15 saeed M

你的第一個引理似乎不太可能：我們知道存在一個b，使得P b成立iff b \in [a]。但是，我們不知道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。你可能需要一個引理如：

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

但這需要可判定爲超過x類型的平等，見引理in_dec。如果您在l1, l2拆分列表l，那麼它遵循：

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

它允許情況下的推理。

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

其中{ x & P x}是Type版本的exists x, P x：更有趣的設施，通過數學補償的path.v，它允許在一個方便的方式來推斷給出。

來源

2016-09-16 07:21:27 ejgallego

謝謝你的回答。我有另一個問題。在使用apply時出現「Impossible to Unify」錯誤。我已經看到我們可以使用'模式'策略，但我無法正確使用它。我已經證明如下：〜（存在b：X，In b l - > P b） - > （全部b：X，In b l→P b）。 –

並希望將我的目標中的所有表達式更改爲〜exists .... –

我使用了模式（forall b：X，In bl - >〜P b），它產生了'有趣'但又無法使用申請my_lemma替換所有〜存在......你能幫助我如何正確使用模式來指導應用策略嗎？ –

-1

對於第一個，我說你可能也需要這樣一個事實：X平等是可判定：要麼a = b並且可以替代，或a <> b你得到一個矛盾，但你需要能夠進行這種案例分析。

對於第二個，你可以刪除a :: l <> []部分，它永遠是真的，並沒有給你任何東西。我敢肯定，你也需要可判斷的平等（出於同樣的原因）。

來源

2016-09-16 07:08:16 Vinz

Coq變量存在於列表中

回答

相關問題