Commit cdfa7d0e authored by Guillaume Melquiond's avatar Guillaume Melquiond

Change _format predicates into inductive types.

parent 4b515a47
Version 3.0.0:
- stripped prefix from all the file names, renamed some files
- renamed canonic_exp into cexp, canonic into canonical
- changed FLX, FIX, FLT, FLXN, FTZ_format into inductive types
Version 2.5.2:
- ensured compatibility from Coq 8.4 to 8.6
......
......@@ -51,34 +51,32 @@ Proof with auto with typeclass_instances.
intros u Fu.
apply generic_format_FLT.
apply FLT_format_generic in Fu...
destruct Fu as (uf, (H1,(H2,H3))).
destruct Fu as [uf H1 H2 H3].
exists (Float radix2 (Fnum uf) (Fexp uf+1)).
split.
rewrite H1; unfold F2R; simpl.
rewrite bpow_plus, bpow_1.
simpl;ring.
split.
now simpl.
simpl; apply Zle_trans with (1:=H3).
omega.
easy.
apply Zle_trans with (1:=H3).
apply Zle_succ.
Qed.
Lemma FLT_format_half: forall u,
format u -> bpow (prec+emin) <= Rabs u -> format (u/2).
Proof with auto with typeclass_instances.
intros u Fu H.
apply FLT_format_generic in Fu...
destruct Fu as ((n,e),(H1,(H2,H3))).
destruct Fu as [[n e] H1 H2 H3].
simpl in H1, H2, H3.
apply generic_format_FLT.
exists (Float radix2 n (e-1)).
split; simpl.
rewrite H1; unfold F2R; simpl.
unfold Zminus; rewrite bpow_plus.
simpl; unfold Rdiv; ring.
split;[assumption|idtac].
assert (prec + emin < prec +e)%Z;[idtac|omega].
easy.
simpl.
cut (prec + emin < prec +e)%Z.
simpl ; omega.
apply lt_bpow with radix2.
apply Rle_lt_trans with (1:=H).
rewrite H1; unfold F2R; simpl.
......@@ -90,10 +88,9 @@ apply bpow_gt_0.
rewrite <- Z2R_abs.
rewrite <- Z2R_Zpower.
now apply Z2R_lt.
unfold Prec_gt_0 in prec_gt_0_; omega.
now apply Zlt_le_weak.
Qed.
Lemma FLT_round_half: forall z, bpow (prec+emin) <= Rabs z ->
round_flt (z/2)= round_flt z /2.
Proof with auto with typeclass_instances.
......@@ -147,9 +144,7 @@ rewrite bpow_plus.
simpl; field.
unfold Zminus; rewrite bpow_plus.
simpl; field.
Qed.
Qed.
Lemma FLT_ulp_le_id: forall u, bpow emin <= u -> ulp_flt u <= u.
Proof with auto with typeclass_instances.
......@@ -1141,7 +1136,7 @@ Lemma average3_no_underflow_aux1: forall f, format f -> 0 < f ->
Proof with auto with typeclass_instances.
intros f Ff Hf1 Hf2.
apply FLT_format_generic in Ff...
destruct Ff as (g, (H1,(H2,H3))).
destruct Ff as [g H1 H2 H3].
case (Zle_lt_or_eq emin (Fexp g)); try exact H3; intros H4.
contradict Hf2.
apply Rlt_not_le.
......@@ -1153,12 +1148,10 @@ apply Rmult_lt_0_compat; try assumption.
auto with real.
apply generic_format_FLT.
exists (Float radix2 (Fnum g) (Fexp g-1)).
split.
rewrite H1; unfold F2R; simpl.
unfold Zminus; rewrite bpow_plus.
simpl; field.
split.
now simpl.
apply Rmult_assoc.
easy.
simpl; omega.
contradict Hf2; apply Rlt_not_le.
unfold round, scaled_mantissa.
......@@ -1305,8 +1298,8 @@ pose (b:=(u+v)/2); fold b.
intros (H1,H2).
apply generic_format_FIX_FLT,FIX_format_generic in Fu.
apply generic_format_FIX_FLT,FIX_format_generic in Fv.
destruct Fu as ((nu,eu),(J1,J2)).
destruct Fv as ((nv,ev),(J3,J4)); simpl in J2, J4.
destruct Fu as [[nu eu] J1 J2].
destruct Fv as [[nv ev] J3 J4]; simpl in J2, J4.
(* b is bpow emin /2 *)
assert (b = Z2R (nu+nv) * bpow (emin-1)).
unfold b; rewrite J1, J3; unfold F2R; rewrite J2,J4; simpl.
......@@ -1579,15 +1572,15 @@ replace (2*b) with (u+v).
2: unfold b; field.
apply generic_format_FIX_FLT,FIX_format_generic in Fu.
apply generic_format_FIX_FLT,FIX_format_generic in Fv.
destruct Fu as (fu,(J1,J2)).
destruct Fv as (fv,(J3,J4)).
destruct Fu as [fu J1 J2].
destruct Fv as [fv J3 J4].
apply generic_format_FIX.
exists (Float radix2 (Fnum fu+Fnum fv) emin).
split;[idtac|reflexivity].
rewrite J1,J3; unfold F2R; simpl.
rewrite J2,J4, Z2R_plus; ring.
easy.
apply FIX_format_generic in H.
destruct H as ((n,e),(J1,J2)).
destruct H as [[n e] J1 J2].
rewrite J1; unfold F2R; rewrite J2.
simpl; rewrite Rabs_mult.
pattern (bpow emin) at 1; rewrite <- (Rmult_1_l (bpow emin)).
......@@ -1603,7 +1596,8 @@ apply Z.abs_pos.
intros M; apply K1.
apply Rmult_eq_reg_l with 2.
2: apply Rgt_not_eq, Rlt_gt; now auto with real.
rewrite Rmult_0_r, J1,M; unfold F2R; simpl; ring.
rewrite Rmult_0_r, J1, M.
apply F2R_0.
rewrite Rabs_mult.
rewrite Rabs_right.
2: apply Rle_ge; auto with real.
......
......@@ -28,10 +28,9 @@ Notation bpow := (bpow beta).
Variable emin : Z.
(* fixed-point format with exponent emin *)
Definition FIX_format (x : R) :=
exists f : float beta,
x = F2R f /\ (Fexp f = emin)%Z.
Inductive FIX_format (x : R) : Prop :=
FIX_spec : forall f : float beta,
x = F2R f -> (Fexp f = emin)%Z -> FIX_format x.
Definition FIX_exp (e : Z) := emin.
......@@ -51,7 +50,7 @@ Qed.
Theorem generic_format_FIX :
forall x, FIX_format x -> generic_format beta FIX_exp x.
Proof.
intros x ((xm, xe), (Hx1, Hx2)).
intros x [[xm xe] Hx1 Hx2].
rewrite Hx1.
now apply generic_format_canonical.
Qed.
......@@ -80,7 +79,8 @@ intros ex ey H.
apply Zle_refl.
Qed.
Theorem ulp_FIX: forall x, ulp beta FIX_exp x = bpow emin.
Theorem ulp_FIX :
forall x, ulp beta FIX_exp x = bpow emin.
Proof.
intros x; unfold ulp.
case Req_bool_spec; intros Zx.
......@@ -91,5 +91,4 @@ intros n _; reflexivity.
reflexivity.
Qed.
End RND_FIX.
......@@ -31,10 +31,10 @@ Variable emin prec : Z.
Context { prec_gt_0_ : Prec_gt_0 prec }.
(* floating-point format with gradual underflow *)
Definition FLT_format (x : R) :=
exists f : float beta,
x = F2R f /\ (Zabs (Fnum f) < Zpower beta prec)%Z /\ (emin <= Fexp f)%Z.
Inductive FLT_format (x : R) : Prop :=
FLT_spec : forall f : float beta,
x = F2R f -> (Zabs (Fnum f) < Zpower beta prec)%Z ->
(emin <= Fexp f)%Z -> FLT_format x.
Definition FLT_exp e := Zmax (e - prec) emin.
......@@ -52,7 +52,7 @@ Theorem generic_format_FLT :
forall x, FLT_format x -> generic_format beta FLT_exp x.
Proof.
clear prec_gt_0_.
intros x ((mx, ex), (H1, (H2, H3))).
intros x [[mx ex] H1 H2 H3].
simpl in H2, H3.
rewrite H1.
apply generic_format_F2R.
......
......@@ -34,10 +34,9 @@ Class Prec_gt_0 :=
Context { prec_gt_0_ : Prec_gt_0 }.
(* unbounded floating-point format *)
Definition FLX_format (x : R) :=
exists f : float beta,
x = F2R f /\ (Zabs (Fnum f) < Zpower beta prec)%Z.
Inductive FLX_format (x : R) : Prop :=
FLX_spec : forall f : float beta,
x = F2R f -> (Zabs (Fnum f) < Zpower beta prec)%Z -> FLX_format x.
Definition FLX_exp (e : Z) := (e - prec)%Z.
......@@ -58,7 +57,7 @@ Theorem FIX_format_FLX :
FIX_format beta (e - prec) x.
Proof.
clear prec_gt_0_.
intros x e Hx ((xm, xe), (H1, H2)).
intros x e Hx [[xm xe] H1 H2].
rewrite H1, (F2R_prec_normalize beta xm xe e prec).
now eexists.
exact H2.
......@@ -70,7 +69,6 @@ Theorem FLX_format_generic :
Proof.
intros x H.
rewrite H.
unfold FLX_format.
eexists ; repeat split.
simpl.
apply lt_Z2R.
......@@ -96,7 +94,7 @@ Theorem generic_format_FLX :
forall x, FLX_format x -> generic_format beta FLX_exp x.
Proof.
clear prec_gt_0_.
intros x ((mx,ex),(H1,H2)).
intros x [[mx ex] H1 H2].
simpl in H2.
rewrite H1.
apply generic_format_F2R.
......@@ -133,15 +131,16 @@ apply Zle_refl.
Qed.
(** unbounded floating-point format with normal mantissas *)
Definition FLXN_format (x : R) :=
exists f : float beta,
x = F2R f /\ (x <> R0 ->
Zpower beta (prec - 1) <= Zabs (Fnum f) < Zpower beta prec)%Z.
Inductive FLXN_format (x : R) : Prop :=
FLXN_spec : forall f : float beta,
x = F2R f ->
(x <> R0 -> Zpower beta (prec - 1) <= Zabs (Fnum f) < Zpower beta prec)%Z ->
FLXN_format x.
Theorem generic_format_FLXN :
forall x, FLXN_format x -> generic_format beta FLX_exp x.
Proof.
intros x ((xm,ex),(H1,H2)).
intros x [[xm ex] H1 H2].
destruct (Req_dec x 0) as [Zx|Zx].
rewrite Zx.
apply generic_format_0.
......@@ -158,10 +157,10 @@ Proof.
intros x Hx.
rewrite Hx.
simpl.
eexists ; split. split.
simpl.
eexists. easy.
rewrite <- Hx.
intros Zx.
simpl.
split.
(* *)
apply le_Z2R.
......
......@@ -31,11 +31,12 @@ Variable emin prec : Z.
Context { prec_gt_0_ : Prec_gt_0 prec }.
(* floating-point format with abrupt underflow *)
Definition FTZ_format (x : R) :=
exists f : float beta,
x = F2R f /\ (x <> R0 -> Zpower beta (prec - 1) <= Zabs (Fnum f) < Zpower beta prec)%Z /\
(emin <= Fexp f)%Z.
Inductive FTZ_format (x : R) : Prop :=
FTZ_spec : forall f : float beta,
x = F2R f ->
(x <> R0 -> Zpower beta (prec - 1) <= Zabs (Fnum f) < Zpower beta prec)%Z ->
(emin <= Fexp f)%Z ->
FTZ_format x.
Definition FTZ_exp e := if Zlt_bool (e - prec) emin then (emin + prec - 1)%Z else (e - prec)%Z.
......@@ -68,9 +69,10 @@ Qed.
Theorem FLXN_format_FTZ :
forall x, FTZ_format x -> FLXN_format beta prec x.
Proof.
intros x ((xm, xe), (Hx1, (Hx2, Hx3))).
intros x [[xm xe] Hx1 Hx2 Hx3].
eexists.
apply (conj Hx1 Hx2).
exact Hx1.
exact Hx2.
Qed.
Theorem generic_format_FTZ :
......@@ -80,7 +82,7 @@ intros x Hx.
cut (generic_format beta (FLX_exp prec) x).
apply generic_inclusion_ln_beta.
intros Zx.
destruct Hx as ((xm, xe), (Hx1, (Hx2, Hx3))).
destruct Hx as [[xm xe] Hx1 Hx2 Hx3].
simpl in Hx2, Hx3.
specialize (Hx2 Zx).
assert (Zxm: xm <> Z0).
......@@ -103,12 +105,9 @@ Theorem FTZ_format_generic :
forall x, generic_format beta FTZ_exp x -> FTZ_format x.
Proof.
intros x Hx.
destruct (Req_dec x 0) as [Hx3|Hx3].
destruct (Req_dec x 0) as [->|Hx3].
exists (Float beta 0 emin).
split.
unfold F2R. simpl.
now rewrite Rmult_0_l.
split.
apply sym_eq, F2R_0.
intros H.
now elim H.
apply Zle_refl.
......
......@@ -250,14 +250,14 @@ apply generic_format_FLT_FIX...
rewrite Zplus_comm; assumption.
apply generic_format_FIX_FLT, FIX_format_generic in Fx.
apply generic_format_FIX_FLT, FIX_format_generic in Fy.
destruct Fx as (nx,(H1x,H2x)).
destruct Fy as (ny,(H1y,H2y)).
destruct Fx as [nx H1x H2x].
destruct Fy as [ny H1y H2y].
apply generic_format_FIX.
exists (Float beta (Fnum nx+Fnum ny)%Z emin).
split;[idtac|reflexivity].
rewrite H1x,H1y; unfold F2R; simpl.
rewrite H2x, H2y.
rewrite Z2R_plus; ring.
easy.
Qed.
End Fprop_plus_FLT.
......
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