The Coq mailing list

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

This is weird. Coq was saying that the problem is with cons branch,
not nil branch. But when I changed nil branch it worked. So this also
works:

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

Thanks again.

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


2014-04-07 13:24 GMT+03:00 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