The Coq mailing list

[Ömer Sinan Ağacan <omeragacan AT gmail.com>]

It works, but I don't understand how can this work. Can anyone explain
how is this definition different than:

  Fixpoint pt_aux h len (v : Vector.t nat len) : Vector.t nat len :=
    match v with
    | Vector.nil => v
    | Vector.cons h' _ t' =>
        Vector.cons nat (h + h') _ (pt_aux h' _ t')
    end.

?

---
Ömer Sinan Ağacan
http://osa1.net


2014-04-07 12:54 GMT+03:00 Arthur Azevedo de Amorim 
<arthur.aa AT gmail.com>:
> Does this work?
>
> Require Vector.
>
> Import Vector.VectorNotations.
>
> Fixpoint pt_aux h len (v : Vector.t nat len) : Vector.t nat len :=
>   match v with
>   | [] => []
>   | h' :: v' => (h + h') :: pt_aux h' _ v'
>   end.
>
> 2014-04-07 11:45 GMT+02:00 Ömer Sinan Ağacan 
> <omeragacan AT gmail.com>:
>> I'm stuck again :-) Coq gives this error:
>>
>> The term "Vector.cons nat (h + h') l' (fn h' l' t')" has type
>>  "Vector.t nat (S l')" while it is expected to have type "Vector.t nat 
>> len".
>>
>> in this code:
>>
>>   Definition pt_aux : forall (h len : nat), Vector.t nat len ->
>> Vector.t nat len :=
>>     fix fn h len v :=
>>       match v return Vector.t nat len with
>>       | Vector.nil => v
>>       | Vector.cons h' l' t'  =>
>>           Vector.cons nat (h + h') l' (fn h' l' t')
>>       end.
>>
>> so I need to somehow tell Coq that S l' = len, because t' is tail part
>> of vector v and v has length len.
>>
>> I tried implementing something like
>>
>>   Definition vector_cases {T : Type} (len len' : nat) (v : Vector.t T len) 
>> :
>>     {ve : T * Vector.t T len' | len = S len'} + {len = 0}.
>>
>> but this is obviously wrong, because I need to get len' as return, I
>> don't know if such a len' exists or if it does, whar is it. I don't
>> know how to encode this idea in Coq.
>>
>> Maybe I should read one or two more chapters in CPDT :-)
>>
>> ---
>> Ömer Sinan Ağacan
>> http://osa1.net
>
>
>
> --
> Arthur Azevedo de Amorim