RealRationalProps.v 4.36 KB
 Heiko Becker committed Sep 18, 2016 1 2 3 4 ``````(** 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. **) `````` Heiko Becker committed Aug 20, 2016 5 6 ``````Require Import Coq.QArith.QArith Coq.QArith.Qminmax Coq.QArith.Qabs Coq.QArith.Qreals. Require Import Coq.Reals.Reals Coq.micromega.Psatz. `````` Heiko Becker committed Nov 18, 2016 7 ``````Require Import Daisy.Infra.RationalSimps Daisy.Infra.Abbrevs. `````` Raphaël Monat committed Feb 27, 2017 8 ``````Require Import Daisy.IntervalArith Daisy.Infra.RealSimps. `````` Heiko Becker committed Aug 20, 2016 9 `````` `````` Heiko Becker committed Aug 21, 2016 10 11 12 13 14 ``````Lemma Q2R0_is_0: Q2R 0 = 0%R. Proof. unfold Q2R; simpl; lra. Qed. `````` Heiko Becker committed Aug 20, 2016 15 `````` `````` Heiko Becker committed Nov 04, 2016 16 17 18 19 ``````Lemma Q2R1: (Q2R 1 = 1)%R. Proof. unfold Q2R; simpl; lra. `````` Heiko Becker committed Nov 08, 2016 20 ``````Qed. `````` Heiko Becker committed Nov 04, 2016 21 `````` `````` Heiko Becker committed Aug 21, 2016 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 ``````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. `````` Heiko Becker committed Aug 23, 2016 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 ``````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. `````` Heiko Becker committed Sep 05, 2016 109 110 ``````Qed. `````` Heiko Becker committed Nov 08, 2016 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 ``````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. `````` Raphaël Monat committed Mar 01, 2017 142 143 144 145 146 147 148 149 150 ``````(* 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. *) `````` Heiko Becker committed Oct 31, 2016 151 `````` `````` Heiko Becker committed Nov 09, 2016 152 153 154 155 156 ``````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. `````` Heiko Becker committed Nov 08, 2016 157 ``Qed.``