Une MAJ de sécurité est nécessaire sur notre version actuelle. Elle sera effectuée lundi 02/08 entre 12h30 et 13h. L'interruption de service devrait durer quelques minutes (probablement moins de 5 minutes).

Commit 2c78bda7 authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files

Adapt plugin to Coq 8.6.

parent df9875a9
......@@ -760,7 +760,7 @@ COQPDEP = $(addsuffix .dep, $(COQPMODULES))
COQPCMO = $(addsuffix .cmo, $(COQPMODULES))
COQPCMX = $(addsuffix .cmx, $(COQPMODULES))
COQPTREES = kernel interp intf lib library parsing pretyping proofs printing tactics toplevel
COQPTREES = engine interp intf kernel lib library ltac parsing pretyping printing proofs tactics toplevel
COQPINCLUDES = -I src/coq-tactic -I $(COQCAMLPLIB) $(addprefix -I @COQLIB@/, $(COQPTREES)) @ZIPINCLUDE@
$(COQPDEP): DEPFLAGS += -I src/coq-tactic
......@@ -786,14 +786,20 @@ src/coq-tactic/why3tac.ml: src/coq-tactic/why3tac.ml4
$(SHOW) 'Camlp $<'
$(HIDE)$(COQCAMLP) pr_dump.cmo @COQPPLIBS@ pa_macro.cmo -D@coq_compat_version@ -impl $^ -o $@
COQRTAC = -R lib/coq-tactic Why3 -R lib/coq Why3
ifeq (@coq_compat_version@,COQ86)
COQRTAC += -I lib/coq-tactic
endif
src/coq-tactic/.why3-vo-byte: lib/coq-tactic/Why3.v lib/coq/BuiltIn.vo lib/coq-tactic/why3tac.cma
$(SHOW) 'Coqc $<'
$(HIDE)WHY3CONFIG="" $(COQC) -byte -R lib/coq-tactic Why3 -R lib/coq Why3 $< && \
$(HIDE)WHY3CONFIG="" $(COQC) -byte $(COQRTAC) $< && \
touch src/coq-tactic/.why3-vo-byte
src/coq-tactic/.why3-vo-opt: lib/coq-tactic/Why3.v lib/coq/BuiltIn.vo lib/coq-tactic/why3tac.cmxs
$(SHOW) 'Coqc $<'
$(HIDE)WHY3CONFIG="" $(COQC) -opt -R lib/coq-tactic Why3 -R lib/coq Why3 $< && \
$(HIDE)WHY3CONFIG="" $(COQC) -opt $(COQRTAC) $< && \
touch src/coq-tactic/.why3-vo-opt
# depend and clean targets
......@@ -1570,10 +1576,10 @@ test-session.opt: examples/use_api/create_session.ml lib/why3/why3.cmxa
@rm -f test-session.opt why3session.xml why3shapes why3shapes.gz
test-coq-tactic.byte: src/coq-tactic/.why3-vo-byte
$(COQC) -byte -R lib/coq-tactic Why3 -R lib/coq Why3 bench/coq-tactic/test.v
$(COQC) -byte $(COQRTAC) bench/coq-tactic/test.v
test-coq-tactic.opt: src/coq-tactic/.why3-vo-opt
$(COQC) -opt -R lib/coq-tactic Why3 -R lib/coq Why3 bench/coq-tactic/test.v
$(COQC) -opt $(COQRTAC) bench/coq-tactic/test.v
#only test the compilation of runstrat
test-runstrat.byte: lib/why3/why3.cma lib/why3/META
......
......@@ -525,11 +525,16 @@ if test "$enable_coq_support" = yes; then
COQPPLIBS="$COQLIB/parsing/grammar.cma"
AC_MSG_RESULT($COQVERSION)
;;
8.5*|trunk)
8.5*)
coq_compat_version="COQ85"
COQPPLIBS="$OCAMLLIB/unix.cma $OCAMLLIB/threads/threads.cma $COQLIB/grammar/grammar.cma"
AC_MSG_RESULT($COQVERSION)
;;
8.6*|trunk)
coq_compat_version="COQ86"
COQPPLIBS="$OCAMLLIB/unix.cma $OCAMLLIB/threads/threads.cma $COQLIB/grammar/grammar.cma"
AC_MSG_RESULT($COQVERSION)
;;
*)
enable_coq_support=no
AC_MSG_WARN(You need Coq 8.4 or later; Coq discarded)
......
(* 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.
Parameter last_bit : nat.
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 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'.