How do I convince coq that (A/\B)/\C == A /\ B /\ C?

Question

In my proof I stumble upon problems where there is an A /\ B /\ C in my assumptions, and I need to prove (A /\ B) /\ C. These are logically exactly the same, but coq won't solve these with assumption..

I have been solving these by applying an axiom, but is there a more elegant (and correct) way to handle this?

Answer 1

So the way I've gone about it is by defining my lemma,

Lemma conj_assoc : forall A B C, A /\ (B /\ C) <-> (A /\ B) /\ C.

That is one implies the other.

intros. split. will then split this into two goals.

1. A /\ (B /\ C) -> (A /\ B) /\ C
2. (A /\ B) /\ C -> A /\ (B /\ C)

Proving each of these is roughly the same. For (1),

• intro Habc. to get the assumption from the left hand size.
• destruct Habc as [Ha Hbc]. destruct Hbc as [Hb Hc]. to get the individual assumptions.
• auto to use these assumptions.

I leave it to you to work out (2) but it is very similar.

Then Qed.