FPred.v

(****************************************************************************                                                                                         IEEE754  :  FPred                                                                                                                                              Laurent Thery                                                                                                                                     ***************************************************************************** *)
Require Import PolyList.
Require Import Float.
Require Import Fnorm.
Require Import Fop.
Require Import Fcomp.
Require Import FSucc.
Section pred.
Variable b:Fbound.
Variable radix:nat.
Variable precision:nat.

Local FtoRradix := (FtoR radix).
Coercion FtoRradix : float >-> R.
Hypothesis radixMoreThanOne:(lt (S O) radix).
Hypothesis precisionNotZero:~ precision=O.
Hypothesis pGivesBound:(vNum b)=(minus (exp radix precision) (1)).

Definition FPred :=
   [x:float]
      Cases (Z_eq_dec (Fnum x) (Zopp (vNum b))) of
          (left _) => (Float (Zopp (nNormMin radix precision)) (Zs (Fexp x)))
         | (right _) => Cases (Z_eq_dec (Fnum x) (nNormMin radix precision)) of
                            (left _) =>
                              Cases (Z_eq_dec (Fexp x) (Zopp (dExp b))) of
                                  (left _) => (Float (Zpred (Fnum x)) (Fexp x))
                                 | (right _) =>
                                     (Float (vNum b) (Zpred (Fexp x)))
                              end
                           | (right _) => (Float (Zpred (Fnum x)) (Fexp x))
                        end
      end.

Theorem FPredSimpl1:
  (x:float) (Fnum x)=(Zopp (vNum b)) ->
  (FPred x)=(Float (Zopp (nNormMin radix precision)) (Zs (Fexp x))).
Intros x H'; Unfold FPred.
Case (Z_eq_dec (Fnum x) (Zopp (vNum b))); Auto.
Intros H'0; Contradict H'0; Auto.
Qed.

Theorem FPredSimpl2:
  (x:float) (Fnum x)=(nNormMin radix precision) -> ~ (Fexp x)=(Zopp (dExp b)) ->
  (FPred x)=(Float (vNum b) (Zpred (Fexp x))).
Intros x H' H'0; Unfold FPred.
Case (Z_eq_dec (Fnum x) (Zopp (vNum b))); Auto.
Intros H'0; Absurd (Zlt O (vNum b)); Auto with zarith arith.
Apply inj_lt; Apply lt_vNum with 3 := pGivesBound; Auto.
Intros H'1; Case (Z_eq_dec (Fnum x) (nNormMin radix precision)).
Intros H'2; Case (Z_eq_dec (Fexp x) (Zopp (dExp b))); Auto.
Intros H'3; Contradict H'0; Auto.
Intros H'2; Contradict H'2; Auto.
Qed.

Theorem FPredSimpl3:
  (FPred (Float (nNormMin radix precision) (Zopp (dExp b))))=
  (Float (Zpred (nNormMin radix precision)) (Zopp (dExp b))).
Unfold FPred; Simpl.
Case (Z_eq_dec (nNormMin radix precision) (Zopp (vNum b))); Auto.
Intros H'0; Absurd (Zlt O (vNum b)); Auto with zarith arith.
Apply inj_lt; Apply lt_vNum with 3 := pGivesBound; Auto.
Intros H'; Case (Z_eq_dec (nNormMin radix precision) (nNormMin radix precision)).
Intros H'0; Case (Z_eq_dec (Zopp (dExp b)) (Zopp (dExp b))); Auto.
Intros H'1; Contradict H'1; Auto.
Intros H'1; Contradict H'1; Auto.
Qed.

Theorem FPredSimpl4:
  (x:float)
  ~ (Fnum x)=(Zopp (vNum b)) -> ~ (Fnum x)=(nNormMin radix precision) ->
  (FPred x)=(Float (Zpred (Fnum x)) (Fexp x)).
Intros x H' H'0; Unfold FPred.
Case (Z_eq_dec (Fnum x) (Zopp (vNum b))); Auto.
Intros H'1; Contradict H'; Auto.
Intros H'1; Case (Z_eq_dec (Fnum x) (nNormMin radix precision)); Auto.
Intros H'2; Contradict H'0; Auto.
Qed.

Theorem FPredFopFSucc:
  (x:float)(FPred x)=(Fopp (FSucc b radix precision (Fopp x))).
Intros x.
Case (Z_eq_dec (Fnum x) (Zopp (vNum b))); Intros H'1.
Rewrite FPredSimpl1; Auto; Rewrite FSuccSimpl1; Auto.
Unfold Fopp; Simpl; Rewrite H'1; Auto with zarith.
Case (Z_eq_dec (Fnum x) (nNormMin radix precision)); Intros H'2.
Case (Z_eq_dec (Fexp x) (Zopp (dExp b))); Intros H'3.
Replace x with (Float (Fnum x) (Fexp x)).
Rewrite H'2; Rewrite H'3; Rewrite FPredSimpl3; Unfold Fopp; Simpl;
Rewrite FSuccSimpl3; Simpl; Auto.
Rewrite <- Zopp_Zpred_Zs; Rewrite Zopp_Zopp; Auto.
Case x; Simpl; Auto.
Rewrite FPredSimpl2; Auto; Rewrite FSuccSimpl2; Unfold Fopp; Simpl;
Try Rewrite Zopp_Zopp; Auto.
Rewrite H'2; Auto.
Rewrite FPredSimpl4; Auto; Rewrite FSuccSimpl4; Auto.
Unfold Fopp; Simpl; Rewrite <- Zopp_Zpred_Zs; Rewrite Zopp_Zopp; Auto.
Unfold Fopp; Simpl; Contradict H'1; Rewrite <- H'1; Rewrite Zopp_Zopp; Auto.
Unfold Fopp; Simpl; Contradict H'2; Auto with zarith.
Qed.

Theorem FPredDiff1:
  (x:float) ~ (Fnum x)=(nNormMin radix precision) ->
  <R> (Fminus radix x (FPred x))==(Float (1) (Fexp x)).
Intros x H'; Rewrite (FPredFopFSucc x).
Pattern 1 x; Rewrite <- (Fopp_Fopp x).
Rewrite <- Fopp_Fminus_dist.
Rewrite Fopp_Fminus.
Unfold FtoRradix; Rewrite FSuccDiff1; Auto.
Replace (Fnum (Fopp x)) with (Zopp (Fnum x)).
Contradict H'; Rewrite <- (Zopp_Zopp (Fnum x)); Rewrite H'; Auto with zarith.
Case x; Simpl; Auto.
Qed.

Theorem FPredDiff2:
  (x:float) (Fnum x)=(nNormMin radix precision) -> (Fexp x)=(Zopp (dExp b)) ->
  <R> (Fminus radix x (FPred x))==(Float (1) (Fexp x)).
Intros x H' H'0; Rewrite (FPredFopFSucc x).
Pattern 1 x; Rewrite <- (Fopp_Fopp x).
Rewrite <- Fopp_Fminus_dist.
Rewrite Fopp_Fminus.
Unfold FtoRradix; Rewrite FSuccDiff2; Auto.
Rewrite <- H'; Case x; Auto.
Qed.

Theorem FPredDiff3:
  (x:float) (Fnum x)=(nNormMin radix precision) -> ~ (Fexp x)=(Zopp (dExp b)) ->
  <R> (Fminus radix x (FPred x))==(Float (1) (Zpred (Fexp x))).
Intros x H' H'0; Rewrite (FPredFopFSucc x).
Pattern 1 x; Rewrite <- (Fopp_Fopp x).
Rewrite <- Fopp_Fminus_dist.
Rewrite Fopp_Fminus.
Unfold FtoRradix; Rewrite FSuccDiff3; Auto.
Rewrite <- H'; Case x; Auto.
Qed.

Theorem FBoundedPred: (f:float) (Fbounded b f) ->(Fbounded b (FPred f)).
Intros f H'; Rewrite (FPredFopFSucc f); Auto with float.
Qed.

Theorem FPredCanonic:
  (a:float) (Fcanonic radix b precision a) ->
  (Fcanonic radix b precision (FPred a)).
Intros a H'.
Rewrite FPredFopFSucc; Auto with float.
Qed.

Theorem FPredLt: (a:float)(Rlt (FPred a) a).
Intros a; Rewrite FPredFopFSucc.
Pattern 2 a; Rewrite <- (Fopp_Fopp a).
Unfold FtoRradix; Repeat Rewrite Fopp_correct.
Apply Rlt_Ropp.
Rewrite <- Fopp_correct; Auto with float.
Qed.

Theorem R0RltRleSucc: (x:float) (Rlt R0 x) ->(Rle R0 (FPred x)).
Intros x H'; Rewrite FPredFopFSucc.
Unfold FtoRradix; Repeat Rewrite Fopp_correct.
Replace R0 with (Ropp R0); Auto with real.
Apply Rle_Ropp.
Apply R0RltRleSucc; Auto.
Unfold FtoRradix; Repeat Rewrite Fopp_correct.
Replace R0 with (Ropp R0); Auto with real.
Qed.

Theorem FPredProp:
  (x, y:float)
  (Fcanonic radix b precision x) ->
  (Fcanonic radix b precision y) -> (Rlt x y) ->(Rle x (FPred y)).
Intros x y H' H'0 H'1; Rewrite FPredFopFSucc.
Rewrite <- (Fopp_Fopp x).
Unfold FtoRradix; Rewrite Fopp_correct with x := (Fopp x).
Rewrite Fopp_correct with x := (FSucc b radix precision (Fopp y));
Auto with float real.
Apply Rle_Ropp.
Apply FSuccProp; Auto with float.
Repeat Rewrite Fopp_correct; Auto with real.
Qed.

Theorem FPredZleEq:
  (p, q:float) (Rlt (FPred p) q) -> (Rle q p) -> (Zle (Fexp p) (Fexp q)) ->
  <R> p==q.
Intros p q H' H'0 H'1.
Rewrite <- (Ropp_Ropp p); Rewrite <- (Ropp_Ropp q); Apply eq_Ropp.
Unfold FtoRradix; Repeat Rewrite <- Fopp_correct.
Apply FSuccZleEq with b := b precision := precision; Auto.
Repeat Rewrite Fopp_correct; Auto with real.
Apply Ropp_Rlt.
Repeat Rewrite <- Fopp_correct; Rewrite <- FPredFopFSucc; Rewrite Fopp_Fopp;
Auto.
Qed.

Definition FNPred := [x:float](FPred (Fnormalize radix b precision x)).

Theorem FNPredFopFNSucc:
  (x:float)(FNPred x)=(Fopp (FNSucc b radix precision (Fopp x))).
Intros x; Unfold FNPred FNSucc; Auto.
Rewrite Fnormalize_Fopp; Auto.
Apply FPredFopFSucc; Auto.
Qed.

Theorem FNPredCanonic:
  (a:float) (Fbounded b a) ->(Fcanonic radix b precision (FNPred a)).
Intros a H'; Unfold FNPred.
Apply FPredCanonic; Auto with float.
Qed.

Theorem FNPredLt: (a:float)(Rlt (FNPred a) a).
Intros a; Unfold FNPred.
Unfold FtoRradix;
Rewrite <- (FnormalizeCorrect ? radixMoreThanOne b precision a).
Apply FPredLt; Auto.
Qed.

Theorem FNPredProp:
  (x, y:float) (Fbounded b x) -> (Fbounded b y) -> (Rlt x y) ->
  (Rle x (FNPred y)).
Intros x y H' H'0 H'1; Unfold FNPred.
Replace (FtoRradix x) with (FtoRradix (Fnormalize radix b precision x)).
Apply FPredProp; Auto with float.
Unfold FtoRradix; Repeat Rewrite FnormalizeCorrect; Auto.
Unfold FtoRradix; Repeat Rewrite FnormalizeCorrect; Auto.
Qed.

Theorem FPredSuc:
  (x:float) (Fcanonic radix b precision x) ->
  (FPred (FSucc b radix precision x))=x.
Intros x H; Unfold FPred FSucc.
Case (Z_eq_dec (Fnum x) (vNum b)); Simpl.
Case (Z_eq_dec (nNormMin radix precision) (Zopp (vNum b))); Simpl.
Intros H'; Contradict H'; Apply sym_not_equal; Apply Zlt_not_eq; Auto.
Apply Zlt_le_trans with (Zopp O).
Apply Zlt_Zopp; Apply inj_lt.
Apply lt_vNum with radix := radix precision := precision; Auto.
Auto with zarith arith.
Case (Z_eq_dec (nNormMin radix precision) (nNormMin radix precision)); Simpl.
Case (Z_eq_dec (Zs (Fexp x)) (Zopp (dExp b))); Simpl.
Intros H' H'0 H'1 H'2; Absurd (Zle (Zopp (dExp b)) (Fexp x)); Auto.
Rewrite <- H'; Auto with zarith.
Intuition.
Replace (Zpred (Zs (Fexp x))) with (Fexp x); [Idtac | Unfold Zs Zpred; Ring].
Intros H' H'0 H'1 H'2; Rewrite <- H'2; Auto.
Apply floatEq; Auto.
Intros H'; Case H'; Auto.
Case (Z_eq_dec (Fnum x) (Zopp (nNormMin radix precision))); Simpl.
Case (Z_eq_dec (Fexp x) (Zopp (dExp b))); Simpl.
Case (Z_eq_dec (Zs (Fnum x)) (Zopp (vNum b))); Simpl.
Intros H'; Absurd (Zle (Zopp (vNum b)) (Fnum x)).
Rewrite <- H'; Auto with zarith.
Intuition.
Case (Z_eq_dec (Zs (Fnum x)) (nNormMin radix precision)); Simpl.
Intros H' H'0 H'1 H'2; Contradict H'2.
Rewrite <- H'; Auto with zarith.
Replace (Zpred (Zs (Fnum x))) with (Fnum x); [Idtac | Unfold Zs Zpred; Ring];
Auto.
Intros H' H'0 H'1 H'2 H'3; Apply floatEq; Auto.
Case (Z_eq_dec (Zopp (vNum b)) (Zopp (vNum b))); Auto.
Intros H' H'0 H'1 H'2; Rewrite <- H'1.
Replace (Zs (Zpred (Fexp x))) with (Fexp x); [Idtac | Unfold Zs Zpred; Ring];
Auto.
Apply floatEq; Auto.
Intros H'; Case H'; Auto.
Case (Z_eq_dec (Zs (Fnum x)) (Zopp (vNum b))); Simpl.
Intros H'; Absurd (Zle (Zopp (vNum b)) (Fnum x)).
Rewrite <- H'; Auto with zarith.
Intuition.
Case (Z_eq_dec (Zs (Fnum x)) (nNormMin radix precision)); Simpl.
Case (Z_eq_dec (Fexp x) (Zopp (dExp b))); Simpl.
Intros H' H'0 H'1 H'2 H'3.
Replace (Zpred (Zs (Fnum x))) with (Fnum x); [Idtac | Unfold Zs Zpred; Ring];
Auto.
Apply floatEq; Auto.
Intros H' H'0 H'1 H'2 H'3; Case H.
Intros H'4; Absurd (le (nNormMin radix precision) (absolu (Fnum x))).
Replace (Fnum x) with (Zpred (Zs (Fnum x))); [Idtac | Unfold Zs Zpred; Ring];
Auto.
Rewrite H'0.
Generalize (nNormNotZero ? radixMoreThanOne precision);
Case (nNormMin radix precision); Auto.
Intros n H'5; Replace (Zpred (S n)) with (INZ n); Auto.
Rewrite absolu_INR; Auto with arith.
Unfold INZ; Rewrite inj_S; Auto.
Unfold Zpred Zs; Ring.
Apply pNormal_absolu_min with b := b; Auto.
Intros H'4; Contradict H'; Intuition.
Intros H' H'0 H'1 H'2; Apply floatEq; Simpl; Auto.
Unfold Zpred Zs; Ring.
Qed.

Theorem FSucPred:
  (x:float) (Fcanonic radix b precision x) ->
  (FSucc b radix precision (FPred x))=x.
Intros x H; Unfold FPred FSucc.
Case (Z_eq_dec (Fnum x) (Zopp (vNum b))); Simpl.
Case (Z_eq_dec (Zopp (nNormMin radix precision)) (vNum b)); Simpl.
Intros H'; Contradict H'; Apply Zlt_not_eq; Auto.
Rewrite <- (Zopp_Zopp (vNum b)); Apply Zlt_Zopp.
Apply Zlt_le_trans with (Zopp O).
Apply Zlt_Zopp; Apply inj_lt.
Apply lt_vNum with radix := radix precision := precision; Auto.
Auto with zarith arith.
Case (Z_eq_dec
        (Zopp (nNormMin radix precision)) (Zopp (nNormMin radix precision)));
Simpl.
Case (Z_eq_dec (Zs (Fexp x)) (Zopp (dExp b))); Simpl.
Intros H' H'0 H'1 H'2; Absurd (Zle (Zopp (dExp b)) (Fexp x)); Auto.
Rewrite <- H'; Auto with zarith.
Intuition.
Intros H' H'0 H'1 H'2; Rewrite <- H'2; Apply floatEq; Simpl; Auto;
Unfold Zs Zpred; Ring.
Intros H'; Case H'; Auto.
Case (Z_eq_dec (Fnum x) (nNormMin radix precision)); Simpl.
Case (Z_eq_dec (Fexp x) (Zopp (dExp b))); Simpl.
Case (Z_eq_dec (Zpred (Fnum x)) (vNum b)); Simpl.
Intros H' H'0 H'1 H'2; Absurd (Zle (nNormMin radix precision) (vNum b)).
Rewrite <- H'; Rewrite H'1; Auto with zarith.
Apply Zlt_not_le; Auto with zarith.
Apply Zlt_pred_n_n; Auto.
Rewrite <- H'1; Intuition.
Case (Z_eq_dec (Zpred (Fnum x)) (Zopp (nNormMin radix precision))); Simpl.
Intros H' H'0 H'1 H'2 H'3; Contradict H'.
Rewrite H'2; Auto.
Case (nNormMin radix precision).
Simpl; Red; Intros; Discriminate.
Intros n; Replace (Zpred (S n)) with (inject_nat n).
Apply sym_not_equal; Apply Zlt_not_eq; Auto.
Apply Zlt_le_trans with (inject_nat O); Auto with zarith arith.
Simpl; Red; Simpl; Auto.
Rewrite inj_S; Unfold Zpred Zs; Ring; Auto.
Intros H' H'0 H'1 H'2 H'3; Apply floatEq; Simpl; Auto; Unfold Zpred Zs; Ring.
Case (Z_eq_dec (vNum b) (vNum b)); Auto.
Intros H' H'0 H'1 H'2; Rewrite <- H'1; Apply floatEq; Simpl; Auto;
Unfold Zpred Zs; Ring.
Intros H'; Case H'; Auto.
Case (Z_eq_dec (Zpred (Fnum x)) (vNum b)); Simpl.
Intros H'; Absurd (Zle (Fnum x) (vNum b)).
Rewrite <- H'.
Apply Zlt_not_le; Apply Zlt_pred_n_n; Auto.
Intuition.
Case (Z_eq_dec (Zpred (Fnum x)) (Zopp (nNormMin radix precision))); Simpl.
Case (Z_eq_dec (Fexp x) (Zopp (dExp b))); Simpl.
Intros H' H'0 H'1 H'2 H'3; Apply floatEq; Simpl; Auto; Unfold Zs Zpred; Ring.
Intros H' H'0 H'1 H'2 H'3; Case H; Intros C0.
Absurd (le (nNormMin radix precision) (absolu (Fnum x))).
Replace (Fnum x) with (Zs (Zpred (Fnum x))); [Idtac | Unfold Zs Zpred; Ring].
Rewrite H'0.
Generalize (nNormNotZero ? radixMoreThanOne precision);
Case (nNormMin radix precision); Auto.
Intros n H'4; Rewrite <- Zopp_Zpred_Zs; Replace (Zpred (S n)) with (INZ n).
Rewrite absolu_Zopp; Rewrite absolu_INR; Auto with arith.
Unfold INZ; Rewrite inj_S; Auto.
Unfold Zpred Zs; Ring.
Apply pNormal_absolu_min with b := b; Auto.
Contradict H'; Intuition.
Intros H' H'0 H'1 H'2; Apply floatEq; Simpl; Auto.
Unfold Zpred Zs; Ring.
Qed.

Theorem FNPredSuc:
  (x:float) (Fbounded b x) -><R> (FNPred (FNSucc b radix precision x))==x.
Intros x H'; Unfold FNPred; Rewrite FcanonicFormalizeEq; Auto.
Unfold FNSucc; Rewrite FPredSuc; Auto.
Unfold FtoRradix; Apply FnormalizeCorrect; Auto.
Apply FnormalizeCanonic; Auto.
Apply FNSuccCanonic; Auto.
Qed.

Theorem FNPredSucEq:
  (x:float) (Fcanonic radix b precision x) ->
  (FNPred (FNSucc b radix precision x))=x.
Intros x H'.
Apply FcanonicUnique with 5 := H'; Auto.
Apply FNPredCanonic; Auto.
Apply FcanonicBound with radix := radix precision := precision; Auto.
Apply FNSuccCanonic; Auto.
Apply FcanonicBound with radix := radix precision := precision; Auto.
Apply FNPredSuc; Auto.
Apply FcanonicBound with radix := radix precision := precision; Auto.
Qed.

Theorem FNSucPred:
  (x:float) (Fbounded b x) -><R> (FNSucc b radix precision (FNPred x))==x.
Intros x H'; Unfold FNSucc; Rewrite FcanonicFormalizeEq; Auto.
Unfold FNPred; Rewrite FSucPred; Auto.
Unfold FtoRradix; Apply FnormalizeCorrect; Auto.
Apply FnormalizeCanonic; Auto.
Apply FNPredCanonic; Auto.
Qed.

Theorem FNSucPredEq:
  (x:float) (Fcanonic radix b precision x) ->
  (FNSucc b radix precision (FNPred x))=x.
Intros x H'.
Apply FcanonicUnique with 5 := H'; Auto.
Apply FNSuccCanonic; Auto.
Apply FcanonicBound with radix := radix precision := precision; Auto.
Apply FNPredCanonic; Auto.
Apply FcanonicBound with radix := radix precision := precision; Auto.
Apply FNSucPred; Auto.
Apply FcanonicBound with radix := radix precision := precision; Auto.
Qed.
End pred.
Hints Resolve
FBoundedPred FPredCanonic FPredLt R0RltRleSucc FPredProp FNPredCanonic FNPredLt
FNPredProp :float.

14/12/100, 15:07