proposition: Lemma neg_correct : forall x, match classify x with | Freal => toX (neg x) = Xneg (toX x) | Sig.Fnan => classify (neg x) = Sig.Fnan | Fminfty => classify (neg x) = Fpinfty | Fpinfty => classify (neg x) = Fminfty end.
proof: Proof. intro x. unfold classify. rewrite !classify_spec. unfold toX, toF. unfold neg. rewrite opp_spec. case Prim2SF; [intros [ | ]..| |intros [ | ] mx ex]; try reflexivity; simpl; try (rewrite Ropp_0; reflexivity); unfold FtoR; 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]); case ex => [ |pex|pex]; unfold Rdiv; try rewrite Ropp_mult_distr_l; try rewrite <-opp_IZR; now try rewrite Zopp_mult_distr_l. Qed.
imports: Coq(ZArith Reals) Int63Compat Coq(Floats Psatz) Flocq(Zaux Raux BinarySingleNaN PrimFloat Sterbenz Mult_error) Missing.Stdlib Missing.Flocq Xreal Basic Sig