Rextended.v

From Flocq Require Import IEEE754.BinarySingleNaN.
From Coq Require Import ZArith Psatz Reals.

(*********************************************************
       Extension of R with special values +oo, -oo
**********************************************************)

Set Implicit Arguments.

Section Rutils.

Definition sign (r : R) :=
  Raux.Rlt_bool r 0.

Lemma sign_pos_inv :
  forall r, sign r = false -> (0 <= r)%R.
Proof.
  intros.
  unfold sign in H.
  now destruct (Raux.Rlt_bool_spec r 0).
Qed.

Lemma sign_neg_inv :
  forall r, sign r = true -> (r <= 0)%R.
Proof.
  intros.
  unfold sign in H. left.
  now destruct (Raux.Rlt_bool_spec r 0).
Qed.

Lemma sign_neg_inv_strict:
  forall r, sign r = true -> (r < 0)%R.
Proof.
  intros.
  unfold sign in H.
  now destruct (Raux.Rlt_bool_spec r 0).
Qed.

Lemma minus_pos_lt :
  forall r1 r2, (0 < r2)%R -> (r1 - r2 < r1)%R.
Proof.
  intros; lra.
Qed.

Lemma IZR_neg :
  (forall x, IZR (Z.neg x) < 0)%R.
Proof.
  induction x; try lra;
  apply (Rgt_trans _ (IZR (Z.neg x))); auto;
  apply IZR_lt; lia.
Qed.

Lemma IZR_pos :
  (forall x, IZR (Z.pos x) > 0)%R.
Proof.
  induction x; try lra;
  apply (Rgt_trans _ (IZR (Z.pos x))); auto;
  apply IZR_lt; lia.
Qed.

End Rutils.


Section Rextended.

Variable prec : Z.
Variable emax : Z.
Context (Hprec : FLX.Prec_gt_0 prec).
Context (Hemax : Prec_lt_emax prec emax).