Commit 36d94772 authored by MARCHE Claude's avatar MARCHE Claude

Coq realizations: allow correct update-coq without warnings

parent f57a7f13
......@@ -8,7 +8,10 @@ Require int.Abs.
Require int.EuclideanDivision.
Require bv.Pow2int.
Parameter last_bit : nat.
Local Parameter last_bit : nat.
(* Important notice: do not remove 'Local' above, otherwise 'why3 realize' will
assume it comes from Why3 and will remove it. We use 'Parameter' instead of
'Variable' to avoid a Coq warning *)
Definition size_nat: nat := S last_bit.
......@@ -205,7 +208,6 @@ 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.
......@@ -716,7 +718,7 @@ Lemma twos_complement_extensionality : forall {m} (v v' : Bvector m),
apply Vector.case0 with (v := v'); trivial.
revert v h H.
apply Vector.caseS with (v := v'); intros.
assert (tmp : forall {n} v v',
assert (tmp : forall {n} v v',
twos_complement (S n) (false :: v) <> twos_complement (S n) (true :: v')).
intros n1 v0 v'0 H1.
assert ((twos_complement (S n1) (true :: v'0) >= 0)%Z).
......@@ -1704,7 +1706,7 @@ Lemma mask_succ :
Qed.
Definition add_aux {l} (v w : Vector.t bool l) : Vector.t bool l :=
nat_to_bvec l (Z.to_nat (mod1
nat_to_bvec l (Z.to_nat (mod1
(Z.of_nat (bvec_to_nat l v) + Z.of_nat (bvec_to_nat l w))
(Pow2int.pow2 (Z.of_nat l)))).
......@@ -1765,7 +1767,7 @@ Lemma mask_succ_tmp :
intros; apply bvec_to_nat_extensionality.
apply bvec_to_nat_nat_to_bvec.
apply Z.lt_le_pred.
rewrite <-Z2Nat.id by (transitivity (Pow2int.pow2 (Z.of_nat l0) - 1);
rewrite <-Z2Nat.id by (transitivity (Pow2int.pow2 (Z.of_nat l0) - 1);
[apply max_int_nat|auto with zarith]).
apply inj_lt, bvec_to_nat_range.
rewrite nat_to_bvec_bvec_to_nat.
......@@ -2011,3 +2013,4 @@ Lemma Extensionality : forall (x:t) (y:t), (eq_sub x y 0%Z size) -> (x = y).
intros x y.
apply Extensionality_aux.
Qed.
......@@ -52,7 +52,10 @@ Defined.
Coercion mode_to_IEEE : mode >-> Fappli_IEEE.mode.
Axiom eb_pos sb_pos : positive.
Local Axiom eb_pos sb_pos : positive.
(* Important notice: do not remove 'Local' above, otherwise 'why3 realize' will
assume it comes from Why3 and will remove it. We use 'Axiom' instead of
'Hypothesis' to avoid a Coq warning *)
(* Why3 goal *)
Definition eb: Z.
......@@ -64,8 +67,8 @@ Definition sb: Z.
exact (Z.pos sb_pos).
Defined.
Axiom Heb : Zlt_bool 1 eb = true.
Axiom Hsbb : Zlt_bool 1 sb = true.
Local Axiom Heb : Zlt_bool 1 eb = true.
Local Axiom Hsbb : Zlt_bool 1 sb = true.
(* Why3 goal *)
Lemma eb_gt_1 : (1%Z < eb)%Z.
......@@ -101,7 +104,7 @@ Notation fexp := (FLT_exp emin sb).
Lemma Hsb : Zlt_bool 0 sb = true. auto with zarith. Qed.
Lemma Hsb': (0 < sb)%Z. unfold sb; auto with zarith. Qed.
Axiom Hemax : Zlt_bool sb emax = true. (* put as assumption in theory ? *)
Local Axiom Hemax : Zlt_bool sb emax = true. (* put as assumption in theory ? *)
Lemma Hemax': (sb < emax)%Z.
rewrite Zlt_is_lt_bool.
......
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