proposition: Theorem MinOrMax1 : forall (z : R) (p : float), Fbounded b p -> Fcanonic radix b p -> (0 < p)%R -> (Rabs (z - p) < Fulp b radix precision (FPred b radix precision p))%R -> MinOrMax z p.
proof: Proof. intros z p Hp Hcan Hblop. case (Rcase_abs (z - p)); intros H1; [ rewrite Rabs_left | rewrite Rabs_right ]; auto; intros H. right; unfold isMax in |- *. split; auto; split. fold FtoRradix in |- *; apply Rplus_le_reg_l with (- p)%R. ring_simplify (- p + p)%R; rewrite Rplus_comm; auto with real. intros f Hf H2. replace (FtoR radix f) with (FtoR radix (Fnormalize radix b precision f)); [ idtac | apply FnormalizeCorrect; auto with zarith arith ]. replace p with (FSucc b radix precision (FPred b radix precision p)); [ idtac | apply FSucPred; auto with zarith arith ]. apply FSuccProp; auto with zarith arith. apply FPredCanonic; auto with arith zarith. apply FnormalizeCanonic; auto with arith zarith. apply Rlt_le_trans with z. 2: rewrite FnormalizeCorrect; auto with arith zarith. apply Rle_lt_trans with (p - Fulp b radix precision (FPred b radix precision p))%R. 2: apply Ropp_lt_cancel. 2: apply Rplus_lt_reg_r with (FtoRradix p). 2: ring_simplify. 2: apply Rle_lt_trans with (2 := H); right; ring. replace (FtoRradix p) with (FPred b radix precision p + Fulp b radix precision (FPred b radix precision p))%R; [ right; fold FtoRradix; ring | unfold FtoRradix in |- *; apply FpredUlpPos; auto with zarith arith ]. left; unfold isMin in |- *. split; auto; split. fold FtoRradix in |- *; apply Rplus_le_reg_l with (- p)%R. ring_simplify (- p + p)%R; rewrite Rplus_comm; auto with real. intros f Hf H2. replace (FtoR radix f) with (FtoR radix (Fnormalize radix b precision f)); [ idtac | apply FnormalizeCorrect; auto with zarith arith ]. replace p with (FPred b radix precision (FSucc b radix precision p)); [ idtac | apply FPredSuc; auto with zarith arith ]. apply FPredProp; auto with zarith arith. apply FnormalizeCanonic; auto with arith zarith. apply FSuccCanonic; auto with arith zarith. apply Rle_lt_trans with z. rewrite FnormalizeCorrect; auto with arith zarith. apply Rlt_le_trans with (p + Fulp b radix precision (FPred b radix precision p))%R. apply Rplus_lt_reg_r with (- FtoRradix p)%R. ring_simplify. apply Rle_lt_trans with (2 := H); right; ring. apply Rle_trans with (FtoRradix p + Fulp b radix precision p)%R; [ apply Rplus_le_compat_l | idtac ]. apply LeFulpPos; auto with arith zarith. apply FBoundedPred; auto with arith zarith. unfold FtoRradix in |- *; apply R0RltRlePred; auto with arith zarith. apply Rlt_le; unfold FtoRradix in |- *; apply FPredLt; auto with arith zarith. pattern p at -3 in |- *; replace p with (FPred b radix precision (FSucc b radix precision p)); [ idtac | apply FPredSuc; auto with zarith arith ]. unfold FtoRradix in |- *; rewrite FpredUlpPos with (x := FSucc b radix precision p); auto with zarith arith real. apply FSuccCanonic; auto with zarith arith. apply Rlt_trans with (FtoRradix p); auto with real. unfold FtoRradix in |- *; apply FSuccLt; auto with zarith real. Qed.
imports: Reals ZArith List PeanoNat Psatz