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

Question

In my proof, I come across problems when there is A /\ B /\ C in my assumptions, and I need to prove (A /\ B) /\ C They are logically the same, but coq does not solve them with assumption. .

I solved them using the axiom, but is there a more elegant (and correct) way to handle this?

Answer 1

So, as I did, this is the definition of my lemma,

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

This one means the other.

intros. split. will divide it into two goals.

• A /\ (B /\ C) -> (A /\ B) /\ C
• (A /\ B) /\ C -> A /\ (B /\ C)

The proof of each of them is about the same. For (1),

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

I leave this to you for development (2), but it is very similar.

Then Qed.

Answer 2

If you have A /\ B /\ C as an assumption and your target is (A /\ B) /\ C , you can use tauto tactics. This tactic solves all tautologies in the propositional calculus. There is a firstorder tactic that can resolve some formulas with quantifiers.

If you have A /\ B /\ C and you want to pass (A /\ B) /\ C as an argument to the lemma, you will need to work a little. One way is to set (A /\ B) /\ C as an intermediate target and prove it:

 assert ((A /\ B) /\ C). tauto. 

If A , B and C are big expressions, you can use complex tactics to match hypothesis H : A /\ B /\ C and apply tauto tactics to it. This is a difficult approach, superfluous in this case, but useful in more complex situations, when you want to automate the proof with many similar cases.

 match type of H with ?x /\ ?y /\ ?z => assert (x /\ (y /\ z)); [tauto | clear H] end. 

There is an easier way, which is to apply the well-known lemma that performs the transformation.

 apply and_assoc in H. 

You can find the lemma by looking at the library documentation. You can also find it. This is not the easiest lemma for searching, because equivalence and search tools are focused on consequences and equalities. You can use SearchPattern (_ /\ _ /\ _). to search for lemmas of the form forall x1 … xn, ?A /\ ?B /\ ?C (where ?A ?B and ?C can be any expression). You can use SearchRewrite (_ /\ _ /\ _) to search for lemmas of the form forall x1 … xn, (?A /\ ?B /\ ?C) = ?D Unfortunately, this does not find what we need, which is a lemma of the form forall x1 … xn, (?A /\ ?B /\ ?C) <-> ?D What works

 Coq < SearchPattern (_ <-> (_ /\ _ /\ _)) and_assoc: forall ABC : Prop, (A /\ B) /\ C <-> A /\ B /\ C 

Answer 3

As a general tip, if you have something like this that you suspect to be obvious, check out the standard library. Here's how: Locate "/\". creates an answer that Notation allows for us,

 Notation Scope "A /\ B" := and AB : type_scope (default interpretation) 

Now we can issue the SearchAbout and. command SearchAbout and. to see what is in scope and find that and_assoc is a witness to the implication you are interested in. In fact, you can take a hint from your intuition: intuition tactics can take advantage of this implication on its own.

 Lemma conj_example : forall ABCD, (A /\ B) /\ C -> (A /\ (B /\ C) -> D) -> D. Proof. intuition. Qed.