# Module LinearQuery

Require Import Utf8 Coqlib Util FastArith.
Require Import IdealExpr IdealIntervals ZIntervals.
Require Import FloatIntervals FloatLib.

Transparent Float.neg Float.zero.

Definition r_of_inum (x:ideal_num) : option R :=
match x with
| INz z => Some (z:R)
| INf f => if is_finite f then Some (f:R) else None
end.

Definition RF_le (x:R) (y:float) :=
if is_finite y then (x <= y)
else y = B754_infinity false.

Local Instance fitv_gamma_R : gamma_op fitv R :=
fun itv x =>
let 'FITV a b := itv in
RF_le x b /\ RF_le (-x) (Float.neg a).

Local Instance fitv_gamma_oR : gamma_op fitv (option R) :=
fun itv x => match x with None => False | Some x => x ∈ γ itv end.

Instance igR_meet_op_correct : meet_op_correct fitv (fitv+⊥) R.
Proof.
repeat intro. destruct x, y, H as [[][]]. unfold meet, fitv_meet.
assert (forall (f:float) b, is_finite f = true -> Fleb (B754_infinity b) f = b).
{ intros [] []; try discriminate; reflexivity. }
assert (forall (f:float) b, is_finite f = true -> Fleb f (B754_infinity b) = negb b).
{ intros [|[]| |[]] []; try discriminate; try reflexivity. }
assert (forall f, Bopp 53 1024 Float.neg_pl f = B754_infinity false ->
f = B754_infinity true).
{ intros [|[]| |]; try discriminate. auto. }
unfold RF_le, Float.neg in H, H0, H1, H2.
repeat match goal with
| H:if ?FIN then _ else _ |- _ => destruct FIN eqn:?
end;
repeat match goal with
| H:Bopp _ _ _ ?f = B754_infinity false |- _ => apply H5 in H
end;
subst; rewrite is_finite_Bopp in *; rewrite ?H3, ?H4 by auto; simpl;
repeat match goal with
| |- context [Fleb ?f1 ?f2] =>
let EQ := fresh in
destruct (Fleb f1 f2) eqn:EQ;
rewrite Fleb_Rle in EQ by auto;
Rle_bool_case EQ; try discriminate
end; simpl;
repeat match goal with
| |- context [Fleb (B754_infinity _) ?f] => rewrite (H3 f) by auto
| |- context [Fleb ?f (B754_infinity _)] => rewrite (H4 f) by auto; simpl
end;
simpl; unfold RF_le, Float.neg;
rewrite ?is_finite_Bopp, ?B2R_Bopp in * by auto; simpl;
repeat match goal with
| H:is_finite ?f = true |- _ => rewrite H
end;
try split; try reflexivity; try Psatz.lra.
Qed.

Instance igoR_meet_op_correct : meet_op_correct fitv (fitv+⊥) (option R).
Proof.
repeat intro. destruct a. 2:destruct H as [[]]. apply igR_meet_op_correct in H.
destruct (xy); auto.
Qed.

Definition fitv_of_zitv (i:zitv) : fitv :=
let 'ZITV a b := i in
FITV (binary_normalize 53 1024 eq_refl eq_refl mode_DN a 0 false)
(binary_normalize 53 1024 eq_refl eq_refl mode_UP b 0 false).

Lemma fitv_of_zitv_correct:
∀ i (z:Z), z ∈ γ i -> (z:R) ∈ γ (fitv_of_zitv i).
Proof.
intros. destruct i. simpl. unfold RF_le. split.
- pose proof binary_normalize_correct 53 1024 eq_refl eq_refl mode_UP z1 0 false.
simpl in H0. destruct H. apply Z2R_le in H. apply Z2R_le in H1.
Rlt_bool_case H0. 2:Rlt_bool_case H0.
+ destruct H0 as (? & ? & ?). rewrite H3, H0.
eapply Rle_trans. apply round_UP_pt. apply (fexp_correct 53 1024). reflexivity.
apply round_le. apply (fexp_correct 53 1024), eq_refl.
apply (valid_rnd_round_mode mode_UP).
unfold F2R. simpl. Psatz.lra.
+ destruct binary_normalize as [| |? []|]; inv H0.
eapply Rlt_le, round_le in H3. rewrite round_0 in H3.
rewrite Rabs_left1 in H2 by apply H3.
eapply Rle_trans. apply H1.
eapply Rle_trans. apply (round_UP_pt radix2), (fexp_correct 53 1024), eq_refl.
unfold F2R in H2. simpl in H2. rewrite Rmult_1_r in H2.
apply Ropp_le_cancel. eapply Rle_trans, H2. compute; Psatz.lra.
apply (valid_rnd_round_mode mode_UP). apply (fexp_correct 53 1024), eq_refl.
apply (valid_rnd_round_mode mode_UP).
+ destruct binary_normalize as [| |? []|]; inv H0. reflexivity.
- pose proof binary_normalize_correct 53 1024 eq_refl eq_refl mode_DN z0 0 false.
simpl in H0. destruct H. apply Z2R_le in H. apply Z2R_le in H1.
unfold Float.neg. rewrite is_finite_Bopp, B2R_Bopp.
Rlt_bool_case H0. 2:Rlt_bool_case H0.
+ destruct H0 as (? & ? & ?). rewrite H3, H0.
apply Ropp_le_contravar. eapply Rle_trans, H.
unfold F2R. simpl. rewrite Rmult_1_r. apply round_DN_pt.
apply (fexp_correct 53 1024), eq_refl.
+ destruct binary_normalize as [| |? []|]; inv H0. reflexivity.
+ destruct binary_normalize as [| |? []|]; inv H0.
eapply round_le in H3. rewrite round_0 in H3.
rewrite Rabs_right in H2 by apply Rle_ge, H3.
eapply Ropp_le_contravar, Rle_trans, H.
unfold F2R in H2. simpl in H2. rewrite Rmult_1_r in H2.
eapply Rle_trans, round_DN_pt. eapply Rle_trans, H2.
compute; Psatz.lra.
apply (fexp_correct 53 1024), eq_refl. apply (valid_rnd_round_mode mode_DN).
apply (fexp_correct 53 1024), eq_refl. apply (valid_rnd_round_mode mode_DN).
Qed.

Definition fitv_of_z (z:Zfast) : fitv :=
fitv_of_zitv (ZITV z z).

Lemma fitv_of_z_correct:
∀ (z:Z), (z:R) ∈ γ (fitv_of_z z).
Proof.
intros. apply fitv_of_zitv_correct. simpl. Psatz.lia.
Qed.

Definition fitv_of_iitv (i:iitv+⊤+⊥) : fitv+⊤ :=
match i with
| Bot | NotBot All => All
| NotBot (Just (Az i)) => Just (fitv_of_zitv i)
| NotBot (Just (Af (FITV a b as i))) => if is_finite a && is_finite b then Just i else All
end.

Lemma fitv_of_iitv_correct:
∀ i x, x ∈ γ i -> r_of_inum x ∈ γ (fitv_of_iitv i).
Proof.
unfold fitv_of_iitv. intros. destruct i as [|[|[|[]]]]; try exact I.
- destruct x. destruct H. apply fitv_of_zitv_correct, H.
- destruct x. 2:destruct H.
destruct (is_finite f) eqn:FINf, (is_finite f0) eqn:FINf0;
try exact I. destruct H.
assert (FINf1:is_finite f1 = true).
{ destruct f as [| | |[]], f1 as [|[]| |], f0; try discriminate; reflexivity. }
simpl. rewrite FINf1. split; unfold RF_le, Float.neg.
+ rewrite FINf0. rewrite Fleb_Rle in H0 by auto. Rle_bool_case H0. auto. discriminate.
+ rewrite is_finite_Bopp, FINf, B2R_Bopp.
rewrite Fleb_Rle in H by auto. Rle_bool_case H. Psatz.lra. discriminate.
Qed.

Definition iitv_of_fitv (ty:ideal_num_ty) (i:fitv) : iitv+⊤ :=
match ty with
| INTf => Just (Af i)
| INTz =>
let 'FITV a b := i in
match Zoffloat_DN (Float.neg a), Zoffloat_DN b with
| Some a, Some b => Just (Az (ZITV (-a)%Z b))
| _, _ => All
end
end.

Lemma iitv_of_fitv_correct:
∀ i x ty, r_of_inum x ∈ γ i -> x ∈ γ ty -> x ∈ γ (iitv_of_fitv ty i).
Proof.
destruct 2, i; intros; simpl.
- pose proof Zoffloat_DN_correct (Float.neg f).
pose proof Zoffloat_DN_correct f0.
destruct (Zoffloat_DN (Float.neg f)), (Zoffloat_DN f0), H0, H1; try exact I.
simpl in H. unfold RF_le, Float.neg in *. rewrite H0, H1, B2R_Bopp in H.
destruct H. apply Ropp_le_cancel in H4.
split; apply le_Z2R.
+ apply Ropp_le_cancel. simpl. rewrite Z2R_opp, H2, Ropp_involutive, B2R_Bopp.
apply round_DN_pt. apply Fcore_FIX.FIX_exp_valid.
apply generic_format_opp. 2:Psatz.lra.
apply Fcore_FIX.generic_format_FIX. exists (Float radix2 i0 0); unfold F2R; simpl.
split. ring. auto.
+ simpl. rewrite H3. apply round_DN_pt, H. apply Fcore_FIX.FIX_exp_valid.
apply Fcore_FIX.generic_format_FIX. exists (Float radix2 i0 0); unfold F2R; simpl.
split. ring. auto.
- red in H. simpl in H. red in H. destruct (is_finite f) eqn:FINf. 2:contradiction.
simpl in H. unfold RF_le, Float.neg in H. rewrite B2R_Bopp, is_finite_Bopp in H.
destruct H. split.
+ destruct (is_finite f0) eqn:FINf0. rewrite Fleb_Rle by auto.
apply Rle_bool_true. Psatz.lra.
destruct f0 as [|[]| |], f; try discriminate; reflexivity.
+ destruct (is_finite f1) eqn:FINf1. rewrite Fleb_Rle by auto.
apply Rle_bool_true. Psatz.lra. subst.
destruct f as [| | |[]]; try discriminate; reflexivity.
Qed.

Definition opp_itv (x:fitv) : fitv :=
match x with
| FITV m M => FITV (Float.neg M) (Float.neg m)
end.

Lemma opp_itv_correct:
∀ ix x, x ∈ γ ix -> (-x) ∈ γ (opp_itv ix).
Proof.
intros. unfold opp_itv. destruct ix, H; split. auto. clear H0.
unfold RF_le, Float.neg in *. rewrite !is_finite_Bopp, !B2R_Bopp, !Ropp_involutive.
destruct @is_finite. auto. subst. auto.
Qed.

Definition add_itv (x y:fitv) : fitv :=
match x, y with
| FITV mx Mx, FITV my My =>
let m := Bplus 53 1024 eq_refl eq_refl Float.binop_pl mode_DN mx my in
let m := if is_nan m then B754_infinity true else m in
let M := Bplus 53 1024 eq_refl eq_refl Float.binop_pl mode_UP Mx My in
let M := if is_nan M then B754_infinity false else M in
FITV m M
end.

∀ ix iy x y,
x ∈ γ ix -> y ∈ γ iy ->
(x+y) ∈ γ (add_itv ix iy).
Proof.
intros [mx Mx] [my My] x y [HMx Hmx] [HMy Hmy]. split; unfold add_itv, RF_le in *.
- clear Hmx Hmy.
destruct (is_finite Mx) eqn:FINx, (is_finite My) eqn:FINy.
+ pose proof Bplus_correct 53 1024 eq_refl eq_refl Float.binop_pl mode_UP Mx My FINx FINy.
pose proof @round_UP_pt radix2 _ (fexp_correct 53 1024 eq_refl) (Mx + My).
destruct H0 as (? & ? & ?).
unfold round_mode in H. Rlt_bool_case H.
* destruct H as (? & ? & ?). rewrite is_finite_not_is_nan, H4 by auto. Psatz.lra.
* destruct H, (Bsign Mx) eqn:signMx,
(Bplus 53 1024 eq_refl eq_refl Float.binop_pl mode_UP Mx My) as [| |? []|];
inv H. 2:now auto. simpl.
apply Rabs_ge_inv in H3. destruct H3.
apply Rle_trans with (r2:=- bpow radix2 1024). Psatz.lra. compute. Psatz.lra.
assert (Mx <= 0).
{ destruct Mx as [[]|[]|[]|[]]; inv signMx; simpl; try Psatz.lra.
apply F2R_le_0_compat. compute; discriminate. }
assert (My <= 0).
{ destruct My as [[]|[]|[]|[]]; inv H4; simpl; try Psatz.lra.
apply F2R_le_0_compat. compute; discriminate. }
specialize (H2 _ (generic_format_0 _ _)). lapply H2. 2:Psatz.lra.
assert (bpow radix2 1024 <= 0) by Psatz.lra.
compute in H6. Psatz.lra.
+ subst. destruct Mx as [[]|[]|[]|[]]; try discriminate; reflexivity.
+ subst. destruct My as [[]|[]|[]|[]]; try discriminate; reflexivity.
+ subst. reflexivity.
- clear HMx HMy.
destruct (is_finite (Float.neg mx)) eqn:FINx,
(is_finite (Float.neg my)) eqn:FINy;
unfold Float.neg in FINx, FINy; rewrite is_finite_Bopp in FINx, FINy.
+ pose proof Bplus_correct 53 1024 eq_refl eq_refl Float.binop_pl mode_DN mx my FINx FINy.
pose proof @round_DN_pt radix2 _ (fexp_correct 53 1024 eq_refl) (mx + my).
destruct H0 as (? & ? & ?).
unfold round_mode in H. Rlt_bool_case H.
* destruct H as (? & ? & ?). unfold Float.neg.
rewrite is_finite_Bopp, is_finite_not_is_nan, H4, B2R_Bopp by auto.
unfold Float.neg in Hmx, Hmy. rewrite B2R_Bopp in Hmx, Hmy. Psatz.lra.
* destruct H, (Bsign mx) eqn:signmx,
(Bplus 53 1024 eq_refl eq_refl Float.binop_pl mode_DN mx my) as [| |? []|];
inv H. now auto. simpl.
apply Rabs_ge_inv in H3. destruct H3.
assert (0 <= mx).
{ destruct mx as [[]|[]|[]|[]]; inv signmx; simpl; try Psatz.lra.
apply F2R_ge_0_compat. compute; discriminate. }
assert (0 <= my).
{ destruct my as [[]|[]|[]|[]]; inv H4; simpl; try Psatz.lra.
apply F2R_ge_0_compat. compute; discriminate. }
specialize (H2 _ (generic_format_0 _ _)). lapply H2. 2:Psatz.lra.
assert (bpow radix2 1024 <= 0) by Psatz.lra.
compute in H6. Psatz.lra.
apply Rle_trans with (r2:=-bpow radix2 1024).
unfold Float.neg in Hmx, Hmy. rewrite B2R_Bopp in Hmx, Hmy. Psatz.lra.
compute. Psatz.lra.
+ destruct mx as [[]|[]|[]|[]], my as [[]|[]|[]|[]]; try discriminate; reflexivity.
+ destruct mx as [[]|[]|[]|[]], my as [[]|[]|[]|[]]; try discriminate; reflexivity.
+ destruct mx as [[]|[]|[]|[]], my as [[]|[]|[]|[]]; try discriminate; reflexivity.
Qed.

Definition mult_itv (x y:fitv) : fitv :=
match x, y with
| FITV mx Mx, FITV my My =>
let m1 :=
if Bsign mx then Bmult 53 1024 eq_refl eq_refl Float.binop_pl mode_DN mx My
else Bmult 53 1024 eq_refl eq_refl Float.binop_pl mode_DN mx my
in
let m1 := if is_nan m1 then Float.zero else m1 in
let m2 :=
if Bsign Mx then Bmult 53 1024 eq_refl eq_refl Float.binop_pl mode_DN Mx My
else Bmult 53 1024 eq_refl eq_refl Float.binop_pl mode_DN Mx my
in
let m2 := if is_nan m2 then Float.zero else m2 in
let m := if Fleb m1 m2 then m1 else m2 in
let M1 :=
if Bsign mx then Bmult 53 1024 eq_refl eq_refl Float.binop_pl mode_UP mx my
else Bmult 53 1024 eq_refl eq_refl Float.binop_pl mode_UP mx My
in
let M1 := if is_nan M1 then Float.zero else M1 in
let M2 :=
if Bsign Mx then Bmult 53 1024 eq_refl eq_refl Float.binop_pl mode_UP Mx my
else Bmult 53 1024 eq_refl eq_refl Float.binop_pl mode_UP Mx My
in
let M2 := if is_nan M2 then Float.zero else M2 in
let M := if Fleb M1 M2 then M2 else M1 in
FITV m M
end.

Lemma mult_itv_correct:
∀ ix iy x y,
x ∈ γ ix -> y ∈ γ iy ->
(x*y) ∈ γ (mult_itv ix iy).
Proof.
intros [mx Mx] [my My] x y [HMx Hmx] [HMy Hmy]. unfold mult_itv.
set (m1 :=
if Bsign mx then Bmult 53 1024 eq_refl eq_refl Float.binop_pl mode_DN mx My
else Bmult 53 1024 eq_refl eq_refl Float.binop_pl mode_DN mx my).
set (m1':=if is_nan m1 then Float.zero else m1).
set (m2 :=
if Bsign Mx then Bmult 53 1024 eq_refl eq_refl Float.binop_pl mode_DN Mx My
else Bmult 53 1024 eq_refl eq_refl Float.binop_pl mode_DN Mx my).
set (m2':=if is_nan m2 then Float.zero else m2).
set (M1 :=
if Bsign mx then Bmult 53 1024 eq_refl eq_refl Float.binop_pl mode_UP mx my
else Bmult 53 1024 eq_refl eq_refl Float.binop_pl mode_UP mx My).
set (M1':=if is_nan M1 then Float.zero else M1).
set (M2 :=
if Bsign Mx then Bmult 53 1024 eq_refl eq_refl Float.binop_pl mode_UP Mx my
else Bmult 53 1024 eq_refl eq_refl Float.binop_pl mode_UP Mx My).
set (M2':=if is_nan M2 then Float.zero else M2).
unfold mult_itv, Float.neg, RF_le in *.
rewrite is_finite_Bopp, B2R_Bopp in Hmx, Hmy.
split; unfold mult_itv, Float.neg, RF_le in *; destruct (Rle_lt_dec 0 y) as [ySgn|ySgn].
- assert (RF_le (x*y) M2').
{ subst M1 M1' M2 M2' m1 m1' m2 m2'. clear mx Hmx.
destruct (is_finite Mx) eqn:FINMx.
- assert (x*y <= Mx*y) by (apply Rmult_le_compat_r; auto).
destruct (Bsign Mx) eqn:SGNMx.
+ pose proof Bsign_true_le_0 _ _ _ SGNMx.
destruct (is_finite my) eqn:FINmy.
* assert (x*y <= Mx*my).
{ eapply Rle_trans. eauto. apply Rmult_le_compat_neg_l; Psatz.lra. }
clear HMx My HMy Hmy ySgn H.
{ pose proof Bmult_correct 53 1024 eq_refl eq_refl Float.binop_pl mode_UP Mx my.
rewrite FINMx, FINmy, SGNMx in H. Rlt_bool_case H.
- destruct H as (? & ? & _).
unfold RF_le. rewrite is_finite_not_is_nan, H3, H by auto.
eapply Rle_trans. eauto. apply round_UP_pt. apply fexp_correct. reflexivity.
- destruct (Bsign my) eqn:SGNmy, Bmult as [| |? []|]; inv H.
reflexivity.
eapply Rle_trans. eauto. clear x y H1. apply Bsign_false_ge_0 in SGNmy.
assert (Mx * my <= 0).
{ apply Ropp_le_cancel. rewrite Ropp_0, <- Ropp_mult_distr_l_reverse.
apply Rmult_le_pos; Psatz.lra. }
apply Rabs_ge_inv in H2. destruct H2.
+ eapply Rle_trans. apply round_UP_pt with (beta:=radix2).
apply (fexp_correct 53). reflexivity.
eapply Rle_trans. apply H1. compute; Psatz.lra.
+ eapply Rle_trans with (r3:=0) in H1. compute in H1. Psatz.lra.
eapply Rle_trans. apply round_UP_pt with (beta:=radix2).
apply fexp_correct. reflexivity. apply generic_format_0. auto.
Psatz.lra. }
* destruct Mx as [[]| | |[]], my as [|[]| |]; try discriminate.
unfold RF_le. simpl in *. Psatz.lra. reflexivity.
+ pose proof Bsign_false_ge_0 _ _ _ SGNMx.
destruct (is_finite My) eqn:FINMy.
* assert (x*y <= Mx * My).
{ eapply Rle_trans, Ropp_le_cancel. eauto.
rewrite <- !Ropp_mult_distr_l_reverse.
apply Rmult_le_compat_neg_l; Psatz.lra. }
clear HMx my HMy Hmy ySgn H.
{ pose proof Bmult_correct 53 1024 eq_refl eq_refl Float.binop_pl mode_UP Mx My.
rewrite FINMx, FINMy, SGNMx in H. Rlt_bool_case H.
- destruct H as (? & ? & _).
unfold RF_le. rewrite is_finite_not_is_nan, H3, H by auto.
eapply Rle_trans. eauto. apply round_UP_pt. apply fexp_correct. reflexivity.
- destruct (Bsign My) eqn:SGNMy, Bmult as [| |? []|]; inv H.
2:reflexivity.
eapply Rle_trans. eauto. clear x y H1. apply Bsign_true_le_0 in SGNMy.
assert (Mx * My <= 0).
{ apply Ropp_le_cancel. rewrite Ropp_0, <- Ropp_mult_distr_r_reverse.
apply Rmult_le_pos; Psatz.lra. }
apply Rabs_ge_inv in H2. destruct H2.
+ eapply Rle_trans. apply round_UP_pt with (beta:=radix2).
apply (fexp_correct 53). reflexivity.
eapply Rle_trans. apply H1. compute; Psatz.lra.
+ eapply Rle_trans with (r3:=0) in H1. compute in H1. Psatz.lra.
eapply Rle_trans. apply round_UP_pt with (beta:=radix2).
apply fexp_correct. reflexivity. apply generic_format_0. auto.
Psatz.lra. }
* destruct Mx as [[]| | |[]], My as [|[]| |]; try discriminate.
unfold RF_le. simpl in *. Psatz.lra. reflexivity.
- clear FINMx. subst Mx. destruct My as [|[]| |]; try discriminate.
simpl in *. replace y with 0 by Psatz.lra. rewrite Rmult_0_r. apply Rle_refl.
reflexivity.
simpl in HMy. eapply Rle_trans in HMy.
apply F2R_ge_0_reg in HMy. destruct b.
destruct HMy. auto. reflexivity. auto. }
clear - H. destruct (Fleb M1' M2') eqn:EQFleb. apply H.
unfold RF_le in H.
destruct (is_finite M1') eqn:FINM1', (is_finite M2') eqn:FINM2'.
+ rewrite Fleb_Rle in EQFleb by auto. Rle_bool_case EQFleb. discriminate. Psatz.lra.
+ rewrite H in EQFleb. destruct M1 as [| | |[]]; discriminate.
+ destruct M1 as [|[]| |]; try discriminate. 2:now auto.
destruct M2'; discriminate.
+ destruct M1 as [|[]| |]; try discriminate. 2:now auto.
destruct M2' as [|[]| |]; discriminate.
- assert (RF_le (x*y) M1').
{ subst M1 M1' M2 M2' m1 m1' m2 m2'. clear Mx HMx.
destruct (is_finite mx) eqn:FINmx.
- assert (x*y <= mx*y).
{ apply Ropp_le_cancel. rewrite <- !Ropp_mult_distr_r_reverse.
apply Rmult_le_compat_r; Psatz.lra. }
destruct (Bsign mx) eqn:SGNmx.
+ pose proof Bsign_true_le_0 _ _ _ SGNmx.
destruct (is_finite my) eqn:FINmy.
* assert (x*y <= mx*my).
{ eapply Rle_trans, Ropp_le_cancel. eauto.
rewrite <- !Ropp_mult_distr_l_reverse.
apply Rmult_le_compat_l; Psatz.lra. }
clear Hmx My HMy Hmy ySgn H.
{ pose proof Bmult_correct 53 1024 eq_refl eq_refl Float.binop_pl mode_UP mx my.
rewrite FINmx, FINmy, SGNmx in H. Rlt_bool_case H.
- destruct H as (? & ? & _).
unfold RF_le. rewrite is_finite_not_is_nan, H3, H by auto.
eapply Rle_trans. eauto. apply round_UP_pt. apply fexp_correct. reflexivity.
- destruct (Bsign my) eqn:SGNmy, Bmult as [| |? []|]; inv H.
reflexivity.
eapply Rle_trans. eauto. clear x y H1. apply Bsign_false_ge_0 in SGNmy.
assert (mx*my <= 0).
{ apply Ropp_le_cancel. rewrite Ropp_0, <- Ropp_mult_distr_l_reverse.
apply Rmult_le_pos; Psatz.lra. }
apply Rabs_ge_inv in H2. destruct H2.
+ eapply Rle_trans. apply round_UP_pt with (beta:=radix2).
apply (fexp_correct 53). reflexivity.
eapply Rle_trans. apply H1. compute; Psatz.lra.
+ eapply Rle_trans with (r3:=0) in H1. compute in H1. Psatz.lra.
eapply Rle_trans. apply round_UP_pt with (beta:=radix2).
apply fexp_correct. reflexivity. apply generic_format_0. auto.
Psatz.lra. }
* destruct mx as [[]| | |[]], my as [|[]| |]; try discriminate.
unfold RF_le. simpl in *. Psatz.lra. reflexivity.
+ pose proof Bsign_false_ge_0 _ _ _ SGNmx.
destruct (is_finite My) eqn:FINMy.
* assert (x*y <= mx*My).
{ eapply Rle_trans, Ropp_le_cancel. eauto.
rewrite <- !Ropp_mult_distr_r_reverse.
apply Rmult_le_compat_l; Psatz.lra. }
clear Hmx my HMy Hmy ySgn H.
{ pose proof Bmult_correct 53 1024 eq_refl eq_refl Float.binop_pl mode_UP mx My.
rewrite FINmx, FINMy, SGNmx in H. Rlt_bool_case H.
- destruct H as (? & ? & _).
unfold RF_le. rewrite is_finite_not_is_nan, H3, H by auto.
eapply Rle_trans. eauto. apply round_UP_pt. apply fexp_correct. reflexivity.
- destruct (Bsign My) eqn:SGNMy, Bmult as [| |? []|]; inv H.
2:reflexivity.
eapply Rle_trans. eauto. clear x y H1. apply Bsign_true_le_0 in SGNMy.
assert (mx*My <= 0).
{ apply Ropp_le_cancel. rewrite Ropp_0, <- Ropp_mult_distr_r_reverse.
apply Rmult_le_pos; Psatz.lra. }
apply Rabs_ge_inv in H2. destruct H2.
+ eapply Rle_trans. apply round_UP_pt with (beta:=radix2).
apply (fexp_correct 53). reflexivity.
eapply Rle_trans. apply H1. compute; Psatz.lra.
+ eapply Rle_trans with (r3:=0) in H1. compute in H1. Psatz.lra.
eapply Rle_trans. apply round_UP_pt with (beta:=radix2).
apply fexp_correct. reflexivity. apply generic_format_0. auto.
Psatz.lra. }
* destruct mx as [[]| | |[]], My as [|[]| |]; try discriminate.
unfold RF_le. simpl in *. Psatz.lra. reflexivity.
- clear FINmx. destruct mx as [|[]| |]; inv Hmx.
destruct my as [|[]| |]; try discriminate. simpl in *. Psatz.lra. reflexivity.
simpl in Hmy. eapply Rle_trans in Hmy.
apply Ropp_le_cancel, F2R_le_0_reg in Hmy. destruct b.
reflexivity. destruct Hmy. auto. Psatz.lra. }
clear - H. destruct (Fleb M1' M2') eqn:EQFleb. 2:apply H.
unfold RF_le in H.
destruct (is_finite M1') eqn:FINM1', (is_finite M2') eqn:FINM2'.
+ rewrite Fleb_Rle in EQFleb by auto. Rle_bool_case EQFleb. Psatz.lra. discriminate.
+ destruct M1' as [| | |[]], M2' as [|[]| |]; try discriminate; reflexivity.
+ rewrite H in EQFleb. destruct M2'; discriminate.
+ rewrite H in EQFleb. destruct M2' as [|[]| |]; try discriminate. auto.
- assert (RF_le (-(x*y)) (Bopp _ _ Float.neg_pl m1')).
{ subst M1 M1' M2 M2' m1 m1' m2 m2'. clear Mx HMx.
destruct (is_finite mx) eqn:FINmx.
- assert (mx*y <= x*y) by (apply Rmult_le_compat_r; Psatz.lra).
destruct (Bsign mx) eqn:SGNmx.
+ pose proof Bsign_true_le_0 _ _ _ SGNmx.
destruct (is_finite My) eqn:FINMy.
* assert (mx*My <= x*y).
{ eapply Rle_trans, H.
apply Ropp_le_cancel. rewrite <- !Ropp_mult_distr_l_reverse.
apply Rmult_le_compat_l; Psatz.lra. }
clear Hmx my Hmy HMy ySgn H.
{ pose proof Bmult_correct 53 1024 eq_refl eq_refl Float.binop_pl mode_DN mx My.
rewrite FINmx, FINMy, SGNmx in H. Rlt_bool_case H.
- destruct H as (? & ? & _).
unfold RF_le.
rewrite is_finite_not_is_nan, is_finite_Bopp, H3, B2R_Bopp, H by auto.
eapply Ropp_le_contravar, Rle_trans. 2:eauto.
apply round_DN_pt. apply fexp_correct. reflexivity.
- destruct (Bsign My) eqn:SGNMy, Bmult as [| |? []|]; inv H.
2:reflexivity.
eapply Rle_trans. apply Ropp_le_contravar, H1.
clear x y H1. apply Bsign_true_le_0 in SGNMy.
rewrite B2R_Bopp. apply Ropp_le_contravar.
assert (0 <= mx*My).
{ rewrite <- Rmult_opp_opp. apply Rmult_le_pos; Psatz.lra. }
apply Rabs_ge_inv in H2. destruct H2.
+ eapply Rle_trans with (r1:=0) in H1. compute in H1. Psatz.lra.
eapply Rle_trans. 2:apply round_DN_pt with (beta:=radix2).
2:apply fexp_correct. 2:reflexivity. 2:apply generic_format_0.
Psatz.lra. auto.
+ eapply Rle_trans. 2:apply round_DN_pt with (beta:=radix2).
2:apply (fexp_correct 53). 2:reflexivity.
eapply Rle_trans. 2:apply H1. compute; Psatz.lra. }
* destruct mx as [[]| | |[]], My as [|[]| |]; try discriminate.
unfold RF_le. simpl in *. Psatz.lra. reflexivity.
+ pose proof Bsign_false_ge_0 _ _ _ SGNmx.
destruct (is_finite my) eqn:FINmy.
* assert (mx*my <= x*y).
{ eapply Rle_trans, H. apply Rmult_le_compat_l; Psatz.lra. }
clear Hmx My Hmy HMy ySgn H.
{ pose proof Bmult_correct 53 1024 eq_refl eq_refl Float.binop_pl mode_DN mx my.
rewrite FINmx, FINmy, SGNmx in H. Rlt_bool_case H.
- destruct H as (? & ? & _).
unfold RF_le.
rewrite is_finite_not_is_nan, is_finite_Bopp, B2R_Bopp, H3, H by auto.
eapply Ropp_le_contravar, Rle_trans. 2:eauto.
apply round_DN_pt. apply fexp_correct. reflexivity.
- destruct (Bsign my) eqn:SGNmy, Bmult as [| |? []|]; inv H.
reflexivity.
eapply Rle_trans. eapply Ropp_le_contravar. eauto.
clear x y H1. apply Bsign_false_ge_0 in SGNmy.
assert (0 <= mx*my).
{ apply Rmult_le_pos; Psatz.lra. }
apply Rabs_ge_inv in H2. destruct H2.
+ eapply Rle_trans with (r1:=0) in H1. compute in H1. Psatz.lra.
eapply Rle_trans. 2:apply round_DN_pt with (beta:=radix2).
2:apply fexp_correct. 2:reflexivity. 2:apply generic_format_0.
Psatz.lra. auto.
+ rewrite B2R_Bopp. apply Ropp_le_contravar.
eapply Rle_trans. 2:apply round_DN_pt with (beta:=radix2).
2:apply (fexp_correct 53). 2:reflexivity.
eapply Rle_trans. 2:apply H1. compute; Psatz.lra. }
* destruct mx as [[]| | |[]], my as [|[]| |]; try discriminate.
unfold RF_le. simpl in *. Psatz.lra. reflexivity.
- clear FINmx. destruct mx as [|[]| |], My as [|[]| |]; try discriminate.
simpl in *. replace y with 0 by Psatz.lra.
rewrite Rmult_0_r, Ropp_0. apply Rle_refl. reflexivity.
simpl in HMy. eapply Rle_trans in HMy.
apply F2R_ge_0_reg in HMy. destruct b.
destruct HMy. auto. reflexivity. auto. }
clear - H. destruct (Fleb m1' m2') eqn:EQFleb. apply H.
unfold RF_le in H. rewrite is_finite_Bopp, B2R_Bopp in *.
destruct (is_finite m1') eqn:FINm1', (is_finite m2') eqn:FINm2'.
+ rewrite Fleb_Rle in EQFleb by auto. Rle_bool_case EQFleb. discriminate. Psatz.lra.
+ destruct m2 as [|[]| |]; try discriminate. now auto.
destruct m1' as [| | |[]]; discriminate.
+ destruct m1' as [|[]| |]; try discriminate. destruct m2; discriminate.
+ destruct m2 as [|[]| |]; try discriminate. now auto.
destruct m1' as [|[]| |]; discriminate.
- assert (RF_le (-(x*y)) (Bopp _ _ Float.neg_pl m2')).
{ subst M1 M1' M2 M2' m1 m1' m2 m2'. clear mx Hmx.
destruct (is_finite Mx) eqn:FINMx.
- assert (Mx*y <= x*y).
{ apply Ropp_le_cancel. rewrite <- !Ropp_mult_distr_r_reverse.
apply Rmult_le_compat_r; Psatz.lra. }
destruct (Bsign Mx) eqn:SGNMx.
+ pose proof Bsign_true_le_0 _ _ _ SGNMx.
destruct (is_finite My) eqn:FINMy.
* assert (Mx*My <= x*y).
{ eapply Rle_trans, H. eapply Ropp_le_cancel.
rewrite <- !Ropp_mult_distr_l_reverse.
apply Rmult_le_compat_l; Psatz.lra. }
clear HMx my Hmy HMy ySgn H.
{ pose proof Bmult_correct 53 1024 eq_refl eq_refl Float.binop_pl mode_DN Mx My.
rewrite FINMx, FINMy, SGNMx in H. Rlt_bool_case H.
- destruct H as (? & ? & _).
unfold RF_le.
rewrite is_finite_not_is_nan, is_finite_Bopp, H3, B2R_Bopp, H by auto.
eapply Ropp_le_contravar, Rle_trans. 2:eauto.
apply round_DN_pt. apply fexp_correct. reflexivity.
- destruct (Bsign My) eqn:SGNMy, Bmult as [| |? []|]; inv H.
2:reflexivity.
eapply Rle_trans. apply Ropp_le_contravar, H1.
clear x y H1. apply Bsign_true_le_0 in SGNMy.
rewrite B2R_Bopp. apply Ropp_le_contravar.
assert (0 <= Mx*My).
{ rewrite <- Rmult_opp_opp. apply Rmult_le_pos; Psatz.lra. }
apply Rabs_ge_inv in H2. destruct H2.
+ eapply Rle_trans with (r1:=0) in H1. compute in H1. Psatz.lra.
eapply Rle_trans. 2:apply round_DN_pt with (beta:=radix2).
2:apply fexp_correct. 2:reflexivity. 2:apply generic_format_0.
Psatz.lra. auto.
+ eapply Rle_trans. 2:apply round_DN_pt with (beta:=radix2).
2:apply (fexp_correct 53). 2:reflexivity.
eapply Rle_trans. 2:apply H1. compute; Psatz.lra. }
* destruct Mx as [[]| | |[]], My as [|[]| |]; try discriminate.
unfold RF_le. simpl in *. Psatz.lra. reflexivity.
+ pose proof Bsign_false_ge_0 _ _ _ SGNMx.
destruct (is_finite my) eqn:FINmy.
* assert (Mx*my <= x*y).
{ eapply Rle_trans, H. eapply Ropp_le_cancel.
rewrite <- !Ropp_mult_distr_r_reverse.
apply Rmult_le_compat_l; Psatz.lra. }
clear HMx My Hmy HMy ySgn H.
{ pose proof Bmult_correct 53 1024 eq_refl eq_refl Float.binop_pl mode_DN Mx my.
rewrite FINMx, FINmy, SGNMx in H. Rlt_bool_case H.
- destruct H as (? & ? & _).
unfold RF_le.
rewrite is_finite_not_is_nan, is_finite_Bopp, B2R_Bopp, H3, H by auto.
eapply Ropp_le_contravar, Rle_trans. 2:eauto.
apply round_DN_pt. apply fexp_correct. reflexivity.
- destruct (Bsign my) eqn:SGNmy, Bmult as [| |? []|]; inv H.
reflexivity.
eapply Rle_trans. eapply Ropp_le_contravar. eauto.
clear x y H1. apply Bsign_false_ge_0 in SGNmy.
assert (0 <= Mx*my).
{ apply Rmult_le_pos; Psatz.lra. }
apply Rabs_ge_inv in H2. destruct H2.
+ eapply Rle_trans with (r1:=0) in H1. compute in H1. Psatz.lra.
eapply Rle_trans. 2:apply round_DN_pt with (beta:=radix2).
2:apply fexp_correct. 2:reflexivity. 2:apply generic_format_0.
Psatz.lra. auto.
+ rewrite B2R_Bopp. apply Ropp_le_contravar.
eapply Rle_trans. 2:apply round_DN_pt with (beta:=radix2).
2:apply (fexp_correct 53). 2:reflexivity.
eapply Rle_trans. 2:apply H1. compute; Psatz.lra. }
* destruct Mx as [[]| | |[]], my as [|[]| |]; try discriminate.
unfold RF_le. simpl in *. Psatz.lra. reflexivity.
- clear FINMx. subst Mx. destruct my as [|[]| |]; try discriminate.
simpl in *. Psatz.lra. reflexivity.
simpl in Hmy. apply Ropp_le_cancel in Hmy. eapply Rle_lt_trans in Hmy.
apply F2R_lt_0_reg in Hmy. destruct b.
reflexivity. discriminate. auto. }
clear - H. destruct (Fleb m1' m2') eqn:EQFleb. 2:apply H.
unfold RF_le in H. rewrite is_finite_Bopp, B2R_Bopp in *.
destruct (is_finite m1') eqn:FINm1', (is_finite m2') eqn:FINm2'.
+ rewrite Fleb_Rle in EQFleb by auto. Rle_bool_case EQFleb. Psatz.lra. discriminate.
+ destruct m2 as [|[]| |]; try discriminate. destruct m1 as [| | |[]]; discriminate.
+ destruct m1' as [|[]| |]; try discriminate. reflexivity. destruct m2; discriminate.
+ destruct m1 as [|[]| |]; try discriminate. now auto.
destruct m2' as [|[]| |]; discriminate.
Qed.

Definition fitv_is_top (i:fitv) : bool :=
match i with
| FITV (B754_infinity true) (B754_infinity false) => true
| _ => false
end.

Definition rρ (ρ : var -> ideal_num) (x:var) : option R := r_of_inumx).

Definition linear_expr := (fitv * list (var * (fitv * fitv)))%type.

Definition eval_linear_expr (ρ:var -> ideal_num) (e:linear_expr): ℘(R) :=
List.fold_right
(fun (kitvs:var*(fitv*fitv)) X =>
let '(k, (itvα, itvk)) := kitvs in
fun y =>
match rρ ρ k with
| None => False
| Some kx => (∃ α, α ∈ γ itvα /\ X (y - α * kx)) /\
rρ ρ k ∈ γ itvk
end)
(γ (fst e)) (snd e).

Definition T_linear_expr := (fitv * T.t (fitv * fitv))%type.

Definition eval_T_linear_expr ρ (e:T_linear_expr) : ℘(R) :=
eval_linear_expr ρ (fst e, T.elements (snd e)).