Skip to content
Snippets Groups Projects
Commit 041e82e2 authored by Arthur Correnson's avatar Arthur Correnson
Browse files

[ieee/coq] organizing the lemmas in modules

parent 765c7cb1
No related branches found
No related tags found
1 merge request!16Fp/ieee
Pipeline #36468 waiting for manual action
Stage: test
Stage: deploy
Hide whitespace changes
Inline Side-by-side
src_common/ieee/coq/Correction_thms.v
+ 6
− 6
View file @ 041e82e2
......@@ -154,7 +154,7 @@ Proof.
rewrite (Bplus_correct m a c Hnan1).
rewrite (Bplus_correct m b c Hnan2).
apply round_le.
apply add_leb_compat.
apply add_leb_mono_l.
fdestruct a; fdestruct b; simpl.
- apply Raux.Rle_bool_true; lra.
- apply Raux.Rle_bool_true; lra.
......@@ -185,7 +185,7 @@ Proof.
pose proof (Raux.bpow_gt_0 Zaux.radix2 e).
nra.
- destruct s, s0; simpl; try easy;
apply Bleb_le in Hab; auto;
apply Bleb_Rle in Hab; auto;
now apply Raux.Rle_bool_true.
Qed.
......@@ -201,7 +201,7 @@ Proof.
rewrite (Bplus_correct m c a Hnan1).
rewrite (Bplus_correct m c b Hnan2).
apply round_le.
apply add_leb_compat_l.
apply add_leb_mono_r.
fdestruct a; fdestruct b; simpl.
- apply Raux.Rle_bool_true; lra.
- apply Raux.Rle_bool_true; lra.
......@@ -232,7 +232,7 @@ Proof.
pose proof (Raux.bpow_gt_0 Zaux.radix2 e).
nra.
- destruct s, s0; simpl; try easy;
apply Bleb_le in Hab; auto;
apply Bleb_Rle in Hab; auto;
now apply Raux.Rle_bool_true.
Qed.
......@@ -250,10 +250,10 @@ Proof.
rewrite (Bplus_correct m c d); auto.
eapply leb_trans.
- apply round_le.
apply add_leb_compat.
apply add_leb_mono_l.
apply (le_B2Rx _ _ H1).
- apply round_le.
apply add_leb_compat_l.
apply add_leb_mono_r.
apply (le_B2Rx _ _ H2).
Qed.
......
src_common/ieee/coq/Interval.v
+ 2
− 185
View file @ 041e82e2
......@@ -84,11 +84,10 @@ Proof.
repeat (rewrite Bplus_correct; auto).
apply round_le.
eapply leb_trans.
- apply (add_leb_compat _ _ _ (le_B2Rx _ _ H)).
- apply (add_leb_compat_l _ _ _ (le_B2Rx _ _ H')).
- apply (add_leb_mono_l _ _ _ (le_B2Rx _ _ H)).
- apply (add_leb_mono_r _ _ _ (le_B2Rx _ _ H')).
Qed.
Definition Interval := { I : Interval_aux | valid_interval I }.
Program Definition Iadd (m : mode) (I1 I2 : Interval) : Interval :=
......@@ -98,23 +97,6 @@ Next Obligation.
now destruct I1, I2.
Defined.
Lemma Bplus_nan_inv :
forall (m : mode) (x y:float), is_nan (Bplus m x y) = true ->
x = +oo /\ y = -oo \/ x = -oo /\ y = +oo \/ x = NaN \/ y = NaN.
Proof.
intros; fdestruct x; fdestruct y; auto.
- now destruct m.
- now destruct m.
- now rewrite Bplus_finites_not_nan in H.
Qed.
Lemma Bplus_not_nan_inv' :
forall (m : mode) (x y:float), is_nan (Bplus m x y) = false ->
~(x = +oo /\ y = -oo) /\ ~(x = -oo /\ y = +oo) /\ (is_nan x = false) /\ (is_nan y = false).
Proof.
intros; repeat split; fdestruct x; fdestruct y.
Qed.
Program Lemma Iadd_correct :
forall m (I1 I2 : Interval) (x y : float), contains I1 x -> contains I2 y -> contains (Iadd m I1 I2) (Bplus m x y).
Proof.
......@@ -176,168 +158,6 @@ Proof.
+ fdestruct y; fdestruct x; destruct n; simpl; intuition.
Qed.
Lemma Bleb_refl :
forall x:float, is_nan x = false -> Bleb x x = true.
Proof.
intros x Hx; fdestruct x.
apply le_Bleb; auto; lra.
Qed.
Lemma Bleb_false_Bltb :
forall x y:float, is_nan x = false -> is_nan y = false -> Bleb x y = false -> Bltb y x = true.
Proof.
intros x y Hx Hy Hxy.
destruct x as [ | [ ] | | ] eqn:Ex, y as [ | [ ] | | ] eqn:Ey; try easy; rewrite <- Ex, <- Ey in *;
unfold Bleb, SpecFloat.SFleb in Hxy;
replace (SpecFloat.SFcompare (B2SF _) (B2SF _)) with (Bcompare x y) in Hxy by auto;
assert (Fx: is_finite x = true) by (rewrite Ex; auto);
assert (Fy: is_finite y = true) by (rewrite Ey; auto);
rewrite (Bcompare_correct _ _ x y Fx Fy) in Hxy; auto;
destruct (Raux.Rcompare _ _) eqn:E; try easy;
apply Raux.Rcompare_Gt_inv in E;
apply lt_Bltb; auto.
Qed.
Definition Bmax (f1 f2 : float) : float :=
if is_nan f1 || is_nan f2 then NaN
else if Bleb f1 f2 then f2
else f1.
Definition Bmin (f1 f2 : float) : float :=
if is_nan f1 || is_nan f2 then NaN
else if Bleb f1 f2 then f1
else f2.
Lemma Bmax_max_1 :
forall x y, (Bmax x y = x \/ Bmax x y = y).
Proof.
intros [ ] [ ]; unfold Bmax; destruct Bleb; intuition.
Qed.
Lemma Bltb_Bleb :
forall x y : float, Bltb x y = true -> Bleb x y = true.
Proof.
intros x y Hxy.
fdestruct x; fdestruct y;
apply le_Bleb; auto;
apply Bltb_lt in Hxy; auto;
lra.
Qed.
Lemma Bmax_max_2 :
forall x y, is_finite x = true -> is_finite y = true -> x <= Bmax x y /\ y <= Bmax x y.
Proof.
intros x y Fx Fy; unfold Bmax.
assert (HnanX: is_nan x = false) by fdestruct x.
assert (HnanY: is_nan y = false) by fdestruct y.
rewrite HnanX, HnanY; simpl.
split.
- destruct (Bleb x y) eqn:?; auto.
apply Bleb_refl; fdestruct x.
- destruct (Bleb x y) eqn:E.
+ apply Bleb_refl; fdestruct y.
+ apply Bleb_false_Bltb in E; auto.
now apply Bltb_Bleb in E.
Qed.
Lemma Bmax_le :
forall x y z : float, x <= z -> y <= z -> Bmax x y <= z.
Proof.
intros x y z Hxz Hyz.
assert (HnanX: is_nan x = false) by fdestruct x.
assert (HnanY: is_nan y = false) by fdestruct y.
unfold Bmax.
rewrite HnanX, HnanY; simpl.
now destruct (Bleb x y).
Qed.
Lemma Bmax_not_nan_inv :
forall x y, is_nan (Bmax x y) = false -> is_nan x = false /\ is_nan y = false.
Proof.
intros; split.
+ fdestruct x.
+ fdestruct x; fdestruct y.
Qed.
Lemma Bmin_not_nan_inv :
forall x y, is_nan (Bmin x y) = false -> is_nan x = false /\ is_nan y = false.
Proof.
intros; split.
+ fdestruct x.
+ fdestruct x; fdestruct y.
Qed.
Lemma Bmax_le_inv :
forall x y z : float, Bmax x y <= z -> x <= z /\ y <= z.
Proof.
intros x y z Hxyz.
assert (is_nan (Bmax x y) = false) by (fdestruct (Bmax x y)).
unfold Bmax in Hxyz.
apply Bmax_not_nan_inv in H.
destruct H as [H1 H2].
rewrite H1, H2 in Hxyz.
simpl in *.
destruct (Bleb x y) eqn:E; split; auto.
- now apply (Bleb_trans _ _ x y z).
- apply Bleb_false_Bltb in E; auto.
apply Bltb_Bleb in E; auto.
now apply (Bleb_trans _ _ y x z).
Qed.
Lemma Bmin_min_1 :
forall x y, (Bmin x y = x \/ Bmin x y = y).
Proof.
intros [ ] [ ]; unfold Bmin; destruct Bleb; intuition.
Qed.
Lemma Bmin_min_2 :
forall x y, is_finite x = true -> is_finite y = true -> Bmin x y <= x /\ Bmin x y <= y.
Proof.
intros x y Fx Fy; unfold Bmin.
assert (HnanX: is_nan x = false) by fdestruct x.
assert (HnanY: is_nan y = false) by fdestruct y.
rewrite HnanX, HnanY; simpl.
split.
- destruct (Bleb x y) eqn:?.
+ apply Bleb_refl; fdestruct x.
+ assert (Hx : is_nan x = false) by (fdestruct x).
assert (Hy : is_nan y = false) by (fdestruct y).
apply Bleb_false_Bltb in Heqb; auto.
apply Bltb_lt in Heqb; auto.
apply le_Bleb; auto.
lra.
- destruct (Bleb x y) eqn:E; auto.
apply Bleb_refl; fdestruct y.
Qed.
Lemma Bmin_le :
forall x y z : float, z <= x -> z <= y -> z <= Bmin x y.
Proof.
intros x y z Hxz Hyz.
assert (HnanX: is_nan x = false) by (fdestruct z; fdestruct x).
assert (HnanY: is_nan y = false) by (fdestruct z; fdestruct y).
unfold Bmin.
rewrite HnanX, HnanY; simpl.
now destruct (Bleb x y).
Qed.
Lemma Bmin_le_inv :
forall x y z : float, z <= Bmin x y -> z <= x /\ z <= y.
Proof.
intros x y z Hxyz.
assert (is_nan (Bmin x y) = false) by (fdestruct (Bmin x y); fdestruct z).
unfold Bmin in Hxyz.
apply Bmin_not_nan_inv in H.
destruct H as [H1 H2].
rewrite H1, H2 in Hxyz.
simpl in *.
destruct (Bleb x y) eqn:E; split; auto.
- now apply (Bleb_trans _ _ z x y).
- apply Bleb_false_Bltb in E; auto.
apply Bltb_Bleb in E.
now apply (Bleb_trans _ _ z y x).
Qed.
Definition inter_aux (I1 I2 : Interval_aux) : Interval_aux :=
match I1, I2 with
| I_Bot, _ => I_Bot
......@@ -351,7 +171,6 @@ Definition inter_aux (I1 I2 : Interval_aux) : Interval_aux :=
else I_intv (Bmax l l') (Bmin h h') (b && b')
end.
Lemma valid_interval_inter :
forall I1 I2, valid_interval I1 -> valid_interval I2 -> valid_interval (inter_aux I1 I2).
Proof.
......@@ -379,8 +198,6 @@ Next Obligation.
now apply valid_interval_inter.
Defined.
Compute (inter_aux (I_intv (-oo) (-oo) true) (I_intv (+oo) (+oo) true)).
Program Lemma inter_correct_l :
forall I1 I2, forall x, contains (inter I1 I2) x -> contains I1 x.
Proof.
......
src_common/ieee/coq/Rextended.v
+ 38
− 102
View file @ 041e82e2
From Flocq Require Import IEEE754.BinarySingleNaN.
From Coq Require Import ZArith Psatz Reals.
(*********************************************************
Extension of R with special values +oo, -oo
**********************************************************)
From Flocq Require Import IEEE754.BinarySingleNaN.
From Coq Require Import ZArith Psatz Reals.
From F Require Import Utils.
Set Implicit Arguments.
(**
Usefull facts & definitions about R
*)
Section Rutils.
Definition sign (r : R) :=
......@@ -61,6 +65,9 @@ Qed.
End Rutils.
(**
Inject BinarySingleNan in R extended with infinities
*)
Section Rextended.
Variable prec : Z.
......@@ -106,61 +113,20 @@ Proof.
+ lia.
Qed.
(** Futils *)
Lemma le_Bleb :
forall (x y : float),
is_finite x = true ->
is_finite y = true ->
(B2R x <= B2R y)%R ->
Bleb x y = true.
Proof.
intros x y Fx Fy Hxy.
unfold Bleb, SpecFloat.SFleb.
replace (SpecFloat.SFcompare (_ x) (_ y)) with (Bcompare x y) by auto.
rewrite (Bcompare_correct _ _ x y Fx Fy).
destruct Raux.Rcompare eqn:E; try easy.
apply Raux.Rcompare_Gt_inv in E; lra.
Qed.
Lemma lt_Bltb :
forall (x y : float),
is_finite x = true ->
is_finite y = true ->
(B2R x < B2R y)%R ->
Bltb x y = true.
Proof.
intros x y Fx Fy Hxy.
unfold Bltb, SpecFloat.SFltb.
replace (SpecFloat.SFcompare (_ x) (_ y)) with (Bcompare x y) by auto.
rewrite (Bcompare_correct _ _ x y Fx Fy).
destruct Raux.Rcompare eqn:E; auto.
- apply Raux.Rcompare_Eq_inv in E; lra.
- apply Raux.Rcompare_Gt_inv in E; lra.
Qed.
Lemma F_fmax_max :
forall (x : float), is_finite x = true -> Bleb x F_fmax = true.
Proof.
intros [ [ ] | [ ] | | [ ] m e Hbound'] Fx; auto.
apply le_Bleb; auto.
apply Rle_Bleb; auto.
rewrite <- R2F_fmax.
now apply bounded_le_emax_minus_prec.
Qed.
(** Futils *)
Lemma pos_Bopp_neg :
forall m e Hb, @B754_finite prec emax true m e Hb = Bopp (B754_finite false m e Hb).
Proof. reflexivity. Qed.
Lemma neg_Bopp_pos :
forall m e Hb, @B754_finite prec emax false m e Hb = Bopp (B754_finite true m e Hb).
Proof. reflexivity. Qed.
Lemma F_fmax_min :
forall (x : float), is_finite x = true -> Bleb (Bopp F_fmax) x = true.
Proof.
intros [ [ ] | [ ] | | [ ] m e Hbound'] Fx; auto.
apply le_Bleb; auto.
apply Rle_Bleb; auto.
rewrite pos_Bopp_neg, B2R_Bopp, B2R_Bopp, <- R2F_fmax.
apply Ropp_le_contravar.
now apply bounded_le_emax_minus_prec.
......@@ -172,31 +138,6 @@ Proof.
apply minus_pos_lt, Raux.bpow_gt_0.
Qed.
Lemma Bleb_le :
forall x y : float, is_finite x = true -> is_finite y = true ->
Bleb x y = true -> (B2R x <= B2R y)%R.
Proof.
intros x y Fx Fy H.
unfold Bleb, SpecFloat.SFleb in H.
replace (SpecFloat.SFcompare (_ x) (_ y)) with (Bcompare x y) in H by auto.
rewrite (Bcompare_correct _ _ x y Fx Fy) in H.
destruct (Raux.Rcompare) eqn:E in H; try easy.
+ apply Raux.Rcompare_Eq_inv in E; lra.
+ apply Raux.Rcompare_Lt_inv in E; lra.
Qed.
Lemma Bltb_lt :
forall x y : float, is_finite x = true -> is_finite y = true ->
Bltb x y = true -> (B2R x < B2R y)%R.
Proof.
intros x y Fx Fy H.
unfold Bltb, SpecFloat.SFltb in H.
replace (SpecFloat.SFcompare (_ x) (_ y)) with (Bcompare x y) in H by auto.
rewrite (Bcompare_correct _ _ x y Fx Fy) in H.
destruct (Raux.Rcompare) eqn:E in H; try easy.
apply Raux.Rcompare_Lt_inv in E; lra.
Qed.
Definition leb (x y : Rx) :=
match x with
| Inf true => true
......@@ -279,7 +220,7 @@ Definition round (m : mode) (r : Rx) : Rx :=
| _ => r
end.
Lemma sign_le :
Lemma pos_Rleb_neg :
forall r1 r2,
sign r1 = false ->
sign r2 = true ->
......@@ -291,7 +232,7 @@ Proof.
apply Raux.Rle_bool_false; lra.
Qed.
Lemma Rle_le :
Lemma Rleb_Rle :
forall r1 r2, Raux.Rle_bool r1 r2 = true -> (r1 <= r2)%R.
Proof.
intros.
......@@ -339,7 +280,7 @@ Proof.
apply generic_format_Rimax.
Qed.
Lemma Rlt_lt :
Lemma Rltb_lt :
forall x y, Raux.Rlt_bool x y = true -> (x < y)%R.
Proof.
intros.
......@@ -382,15 +323,15 @@ Proof.
- unfold do_overflow in H.
unfold Rabs in H.
destruct Rcase_abs.
+ apply Rle_le in H.
+ apply Rleb_Rle in H.
right. apply Raux.Rle_bool_true.
apply Ropp_le_contravar in H.
replace (rx) with (--rx)%R by lra.
subst rx; auto.
+ apply Rle_le in H.
+ apply Rleb_Rle in H.
left. apply Raux.Rle_bool_true.
auto.
- destruct H; apply Raux.Rle_bool_true; apply Rle_le in H.
- destruct H; apply Raux.Rle_bool_true; apply Rleb_Rle in H.
+ eauto using Rle_trans, H, Rle_abs.
+ apply Ropp_le_contravar in H.
replace (--R_imax)%R with R_imax in H by lra.
......@@ -403,12 +344,7 @@ Proof.
auto.
Qed.
Lemma overflow_le :
Lemma overflow_is_le :
forall m r1 r2,
(r1 <= r2)%R ->
(0 <= r1)%R ->
......@@ -417,14 +353,14 @@ Lemma overflow_le :
Proof.
intros m r1 r2 Hle Hr1 Ho.
rewrite do_overflow_iff in Ho. destruct Ho as [H | H].
- apply Rle_le in H.
- apply Rleb_Rle in H.
rewrite do_overflow_iff. left.
apply Raux.Rle_bool_true.
eapply Generic_fmt.round_le in Hle.
+ eapply Rle_trans; [apply H | apply Hle].
+ now apply fexp_correct.
+ intuition.
- apply Rle_le in H.
- apply Rleb_Rle in H.
assert (-R_imax < 0)%R.
{ assert (R_imax > 0)%R by apply R_imax_gt_0. lra. }
pose proof H0.
......@@ -443,7 +379,7 @@ Proof.
+ intuition.
Qed.
Lemma overflow_le' :
Lemma overflow_is_ge :
forall m r1 r2,
(r1 <= r2)%R ->
(r2 <= 0)%R ->
......@@ -452,7 +388,7 @@ Lemma overflow_le' :
Proof.
intros m r1 r2 Hle Hr1 Ho.
rewrite do_overflow_iff in Ho. destruct Ho as [H | H].
- apply Rle_le in H.
- apply Rleb_Rle in H.
rewrite <- (round_Rimax m) in H.
eapply (Generic_fmt.round_le Zaux.radix2 fexp (round_mode m)) in Hr1; intuition.
rewrite Generic_fmt.round_0 in Hr1.
......@@ -464,7 +400,7 @@ Proof.
rewrite (round_Rimax m) in H0.
lra.
+ intuition.
- apply Rle_le in H.
- apply Rleb_Rle in H.
rewrite do_overflow_iff. right.
apply Raux.Rle_bool_true.
apply (Generic_fmt.round_le Zaux.radix2 fexp (round_mode m)) in Hle.
......@@ -499,12 +435,12 @@ Proof.
| [ Ho1 : do_overflow _ _ = false |- _ ] =>
apply Raux.Rle_bool_true;
destruct (dont_overflow_inv _ _ Ho1) as (f & [?Hreq ?Hf]);
rewrite ?Hreq; first [now apply Bleb_le, F_fmax_min | now apply Bleb_le, F_fmax_max ]
rewrite ?Hreq; first [now apply Bleb_Rle, F_fmax_min | now apply Bleb_Rle, F_fmax_max ]
end.
Ltac freals :=
match goal with
| [ H : Raux.Rle_bool _ _ = true |- _ ] =>
apply Raux.Rle_bool_true; apply Rle_le in H;
apply Raux.Rle_bool_true; apply Rleb_Rle in H;
now apply Generic_fmt.round_le; fformat
end.
Ltac finfinites :=
......@@ -512,7 +448,7 @@ Proof.
Ltac absurd_sign :=
match goal with
| [ Hs2 : sign _ = true, Hs1 : sign _ = false, H : Raux.Rle_bool _ _ = true |- _ ] =>
now rewrite (sign_le _ _ Hs1 Hs2) in H
now rewrite (pos_Rleb_neg _ _ Hs1 Hs2) in H
end.
Ltac absurd_mode :=
match goal with
......@@ -525,19 +461,19 @@ Proof.
Ho1 : do_overflow _ _ = true,
Ho2 : do_overflow _ _ = false
|- _
] => apply Rle_le in H; now rewrite (overflow_le _ H (sign_pos_inv _ Hs) Ho1) in Ho2
] => apply Rleb_Rle in H; now rewrite (overflow_is_le _ H (sign_pos_inv _ Hs) Ho1) in Ho2
| [ H : Raux.Rle_bool _ _ = true,
Hs : sign _ = true,
Ho1 : do_overflow _ _ = false,
Ho2 : do_overflow _ _ = true
|- _
] => apply Rle_le in H; now rewrite (overflow_le' _ H (sign_neg_inv _ Hs) Ho2) in Ho1
] => apply Rleb_Rle in H; now rewrite (overflow_is_ge _ H (sign_neg_inv _ Hs) Ho2) in Ho1
| [ H : Raux.Rle_bool _ _ = false,
Hs : sign _ = true,
Ho1 : do_overflow _ _ = true,
Ho2 : do_overflow _ _ = false
|- _
] => apply Rle_le in H; now rewrite (overflow_le' _ H (sign_neg_inv _ Hs) Ho2) in Ho1
] => apply Rleb_Rle in H; now rewrite (overflow_is_ge _ H (sign_neg_inv _ Hs) Ho2) in Ho1
| [ H1 : overflow_to_inf _ _ = true, H2 : overflow_to_inf _ _ = false |- _ ] =>
now rewrite H1 in H2
end.
......@@ -616,19 +552,19 @@ Lemma leb_trans :
forall x y z : Rx, leb x y = true -> leb y z = true -> leb x z = true.
Proof.
intros [ rx | [ ] ] [ ry | [ ] ] [ rz | [ ] ] Hxy Hyz; simpl in *; try easy.
apply Rle_le in Hxy.
apply Rle_le in Hyz.
apply Rleb_Rle in Hxy.
apply Rleb_Rle in Hyz.
apply Raux.Rle_bool_true.
lra.
Qed.
Lemma add_leb_compat :
Lemma add_leb_mono_l :
forall x y z : Rx,
leb x y = true -> leb (add x z) (add y z) = true.
Proof.
intros [ ] [ ] [ ] H.
- simpl in *.
apply Rle_le in H.
apply Rleb_Rle in H.
apply Raux.Rle_bool_true.
lra.
- now destruct b.
......@@ -640,13 +576,13 @@ Proof.
- now destruct b, b0, b1.
Qed.
Lemma add_leb_compat_l :
Lemma add_leb_mono_r :
forall x y z : Rx,
leb x y = true -> leb (add z x) (add z y) = true.
Proof.
intros [ | [ ]] [ | [ ]] [ | [ ]] H; try easy.
simpl in *.
apply Rle_le in H.
apply Rleb_Rle in H.
apply Raux.Rle_bool_true.
lra.
Qed.
......@@ -688,11 +624,11 @@ Proof.
apply Ropp_lt_contravar.
rewrite <- B2R_Bopp; simpl (Bopp _).
apply (Rle_lt_trans _ R_fmax).
- rewrite R2F_fmax. auto using Bleb_le, F_fmax_max.
- rewrite R2F_fmax. auto using Bleb_Rle, F_fmax_max.
- apply Rimax_Rfmax.
+ rewrite Generic_fmt.round_generic by (intuition; apply generic_format_B2R).
apply (Rle_lt_trans _ R_fmax).
- rewrite R2F_fmax. auto using Bleb_le, F_fmax_max.
- rewrite R2F_fmax. auto using Bleb_Rle, F_fmax_max.
- apply Rimax_Rfmax.
Qed.
......
src_common/ieee/coq/Utils.v
+ 265
− 62
View file @ 041e82e2
From Flocq Require Import IEEE754.BinarySingleNaN.
From Coq Require Import ZArith Lia Reals Psatz.
From F Require Import Rextended.
From Coq Require Import ZArith Lia Reals Psatz Bool.
(* From F Require Import Rextended. *)
(*********************************************************
Simple & usefull results on floats
......@@ -92,15 +92,6 @@ Lemma le_infm_finite:
forall x : float, is_finite x = true -> x <= -oo -> False.
Proof. now intros [ ]. Qed.
Lemma Bplus_not_nan_inv :
forall m (x y : float),
is_nan (Bplus m x y) = false ->
is_nan x = false /\ is_nan y = false.
Proof.
fdestruct x; fdestruct y.
Qed.
Lemma Bplus_finites_not_nan :
forall m (x y : float),
is_finite x = true ->
......@@ -114,7 +105,24 @@ Proof.
auto using (is_nan_binary_normalize prec emax).
Qed.
Lemma Bplus_nan_if :
Lemma Bplus_nan_inv :
forall (m : mode) (x y:float), is_nan (Bplus m x y) = true ->
x = +oo /\ y = -oo \/ x = -oo /\ y = +oo \/ x = NaN \/ y = NaN.
Proof.
intros; fdestruct x; fdestruct y; auto.
- now destruct m.
- now destruct m.
- now rewrite Bplus_finites_not_nan in H.
Qed.
Lemma Bplus_not_nan_inv :
forall (m : mode) (x y:float), is_nan (Bplus m x y) = false ->
~(x = +oo /\ y = -oo) /\ ~(x = -oo /\ y = +oo) /\ (is_nan x = false) /\ (is_nan y = false).
Proof.
intros; repeat split; fdestruct x; fdestruct y.
Qed.
(* Lemma Bplus_nan_if :
forall m (x y : float),
is_nan x = false ->
is_nan y = false ->
......@@ -125,7 +133,7 @@ Proof.
fdestruct x; fdestruct y; try now destruct m; intuition.
assert (is_nan (Bplus m (B754_finite s m0 e e0) (B754_finite s0 m1 e1 e2)) = false) by auto using Bplus_finites_not_nan.
rewrite H1 in H2; discriminate.
Qed.
Qed. *)
Lemma Bplus_zero :
forall m b (x : float),
......@@ -136,14 +144,78 @@ Proof.
- simpl; destruct m; reflexivity.
Qed.
Lemma pos_Bopp_neg :
forall m e Hb, @B754_finite prec emax true m e Hb = Bopp (B754_finite false m e Hb).
Proof. reflexivity. Qed.
Lemma neg_Bopp_pos :
forall m e Hb, @B754_finite prec emax false m e Hb = Bopp (B754_finite true m e Hb).
Proof. reflexivity. Qed.
Lemma Rle_Bleb :
forall (x y : float),
is_finite x = true ->
is_finite y = true ->
(B2R x <= B2R y)%R ->
Bleb x y = true.
Proof.
intros x y Fx Fy Hxy.
unfold Bleb, SpecFloat.SFleb.
replace (SpecFloat.SFcompare (_ x) (_ y)) with (Bcompare x y) by auto.
rewrite (Bcompare_correct _ _ x y Fx Fy).
destruct Raux.Rcompare eqn:E; try easy.
apply Raux.Rcompare_Gt_inv in E; lra.
Qed.
Lemma Rlt_Bltb :
forall (x y : float),
is_finite x = true ->
is_finite y = true ->
(B2R x < B2R y)%R ->
Bltb x y = true.
Proof.
intros x y Fx Fy Hxy.
unfold Bltb, SpecFloat.SFltb.
replace (SpecFloat.SFcompare (_ x) (_ y)) with (Bcompare x y) by auto.
rewrite (Bcompare_correct _ _ x y Fx Fy).
destruct Raux.Rcompare eqn:E; auto.
- apply Raux.Rcompare_Eq_inv in E; lra.
- apply Raux.Rcompare_Gt_inv in E; lra.
Qed.
Lemma Bleb_Rle :
forall x y : float, is_finite x = true -> is_finite y = true ->
Bleb x y = true -> (B2R x <= B2R y)%R.
Proof.
intros x y Fx Fy H.
unfold Bleb, SpecFloat.SFleb in H.
replace (SpecFloat.SFcompare (_ x) (_ y)) with (Bcompare x y) in H by auto.
rewrite (Bcompare_correct _ _ x y Fx Fy) in H.
destruct (Raux.Rcompare) eqn:E in H; try easy.
+ apply Raux.Rcompare_Eq_inv in E; lra.
+ apply Raux.Rcompare_Lt_inv in E; lra.
Qed.
Lemma Bltb_Rlt :
forall x y : float, is_finite x = true -> is_finite y = true ->
Bltb x y = true -> (B2R x < B2R y)%R.
Proof.
intros x y Fx Fy H.
unfold Bltb, SpecFloat.SFltb in H.
replace (SpecFloat.SFcompare (_ x) (_ y)) with (Bcompare x y) in H by auto.
rewrite (Bcompare_correct _ _ x y Fx Fy) in H.
destruct (Raux.Rcompare) eqn:E in H; try easy.
apply Raux.Rcompare_Lt_inv in E; lra.
Qed.
Lemma Bleb_trans :
forall (x y z : float), x <= y -> y <= z -> x <= z.
Proof.
intros x y z Hxy Hyz.
fdestruct x; fdestruct y; fdestruct z;
apply le_Bleb; auto;
apply Bleb_le in Hxy; auto;
apply Bleb_le in Hyz; auto;
apply Rle_Bleb; auto;
apply Bleb_Rle in Hxy; auto;
apply Bleb_Rle in Hyz; auto;
lra.
Qed.
......@@ -152,9 +224,9 @@ Lemma Bltb_trans :
Proof.
intros x y z Hxy Hyz.
fdestruct x; fdestruct y; fdestruct z;
apply lt_Bltb; auto;
apply Bltb_lt in Hxy; auto;
apply Bltb_lt in Hyz; auto;
apply Rlt_Bltb; auto;
apply Bltb_Rlt in Hxy; auto;
apply Bltb_Rlt in Hyz; auto;
lra.
Qed.
......@@ -163,9 +235,9 @@ Lemma Bltb_Bleb_trans :
Proof.
intros x y z Hxy Hyz.
fdestruct x; fdestruct y; fdestruct z;
apply lt_Bltb; auto;
apply Bltb_lt in Hxy; auto;
apply Bleb_le in Hyz; auto;
apply Rlt_Bltb; auto;
apply Bltb_Rlt in Hxy; auto;
apply Bleb_Rle in Hyz; auto;
lra.
Qed.
......@@ -174,49 +246,173 @@ Lemma Bleb_Bltb_trans :
Proof.
intros x y z Hxy Hyz.
fdestruct x; fdestruct y; fdestruct z;
apply lt_Bltb; auto;
apply Bleb_le in Hxy; auto;
apply Bltb_lt in Hyz; auto;
apply Rlt_Bltb; auto;
apply Bleb_Rle in Hxy; auto;
apply Bltb_Rlt in Hyz; auto;
lra.
Qed.
(* Lemma Bplus_correct_full :
forall (m : mode) (x y : float),
is_nan (Bplus m x y) = false ->
B2Rx (Bplus m x y) = round m (add (B2Rx x) (B2Rx y)).
Proof.
intros m x y HnanS.
destruct (Bplus_not_nan_inv _ _ _ HnanS) as [HnanX HnanY].
induction x as [ [ ] | [ ] | | ] eqn:Ex, y as [ [ ] | [ ] | | ] eqn:Ey; try easy.
- simpl (Bplus m (B754_zero _) _).
simpl (B2Rx (B754_zero _)).
rewrite add_0_l. apply round_0.
- simpl (Bplus m (B754_zero _) _).
simpl (B2Rx (B754_zero _)).
rewrite add_0_l. destruct m; auto using round_0.
- simpl (Bplus m (B754_zero true) _).
simpl (B2Rx (B754_zero _)).
rewrite add_0_l.
apply round_id.
- simpl (Bplus m (B754_zero _) _).
simpl (B2Rx (B754_zero _)).
rewrite add_0_r. destruct m; auto using round_0.
- simpl (Bplus m (B754_zero _) _).
rewrite add_0_l.
simpl (B2Rx _).
apply round_0.
- simpl (Bplus m (B754_zero _) _).
rewrite add_0_l.
apply round_id.
- simpl (Bplus m _ (B754_zero _)).
rewrite add_0_r.
apply round_id.
- simpl (Bplus m _ (B754_zero _)).
rewrite add_0_r.
apply round_id.
- Check (Bplus_correct).
admit.
Admitted. *)
Lemma Bleb_refl :
forall x:float, is_nan x = false -> Bleb x x = true.
Proof.
intros x Hx; fdestruct x.
apply Rle_Bleb; auto; lra.
Qed.
Lemma Bltb_Bleb :
forall x y : float, Bltb x y = true -> Bleb x y = true.
Proof.
intros x y Hxy.
fdestruct x; fdestruct y;
apply Rle_Bleb; auto;
apply Bltb_Rlt in Hxy; auto;
lra.
Qed.
Lemma Bleb_false_Bltb :
forall x y:float, is_nan x = false -> is_nan y = false -> Bleb x y = false -> Bltb y x = true.
Proof.
intros x y Hx Hy Hxy.
destruct x as [ | [ ] | | ] eqn:Ex, y as [ | [ ] | | ] eqn:Ey; try easy; rewrite <- Ex, <- Ey in *;
unfold Bleb, SpecFloat.SFleb in Hxy;
replace (SpecFloat.SFcompare (B2SF _) (B2SF _)) with (Bcompare x y) in Hxy by auto;
assert (Fx: is_finite x = true) by (rewrite Ex; auto);
assert (Fy: is_finite y = true) by (rewrite Ey; auto);
rewrite (Bcompare_correct _ _ x y Fx Fy) in Hxy; auto;
destruct (Raux.Rcompare _ _) eqn:E; try easy;
apply Raux.Rcompare_Gt_inv in E;
apply Rlt_Bltb; auto.
Qed.
Definition Bmax (f1 f2 : float) : float :=
if is_nan f1 || is_nan f2 then NaN
else if Bleb f1 f2 then f2
else f1.
Definition Bmin (f1 f2 : float) : float :=
if is_nan f1 || is_nan f2 then NaN
else if Bleb f1 f2 then f1
else f2.
Lemma Bmax_max_1 :
forall x y, (Bmax x y = x \/ Bmax x y = y).
Proof.
intros [ ] [ ]; unfold Bmax; destruct Bleb; intuition.
Qed.
Lemma Bmax_max_2 :
forall x y, is_finite x = true -> is_finite y = true -> x <= Bmax x y /\ y <= Bmax x y.
Proof.
intros x y Fx Fy; unfold Bmax.
assert (HnanX: is_nan x = false) by fdestruct x.
assert (HnanY: is_nan y = false) by fdestruct y.
rewrite HnanX, HnanY; simpl.
split.
- destruct (Bleb x y) eqn:?; auto.
apply Bleb_refl; fdestruct x.
- destruct (Bleb x y) eqn:E.
+ apply Bleb_refl; fdestruct y.
+ apply Bleb_false_Bltb in E; auto.
now apply Bltb_Bleb in E.
Qed.
Lemma Bmax_le :
forall x y z : float, x <= z -> y <= z -> Bmax x y <= z.
Proof.
intros x y z Hxz Hyz.
assert (HnanX: is_nan x = false) by fdestruct x.
assert (HnanY: is_nan y = false) by fdestruct y.
unfold Bmax.
rewrite HnanX, HnanY; simpl.
now destruct (Bleb x y).
Qed.
Lemma Bmax_not_nan_inv :
forall x y, is_nan (Bmax x y) = false -> is_nan x = false /\ is_nan y = false.
Proof.
intros; split.
+ fdestruct x.
+ fdestruct x; fdestruct y.
Qed.
Lemma Bmin_not_nan_inv :
forall x y, is_nan (Bmin x y) = false -> is_nan x = false /\ is_nan y = false.
Proof.
intros; split.
+ fdestruct x.
+ fdestruct x; fdestruct y.
Qed.
Lemma Bmax_le_inv :
forall x y z : float, Bmax x y <= z -> x <= z /\ y <= z.
Proof.
intros x y z Hxyz.
assert (is_nan (Bmax x y) = false) by (fdestruct (Bmax x y)).
unfold Bmax in Hxyz.
apply Bmax_not_nan_inv in H.
destruct H as [H1 H2].
rewrite H1, H2 in Hxyz.
simpl in *.
destruct (Bleb x y) eqn:E; split; auto.
- now apply (Bleb_trans x y z).
- apply Bleb_false_Bltb in E; auto.
apply Bltb_Bleb in E; auto.
now apply (Bleb_trans y x z).
Qed.
Lemma Bmin_min_1 :
forall x y, (Bmin x y = x \/ Bmin x y = y).
Proof.
intros [ ] [ ]; unfold Bmin; destruct Bleb; intuition.
Qed.
Lemma Bmin_min_2 :
forall x y, is_finite x = true -> is_finite y = true -> Bmin x y <= x /\ Bmin x y <= y.
Proof.
intros x y Fx Fy; unfold Bmin.
assert (HnanX: is_nan x = false) by fdestruct x.
assert (HnanY: is_nan y = false) by fdestruct y.
rewrite HnanX, HnanY; simpl.
split.
- destruct (Bleb x y) eqn:?.
+ apply Bleb_refl; fdestruct x.
+ assert (Hx : is_nan x = false) by (fdestruct x).
assert (Hy : is_nan y = false) by (fdestruct y).
apply Bleb_false_Bltb in Heqb; auto.
apply Bltb_Rlt in Heqb; auto.
apply Rle_Bleb; auto.
lra.
- destruct (Bleb x y) eqn:E; auto.
apply Bleb_refl; fdestruct y.
Qed.
Lemma Bmin_le :
forall x y z : float, z <= x -> z <= y -> z <= Bmin x y.
Proof.
intros x y z Hxz Hyz.
assert (HnanX: is_nan x = false) by (fdestruct z; fdestruct x).
assert (HnanY: is_nan y = false) by (fdestruct z; fdestruct y).
unfold Bmin.
rewrite HnanX, HnanY; simpl.
now destruct (Bleb x y).
Qed.
Lemma Bmin_le_inv :
forall x y z : float, z <= Bmin x y -> z <= x /\ z <= y.
Proof.
intros x y z Hxyz.
assert (is_nan (Bmin x y) = false) by (fdestruct (Bmin x y); fdestruct z).
unfold Bmin in Hxyz.
apply Bmin_not_nan_inv in H.
destruct H as [H1 H2].
rewrite H1, H2 in Hxyz.
simpl in *.
destruct (Bleb x y) eqn:E; split; auto.
- now apply (Bleb_trans z x y).
- apply Bleb_false_Bltb in E; auto.
apply Bltb_Bleb in E.
now apply (Bleb_trans z y x).
Qed.
End Utils.
......@@ -228,3 +424,10 @@ Arguments is_infm {prec} {emax}.
Arguments is_infp {prec} {emax}.
Arguments is_inf {prec} {emax}.
Arguments Bplus_not_nan_inv {prec} {emax} {Hprec} {Hemax}.
Arguments Bplus_nan_inv {prec} {emax} {Hprec} {Hemax}.
Arguments Bmin {prec} {emax}.
Arguments Bmax {prec} {emax}.
Arguments Bmax_max_1 {prec} {emax}.
Arguments Bmax_max_2 {prec} {emax}.
Arguments Bmin_min_1 {prec} {emax}.
Arguments Bmin_min_2 {prec} {emax}.
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