Fcomp.v


(****************************************************************************
                                                                             
          IEEE754  :  Fcomp                                                     
                                                                             
          Laurent Thery                                                      
                                                                             
*****************************************************************************
*)
Require Import Float.
Section comparisons.
Variable radix:nat.
Hypothesis radixMoreThanOne:(lt (S O) radix).

Local zr := (inject_nat radix).

Definition Fdiff :=
   [x, y:float]
   (Zminus
      (Zmult
         (Fnum x)
         (Zpower_nat zr (absolu (Zminus (Fexp x) (Zmin (Fexp x) (Fexp y))))))
      (Zmult
         (Fnum y)
         (Zpower_nat zr (absolu (Zminus (Fexp y) (Zmin (Fexp x) (Fexp y))))))).

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

Theorem Fdiff_correct:
  (x, y:float)
  (Rmult (Fdiff x y) (powerRZ radix (Zmin (Fexp x) (Fexp y))))==(Rminus x y).
Intros x y; Unfold Fdiff.
Rewrite <- Z_R_minus.
Rewrite Rmult_sym; Rewrite Rmult_Rminus_distr.
Repeat Rewrite Rmult_IZR.
Unfold zr; Repeat Rewrite Zpower_nat_powerRZ; Auto.
Rewrite (Rmult_sym (Fnum x)); Rewrite (Rmult_sym (Fnum y)).
Repeat Rewrite <- Rmult_assoc.
Repeat Rewrite <- powerRZ_add; Auto with real arith.
Repeat Rewrite inj_abs; Auto with arith.
Repeat Rewrite Zle_plus_minus; Auto.
Rewrite [t:R](Rmult_sym t (Fnum x)); Rewrite [t:R](Rmult_sym t (Fnum y)); Auto.
Apply Zsimpl_le_plus_l with p := (Zmin (Fexp x) (Fexp y)); Auto with arith.
Rewrite Zle_plus_minus; Rewrite Zero_right; Apply Zle_min_r; Auto.
Apply Zsimpl_le_plus_l with p := (Zmin (Fexp x) (Fexp y)); Auto with arith.
Rewrite Zle_plus_minus; Rewrite Zero_right; Apply Zle_min_l; Auto.
Qed.

(* Definition of  comparison functions*)

Definition Feq := [x, y:float]<R> x==y.

Definition Fle := [x, y:float](Rle x y).

Definition Flt := [x, y:float](Rlt x y).

Definition Fge := [x, y:float](Rge x y).

Definition Fgt := [x, y:float](Rgt x y).

Definition Fcompare := [x, y:float](Zcompare ZERO (Fdiff x y)).

Definition Feq_bool :=
   [x, y:float]
      Cases (Fcompare x y) of
          EGAL => true
         | _ => false
      end.

Theorem Feq_bool_correct_t: (x, y:float) (Feq_bool x y)=true ->(Feq x y).
Intros x y H'; Red.
Apply r_Rplus_plus with r := (Ropp y).
Repeat Rewrite (Rplus_sym (Ropp y)).
Rewrite Rplus_Ropp_r.
Change (Rminus x y)==R0.
Rewrite <- Fdiff_correct.
Apply without_div_Oi1; Auto.
Apply IZR_zero; Auto.
Apply sym_equal; Apply Zcompare_EGAL; Auto.
Generalize H'; Unfold Feq_bool Fcompare; Case (Zcompare ZERO (Fdiff x y)); 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 (Rminus x y)==R0.
Rewrite <- Fdiff_correct; Intros H'1; Case without_div_Od with 1 := H'1.
Intros H'0; Unfold Feq_bool Fcompare.
Rewrite (IZR_zero_r (Fdiff x y)); Auto.
Intros H'0; Contradict H'0.
Case (Zmin (Fexp x) (Fexp y)); Simpl; Auto 10 with real arith.
Apply r_Rplus_plus with r := (FtoR radix y).
Rewrite Rplus_Rminus; Rewrite Rplus_ne_l; 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; Intros H'0; Discriminate.
Qed.

Definition Flt_bool :=
   [x, y:float]
      Cases (Fcompare x y) of
          SUPERIEUR => true
         | _ => false
      end.

Theorem Flt_bool_correct_t: (x, y:float) (Flt_bool x y)=true ->(Flt x y).
Intros x y H'; Red.
Apply Rlt_anti_compatibility with r := (Ropp y).
Repeat Rewrite (Rplus_sym (Ropp y)).
Rewrite Rplus_Ropp_r.
Change (Rlt (Rminus x y) R0).
Rewrite <- Fdiff_correct.
Replace R0 with (Rmult (powerRZ radix (Zmin (Fexp x) (Fexp y))) R0);
 Auto with real arith.
Rewrite (Rmult_sym (Fdiff x y)).
Apply Rlt_monotony; Auto with real arith.
Replace R0 with (IZR ZERO); Auto with real arith.
Apply Rlt_IZR; Apply Zgt_lt; Red.
Generalize H'; Unfold Flt_bool Fcompare.
Case (Zcompare ZERO (Fdiff x y)); 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 (Rlt R0 (Rminus y x)); Auto with arith.
2:Apply Rlt_anti_compatibility with r := (FtoRradix x); AutoRewrite [Rsimpl];
   Auto with real.
Intros H'0.
Cut (Rlt (Fdiff x y) R0); Auto with arith.
Intros H'1.
Cut (Zlt (Fdiff x y) ZERO); Auto with zarith.
Intros H'2; Generalize (Zlt_Zcompare ? ? H'2);
 Unfold Flt_bool Fcompare Zcompare; Case (Fdiff x y); Auto with arith; Intros;
 Contradiction.
Apply lt_IZR; Auto with arith.
Apply (Rlt_mult_anticompatibility_exp radix) with z := (Zmin (Fexp x) (Fexp y));
 Auto with arith real; AutoRewrite [Rsimpl].
Rewrite Fdiff_correct; Auto with real.
Replace (Rminus x y) with (Ropp (Rminus y x)); [Idtac | Ring].
Apply Rgt_RoppO; Auto with arith.
Qed.

Theorem Flt_bool_correct_f: (x, y:float) (Flt_bool x y)=false ->(Fle y x).
Intros x y H'.
Case (total_order (FtoRradix y) (FtoRradix x)); Auto with real.
Intros H'0; Red; Apply Rlt_le; Auto with real.
Intros H'0; Elim H'0; Clear H'0; Intros H'1.
Red; Rewrite H'1; Auto with real.
Contradict H'; Rewrite Flt_bool_correct_r; Auto with real.
Red; Intros H'; Discriminate.
Qed.

Definition Fle_bool :=
   [x, y:float]
      Cases (Fcompare x y) of
          SUPERIEUR => true
         | EGAL => true
         | _ => 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; Apply eq_Rle; Auto with real.
Red; 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; 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; Case (Fcompare x y); Auto.
Generalize (Flt_bool_correct_r x y); Unfold Fle_bool Feq_bool Flt_bool;
 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 (total_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; Intros H'; Discriminate.
Red; Rewrite H'1; Auto with real.
Contradict H'.
Rewrite Fle_bool_correct_r; Auto with real.
Red; Intros H'; Discriminate.
Red; Auto with real.
Apply Rlt_le; Auto with real.
Qed.

Lemma Fle_Zle: (n1, n2, d:Z) (Zle n1 n2) ->(Fle (Float n1 d) (Float n2 d)).
Intros; Unfold Fle FtoRradix FtoR; Simpl; 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) (Zlt n1 n2) ->(Flt (Float n1 d) (Float n2 d)).
Intros; Unfold Flt FtoRradix FtoR; Simpl; Auto with real.
Qed.

Lemma Fle_Fge: (x, y:float) (Fle x y) ->(Fge y x).
Unfold Fle Fge; Intros x y H'; Auto with real.
Apply Rle_sym1; Auto.
Qed.

Lemma Fge_Zge: (n1, n2, d:Z) (Zge n1 n2) ->(Fge (Float n1 d) (Float n2 d)).
Intros n1 n2 d H'; Apply Fle_Fge; Auto.
Apply Fle_Zle; Auto.
Apply Zge_le; Auto.
Qed.

Lemma Flt_Fgt: (x, y:float) (Flt x y) ->(Fgt y x).
Unfold Flt Fgt; Intros x y H'; Auto.
Qed.

Lemma Fgt_Zgt: (n1, n2, d:Z) (Zgt n1 n2) ->(Fgt (Float n1 d) (Float n2 d)).
Intros n1 n2 d H'; Apply Flt_Fgt; Auto.
Apply Flt_Zlt; Auto.
Apply Zgt_lt; Auto.
Qed.
(* Arithmetic properties on F : Fle is reflexive, transitive, antisymmetric *)

Lemma Fle_refl: (x, y:float) (Feq x y) ->(Fle x y).
Unfold Feq; Unfold Fle; 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; Intros.
Apply Rle_trans with r2 := (FtoR radix y); Auto.
Qed.

Theorem Rlt_Fexp_eq_Zlt:
  (x, y:float) (Rlt x y) -> (Fexp x)=(Fexp y) ->(Zlt (Fnum x) (Fnum y)).
Intros x y H' H'0.
Apply lt_IZR.
Apply (Rlt_mult_anticompatibility_exp radix) with z := (Fexp x);
 Auto with real arith.
Pattern 2 (Fexp x); Rewrite H'0; Auto.
Qed.

Theorem Rle_Fexp_eq_Zle:
  (x, y:float) (Rle x y) -> (Fexp x)=(Fexp y) ->(Zle (Fnum x) (Fnum y)).
Intros x y H' H'0.
Apply le_IZR.
Apply (Rle_mult_anticompatibility_exp radix) with z := (Fexp x);
 Auto with real arith.
Pattern 2 (Fexp x); Rewrite H'0; Auto.
Qed.

Theorem LtR0Fnum: (p:float) (Rlt R0 p) ->(Zlt ZERO (Fnum p)).
Intros p H'.
Apply lt_IZR.
Apply (Rlt_mult_anticompatibility_exp radix) with z := (Fexp p);
 Auto with real arith.
AutoRewrite [Rsimpl]; Auto.
Qed.

Theorem LeR0Fnum: (p:float) (Rle R0 p) ->(Zle ZERO (Fnum p)).
Intros p H'.
Apply le_IZR.
Apply (Rle_mult_anticompatibility_exp radix) with z := (Fexp p);
 Auto with real arith.
AutoRewrite [Rsimpl]; Auto.
Qed.

Theorem LeFnumZERO: (x:float) (Zle ZERO (Fnum x)) ->(Rle R0 x).
Intros x H'; Unfold FtoRradix FtoR.
Replace R0 with (Rmult ZERO ZERO); Auto with real.
Apply Rle_Rmult_comp; Auto with real zarith arith.
Qed.

Theorem R0LtFnum: (p:float) (Rlt p R0) ->(Zlt (Fnum p) ZERO).
Intros p H'.
Apply lt_IZR.
Apply (Rlt_mult_anticompatibility_exp radix) with z := (Fexp p);
 Auto with real arith.
AutoRewrite [Rsimpl]; Auto.
Qed.

Theorem R0LeFnum: (p:float) (Rle p R0) ->(Zle (Fnum p) ZERO).
Intros p H'.
Apply le_IZR.
Apply (Rle_mult_anticompatibility_exp radix) with z := (Fexp p);
 Auto with real arith.
AutoRewrite [Rsimpl]; Auto.
Qed.

Theorem LeZEROFnum: (x:float) (Zle (Fnum x) ZERO) ->(Rle x R0).
Intros x H'; Unfold FtoRradix FtoR.
Apply Ropp_Rle; AutoRewrite [Rsimpl]; Rewrite <- Ropp_mul1.
Replace R0 with (Rmult (Ropp ZERO) ZERO); Auto with real.
Apply Rle_Rmult_comp; Auto with real zarith arith.
Simpl; AutoRewrite [Rsimpl]; Auto with real.
Qed.
End comparisons.
Hints Resolve LeFnumZERO LeZEROFnum :float.
14/12/100, 02:49