(** Some rewriting properties for translating between rationals and real numbers. These are used in the soundness proofs since we want to have the final theorem on the real valued evaluation. **) Require Import Coq.QArith.QArith Coq.QArith.Qminmax Coq.QArith.Qabs Coq.QArith.Qreals. Require Import Coq.Reals.Reals Coq.micromega.Psatz. Require Import Daisy.Infra.RationalSimps Daisy.Infra.Abbrevs. Require Import Daisy.IntervalArith Daisy.Infra.RealSimps. Lemma Q2R0_is_0: Q2R 0 = 0%R. Proof. unfold Q2R; simpl; lra. Qed. Lemma Q2R1: (Q2R 1 = 1)%R. Proof. unfold Q2R; simpl; lra. Qed. Lemma Rabs_eq_Qabs: forall x, Rabs (Q2R x) = Q2R (Qabs x). Proof. intro. apply Qabs_case; unfold Rabs; destruct Rcase_abs; intros; try auto. - apply Qle_Rle in H. exfalso. apply Rle_not_lt in H; apply H. assert (Q2R 0 = 0%R) by (unfold Q2R; simpl; lra). rewrite H0. apply r. - unfold Q2R. simpl. rewrite (Ropp_mult_distr_l). f_equal. rewrite opp_IZR; auto. - apply Qle_Rle in H. hnf in r; hnf in H. destruct r, H. + exfalso. apply Rlt_not_ge in H. apply H; hnf. left; rewrite Q2R0_is_0; auto. + rewrite H in H0. apply Rgt_not_le in H0. exfalso; apply H0. rewrite Q2R0_is_0. hnf; right; auto. + rewrite H0 in H. rewrite Q2R0_is_0 in H. apply Rlt_not_ge in H; exfalso; apply H. hnf; right; auto. + unfold Q2R in *; simpl in *. rewrite opp_IZR; lra. Qed. Lemma Q2R_max (a:Q) (b:Q) : Rmax (Q2R a) (Q2R b) = Q2R (Qmax a b). Proof. apply Q.max_case_strong. - intros c d eq_c_d Rmax_x. rewrite Rmax_x. unfold Q2R. rewrite <- RMicromega.Rinv_elim. setoid_rewrite Rmult_comm at 1. + rewrite <- Rmult_assoc. rewrite <- RMicromega.Rinv_elim. rewrite <- mult_IZR. rewrite eq_c_d. rewrite mult_IZR. rewrite Rmult_comm; auto. hnf; intros. pose proof (pos_INR_nat_of_P (Qden d)). simpl in H. rewrite H in H0. lra. + simpl; hnf; intros. pose proof (pos_INR_nat_of_P (Qden c)). rewrite H in H0; lra. - intros less. apply Qle_Rle in less. assert (Rmax (Q2R a) (Q2R b) = Q2R a) by (apply Rmax_left; auto). rewrite H; auto. - intros less. apply Qle_Rle in less. assert (Rmax (Q2R a) (Q2R b) = Q2R b) by (apply Rmax_right; auto). rewrite H; auto. Qed. Lemma Q2R_min (a:Q) (b:Q) : Rmin (Q2R a) (Q2R b) = Q2R (Qmin a b). Proof. apply Q.min_case_strong. - intros c d eq_c_d Rmin_x. rewrite Rmin_x. unfold Q2R. rewrite <- RMicromega.Rinv_elim. setoid_rewrite Rmult_comm at 1. + rewrite <- Rmult_assoc. rewrite <- RMicromega.Rinv_elim. rewrite <- mult_IZR. rewrite eq_c_d. rewrite mult_IZR. rewrite Rmult_comm; auto. hnf; intros. pose proof (pos_INR_nat_of_P (Qden d)). simpl in H. rewrite H in H0. lra. + simpl; hnf; intros. pose proof (pos_INR_nat_of_P (Qden c)). rewrite H in H0; lra. - intros less. apply Qle_Rle in less. assert (Rmin (Q2R a) (Q2R b) = Q2R a) by (apply Rmin_left; auto). rewrite H; auto. - intros less. apply Qle_Rle in less. assert (Rmin (Q2R a) (Q2R b) = Q2R b) by (apply Rmin_right; auto). rewrite H; auto. Qed. Lemma maxAbs_impl_RmaxAbs (ivlo:Q) (ivhi:Q): RmaxAbsFun (Q2R ivlo, Q2R ivhi) = Q2R (maxAbs (ivlo, ivhi)). Proof. unfold RmaxAbsFun, maxAbs. simpl; repeat rewrite Rabs_eq_Qabs. rewrite Q2R_max; auto. Qed. Definition Q2RP (iv:Q*Q) := let (lo,hi) := iv in (Q2R lo, Q2R hi). Corollary maxAbs_impl_RmaxAbs_iv iv: RmaxAbsFun (Q2RP iv) = Q2R (maxAbs iv). Proof. unfold Q2RP; destruct iv; apply maxAbs_impl_RmaxAbs. Qed. Lemma minAbs_impl_RminAbs (ivlo ivhi:Q) : RminAbsFun (Q2R ivlo, Q2R ivhi) = Q2R (minAbs (ivlo, ivhi)). Proof. unfold RminAbsFun, minAbs; simpl. repeat rewrite Rabs_eq_Qabs. rewrite Q2R_min; auto. Qed. Corollary minAbs_impl_RminAbs_iv iv: RminAbsFun (Q2RP iv) = Q2R (minAbs iv). Proof. unfold Q2RP; destruct iv; apply minAbs_impl_RminAbs. Qed. (* Lemma mEps_geq_zero: *) (* (0 <= Q2R RationalSimps.machineEpsilon)%R. *) (* Proof. *) (* rewrite <- Q2R0_is_0. *) (* apply Qle_Rle. *) (* unfold machineEpsilon. *) (* apply Qle_bool_iff. *) (* unfold Qle_bool; auto. *) (* Qed. *) Lemma Q_case_div_to_R_case_div a b: (b < 0 \/ 0 < a)%Q -> (Q2R b < 0 \/ 0 < Q2R a)%R. Proof. intros [le | gr]; [left | right]; rewrite <- Q2R0_is_0; apply Qlt_Rlt; auto. Qed.