The Coq mailing list

[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