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

Question

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 !

Answer 1

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.

Answer 2

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.