RealRationalProps.v 4.03 KB
Newer Older
Heiko Becker's avatar
Heiko Becker committed
1
2
Require Import Coq.QArith.QArith Coq.QArith.Qminmax Coq.QArith.Qabs Coq.QArith.Qreals.
Require Import Coq.Reals.Reals Coq.micromega.Psatz.
3
Require Import Daisy.Infra.RationalSimps Daisy.Infra.Abbrevs Daisy.Expressions.
Heiko Becker's avatar
Heiko Becker committed
4

5
6
7
8
9
10
11
Fixpoint toRExp (e:exp Q) :=
  match e with
  |Var v => Var R v
  |Param v => Param R v
  |Const n => Const (Q2R n)
  |Binop b e1 e2 => Binop b (toRExp e1) (toRExp e2)
  end.
Heiko Becker's avatar
Heiko Becker committed
12

13
14
Definition RmaxAbsFun (iv:intv) :=
  Rmax (Rabs (Q2R (fst iv))) (Rabs (Q2R (snd iv))).
Heiko Becker's avatar
Heiko Becker committed
15

16
17
18
19
20
Lemma Q2R0_is_0:
  Q2R 0 = 0%R.
Proof.
  unfold Q2R; simpl; lra.
Qed.
Heiko Becker's avatar
Heiko Becker committed
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
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
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 maxAbs_impl_RmaxAbs (iv:intv):
  RmaxAbsFun iv = Q2R (maxAbs iv).
Proof.
  unfold RmaxAbsFun, maxAbs.
  repeat rewrite Rabs_eq_Qabs.
  apply Q.max_case_strong.
  - intros x y x_eq_y 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 x_eq_y.
      rewrite mult_IZR.
      rewrite Rmult_comm; auto.
      hnf; intros.
      pose proof (pos_INR_nat_of_P (Qden y)).
      simpl in H.
      rewrite H in H0.
      lra.
    + simpl; hnf; intros.
      pose proof (pos_INR_nat_of_P (Qden x)).
      rewrite H in H0; lra.
  - intros snd_le_fst.
    apply Qle_Rle in snd_le_fst.
    apply Rmax_left in snd_le_fst.
    subst; auto.
  - intros fst_le_snd.
    apply Qle_Rle in fst_le_snd.
    apply Rmax_right in fst_le_snd.
    subst; auto.
Heiko Becker's avatar
Heiko Becker committed
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
109
110
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
142
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.
143
Qed.