Beispiel für die Einführung Muster (p1 & ... & pn) funktioniert nicht

Question

Ich lese das Coq (8.5p1) Referenzhandbuch,

introduction via (p1 & ... & pn) is a shortcut for introduction via (p1,(...,(...,pn)...)); it expects the hypothesis to be a sequence of right-associative binary inductive constructors such as conj or ex_intro; for instance, an hypothesis with type A/(exists x, B/\C/\D) can be introduced via pattern (a & x & b & c & d);

Der Versuch, dies heraus zu testen, habe ich:

Goal forall A B C D: Prop, A/\(exists x:nat, B/\C/\D) -> D. 
intros (a & x & b & c & d). 

Aber Coq ist mir zu sagen:

Error: Not an inductive product.

Und ich habe den gleichen Fehler für einige andere Varianten, wie man ohne die -> D.

Kann jemand bitte erklären, was die richtige Verwendung ist (in einem hoffentlich nützlichen Beispiel)?

Answer 1

Da Ihr Ziel mit forall A B C D: Prop, beginnt müssen Sie einführen A B C D zuerst:

intros A B C D (a & x & b & c & d). 

Ich denke, diese Syntax eingeführt wurde von verschachtelten eckigen Klammern, um loszuwerden, die verwendet werden können, während der Einführungsphase destrukturiert. Vergleichen Sie die folgenden zwei Beweise:

Goal forall A B C D: Prop, 
    A /\ (exists x:nat, B /\ C /\ D) -> D. 
intros A B C D (_ & _ & _ & _ & d). assumption. Qed. 

Goal forall A B C D: Prop, 
    A /\ (exists x:nat, B /\ C /\ D) -> D. 
intros A B C D [_ [_ [_ [_ d]]]]. assumption. Qed. 

Ich denke, die erste ist einfacher auf die Augen.