Can Coq intros pattern split at the rightmost opportunity for conjunction?

Question

I am wondering if there is some intro pattern which can introduce A /\ B /\ C as

A, B, C: Prop
H1: A /\ B
H2: C

I'm aware that intros [H1 H2] will produce

A, B, C: Prop
H1: A
H2: B /\ C

but cannot figure out how to configure the brackets for the other direction. This is a trivial example; but I have a more complicated combination of conjunctions and disjunctions that I would much prefer to destruct from right to left.

Thanks,

Answer

The _ /\ _ notation in Coq is a right-associative binary operator, so A /\ B /\ C really stands for A /\ (B /\ C). If you want to build some A /\ B you should first fully decompose the /\ (intros [HA [HB HC]]., you can nest the patterns arbitrarily) and then build the A /\ B hypothesis (for instance using assert (A /\ B) as HAB by (split; [exact HA| exact HB]). or any other way you prefer to add an hypothesis).

In a more complex setting, you might want to write a lemma and_assoc : forall A B C, A /\ B /\ C -> (A /\ B) /\ C and use a view-pattern. Starting from a goal A /\ B /\ C -> P you can use intros [HAB HC]%and_assoc. to obtain HAB : A /\ B and HC : C : the pat%and_assoc part says that and_assoc should be applied first to the top assumption and then further destructed with pat.