coq中的空列表和非空列表的分離

我是Coq中的新手。我如何證明空列表和非空列表的分離是真實的？coq中的空列表和非空列表的分離

l = [] \/ l <> []

這是我工作的引理：

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

所以爲了證明引理的一種方式似乎要考慮兩種情況：

if l = [] or l <> []

然後

if l = [], P a holds

and

if l <> [], ~ P a /\ l <> [] /\ (exists b : X, In b l -> P b) holds

我可以用這種方法證明這個引理，但我不知道如何去這樣。對於類型爲Prop的變量R，我爲Prop類型（不是列表）做了類似的事情，它考慮兩種True或False情況。我不確定我是否可以爲列表做類似的事情。

destruct (classic R) as [r | rn].

感謝，

來源

2016-09-20 saeed M

對不起，沒有完全澄清問題。我編輯了我的問題。 –

這個'in_list'引理似乎不可證明。 '如果l = []，P持有'是不可證明的，因爲在前提中根本沒有足夠的信息（我的意思是'In x [a] - > P x'（對於某些'x'）似乎沒有在'x <> a'時是有用的）。你能說明應該使用'in_list'的問題嗎？ –

在我的假設（存在...）中，如果列表l是[]，那麼列表中必須有一個元素，它必須是P a保持的'a'。 –

你已經知道了：

destruct (classic R) as [r | rn].

它可以與任何R : Prop使用，並且它的內部排除依賴中等公理。

一個簡單的版本存在不需要公理在那裏，因爲你已經知道，對象只能是幾種形式：

destruct l.

其中l是你的列表在這裏，但它可能是一個自然數，以及或脫離的證據...

來源

2016-09-21 08:54:06

這是一個非常基本的問題，它看起來像一個家庭作業的問題1，所以我會建議你：

想想在紙上：如何你會用筆&紙證明嗎？
你知道什麼策略，哪一個可以在這裏適用？
爲@anton說，至少說明我們你嘗試過什麼，什麼失敗

來源

2016-09-20 07:01:16 Vinz

抱歉沒有完全澄清問題。我編輯了我的問題。 –

coq中的空列表和非空列表的分離

回答

相關問題