Geek Answers Handbook

Define an inductive dependent type with restrictions on the type parameter

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

I read this Xavier Leroy blog post in which it defines a structure like the one below:

Require Import Vector.

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

Then, to check this execution method, I tried to define the bitwise negation operator as follows:

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

And, he began to prove that, applying twice, negation is equivalent to identity:

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

But, although I was trying to make a proof, I realized that having a zero-sized bit vector does not make sense and power to handle a special case n = 0in each proof.

So, I would like to know how to make a parameter of an inductive dependent type be strictly positive.

!

+4
3

- , Vector S n.

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

, , , : , , , .

( S n):

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.

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.

, :

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

, , , Coq, .

-, Coq, Coq.Bool.Bvector, , ... ( ) , , , size = 1).

, - Coq.Bool.Bvector, , ( , ).

:

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

() :

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.

, ( ), .

, , . Coq, .

+2

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.
+2

More articles:


All Articles