(****************************************************************************
                                                                             
          IEEE754  :  Fround                                                     
                                                                             
          Laurent Thery                                                      
                                                                             
  ******************************************************************************)
Require Export Fprop.
Require Export Fodd.
Section FRound.
Variable b : Fbound.
Variable radix : Z.
Variable precision : nat.
 
Let FtoRradix := FtoR radix.
Local Coercion FtoRradix : float >-> R.

Hypothesis radixMoreThanOne : (1 < radix)%Z.
Hypothesis precisionGreaterThanOne : 1 < precision.
Hypothesis pGivesBound : Zpos (vNum b) = Zpower_nat radix precision.
 
Definition TotalP (P : R -> float -> Prop) :=
  forall r : R, exists p : float, P r p.
 
Definition UniqueP (P : R -> float -> Prop) :=
  forall (r : R) (p q : float), P r p -> P r q -> p = q :>R.
 
Definition CompatibleP (P : R -> float -> Prop) :=
  forall (r1 r2 : R) (p q : float),
  P r1 p -> r1 = r2 -> p = q :>R -> Fbounded b q -> P r2 q.
 
Definition MinOrMaxP (P : R -> float -> Prop) :=
  forall (r : R) (p : float), P r p -> isMin b radix r p \/ isMax b radix r p.
 
Definition RoundedModeP (P : R -> float -> Prop) :=
  TotalP P /\ CompatibleP P /\ MinOrMaxP P /\ MonotoneP radix P.
 
Theorem RoundedModeP_inv1 : forall P, RoundedModeP P -> TotalP P.
(* Goal: forall (P : forall (_ : R) (_ : float), Prop) (_ : RoundedModeP P), TotalP P *)
intros P H; case H; auto.
Qed.
 
Theorem RoundedModeP_inv2 : forall P, RoundedModeP P -> CompatibleP P.
(* Goal: forall (P : forall (_ : R) (_ : float), Prop) (_ : RoundedModeP P), CompatibleP P *)
intros P H; Casec H; intros H H1; Casec H1; auto.
Qed.
 
Theorem RoundedModeP_inv3 : forall P, RoundedModeP P -> MinOrMaxP P.
(* Goal: forall (P : forall (_ : R) (_ : float), Prop) (_ : RoundedModeP P), MonotoneP radix P *)
intros P H; Casec H; intros H H1; Casec H1; intros H1 H2; Casec H2; auto.
Qed.
 
Theorem RoundedModeP_inv4 : forall P, RoundedModeP P -> MonotoneP radix P.
(* Goal: forall (P : forall (_ : R) (_ : float), Prop) (_ : RoundedModeP P), MonotoneP radix P *)
intros P H; Casec H; intros H H1; Casec H1; intros H1 H2; Casec H2; auto.
Qed.
Hint Resolve RoundedModeP_inv1 RoundedModeP_inv2 RoundedModeP_inv3
  RoundedModeP_inv4: inv.
 
Theorem RoundedProjector : forall P, RoundedModeP P -> ProjectorP b radix P.
intros P H'; red in |- *; simpl in |- *.
intros p q H'0 H'1.
red in H'.
elim H'; intros H'2 H'3; elim H'3; intros H'4 H'5; elim H'5; intros H'6 H'7;
 case (H'6 p q); clear H'5 H'3 H'; auto.
intros H'; apply (ProjectMin b radix p); auto.
intros H'; apply (ProjectMax b radix p); auto.
Qed.
 
Theorem MinCompatible : CompatibleP (isMin b radix).
(* Goal: UniqueP ToInfinityP *)
red in |- *.
(* Goal: forall (r1 r2 : R) (p q : float) (_ : isMax b radix r1 p) (_ : @eq R r1 r2) (_ : @eq R (FtoRradix p) (FtoRradix q)) (_ : Fbounded b q), isMax b radix r2 q *)
intros r1 r2 p q H' H'0 H'1 H'2; split; auto.
(* Goal: and (Rle r2 (FtoR radix q)) (forall (f : float) (_ : Fbounded b f) (_ : Rle r2 (FtoR radix f)), Rle (FtoR radix q) (FtoR radix f)) *)
rewrite <- H'0; unfold FtoRradix in H'1; rewrite <- H'1; case H'; auto.
Qed.
 
Theorem MinRoundedModeP : RoundedModeP (isMin b radix).
(* Goal: UniqueP ToInfinityP *)
split; try red in |- *.
(* Goal: forall r : R, @ex float (fun p : float => isMin b radix r p) *)
(* Goal: and (CompatibleP (isMin b radix)) (and (MinOrMaxP (isMin b radix)) (MonotoneP radix (isMin b radix))) *)
intros r; apply MinEx with (precision := precision); auto with arith.
(* Goal: and (CompatibleP (isMin b radix)) (and (MinOrMaxP (isMin b radix)) (MonotoneP radix (isMin b radix))) *)
split; try exact MinCompatible.
(* Goal: and (MinOrMaxP (isMin b radix)) (MonotoneP radix (isMin b radix)) *)
split; try apply MonotoneMin; red in |- *; auto.
Qed.
 
Theorem MaxCompatible : CompatibleP (isMax b radix).
(* Goal: UniqueP ToInfinityP *)
red in |- *.
(* Goal: forall (r1 r2 : R) (p q : float) (_ : isMax b radix r1 p) (_ : @eq R r1 r2) (_ : @eq R (FtoRradix p) (FtoRradix q)) (_ : Fbounded b q), isMax b radix r2 q *)
intros r1 r2 p q H' H'0 H'1 H'2; split; auto.
(* Goal: and (Rle r2 (FtoR radix q)) (forall (f : float) (_ : Fbounded b f) (_ : Rle r2 (FtoR radix f)), Rle (FtoR radix q) (FtoR radix f)) *)
rewrite <- H'0; unfold FtoRradix in H'1; rewrite <- H'1; case H'; auto.
Qed.
 
Theorem MaxRoundedModeP : RoundedModeP (isMax b radix).
(* Goal: UniqueP ToInfinityP *)
split; try red in |- *.
(* Goal: forall r : R, @ex float (fun p : float => isMax b radix r p) *)
(* Goal: and (CompatibleP (isMax b radix)) (and (MinOrMaxP (isMax b radix)) (MonotoneP radix (isMax b radix))) *)
intros r; apply MaxEx with (precision := precision); auto with arith.
(* Goal: and (CompatibleP (isMax b radix)) (and (MinOrMaxP (isMax b radix)) (MonotoneP radix (isMax b radix))) *)
split; try exact MaxCompatible.
(* Goal: and (MinOrMaxP (isMax b radix)) (MonotoneP radix (isMax b radix)) *)
split; try apply MonotoneMax; red in |- *; auto.
Qed.
 
Definition ToZeroP (r : R) (p : float) :=
  (0 <= r)%R /\ isMin b radix r p \/ (r <= 0)%R /\ isMax b radix r p.
 
Theorem ToZeroTotal : TotalP ToZeroP.
(* Goal: TotalP ToInfinityP *)
red in |- *; intros r; case (Rle_or_lt r 0); intros H1.
(* Goal: @ex float (fun p : float => ToInfinityP r p) *)
case MaxEx with (r := r) (3 := pGivesBound); auto with arith.
(* Goal: forall (x : float) (_ : isMin b radix r x), @ex float (fun p : float => ToInfinityP r p) *)
(* Goal: @ex float (fun p : float => ToInfinityP r p) *)
intros x H'; exists x; red in |- *; auto.
(* Goal: @ex float (fun p : float => ToInfinityP r p) *)
(* Goal: @ex float (fun p : float => ToInfinityP r p) *)
case MinEx with (r := r) (3 := pGivesBound); auto with arith.
(* Goal: forall (x : float) (_ : isMin b radix r x), @ex float (fun p : float => ToZeroP r p) *)
intros x H'; exists x; red in |- *; left; split; auto.
(* Goal: Rle (IZR Z0) r *)
apply Rlt_le; auto.
Qed.
 
Theorem ToZeroCompatible : CompatibleP ToZeroP.
(* Goal: UniqueP ToInfinityP *)
red in |- *.
(* Goal: forall (r1 r2 : R) (p q : float) (_ : ToInfinityP r1 p) (_ : @eq R r1 r2) (_ : @eq R (FtoRradix p) (FtoRradix q)) (_ : Fbounded b q), ToInfinityP r2 q *)
intros r1 r2 p q H'; case H'.
intros H'0 H'1 H'2; left; split;
 try apply MinCompatible with (p := p) (r1 := r1); 
 try rewrite <- H'1; auto; case H'0; auto.
intros H'0 H'1 H'2; right; split;
 try apply MaxCompatible with (p := p) (r1 := r1); 
 try rewrite <- H'1; auto; case H'0; auto.
Qed.
 
Theorem ToZeroMinOrMax : MinOrMaxP ToZeroP.
(* Goal: UniqueP ToInfinityP *)
red in |- *.
(* Goal: forall (r : R) (p : float) (_ : ToInfinityP r p), or (isMin b radix r p) (isMax b radix r p) *)
intros r p H'; case H'; clear H'; intros H'; case H'; auto.
Qed.
 
Theorem ToZeroMonotone : MonotoneP radix ToZeroP.
(* Goal: UniqueP ToInfinityP *)
red in |- *.
cut (FtoR radix (Fzero (- dExp b)) = 0%R);
 [ intros Eq0 | unfold FtoR in |- *; simpl in |- * ]; 
 auto with real.
(* Goal: forall (p q : R) (p' q' : float) (_ : Rlt p q) (_ : ToZeroP p p') (_ : ToZeroP q q'), Rle (FtoR radix p') (FtoR radix q') *)
simpl in |- *; intros p q p' q' H' H'0; case H'0; clear H'0.
(* Goal: forall (_ : and (Rle (IZR Z0) p) (isMin b radix p p')) (_ : ToZeroP q q'), Rle (FtoR radix p') (FtoR radix q') *)
(* Goal: forall (_ : and (Rle p (IZR Z0)) (isMax b radix p p')) (_ : ToZeroP q q'), Rle (FtoR radix p') (FtoR radix q') *)
intros H'0; elim H'0; intros H'1 H'2; clear H'0; intros H'0.
(* Goal: Rle (FtoR radix p') (FtoR radix q') *)
(* Goal: forall (_ : and (Rle p (IZR Z0)) (isMax b radix p p')) (_ : ToZeroP q q'), Rle (FtoR radix p') (FtoR radix q') *)
case H'0; intros H'3; elim H'3; clear H'3; auto.
(* Goal: forall (_ : Rle q (IZR Z0)) (_ : isMax b radix q q'), Rle (FtoR radix p') (FtoR radix q') *)
(* Goal: forall (_ : and (Rle p (IZR Z0)) (isMax b radix p p')) (_ : ToZeroP q q'), Rle (FtoR radix p') (FtoR radix q') *)
intros H'3 H'4.
(* Goal: Rle (FtoR radix p') (FtoR radix q') *)
(* Goal: forall (_ : Rle q (IZR Z0)) (_ : isMax b radix q q'), Rle (FtoR radix p') (FtoR radix q') *)
(* Goal: forall (_ : and (Rle p (IZR Z0)) (isMax b radix p p')) (_ : ToZeroP q q'), Rle (FtoR radix p') (FtoR radix q') *)
apply (MonotoneMin b radix) with (p := p) (q := q); auto.
(* Goal: forall (_ : Rle q (IZR Z0)) (_ : isMax b radix q q'), Rle (FtoR radix p') (FtoR radix q') *)
(* Goal: forall (_ : and (Rle p (IZR Z0)) (isMax b radix p p')) (_ : ToZeroP q q'), Rle (FtoR radix p') (FtoR radix q') *)
intros H'3 H'4.
(* Goal: Rle (FtoR radix p') (FtoR radix q') *)
(* Goal: forall (_ : and (Rle p (IZR Z0)) (isMax b radix p p')) (_ : ToZeroP q q'), Rle (FtoR radix p') (FtoR radix q') *)
apply Rle_trans with p; [ apply isMin_inv1 with (1 := H'2); auto | idtac ].
(* Goal: Rle p (FtoR radix q') *)
(* Goal: forall (_ : and (Rle p (IZR Z0)) (isMax b radix p p')) (_ : ToZeroP q q'), Rle (FtoR radix p') (FtoR radix q') *)
apply Rle_trans with q; [ idtac | apply isMax_inv1 with (1 := H'4) ]; auto.
(* Goal: Rle (IZR Z0) r *)
apply Rlt_le; auto.
(* Goal: forall (_ : and (Rle p (IZR Z0)) (isMax b radix p p')) (_ : ToZeroP q q'), Rle (FtoR radix p') (FtoR radix q') *)
intros H'0; elim H'0; intros H'1 H'2; clear H'0.
intros H'0; case H'0; clear H'0; intros H'0; case H'0; intros H'3 H'4;
 clear H'0.
(* Goal: Rle (FtoR radix p') (FtoR radix q') *)
(* Goal: Rle (FtoR radix p') (FtoR radix q') *)
apply Rle_trans with (FtoRradix (Fzero (- dExp b))); auto.
(* Goal: Rle (FtoR radix p') (FtoRradix (Fzero (Z.opp (Z.of_N (dExp b))))) *)
(* Goal: Rle (FtoRradix (Fzero (Z.opp (Z.of_N (dExp b))))) (FtoR radix q') *)
(* Goal: Rle (FtoR radix p') (FtoR radix q') *)
elim H'2.
(* Goal: forall (_ : Fbounded b q') (_ : and (Rle (FtoR radix q') q) (forall (f : float) (_ : Fbounded b f) (_ : Rle (FtoR radix f) q), Rle (FtoR radix f) (FtoR radix q'))), Rle (FtoRradix (Fzero (Z.opp (Z.of_N (dExp b))))) (FtoR radix q') *)
(* Goal: Rle (FtoR radix p') (FtoR radix q') *)
intros H'0 H'5; elim H'5; intros H'6 H'7; apply H'7; clear H'5; auto.
(* Goal: Fbounded b (Fzero (Z.opp (Z.of_N (dExp b)))) *)
(* Goal: Rle (FtoR radix (Fzero (Z.opp (Z.of_N (dExp b))))) q *)
(* Goal: Rle (FtoR radix p') (FtoR radix q') *)
repeat split; simpl in |- *; auto with zarith.
(* Goal: Rle (FtoR radix (Fzero (Z.opp (Z.of_N (dExp b))))) q *)
(* Goal: Rle (FtoR radix p') (FtoR radix q') *)
rewrite Eq0; auto.
(* Goal: Rle (FtoRradix (Fzero (Z.opp (Z.of_N (dExp b))))) (FtoR radix q') *)
(* Goal: Rle (FtoR radix p') (FtoR radix q') *)
elim H'4.
(* Goal: forall (_ : Fbounded b q') (_ : and (Rle (FtoR radix q') q) (forall (f : float) (_ : Fbounded b f) (_ : Rle (FtoR radix f) q), Rle (FtoR radix f) (FtoR radix q'))), Rle (FtoRradix (Fzero (Z.opp (Z.of_N (dExp b))))) (FtoR radix q') *)
(* Goal: Rle (FtoR radix p') (FtoR radix q') *)
intros H'0 H'5; elim H'5; intros H'6 H'7; apply H'7; clear H'5; auto.
(* Goal: Fbounded b (Fzero (Z.opp (Z.of_N (dExp b)))) *)
(* Goal: Rle (FtoR radix (Fzero (Z.opp (Z.of_N (dExp b))))) q *)
(* Goal: Rle (FtoR radix p') (FtoR radix q') *)
repeat split; simpl in |- *; auto with zarith.
(* Goal: Rle (FtoR radix (Fzero (Z.opp (Z.of_N (dExp b))))) q *)
(* Goal: Rle (FtoR radix p') (FtoR radix q') *)
rewrite Eq0; auto.
(* Goal: Rle (FtoR radix p') (FtoR radix q') *)
apply (MonotoneMax b radix) with (p := p) (q := q); auto.
Qed.
 
Theorem ToZeroRoundedModeP : RoundedModeP ToZeroP.
(* Goal: RoundedModeP ToInfinityP *)
repeat split.
(* Goal: TotalP ToZeroP *)
(* Goal: CompatibleP ToZeroP *)
(* Goal: MinOrMaxP ToZeroP *)
(* Goal: MonotoneP radix ToZeroP *)
try exact ToZeroTotal.
(* Goal: CompatibleP ToZeroP *)
(* Goal: MinOrMaxP ToZeroP *)
(* Goal: MonotoneP radix ToZeroP *)
try exact ToZeroCompatible.
(* Goal: MinOrMaxP ToZeroP *)
(* Goal: MonotoneP radix ToZeroP *)
try exact ToZeroMinOrMax.
(* Goal: MonotoneP radix ToZeroP *)
try exact ToZeroMonotone.
Qed.
 
Definition ToInfinityP (r : R) (p : float) :=
  (r <= 0)%R /\ isMin b radix r p \/ (0 <= r)%R /\ isMax b radix r p.
 
Theorem ToInfinityTotal : TotalP ToInfinityP.
(* Goal: TotalP ToInfinityP *)
red in |- *; intros r; case (Rle_or_lt r 0); intros H1.
(* Goal: @ex float (fun p : float => ToInfinityP r p) *)
(* Goal: @ex float (fun p : float => ToInfinityP r p) *)
case MinEx with (r := r) (3 := pGivesBound); auto with arith.
(* Goal: forall (x : float) (_ : isMin b radix r x), @ex float (fun p : float => ToInfinityP r p) *)
(* Goal: @ex float (fun p : float => ToInfinityP r p) *)
intros x H'; exists x; red in |- *; auto.
(* Goal: @ex float (fun p : float => ToInfinityP r p) *)
case MaxEx with (r := r) (3 := pGivesBound); auto with arith.
(* Goal: forall (x : float) (_ : isMax b radix r x), @ex float (fun p : float => ToInfinityP r p) *)
intros x H'; exists x; red in |- *; right; split; auto.
(* Goal: Rle (IZR Z0) r *)
apply Rlt_le; auto.
Qed.
 
Theorem ToInfinityCompatible : CompatibleP ToInfinityP.
(* Goal: UniqueP ToInfinityP *)
red in |- *.
(* Goal: forall (r1 r2 : R) (p q : float) (_ : ToInfinityP r1 p) (_ : @eq R r1 r2) (_ : @eq R (FtoRradix p) (FtoRradix q)) (_ : Fbounded b q), ToInfinityP r2 q *)
intros r1 r2 p q H'; case H'.
intros H'0 H'1 H'2; left; split;
 try apply MinCompatible with (p := p) (r1 := r1); 
 try rewrite <- H'1; case H'0; auto.
intros H'0 H'1 H'2; right; split;
 try apply MaxCompatible with (p := p) (r1 := r1); 
 try rewrite <- H'1; case H'0; auto.
Qed.
 
Theorem ToInfinityMinOrMax : MinOrMaxP ToInfinityP.
(* Goal: UniqueP ToInfinityP *)
red in |- *.
(* Goal: forall (r : R) (p : float) (_ : ToInfinityP r p), or (isMin b radix r p) (isMax b radix r p) *)
intros r p H'; case H'; clear H'; intros H'; case H'; auto.
Qed.
 
Theorem ToInfinityMonotone : MonotoneP radix ToInfinityP.
red in |- *; simpl in |- *.
cut (FtoR radix (Fzero (- dExp b)) = 0%R);
 [ intros Eq0 | unfold FtoR in |- *; simpl in |- * ]; 
 auto with real.
intros p q p' q' H' H'0; case H'0; clear H'0.
(* Goal: forall (_ : and (Rle (IZR Z0) p) (isMin b radix p p')) (_ : ToZeroP q q'), Rle (FtoR radix p') (FtoR radix q') *)
(* Goal: forall (_ : and (Rle p (IZR Z0)) (isMax b radix p p')) (_ : ToZeroP q q'), Rle (FtoR radix p') (FtoR radix q') *)
intros H'0; elim H'0; intros H'1 H'2; clear H'0; intros H'0.
(* Goal: Rle (FtoR radix p') (FtoR radix q') *)
(* Goal: forall (_ : and (Rle p (IZR Z0)) (isMax b radix p p')) (_ : ToZeroP q q'), Rle (FtoR radix p') (FtoR radix q') *)
case H'0; intros H'3; elim H'3; clear H'3; auto.
(* Goal: forall (_ : Rle q (IZR Z0)) (_ : isMax b radix q q'), Rle (FtoR radix p') (FtoR radix q') *)
(* Goal: forall (_ : and (Rle p (IZR Z0)) (isMax b radix p p')) (_ : ToZeroP q q'), Rle (FtoR radix p') (FtoR radix q') *)
intros H'3 H'4.
(* Goal: Rle (FtoR radix p') (FtoR radix q') *)
(* Goal: forall (_ : Rle q (IZR Z0)) (_ : isMax b radix q q'), Rle (FtoR radix p') (FtoR radix q') *)
(* Goal: forall (_ : and (Rle p (IZR Z0)) (isMax b radix p p')) (_ : ToZeroP q q'), Rle (FtoR radix p') (FtoR radix q') *)
apply (MonotoneMin b radix) with (p := p) (q := q); auto.
(* Goal: forall (_ : Rle q (IZR Z0)) (_ : isMax b radix q q'), Rle (FtoR radix p') (FtoR radix q') *)
(* Goal: forall (_ : and (Rle p (IZR Z0)) (isMax b radix p p')) (_ : ToZeroP q q'), Rle (FtoR radix p') (FtoR radix q') *)
intros H'3 H'4.
(* Goal: Rle (FtoR radix p') (FtoR radix q') *)
(* Goal: forall (_ : and (Rle p (IZR Z0)) (isMax b radix p p')) (_ : ToZeroP q q'), Rle (FtoR radix p') (FtoR radix q') *)
apply Rle_trans with p; [ apply isMin_inv1 with (1 := H'2); auto | idtac ].
apply Rle_trans with q; [ auto | apply isMax_inv1 with (1 := H'4) ]; auto.
(* Goal: Rle (IZR Z0) r *)
apply Rlt_le; auto.
(* Goal: forall (_ : and (Rle p (IZR Z0)) (isMax b radix p p')) (_ : ToZeroP q q'), Rle (FtoR radix p') (FtoR radix q') *)
intros H'0; elim H'0; intros H'1 H'2; clear H'0.
intros H'0; case H'0; clear H'0; intros H'0; case H'0; intros H'3 H'4;
 clear H'0.
(* Goal: Rle (FtoR radix p') (FtoR radix q') *)
2: apply (MonotoneMax b radix) with (p := p) (q := q); auto.
(* Goal: Rle (FtoR radix p') (FtoR radix q') *)
(* Goal: Rle (FtoR radix p') (FtoR radix q') *)
apply Rle_trans with (FtoRradix (Fzero (- dExp b))); auto.
(* Goal: Rle (FtoR radix p') (FtoRradix (Fzero (Z.opp (Z.of_N (dExp b))))) *)
(* Goal: Rle (FtoRradix (Fzero (Z.opp (Z.of_N (dExp b))))) (FtoR radix q') *)
(* Goal: Rle (FtoR radix p') (FtoR radix q') *)
elim H'2.
(* Goal: forall (_ : Fbounded b q') (_ : and (Rle (FtoR radix q') q) (forall (f : float) (_ : Fbounded b f) (_ : Rle (FtoR radix f) q), Rle (FtoR radix f) (FtoR radix q'))), Rle (FtoRradix (Fzero (Z.opp (Z.of_N (dExp b))))) (FtoR radix q') *)
(* Goal: Rle (FtoR radix p') (FtoR radix q') *)
intros H'0 H'5; elim H'5; intros H'6 H'7; apply H'7; clear H'5; auto.
(* Goal: Fbounded b (Fzero (Z.opp (Z.of_N (dExp b)))) *)
(* Goal: Rle (FtoR radix (Fzero (Z.opp (Z.of_N (dExp b))))) q *)
(* Goal: Rle (FtoR radix p') (FtoR radix q') *)
repeat split; simpl in |- *; auto with zarith.
apply Rle_trans with q; auto.
(* Goal: Rle (IZR Z0) r *)
apply Rlt_le; auto.
(* Goal: Rle (FtoR radix (Fzero (Z.opp (Z.of_N (dExp b))))) q *)
(* Goal: Rle (FtoR radix p') (FtoR radix q') *)
rewrite Eq0; auto.
(* Goal: Rle (FtoRradix (Fzero (Z.opp (Z.of_N (dExp b))))) (FtoR radix q') *)
(* Goal: Rle (FtoR radix p') (FtoR radix q') *)
elim H'4.
(* Goal: forall (_ : Fbounded b q') (_ : and (Rle (FtoR radix q') q) (forall (f : float) (_ : Fbounded b f) (_ : Rle (FtoR radix f) q), Rle (FtoR radix f) (FtoR radix q'))), Rle (FtoRradix (Fzero (Z.opp (Z.of_N (dExp b))))) (FtoR radix q') *)
(* Goal: Rle (FtoR radix p') (FtoR radix q') *)
intros H'0 H'5; elim H'5; intros H'6 H'7; apply H'7; clear H'5; auto.
(* Goal: Fbounded b (Fzero (Z.opp (Z.of_N (dExp b)))) *)
(* Goal: Rle (FtoR radix (Fzero (Z.opp (Z.of_N (dExp b))))) q *)
(* Goal: Rle (FtoR radix p') (FtoR radix q') *)
repeat split; simpl in |- *; auto with zarith.
apply Rle_trans with p; auto.
(* Goal: Rle (FtoR radix (Fzero (Z.opp (Z.of_N (dExp b))))) q *)
(* Goal: Rle (FtoR radix p') (FtoR radix q') *)
rewrite Eq0; auto.
(* Goal: Rle (IZR Z0) r *)
apply Rlt_le; auto.
Qed.
 
Theorem ToInfinityRoundedModeP : RoundedModeP ToInfinityP.
(* Goal: RoundedModeP ToInfinityP *)
repeat split.
(* Goal: TotalP ToInfinityP *)
(* Goal: CompatibleP ToInfinityP *)
(* Goal: MinOrMaxP ToInfinityP *)
(* Goal: MonotoneP radix ToInfinityP *)
try exact ToInfinityTotal.
(* Goal: CompatibleP ToInfinityP *)
(* Goal: MinOrMaxP ToInfinityP *)
(* Goal: MonotoneP radix ToInfinityP *)
try exact ToInfinityCompatible.
(* Goal: MinOrMaxP ToInfinityP *)
(* Goal: MonotoneP radix ToInfinityP *)
try exact ToInfinityMinOrMax.
(* Goal: MonotoneP radix ToInfinityP *)
try exact ToInfinityMonotone.
Qed.
 
Theorem MinUniqueP : UniqueP (isMin b radix).
(* Goal: UniqueP ToInfinityP *)
red in |- *.
(* Goal: forall (r : R) (p q : float) (_ : ToInfinityP r p) (_ : ToInfinityP r q), @eq R (FtoRradix p) (FtoRradix q) *)
intros r p q H' H'0.
(* Goal: @eq R (FtoRradix p) (FtoRradix q) *)
unfold FtoRradix in |- *; apply MinEq with (1 := H'); auto.
Qed.
 
Theorem MaxUniqueP : UniqueP (isMax b radix).
(* Goal: UniqueP ToInfinityP *)
red in |- *.
(* Goal: forall (r : R) (p q : float) (_ : ToInfinityP r p) (_ : ToInfinityP r q), @eq R (FtoRradix p) (FtoRradix q) *)
intros r p q H' H'0.
(* Goal: @eq R (FtoRradix p) (FtoRradix q) *)
unfold FtoRradix in |- *; apply MaxEq with (1 := H'); auto.
Qed.
 
Theorem ToZeroUniqueP : UniqueP ToZeroP.
(* Goal: UniqueP ToInfinityP *)
red in |- *.
(* Goal: forall (r : R) (p q : float) (_ : ToInfinityP r p) (_ : ToInfinityP r q), @eq R (FtoRradix p) (FtoRradix q) *)
intros r p q H' H'0.
inversion H'; inversion H'0; elim H0; elim H; clear H0 H;
 intros H'1 H'2 H'3 H'4.
(* Goal: @eq R (FtoRradix p) (FtoRradix q) *)
(* Goal: @eq R (FtoRradix p) (FtoRradix q) *)
(* Goal: @eq R (FtoRradix p) (FtoRradix q) *)
(* Goal: @eq R (FtoRradix p) (FtoRradix q) *)
apply (MinUniqueP r); auto.
cut (r = Fzero (- dExp b) :>R);
 [ intros Eq0
 | apply Rle_antisym; unfold FtoRradix, Fzero, FtoR in |- *; simpl in |- * ];
 try rewrite Rmult_0_l; auto with real.
(* Goal: @eq R (FtoRradix p) (FtoRradix q) *)
(* Goal: @eq R (FtoRradix p) (FtoRradix q) *)
apply trans_eq with (FtoRradix (Fzero (- dExp b))).
apply sym_eq; unfold FtoRradix in |- *;
 apply (RoundedProjector _ ToZeroRoundedModeP); auto with float.
(* Goal: ToInfinityP (FtoR radix (Fzero (Z.opp (Z.of_N (dExp b))))) q *)
(* Goal: @eq R (FtoRradix p) (FtoRradix q) *)
unfold FtoRradix in Eq0; rewrite <- Eq0; auto.
unfold FtoRradix in |- *; apply (RoundedProjector _ ToZeroRoundedModeP);
 auto with float.
(* Goal: ToInfinityP (FtoR radix (Fzero (Z.opp (Z.of_N (dExp b))))) q *)
(* Goal: @eq R (FtoRradix p) (FtoRradix q) *)
unfold FtoRradix in Eq0; rewrite <- Eq0; auto.
cut (r = Fzero (- dExp b) :>R);
 [ intros Eq0
 | apply Rle_antisym; unfold FtoRradix, Fzero, FtoR in |- *; simpl in |- * ];
 try rewrite Rmult_0_l; auto with real.
(* Goal: @eq R (FtoRradix p) (FtoRradix q) *)
(* Goal: @eq R (FtoRradix p) (FtoRradix q) *)
apply trans_eq with (FtoRradix (Fzero (- dExp b))).
apply sym_eq; unfold FtoRradix in |- *;
 apply (RoundedProjector _ ToZeroRoundedModeP); auto with float.
(* Goal: ToInfinityP (FtoR radix (Fzero (Z.opp (Z.of_N (dExp b))))) q *)
(* Goal: @eq R (FtoRradix p) (FtoRradix q) *)
unfold FtoRradix in Eq0; rewrite <- Eq0; auto.
unfold FtoRradix in |- *; apply (RoundedProjector _ ToZeroRoundedModeP);
 auto with float.
(* Goal: ToInfinityP (FtoR radix (Fzero (Z.opp (Z.of_N (dExp b))))) q *)
(* Goal: @eq R (FtoRradix p) (FtoRradix q) *)
unfold FtoRradix in Eq0; rewrite <- Eq0; auto.
(* Goal: @eq R (FtoRradix p) (FtoRradix q) *)
apply (MaxUniqueP r); auto.
Qed.
 
Theorem ToInfinityUniqueP : UniqueP ToInfinityP.
(* Goal: UniqueP ToInfinityP *)
red in |- *.
(* Goal: forall (r : R) (p q : float) (_ : ToInfinityP r p) (_ : ToInfinityP r q), @eq R (FtoRradix p) (FtoRradix q) *)
intros r p q H' H'0.
inversion H'; inversion H'0; elim H0; elim H; clear H0 H;
 intros H'1 H'2 H'3 H'4.
(* Goal: @eq R (FtoRradix p) (FtoRradix q) *)
(* Goal: @eq R (FtoRradix p) (FtoRradix q) *)
(* Goal: @eq R (FtoRradix p) (FtoRradix q) *)
(* Goal: @eq R (FtoRradix p) (FtoRradix q) *)
apply (MinUniqueP r); auto.
cut (r = Fzero (- dExp b) :>R);
 [ intros Eq0
 | apply Rle_antisym; unfold FtoRradix, Fzero, FtoR in |- *; simpl in |- * ];
 try rewrite Rmult_0_l; auto with real.
(* Goal: @eq R (FtoRradix p) (FtoRradix q) *)
(* Goal: @eq R (FtoRradix p) (FtoRradix q) *)
apply trans_eq with (FtoRradix (Fzero (- dExp b))).
apply sym_eq; unfold FtoRradix in |- *;
 apply (RoundedProjector _ ToInfinityRoundedModeP); 
 auto.
(* Goal: Fbounded b (Fzero (Z.opp (Z.of_N (dExp b)))) *)
(* Goal: ToInfinityP (FtoR radix (Fzero (Z.opp (Z.of_N (dExp b))))) q *)
(* Goal: @eq R (FtoRradix p) (FtoRradix q) *)
apply FboundedFzero; auto.
(* Goal: ToInfinityP (FtoR radix (Fzero (Z.opp (Z.of_N (dExp b))))) q *)
(* Goal: @eq R (FtoRradix p) (FtoRradix q) *)
unfold FtoRradix in Eq0; rewrite <- Eq0; auto.
unfold FtoRradix in |- *; apply (RoundedProjector _ ToInfinityRoundedModeP);
 auto.
(* Goal: Fbounded b (Fzero (Z.opp (Z.of_N (dExp b)))) *)
(* Goal: ToInfinityP (FtoR radix (Fzero (Z.opp (Z.of_N (dExp b))))) q *)
(* Goal: @eq R (FtoRradix p) (FtoRradix q) *)
apply FboundedFzero; auto.
(* Goal: ToInfinityP (FtoR radix (Fzero (Z.opp (Z.of_N (dExp b))))) q *)
(* Goal: @eq R (FtoRradix p) (FtoRradix q) *)
unfold FtoRradix in Eq0; rewrite <- Eq0; auto.
cut (r = Fzero (- dExp b) :>R);
 [ intros Eq0
 | apply Rle_antisym; unfold FtoRradix, Fzero, FtoR in |- *; simpl in |- * ];
 try rewrite Rmult_0_l; auto with float.
(* Goal: @eq R (FtoRradix p) (FtoRradix q) *)
(* Goal: @eq R (FtoRradix p) (FtoRradix q) *)
apply trans_eq with (FtoRradix (Fzero (- dExp b))).
apply sym_eq; unfold FtoRradix in |- *;
 apply (RoundedProjector _ ToInfinityRoundedModeP); 
 auto.
(* Goal: Fbounded b (Fzero (Z.opp (Z.of_N (dExp b)))) *)
(* Goal: ToInfinityP (FtoR radix (Fzero (Z.opp (Z.of_N (dExp b))))) q *)
(* Goal: @eq R (FtoRradix p) (FtoRradix q) *)
apply FboundedFzero; auto.
(* Goal: ToInfinityP (FtoR radix (Fzero (Z.opp (Z.of_N (dExp b))))) q *)
(* Goal: @eq R (FtoRradix p) (FtoRradix q) *)
unfold FtoRradix in Eq0; rewrite <- Eq0; auto.
unfold FtoRradix in |- *; apply (RoundedProjector _ ToInfinityRoundedModeP);
 auto.
(* Goal: Fbounded b (Fzero (Z.opp (Z.of_N (dExp b)))) *)
(* Goal: ToInfinityP (FtoR radix (Fzero (Z.opp (Z.of_N (dExp b))))) q *)
(* Goal: @eq R (FtoRradix p) (FtoRradix q) *)
apply FboundedFzero; auto.
(* Goal: ToInfinityP (FtoR radix (Fzero (Z.opp (Z.of_N (dExp b))))) q *)
(* Goal: @eq R (FtoRradix p) (FtoRradix q) *)
unfold FtoRradix in Eq0; rewrite <- Eq0; auto.
(* Goal: @eq R (FtoRradix p) (FtoRradix q) *)
apply (MaxUniqueP r); auto.
Qed.
 
 
Theorem MinOrMaxRep :
 forall P,
 MinOrMaxP P ->
 forall p q : float, P p q -> exists m : Z, q = Float m (Fexp p) :>R.
(* Goal: forall (P : forall (_ : R) (_ : float), Prop) (_ : MinOrMaxP P) (p q : float) (_ : P (FtoRradix p) q), @ex Z (fun m : Z => @eq R (FtoRradix q) (FtoRradix (Float m (Fexp p)))) *)
intros P H' p q H'0; case (H' p q); auto; intros H'1.
(* Goal: @ex Z (fun m : Z => @eq R (FtoRradix q) (FtoRradix (Float m (Fexp p)))) *)
(* Goal: @ex Z (fun m : Z => @eq R (FtoRradix q) (FtoRradix (Float m (Fexp p)))) *)
apply FminRep with (3 := pGivesBound); auto with arith.
(* Goal: @ex Z (fun m : Z => @eq R (FtoRradix q) (FtoRradix (Float m (Fexp p)))) *)
apply FmaxRep with (3 := pGivesBound); auto with arith.
Qed.
 
Theorem RoundedModeRep :
 forall P,
 RoundedModeP P ->
 forall p q : float, P p q -> exists m : Z, q = Float m (Fexp p) :>R.
(* Goal: forall (P : forall (_ : R) (_ : float), Prop) (_ : RoundedModeP P) (p q : float) (_ : P (FtoRradix p) q), @ex Z (fun m : Z => @eq R (FtoRradix q) (FtoRradix (Float m (Fexp p)))) *)
intros P H' p q H'0.
(* Goal: @ex Z (fun m : Z => @eq R (FtoRradix q) (FtoRradix (Float m (Fexp p)))) *)
apply MinOrMaxRep with (P := P); auto with inv.
Qed.
 
Definition SymmetricP (P : R -> float -> Prop) :=
  forall (r : R) (p : float), P r p -> P (- r)%R (Fopp p).
 
Theorem ToZeroSymmetric : SymmetricP ToZeroP.
red in |- *; intros r p H'; case H'; clear H'; intros H'; case H';
 intros H'1 H'2.
(* Goal: ToInfinityP (Ropp r) (Fopp p) *)
(* Goal: ToInfinityP (Ropp r) (Fopp p) *)
right; split; auto.
(* Goal: Rle (Ropp r) (IZR Z0) *)
(* Goal: isMin b radix (Ropp r) (Fopp p) *)
replace 0%R with (-0)%R; auto with real.
(* Goal: isMax b radix (Ropp r) (Fopp p) *)
(* Goal: ToInfinityP (Ropp r) (Fopp p) *)
apply MinOppMax; auto.
(* Goal: ToInfinityP (Ropp r) (Fopp p) *)
left; split; auto.
(* Goal: Rle (Ropp r) (IZR Z0) *)
(* Goal: isMin b radix (Ropp r) (Fopp p) *)
replace 0%R with (-0)%R; auto with real.
(* Goal: isMin b radix (Ropp r) (Fopp p) *)
apply MaxOppMin; auto.
Qed.
 
Theorem ToInfinitySymmetric : SymmetricP ToInfinityP.
red in |- *; intros r p H'; case H'; clear H'; intros H'; case H';
 intros H'1 H'2.
(* Goal: ToInfinityP (Ropp r) (Fopp p) *)
(* Goal: ToInfinityP (Ropp r) (Fopp p) *)
right; split; auto.
(* Goal: Rle (Ropp r) (IZR Z0) *)
(* Goal: isMin b radix (Ropp r) (Fopp p) *)
replace 0%R with (-0)%R; auto with real.
(* Goal: isMax b radix (Ropp r) (Fopp p) *)
(* Goal: ToInfinityP (Ropp r) (Fopp p) *)
apply MinOppMax; auto.
(* Goal: ToInfinityP (Ropp r) (Fopp p) *)
left; split; auto.
(* Goal: Rle (Ropp r) (IZR Z0) *)
(* Goal: isMin b radix (Ropp r) (Fopp p) *)
replace 0%R with (-0)%R; auto with real.
(* Goal: isMin b radix (Ropp r) (Fopp p) *)
apply MaxOppMin; auto.
Qed.
 
Theorem ScalableRoundedModeP :
 forall P (f s t : float),
 RoundedModeP P ->
 Fbounded b f -> P (radix * f)%R s -> P (s / radix)%R t -> f = t :>R.
intros P f s t HP Ff H1 H2.
cut (ProjectorP b radix P);
 [ unfold ProjectorP in |- *; intros HP2 | apply RoundedProjector; auto ].
cut (FtoR radix (Float (Fnum f) (Zsucc (Fexp f))) = (radix * FtoR radix f)%R);
 [ intros V | idtac].
2: unfold FtoR, Zsucc in |- *; simpl in |- *; ring_simplify.
2: rewrite powerRZ_add; [ simpl in |- *; ring | auto with zarith real ].
unfold FtoRradix in |- *; apply HP2; auto.
replace (FtoR radix f) with (FtoR radix s / radix)%R; auto.
replace (FtoR radix s) with (radix * FtoR radix f)%R;
 [ unfold Rdiv in |- * | rewrite <- V ].
rewrite Rmult_comm; rewrite <- Rmult_assoc; rewrite Rinv_l;
 auto with real zarith.
apply HP2; auto with float.
repeat (split; simpl in |- *; auto with zarith float).
rewrite V; auto.
Qed.
 
Theorem RoundLessThanIsMax :
 forall P,
 RoundedModeP P ->
 forall (p m : float) (x : R), P x p -> isMax b radix x m -> (p <= m)%R.
(* Goal: forall (P : forall (_ : R) (_ : float), Prop) (_ : RoundedModeP P) (p m : float) (x : R) (_ : P x p) (_ : isMax b radix x m), Rle (FtoRradix p) (FtoRradix m) *)
intros.
(* Goal: forall (P : forall (_ : R) (_ : float), Prop) (_ : RoundedModeP P) (p m : float) (x : R) (_ : P x p) (_ : isMax b radix x m), Rle (FtoRradix p) (FtoRradix m) *)
elim H; intros.
(* Goal: Rle (FtoRradix p) (FtoRradix m) *)
elim H3; intros H' H'0; clear H3.
(* Goal: Rle (FtoRradix p) (FtoRradix m) *)
elim H'0; intros; clear H'0.
(* Goal: Rle (FtoRradix p) (FtoRradix m) *)
case (H3 x p); auto.
(* Goal: forall _ : isMin b radix x p, Rle (FtoRradix p) (FtoRradix m) *)
(* Goal: forall _ : isMax b radix x p, Rle (FtoRradix p) (FtoRradix m) *)
intros; apply Rle_trans with x; auto.
(* Goal: Rle (FtoRradix p) x *)
(* Goal: Rle x (FtoRradix m) *)
(* Goal: forall _ : isMax b radix x p, Rle (FtoRradix p) (FtoRradix m) *)
elim H5; intros; elim H7; intros; auto with real.
(* Goal: Rle x (FtoRradix m) *)
(* Goal: forall _ : isMax b radix x p, Rle (FtoRradix p) (FtoRradix m) *)
elim H1; intros; elim H7; intros; auto with real.
(* Goal: forall _ : isMax b radix x p, Rle (FtoRradix p) (FtoRradix m) *)
intros; replace (FtoRradix p) with (FtoRradix m); auto with real.
(* Goal: @eq R (FtoRradix m) (FtoRradix p) *)
unfold FtoRradix in |- *; apply MaxEq with b x; auto.
Qed.
End FRound.
Hint Resolve RoundedProjector MinCompatible MinRoundedModeP MaxCompatible
  MaxRoundedModeP ToZeroTotal ToZeroCompatible ToZeroMinOrMax ToZeroMonotone
  ToZeroRoundedModeP ToInfinityTotal ToInfinityCompatible ToInfinityMinOrMax
  ToInfinityMonotone ToInfinityRoundedModeP MinUniqueP MaxUniqueP
  ToZeroUniqueP ToInfinityUniqueP FnOddNEven ToZeroSymmetric
  ToInfinitySymmetric: float.
Hint Resolve RoundedModeP_inv1 RoundedModeP_inv2 RoundedModeP_inv3
  RoundedModeP_inv4: inv.