## Stream: Coq users

### Topic: [noob] Usage of `Vector.take`

#### Julin S (Aug 12 2021 at 10:16):

How can we use the `Vector.take` function from https://coq.github.io/doc/v8.9/stdlib/Coq.Init.Datatypes.html ?

`Vector.take`'s type (as obtained by a `Check`) is:

``````take
: forall p : nat, p <= ?n -> t ?A ?n -> t ?A p
where
?A : [ |- Type]
?n : [ |- nat]
``````

where (as I understood it):

• `p`: number of element to 'take'
• `p <= ?n`: Is this some kind of proof? How can we provide it?
• `t ?A ?n`: the vector

How can we provide the `p <= ?n` part to `Vector.take`?

``````(* Vector.take 3 (3<=4) [1;2;3;4] *)
``````

#### Julin S (Aug 12 2021 at 11:50):

I did

``````Lemma pr : 3 <= 5.
repeat constructor.
Qed.

Compute Vector.take 3 pr [1;2;3;4;5].
(*
= [1; 2; 3]
: t nat 3
*)
``````

and it worked.

But how can we do this without creating a lemma like this every time we use `Vector.take`?

#### Julin S (Aug 12 2021 at 13:05):

I tried this afterwards:

``````Compute Vector.take 3 (le_n_S 2 4) [1;2;3;4;5].
``````

but that didn't work either:

``````The term "le_n_S 2 4" has type "2 <= 4 -> 3 <= 5"
while it is expected to have type "3 <= ?n".
``````

#### Gaëtan Gilbert (Aug 12 2021 at 13:23):

try `Print pr` to see what the actual term you need is
you could also do `Compute Vector.take 3 (ltac:(repeat constructor) : 3 <= 5) [1;2;3;4;5].`

#### Julin S (Aug 12 2021 at 13:33):

`pr` gives

``````pr = le_S 3 4 (le_S 3 3 (le_n 3))
: 3 <= 5
``````

But would we have to make a lemma like that every time we use `Vector.take`?

I gave this a try, but coq wouldn't accept that. Gave an error that I couldn't understand.

``````Definition mTake {A n} (t : nat) (v : Vector.t A n) : Vector.t A t :=
Vector.take t (ltac:(repeat constructor) : t <= n) v.

(* Error:
The following term contains unresolved implicit arguments:
(fun (A : Type) (n t0 : nat) (v : t A n) =>
take t0 (?Goal@{t:=t0} : t0 <= n) v)
More precisely:
- ?Goal: Cannot infer an existential variable of type
"t <= n" in environment:
A : Type
n, t : nat
v : Vector.t A n
*)
``````

#### Gaëtan Gilbert (Aug 12 2021 at 13:35):

that tactic will only work for inequalities between specific numbers, not variables

#### Gaëtan Gilbert (Aug 12 2021 at 13:36):

you'll get a better error with `now repeat constructor`

#### Gaëtan Gilbert (Aug 12 2021 at 13:37):

But would we have to make a lemma like that every time we use Vector.take?

you have to provide a proof, it doesn't need to be in a separate definition of course

#### Julin S (Aug 12 2021 at 13:39):

it doesn't need to be in a separate definition of course

What other ways are there? Would some form of the `(ltac: ...)` work?

you'll get a better error with now repeat constructor

Well, yeah.. it says `Tactic failure: Cannot solve this goal`..

#### Gaëtan Gilbert (Aug 12 2021 at 13:40):

What other ways are there? Would some form of the (ltac: ...) work?

you can paste the value from the Print pr or any other proof term

#### Paolo Giarrusso (Aug 13 2021 at 23:03):

Many recommend avoiding Vector altogether, and especially in the beginning.

#### Paolo Giarrusso (Aug 13 2021 at 23:05):

No mTake function can be written with that type, since t could be greater than n; you'll need a proof that t <= n (like take) or a proof of something stronger

Last updated: Sep 30 2023 at 15:01 UTC