proposition: Theorem Bcompare_correct : forall f1 f2, is_finite f1 = true -> is_finite f2 = true -> Bcompare f1 f2 = Some (Rcompare (B2R f1) (B2R f2)).
proof: Proof. assert (Hb: forall m1 e1 m2 e2, bounded m1 e1 = true -> bounded m2 e2 = true -> (e1 < e2)%Z -> (F2R (Float radix2 (Zpos m1) e1) < F2R (Float radix2 (Zpos m2) e2))%R). { intros m1 e1 m2 e2 B1 B2 He. apply (lt_cexp_pos radix2 fexp). now apply F2R_gt_0. rewrite <- (canonical_bounded false _ _ B1). rewrite <- (canonical_bounded false _ _ B2). easy. } assert (Hc: forall m1 e1 m2 e2, bounded m1 e1 = true -> bounded m2 e2 = true -> Rcompare (F2R (Float radix2 (Zpos m1) e1)) (F2R (Float radix2 (Zpos m2) e2)) = match Z.compare e1 e2 with Eq => Z.compare (Zpos m1) (Zpos m2) | Lt => Lt | Gt => Gt end). { intros m1 e1 m2 e2 B1 B2. case Zcompare_spec ; intros He. + apply Rcompare_Lt. now apply Hb. + now rewrite He, Rcompare_F2R. + apply Rcompare_Gt. now apply Hb. } intros [s1|[|]| |[|] m1 e1 B1] ; try easy ; intros [s2|[|]| |[|] m2 e2 B2] ; try easy ; intros _ _ ; apply (f_equal Some), eq_sym. - now apply Rcompare_Eq. - apply Rcompare_Gt. now apply F2R_lt_0. - apply Rcompare_Lt. now apply F2R_gt_0. - apply Rcompare_Lt. now apply F2R_lt_0. - unfold B2R. rewrite 2!F2R_cond_Zopp. rewrite Rcompare_opp. rewrite Hc by easy. rewrite (Z.compare_antisym e1), (Z.compare_antisym (Zpos m1)). now case Z.compare. - apply Rcompare_Lt. apply Rlt_trans with 0%R. now apply F2R_lt_0. now apply F2R_gt_0. - apply Rcompare_Gt. now apply F2R_gt_0. - apply Rcompare_Gt. apply Rlt_trans with 0%R. now apply F2R_lt_0. now apply F2R_gt_0. - now apply Hc. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative