Stream: Coq users

Topic: Function to index elements of a vector

Julin S (Aug 10 2021 at 13:47):

I was trying to make a way to access elements of a Vector.t by the 'index' of the elements (where indexing starts from zero).

I tried:

Fixpoint index {A n} (i : nat) (v : Vector.t A n) :
  (*match n with*)
  match n, v return Type with
  | _, nil _        => unit
  | _, cons _ _ _ _ => A
  end :=
  match n, v with
  | _, nil _            => tt
  | 0, cons _ x _ xs    => x
  | S n', cons _ x z xs => index i xs
  end.

but am getting error that says:

The term "tt" has type "unit" while it is expected to have type
 "match ?t@{v:=v0; n2:=0; n3:=0; v1:=[]} with
  | [] => unit
  | _ :: _ => A
  end".

I thought doing the match for the return type would've avoided such an error.

How can this be set right?

Olivier Laurent (Aug 10 2021 at 19:51):

As far as I understand, you are trying to say that your index function returns an element of type A whenever v is not empty, but your code would give index (S 0) (cons _ _ _ (nil _)) = tt.

Julin S (Aug 12 2021 at 07:20):

Yeah, I wanted index to return an A when v isn't empty and the index is valid.

I meant indexing to start from 0. (cons _ _ _ (nil _)) means a vector with a single element, right? So an index of (S 0) would be invalid.

I gave tt as a way to handle invalid cases (don't even know if that's how it's usually done..).

Edit: Oh.. I see that the index is not taken into account while defining the return type..

Last updated: Oct 03 2023 at 20:01 UTC