proposition: Lemma cmp_correct : forall x y, cmp x y = match classify x, classify y with | Sig.Fnan, _ | _, Sig.Fnan => Xund | Fminfty, Fminfty => Xeq | Fminfty, _ => Xlt | _, Fminfty => Xgt | Fpinfty, Fpinfty => Xeq | _, Fpinfty => Xlt | Fpinfty, _ => Xgt | Freal, Freal => Xcmp (toX x) (toX y) end.
proof: Proof. intros x y. unfold cmp, classify, toX, toF. rewrite compare_equiv. rewrite !classify_spec, <-!B2SF_Prim2B. set (fx := Prim2B x). set (fy := Prim2B y). generalize (Bcompare_correct _ _ fx fy). case fx; [intros [ | ]..| |intros [ | ] mx ex Hx]; (case fy; [intros [ | ]..| |intros [ | ] my ey Hy]); intro Hcmp; try rewrite (Hcmp eq_refl eq_refl); simpl; unfold Defs.F2R; simpl; try rewrite !FtoR_split; simpl; unfold Defs.F2R; simpl; repeat (replace match (if match _ with 53%positive => true | _ => _ end then _ else _) with PInf | NInf | NaN => _ | _ => Freal end with Freal; [ |now case match _ with 53%positive => true | _ => _ end]); try reflexivity; now case Rcompare. Qed.
imports: Coq(ZArith Reals) Int63Compat Coq(Floats Psatz) Flocq(Zaux Raux BinarySingleNaN PrimFloat Sterbenz Mult_error) Missing.Stdlib Missing.Flocq Xreal Basic Sig