空で空でないリストとcoqの論理和

Question

私は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)) 

ので補題を証明する一つの方法は、2つのケースを考慮しているようだ：

if l = [] or l <> [] 

その後

if l = [], P a holds 

および

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

私はこのように補題を証明することができますが、私はこのようにする方法を知らない。私はProp型の変数R（TrueまたはFalseの2つのケースを考慮する）のように、Prop型（リストではない）と同様のことをしました。私はリストに似たようなことができるかどうかはわかりません。

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

おかげで、

Answer 1

を失敗した何をしようとしたものを私たちに説明し、言ったように：

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

それはどんなR : Propで使用することができ、それは除外に内部的に依存しています-middle axiom。

すでにオブジェクトが唯一のいくつかの形式のものとすることができることを知っているので、何の公理が必要とされていない場所の一つ簡単なバージョンが存在する：

lここにあなたのリストであるが、それは同様の自然数である可能性があり

destruct l. 

または離婚の証明...

Answer 2

これは、家庭の割り当ての問題1のように見える非常に基本的な質問ですので、私はあなたを助言する：

• は、紙の上にそれについて考える：どのようにあなたはペンでそれを証明するでしょう&紙？
• ここではどのような戦術を知っていますか？
• @antonは、少なくともあなたが既に知っている