What is eq_rect and where is it defined in Coq?

Question

From what I have read, eq_rect and equality seem deeply interlinked. Weirdly, I'm not able to find a definition on the manual for it.

Where does it come from, and what does it state?

Answer 1

If you use Locate eq_rect you will find that eq_rect is located in Coq.Init.Logic, but if you look in that file there is no eq_rect in it. So, what's going on?

When you define an inductive type, Coq in many cases automatically generates 3 induction principles for you, appending _rect, _rec, _ind to the name of the type.

To understand what eq_rect means you need its type,

Check eq_rect.

here we go:

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

and you need to understand the notion of Leibniz's equality:

Leibniz characterized the notion of equality as follows: Given any x and y, x = y if and only if, given any predicate P, P(x) if and only if P(y).

In this law, "P(x) if and only if P(y)" can be weakened to "P(x) if P(y)"; the modified law is equivalent to the original, since a statement that applies to "any x and y" applies just as well to "any y and x".

Speaking less formally, the above quotation says that if x and y are equal, their "behavior" for every predicate is the same.

To see more clearly that Leibniz's equality directly corresponds to eq_rect we can rearrange the order of parameters of eq_rect into the following equivalent formulation:

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