The Coq mailing list

[Valentin Robert <valentin.robert.42 AT gmail.com>]

The body of a dependent pattern matching is checked against the return
annotation where the indices are instantiated with the particular
values for the discriminated constructor.

That is, in the eq_refl branch, the body is checked against (P y0),
where eq_refl : @eq _ _ y0.
Now if you look at the equation for eq_refl, it says: eq_refl : eq A x x.
So y0 is unified with the second parameter of eq, x.

From outside the match though, the entire match has the type given by
the return annotation, but with y0 instantiated to be the index of the
discriminee (here e). So indeed this match builds a (P y0) where e :
@eq _ _ y0, and since e : @eq A x y, you can see that y0 is unified
with y.

Did this make sense?

- Valentin

On Mon, Oct 14, 2013 at 2:35 PM, t x 
<txrev319 AT gmail.com>
 wrote:
> 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!