例は

Question

私はコック（8.5p1）リファレンスマニュアルを読んでいる、

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

はこれをテストするためにしようと動作しません、私がやった：

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

しかし、Coqのは、私に言っている：

Error: Not an inductive product.

そして私は、そのような-> Dないものとして、いくつかの他の変種のために同じエラーを得ました。

正しい使い方（うまくいけば便利な例）を教えてください。あなたの目標はforall A B C D: Prop,から始まるので

Answer 1

最初A B C Dを導入する必要があります。

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

私はこの構文は、導入フェーズでdestructureするために使用することができネストされた角括弧、取り除くために導入されたと思います。次の2つの証明を比較してください：

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. 

私は最初のものは目が簡単だと思います。