MAJ terminée. Nous sommes passés en version 14.6.2 . Pour consulter les "releases notes" associées c'est ici :

https://about.gitlab.com/releases/2022/01/11/security-release-gitlab-14-6-2-released/
https://about.gitlab.com/releases/2022/01/04/gitlab-14-6-1-released/

Commit 218d843c authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files

Proved FIX using generic format.

parent a0cf797a
......@@ -39,20 +39,12 @@ Definition FLT_format (emin prec : Z) (x : R) :=
exists f : float beta,
x = F2R f /\ (Zabs (Fnum f) < Zpower (radix_val beta) prec)%Z /\ (emin <= Fexp f)%Z.
(* fixed-point format *)
Definition FIX_format (emin : Z) (x : R) :=
exists f : float beta,
x = F2R f /\ (Fexp f = emin)%Z.
Definition FLX_RoundingModeP (prec : Z) (rnd : R -> R):=
Rounding_for_Format (FLX_format prec) rnd.
Definition FLT_RoundingModeP (emin prec : Z) (rnd : R -> R):=
Rounding_for_Format (FLT_format emin prec) rnd.
Definition FIX_RoundingModeP (emin : Z) (rnd : R -> R):=
Rounding_for_Format (FIX_format emin) rnd.
End Def.
Implicit Arguments Fnum [[beta]].
......
Require Import Flocq_Raux.
Require Import Flocq_defs.
Require Import Flocq_rnd_ex.
Require Import Flocq_rnd_generic.
Section RND_FIX.
Open Scope R_scope.
Variable beta : radix.
Notation bpow := (epow beta).
Variable emin : Z.
(* fixed-point format *)
Definition FIX_format (x : R) :=
exists f : float beta,
x = F2R f /\ (Fexp f = emin)%Z.
Definition FIX_RoundingModeP (rnd : R -> R):=
Rounding_for_Format FIX_format rnd.
Theorem FIX_format_satisfies_any :
satisfies_any (FIX_format beta emin).
satisfies_any FIX_format.
Proof.
refine ((fun D => Satisfies_any _ _ _ (projT1 D) (projT2 D)) _).
(* symmetric set *)
pose (fexp (e : Z) := emin).
(* . *)
destruct (generic_format_satisfies_any beta fexp) as (Hzero, Hsym, rnd, Hrnd).
intros k.
unfold fexp.
split ; intros H.
now apply Zlt_le_weak.
split.
apply Zle_refl.
now intros _ _.
(* . *)
assert (Heq : forall x, generic_format beta fexp x <-> FIX_format x).
split.
intros ((xm, xe), (Hx1, Hx2)).
destruct (Req_dec x 0) as [Hx3|Hx3].
exists (Float beta 0 emin).
repeat split.
unfold F2R. simpl.
now rewrite Rmult_0_l.
destruct Hx2 as [Hx2|Hx2].
now elim Hx3.
exists (Float beta xm emin).
repeat split.
rewrite Hx1.
apply (f_equal (fun e => F2R (Float beta xm e))).
simpl in Hx2.
unfold fexp in Hx2.
apply Hx2.
now apply Rabs_pos_lt.
intros ((xm, xe), (Hx1, Hx2)).
destruct (Req_dec x 0) as [Hx3|Hx3].
exists (Float beta 0 0).
split.
unfold F2R.
unfold F2R. simpl.
now rewrite Rmult_0_l.
apply refl_equal.
intros x ((m,e),(H1,H2)).
exists (Float beta (-m) emin).
now left.
exists (Float beta xm (fexp xe)).
split.
unfold fexp.
now rewrite <- Hx2.
right.
split.
rewrite H1.
unfold F2R.
simpl.
rewrite opp_Z2R, Ropp_mult_distr_l_reverse.
now rewrite <- H2.
apply refl_equal.
(* rounding down *)
exists (fun x => F2R (Float beta (up (x * bpow (Zopp emin)) - 1) emin)).
(* . *)
refine (Satisfies_any _ _ _ rnd _).
now apply -> Heq.
intros x Hx.
apply -> Heq.
apply Hsym.
now apply <- Heq.
intros x.
set (m := up (x * bpow (Zopp emin))).
set (f := Float beta (m - 1) emin).
destruct (Hrnd x) as (H1, (H2, H3)).
split.
now exists f.
now apply -> Heq.
split.
unfold F2R, f, m.
simpl.
pattern x at 2 ; rewrite <- Rmult_1_r.
change 1 with (bpow Z0).
rewrite <- (Zplus_opp_l emin).
rewrite epow_add.
rewrite <- Rmult_assoc.
apply Rmult_le_compat_r.
apply epow_ge_0.
generalize (x * bpow (- emin)%Z)%R.
clear.
intros.
rewrite minus_Z2R.
simpl.
apply Rminus_le.
replace (Z2R (up r) - 1 - r) with ((Z2R (up r) - r) - 1) by ring.
apply Rle_minus.
rewrite Z2R_IZR.
eapply for_base_fp.
intros g ((mx,ex),(H1,H2)) H3.
rewrite H1.
unfold F2R.
rewrite H2.
simpl.
apply Rmult_le_compat_r.
apply epow_ge_0.
apply Z2R_le.
apply Zlt_succ_le.
apply lt_Z2R.
apply Rmult_lt_reg_r with (bpow emin).
apply epow_gt_0.
apply Rle_lt_trans with x.
rewrite <- H2.
change (F2R (Float beta mx ex) <= x).
now rewrite <- H1.
pattern x ; rewrite <- Rmult_1_r.
change R1 with (bpow Z0).
rewrite <- (Zplus_opp_l emin).
rewrite epow_add.
rewrite <- Rmult_assoc.
apply Rmult_lt_compat_r.
apply epow_gt_0.
change (m - 1)%Z with (Zpred m).
rewrite <- Zsucc_pred.
rewrite Z2R_IZR.
eapply archimed.
exact H2.
intros g Hg Hgx.
apply H3 ; try assumption.
now apply <- Heq.
Qed.
End RND_FIX.
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