The Coq mailing list

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

1) The type of E is fixed, I just needed names to refer to the
concrete instances of the indices in E. So e1 stands for whatever
concrete value the term E has for its first index.

2) It's actually put quite well in Adam's book.

- Valentin

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