Hi. I had been trying to use the `Bvector`

module.

With it, I tried to make a function that will pad a given vector to a specific length.

If the specified length is smaller than the length of the given vector, the same vector is returned.

So, I tried:

```
Fixpoint pad {z:nat} (nz:nat) (bv: Bvector.Bvector z) : Bvector.Bvector (Nat.max z nz) :=
match (nz-z) return
match (nz-z) with
| O => Bvector.Bvector z
| _ => Bvector.Bvector nz
end with
| O => bv
| S nz' => Vector.cons _ false _ (pad nz' bv)
end.
```

Got error:

```
In environment
pad : forall z nz : nat, Bvector.Bvector z -> Bvector.Bvector (Nat.max z nz)
z : nat
nz : nat
bv : Bvector.Bvector z
The term "bv" has type "Bvector.Bvector z" while it is expected to have type
"match nz - z with
| 0 => Bvector.Bvector z
| S _ => Bvector.Bvector nz
end".
```

Is this because the value `z`

is bound early (as in it would be bound later if `bv`

had been an index instead of a parameter)?

Is there a way to get around this error?

Just saw in another thread that indexed vectors are a pain and dependent sums (I guess that means subset types) are better.

If that's the case, why does coq's stdlib still not have the latter version? Just curious.

Here is an implementation that is accepted by Coq:

```
Fixpoint repeat (n : nat) (b : bool) : Bvector.Bvector n :=
match n with
| O => []
| S n' => b :: repeat n' b
end.
Fixpoint pad_left {z:nat} (bv: Bvector.Bvector z) (nz:nat) : Bvector.Bvector (Nat.max z nz) :=
match bv with
| [] => repeat nz false
| h :: t =>
match nz with
| 0 => h :: t
| S nz' => h :: (pad_left t nz')
end
end.
```

The important "trick" that makes this implementation work is that its structure is exactly the same as that of `Nat.max`

, in the sense that if you were to erase all content of the vectors and were just keeping their structure (which looks like a nat: a bunch of cons, finishing in a nil), then you'd get *exactly* `Nat.max`

. Due to this, you have all the necessary equations on your indices for Coq to accept the program as well-typed.

Julin S said:

If that's the case, why does coq's stdlib still not have the latter version? Just curious.

The standard library is "standard" in the sense that it's bundled in with Coq and that it's the historically main available library for basic data structures. It is not "standard" in the sense of being optimized for anything in particular, or use "best" practices, or be internally coherent, etc. Many people end up disregarding it and using one of the other libraries for basic types that were indeed created and are maintained as an overall coherent unit sticking with chosen conventions, such as std++ or mathcomp.

I was trying to have bitvectors within coq. Any suggestions on what to use? I'm trying to model simple circuits like full-adders.

I mean, other than std++ and mathcomp.

Just to know.

mathcomp takes some time to get used to.

Hi @Julin S

You probably found this already: bits

It even has `full-adder`

already specified in its operations.

It builds upon mathcomp and ssreflect but in my opinion getting into mathcomp and especially learning ssreflect is absolutely worth the effort.

(And the community here is very helpful with getting started in both.)

Cheers,

Sebastian

Thanks.

Last updated: Jun 25 2024 at 19:01 UTC