proposition: Lemma max_correct : forall x y, match classify x, classify y with | Sig.Fnan, _ | _, Sig.Fnan => classify (max x y) = Sig.Fnan | Fpinfty, _ | _, Fpinfty => classify (max x y) = Fpinfty | Fminfty, _ => max x y = y | _, Fminfty => max x y = x | Freal, Freal => toX (max x y) = Xmax (toX x) (toX y) end.
proof: Proof. intros [|mx ex] [|my ey]; [simpl; easy..|]. unfold classify. rewrite 2!toX_Float. unfold max, Xmax. rewrite cmp_correct by apply toX_Float. simpl. unfold Xcmp, toR. generalize (classify_correct (Float mx ex)). generalize (classify_correct (Float my ey)). rewrite !real_correct. simpl. case_eq (toX (Float my ey)); [easy|]; intros ry Hry _. case_eq (toX (Float mx ex)); [easy|]; intros rx Hrx _. simpl. case Rcompare_spec; intros H; rewrite toX_Float; unfold valid_lb, valid_ub; simpl. { unfold toR; rewrite Hry; simpl. now apply f_equal; rewrite Rmax_right; [|apply Rlt_le]. } { unfold toR; rewrite Hry; simpl. now apply f_equal; rewrite Rmax_right; [|apply Req_le]. } unfold toR; rewrite Hrx; simpl. now apply f_equal; rewrite Rmax_left; [|apply Rlt_le]. Qed.
imports: Coq(ZArith Reals Lia Bool Psatz) Flocq(Zaux Raux Digits Bracket) mathcomp.ssreflect(ssrbool) Xreal Basic Generic Generic_proof Sig Specific_sig