Skip to content

why3
why3
Commit e905b926 authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files
Options

Convert to Flocq 3.1. 

This commit also removes some occurrences of 'fourier'.
parent 32f7576f
Hide whitespace changes
Inline Side-by-side
Showing with 644 additions and 709 deletions
CHANGES.md
View file @ e905b926
......@@ -49,6 +49,7 @@ Provers
* support for Z3 4.8.1 (released Oct 16, 2018)
* support for Z3 4.8.3 (released Nov 20, 2018)
* support for Z3 4.8.4 (released Dec 20, 2018)
* upgraded Coq realizations for floating-point arithmetic to Flocq 3.1
Version 1.1.1, December 17, 2018
--------------------------------
......
configure.in
View file @ e905b926
......@@ -728,14 +728,14 @@ fi
if test "$enable_coq_libs" = yes; then
AC_MSG_CHECKING([for Flocq])
AS_IF(
[ echo "Require Import Flocq.Flocq_version BinNat." \
"Goal (20500 <= Flocq_version)%N. easy. Qed." > conftest.v
[ echo "Require Import Flocq.Version BinNat." \
"Goal (30100 <= Flocq_version)%N. easy. Qed." > conftest.v
"$COQC" conftest.v > conftest.err ],
[ AC_MSG_RESULT(yes) ],
[ AC_MSG_RESULT(no)
enable_coq_fp_libs=no
AC_MSG_WARN(Cannot find Flocq.)
reason_coq_fp_libs=" (Flocq >= 2.5, < 3.0 not found)" ])
reason_coq_fp_libs=" (Flocq >= 3.1 not found)" ])
rm -f conftest.v conftest.vo conftest.err
fi
......
lib/coq/floating_point/GenFloat.v
View file @ e905b926
......@@ -21,8 +21,8 @@ Require real.Abs.
Require real.FromInt.
Require floating_point.Rounding.
Require Import Flocq.Core.Fcore.
Require Import Flocq.Appli.Fappli_IEEE.
Require Import Flocq.Core.Core.
Require Import Flocq.IEEE754.Binary.
Require Import int.Abs.
Section GenFloat.
......@@ -65,7 +65,7 @@ match goal with
end.
split.
split.
apply Fappli_IEEE.B754_zero.
apply B754_zero.
exact false.
exact R0.
exact R0.
......@@ -93,16 +93,11 @@ intros H _ _.
now injection H.
clear.
destruct (Bool.bool_dec xs ys) as [->|Hs].
destruct (Z_eq_dec (Zpos (proj1_sig xm')) (Zpos (proj1_sig ym'))) as [Hm'|Hm'].
destruct (Pos.eq_dec xm' ym') as [Hm'|Hm'].
left.
apply f_equal3 ; try easy.
apply f_equal2 ; try easy.
destruct xm' as [xm' pxm'].
destruct ym' as [ym' pym'].
simpl in Hm'.
injection Hm'.
intros ->.
now rewrite (eqbool_irrelevance _ pxm' pym').
revert e; rewrite Hm'; intros e.
now rewrite (eqbool_irrelevance _ e0 e).
right.
apply t_inv.
intros H _ _.
......@@ -142,7 +137,7 @@ Definition rnd_of_mode (m:mode) :=
Definition r_to_fp rnd x : binary_float prec emax :=
let r := round radix2 fexp (round_mode rnd) x in
let m := Ztrunc (scaled_mantissa radix2 fexp r) in
let e := canonic_exp radix2 fexp r in
let e := cexp radix2 fexp r in
binary_normalize prec emax Hprec' Hemax' rnd m e false.
Lemma is_finite_FF2B :
......@@ -166,7 +161,7 @@ Theorem r_to_fp_correct :
Proof with auto with typeclass_instances.
intros rnd x r Bx.
unfold r_to_fp. fold r.
generalize (binary_normalize_correct prec emax Hprec' Hemax' rnd (Ztrunc (scaled_mantissa radix2 fexp r)) (canonic_exp radix2 fexp r) false).
generalize (binary_normalize_correct prec emax Hprec' Hemax' rnd (Ztrunc (scaled_mantissa radix2 fexp r)) (cexp radix2 fexp r) false).
unfold r.
elim generic_format_round...
fold emin r.
......@@ -223,30 +218,30 @@ apply Rabs_le.
assert (generic_format radix2 fexp max).
apply generic_format_F2R.
intros H.
unfold canonic_exp.
rewrite ln_beta_F2R with (1 := H).
rewrite (ln_beta_unique _ _ prec).
unfold cexp.
rewrite mag_F2R with (1 := H).
rewrite (mag_unique _ _ prec).
ring_simplify (prec + (emax - prec))%Z.
unfold FLT_exp.
rewrite Zmax_l.
apply Zle_refl.
unfold emin.
generalize Hprec' Hemax' ; clear ; omega.
rewrite <- Z2R_abs, Zabs_eq, <- 2!Z2R_Zpower.
rewrite <- abs_IZR, Zabs_eq, <- 2!IZR_Zpower.
split.
apply Z2R_le.
apply IZR_le.
apply Zlt_succ_le.
change (2 ^ prec - 1)%Z with (Zpred (2^prec))%Z.
rewrite <- Zsucc_pred.
apply lt_Z2R.
apply lt_IZR.
change 2%Z with (radix_val radix2).
rewrite 2!Z2R_Zpower.
rewrite 2!IZR_Zpower.
apply bpow_lt.
apply Zlt_pred.
apply Zlt_le_weak.
exact Hprec'.
generalize Hprec' ; clear ; omega.
apply Z2R_lt.
apply IZR_lt.
apply Zlt_pred.
apply Zlt_le_weak.
exact Hprec'.
......@@ -299,7 +294,7 @@ Lemma Bounded_value : forall (x:t), ((Rabs (value x)) <= max)%R.
Proof with auto with typeclass_instances.
intros x.
replace max with (pred radix2 fexp (bpow radix2 emax)).
apply le_pred_lt...
apply pred_ge_gt...
apply generic_format_abs.
apply generic_format_B2R.
apply generic_format_bpow.
......@@ -308,7 +303,7 @@ zify ; generalize Hprec' Hemax' ; omega.
apply abs_B2R_lt_emax.
rewrite pred_eq_pos.
unfold pred_pos.
rewrite ln_beta_bpow.
rewrite mag_bpow.
ring_simplify (emax+1-1)%Z.
rewrite Req_bool_true by easy.
unfold FLT_exp, emin.
......@@ -317,7 +312,7 @@ unfold max, F2R; simpl.
pattern emax at 1; replace emax with (prec+(emax-prec))%Z by ring.
rewrite bpow_plus.
change 2%Z with (radix_val radix2).
rewrite Z2R_minus, Z2R_Zpower.
rewrite minus_IZR, IZR_Zpower.
simpl; ring.
apply Zlt_le_weak.
exact Hprec'.
......@@ -343,15 +338,13 @@ destruct (Zle_lt_or_eq _ _ H) as [Bz|Bz] ; clear H Hz.
apply generic_format_FLT.
exists (Float radix2 z 0).
unfold F2R ; simpl.
split.
rewrite Z2R_IZR.
now rewrite Rmult_1_r.
split. easy.
unfold emin; generalize Hprec' Hemax'; omega.
easy.
simpl; unfold emin; generalize Hprec' Hemax'; omega.
unfold max_representable_integer in Bz.
change 2%Z with (radix_val radix2) in Bz.
apply generic_format_abs_inv.
rewrite <- Z2R_IZR, <- Z2R_abs, Bz, Z2R_Zpower.
rewrite <- abs_IZR, Bz, IZR_Zpower.
apply generic_format_bpow.
unfold FLT_exp, emin.
clear Bz; generalize Hprec' Hemax'; zify.
......@@ -413,8 +406,8 @@ rewrite bpow_plus.
apply Rmult_lt_compat_r.
apply bpow_gt_0.
simpl.
rewrite <- Z2R_Zpower.
apply Z2R_lt.
rewrite <- IZR_Zpower.
apply IZR_lt.
apply Zlt_pred.
apply Zlt_le_weak.
exact Hprec'.
......
lib/coq/floating_point/Single.v
View file @ e905b926
......@@ -25,21 +25,25 @@ Require Import floating_point.GenFloat.
(* Why3 goal *)
Definition round : floating_point.Rounding.mode -> R -> R.
Proof.
exact (round 24 128).
Defined.
(* Why3 goal *)
Definition value : floating_point.SingleFormat.single -> R.
Proof.
exact (value 24 128).
Defined.
(* Why3 goal *)
Definition exact : floating_point.SingleFormat.single -> R.
Proof.
exact (exact 24 128).
Defined.
(* Why3 goal *)
Definition model : floating_point.SingleFormat.single -> R.
Proof.
exact (model 24 128).
Defined.
......@@ -57,8 +61,10 @@ Definition no_overflow (m:floating_point.Rounding.mode) (x:R) : Prop :=
(33554430 * 10141204801825835211973625643008)%R)%R.
Lemma max_single_eq: (33554430 * 10141204801825835211973625643008 = max 24 128)%R.
unfold max, Fcore_defs.F2R; simpl.
ring.
Proof.
unfold max, Defs.F2R.
simpl Raux.bpow.
now rewrite <- 2!mult_IZR.
Qed.
(* Why3 goal *)
......@@ -67,6 +73,7 @@ Lemma Bounded_real_no_overflow :
((Reals.Rbasic_fun.Rabs x) <=
(33554430 * 10141204801825835211973625643008)%R)%R ->
no_overflow m x.
Proof.
intros m x Hx.
unfold no_overflow.
rewrite max_single_eq in *.
......@@ -77,6 +84,7 @@ Qed.
Lemma Round_monotonic :
forall (m:floating_point.Rounding.mode) (x:R) (y:R), (x <= y)%R ->
((round m x) <= (round m y))%R.
Proof.
apply Round_monotonic.
easy.
Qed.
......@@ -86,6 +94,7 @@ Lemma Round_idempotent :
forall (m1:floating_point.Rounding.mode) (m2:floating_point.Rounding.mode)
(x:R),
((round m1 (round m2 x)) = (round m2 x)).
Proof.
now apply Round_idempotent.
Qed.
......@@ -94,6 +103,7 @@ Lemma Round_value :
forall (m:floating_point.Rounding.mode)
(x:floating_point.SingleFormat.single),
((round m (value x)) = (value x)).
Proof.
now apply Round_value.
Qed.
......@@ -102,6 +112,7 @@ Lemma Bounded_value :
forall (x:floating_point.SingleFormat.single),
((Reals.Rbasic_fun.Rabs (value x)) <=
(33554430 * 10141204801825835211973625643008)%R)%R.
Proof.
rewrite max_single_eq.
now apply Bounded_value.
Qed.
......@@ -119,12 +130,14 @@ Qed.
(* Why3 goal *)
Lemma Round_down_le :
forall (x:R), ((round floating_point.Rounding.Down x) <= x)%R.
Proof.
now apply Round_down_le.
Qed.
(* Why3 goal *)
Lemma Round_up_ge :
forall (x:R), (x <= (round floating_point.Rounding.Up x))%R.
Proof.
now apply Round_up_ge.
Qed.
......@@ -133,6 +146,7 @@ Lemma Round_down_neg :
forall (x:R),
((round floating_point.Rounding.Down (-x)%R) =
(-(round floating_point.Rounding.Up x))%R).
Proof.
now apply Round_down_neg.
Qed.
......@@ -141,12 +155,14 @@ Lemma Round_up_neg :
forall (x:R),
((round floating_point.Rounding.Up (-x)%R) =
(-(round floating_point.Rounding.Down x))%R).
Proof.
now apply Round_up_neg.
Qed.
(* Why3 goal *)
Definition round_logic :
floating_point.Rounding.mode -> R -> floating_point.SingleFormat.single.
Proof.
exact (round_logic 24 128 (refl_equal true) (refl_equal true)).
Defined.
......
lib/coq/ieee_float/Float32.v
View file @ e905b926
......@@ -26,8 +26,8 @@ Require bv.Pow2int.
Require ieee_float.RoundingMode.
Require ieee_float.GenericFloat.
Import Flocq.Core.Fcore.
Import Flocq.Appli.Fappli_IEEE.
Import Flocq.Core.Core.
Import Flocq.IEEE754.Binary.
Import ieee_float.RoundingMode.
Import ieee_float.GenericFloat.
......@@ -59,7 +59,7 @@ intros x _.
apply Rabs_le_inv.
change (Rabs (B2R _ _ x) <= F2R (Float radix2 (Zpower radix2 24 - 1) (127 - 23)))%R.
destruct x as [s|s|s|s m e H] ;
try (simpl ; rewrite Rabs_R0 ; now apply F2R_ge_0_compat).
try (simpl ; rewrite Rabs_R0 ; now apply F2R_ge_0).
simpl.
rewrite <- F2R_Zabs.
rewrite abs_cond_Zopp.
......@@ -67,15 +67,15 @@ apply andb_prop in H.
destruct H as [H1 H2].
apply Zeq_bool_eq in H1.
apply Zle_bool_imp_le in H2.
rewrite Fcore_digits.Zpos_digits2_pos in H1.
rewrite Digits.Zpos_digits2_pos in H1.
apply Rmult_le_compat.
now apply (Z2R_le 0).
now apply (IZR_le 0).
apply bpow_ge_0.
apply Z2R_le.
apply IZR_le.
apply (Z.lt_le_pred (Zabs (Zpos m)) (Zpower radix2 24)).
apply Fcore_digits.Zpower_gt_Zdigits.
apply Digits.Zpower_gt_Zdigits.
revert H1.
generalize (Fcore_digits.Zdigits radix2 (Z.pos m)).
generalize (Digits.Zdigits radix2 (Z.pos m)).
unfold FLT_exp, sb.
intros ; zify ; omega.
now apply bpow_le.
......@@ -114,13 +114,13 @@ Defined.
(* Why3 goal *)
Definition abs : t -> t.
Proof.
apply abs.
now apply abs.
Defined.
(* Why3 goal *)
Definition neg : t -> t.
Proof.
apply neg.
now apply neg.
Defined.
(* Why3 goal *)
......@@ -307,7 +307,7 @@ Lemma max_real_int :
((33554430 * 10141204801825835211973625643008)%R = (BuiltIn.IZR max_int)).
Proof.
unfold max_int.
now rewrite mult_IZR, <- !Z2R_IZR.
now rewrite mult_IZR.
Qed.
(* Why3 assumption *)
......
lib/coq/ieee_float/Float64.v
View file @ e905b926
......@@ -26,8 +26,8 @@ Require bv.Pow2int.
Require ieee_float.RoundingMode.
Require ieee_float.GenericFloat.
Import Flocq.Core.Fcore.
Import Flocq.Appli.Fappli_IEEE.
Import Flocq.Core.Core.
Import Flocq.IEEE754.Binary.
Import ieee_float.RoundingMode.
Import ieee_float.GenericFloat.
......@@ -61,7 +61,7 @@ intros x _.
apply Rabs_le_inv.
change (Rabs (B2R _ _ x) <= F2R (Float radix2 (Zpower radix2 53 - 1) (1023 - 52)))%R.
destruct x as [s|s|s|s m e H] ;
try (simpl ; rewrite Rabs_R0 ; now apply F2R_ge_0_compat).
try (simpl ; rewrite Rabs_R0 ; now apply F2R_ge_0).
simpl.
rewrite <- F2R_Zabs.
rewrite abs_cond_Zopp.
......@@ -69,15 +69,15 @@ apply andb_prop in H.
destruct H as [H1 H2].
apply Zeq_bool_eq in H1.
apply Zle_bool_imp_le in H2.
rewrite Fcore_digits.Zpos_digits2_pos in H1.
rewrite Digits.Zpos_digits2_pos in H1.
apply Rmult_le_compat.
now apply (Z2R_le 0).
now apply (IZR_le 0).
apply bpow_ge_0.
apply Z2R_le.
apply IZR_le.
apply (Z.lt_le_pred (Zabs (Zpos m)) (Zpower radix2 53)).
apply Fcore_digits.Zpower_gt_Zdigits.
apply Digits.Zpower_gt_Zdigits.
revert H1.
generalize (Fcore_digits.Zdigits radix2 (Z.pos m)).
generalize (Digits.Zdigits radix2 (Z.pos m)).
unfold FLT_exp, sb.
intros ; zify ; omega.
now apply bpow_le.
......@@ -116,13 +116,13 @@ Defined.
(* Why3 goal *)
Definition abs : t -> t.
Proof.
apply abs.
now apply abs.
Defined.
(* Why3 goal *)
Definition neg : t -> t.
Proof.
apply neg.
now apply neg.
Defined.
(* Why3 goal *)
......@@ -309,7 +309,7 @@ Lemma max_real_int :
= (BuiltIn.IZR max_int)).
Proof.
unfold max_int.
now rewrite mult_IZR, <- !Z2R_IZR.
now rewrite mult_IZR.
Qed.
(* Why3 assumption *)
......
lib/coq/ieee_float/GenericFloat.v
View file @ e905b926
This source diff could not be displayed because it is too large. You can view the blob instead.
lib/coq/real/Truncate.v
View file @ e905b926
......@@ -17,7 +17,7 @@ Require int.Int.
Require real.Real.
Require real.FromInt.
Require Import Flocq.Core.Fcore.
Require Import Flocq.Core.Core.
Require Import Fourier.
(* Why3 goal *)
......@@ -26,9 +26,7 @@ Notation truncate := Ztrunc.
(* Why3 goal *)
Lemma Truncate_int : forall (i:Z), ((truncate (BuiltIn.IZR i)) = i).
Proof.
intro i.
rewrite <-Z2R_IZR.
apply Ztrunc_Z2R.
exact Ztrunc_IZR.
Qed.
(* Why3 goal *)
......@@ -38,10 +36,10 @@ Lemma Truncate_down_pos :
(x < (BuiltIn.IZR ((truncate x) + 1%Z)%Z))%R.
Proof.
intros x h.
rewrite (Ztrunc_floor x h), <-Z2R_IZR, <-Z2R_IZR.
rewrite (Ztrunc_floor x h).
split.
apply Zfloor_lb.
rewrite Z2R_plus; simpl.
rewrite plus_IZR; simpl.
apply Zfloor_ub.
Qed.
......@@ -52,13 +50,13 @@ Lemma Truncate_up_neg :
(x <= (BuiltIn.IZR (truncate x)))%R.
Proof.
intros x h.
rewrite (Ztrunc_ceil x h), <-Z2R_IZR, <-Z2R_IZR.
rewrite (Ztrunc_ceil x h).
split;[|apply Zceil_ub].
case (Req_dec (Z2R (Zfloor x)) x); intro.
rewrite <-H, Zceil_Z2R, H, Z2R_minus; simpl.
case (Req_dec (IZR (Zfloor x)) x); intro.
rewrite <-H, Zceil_IZR, H, minus_IZR; simpl.
fourier.
rewrite (Zceil_floor_neq _ H).
rewrite Z2R_minus, Z2R_plus; simpl.
rewrite minus_IZR, plus_IZR; simpl.
pose proof (Zfloor_lb x).
destruct (Rle_lt_or_eq_dec _ _ H0); try easy.
fourier.
......@@ -71,15 +69,14 @@ Lemma Real_of_truncate :
((BuiltIn.IZR (truncate x)) <= (x + 1%R)%R)%R.
Proof.
intro x.
rewrite <- (Z2R_IZR (truncate x)).
destruct (Rle_lt_dec x 0).
+ rewrite Ztrunc_ceil; auto.
destruct (Req_dec (Z2R (Zfloor x)) x).
rewrite <-H at 2 3; rewrite Zceil_Z2R, H; split; fourier.
destruct (Req_dec (IZR (Zfloor x)) x).
rewrite <-H at 2 3; rewrite Zceil_IZR, H; split; fourier.
rewrite Zceil_floor_neq; auto.
pose proof (Zfloor_lb x);
pose proof (Zfloor_ub x).
rewrite Z2R_plus; simpl Z2R; split; fourier.
rewrite plus_IZR; split; fourier.
+ rewrite Ztrunc_floor by fourier.
pose proof (Zfloor_lb x);
pose proof (Zfloor_ub x).
......@@ -98,12 +95,11 @@ Lemma Truncate_monotonic_int1 :
forall (x:R) (i:Z), (x <= (BuiltIn.IZR i))%R -> ((truncate x) <= i)%Z.
Proof.
intros x i h.
rewrite <-Z2R_IZR in h.
destruct (Rle_lt_dec x 0).
+ rewrite Ztrunc_ceil; auto.
apply Zceil_glb; assumption.
+ rewrite Ztrunc_floor by fourier.
apply le_Z2R.
apply le_IZR.
apply Rle_trans with (r2:=x);[apply Zfloor_lb|assumption].
Qed.
......@@ -112,10 +108,9 @@ Lemma Truncate_monotonic_int2 :
forall (x:R) (i:Z), ((BuiltIn.IZR i) <= x)%R -> (i <= (truncate x))%Z.
Proof.
intros x i h.
rewrite <-Z2R_IZR in h.
destruct (Rle_lt_dec x 0).
+ rewrite Ztrunc_ceil; auto.
apply le_Z2R.
apply le_IZR.
apply Rle_trans with (r2:=x);[assumption|apply Zceil_ub].
+ rewrite Ztrunc_floor by fourier.
apply Zfloor_lub; assumption.
......@@ -130,15 +125,13 @@ Notation ceil := Zceil.
(* Why3 goal *)
Lemma Floor_int : forall (i:Z), ((floor (BuiltIn.IZR i)) = i).
Proof.
intro i; rewrite <-Z2R_IZR.
apply Zfloor_Z2R.
exact Zfloor_IZR.
Qed.
(* Why3 goal *)
Lemma Ceil_int : forall (i:Z), ((ceil (BuiltIn.IZR i)) = i).
Proof.
intro i; rewrite <-Z2R_IZR.
apply Zceil_Z2R.
exact Zceil_IZR.
Qed.
(* Why3 goal *)
......@@ -148,19 +141,19 @@ Lemma Floor_down :
(x < (BuiltIn.IZR ((floor x) + 1%Z)%Z))%R.
Proof.
intro x.
rewrite <-Z2R_IZR, <-Z2R_IZR; split.
split.
apply Zfloor_lb.
rewrite Z2R_plus.
rewrite plus_IZR.
apply Zfloor_ub.
Qed.
Lemma ceil_lb: forall x, ((Z2R (ceil x) - 1) < x).
Lemma ceil_lb: forall x, ((IZR (ceil x) - 1) < x).
Proof.
intro.
case (Req_dec (Z2R (Zfloor x)) x); intro.
rewrite <-H, Zceil_Z2R, H; simpl; fourier.
case (Req_dec (IZR (Zfloor x)) x); intro.
rewrite <-H, Zceil_IZR, H; simpl; fourier.
rewrite (Zceil_floor_neq _ H).
rewrite Z2R_plus; simpl.
rewrite plus_IZR; simpl.
pose proof (Zfloor_lb x).
destruct (Rle_lt_or_eq_dec _ _ H0); try easy.
fourier.
......@@ -172,8 +165,8 @@ Lemma Ceil_up :
((BuiltIn.IZR ((ceil x) - 1%Z)%Z) < x)%R /\ (x <= (BuiltIn.IZR (ceil x)))%R.
Proof.
intro x.
rewrite <-Z2R_IZR, <-Z2R_IZR; split; [|apply Zceil_ub].
rewrite Z2R_minus.
split; [|apply Zceil_ub].
rewrite minus_IZR.
apply ceil_lb.
Qed.
......
opam/why3-coq.opam
View file @ e905b926
......@@ -47,12 +47,7 @@ depends: [
]
depopts: [
"coq-flocq"
]
conflicts: [
"coq-flocq" {< "2.5"}
"coq-flocq" {>= "3.0~"}
"coq-flocq" {>= "3.1"}
]
synopsis: "Why3 environment for deductive program verification"
......
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