Search code examples
coq

Using the commutativity of the AND operator in Coq

I’m trying to prove something in Coq using the commutativity of the logic AND operator. I coded this short example:

Axiom ax1 : A /\ B.
Theorem th1 : B /\ A.
Proof.
  pose proof (ax1) as H.
  symmetry.
  apply H.
Qed.

I use axiom (ax1) in my proof, and I get stuck on the symmetry command. This is my current goal:

1 subgoal
H : A /\ B
______________________________________(1/1)
B /\ A

When I use the symmetry command, I get the following error:

Tactic failure:  The relation and is not a declared symmetric relation. Maybe you need to require the Coq.Classes.RelationClasses library.

My current solution is to destruct hypothesis H, split the goal, and apply the right sub-hypothesis to the right subgoal. It takes a lot of space and is a bit frustrating to not be able to use AND commutativity.

So I’ve some questions: is symmetry the right command to use with a commutative relation? If yes, how can I fix my code for it to work? If not, is there a way to use the commutativity of the AND operator?

Solution

  • The symmetry tactic is specifically for reasoning about equalities (a = b iff b = a).

    I don't know of general machinery for commutative operators, but you can find the lemma you need with something like this:

    Search _ (?a /\ ?b <-> ?b /\ ?a)

    (I cheated: originally, I used -> and only switched to <-> when that didn't find anything!)

    There's exactly one lemma of this form in the base library and it's called and_comm. You should be able to solve your remaining proof obligation with it: apply and_comm.