Padding bitvectors · Coq users · Zulip Chat Archive

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.

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.

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)?

Julin S (May 15 2023 at 10:17):

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.

Meven Lennon-Bertrand (May 15 2023 at 12:24):

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.

Ana de Almeida Borges (May 15 2023 at 12:48):

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.

Julin S (May 16 2023 at 06:03):

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

Julin S (May 16 2023 at 06:45):

I mean, other than std++ and mathcomp.
Just to know.
mathcomp takes some time to get used to.

Sebastian Ertel (May 16 2023 at 07:19):

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.)

Stream: Coq users

Topic: Padding bitvectors