proposition: Theorem clamp_correct : forall xi h x, contains (I.convert xi) (Xreal x) -> (0 <= x <= IZR h)%R -> let yi := clamp xi h in (IZR (fst yi) <= x <= IZR (snd yi))%R.
proof: Proof. intros xi h x Bx Hx. unfold clamp. assert (Nx := not_empty_contains _ _ Bx). split ; simpl. - assert (Vl := I.lower_correct _ Nx). change I.F.convert with F.convert in Vl. unfold F.convert in Vl. destruct F.toF as [| |[|] mx ex] ; try easy. destruct (I.convert xi) as [|[|xl] xu] ; try easy. apply Rle_trans with (2 := proj1 Bx). clear -Vl. injection Vl as <-. unfold clamp_lower. apply Rle_trans with (IZR (Z.shiftl (Zpos mx) ex)). { destruct (Z.leb_spec h (Z.shiftl (Zpos mx) ex)) as [H|H]. now apply IZR_le. apply Rle_refl. } unfold Basic.FtoR. destruct ex as [|ex|ex]. + apply Rle_refl. + rewrite Z.shiftl_mul_pow2 by easy. apply Rle_refl. + rewrite Z.shiftl_div_pow2 by easy. rewrite <- Raux.Zfloor_div. apply Raux.Zfloor_lb. apply Zaux.Zgt_not_eq. now apply Z.pow_pos_nonneg. - assert (Vu := I.upper_correct _ Nx). clear Nx. change I.F.convert with F.convert in Vu. unfold F.convert in Vu. destruct (I.convert xi) as [|xl [|xu]] ; try easy. now destruct F.toF. now destruct F.toF. destruct F.toF as [| |[|] mx ex] ; try easy. { apply Rle_trans with (1 := proj2 Bx). injection Vu as <-. apply Rle_refl. } { apply Rle_trans with (1 := proj2 Bx). injection Vu as <-. apply Rlt_le, Generic_proof.FtoR_Rneg. } unfold clamp_upper. destruct Z.leb. { easy. } apply Rle_trans with (1 := proj2 Bx). clear -Vu. injection Vu as <-. destruct ex as [|ex|ex]. + apply Rle_refl. + rewrite Z.shiftl_mul_pow2 by easy. apply Rle_refl. + rewrite Z.shiftl_div_pow2 by easy. rewrite Z.shiftl_mul_pow2 by easy. simpl Z.opp. simpl Basic.FtoR. fold (2 ^ Zpos ex)%Z. apply Generic_proof.Rdiv_ge_mult_pos. apply IZR_lt. now apply Z.pow_pos_nonneg. rewrite <- mult_IZR. apply IZR_le. apply Z.lt_pred_le. replace (Zpos mx + 1 * 2 ^ Zpos ex - 1)%Z with (Zpos mx - 1 + 1 * 2 ^ Zpos ex)%Z by ring. rewrite Zdiv.Z_div_plus_full. apply Z.mul_succ_div_gt. now apply Z.pow_pos_nonneg. apply Zaux.Zgt_not_eq. now apply Z.pow_pos_nonneg. Qed.
imports: Coq(Reals List) Sig Generic_proof Interval_helper Xreal Interval Tree Reify Prog