proposition: Theorem mBFadic_correct1 : forall (r : R) (q : float), ~ is_Fzero q -> (Fopp (boundR r) < q)%R -> (q < boundR r)%R -> Fbounded b q -> In q (mBFloat r).
proof: Proof. intros r q. case (Zle_or_lt (Fexp (boundR r)) (Fexp q)); intros H'. intros H'0 H'1 H'2 H'3; case H'0. apply is_Fzero_rep2 with (radix := radix); auto. rewrite <- FshiftCorrect with (n := Z.abs_nat (Fexp q - Fexp (boundR r))) (x := q); auto with arith. apply is_Fzero_rep1 with (radix := radix). unfold is_Fzero in |- *. cut (forall p : Z, (- 1 < p)%Z -> (p < 1)%Z -> p = 0%Z); [ intros tmp; apply tmp | idtac ]. replace (- 1)%Z with (Fnum (Fopp (boundR r))). apply Rlt_Fexp_eq_Zlt with (radix := radix); auto with real zarith. rewrite FshiftCorrect; auto. unfold Fshift in |- *; simpl in |- *. rewrite (fun x y => inj_abs (x - y)); auto with zarith. apply Zle_minus_le_0; assumption. now simpl. replace 1%Z with (Fnum (boundR r)). apply Rlt_Fexp_eq_Zlt with (radix := radix); auto with zarith. rewrite FshiftCorrect; auto. unfold Fshift in |- *; simpl in |- *. rewrite inj_abs; auto with zarith. apply Zle_minus_le_0; assumption. now simpl. intros p0; case p0; simpl in |- *; auto with zarith. intros H'0 H'1 H'2 H'3; unfold mBFloat in |- *. replace q with ((fun p : Z * Z => Float (fst p) (snd p)) (Fnum q, Fexp q)). apply in_map with (f := fun p : Z * Z => Float (fst p) (snd p)); auto. apply mProd_correct; auto. apply mZlist_correct; auto. apply Zle_Zabs_inv1; apply Zle_Zpred, H'3. apply Zle_Zabs_inv2; apply Zle_Zpred, H'3. apply mZlist_correct; try apply H'3. auto with zarith. case q; simpl in |- *; auto with zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz