I am working on a verification project where the specification uses the following inductive datatype to represent bitvectors (MIT's bbv)

Inductive word : nat -> Set :=
| WO : word O
| WS : bool -> forall n, word n -> word (S n).

On the implementation side, however, the EDSL I am using uses Coq's stdlib Vector to represent bitvectors (with type parameter A set to bool)

Inductive t A : nat -> Type :=
  |nil : t A 0
  |cons : forall (h:A) (n:nat), t A n -> t A (S n).

In order to compare the behavior of functions on the implementation side with the spec correspondents, I need to be able to reason about equality between these different datatypes. I have therefore written the following recursive Prop, which will generate a rewritable bool equality for each bit in the bitvectors.

Fixpoint eq_bbvword_bvector {sz} : word sz -> Bvector sz -> Prop :=
        match sz with
        | 0 => fun _ _ => True
        | S n => fun w bv => (whd w) = (Vector.hd bv) /\
        eq_bbvword_bvector (@wtl n w) (Vector.tl bv)

This works fine, but I wanted to able to work with rewritable equalities between word and Bvector (alias for Vector bool) instead of always referring to this predicate to compare.

Any tips on how to do this ?

  • 4
    $\begingroup$ You can write a function that converts Bvector sz to word sz and use equality on the conversion result with word sz values. $\endgroup$
    – ice1000
    Mar 20, 2023 at 21:24
  • $\begingroup$ Can you give an example of the kind of goals you are aiming at rewriting? Also, your code as is is not self-contained, which makes it harder to help you, because we cannot run it on our side. $\endgroup$ Mar 22, 2023 at 17:49


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.