Nachweis für alle Elemente einer Liste in Coq

Wie kann ich beweisen, dass H und mein Ziel für alle Elemente der Liste gleich sind?Nachweis für alle Elemente einer Liste in Coq

X : Type 
P : X -> Prop 
l : list X 
H : forall n : X, ~ (In n l /\ ~ P n) 
______________________________________(1/1) 
forall b : X, In b l -> P b

Die beiden Aussagen ~ (In n l /\ ~ P n) und In b l -> P b sind gleich. Ich versuchte apply imply_to_or auf das Ziel zu vereinfachen, konnte aber nicht vereinheitlichen.

Danke,

Quelle

2016-09-23 saeed M

Sind Sie sicher, dass dies konstruktiv wahr ist? – jbapple

Es wäre besser, wenn Sie Ihre Importe und die tatsächliche Aussage zur Verfügung stellen, was Sie versuchen zu beweisen ([mcve]). (1) Es wird uns ein wenig Tipparbeit ersparen. (2) Es wird uns sagen, dass Sie im Bereich der klassischen Logik arbeiten. Ich denke auch, was immer Sie über Listen beweisen, kann mit konstruktiver Logik bewiesen werden. (Ich meine auf breiter Ebene, nicht dieses Beispiel). –

Zunächst einmal müssen wir einige Importe:

Require Import Coq.Logic.Classical_Prop. 
Require Import Coq.Lists.List.

Wir Grund "rückwärts", wenn Lemmata, um das Ziel der Anwendung. Dies bedeutet, dass Sie ein Lemma benötigen, das eine Implikation als Konsequenz hat, nicht Prämisse.

können wir Search (~ ?p \/ ?c -> ?p -> ?c). für sich und diese erhalten Sie:

or_to_imply: forall P Q : Prop, ~ P \/ Q -> P -> Q

Die obige Lemma funktionieren wird, aber wir können ein wenig besser machen: Können wir die Verwendung der tauto Taktik machen, und voilà, Sie habe einen einfachen Beweis:

Goal forall (X : Type) (P : X -> Prop) (l : list X), 
     (forall n, ~ (In n l /\ ~ P n)) -> 
     forall b, In b l -> P b. 
    intros X P l H b. 
    specialize H with b. 
    tauto. 
Qed.

Quelle

2016-09-23 05:54:10

Nachweis für alle Elemente einer Liste in Coq

Antwort

Verwandte Themen