Stream: Coq users

Topic: A 'head' function for 'Vector.t'

Julin S (Aug 09 2021 at 10:06):

I have been trying make a function that accepts a Vector.t and returns its first element.

But couldn't understand how to handle Vector.cons while doing pattern matching.

Require Import Vector.
Import VectorNotations.
Definition head {A n} (v : Vector.t A n) : nat :=
  match v with
  | Vector.nil _ => []
  | @Vector.cons _ _ _ n => 0
  end.

Print Vector.cons.

gives

Inductive t (A : Type) : nat -> Type :=
    nil : t A 0 | cons : A -> forall n : nat, t A n -> t A (S n)

Does A -> forall n : nat, t A n -> t A (S n) mean that it takes:

• a type A (implicit?)
• a Vector.t of size n

and gives a Vector.t of size n+1?

If so, where does the contents of the vector come in?

I mean, how can we access the elements of the vector?

Andrej Dudenhefner (Aug 09 2021 at 11:00):

A -> forall n : nat, t A n -> t A (S n) means that given an element of type A (the head, let's call it x), a natural number n (the length) and a vector of length n (lets call it v) over the type A you construct a longer vector (here x,v).

Julin S (Aug 09 2021 at 11:15):

How can we construct a Vector.t nat 2 element?

Suppose we need to make [10; 20] using the constructors of Vector.t? How do we do that?

Gaëtan Gilbert (Aug 09 2021 at 11:16):

@cons nat 10 1 (@cons nat 20 0 (@nil nat))

Julin S (Aug 09 2021 at 12:11):

Thanks! Had trouble getting that right.

Julin S (Aug 10 2021 at 04:26):

How would we able to make the actual head function though?

I tried

Definition head {A n} (v : Vector.t A n) :
  match v with
  | Vector.nil _ => unit
  | Vector.cons _ _ _ _ => A
  end
   :=
  match v with
  | Vector.nil _ => tt
  | Vector.cons _ x n xs => x
  end.

But am getting an error saying

term "A" has type "Type" while it is expected to have type "Set"

because of the return type.

I did a match for the return type to handle cases where v is an empty vector. Isn't that needed?

What could we place in the return type instead of A?

Gaëtan Gilbert (Aug 10 2021 at 09:00):

that's a stupid issue when the first branch of the match returns Set
you need to explicitly use match v return Type with ...
(btw matching on n for the type should work too)

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

That did the trick!

What does return Type do here?

I looked here: https://coq.inria.fr/refman/language/extensions/match.html
but didn't really understood.

It is not like type-casting in programming languages like C, right?

Kenji Maillard (Aug 13 2021 at 08:03):

The return Type provides explicitely the required type annotation for the result of the match construct: in presence of dependent types this return type can depend on the scrutinee (v here) and cannot be inferred in general (in the sense that the general type inference problem is undecidable). Coq has some heuristics to try to infer a reasonable return type in most simply typed matches (where the return type does not depend on the scrutinee) but plays badly with the inference of Set vs Type.

Last updated: Oct 08 2024 at 16:02 UTC