The Coq mailing list

[Arthur Azevedo de Amorim <arthur.aa AT gmail.com>]

The problem is that you are trying to return v on the nil branch, and
Coq is not smart enough to understand that it should have length zero
because it is the very same thing you just did pattern-matching on. If
you need to absolutely use v on that branch, you need to apply the
convoy pattern and reabstract it:

Fixpoint pt_aux h len (v : Vector.t nat len) : Vector.t nat len :=
  match v in Vector.t _ len return Vector.t _ len -> Vector.t _ len with
  | [] => fun v => v
  | h' :: v' => fun _ => (h + h') :: pt_aux h' _ v'
  end v.

Notice how the match is returning a function, which is the identity in
the nil case, and that the variable is discarded in the cons case.



2014-04-07 12:15 GMT+02:00 Ö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



-- 
Arthur Azevedo de Amorim