Disjunktion der leeren und nicht leeren Liste in Coq

Question

Ich bin neu in Coq. Wie kann ich beweisen, dass die Trennung von leerer und nicht leerer Liste wahr ist?

l = [] \/ l <> [] 

Dies ist das Lemma Ich arbeite an:

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

Also das Lemma eine Möglichkeit zu beweisen, scheint zwei Fälle in Betracht ziehen:

if l = [] or l <> [] 

Dann

if l = [], P a holds 

und

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

Ich kann das Lemma auf diese Weise beweisen, aber ich weiß nicht, wie ich diesen Weg gehen soll. Ich habe etwas Ähnliches für Prop-Typ (keine Liste) wie folgt für Variable R vom Typ Prop gemacht, die zwei Fälle von True oder False berücksichtigt. Ich bin mir nicht sicher, ob ich etwas ähnliches für die Liste machen kann.

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

Danke,

Answer 1

Sie bereits kennen:

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

kann es mit jedem R : Prop verwendet werden, und es verlässt sich intern auf dem ausgeschlossenen -Mittelaxiom.

Eine einfachere Version vorhanden ist, wo kein Axiom ist erforderlich, da Sie bereits wissen, dass das Objekt nur von mehreren Formen annehmen kann:

destruct l. 

wo l Ihre Liste ist hier, aber es könnte auch eine natürliche Zahl sein oder ein Beweis für eine Disjunktion ...

Answer 2

Dies ist eine sehr grundlegende Frage, die wie Frage 1 von einer Hausarbeit aussieht, so würde ich Ihnen raten:

• darüber nachdenken, es auf dem Papier: wie Würden Sie das mit Stift & Papier beweisen?
• Welche Taktik kennen Sie, welche könnte man hier anwenden?
• als @anton sagte, zumindest erklären Sie uns, was Sie versucht haben und was fehlgeschlagen