Stream: Coq users

Topic: Function to index elements of a vector


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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: Feb 04 2023 at 21:02 UTC