Stream: Coq users

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


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

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

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

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

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

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

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

view this post on Zulip Gaëtan Gilbert (Aug 12 2021 at 13:35):

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

view this post on Zulip Gaëtan Gilbert (Aug 12 2021 at 13:36):

you'll get a better error with now repeat constructor

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

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

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

view this post on Zulip Paolo Giarrusso (Aug 13 2021 at 23:03):

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

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