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 vectorHow 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: Oct 13 2024 at 01:02 UTC