Commit ce356884 authored by MARCHE Claude's avatar MARCHE Claude

Coq support: BV_Gen theory compatibility with 8.4 and 8.5

parent d64f9981
......@@ -876,6 +876,21 @@ ifeq (@enable_coq_support@,yes)
ifeq (@enable_coq_libs@,yes)
COQVERSIONSPECIFIC=bv/BV_Gen.v
COQVERSIONSPECIFICTARGETS=$(addprefix lib/coq/, $(COQVERSIONSPECIFIC))
COQVERSIONSPECIFICSOURCES=$(addsuffix .@coq_compat_version@, $(COQVERSIONSPECIFICTARGETS))
$(COQVERSIONSPECIFICTARGETS): $(COQVERSIONSPECIFICSOURCES)
for i in $(COQVERSIONSPECIFIC); do \
cp lib/coq/$$i.@coq_compat_version@ lib/coq/$$i ; \
done
clean::
rm -f $(COQVERSIONSPECIFICTARGETS)
COQLIBS_INT_FILES = Abs ComputerDivision Div2 EuclideanDivision Int MinMax Power NumOf
COQLIBS_INT_ALL_FILES = Exponentiation $(COQLIBS_INT_FILES)
COQLIBS_INT = $(addprefix lib/coq/int/, $(COQLIBS_INT_ALL_FILES))
......
This diff is collapsed.
......@@ -74,7 +74,7 @@ Defined.
Definition set: forall {a:Type} {a_WT:WhyType a}, (seq a) -> Z -> a -> (seq
a).
admit.
Defined.
Admitted.
(* Why3 goal *)
Lemma set_def1 : forall {a:Type} {a_WT:WhyType a}, forall (s:(seq a)) (i:Z)
......@@ -82,14 +82,14 @@ Lemma set_def1 : forall {a:Type} {a_WT:WhyType a}, forall (s:(seq a)) (i:Z)
v)) = (length s)).
intros a a_WT s i v (h1,h2).
admit.
Qed.
Admitted.
(* Why3 goal *)
Lemma set_def2 : forall {a:Type} {a_WT:WhyType a}, forall (s:(seq a)) (i:Z)
(v:a), ((0%Z <= i)%Z /\ (i < (length s))%Z) -> ((get (set s i v) i) = v).
intros a a_WT s i v (h1,h2).
admit.
Qed.
Admitted.
(* Why3 goal *)
Lemma set_def3 : forall {a:Type} {a_WT:WhyType a}, forall (s:(seq a)) (i:Z)
......@@ -98,7 +98,7 @@ Lemma set_def3 : forall {a:Type} {a_WT:WhyType a}, forall (s:(seq a)) (i:Z)
j) = (get s j))).
intros a a_WT s i v (h1,h2) j (h3,h4) h5.
admit.
Qed.
Admitted.
(* Why3 assumption *)
Definition infix_eqeq {a:Type} {a_WT:WhyType a} (s1:(seq a)) (s2:(seq
......@@ -243,7 +243,7 @@ rewrite (Zabs2Nat.id (Datatypes.length l)). omega.
subst i.
rewrite (Zabs2Nat.id (Datatypes.length l)). omega.
*)
Qed.
Admitted.
(* Why3 goal *)
Lemma snoc_last : forall {a:Type} {a_WT:WhyType a}, forall (s:(seq a)) (x:a),
......@@ -296,7 +296,7 @@ unfold length, infix_plpl.
rewrite List.app_length.
rewrite Nat2Z.inj_add. auto.
*)
Qed.
Admitted.
(* Why3 goal *)
Lemma concat_get1 : forall {a:Type} {a_WT:WhyType a}, forall (s1:(seq a))
......
......@@ -404,6 +404,7 @@ theory BV64
constant two_power_size = two_power_size,
constant max_int = max_int
meta "remove_prop" prop size_pos
meta "remove_prop" prop two_power_size_val
meta "remove_prop" prop max_int_val
......@@ -419,6 +420,7 @@ theory BV32
constant two_power_size = two_power_size,
constant max_int = max_int
meta "remove_prop" prop size_pos
meta "remove_prop" prop two_power_size_val
meta "remove_prop" prop max_int_val
......@@ -434,6 +436,7 @@ theory BV16
constant two_power_size = two_power_size,
constant max_int = max_int
meta "remove_prop" prop size_pos
meta "remove_prop" prop two_power_size_val
meta "remove_prop" prop max_int_val
......@@ -449,6 +452,7 @@ theory BV8
constant two_power_size = two_power_size,
constant max_int = max_int
meta "remove_prop" prop size_pos
meta "remove_prop" prop two_power_size_val
meta "remove_prop" prop max_int_val
......
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