Skip to content

GitLab

why3
why3
Commit f57a7f13 authored by MARCHE Claude's avatar MARCHE Claude
Browse files
Options

Dropped Coq realization of bv/BV_Gen for Coq 8.4 

Good thing, there is no more any version-specific Coq realizations
parent 011a0323
Hide whitespace changes
Inline Side-by-side
Showing with 18 additions and 4038 deletions
.gitignore
View file @ f57a7f13
...@@ -148,7 +148,6 @@ why3.conf ...@@ -148,7 +148,6 @@ why3.conf
/src/coq-tactic/.why3-vo-* /src/coq-tactic/.why3-vo-*
# Coq # Coq
/lib/coq/bv/BV_Gen.v
# PVS # PVS
.pvscontext .pvscontext
......
Makefile.in
View file @ f57a7f13
...@@ -896,7 +896,7 @@ ifeq (@enable_coq_support@,yes) ...@@ -896,7 +896,7 @@ ifeq (@enable_coq_support@,yes)
ifeq (@enable_coq_libs@,yes) ifeq (@enable_coq_libs@,yes)
COQVERSIONSPECIFIC=bv/BV_Gen.v COQVERSIONSPECIFIC=
COQVERSIONSPECIFICTARGETS=$(addprefix lib/coq/, $(COQVERSIONSPECIFIC)) COQVERSIONSPECIFICTARGETS=$(addprefix lib/coq/, $(COQVERSIONSPECIFIC))
COQVERSIONSPECIFICSOURCES=$(addsuffix .@coq_compat_version@, $(COQVERSIONSPECIFICTARGETS)) COQVERSIONSPECIFICSOURCES=$(addsuffix .@coq_compat_version@, $(COQVERSIONSPECIFICTARGETS))
...@@ -942,7 +942,11 @@ COQLIBS_OPTION = $(addprefix lib/coq/option/, $(COQLIBS_OPTION_FILES)) ...@@ -942,7 +942,11 @@ COQLIBS_OPTION = $(addprefix lib/coq/option/, $(COQLIBS_OPTION_FILES))
COQLIBS_SEQ_FILES = Seq COQLIBS_SEQ_FILES = Seq
COQLIBS_SEQ = $(addprefix lib/coq/seq/, $(COQLIBS_SEQ_FILES)) COQLIBS_SEQ = $(addprefix lib/coq/seq/, $(COQLIBS_SEQ_FILES))
ifeq (@coq_compat_version@,COQ84)
COQLIBS_BV_FILES = Pow2int
else
COQLIBS_BV_FILES = Pow2int BV_Gen COQLIBS_BV_FILES = Pow2int BV_Gen
endif
COQLIBS_BV = $(addprefix lib/coq/bv/, $(COQLIBS_BV_FILES)) COQLIBS_BV = $(addprefix lib/coq/bv/, $(COQLIBS_BV_FILES))
ifeq (@enable_coq_fp_libs@,yes) ifeq (@enable_coq_fp_libs@,yes)
......
lib/coq/bv/BV_Gen.v.COQ84 deleted 100644 → 0
View file @ 011a0323
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
Require bool.Bool.
Require int.Int.
Require int.Abs.
Require int.EuclideanDivision.
Require bv.Pow2int.
Definition last_bit : nat.
Admitted.
Definition size_nat: nat := S last_bit.
(* Why3 goal *)
Definition size: Z.
exact (Z.of_nat size_nat).
Defined.
Lemma size_int_S : size = Z.succ (Z.of_nat last_bit).
unfold size, size_nat.
rewrite Nat2Z.inj_succ; trivial.
Qed.
(* Why3 goal *)
Lemma size_pos : (0%Z < size)%Z.
rewrite size_int_S; omega.
Qed.
Require Import Bool.Bvector.
(* Why3 goal *)
Definition t : Type.
exact (Bvector size_nat).
Defined.
Fixpoint nth_aux {l} (v : Vector.t bool l) (m : Z) : bool :=
match v with
| Vector.nil => false
| Vector.cons b _ tl => if Z_eq_dec m 0 then b else nth_aux tl (Z.pred m)
end.
(* nth helper lemmas *)
Lemma nth_cons {l} (v : Vector.t bool l) (m : Z) b : (m <> -1)%Z ->
nth_aux (Vector.cons bool b l v) (Z.succ m) = nth_aux v m.
intro; simpl.
case Z.eq_dec; intro.
assert False by omega; easy.
rewrite <- Zpred_succ; easy.
Qed.
Lemma nth_cons_pred {l} (v : Vector.t bool l) (m : Z) b : (m <> 0)%Z ->
nth_aux (Vector.cons bool b l v) m = nth_aux v (Z.pred m).
intro.
rewrite Zsucc_pred with (n := m), <- Zpred_succ; apply nth_cons; omega.
Qed.
Lemma nth_high : forall {l} (v : Vector.t bool l) m, (m >= (Z.of_nat l))%Z -> nth_aux v m = false.
induction v.
easy.
rewrite Nat2Z.inj_succ.
intros; rewrite nth_cons_pred by omega.
apply IHv; omega.
Qed.
Lemma nth_low : forall {l} (v : Vector.t bool l) m, (m < 0)%Z -> nth_aux v m = false.
induction v.
easy.
intros; rewrite nth_cons_pred by omega.
apply IHv; omega.
Qed.
Lemma nth_zeros_is_hd : forall {l} (b : Vector.t bool (S l)), nth_aux b 0 = Vector.hd b.
apply Vector.rectS; easy.
Qed.
Lemma nth_predl_is_last : forall {l} (b : Vector.t bool (S l)), nth_aux b (Z.of_nat l) = Vector.last b.
apply Vector.rectS.
easy.
intros.
rewrite Nat2Z.inj_succ, nth_cons by omega.
easy.
Qed.
Lemma nth_const {l} (m : Z) b: (0 <= m < Z.of_nat l)%Z -> nth_aux (Vector.const b l) m = b.
revert b m.
induction l.
simpl.
intros; assert False by omega; easy.
rewrite Nat2Z.inj_succ; intros; simpl.
case (Z.eq_dec m 0); intro.
easy.
apply IHl; omega.
Qed.
Lemma nth_aux_map : forall {l} (f : bool -> bool) (v : Vector.t bool l) m,
(0 <= m < Z.of_nat l)%Z ->
f (nth_aux v m) = nth_aux (Vector.map f v) m.
induction v.
simpl; intros; assert False by omega; easy.
rewrite Nat2Z.inj_succ; intros; simpl.
case (Z.eq_dec m 0); intro.
easy.
apply IHv; omega.
Qed.
Lemma nth_aux_map2 : forall {l} (f : bool -> bool -> bool) (v1 v2 : Vector.t bool l) m,
(0 <= m < Z.of_nat l)%Z ->
f (nth_aux v1 m) (nth_aux v2 m) = nth_aux (Vector.map2 f v1 v2) m.
intros l f v1 v2; pattern l, v1, v2.
apply Vector.rect2.
simpl; intros; assert False by omega; easy.
intros.
rewrite Nat2Z.inj_succ in H0; simpl.
case (Z.eq_dec m 0); intro.
easy.
apply H; omega.
Qed.
Lemma nth_aux_tl : forall {l} (v : Vector.t bool (S l)) m, (m <> -1)%Z -> nth_aux (Vector.tl v) m = nth_aux v (Z.succ m).
intros l v; pattern l, v.
apply Vector.rectS.
simpl.
intros; case Z.eq_dec.
intro; assert False by omega; easy.
trivial.
intros.
simpl (Vector.tl (a :: v0)).
symmetry; apply nth_cons; omega.
Qed.
Lemma nth_aux_shiftout_last : forall {l} (v : Vector.t bool (S l)), nth_aux (Vector.shiftout v) (Z.of_nat l) = false.
intros l v; pattern l, v.
apply Vector.rectS; intros.
easy.
rewrite Nat2Z.inj_succ.
assert (Vector.shiftout (a :: v0) = a :: (Vector.shiftout v0)) by easy.
rewrite H0, nth_cons by omega.
apply H.
Qed.
Lemma nth_aux_shiftout_not_last : forall {l} (v : Vector.t bool (S l)) m, (m <> Z.of_nat l)%Z -> nth_aux (Vector.shiftout v) m = nth_aux v m.
intros l v; pattern l, v.
apply Vector.rectS; intros.
simpl; case Z.eq_dec; easy.
simpl; case Z.eq_dec; trivial.
intro; apply H.
rewrite Nat2Z.inj_succ in H0; omega.
Qed.
Lemma nth_aux_shiftin_false : forall {l} (v : Vector.t bool l) m, nth_aux (Vector.shiftin false v) m = nth_aux v m.
induction v; intro; simpl; case (Z.eq_dec m 0); trivial.
Qed.
Lemma nth_aux_shiftin_low : forall {l} (v : Vector.t bool l) m b, 0 < l -> (0 <= m < Z.of_nat l)%Z -> nth_aux (Vector.shiftin b v) m = nth_aux v m.
induction v; intros.
easy.
simpl; case Z.eq_dec.
easy.
rewrite Nat2Z.inj_succ in H0.
intro; apply IHv; omega.
Qed.
Lemma nth_aux_shiftin_high : forall {l} (v : Vector.t bool l) b, nth_aux (Vector.shiftin b v) (Z.of_nat l) = b.
induction v.
easy.
unfold Vector.shiftin.
fold (@Vector.shiftin bool).
rewrite Nat2Z.inj_succ.
intro; rewrite nth_cons by omega.
apply IHv.
Qed.
(* end of nth helpers *)
(* Why3 goal *)
Definition nth: t -> Z -> bool.
exact nth_aux.
Defined.
Lemma nth_aux_out_of_bound : forall {l} (v : Vector.t bool l) (n : Z), ((n < 0%Z)%Z \/
(Z.of_nat l <= n)%Z) -> ((nth_aux v n) = false).
induction v.
simpl; auto.
simpl.
intros.
case Z.eq_dec.
intros; elimtype False; destruct H.
omega.
subst n0.
auto with zarith.
intro; rewrite IHv;auto.
intuition; auto with zarith.
right.
rewrite Zpos_P_of_succ_nat in H0.
omega.
Qed.
(* Why3 goal *)
Lemma nth_out_of_bound : forall (x:t) (n:Z), ((n < 0%Z)%Z \/
(size <= n)%Z) -> ((nth x n) = false).
intros.
unfold nth.
rewrite nth_aux_out_of_bound; auto with zarith.
Qed.
Definition zeros_aux {l} : Vector.t bool l.
exact (Vector.const false l).
Defined.
(* Why3 goal *)
Definition zeros: t.
exact zeros_aux.
Defined.
Lemma Nth_zeros_aux : forall {l} (n:Z), ((@nth_aux l zeros_aux n) = false).
induction l.
easy.
simpl.
intro n; case (Z.eq_dec n 0); easy.
Qed.
(* Why3 goal *)
Lemma Nth_zeros : forall (n:Z), ((nth zeros n) = false).
intros n; apply Nth_zeros_aux.
Qed.
Definition one_aux l : Vector.t bool (S l).
exact (Vector.cons bool true l (Vector.const false l)).
Defined.
(* Why3 goal *)
Definition one: t.
exact (one_aux last_bit).
Defined.
Definition ones_aux l : Vector.t bool l.
exact (Vector.const true l).
Defined.
(* Why3 goal *)
Definition ones: t.
exact (ones_aux size_nat).
Defined.
(* Why3 goal *)
Lemma Nth_ones : forall (n:Z), ((0%Z <= n)%Z /\ (n < size)%Z) -> ((nth ones
n) = true).
intros; apply nth_const; easy.
Qed.
(* Why3 goal *)
Definition bw_and: t -> t -> t.
exact (Vector.map2 (fun x y => x && y)).
Defined.
(* Why3 goal *)
Lemma Nth_bw_and : forall (v1:t) (v2:t) (n:Z), ((0%Z <= n)%Z /\
(n < size)%Z) -> ((nth (bw_and v1 v2) n) = (Init.Datatypes.andb (nth v1
n) (nth v2 n))).
symmetry.
apply nth_aux_map2 with (f := fun x y => x && y); easy.
Qed.
(* Why3 goal *)
Definition bw_or: t -> t -> t.
exact (Vector.map2 (fun x y => x || y)).
Defined.
(* Why3 goal *)
Lemma Nth_bw_or : forall (v1:t) (v2:t) (n:Z), ((0%Z <= n)%Z /\
(n < size)%Z) -> ((nth (bw_or v1 v2) n) = (Init.Datatypes.orb (nth v1
n) (nth v2 n))).
symmetry.
apply nth_aux_map2; easy.
Qed.
(* Why3 goal *)
Definition bw_xor: t -> t -> t.
exact (Vector.map2 (fun x y => xorb x y)).
Defined.
(* Why3 goal *)
Lemma Nth_bw_xor : forall (v1:t) (v2:t) (n:Z), ((0%Z <= n)%Z /\
(n < size)%Z) -> ((nth (bw_xor v1 v2) n) = (Init.Datatypes.xorb (nth v1
n) (nth v2 n))).
symmetry.
apply nth_aux_map2; easy.
Qed.
(* Why3 goal *)
Definition bw_not: t -> t.
exact (Vector.map (fun x => negb x)).
Defined.
(* Why3 goal *)
Lemma Nth_bw_not : forall (v:t) (n:Z), ((0%Z <= n)%Z /\ (n < size)%Z) ->
((nth (bw_not v) n) = (Init.Datatypes.negb (nth v n))).
symmetry.
apply nth_aux_map; easy.
Qed.
(* Why3 goal *)
Definition lsr: t -> Z -> t.
exact (fun v m => BshiftRl_iter last_bit v (Z.to_nat m)).
Defined.
Lemma bshiftRl_iter_nth : forall b s m,
(0 <= Z.of_nat s)%Z ->
(0 <= m)%Z ->
nth_aux (BshiftRl_iter last_bit b s) m = nth_aux b (m + Z.of_nat s).
induction s.
simpl.
intros; rewrite <- Zplus_0_r_reverse; easy.
rewrite Nat2Z.inj_succ; intros.
simpl BshiftRl_iter.
unfold BshiftRl, Bhigh.
rewrite nth_aux_tl by omega.
rewrite nth_aux_shiftin_false.
rewrite <- Zplus_succ_r_reverse, <- Z.add_succ_l.
apply IHs; omega.
Qed.
(* Why3 goal *)
Lemma Lsr_nth_low : forall (b:t) (n:Z) (s:Z), (0%Z <= s)%Z ->
((0%Z <= n)%Z -> (((n + s)%Z < size)%Z -> ((nth (lsr b s) n) = (nth b
(n + s)%Z)))).
intros b n s h1 h2 h3.
rewrite <-Z2Nat.id with (n := s) at 2; auto.
apply bshiftRl_iter_nth; omega.
Qed.
(* Why3 goal *)
Lemma Lsr_nth_high : forall (b:t) (n:Z) (s:Z), (0%Z <= s)%Z ->
((0%Z <= n)%Z -> ((size <= (n + s)%Z)%Z -> ((nth (lsr b s) n) = false))).
intros b n s h1 h2 h3.
unfold nth,lsr.
cut (nth_aux b (n + Z.of_nat (Z.to_nat s)) = false).
intro.
rewrite <-H.
apply bshiftRl_iter_nth; omega.
rewrite Z2Nat.id by omega.
apply nth_out_of_bound; omega.
Qed.
(* Why3 goal *)
Lemma lsr_zeros : forall (x:t), ((lsr x 0%Z) = x).
auto.
Qed.
(* Why3 goal *)
Definition asr: t -> Z -> t.
exact (fun v m => BshiftRa_iter last_bit v (Z.to_nat m)).
Defined.
Definition eq_aux {l} (v1 v2 : Vector.t bool l): Prop := forall (n:Z), ((0%Z <= n)%Z /\
(n < (Z.of_nat l))%Z) -> ((nth_aux v1 n) = (nth_aux v2 n)).
Lemma eq_aux_cons : forall {l} v1 v2 b b', b = b' /\ @eq_aux l v1 v2 <-> eq_aux (b :: v1) (b' :: v2).
intros; unfold eq_aux.
rewrite Nat2Z.inj_succ.
split; intros.
simpl; case Z.eq_dec; intro.
easy.
apply H; omega.
split.
apply (H 0%Z); omega.
intros.
rewrite <- (nth_cons v1 n b) by omega.
rewrite <- (nth_cons v2 n b') by omega.
apply H; omega.
Qed.
Lemma Extensionality_aux : forall {l} (x y : Vector.t bool l), eq_aux x y -> x = y.
intros l x y; pattern l, x, y.
apply Vector.rect2.
easy.
intros.
apply (eq_aux_cons v1 v2 a b) in H0; destruct H0.
apply H in H1.
rewrite H0, H1; trivial.
Qed.
(* Vector helper lemmas *)
Lemma singleton_is_singl : forall b : Vector.t bool 1, b = [ Vector.hd b ].
intro; apply Extensionality_aux; unfold eq_aux; intros.
change (Z.of_nat 1) with 1%Z in H; assert (n = 0%Z) as e by omega; rewrite e; simpl.
apply nth_zeros_is_hd.
Qed.
Lemma shiftrepeat_is_shiftin : forall {l} (v : Vector.t bool (S l)), Vector.shiftrepeat v = Vector.shiftin (Vector.last v) v.
apply Vector.rectS.
easy.
intros; simpl.
rewrite H; trivial.
Qed.
Lemma last_tail_shiftreapeat : forall {l} (v : Vector.t bool (S l)), Vector.last (Vector.tl (Vector.shiftrepeat v)) = Vector.last v.
apply Vector.caseS; intros.
induction n.
apply Vector.case0 with (v := t0); easy.
simpl.
apply Vector.shiftrepeat_last.
Qed.
(* end of Vector helpers *)
Lemma BshiftRa_iter_nth_low : forall (b:t) (s:nat) (n:Z),
(0%Z <= n < (size - (Z.of_nat s)))%Z ->
(nth_aux (BshiftRa_iter last_bit b s) n) = (nth_aux b (n + Z.of_nat s)%Z).
induction s.
simpl.
intros; rewrite <- Zplus_0_r_reverse; easy.
rewrite Nat2Z.inj_succ; intros.
simpl BshiftRa_iter.
unfold BshiftRa, Bhigh.
rewrite nth_aux_tl by omega.
rewrite shiftrepeat_is_shiftin.
rewrite nth_aux_shiftin_low.
rewrite <- Zplus_succ_r_reverse, <- Z.add_succ_l.
apply IHs; omega.
omega.
fold size_nat; fold size; omega.
Qed.
(* Why3 goal *)
Lemma Asr_nth_low : forall (b:t) (n:Z) (s:Z), (0%Z <= s)%Z ->
(((0%Z <= n)%Z /\ (n < size)%Z) -> (((n + s)%Z < size)%Z -> ((nth (asr b s)
n) = (nth b (n + s)%Z)))).
unfold nth, lsr.
intros.
assert ((n + s)%Z = (n + Z.of_nat (Z.to_nat s))%Z).
rewrite Z2Nat.id with (n := s); omega.
rewrite H2.
apply BshiftRa_iter_nth_low; omega.
Qed.
Lemma bshiftra_iter_last : forall {l} (v : Bvector (S l)) s, Vector.last (BshiftRa_iter l v s) = Vector.last v.
induction s.
easy.
simpl; unfold BshiftRa, Bhigh.
rewrite last_tail_shiftreapeat.
apply IHs.
Qed.
Lemma BhiftRa_iter_nth_high : forall (b:t) (s:nat) (n:Z),
(0%Z <= n < size)%Z ->
(size <= n + Z.of_nat s)%Z -> ((nth_aux (BshiftRa_iter last_bit b s) n) = nth_aux b
(size - 1%Z))%Z.
induction s.
simpl BshiftRa_iter.
simpl (Z.of_nat 0).
intros.
assert (n = size - 1)%Z by omega; rewrite H1; trivial.
rewrite Nat2Z.inj_succ; intros.
simpl BshiftRa_iter.
unfold BshiftRa, Bhigh.
rewrite nth_aux_tl by omega.
rewrite shiftrepeat_is_shiftin.
case (Z.eq_dec (Z.succ n) size).
intro; unfold size in e.
rewrite e, nth_aux_shiftin_high.
rewrite bshiftra_iter_last.
rewrite size_int_S, Z.sub_1_r, <- Zpred_succ.
symmetry; apply nth_predl_is_last.
intro; rewrite nth_aux_shiftin_low.
apply IHs; omega.
omega.
fold size_nat; fold size; omega.
Qed.
(* Why3 goal *)
Lemma Asr_nth_high : forall (b:t) (n:Z) (s:Z), (0%Z <= s)%Z ->
(((0%Z <= n)%Z /\ (n < size)%Z) -> ((size <= (n + s)%Z)%Z -> ((nth (asr b
s) n) = (nth b (size - 1%Z)%Z)))).
unfold nth, asr.
intros.
apply BhiftRa_iter_nth_high.
omega.
rewrite Z2Nat.id; omega.
Qed.
(* Why3 goal *)
Lemma asr_zeros : forall (x:t), ((asr x 0%Z) = x).
auto.
Qed.
(* Why3 goal *)
Definition lsl: t -> Z -> t.
exact (fun v m => BshiftL_iter last_bit v (Z.to_nat m)).
Defined.
Lemma bshiftL_iter_nth_high : forall {l} v s m, (0 <= Z.of_nat s)%Z -> (Z.of_nat s <= m)%Z -> (m < Z.succ (Z.of_nat l))%Z -> nth_aux (BshiftL_iter l v s) m = nth_aux v (m - Z.of_nat s).
induction s; intros.
simpl.
rewrite <-Zminus_0_l_reverse; reflexivity.
simpl.
case Z.eq_dec; intro.
symmetry; apply nth_low.
rewrite e; simpl; apply Pos2Z.neg_is_neg.
rewrite Nat2Z.inj_succ in H, H0.
case (Z.eq_dec (Z.pred m) (Z.of_nat l));intro.
assert False by omega; easy.
rewrite nth_aux_shiftout_not_last by omega.
rewrite Zpos_P_of_succ_nat, Z.sub_succ_r, <- Z.sub_pred_l.
apply IHs; omega.
Qed.
(* Why3 goal *)
Lemma Lsl_nth_high : forall (b:t) (n:Z) (s:Z), ((0%Z <= s)%Z /\
((s <= n)%Z /\ (n < size)%Z)) -> ((nth (lsl b s) n) = (nth b (n - s)%Z)).
intros.
unfold lsl, nth.
rewrite <-Z2Nat.id with (n := s) at 2 by omega.
destruct H.
destruct H0.
apply (bshiftL_iter_nth_high b (Z.to_nat s) n).
auto with zarith.
rewrite Z2Nat.id; omega.
rewrite size_int_S in H1.
omega.
Qed.
Lemma Lsl_nth_low_aux : forall {l} x b (n : int),
(0 <= n < Z.of_nat x)%Z -> nth_aux (BshiftL_iter l b x) n = false.
induction x.
simpl; intros; assert False by omega; easy.
rewrite Nat2Z.inj_succ; intros.
simpl.
case Z.eq_dec;intro.
trivial.
case (Z.eq_dec (Z.pred n) (Z.of_nat l));intro.
apply nth_high; omega.
rewrite nth_aux_shiftout_not_last by auto.
apply IHx; omega.
Qed.
(* Why3 goal *)
Lemma Lsl_nth_low : forall (b:t) (n:Z) (s:Z), ((0%Z <= n)%Z /\ (n < s)%Z) ->
((nth (lsl b s) n) = false).
intros.
apply Lsl_nth_low_aux.
rewrite Z2Nat.id; omega.
Qed.
(* Why3 goal *)
Lemma lsl_zeros : forall (x:t), ((lsl x 0%Z) = x).
auto.
Qed.
Lemma max_int_nat : forall l, (0 <= Pow2int.pow2 (Z.of_nat l) - 1)%Z.
intro.
rewrite Z.sub_1_r.
apply Zlt_0_le_0_pred.
apply Pow2int.pow2pos.
omega.
Qed.
Fixpoint bvec_to_nat n (v : Bvector n) {struct v} : nat :=
match v with
| Vector.nil => O
| Vector.cons false n v => 2 * bvec_to_nat n v
| Vector.cons true n v => 1 + 2 * bvec_to_nat n v
end.
Lemma bvec_to_nat_zeros : forall {l}, bvec_to_nat l (Vector.const false l) = 0.
induction l; [easy|simpl; omega].
Qed.
Definition twos_complement n (v : Bvector n) : Z :=
match v with
| Vector.nil => 0%Z
| Vector.cons false n v => Z.of_nat (bvec_to_nat n v)
| Vector.cons true n v => (Z.of_nat (bvec_to_nat n v) - Pow2int.pow2 (Z.of_nat (S n)))%Z
end.
Require Arith.Div2.
Fixpoint nat_to_bvec (length val : nat) {struct length} : Bvector length :=
match length as x return Bvector x with
| O => Bnil
| S length =>
Bcons (Z.odd (Z.of_nat val)) length (nat_to_bvec length (Div2.div2 val))
end.
Lemma Nat_to_bvec_zeros : forall {n}, Vector.const false n = nat_to_bvec n 0.
induction n.
easy.
simpl.
unfold Bcons.
rewrite IHn; trivial.
Qed.
Lemma bvec_to_nat_extensionality : forall {m} (v v' : Bvector m),
(bvec_to_nat m v) = (bvec_to_nat m v') -> v = v'.
unfold Bvector.
intros m v v'.
pattern m,v,v'.
apply Vector.rect2.
trivial.
case a, b; intros.
rewrite H; auto; inversion H0; omega.
inversion H0; assert False; omega.
inversion H0; assert False; omega.
rewrite H; auto; inversion H0; omega.
Qed.
(* pow2 helper lemmas *)
Lemma id_lt_pow2: forall n, (Z.of_nat (S n) < Pow2int.pow2 (Z.of_nat (S n)))%Z.
intro.
induction n.
easy.
rewrite Nat2Z.inj_succ.
apply Z.le_lt_trans with (m := (2 * Z.of_nat (S n))%Z).
rewrite Nat2Z.inj_succ; omega.
apply Z.lt_le_trans with (m := (2 * Pow2int.pow2 (Z.of_nat (S n)))%Z).
omega.
rewrite two_p_S by omega.
unfold Pow2int.pow2; omega.
Qed.
Lemma pow2_lt_mono_nat : forall i j : nat, (i < j) -> (Pow2int.pow2 (Z.of_nat i) < Pow2int.pow2 (Z.of_nat j))%Z.
intros.
unfold Pow2int.pow2; rewrite two_p_equiv, two_p_equiv.
apply Z.pow_lt_mono_r; omega.
Qed.
Lemma pow2_le_mono_nat : forall i j : nat, (i <= j) -> (Pow2int.pow2 (Z.of_nat i) <= Pow2int.pow2 (Z.of_nat j))%Z.
intros.
unfold Pow2int.pow2; rewrite two_p_equiv, two_p_equiv.
apply Z.pow_le_mono_r; omega.
Qed.
Lemma pow2_le_mono_pos : forall i j : positive, (Pos.le i j) -> (Pow2int.pow2 (Zpos i) <= Pow2int.pow2 (Zpos j))%Z.
intros.
rewrite <- positive_nat_Z, <- positive_nat_Z.
apply pow2_le_mono_nat.
apply Pos2Nat.inj_le; trivial.
Qed.