In the pattern-matching, Coq does know that x, y andz "are the same", but the way this work is relatively basic. The full syntax for pattern-matching (on an equality) is (roughly)
match s in x == y return P with
| eq_refl z => t
end
and the rule for typing it says that
s should have some type a == b where a and b are of type AP should be a type (ie of type Prop, Set or Type), it is allowed to mention the variables x, y : At should have type P[z/x,z/y]- when all the previous hold, the whole pattern-matching has type
P[a/x,b/y]
The fact that in 3. x and y are substituted by z is what corresponds to "knowing that x, y and z are the same".
However, note that this only applies when typing the term t. In particular, variables which are already in context, like Px in your first example, do not get altered. This is why your first example does not type-check: Px has type P x while in the branch you should give a term of type P z. The error message is quite confusing because Coq tries to guess what the P in the return above should be, but it gets lost. You can get a better error message by giving P explicitly:
Fail Definition equality__leibniz_equality_term : forall (X : Type) (x y: X),
x == y -> forall P : (X -> Prop), P x -> P y :=
fun X x y H P Px=>
match H in x' == y' return P x' with
| eq_refl z => Px
end.
(* The term "Px" has type "P x" while it is expected to have type "P z". *)
In your second example, though, you do not introduce Px right away. Thus, its type is part of P, and get updated in the branch, where the identity function does the trick. We can be more explicit, as above:
Definition equality__leibniz_equality_term : forall (X : Type) (x y: X),
x == y -> forall P : (X -> Prop), P x -> P y :=
fun X x y H P=>
match H in x' == y' return P x' -> P y' with
| eq_refl z => fun Px => Px
end.
By step 3. above, we see that fun Px => Px must now be of type P z -> P z,
which the identity type has. And looking at step 4., the whole pattern-matching has type P x -> P y, as expected. Coq is smart enough to figure this out, so in practice you do not need to give the return or in clauses explicitly.
There is a third solution, which works even if you already introduced a variable: generalization. This works as follows:
Definition equality__leibniz_equality_term : forall (X : Type) (x y: X),
x == y -> forall P : (X -> Prop), P x -> P y :=
fun X x y H P Px =>
match H in x == y return P x -> P y with
| eq_refl z => fun Px' => Px'
end Px.
This is in some sense a combination of the first two solution: Px is still introduced, but we use the same pattern as in the second solution to get a term that type-checks as expected.
This last solution is the most flexible one, and in fact it is what many tactics in Coq, such as destruct, do under the hood, to correctly replace a variable in all the right places. Solution 1 would correspond to the more primitive case tactic, and if you use that one you will notice the same problem that variables that you would expect to be identified in fact are not.
So why doesn't Coq always do something like this last solution? The answer is that we want to keep the language of terms as simple as possible, and having pattern-matching touch the whole context would make it even more complicated than it already is. And as this last solution shows, this is in fact not too restricting: we can recover the stronger behaviour when needed, by cleverly using the simpler one.
