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] *)
```

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`

?

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".
```

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].`

`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
*)
```

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

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

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

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`

..

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

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

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: Jan 29 2023 at 01:02 UTC