Module LinearQuery


Require Import Utf8 Coqlib Util FastArith.
Require Import AdomLib.
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 (x⊓y); 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.

Lemma add_itv_correct:
  ∀ 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_inum (ρ x).

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)).
Generated by coq2html