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?