proposition: Lemma min_correct : forall x y, match classify x, classify y with | Sig.Fnan, _ | _, Sig.Fnan => classify (min x y) = Sig.Fnan | Fminfty, _ | _, Fminfty => classify (min x y) = Fminfty | Fpinfty, _ => min x y = y | _, Fpinfty => min x y = x | Freal, Freal => toX (min x y) = Xmin (toX x) (toX y) end.
proof: Proof. intros x y. unfold min. rewrite compare_cmp, cmp_correct. unfold classify. rewrite !classify_spec. unfold toX, toF. set (fx := Prim2SF x). set (fy := Prim2SF y). rewrite <-(SF2Prim_Prim2SF x). rewrite <-(SF2Prim_Prim2SF y). generalize (Prim2SF_valid x). generalize (Prim2SF_valid y). fold fx; fold fy. case fx; [intros [ | ]..| |intros [ | ] mx ex]; (case fy; [intros [ | ]..| |intros [ | ] my ey]); intros vx vy; try (set (sf := SF2Prim _)); try (set (sf' := SF2Prim _)); simpl; try reflexivity; 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; rewrite Rmin_compare; case Rcompare; simpl; unfold sf; try unfold sf'; now repeat rewrite Prim2SF_SF2Prim. Qed.
imports: Coq(ZArith Reals) Int63Compat Coq(Floats Psatz) Flocq(Zaux Raux BinarySingleNaN PrimFloat Sterbenz Mult_error) Missing.Stdlib Missing.Flocq Xreal Basic Sig