Module FloatIntervals

Require Import Coqlib Utf8 ToString Util.
Require Import AdomLib.
Require Import FloatLib.

Inductive fitv : Type :=
| FITV: float -> float -> fitv.

Instance FitvToString : ToString fitv :=
  { to_string i :=
      let 'FITV min max := i in
      ("[" ++ to_string min ++ "; " ++ to_string max ++ "]")%string
  }.

Instance fitv_leb : leb_op fitv := fun i1 i2 =>
  let 'FITV min1 max1 := i1 in
  let 'FITV min2 max2 := i2 in
  is_nan min1 || is_nan max1 || (Fleb min2 min1 && Fleb max1 max2).

Lemma leb_eq:
  ∀ i:fitv, i ⊑ i = true.

Instance fitv_join : join_op fitv fitv := fun i1 i2 =>
  let 'FITV min1 max1 := i1 in
  let 'FITV min2 max2 := i2 in
  FITV (if Fleb min1 min2 || is_nan min2 then min1 else min2)
       (if Fleb max2 max1 || is_nan max2 then max1 else max2).

Lemma join_eq:
  ∀ x:fitv, x ⊔ x = x.

Instance fitv_meet : meet_op fitv (fitv+⊥) := fun i1 i2 =>
  let 'FITV min1 max1 := i1 in
  let 'FITV min2 max2 := i2 in
  let m := if Fleb min1 min2 then min2 else min1 in
  let M := if Fleb max1 max2 then max1 else max2 in
  if Fleb m M then NotBot (FITV m M)
  else Bot.

Definition fitv_widen i1 i2:=
  let 'FITV min1 max1 := i1 in
  let 'FITV min2 max2 := i2 in
  FITV (if Fleb min1 min2 || is_nan min2 then min1
        else B754_infinity true)
       (if Fleb max2 max1 || is_nan max2 then max1
        else B754_infinity false).

Lemma widen_eq:
  ∀ x:fitv, fitv_widen x x = x.

Instance gamma : gamma_op fitv float := fun i v =>
  let 'FITV m M := i in
  Fleb m v = true /\ Fleb v M = true.

Instance fitv_leb_correct : leb_op_correct fitv float.

Instance fitv_join_correct : join_op_correct fitv fitv float.

Instance fitv_meet_correct: meet_op_correct fitv (fitv+⊥) float.

Lemma widen_incr:
  ∀ ab1 ab2, γ ab1 ⊆ γ (fitv_widen ab1 ab2).

Definition forward_fneg (x:fitv+⊤) : fitv+⊤ :=
  match x with
  | Just (FITV mx Mx) => Just (FITV (Float.neg Mx) (Float.neg mx))
  | All => All
  end.

Lemma forward_fneg_correct:
  ∀ x x_ab, x ∈ γ x_ab -> (Float.neg x) ∈ γ (forward_fneg x_ab).