Commit e9f1f968 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Moved format-specific theorems to their respective files.

parent 6fe707a1
......@@ -2,6 +2,7 @@ Require Import Flocq_Raux.
Require Import Flocq_defs.
Require Import Flocq_rnd_ex.
Require Import Flocq_rnd_generic.
Require Import Flocq_rnd_ne.
Section RND_FIX.
......@@ -56,4 +57,13 @@ exact FIX_format_generic.
exact FIX_exp_correct.
Qed.
Theorem Rnd_NE_pt_FIX :
rounding_pred (Rnd_NE_pt beta FIX_exp).
Proof.
apply Rnd_NE_pt_rounding.
apply FIX_exp_correct.
right.
split ; easy.
Qed.
End RND_FIX.
......@@ -5,6 +5,7 @@ Require Import Flocq_rnd_generic.
Require Import Flocq_float_prop.
Require Import Flocq_rnd_FLX.
Require Import Flocq_rnd_FIX.
Require Import Flocq_rnd_ne.
Section RND_FLT.
......@@ -253,4 +254,27 @@ now apply Zpower_gt_1.
omega.
Qed.
Theorem Rnd_NE_pt_FLT :
Zodd (radix_val beta) \/ (1 < prec)%Z ->
rounding_pred (Rnd_NE_pt beta FLT_exp).
Proof.
intros H.
apply Rnd_NE_pt_rounding.
apply FLT_exp_correct.
destruct H.
now left.
right.
intros e.
unfold FLT_exp.
destruct (Zmax_spec (e - prec) emin) as [(H1,H2)|(H1,H2)].
rewrite H2.
generalize (Zmax_spec (e + 1 - prec) emin).
generalize (Zmax_spec (e - prec + 1 - prec) emin).
omega.
rewrite H2.
generalize (Zmax_spec (e + 1 - prec) emin).
generalize (Zmax_spec (emin + 1 - prec) emin).
omega.
Qed.
End RND_FLT.
......@@ -4,6 +4,7 @@ Require Import Flocq_rnd_ex.
Require Import Flocq_rnd_generic.
Require Import Flocq_float_prop.
Require Import Flocq_rnd_FIX.
Require Import Flocq_rnd_ne.
Section RND_FLX.
......@@ -219,4 +220,17 @@ now apply <- FLX_format_FLXN.
exact FLX_exp_correct.
Qed.
Theorem Rnd_NE_pt_FLX :
Zodd (radix_val beta) \/ (1 < prec)%Z ->
rounding_pred (Rnd_NE_pt beta FLX_exp).
Proof.
intros H.
apply Rnd_NE_pt_rounding.
apply FLX_exp_correct.
destruct H.
now left.
right.
unfold FLX_exp ; split ; omega.
Qed.
End RND_FLX.
......@@ -5,9 +5,6 @@ Require Import Flocq_rnd_prop.
Require Import Flocq_rnd_generic.
Require Import Flocq_float_prop.
Require Import Flocq_ulp.
Require Import Flocq_rnd_FIX.
Require Import Flocq_rnd_FLX.
Require Import Flocq_rnd_FLT.
Section Flocq_rnd_NE.
......@@ -15,8 +12,6 @@ Variable beta : radix.
Notation bpow e := (bpow beta e).
Section Flocq_rnd_NE_generic.
Variable fexp : Z -> Z.
Variable prop_exp : valid_exp fexp.
......@@ -183,7 +178,7 @@ ring_simplify (ex - fexp ex + fexp ex)%Z.
rewrite Hu2, Hud.
unfold ulp.
rewrite ln_beta_unique with beta x ex.
unfold FLX_exp, F2R.
unfold F2R.
simpl. ring.
rewrite Rabs_pos_eq.
exact Hex.
......@@ -285,72 +280,11 @@ apply sym_eq.
now apply Rnd_DN_pt_idempotent with (1 := Hd).
Qed.
End Flocq_rnd_NE_generic.
Section Flocq_rnd_NE_FIX.
Variable emin : Z.
Theorem DN_UP_parity_FIX_pos :
DN_UP_parity_pos_prop (FIX_exp emin).
Proof.
apply DN_UP_parity_generic_pos.
apply FIX_exp_correct.
right.
split ; easy.
Qed.
End Flocq_rnd_NE_FIX.
Section Flocq_rnd_NE_FLX.
Variable prec : Z.
Hypothesis Hp : (0 < prec)%Z.
Theorem DN_UP_parity_FLX_pos :
Zodd (radix_val beta) \/ (1 < prec)%Z ->
DN_UP_parity_pos_prop (FLX_exp prec).
Proof.
intros H.
apply DN_UP_parity_generic_pos.
now apply FLX_exp_correct.
destruct H.
now left.
right.
unfold FLX_exp ; split ; omega.
Qed.
End Flocq_rnd_NE_FLX.
Section Flocq_rnd_NE_FLT.
Variable emin : Z.
Variable prec : Z.
Hypothesis Hp : (0 < prec)%Z.
Theorem DN_UP_parity_FLT_pos :
Zodd (radix_val beta) \/ (1 < prec)%Z ->
DN_UP_parity_pos_prop (FLT_exp emin prec).
Proof.
intros H.
apply DN_UP_parity_generic_pos.
now apply FLT_exp_correct.
destruct H.
now left.
right.
intros e.
unfold FLT_exp.
destruct (Zmax_spec (e - prec) emin) as [(H1,H2)|(H1,H2)].
rewrite H2.
generalize (Zmax_spec (e + 1 - prec) emin).
generalize (Zmax_spec (e - prec + 1 - prec) emin).
omega.
rewrite H2.
generalize (Zmax_spec (e + 1 - prec) emin).
generalize (Zmax_spec (emin + 1 - prec) emin).
omega.
Theorem Rnd_NE_pt_rounding :
rounding_pred Rnd_NE_pt.
split.
apply Rnd_NE_pt_total.
apply Rnd_NE_pt_monotone.
Qed.
End Flocq_rnd_NE_FLT.
End Flocq_rnd_NE.
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