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 classify. destruct x as [|mx ex]. easy. destruct y as [|my ey]. easy. simpl. unfold toR, toX, toF. generalize (mantissa_sign_correct mx) (mantissa_sign_correct my). destruct (mantissa_sign mx) as [|[|] mx'] ; destruct (mantissa_sign my) as [|[|] my'] ; intros Hx Hy. - now simpl; rewrite Rcompare_Eq. - simpl; rewrite Rcompare_Gt. easy. apply FtoR_Rneg. - simpl; rewrite Rcompare_Lt. easy. apply FtoR_Rpos. - simpl; rewrite Rcompare_Lt. easy. apply FtoR_Rneg. - rewrite cmp_aux2_correct by easy. rewrite Fcmp_aux2_correct. simpl. change true with (negb false). rewrite <- 2!FtoR_neg. now rewrite Rcompare_opp. - simpl; rewrite Rcompare_Lt. easy. apply Rlt_trans with 0%R. apply FtoR_Rneg. apply FtoR_Rpos. - simpl; rewrite Rcompare_Gt. easy. apply FtoR_Rpos. - simpl; rewrite Rcompare_Gt. easy. apply Rlt_trans with 0%R. apply FtoR_Rneg. apply FtoR_Rpos. - rewrite cmp_aux2_correct by easy. now rewrite Fcmp_aux2_correct. Qed.
imports: Coq(ZArith Reals Lia Bool Psatz) Flocq(Zaux Raux Digits Bracket) mathcomp.ssreflect(ssrbool) Xreal Basic Generic Generic_proof Sig Specific_sig