Commit 7cbd3090 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Fixed ordering of iff.

parent 4bb55b24
......@@ -33,7 +33,7 @@ now intros _ _.
Qed.
Theorem FIX_format_generic :
forall x : R, generic_format beta FIX_exp x <-> FIX_format x.
forall x : R, FIX_format x <-> generic_format beta FIX_exp x.
Proof.
split.
(* . *)
......
......@@ -49,10 +49,28 @@ omega.
Qed.
Theorem FLT_format_generic :
forall x : R, generic_format beta FLT_exp x <-> FLT_format x.
forall x : R, FLT_format x <-> generic_format beta FLT_exp x.
Proof.
split.
(* . *)
intros ((xm, xe), (Hx1, (Hx2, Hx3))).
destruct (Req_dec x 0) as [Hx4|Hx4].
rewrite Hx4.
apply generic_format_0.
simpl in Hx2, Hx3.
unfold generic_format, canonic, FLT_exp.
destruct (ln_beta beta x) as (ex, Hx5).
simpl.
specialize (Hx5 Hx4).
destruct (Zmax_spec (ex - prec) emin) as [(H1,H2)|(H1,H2)] ;
rewrite H2 ; clear H2.
rewrite Hx1, (F2R_prec_normalize beta xm xe ex prec Hx2).
now eexists.
now rewrite <- Hx1.
rewrite Hx1, (F2R_change_exp beta emin).
now eexists.
exact Hx3.
(* . *)
intros ((xm, xe), (Hx1, Hx2)).
destruct (Req_dec x 0) as [Hx3|Hx3].
exists (Float beta 0 emin).
......@@ -90,31 +108,15 @@ apply abs_F2R.
now apply Zlt_le_weak.
rewrite Hx2.
apply Zle_max_r.
(* . *)
intros ((xm, xe), (Hx1, (Hx2, Hx3))).
destruct (Req_dec x 0) as [Hx4|Hx4].
rewrite Hx4.
apply generic_format_0.
simpl in Hx2, Hx3.
unfold generic_format, canonic, FLT_exp.
destruct (ln_beta beta x) as (ex, Hx5).
simpl.
specialize (Hx5 Hx4).
destruct (Zmax_spec (ex - prec) emin) as [(H1,H2)|(H1,H2)] ;
rewrite H2 ; clear H2.
rewrite Hx1, (F2R_prec_normalize beta xm xe ex prec Hx2).
now eexists.
now rewrite <- Hx1.
rewrite Hx1, (F2R_change_exp beta emin).
now eexists.
exact Hx3.
Qed.
Theorem FLT_format_satisfies_any :
satisfies_any FLT_format.
Proof.
refine (satisfies_any_eq _ _ _ (generic_format_satisfies_any beta FLT_exp _)).
exact FLT_format_generic.
intros x.
apply iff_sym.
apply FLT_format_generic.
exact FLT_exp_correct.
Qed.
......@@ -134,11 +136,11 @@ intros Hx2.
destruct (Req_dec x 0) as [Hx3|Hx3].
(* . . *)
rewrite Hx3.
apply -> FLT_format_generic.
apply <- FLT_format_generic.
apply generic_format_0.
(* . . *)
destruct (proj2 (FLX_format_generic _ _ Hp x) Hx2) as ((xm, xe), (Hx4, Hx5)).
apply -> FLT_format_generic.
destruct (proj1 (FLX_format_generic _ _ Hp x) Hx2) as ((xm, xe), (Hx4, Hx5)).
apply <- FLT_format_generic.
rewrite Hx4.
eexists ; repeat split.
rewrite Hx5. clear Hx5.
......@@ -190,10 +192,10 @@ clear.
intros x Ha.
unfold Rabs in Ha.
destruct (Rcase_abs x) as [Hx|Hx].
apply -> FLT_format_generic.
apply <- FLT_format_generic.
rewrite <- (Ropp_involutive x).
apply generic_format_sym.
now apply <- FLT_format_generic.
now apply -> FLT_format_generic.
exact Ha.
(* . . *)
intros _.
......
......@@ -85,12 +85,13 @@ now apply Zpower_gt_1.
Qed.
Theorem FLX_format_generic :
forall x : R, generic_format beta FLX_exp x <-> FLX_format x.
forall x : R, FLX_format x <-> generic_format beta FLX_exp x.
Proof.
intros x.
destruct (Req_dec x 0) as [Hx|Hx1].
(* . *)
split ; intros H ; rewrite Hx.
apply generic_format_0.
exists (Float beta 0 0).
split.
unfold F2R. simpl.
......@@ -98,28 +99,28 @@ now rewrite Rmult_0_l.
apply Zpower_gt_0.
now apply Zlt_le_trans with (2 := radix_prop beta).
now apply Zlt_le_weak.
apply generic_format_0.
(* . *)
destruct (ln_beta beta x) as (ex, Hx2).
simpl.
specialize (Hx2 Hx1).
apply iff_trans with (generic_format beta (FIX_exp (ex - prec)) x).
apply iff_trans with (FIX_format beta (ex - prec) x).
apply FLX_format_FIX.
exact (conj (proj1 Hx2) (Rlt_le _ _ (proj2 Hx2))).
apply FIX_format_generic.
assert (Hf: FLX_exp (projT1 (ln_beta beta x)) = FIX_exp (ex - prec) (projT1 (ln_beta beta x))).
unfold FIX_exp, FLX_exp.
now rewrite ln_beta_unique with (1 := Hx2).
split ; apply generic_format_fun_eq ; now rewrite Hf.
apply iff_trans with (FIX_format beta (ex - prec) x).
apply FIX_format_generic.
apply iff_sym.
apply FLX_format_FIX.
exact (conj (proj1 Hx2) (Rlt_le _ _ (proj2 Hx2))).
Qed.
Theorem FLX_format_satisfies_any :
satisfies_any FLX_format.
Proof.
refine (satisfies_any_eq _ _ _ (generic_format_satisfies_any beta FLX_exp _)).
exact FLX_format_generic.
intros x.
apply iff_sym.
apply FLX_format_generic.
exact FLX_exp_correct.
Qed.
......@@ -201,7 +202,7 @@ exact H5.
intros ((xm, xe), (H1, H2)).
destruct (Req_dec x 0) as [H3|H3].
rewrite H3.
apply -> FLX_format_generic.
apply <- FLX_format_generic.
apply generic_format_0.
specialize (H2 H3). clear H3.
rewrite H1.
......@@ -215,8 +216,8 @@ Proof.
refine (satisfies_any_eq _ _ _ (generic_format_satisfies_any beta FLX_exp _)).
split ; intros H.
apply -> FLX_format_FLXN.
now apply -> FLX_format_generic.
apply <- FLX_format_generic.
now apply <- FLX_format_generic.
apply -> FLX_format_generic.
now apply <- FLX_format_FLXN.
exact FLX_exp_correct.
Qed.
......
......@@ -49,10 +49,42 @@ split ; intros ; omega.
Qed.
Theorem FTZ_format_generic :
forall x : R, generic_format beta FTZ_exp x <-> FTZ_format x.
forall x : R, FTZ_format x <-> generic_format beta FTZ_exp x.
Proof.
split.
(* . *)
intros ((xm, xe), (Hx1, (Hx2, Hx3))).
destruct (Req_dec x 0) as [Hx4|Hx4].
rewrite Hx4.
apply generic_format_0.
specialize (Hx2 Hx4).
unfold generic_format, canonic, FTZ_exp.
destruct (ln_beta beta x) as (ex, Hx6).
simpl.
specialize (Hx6 Hx4).
generalize (Zlt_cases (ex - prec) emin).
case (Zlt_bool (ex - prec) emin) ; intros H1.
elim (Rlt_not_ge _ _ (proj2 Hx6)).
apply Rle_ge.
rewrite Hx1.
apply Rle_trans with (bpow (prec - 1) * bpow emin)%R.
rewrite <- epow_add.
apply -> epow_le.
omega.
rewrite abs_F2R.
unfold F2R. simpl.
apply Rmult_le_compat.
apply epow_ge_0.
apply epow_ge_0.
rewrite <- Z2R_Zpower.
now apply Z2R_le.
apply Zle_minus_le_0.
now apply (Zlt_le_succ 0).
now apply -> epow_le.
rewrite Hx1, (F2R_prec_normalize beta xm xe ex prec (proj2 Hx2)).
now eexists.
now rewrite <- Hx1.
(* . *)
intros ((xm, xe), (Hx1, Hx2)).
destruct (Req_dec x 0) as [Hx3|Hx3].
exists (Float beta 0 emin).
......@@ -120,45 +152,15 @@ now apply Zlt_le_weak.
simpl.
rewrite Hx2.
now apply Zge_le.
(* . *)
intros ((xm, xe), (Hx1, (Hx2, Hx3))).
destruct (Req_dec x 0) as [Hx4|Hx4].
rewrite Hx4.
apply generic_format_0.
specialize (Hx2 Hx4).
unfold generic_format, canonic, FTZ_exp.
destruct (ln_beta beta x) as (ex, Hx6).
simpl.
specialize (Hx6 Hx4).
generalize (Zlt_cases (ex - prec) emin).
case (Zlt_bool (ex - prec) emin) ; intros H1.
elim (Rlt_not_ge _ _ (proj2 Hx6)).
apply Rle_ge.
rewrite Hx1.
apply Rle_trans with (bpow (prec - 1) * bpow emin)%R.
rewrite <- epow_add.
apply -> epow_le.
omega.
rewrite abs_F2R.
unfold F2R. simpl.
apply Rmult_le_compat.
apply epow_ge_0.
apply epow_ge_0.
rewrite <- Z2R_Zpower.
now apply Z2R_le.
apply Zle_minus_le_0.
now apply (Zlt_le_succ 0).
now apply -> epow_le.
rewrite Hx1, (F2R_prec_normalize beta xm xe ex prec (proj2 Hx2)).
now eexists.
now rewrite <- Hx1.
Qed.
Theorem FTZ_format_satisfies_any :
satisfies_any FTZ_format.
Proof.
refine (satisfies_any_eq _ _ _ (generic_format_satisfies_any beta FTZ_exp _)).
exact FTZ_format_generic.
intros x.
apply iff_sym.
apply FTZ_format_generic.
exact FTZ_exp_correct.
Qed.
......@@ -174,7 +176,7 @@ destruct (Req_dec x 0) as [H4|H4].
intros _.
rewrite H4.
apply -> FLX_format_FLXN.
apply -> FLX_format_generic.
apply <- FLX_format_generic.
apply generic_format_0.
exact Hp.
exact Hp.
......
......@@ -388,7 +388,7 @@ assert (Hd4: (bpow (ex - 1) <= Rabs xd < bpow ex)%R).
rewrite Rabs_pos_eq.
split.
apply Hxd.
apply <- FLX_format_generic.
apply -> FLX_format_generic.
exists (Float beta 1 (ex - 1)).
split.
apply sym_eq.
......@@ -408,7 +408,7 @@ apply (Rlt_not_le _ _ Hu).
apply Rnd_UP_pt_monotone with (generic_format beta FLXf) x (bpow ex).
exact Hxu.
split.
apply <- FLX_format_generic.
apply -> FLX_format_generic.
exists (Float beta 1 ex).
split.
apply sym_eq.
......@@ -537,7 +537,7 @@ intros x f Hf.
apply Rnd_NE_pt_aux.
apply DN_UP_parity_aux.
exact DN_UP_parity_FLX_pos.
now apply <- FLX_format_generic.
now apply -> FLX_format_generic.
Qed.
End Flocq_rnd_NE_FLX.
......@@ -631,7 +631,7 @@ intros x f Hf.
apply Rnd_NE_pt_aux.
apply DN_UP_parity_aux.
exact DN_UP_parity_FLT_pos.
now apply <- FLT_format_generic.
now apply -> FLT_format_generic.
Qed.
End Flocq_rnd_NE_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