Library Float.Fcomp

Require Export Float.
Section comparisons.
Variable radix : Z.
Hypothesis radixMoreThanOne : (1 < radix)%Z.

Let radixMoreThanZERO := Zlt_1_O _ (Zlt_le_weak _ _ radixMoreThanOne).
Hint Resolve radixMoreThanZERO: zarith.

Definition Fdiff (x y : float) :=
  (Fnum x × Zpower_nat radix (Z.abs_nat (Fexp x - Z.min (Fexp x) (Fexp y))) -
   Fnum y × Zpower_nat radix (Z.abs_nat (Fexp y - Z.min (Fexp x) (Fexp y))))%Z.

Let FtoRradix := FtoR radix.
Local Coercion FtoRradix : float >-> R.

Theorem Fdiff_correct :
  x y : float,
 (Fdiff x y × powerRZ radix (Z.min (Fexp x) (Fexp y)))%R = (x - y)%R.
intros x y; unfold Fdiff in |- ×.
rewrite <- Z_R_minus.
rewrite Rmult_comm; rewrite Rmult_minus_distr_l.
repeat rewrite Rmult_IZR.
repeat rewrite Zpower_nat_Z_powerRZ; auto.
rewrite (Rmult_comm (Fnum x)); rewrite (Rmult_comm (Fnum y)).
repeat rewrite <- Rmult_assoc.
repeat rewrite <- powerRZ_add; auto with real zarith.
repeat rewrite inj_abs; auto with arith.
repeat rewrite Zplus_minus; auto.
rewrite (fun t : RRmult_comm t (Fnum x));
 rewrite (fun t : RRmult_comm t (Fnum y)); auto.
apply Zplus_le_reg_l with (p := Z.min (Fexp x) (Fexp y)); auto with arith.
rewrite Zplus_minus; rewrite Zplus_0_r; apply Z.le_min_r; auto.
apply Zplus_le_reg_l with (p := Z.min (Fexp x) (Fexp y)); auto with arith.
rewrite Zplus_minus; rewrite Zplus_0_r; apply Z.le_min_l; auto.
Qed.

Definition Feq (x y : float) := x = y :>R.

Definition Fle (x y : float) := (x y)%R.

Definition Flt (x y : float) := (x < y)%R.

Definition Fge (x y : float) := (x y)%R.

Definition Fgt (x y : float) := (x > y)%R.

Definition Fcompare (x y : float) := (Fdiff x y ?= 0)%Z.

Definition Feq_bool (x y : float) :=
  match Fcompare x y with
  | Eqtrue
  | _false
  end.

Theorem Feq_bool_correct_t :
  x y : float, Feq_bool x y = true Feq x y.
intros x y H'; red in |- ×.
apply Rplus_eq_reg_l with (r := (- y)%R).
repeat rewrite (Rplus_comm (- y)).
rewrite Rplus_opp_r.
change ((x - y)%R = 0%R) in |- ×.
rewrite <- Fdiff_correct.
apply Rmult_eq_0_compat_r; auto.
cut (Fdiff x y = 0%Z); [ intros H; rewrite H | idtac ]; auto with real.
apply Zcompare_EGAL.
generalize H'; unfold Feq_bool, Fcompare in |- ×.
case (Fdiff x y ?= 0)%Z;auto; intros; discriminate.
Qed.

Theorem Feq_bool_correct_r :
  x y : float, Feq x y Feq_bool x y = true.
intros x y H'; cut ((x - y)%R = 0%R).
rewrite <- Fdiff_correct; intros H'1; case Rmult_integral with (1 := H'1).
intros H'0; unfold Feq_bool, Fcompare in |- ×.
rewrite eq_IZR_R0 with (1 := H'0); auto.
intros H'0; Contradict H'0.
case (Z.min (Fexp x) (Fexp y)); simpl in |- *; auto with real zarith.
apply Rplus_eq_reg_l with (r := FtoR radix y); auto with real.
Qed.

Theorem Feq_bool_correct_f :
  x y : float, Feq_bool x y = false ¬ Feq x y.
intros x y H'; Contradict H'.
rewrite Feq_bool_correct_r; auto with arith.
red in |- *; intros H'0; discriminate.
Qed.

Definition Flt_bool (x y : float) :=
  match Fcompare x y with
  | Lttrue
  | _false
  end.

Theorem Flt_bool_correct_t :
  x y : float, Flt_bool x y = true Flt x y.
intros x y H'; red in |- ×.
apply Rplus_lt_reg_r with (r := (- y)%R).
repeat rewrite (Rplus_comm (- y)).
rewrite Rplus_opp_r.
change (x - y < 0)%R in |- ×.
rewrite <- Fdiff_correct.
replace 0%R with (powerRZ radix (Z.min (Fexp x) (Fexp y)) × 0)%R;
 auto with real arith.
rewrite (Rmult_comm (Fdiff x y)).
apply Rmult_lt_compat_l; auto with real zarith.
replace 0%R with (IZR 0); auto with real arith.
apply Rlt_IZR; red in |- ×.
generalize H'; unfold Flt_bool, Fcompare in |- ×.
case (Fdiff x y ?= 0)%Z; auto; intros; try discriminate.
Qed.

Theorem Flt_bool_correct_r :
  x y : float, Flt x y Flt_bool x y = true.
intros x y H'.
cut (0 < y - x)%R; auto with arith.
2: apply Rplus_lt_reg_l with (r := FtoRradix x); rewrite Rplus_0_r;
    rewrite Rplus_minus; auto with real.
intros H'0.
cut (Fdiff x y < 0)%R; auto with arith.
intros H'1.
cut (Fdiff x y < 0)%Z; auto with zarith.
intros H'2; generalize (Zlt_compare _ _ H'2);
 unfold Flt_bool, Fcompare, Z.compare in |- *; case (Fdiff x y);
 auto with arith; intros; contradiction.
apply lt_IZR; auto with arith.
apply (Rlt_monotony_contra_exp radix) with (z := Z.min (Fexp x) (Fexp y));
 auto with arith real; rewrite Rmult_0_l.
rewrite Fdiff_correct; auto with real.
Qed.

Theorem Flt_bool_correct_f :
  x y : float, Flt_bool x y = false Fle y x.
intros x y H'.
case (Rtotal_order (FtoRradix y) (FtoRradix x)); auto with real.
intros H'0; red in |- *; apply Rlt_le; auto with real.
intros H'0; elim H'0; clear H'0; intros H'1.
red in |- *; rewrite H'1; auto with real.
Contradict H'; rewrite Flt_bool_correct_r; auto with real.
red in |- *; intros H'; discriminate.
Qed.

Definition Fle_bool (x y : float) :=
  match Fcompare x y with
  | Lttrue
  | Eqtrue
  | _false
  end.

Theorem Fle_bool_correct_t :
  x y : float, Fle_bool x y = true Fle x y.
intros x y H'.
cut (Feq x y Flt x y).
intros H; case H; intros H1; auto with real.
red in |- *; apply Req_le; auto with real.
red in |- *; apply Rlt_le; auto with real.
generalize H' (Feq_bool_correct_t x y) (Flt_bool_correct_t x y).
unfold Fle_bool, Feq_bool, Flt_bool in |- *; case (Fcompare x y); auto.
Qed.

Theorem Fle_bool_correct_r :
  x y : float, Fle x y Fle_bool x y = true.
intros x y H'.
cut (Feq x y Flt x y).
intros H; case H; intros H1; auto with real.
generalize (Feq_bool_correct_r x y).
unfold Fle_bool, Feq_bool, Flt_bool in |- *; case (Fcompare x y); auto.
generalize (Flt_bool_correct_r x y);
 unfold Fle_bool, Feq_bool, Flt_bool in |- *; case (Fcompare x y);
 auto with arith.
case H'; auto with arith.
Qed.

Theorem Fle_bool_correct_f :
  x y : float, Fle_bool x y = false Flt y x.
intros x y H'.
case (Rtotal_order (FtoRradix y) (FtoRradix x)); auto with real.
intros H'0; elim H'0; clear H'0; intros H'1.
Contradict H'.
rewrite Fle_bool_correct_r; auto with real.
red in |- *; intros H'; discriminate.
red in |- *; rewrite H'1; auto with real.
Contradict H'.
rewrite Fle_bool_correct_r; auto with real.
red in |- *; intros H'; discriminate.
red in |- *; auto with real.
Qed.

Lemma Fle_Zle :
  n1 n2 d : Z, (n1 n2)%Z Fle (Float n1 d) (Float n2 d).
intros; unfold Fle, FtoRradix, FtoR in |- *; simpl in |- *; auto.
case Zle_lt_or_eq with (1 := H); intros H1.
apply Rlt_le; auto with real.
rewrite <- H1; auto with real.
Qed.

Lemma Flt_Zlt :
  n1 n2 d : Z, (n1 < n2)%Z Flt (Float n1 d) (Float n2 d).
intros; unfold Flt, FtoRradix, FtoR in |- *; simpl in |- *; auto with real.
Qed.

Lemma Fle_Fge : x y : float, Fle x y Fge y x.
unfold Fle, Fge in |- *; intros x y H'; auto with real.
Qed.

Lemma Fge_Zge :
  n1 n2 d : Z, (n1 n2)%Z Fge (Float n1 d) (Float n2 d).
intros n1 n2 d H'; apply Fle_Fge; auto.
apply Fle_Zle; auto.
apply Z.ge_le; auto.
Qed.

Lemma Flt_Fgt : x y : float, Flt x y Fgt y x.
unfold Flt, Fgt in |- *; intros x y H'; auto.
Qed.

Lemma Fgt_Zgt :
  n1 n2 d : Z, (n1 > n2)%Z Fgt (Float n1 d) (Float n2 d).
intros n1 n2 d H'; apply Flt_Fgt; auto.
apply Flt_Zlt; auto.
apply Z.gt_lt; auto.
Qed.

Lemma Fle_refl : x y : float, Feq x y Fle x y.
unfold Feq in |- *; unfold Fle in |- *; intros.
rewrite H; auto with real.
Qed.

Lemma Fle_trans : x y z : float, Fle x y Fle y z Fle x z.
unfold Fle in |- *; intros.
apply Rle_trans with (r2 := FtoR radix y); auto.
Qed.

Theorem Rlt_Fexp_eq_Zlt :
  x y : float, (x < y)%R Fexp x = Fexp y (Fnum x < Fnum y)%Z.
intros x y H' H'0.
apply lt_IZR.
apply (Rlt_monotony_contra_exp radix) with (z := Fexp x);
 auto with real arith.
pattern (Fexp x) at 2 in |- *; rewrite H'0; auto.
Qed.

Theorem Rle_Fexp_eq_Zle :
  x y : float, (x y)%R Fexp x = Fexp y (Fnum x Fnum y)%Z.
intros x y H' H'0.
apply le_IZR.
apply (Rle_monotony_contra_exp radix) with (z := Fexp x);
 auto with real arith.
pattern (Fexp x) at 2 in |- *; rewrite H'0; auto.
Qed.

Theorem LtR0Fnum : p : float, (0 < p)%R (0 < Fnum p)%Z.
intros p H'.
apply lt_IZR.
apply (Rlt_monotony_contra_exp radix) with (z := Fexp p);
 auto with real arith.
simpl in |- *; rewrite Rmult_0_l; auto.
Qed.

Theorem LeR0Fnum : p : float, (0 p)%R (0 Fnum p)%Z.
intros p H'.
apply le_IZR.
apply (Rle_monotony_contra_exp radix) with (z := Fexp p);
 auto with real arith.
simpl in |- *; rewrite Rmult_0_l; auto.
Qed.

Theorem LeFnumZERO : x : float, (0 Fnum x)%Z (0 x)%R.
intros x H'; unfold FtoRradix, FtoR in |- ×.
replace 0%R with (0%Z × 0%Z)%R; auto 6 with real zarith.
Qed.

Theorem R0LtFnum : p : float, (p < 0)%R (Fnum p < 0)%Z.
intros p H'.
apply lt_IZR.
apply (Rlt_monotony_contra_exp radix) with (z := Fexp p);
 auto with real arith.
simpl in |- *; rewrite Rmult_0_l; auto.
Qed.

Theorem R0LeFnum : p : float, (p 0)%R (Fnum p 0)%Z.
intros p H'.
apply le_IZR.
apply (Rle_monotony_contra_exp radix) with (z := Fexp p);
 auto with real arith.
simpl in |- *; rewrite Rmult_0_l; auto.
Qed.

Theorem LeZEROFnum : x : float, (Fnum x 0)%Z (x 0)%R.
intros x H'; unfold FtoRradix, FtoR in |- ×.
apply Ropp_le_cancel; rewrite Ropp_0; rewrite <- Ropp_mult_distr_l_reverse.
replace 0%R with (- 0%Z × 0)%R; auto 6 with real zarith.
Qed.
End comparisons.
Hint Resolve LeFnumZERO LeZEROFnum: float.