RealRationalProps.v 4.36 KB
Newer Older
Heiko Becker's avatar
Heiko Becker committed
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's avatar
Heiko Becker committed
5
6
Require Import Coq.QArith.QArith Coq.QArith.Qminmax Coq.QArith.Qabs Coq.QArith.Qreals.
Require Import Coq.Reals.Reals Coq.micromega.Psatz.
7
Require Import Daisy.Infra.RationalSimps Daisy.Infra.Abbrevs.
8
Require Import Daisy.IntervalArith Daisy.Infra.RealSimps.
Heiko Becker's avatar
Heiko Becker committed
9

10
11
12
13
14
Lemma Q2R0_is_0:
  Q2R 0 = 0%R.
Proof.
  unfold Q2R; simpl; lra.
Qed.
Heiko Becker's avatar
Heiko Becker committed
15

16
17
18
19
Lemma Q2R1:
  (Q2R 1 = 1)%R.
Proof.
  unfold Q2R; simpl; lra.
20
Qed.
21

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's avatar
Heiko Becker committed
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.
109
110
Qed.

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.

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. *)
151

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.
157
Qed.