CODEWITHSUNDEEP
coq
Lepticed
Lepticed

Reputation: 381

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?

Upvotes: 1

Views: 302

Answers (2)

Meven Lennon-Bertrand
Meven Lennon-Bertrand

Reputation: 1296

You can make the symmetry tactic work for any relation… as long as you show first that it is symmetric. This is done in the standard library for equality (which is why symmetry works for it out of the box), but not for and. So if you want to use it, you have to do it yourself, like so:

Require Import RelationClasses.

Instance and_comm : Symmetric and.
Proof.
  intros A B [].
  now split.
Qed.

The RelationClasses module of the standard library declares the Symmetric typeclass, which is used by Coq when you call the symmetry tactic. Next we prove that and is indeed symmetric, and declare this as an instance of the Symmetric class. Once this is done, symmetry works as you expect it to.

Upvotes: 4

Rupert Swarbrick
Rupert Swarbrick

Reputation: 2803

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.

Upvotes: 2

Related Questions