proposition: Theorem FminRep : forall p q : float, isMin p q -> exists m : Z, q = Float m (Fexp p) :>R.
proof: Proof. intros p q H'. replace (FtoRradix q) with (FtoRradix (Fnormalize radix b precision q)). 2: unfold FtoRradix in |- *; apply FnormalizeCorrect; auto. case (Zle_or_lt (Fexp (Fnormalize radix b precision q)) (Fexp p)); intros H'1. exists (Fnum p). unfold FtoRradix in |- *; apply FSuccZleEq with (3 := pGivesBound); auto. replace (Float (Fnum p) (Fexp p)) with p; [ idtac | case p ]; auto. replace (FtoR radix (Fnormalize radix b precision q)) with (FtoR radix q); [ idtac | rewrite FnormalizeCorrect ]; auto. apply isMin_inv1 with (1 := H'); auto. replace (FSucc b radix precision (Fnormalize radix b precision q)) with (FNSucc b radix precision q); [ idtac | case p ]; auto. replace (Float (Fnum p) (Fexp p)) with p; [ idtac | case p ]; auto. case (Req_dec p q); intros Eq0. unfold FtoRradix in Eq0; rewrite Eq0. apply FNSuccLt; auto. case (MinMax q p); auto. intros H'2 H'3; elim H'3; intros H'4 H'5; clear H'3. case H'4; auto. intros H'0; absurd (p <= q)%R; rewrite H'0; auto. apply Rlt_not_le; auto. unfold FtoRradix in |- *; apply FNSuccLt; auto. inversion H'. elim H0; intros H'3 H'6; apply H'6; clear H0; auto. rewrite <- H'0; auto with real. exists (Fnum (Fshift radix (Z.abs_nat (Fexp (Fnormalize radix b precision q) - Fexp p)) (Fnormalize radix b precision q))). pattern (Fexp p) at 2 in |- *; replace (Fexp p) with (Fexp (Fshift radix (Z.abs_nat (Fexp (Fnormalize radix b precision q) - Fexp p)) (Fnormalize radix b precision q))). unfold FtoRradix in |- *; rewrite <- FshiftCorrect with (n := Z.abs_nat (Fexp (Fnormalize radix b precision q) - Fexp p)) (x := Fnormalize radix b precision q). case (Fshift radix (Z.abs_nat (Fexp (Fnormalize radix b precision q) - Fexp p)) (Fnormalize radix b precision q)); auto. auto with arith. simpl in |- *; rewrite inj_abs; auto with zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz