Commit bf48eb01 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Partly fix compilation with Coq 8.8.

parent a5d56f8b
......@@ -549,6 +549,11 @@ if test "$enable_coq_support" = yes; then
COQPPLIBS="$OCAMLLIB/unix.cma $OCAMLLIB/threads/threads.cma $COQLIB/grammar/grammar.cma"
AC_MSG_RESULT($COQVERSION)
;;
8.8*)
coq_compat_version="COQ88"
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)
......
......@@ -1829,6 +1829,7 @@ Lemma nth_bit_pred_high :
to_uint i < size ->
to_uint i < Z.of_nat n ->
nth_bv (sub (lsl (of_int 1%Z) (Z.of_nat n)) (of_int 1%Z)) i = true.
Proof.
induction n;intros.
assert (Z.of_nat 0 <= to_uint i) by apply to_uint_bounds.
omega.
......@@ -1844,8 +1845,8 @@ Lemma nth_bit_pred_high :
case (Z_lt_le_dec (to_uint i) 1); intro.
right.
assert (to_uint i = 0).
pose (to_uint_bounds i).
auto with zarith.
assert (H' := to_uint_bounds i).
omega.
rewrite H1; apply nth_zeros_is_hd.
left.
......@@ -1933,10 +1934,11 @@ Lemma mask_correctness :
forall (j:Z),
(j < size -> (to_uint i) <= j -> j < (to_uint i + to_uint n)%Z -> nth mask j = true)
/\ (j < to_uint i \/ j >= to_uint i + to_uint n -> nth mask j = false).
Proof.
split;intros.
rewrite lsl_bv_is_lsl.
pose (to_uint_bounds i).
pose (size_in_range).
assert (a := to_uint_bounds i).
assert (u := size_in_range).
rewrite uint_in_range_power in u.
rewrite Lsl_nth_high; auto with zarith.
assert (j - to_uint i = to_uint (sub (of_int j) i)).
......@@ -1955,8 +1957,8 @@ Lemma mask_correctness :
apply Lsl_nth_low; auto with zarith.
rewrite lsl_bv_is_lsl.
pose (to_uint_bounds i) as u.
pose (to_uint_bounds n) as v.
assert (u := to_uint_bounds i).
assert (v := to_uint_bounds n).
pose size_in_range as w; rewrite uint_in_range_power in w.
assert (0 <= j) by auto with zarith.
......@@ -1983,6 +1985,7 @@ Qed.
(* Why3 goal *)
Lemma eq_sub_equiv : forall (a:t) (b:t) (i:t) (n:t), (eq_sub a b (to_uint i)
(to_uint n)) <-> (eq_sub_bv a b i n).
Proof.
intros a b i n.
unfold eq_sub, eq_sub_bv.
transitivity (eq_aux (bw_and b (lsl_bv (sub (lsl_bv (of_int 1) n) (of_int 1)) i))
......@@ -2007,7 +2010,7 @@ Lemma eq_sub_equiv : forall (a:t) (b:t) (i:t) (n:t), (eq_sub a b (to_uint i)
case (Z_lt_ge_dec j size); intro.
pose (to_uint_bounds i) as u; unfold uint_in_range in u.
assert (u := to_uint_bounds i); unfold uint_in_range in u.
assert (0 <= j < Z.of_nat size_nat) by auto with zarith.
pose (H j H1).
fold nth in e; rewrite Nth_bw_and, Nth_bw_and in e by auto.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment