(****************************************************************************
                                                                             
          IEEE754  :  Fcomp                                                     
                                                                             
          Laurent Thery                                                      
                                                                             
  ******************************************************************************)
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 (Zabs_nat (Fexp x - Zmin (Fexp x) (Fexp y))) -
   Fnum y * Zpower_nat radix (Zabs_nat (Fexp y - Zmin (Fexp x) (Fexp y))))%Z.

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

Theorem Fdiff_correct :
 forall x y : float,
 (Fdiff x y * powerRZ radix (Zmin (Fexp x) (Fexp y)))%R = (x - y)%R.
(* Goal: forall x y : float, @eq R (Rmult (IZR (Fdiff x y)) (powerRZ (IZR radix) (Z.min (Fexp x) (Fexp y)))) (Rminus (FtoRradix x) (FtoRradix y)) *)
intros x y; unfold Fdiff in |- *.
(* Goal: @eq R (Rmult (IZR (Z.sub (Z.mul (Fnum x) (Zpower_nat radix (Z.abs_nat (Z.sub (Fexp x) (Z.min (Fexp x) (Fexp y)))))) (Z.mul (Fnum y) (Zpower_nat radix (Z.abs_nat (Z.sub (Fexp y) (Z.min (Fexp x) (Fexp y)))))))) (powerRZ (IZR radix) (Z.min (Fexp x) (Fexp y)))) (Rminus (FtoRradix x) (FtoRradix y)) *)
rewrite <- Z_R_minus.
(* Goal: @eq R (Rmult (Rminus (IZR (Z.mul (Fnum x) (Zpower_nat radix (Z.abs_nat (Z.sub (Fexp x) (Z.min (Fexp x) (Fexp y))))))) (IZR (Z.mul (Fnum y) (Zpower_nat radix (Z.abs_nat (Z.sub (Fexp y) (Z.min (Fexp x) (Fexp y)))))))) (powerRZ (IZR radix) (Z.min (Fexp x) (Fexp y)))) (Rminus (FtoRradix x) (FtoRradix y)) *)
rewrite Rmult_comm; rewrite Rmult_minus_distr_l.
(* Goal: @eq R (Rminus (Rmult (powerRZ (IZR radix) (Z.min (Fexp x) (Fexp y))) (IZR (Z.mul (Fnum x) (Zpower_nat radix (Z.abs_nat (Z.sub (Fexp x) (Z.min (Fexp x) (Fexp y)))))))) (Rmult (powerRZ (IZR radix) (Z.min (Fexp x) (Fexp y))) (IZR (Z.mul (Fnum y) (Zpower_nat radix (Z.abs_nat (Z.sub (Fexp y) (Z.min (Fexp x) (Fexp y))))))))) (Rminus (FtoRradix x) (FtoRradix y)) *)
repeat rewrite Rmult_IZR.
(* Goal: @eq R (Rminus (Rmult (powerRZ (IZR radix) (Z.min (Fexp x) (Fexp y))) (Rmult (IZR (Fnum x)) (IZR (Zpower_nat radix (Z.abs_nat (Z.sub (Fexp x) (Z.min (Fexp x) (Fexp y)))))))) (Rmult (powerRZ (IZR radix) (Z.min (Fexp x) (Fexp y))) (Rmult (IZR (Fnum y)) (IZR (Zpower_nat radix (Z.abs_nat (Z.sub (Fexp y) (Z.min (Fexp x) (Fexp y))))))))) (Rminus (FtoRradix x) (FtoRradix y)) *)
repeat rewrite Zpower_nat_Z_powerRZ; auto.
(* Goal: @eq R (Rminus (Rmult (powerRZ (IZR radix) (Z.min (Fexp x) (Fexp y))) (Rmult (IZR (Fnum x)) (powerRZ (IZR radix) (Z.of_nat (Z.abs_nat (Z.sub (Fexp x) (Z.min (Fexp x) (Fexp y)))))))) (Rmult (powerRZ (IZR radix) (Z.min (Fexp x) (Fexp y))) (Rmult (IZR (Fnum y)) (powerRZ (IZR radix) (Z.of_nat (Z.abs_nat (Z.sub (Fexp y) (Z.min (Fexp x) (Fexp y))))))))) (Rminus (FtoRradix x) (FtoRradix y)) *)
rewrite (Rmult_comm (Fnum x)); rewrite (Rmult_comm (Fnum y)).
(* Goal: @eq R (Rminus (Rmult (powerRZ (IZR radix) (Z.min (Fexp x) (Fexp y))) (Rmult (powerRZ (IZR radix) (Z.of_nat (Z.abs_nat (Z.sub (Fexp x) (Z.min (Fexp x) (Fexp y)))))) (IZR (Fnum x)))) (Rmult (powerRZ (IZR radix) (Z.min (Fexp x) (Fexp y))) (Rmult (powerRZ (IZR radix) (Z.of_nat (Z.abs_nat (Z.sub (Fexp y) (Z.min (Fexp x) (Fexp y)))))) (IZR (Fnum y))))) (Rminus (FtoRradix x) (FtoRradix y)) *)
repeat rewrite <- Rmult_assoc.
(* Goal: @eq R (Rminus (Rmult (Rmult (powerRZ (IZR radix) (Z.min (Fexp x) (Fexp y))) (powerRZ (IZR radix) (Z.of_nat (Z.abs_nat (Z.sub (Fexp x) (Z.min (Fexp x) (Fexp y))))))) (IZR (Fnum x))) (Rmult (Rmult (powerRZ (IZR radix) (Z.min (Fexp x) (Fexp y))) (powerRZ (IZR radix) (Z.of_nat (Z.abs_nat (Z.sub (Fexp y) (Z.min (Fexp x) (Fexp y))))))) (IZR (Fnum y)))) (Rminus (FtoRradix x) (FtoRradix y)) *)
repeat rewrite <- powerRZ_add; auto with real zarith.
(* Goal: @eq R (Rminus (Rmult (powerRZ (IZR radix) (Z.add (Z.min (Fexp x) (Fexp y)) (Z.of_nat (Z.abs_nat (Z.sub (Fexp x) (Z.min (Fexp x) (Fexp y))))))) (IZR (Fnum x))) (Rmult (powerRZ (IZR radix) (Z.add (Z.min (Fexp x) (Fexp y)) (Z.of_nat (Z.abs_nat (Z.sub (Fexp y) (Z.min (Fexp x) (Fexp y))))))) (IZR (Fnum y)))) (Rminus (FtoRradix x) (FtoRradix y)) *)
repeat rewrite inj_abs; auto with arith.
(* Goal: @eq R (Rminus (Rmult (powerRZ (IZR radix) (Z.add (Z.min (Fexp x) (Fexp y)) (Z.sub (Fexp x) (Z.min (Fexp x) (Fexp y))))) (IZR (Fnum x))) (Rmult (powerRZ (IZR radix) (Z.add (Z.min (Fexp x) (Fexp y)) (Z.sub (Fexp y) (Z.min (Fexp x) (Fexp y))))) (IZR (Fnum y)))) (Rminus (FtoRradix x) (FtoRradix y)) *)
(* Goal: Z.le Z0 (Z.sub (Fexp y) (Z.min (Fexp x) (Fexp y))) *)
(* Goal: Z.le Z0 (Z.sub (Fexp x) (Z.min (Fexp x) (Fexp y))) *)
repeat rewrite Zplus_minus; auto.
rewrite (fun t : R => Rmult_comm t (Fnum x));
 rewrite (fun t : R => Rmult_comm t (Fnum y)); auto.
(* Goal: Z.le Z0 (Z.sub (Fexp x) (Z.min (Fexp x) (Fexp y))) *)
apply Zplus_le_reg_l with (p := Zmin (Fexp x) (Fexp y)); auto with arith.
(* Goal: Z.le (Z.add (Z.min (Fexp x) (Fexp y)) Z0) (Z.add (Z.min (Fexp x) (Fexp y)) (Z.sub (Fexp y) (Z.min (Fexp x) (Fexp y)))) *)
(* Goal: Z.le Z0 (Z.sub (Fexp x) (Z.min (Fexp x) (Fexp y))) *)
rewrite Zplus_minus; rewrite Zplus_0_r; apply Zle_min_r; auto.
(* Goal: Z.le Z0 (Z.sub (Fexp x) (Z.min (Fexp x) (Fexp y))) *)
apply Zplus_le_reg_l with (p := Zmin (Fexp x) (Fexp y)); auto with arith.
(* Goal: Z.le (Z.add (Z.min (Fexp x) (Fexp y)) Z0) (Z.add (Z.min (Fexp x) (Fexp y)) (Z.sub (Fexp x) (Z.min (Fexp x) (Fexp y)))) *)
rewrite Zplus_minus; rewrite Zplus_0_r; apply Zle_min_l; auto.
Qed.
(* Definition of  comparison functions*)
 
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
  | Eq => true
  | _ => false
  end.
 
Theorem Feq_bool_correct_t :
 forall x y : float, Feq_bool x y = true -> Feq x y.
(* Goal: forall (x y : float) (_ : @eq bool (Flt_bool x y) true), Flt x y *)
intros x y H'; red in |- *.
(* Goal: @eq R (FtoRradix x) (FtoRradix y) *)
apply Rplus_eq_reg_l with (r := (- y)%R).
(* Goal: Rlt (Rplus (FtoRradix x) (Ropp (FtoRradix y))) (Rplus (FtoRradix y) (Ropp (FtoRradix y))) *)
repeat rewrite (Rplus_comm (- y)).
(* Goal: Rlt (Rplus (FtoRradix x) (Ropp (FtoRradix y))) (Rplus (FtoRradix y) (Ropp (FtoRradix y))) *)
rewrite Rplus_opp_r.
(* Goal: @eq R (Rplus (FtoRradix x) (Ropp (FtoRradix y))) (IZR Z0) *)
change ((x - y)%R = 0%R) in |- *.
(* Goal: Rlt (Rminus (FtoRradix x) (FtoRradix y)) (IZR Z0) *)
rewrite <- Fdiff_correct.
(* Goal: @eq R (Rmult (IZR (Fdiff x y)) (powerRZ (IZR radix) (Z.min (Fexp x) (Fexp y)))) (IZR Z0) *)
apply Rmult_eq_0_compat_r; auto.
(* Goal: @eq R (IZR (Fdiff x y)) (IZR Z0) *)
cut (Fdiff x y = 0%Z); [ intros H; rewrite H | idtac ]; auto with real.
(* Goal: @eq Z (Fdiff x y) Z0 *)
apply Zcompare_EGAL.
(* Goal: @eq comparison (Z.compare (Fdiff x y) Z0) Eq *)
generalize H'; unfold Feq_bool, Fcompare in |- *.
(* Goal: forall _ : @eq bool match Z.compare (Fdiff x y) Z0 with | Eq => true | Lt => false | Gt => false end true, @eq comparison (Z.compare (Fdiff x y) Z0) Eq *)
case (Fdiff x y ?= 0)%Z;auto; intros; discriminate.
Qed.
 
Theorem Feq_bool_correct_r :
 forall x y : float, Feq x y -> Feq_bool x y = true.
(* Goal: forall (x y : float) (_ : Feq x y), @eq bool (Feq_bool x y) true *)
intros x y H'; cut ((x - y)%R = 0%R).
(* Goal: forall _ : @eq R (Rminus (FtoRradix x) (FtoRradix y)) (IZR Z0), @eq bool (Feq_bool x y) true *)
(* Goal: @eq R (Rminus (FtoRradix x) (FtoRradix y)) (IZR Z0) *)
rewrite <- Fdiff_correct; intros H'1; case Rmult_integral with (1 := H'1).
(* Goal: forall _ : @eq R (IZR (Fdiff x y)) (IZR Z0), @eq bool (Feq_bool x y) true *)
(* Goal: forall _ : @eq R (powerRZ (IZR radix) (Z.min (Fexp x) (Fexp y))) (IZR Z0), @eq bool (Feq_bool x y) true *)
(* Goal: @eq R (Rminus (FtoRradix x) (FtoRradix y)) (IZR Z0) *)
intros H'0; unfold Feq_bool, Fcompare in |- *.
(* Goal: @eq bool match Z.compare (Fdiff x y) Z0 with | Eq => true | Lt => false | Gt => false end true *)
(* Goal: forall _ : @eq R (powerRZ (IZR radix) (Z.min (Fexp x) (Fexp y))) (IZR Z0), @eq bool (Feq_bool x y) true *)
(* Goal: @eq R (Rminus (FtoRradix x) (FtoRradix y)) (IZR Z0) *)
rewrite eq_IZR_R0 with (1 := H'0); auto.
(* Goal: forall _ : @eq R (powerRZ (IZR radix) (Z.min (Fexp x) (Fexp y))) (IZR Z0), @eq bool (Feq_bool x y) true *)
(* Goal: @eq R (Rminus (FtoRradix x) (FtoRradix y)) (IZR Z0) *)
intros H'0; Contradict H'0.
(* Goal: not (@eq R (powerRZ (IZR radix) (Z.min (Fexp x) (Fexp y))) (IZR Z0)) *)
(* Goal: @eq R (Rminus (FtoRradix x) (FtoRradix y)) (IZR Z0) *)
case (Zmin (Fexp x) (Fexp y)); simpl in |- *; auto with real zarith.
(* Goal: @eq R (Rminus (FtoRradix x) (FtoRradix y)) (IZR Z0) *)
apply Rplus_eq_reg_l with (r := FtoR radix y); auto with real.
Qed.
 
Theorem Feq_bool_correct_f :
 forall x y : float, Feq_bool x y = false -> ~ Feq x y.
(* Goal: forall (x y : float) (_ : @eq bool (Feq_bool x y) false), not (Feq x y) *)
intros x y H'; Contradict H'.
(* Goal: not (@eq bool (Feq_bool x y) false) *)
rewrite Feq_bool_correct_r; auto with arith.
(* Goal: not (@eq bool true false) *)
red in |- *; intros H'0; discriminate.
Qed.
 
Definition Flt_bool (x y : float) :=
  match Fcompare x y with
  | Lt => true
  | _ => false
  end.
 
Theorem Flt_bool_correct_t :
 forall x y : float, Flt_bool x y = true -> Flt x y.
(* Goal: forall (x y : float) (_ : @eq bool (Flt_bool x y) true), Flt x y *)
intros x y H'; red in |- *.
(* Goal: Rlt (FtoRradix x) (FtoRradix y) *)
apply Rplus_lt_reg_r with (r := (- y)%R).
(* Goal: Rlt (Rplus (FtoRradix x) (Ropp (FtoRradix y))) (Rplus (FtoRradix y) (Ropp (FtoRradix y))) *)
repeat rewrite (Rplus_comm (- y)).
(* Goal: Rlt (Rplus (FtoRradix x) (Ropp (FtoRradix y))) (Rplus (FtoRradix y) (Ropp (FtoRradix y))) *)
rewrite Rplus_opp_r.
(* Goal: Rlt (Rplus (FtoRradix x) (Ropp (FtoRradix y))) (IZR Z0) *)
change (x - y < 0)%R in |- *.
(* Goal: Rlt (Rminus (FtoRradix x) (FtoRradix y)) (IZR Z0) *)
rewrite <- Fdiff_correct.
replace 0%R with (powerRZ radix (Zmin (Fexp x) (Fexp y)) * 0)%R;
 auto with real arith.
(* Goal: Rlt (Rmult (IZR (Fdiff x y)) (powerRZ (IZR radix) (Z.min (Fexp x) (Fexp y)))) (Rmult (powerRZ (IZR radix) (Z.min (Fexp x) (Fexp y))) (IZR Z0)) *)
rewrite (Rmult_comm (Fdiff x y)).
(* Goal: Rlt (Rmult (powerRZ (IZR radix) (Z.min (Fexp x) (Fexp y))) (IZR (Fdiff x y))) (Rmult (powerRZ (IZR radix) (Z.min (Fexp x) (Fexp y))) (IZR Z0)) *)
apply Rmult_lt_compat_l; auto with real zarith.
(* Goal: Rlt (IZR (Fdiff x y)) (IZR Z0) *)
replace 0%R with (IZR 0); auto with real arith.
(* Goal: Rlt (IZR (Fdiff x y)) (IZR Z0) *)
apply Rlt_IZR; red in |- *.
(* Goal: @eq comparison (Z.compare (Fdiff x y) Z0) Lt *)
generalize H'; unfold Flt_bool, Fcompare in |- *.
(* Goal: forall _ : @eq bool match Z.compare (Fdiff x y) Z0 with | Eq => false | Lt => true | Gt => false end true, @eq comparison (Z.compare (Fdiff x y) Z0) Lt *)
case (Fdiff x y ?= 0)%Z; auto; intros; try discriminate.
Qed.
 
Theorem Flt_bool_correct_r :
 forall x y : float, Flt x y -> Flt_bool x y = true.
(* Goal: forall (x y : float) (_ : @eq bool (Fle_bool x y) false), Flt y x *)
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, Zcompare in |- *; case (Fdiff x y);
 auto with arith; intros; contradiction.
apply lt_IZR; auto with arith.
apply (Rlt_monotony_contra_exp radix) with (z := Zmin (Fexp x) (Fexp y));
 auto with arith real; rewrite Rmult_0_l.
rewrite Fdiff_correct; auto with real.
Qed.
 
Theorem Flt_bool_correct_f :
 forall x y : float, Flt_bool x y = false -> Fle y x.
(* Goal: forall (x y : float) (_ : @eq bool (Fle_bool x y) false), Flt y x *)
intros x y H'.
(* Goal: Flt y x *)
case (Rtotal_order (FtoRradix y) (FtoRradix x)); auto with real.
(* Goal: forall _ : Rlt (FtoRradix y) (FtoRradix x), Fle y x *)
(* Goal: forall _ : or (@eq R (FtoRradix y) (FtoRradix x)) (Rgt (FtoRradix y) (FtoRradix x)), Fle y x *)
intros H'0; red in |- *; apply Rlt_le; auto with real.
intros H'0; elim H'0; clear H'0; intros H'1.
(* Goal: Fle x y *)
(* Goal: Flt y x *)
red in |- *; rewrite H'1; auto with real.
(* Goal: Fle y x *)
Contradict H'; rewrite Flt_bool_correct_r; auto with real.
(* Goal: not (@eq bool true false) *)
(* Goal: Fle x y *)
red in |- *; intros H'; discriminate.
Qed.
 
Definition Fle_bool (x y : float) :=
  match Fcompare x y with
  | Lt => true
  | Eq => true
  | _ => false
  end.
 
Theorem Fle_bool_correct_t :
 forall x y : float, Fle_bool x y = true -> Fle x y.
(* Goal: forall (x y : float) (_ : @eq bool (Fle_bool x y) false), Flt y x *)
intros x y H'.
(* Goal: @eq bool (Fle_bool x y) true *)
cut (Feq x y \/ Flt x y).
(* Goal: forall _ : or (Feq x y) (Flt x y), @eq bool (Fle_bool x y) true *)
(* Goal: or (Feq x y) (Flt x y) *)
intros H; case H; intros H1; auto with real.
(* Goal: Fle x y *)
(* Goal: Fle x y *)
(* Goal: or (Feq x y) (Flt x y) *)
red in |- *; apply Req_le; auto with real.
(* Goal: Fle x y *)
(* Goal: or (Feq x y) (Flt x y) *)
red in |- *; apply Rlt_le; auto with real.
(* Goal: or (Feq x y) (Flt x y) *)
generalize H' (Feq_bool_correct_t x y) (Flt_bool_correct_t x y).
(* Goal: forall _ : forall _ : Feq x y, @eq bool (Feq_bool x y) true, @eq bool (Fle_bool x y) true *)
(* Goal: @eq bool (Fle_bool x y) true *)
(* Goal: or (Feq x y) (Flt x y) *)
unfold Fle_bool, Feq_bool, Flt_bool in |- *; case (Fcompare x y); auto.
Qed.
 
Theorem Fle_bool_correct_r :
 forall x y : float, Fle x y -> Fle_bool x y = true.
(* Goal: forall (x y : float) (_ : @eq bool (Fle_bool x y) false), Flt y x *)
intros x y H'.
(* Goal: @eq bool (Fle_bool x y) true *)
cut (Feq x y \/ Flt x y).
(* Goal: forall _ : or (Feq x y) (Flt x y), @eq bool (Fle_bool x y) true *)
(* Goal: or (Feq x y) (Flt x y) *)
intros H; case H; intros H1; auto with real.
(* Goal: @eq bool (Fle_bool x y) true *)
(* Goal: @eq bool (Fle_bool x y) true *)
(* Goal: or (Feq x y) (Flt x y) *)
generalize (Feq_bool_correct_r x y).
(* Goal: forall _ : forall _ : Feq x y, @eq bool (Feq_bool x y) true, @eq bool (Fle_bool x y) true *)
(* Goal: @eq bool (Fle_bool x y) true *)
(* Goal: or (Feq x y) (Flt 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.
(* Goal: or (Feq x y) (Flt x y) *)
case H'; auto with arith.
Qed.
 
Theorem Fle_bool_correct_f :
 forall x y : float, Fle_bool x y = false -> Flt y x.
(* Goal: forall (x y : float) (_ : @eq bool (Fle_bool x y) false), Flt y x *)
intros x y H'.
(* Goal: Flt y x *)
case (Rtotal_order (FtoRradix y) (FtoRradix x)); auto with real.
intros H'0; elim H'0; clear H'0; intros H'1.
(* Goal: Flt y x *)
Contradict H'.
(* Goal: not (@eq bool (Fle_bool x y) false) *)
rewrite Fle_bool_correct_r; auto with real.
(* Goal: not (@eq bool true false) *)
(* Goal: Fle x y *)
red in |- *; intros H'; discriminate.
(* Goal: Fle x y *)
(* Goal: Flt y x *)
red in |- *; rewrite H'1; auto with real.
(* Goal: Flt y x *)
Contradict H'.
(* Goal: not (@eq bool (Fle_bool x y) false) *)
rewrite Fle_bool_correct_r; auto with real.
(* Goal: not (@eq bool true false) *)
(* Goal: Fle x y *)
red in |- *; intros H'; discriminate.
(* Goal: Fle x y *)
red in |- *; auto with real.
Qed.
 
Lemma Fle_Zle :
 forall n1 n2 d : Z, (n1 <= n2)%Z -> Fle (Float n1 d) (Float n2 d).
(* Goal: forall (n1 n2 d : Z) (_ : Z.le n1 n2), Fle (Float n1 d) (Float n2 d) *)
intros; unfold Fle, FtoRradix, FtoR in |- *; simpl in |- *; auto.
(* Goal: Rle (Rmult (IZR n1) (powerRZ (IZR radix) d)) (Rmult (IZR n2) (powerRZ (IZR radix) d)) *)
case Zle_lt_or_eq with (1 := H); intros H1.
(* Goal: Rle (Rmult (IZR n1) (powerRZ (IZR radix) d)) (Rmult (IZR n2) (powerRZ (IZR radix) d)) *)
(* Goal: Rle (Rmult (IZR n1) (powerRZ (IZR radix) d)) (Rmult (IZR n2) (powerRZ (IZR radix) d)) *)
apply Rlt_le; auto with real.
(* Goal: Rle (Rmult (IZR n1) (powerRZ (IZR radix) d)) (Rmult (IZR n2) (powerRZ (IZR radix) d)) *)
rewrite <- H1; auto with real.
Qed.
 
Lemma Flt_Zlt :
 forall n1 n2 d : Z, (n1 < n2)%Z -> Flt (Float n1 d) (Float n2 d).
(* Goal: forall (n1 n2 d : Z) (_ : Z.lt n1 n2), Flt (Float n1 d) (Float n2 d) *)
intros; unfold Flt, FtoRradix, FtoR in |- *; simpl in |- *; auto with real.
Qed.
 
Lemma Fle_Fge : forall x y : float, Fle x y -> Fge y x.
(* Goal: forall (x y : float) (_ : Fle x y), Fge y x *)
unfold Fle, Fge in |- *; intros x y H'; auto with real.
Qed.
 
Lemma Fge_Zge :
 forall n1 n2 d : Z, (n1 >= n2)%Z -> Fge (Float n1 d) (Float n2 d).
(* Goal: forall (n1 n2 d : Z) (_ : Z.ge n1 n2), Fge (Float n1 d) (Float n2 d) *)
intros n1 n2 d H'; apply Fle_Fge; auto.
(* Goal: Fle (Float n2 d) (Float n1 d) *)
apply Fle_Zle; auto.
(* Goal: Z.le n2 n1 *)
apply Zge_le; auto.
Qed.
 
Lemma Flt_Fgt : forall x y : float, Flt x y -> Fgt y x.
(* Goal: forall (x y : float) (_ : Flt x y), Fgt y x *)
unfold Flt, Fgt in |- *; intros x y H'; auto.
Qed.
 
Lemma Fgt_Zgt :
 forall n1 n2 d : Z, (n1 > n2)%Z -> Fgt (Float n1 d) (Float n2 d).
(* Goal: forall (n1 n2 d : Z) (_ : Z.gt n1 n2), Fgt (Float n1 d) (Float n2 d) *)
intros n1 n2 d H'; apply Flt_Fgt; auto.
(* Goal: Flt (Float n2 d) (Float n1 d) *)
apply Flt_Zlt; auto.
(* Goal: Z.lt n2 n1 *)
apply Zgt_lt; auto.
Qed.
(* Arithmetic properties on F : Fle is reflexive, transitive, antisymmetric *)
 
Lemma Fle_refl : forall x y : float, Feq x y -> Fle x y.
(* Goal: forall (x y : float) (_ : Feq x y), Fle x y *)
unfold Feq in |- *; unfold Fle in |- *; intros.
(* Goal: Rle (FtoRradix x) (FtoRradix y) *)
rewrite H; auto with real.
Qed.
 
Lemma Fle_trans : forall x y z : float, Fle x y -> Fle y z -> Fle x z.
(* Goal: forall (x y z : float) (_ : Fle x y) (_ : Fle y z), Fle x z *)
unfold Fle in |- *; intros.
(* Goal: Rle (FtoRradix x) (FtoRradix z) *)
apply Rle_trans with (r2 := FtoR radix y); auto.
Qed.
 
Theorem Rlt_Fexp_eq_Zlt :
 forall x y : float, (x < y)%R -> Fexp x = Fexp y -> (Fnum x < Fnum y)%Z.
(* Goal: forall (x y : float) (_ : Rle (FtoRradix x) (FtoRradix y)) (_ : @eq Z (Fexp x) (Fexp y)), Z.le (Fnum x) (Fnum y) *)
intros x y H' H'0.
(* Goal: Z.lt (Fnum p) Z0 *)
apply lt_IZR.
apply (Rlt_monotony_contra_exp radix) with (z := Fexp x);
 auto with real arith.
(* Goal: Rle (Rmult (IZR (Fnum x)) (powerRZ (IZR radix) (Fexp x))) (Rmult (IZR (Fnum y)) (powerRZ (IZR radix) (Fexp x))) *)
pattern (Fexp x) at 2 in |- *; rewrite H'0; auto.
Qed.
 
Theorem Rle_Fexp_eq_Zle :
 forall x y : float, (x <= y)%R -> Fexp x = Fexp y -> (Fnum x <= Fnum y)%Z.
(* Goal: forall (x y : float) (_ : Rle (FtoRradix x) (FtoRradix y)) (_ : @eq Z (Fexp x) (Fexp y)), Z.le (Fnum x) (Fnum y) *)
intros x y H' H'0.
(* Goal: Z.le (Fnum p) Z0 *)
apply le_IZR.
apply (Rle_monotony_contra_exp radix) with (z := Fexp x);
 auto with real arith.
(* Goal: Rle (Rmult (IZR (Fnum x)) (powerRZ (IZR radix) (Fexp x))) (Rmult (IZR (Fnum y)) (powerRZ (IZR radix) (Fexp x))) *)
pattern (Fexp x) at 2 in |- *; rewrite H'0; auto.
Qed.
 
Theorem LtR0Fnum : forall p : float, (0 < p)%R -> (0 < Fnum p)%Z.
(* Goal: forall (p : float) (_ : Rle (FtoRradix p) (IZR Z0)), Z.le (Fnum p) Z0 *)
intros p H'.
(* Goal: Z.lt (Fnum p) Z0 *)
apply lt_IZR.
apply (Rlt_monotony_contra_exp radix) with (z := Fexp p);
 auto with real arith.
(* Goal: Rle (Rmult (IZR (Fnum p)) (powerRZ (IZR radix) (Fexp p))) (Rmult (IZR Z0) (powerRZ (IZR radix) (Fexp p))) *)
simpl in |- *; rewrite Rmult_0_l; auto.
Qed.
 
Theorem LeR0Fnum : forall p : float, (0 <= p)%R -> (0 <= Fnum p)%Z.
(* Goal: forall (p : float) (_ : Rle (FtoRradix p) (IZR Z0)), Z.le (Fnum p) Z0 *)
intros p H'.
(* Goal: Z.le (Fnum p) Z0 *)
apply le_IZR.
apply (Rle_monotony_contra_exp radix) with (z := Fexp p);
 auto with real arith.
(* Goal: Rle (Rmult (IZR (Fnum p)) (powerRZ (IZR radix) (Fexp p))) (Rmult (IZR Z0) (powerRZ (IZR radix) (Fexp p))) *)
simpl in |- *; rewrite Rmult_0_l; auto.
Qed.
 
Theorem LeFnumZERO : forall x : float, (0 <= Fnum x)%Z -> (0 <= x)%R.
(* Goal: forall (x : float) (_ : Z.le (Fnum x) Z0), Rle (FtoRradix x) (IZR Z0) *)
intros x H'; unfold FtoRradix, FtoR in |- *.
(* Goal: Rle (IZR Z0) (Rmult (IZR (Fnum x)) (powerRZ (IZR radix) (Fexp x))) *)
replace 0%R with (0%Z * 0%Z)%R; auto 6 with real zarith.
Qed.
 
Theorem R0LtFnum : forall p : float, (p < 0)%R -> (Fnum p < 0)%Z.
(* Goal: forall (p : float) (_ : Rle (FtoRradix p) (IZR Z0)), Z.le (Fnum p) Z0 *)
intros p H'.
(* Goal: Z.lt (Fnum p) Z0 *)
apply lt_IZR.
apply (Rlt_monotony_contra_exp radix) with (z := Fexp p);
 auto with real arith.
(* Goal: Rle (Rmult (IZR (Fnum p)) (powerRZ (IZR radix) (Fexp p))) (Rmult (IZR Z0) (powerRZ (IZR radix) (Fexp p))) *)
simpl in |- *; rewrite Rmult_0_l; auto.
Qed.
 
Theorem R0LeFnum : forall p : float, (p <= 0)%R -> (Fnum p <= 0)%Z.
(* Goal: forall (p : float) (_ : Rle (FtoRradix p) (IZR Z0)), Z.le (Fnum p) Z0 *)
intros p H'.
(* Goal: Z.le (Fnum p) Z0 *)
apply le_IZR.
apply (Rle_monotony_contra_exp radix) with (z := Fexp p);
 auto with real arith.
(* Goal: Rle (Rmult (IZR (Fnum p)) (powerRZ (IZR radix) (Fexp p))) (Rmult (IZR Z0) (powerRZ (IZR radix) (Fexp p))) *)
simpl in |- *; rewrite Rmult_0_l; auto.
Qed.
 
Theorem LeZEROFnum : forall x : float, (Fnum x <= 0)%Z -> (x <= 0)%R.
(* Goal: forall (x : float) (_ : Z.le (Fnum x) Z0), Rle (FtoRradix x) (IZR Z0) *)
intros x H'; unfold FtoRradix, FtoR in |- *.
(* Goal: Rle (Rmult (IZR (Fnum x)) (powerRZ (IZR radix) (Fexp x))) (IZR Z0) *)
apply Ropp_le_cancel; rewrite Ropp_0; rewrite <- Ropp_mult_distr_l_reverse.
(* Goal: Rle (IZR Z0) (Rmult (Ropp (IZR (Fnum x))) (powerRZ (IZR radix) (Fexp x))) *)
replace 0%R with (- 0%Z * 0)%R; auto 6 with real zarith.
Qed.
End comparisons.
Hint Resolve LeFnumZERO LeZEROFnum: float.