I am just starting with Coq and right now trying to prove some stuff that is in "The Little Prover". One of the theorems I came across is the following:
Theorem equal_swap : forall (A: Type) (x:A) (y:A),
(x = y) = (y = x).
However, I am unable to prove this. I tried finding out how to rewrite the right side of the equation with eq_sym, but I am unable to apply it to only one expression of the goal.
How would I go about proving this theorem?
One thing that Coq uses pervasively is the concept of "propositions as types". Intuitively, types are collections of objects. So what are the elements of these collections? They are proofs. A proposition that is provable is a type that contains an element, a proposition that is not provable is a type that does not contain a proof.
So a = b is a type, a type of proofs and b = a is also a type of proofs but they don't prove the same statement. The purpose of the logic in Coq is to be very precise about statements. Can we say that a = b and b = a are the same? Well, in a sense they are not. If I have a goal of the form C(a, b) and I rewrite with a proof of a = b then I obtain C(a, a) and if I rewrite with a proof of b = a then I obtain C(b, b) and these two don't look the same. One make argue that they are the same (because a and b are the same by assumption) but one may also argue that they are not the same (because you don't use them in the same manner).
When designing a logical system like Coq, it turns out that you can do a lot of logic even if you don't try to talk about equality between propositions, but concentrate yourself on just using equivalence between propositions. So people tried to add the least amount of properties to the concept of equality. In particular, equality between types was left naked. You will see that equality is practical to use when talking about equality between first-order data, it is less convenient when talking about higher-order data (like equality between functions), and it is awkward when talking about equality between types.
On the other hand, if they want to study the relation between two propositions, they only try to check whether one proposition implies another one, and if they want to be more precise, they try to see if they imply each other mutually. For most practical purposes this will be enough, and I suggest you stick to this discipline as long as you consider yourself a beginner.
Here, we may want to prove a = b -> b = a. If we do this as a proof using tactics, then intro will help us give a name to a = b (say H) and rewrite H will help us transform b = a into a = a. Now the last proof can be done by reflexivity. But when I say transform b = a into a = a. I only mean that a = a -> b = a has a proof, in other words "there is a function, when given as input a proof of a = a, it produces as output a proof of b = a. When performing a proof, we have the impression that the proof of a = a is transformed into a proof of b = a while staying the same, but it is not: two different proofs are observed here.
In the end, (a = b) <-> (b = a) is just the conjunction of (a = b) -> (b = a) and (b = a) -> (a = b). The rewrite tactic has also been extended so that you can also rewrite with a theorem is an equivalence, instead of an equality.
<->version. – ejgallego(x == y) = (y == x)or(x = y) <-> (y = x), both proofs are easy and can be done with standard tactics. [a == b is the boolean version of eq] – ejgallego