proposition: Lemma abs_correct : forall x, toX (abs x) = Xabs (toX x) /\ (valid_ub (abs x) = true).
proof: Proof. intro x. unfold abs. unfold toX, toF. rewrite <-(SF2Prim_Prim2SF (PrimFloat.abs x)) at 2. generalize (Prim2SF_valid (PrimFloat.abs x)). rewrite abs_spec. rewrite valid_ub_correct. unfold classify. rewrite classify_spec. intro H. rewrite (Prim2SF_SF2Prim _ H). set (fx := Prim2SF x). case fx; [intros [ | ]..| |intros [ | ] mx ex]; simpl; try rewrite Rabs_R0; try (now split); 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]); now rewrite Generic_proof.FtoR_abs. Qed.
imports: Coq(ZArith Reals) Int63Compat Coq(Floats Psatz) Flocq(Zaux Raux BinarySingleNaN PrimFloat Sterbenz Mult_error) Missing.Stdlib Missing.Flocq Xreal Basic Sig