The Coq mailing list

[t x <txrev319 AT gmail.com>]

1) I was not aware that the _TYPE_ of E could also be different. Previously I thought that the type of E was fixed, but the "match type" can depend on the value of E. Now, it's clear to that even the type of E is not fixed.

2) I'm still not convinced I understand dependent type matching (though Adam's 4 paragraphs in CPDT is starting to make more sense.)

Is it possible to express "the one rule of dependent type matching" as a inference rule, i.e. things like:

Env |- t1: A -> B
Env |- t2: A
------------------------

Env |- t1 t2 : B

On Mon, Oct 14, 2013 at 3:38 PM, Valentin Robert <valentin.robert.42 AT gmail.com> wrote:

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?
>
>