The Coq mailing list

[t x <txrev319 AT gmail.com>]

1) eq_rect =

2)  fun (A: Type) (x: A) (P: A -> Type) (f: P x) (y: A) (e : @eq A x y) =>

3)    match e in (@eq _ _ y0) return (P y0) with

4)      | eq_refl => f

5)    end :

6)      forall (A: Type) (x: A) (P: A -> Type),

7)        P x -> forall y : A, @eq A x y -> P y

8) Inductive eq (A: Type) (x: A) : A -> Prop := refl-equal : eq A x x.

I'm reading Chapter 8 of Coq d'Art, and trying to better understand eq.

"equality" has been interesting in that (1) there were many "obviously equal" things that Coq did not agree with me on and (2) I still don't understand how Coq's equality works.

The above definition -- especially line 3, seems a bit magical to me:

a)  we say "match e in (@eq _ _ y0)" -- so y0 must be bound to y

b)  then we say "return (P y0)", which means "return (P y)"

c)  but then we return f, which has type "(P x)"

and Coq is happy and fine with this. I'm not happy with this. What is Coq doing to convert the "(P x)" to a "(P y)" and why is it allowed in this case?

Thanks!