Subsets der Liste nat in coq

Question

definiert ich eine rekursive Funktion für alle Teilmengen von nat_list in coq als

Fixpoint subsets (a: list nat) : (list (list nat)) := 
match a with 
    |[] => [[]] 
    |h::t => subsets t ++ map (app [h]) (subsets t) 
end. 

Ich versuche zu beweisen, dass

forall (a:list nat), In [] (subsets a). 

ich auf ein induct versucht. Der Basisfall war geradlinig. Im Induktionsfall habe ich versucht, den eingebauten Satz in_app_or zu verwenden.

Unable to unify "In ?M1396 ?M1394 \/ In ?M1396 ?M1395" with 
"(fix In (a : list nat) (l : list (list nat)) {struct l} : Prop := 

match l with 
| [] => False 
| b :: m => b = a \/ In a m  
end)               
[] (subsets t ++ map (fun m : list nat => h :: m) (subsets t))". 

Wie beweisen, dass ich einen solchen Satz oder umgehen so ein Problem?

Answer 1

Das Problem mit in_app_or ist, dass der folgende Typ, hat:

forall (A : Type) (l m : list A) (a : A), 
    In a (l ++ m) -> In a l \/ In a m 

und Anwendung von Lemmata zu dem Ziel Werken „rückwärts“: Coq paßt die konsequenten B der Implikation A -> B mit dem Ziel, und wenn Sie können vereinheitlicht werden, Sie haben ein neues Ziel: Sie müssen eine (stärkere) Aussage beweisen A. Und in Ihrem Fall die A und B sind in der falschen Reihenfolge (vertauscht), so müssen Sie in_or_app stattdessen anwenden:

in_or_app : forall (A : Type) (l m : list A) (a : A), 
    In a l \/ In a m -> In a (l ++ m) 

Dies ist, wie Ihr Ziel nachgewiesen werden kann, mit in_or_app:

Goal forall (a:list nat), In [] (subsets a). 
    intros. 
    induction a; simpl; auto. 
    apply in_or_app; auto. 
Qed.