The Coq mailing list

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

Rather (assuming we only talk about indices), if:

E : T e1 ... en

and:

T :=
| Ci: ... -> T ci_1 ... ci_n

Then it is checked that:
1) Bi : U {y is replaced by Ci, xk is replaced by ci_k}

And the resulting term has type:
2) FinalType = U {y is replaced by E, xk is replaced by ek}

Unless I'm mistaken.

- Valentin


On Mon, Oct 14, 2013 at 3:11 PM, t x 
<txrev319 AT gmail.com>
 wrote:
> Valentin: this is helpful, but I'm not quite there yet.
>
> Adam: I've seen that section of
> http://adam.chlipala.net/cpdt/html/MoreDep.html before -- unfortunately, I
> find the prose difficult to understand.
>
>
> Can I think of type checking as follows:
>
> Suppose have:
>
> match E as y in (T x1 ... xn) return U with
> | C1 z1_1 z1_2 ... z1_m1 => B1
> | C2 z2_1 z2_2 ... z2_m2 => B2
> ...
> | Ci  zi_1 zi_2 ... zi_mi => Bi
> ...
> end : FinalType
>
> then to have a valid type check, we need the following properties:
>
> 1) forall i, (E = Ci zi_1 ... zi_mi) ->
>   type_of ( Bi ) =  U { y replaced with Ci zi_1 ... zi_mi}
>
> 2) there needs to be some relation between U and FinalType -- but I think
> it's more subtle than "U = FinalType"
>
>
>
>
>
> On Mon, Oct 14, 2013 at 2:52 PM, Adam Chlipala 
> <adamc AT csail.mit.edu>
>  wrote:
>>
>> Section 8.2, "The One Rule of Dependent Pattern Matching in Coq," in CPDT
>> <http://adam.chlipala.net/cpdt/> might clear this up.  There really is a
>> pretty straightforward typing rule behind this behavior and that of all
>> [match]es in Coq.
>>
>>
>> On 10/14/2013 05:35 PM, t x 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?
>
>