example for introduction pattern (p1 & ... & pn) does not work

1
votes

I am reading the Coq (8.5p1) reference manual,

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

Trying to test this out, I did:

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

But Coq is telling me:

Error: Not an inductive product.

And I got the same error for a few other variants, such as one without the -> D.

Can some one please explain what's the correct usage (in a hopefully useful example)?

1
coq

1 Answers

3
votes

Since your goal starts with forall A B C D: Prop, you need to introduce A B C D first:

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

I think this syntax was introduced to get rid of nested square brackets, which can be used to destructure during the introduction phase. Compare the following two proofs:

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.

I think the first one is easier on eyes.