I am having trouble with a piece of Rocq code that I think has to do with providing a proof argument to a function, but I am not sure.
Here's the relevant code. The code below typechecks:
Require Import Coq.Vectors.Vector.
Import VectorNotations.
Definition Bvector := Vector.t bool.
Definition bv_right_shift_ok (v : Bvector 5) : Bvector 5 :=
Vector.append (Vector.const false 2) (fst (Vector.splitat 3 v)).
But if I replace the bv_right_shift_ok definition with
Definition bv_right_shift_notok1 {shift : nat} (v : Bvector 5) : Bvector 5 :=
Vector.append (Vector.const false shift) (fst (Vector.splitat (5 - shift) v)).
It doesn't typecheck, complaining that:
In environment
shift : nat
v : Bvector 5
The term "v" has type "Bvector 5" while it is expected to have type
"t bool (5 - shift + ?r)".
I think this has to do with the fact that shift could be greater than 5, which is disallowed because the length of the second vector in Vector.append will be negative. So I assume a proof of shift < 5 would then imply that the length >= 0.
I am not sure how to go about supplying/asserting such a proposition to this function though. Fwiw, I also tried (without success):
let s := Nat.min shift 5 in Vector.append (Vector.const false s) (fst (Vector.splitat (5 - s) v)).
But this works:
let s := 3 in Vector.append (Vector.const false s) (fst (Vector.splitat (5 - s) v)).
This is an issue about definitional equality. If you have v : Bvector (n + m), then fst (Vector.split_at n v) has type Bvector n. So with your definition you need v to have type Bvector ((5 - shift) + n) for some n, which is not the case since whatever n is, (5 - shift) + n is not definitionally equal to 5. You will need an explicit cast with a proof of (5 - shift) + n = 5 for the n you want. You will also need to cast the whole definition which a priori has type Bvector (shift + (5 - shift) which is not Bvector 5, so you need a proof of shift + (5 - shift) = 5, for which you indeed need to assume that shift <= 5.