Define an inductive dependent-type with constraints on the type-parameter

4
votes

I try to define an inductive dependent-type in Coq to represent bit-vector variables in bit-vector logic.

I read this blog post by Xavier Leroy in which he defines such a structure as follow:

Require Import Vector.

Inductive bitvector : Type := Bitvector (n: nat) (v: Vector.t bool n).

Then, to test this way of doing I tried to define the bitwise negation operator as follow:

Definition bv_neg (v : bitvector) :=
    match v with
        Bitvector n w => Bitvector n (Vector.map negb w)
    end.

And, started to prove that applying two time the negation is equivalent to the identity:

Lemma double_neg :
   forall (v : bitvector), (bv_neg (bv_neg v) = v).

But, while I was trying to do the proof, I realized that having a zero-sized bit-vector make no sense and force to handle the special case n = 0 in every proof.

So, I would like to know how to force the parameter of the inductive dependent-type to be strictly positive.

Any hint is welcome !

3
coqdependent-type
I think Xavier's point was just that Coq's tactics are not capable of deriving decidable equality for types like bitvector, but not that you would want to use a type like that. Indeed, bitvector as defined there is isomorphic to list bool, precisely because the length index n is allowed to vary freely; on the other hand, the inner Vector argument makes it harder to use, as your question shows. I would recommend dropping bitvector and just using list bool instead, which would simplify your development quite a bit. – Arthur Azevedo De Amorim
I am a beginner in Coq and I am discovering this particular way of doing, so sorry for my errors. But, on one hand, I better understand the point of Xavier Leroy blog's post now. Hidding the parameter inside the structure makes it difficult to access it, and you probably got a point here about using list bool. But, on the other hand, building the whole bit-vector operators will require to add constraints on the size of the arguments (e.g. bv_and a b require the size of a and b to be the same). I guess you can do this with a list, but isn't it easier if the size is part of the type ? – perror
The problem with bitvector, the way it is defined, is precisely that there aren't any useful constraints that you can put on the length. If you want to define e.g. bv_add that requires both bit vectors to have the same length, you can use the Vector type from the Coq standard library directly. bv_add would then have type forall n, Vector.t bool n -> Vector.t bool n -> Vector.t bool n. You can't do a similar definition with the original version of bitvector because the length argument is "hidden" by the constructor and doesn't appear in the type. – Arthur Azevedo De Amorim
I see, in fact the syntactic sugar is of no use here, and hidding the size parameter just makes it more difficult to use in the proofs. I think you convinced me. Thanks a lot for these advices. – perror

3 Answers

7
votes

One way to do so is to make sure that the stored Vector is of size S n.

Inductive bitvector : Type := Bitvector (n: nat) (v: Vector.t bool (S n)).

But, I don't see why you'd want to do that in this particular situation given that the lemma is perfectly provable: it is a rather simple corollary of more general lemmas you'll probably need later on.

Your definitions (without the S n alteration):

Require Import Vector.

Inductive bitvector : Type := Bitvector (n: nat) (v: Vector.t bool n).

Definition bv_neg (v : bitvector) :=
    match v with
        Bitvector n w => Bitvector n (Vector.map negb w)
    end.

Some results on Vector.map:

Lemma map_fusion : 
  forall {A B C} {g : B -> C} {f : A -> B} {n : nat} (v : Vector.t A n),
    Vector.map g (Vector.map f v) = Vector.map (fun x => g (f x)) v.
Proof.
intros A B C g f n v ; induction v.
  - reflexivity.
  - simpl; f_equal; assumption.
Qed.

Lemma map_id : 
  forall {A} {n : nat} (v : Vector.t A n), Vector.map (@id A) v = v.
Proof.
intros A n v ; induction v.
  - reflexivity.
  - simpl; f_equal; assumption.
Qed.

Lemma map_extensional : 
  forall {A B} {f1 f2 : A -> B} 
         (feq : forall a, f1 a = f2 a) {n : nat} (v : Vector.t A n),
    Vector.map f1 v = Vector.map f2 v.
Proof.
intros A B f1 f2 feq n v ; induction v.
  - reflexivity.
  - simpl; f_equal; [apply feq | assumption].
Qed.

Finally, your result:

Lemma double_neg :
   forall (v : bitvector), (bv_neg (bv_neg v) = v).
Proof.
intros (n, v).
 simpl; f_equal.
 rewrite map_fusion, <- map_id.
 apply map_extensional.
 - intros []; reflexivity.
Qed.
2
votes

Just to be sure I understood well the comments of Arthur Azevedo De Amorim, I tried to rewrite my Coq module trying to remove the syntactic sugar and the unnecessary concealement of the size.

First, just by looking at the available module in Coq, one can fin the Coq.Bool.Bvector module that is quite close to what I want... But, a lot is missing (especially the modular arithmetic part) and, moreover, I disagree with a few rules such as encoding the sign or having true and false as a particular case of size = 1).

So, my module is almost a copy of the Coq.Bool.Bvector but with slight modifications to make me happy (I might be wrong, we will see it in the future).

Here is the rewritten module:

Require Import Arith Bool Vector.

(** Unsigned Bitvector type *)
Definition bitvector := Vector.t bool.

Definition nil  := @Vector.nil bool.
Definition cons := @Vector.cons bool.

Definition bv_low := @Vector.hd bool.
Definition bv_high := @Vector.tl bool.

(** A bitvector is false if zero and true otherwise. *)
Definition bv_test n (v : bitvector n) := Vector.fold_left orb false v.

(** Bitwise operators *)
Definition bv_neg n (v : bitvector n) := Vector.map negb v.

Definition bv_and n (v w : bitvector n) := Vector.map2 andb v w.
Definition bv_or  n (v w : bitvector n) := Vector.map2  orb v w.
Definition bv_xor n (v w : bitvector n) := Vector.map2 xorb v w.

(** Shift/Rotate operators *)
(* TODO *)

(** Arithmetic operators *)
(* TODO *)

Then, I tried to prove (again) the double negation thing with the help of the Guillaume Allais hints:

Lemma map_fusion :
  forall {A B C} {g : B -> C} {f : A -> B} {n : nat} (v : Vector.t A n),
    Vector.map g (Vector.map f v) = Vector.map (fun x => g (f x)) v.
Proof.
intros A B C g f n v ; induction v.
  - reflexivity.
  - simpl; f_equal; assumption.
Qed.

Lemma map_id :
  forall {A} {n : nat} (v : Vector.t A n), Vector.map (@id A) v = v.
Proof.
intros A n v ; induction v.
  - reflexivity.
  - simpl; f_equal; assumption.
Qed.

Lemma map_extensional :
  forall {A B} {f1 f2 : A -> B}
         (feq : forall a, f1 a = f2 a) {n : nat} (v : Vector.t A n),
    Vector.map f1 v = Vector.map f2 v.
Proof.
intros A B f1 f2 feq n v ; induction v.
  - reflexivity.
  - simpl; f_equal; [apply feq | assumption].
Qed.

Theorem double_neg :
  forall (n : nat) (v : bitvector n), bv_neg n (bv_neg n v) = v.
Proof.
  intros; unfold bv_neg.
  rewrite map_fusion, <- map_id.
  apply map_extensional.
  - intros []; reflexivity.
Qed.

And, surprisingly (for me), it worked like a charm.

Thanks a lot to all, and if you have comments on this code, feel free to drop a comment. As I am very new to Coq, I really want to improve.

2
votes

You can prove the theorem by induction on v.

Require Import Vector.
Definition bitvector := Vector.t bool.
Definition bv_neg n (v : bitvector n) := Vector.map negb v.

Theorem double_neg :
  forall (n : nat) (v : bitvector n), bv_neg n (bv_neg n v) = v.
Proof.
  induction v as [|x]; [|simpl; destruct x; rewrite IHv]; reflexivity.
Qed.