how to figure out what "=" means in different types in coq

Question

Given a type (like List) in Coq, how do I figure out what the equality symbol "=" mean in that type? What commands should I type to figure out the definition?

Answer 1

The equality symbol is just special infix syntax for the eq predicate. Perhaps surprisingly, it is defined the same way for every type, and we can even ask Coq to print it for us:

Print eq.
(* Answer: *)
Inductive eq (A : Type) (x : A) : Prop :=
| eq_refl : eq x x.

This definition is so minimal that it might be hard to understand what is going on. Roughly speaking, it says that the most basic way to show that two expressions are equal is by reflexivity -- that is, when they are exactly the same. For instance, we can use eq_refl to prove that 5 = 5 or [4] = [4]:

Check eq_refl : 5 = 5.
Check eq_refl : [4] = [4].

There is more to this definition than meets the eye. First, Coq considers any two expressions that are equalivalent up to simplification to be equal. In these cases, we can use eq_refl to show that they are equal as well. For instance:

Check eq_refl : 2 + 2 = 4.

This works because Coq knows the definition of addition on the natural numbers and is able to mechanically simplify the expression 2 + 2 until it arrives at 4.

Furthermore, the above definition tells us how to use an equality to prove other facts. Because of the way inductive types work in Coq, we can show the following result:

eq_elim : 
  forall (A : Type) (x y : A),
    x = y ->
    forall (P : A -> Prop), P x -> P y

Paraphrasing, when two things are equal, any fact that holds of the first one also holds of the second one. This principle is roughly what Coq uses under the hood when you invoke the rewrite tactic.

Finally, equality interacts with other types in interesting ways. You asked what the definition of equality for list was. We can show that the following lemmas are valid:

forall A (x1 x2 : A) (l1 l2 : list A),
  x1 :: l1 = x2 :: l2 -> x1 = x2 /\ l1 = l2

forall A (x : A) (l : list A),
  x :: l <> nil.

In words:

1. if two nonempty lists are equal, then their heads and tails are equal;

2. a nonempty list is different from nil.

More generally, if T is an inductive type, we can show that:

1. if two expressions starting with the same constructor are equal, then their arguments are equal (that is, constructors are injective); and

2. two expressions starting with different constructors are always different (that is, different constructors are disjoint).

These facts are not, strictly speaking, part of the definition of equality, but rather consequences of the way inductive types work in Coq. Unfortunately, it doesn't work as well for other kinds of types in Coq; in particular, the notion of equality for functions in Coq is not very useful, unless you are willing to add extra axioms into the theory.