forked from Eelis/hybrid
-
Notifications
You must be signed in to change notification settings - Fork 1
/
monotonic_flow.v
255 lines (226 loc) · 6.49 KB
/
monotonic_flow.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
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
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
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
Require Import util.
Require Import c_util.
Require Export flow.
Set Implicit Arguments.
Open Local Scope CR_scope.
Section single_inverses.
Variable f: Flow CRasCSetoid.
Variable fmono: mono f.
Lemma purify_mono: forall x, monotonic (f x).
Proof.
intros.
unfold monotonic.
destruct fmono; set (s x); [left | right]; assumption.
Qed.
Definition mle (x x': CR): Prop := if fmono then x <= x' else x' <= x.
Definition mlt (x x': CR): CProp := if fmono then x < x' else x' < x.
Lemma mle_refl x: mle x x.
Proof. unfold mle. destruct fmono; intros; apply CRle_refl. Qed.
Lemma mle_trans x y z: mle x y -> mle y z -> mle x z.
Proof.
unfold mle.
destruct fmono; intros; apply CRle_trans with y; assumption.
Qed.
Lemma mlt_le x x': mlt x x' -> mle x x'.
Proof.
unfold mlt, mle. destruct fmono; intros; apply CRlt_le; assumption.
Qed.
Lemma mono_le_opp v t t': t' < t -> mlt (f v t') (f v t).
Proof.
unfold mlt.
destruct fmono;intros; apply s; assumption.
Qed.
Lemma mono_opp v t t': t' <= t -> mle (f v t') (f v t).
Proof with auto.
unfold mle.
destruct fmono; intros.
apply mildly_increasing...
intros. rewrite H0. reflexivity.
apply mildly_decreasing...
intros. rewrite H0. reflexivity.
Qed.
Variables
(inv: CR -> CR -> Time)
(inv_correct: forall x x', f x (inv x x') == x').
Definition f_eq x t t': f x t == f x t' <-> t == t'.
Proof.
intros.
apply mono_eq.
intros.
rewrite H.
reflexivity.
apply purify_mono.
Qed.
Lemma inv_correct' x t: inv x (f x t) == t.
Proof.
intros.
destruct (f_eq x (inv x (f x t)) t).
clear H0. apply H.
rewrite inv_correct. reflexivity.
Qed.
Add Morphism inv with signature (@cs_eq _) ==> (@cs_eq _) ==> (@cs_eq _)
as inv_wd.
Proof with auto.
intros.
destruct (f_eq x (inv x x0) (inv y y0)).
apply H1.
rewrite inv_correct.
rewrite H.
rewrite inv_correct...
Qed.
Lemma inv_plus x y z: inv x z == inv x y + inv y z.
Proof with auto.
intros. destruct (f_eq x (inv x z) (inv x y + inv y z)).
clear H0. apply H.
rewrite flow_additive...
repeat rewrite inv_correct.
reflexivity.
Qed.
Lemma inv_refl x: inv x x == '0.
Proof with auto.
intros. destruct (f_eq x (inv x x) ('0)).
clear H0. apply H.
repeat rewrite inv_correct...
rewrite flow_zero...
Qed.
Lemma f_le x t t': mle (f x t) (f x t') -> t <= t'.
Proof with auto.
unfold mle. intros. destruct fmono.
apply strongly_increasing_inv_mild with (f x)...
apply strongly_decreasing_inv_mild with (f x)...
Qed.
Lemma inv_le_right a x x': inv a x <= inv a x' <-> mle x x'.
Proof with auto.
unfold mle.
split.
intros.
destruct fmono.
rewrite <- (inv_correct a x).
rewrite <- (inv_correct a x').
apply mildly_increasing...
intros. rewrite H0...
rewrite <- (inv_correct a x).
rewrite <- (inv_correct a x').
apply mildly_decreasing...
intros. rewrite H0...
set f_le. unfold mle in c. clearbody c.
intros.
apply c with a.
destruct fmono; repeat rewrite inv_correct...
Qed.
Lemma inv_very_correct t x: inv (f x t) x == -t.
Proof with auto with real.
intros.
assert (inv x x == '0).
apply inv_refl.
rewrite (inv_plus x (f x t) x) in H.
rewrite inv_correct' in H.
rewrite <- (Radd_0_l CR_ring_theory (-t)).
rewrite <- H.
rewrite (Radd_comm CR_ring_theory).
rewrite (Radd_assoc CR_ring_theory).
rewrite (Radd_comm CR_ring_theory (-t)).
rewrite (Ropp_def CR_ring_theory).
rewrite (Radd_0_l CR_ring_theory)...
Qed.
Lemma inv_inv x y: inv x y == - inv y x.
Proof with auto.
intros.
set (inv_very_correct (inv y x) y).
clearbody s. rewrite <- s.
rewrite inv_correct...
Qed.
Lemma inv_uniq_0 x x': inv x x' == - inv ('0) x + inv ('0) x'.
Proof with auto.
intros.
rewrite (inv_plus x ('0) x').
rewrite (inv_inv x ('0))...
Qed.
(* hm, this shows that inv is uniquely determined by the values it
takes with 0 as first argument. perhaps the reason we don't
just take inv as a unary function is that it is problematic
for flow functions with singularities at 0? *)
Lemma inv_le a x x': mle x x' -> inv a x <= inv a x'.
Proof with auto.
intros.
set f_le. clearbody c.
apply c with a.
unfold mle in *.
destruct fmono; do 2 rewrite inv_correct...
Qed.
Lemma inv_nonneg x x': '0 <= inv x x' <-> mle x x'.
Proof with auto.
unfold mle.
split; intros.
destruct fmono.
rewrite <- (flow_zero f x).
rewrite <- (inv_correct x x').
apply mildly_increasing...
intros. rewrite H0...
rewrite <- (flow_zero f x).
rewrite <- (inv_correct x x').
apply mildly_decreasing...
intros. rewrite H0...
rewrite <- (inv_refl x).
apply inv_le...
Qed.
Lemma inv_zero x x': inv x x' == '0 <-> x == x'.
Proof with auto.
split; intros.
rewrite <- (inv_correct x x').
rewrite H, flow_zero...
rewrite H.
apply inv_refl.
Qed.
Lemma f_le_left x x' t: x <= x' -> f x t <= f x' t.
Proof with auto with real.
intros.
set (inv_nonneg x x').
set (inv_nonneg x' x).
clearbody i i0.
unfold mle in *.
destruct fmono; clear fmono; destruct f.
simpl strongly_increasing in s.
clear f. rename flow_morphism into f.
rewrite <- (inv_correct x x').
rewrite <- flow_additive.
apply mildly_increasing...
intros. rewrite H0...
rewrite <- (Radd_0_l CR_ring_theory t) at 1.
apply t9.
apply i...
apply CRle_refl.
simpl strongly_decreasing in s.
clear f. rename flow_morphism into f.
rewrite <- (inv_correct x x').
simpl.
rewrite <- flow_additive.
apply mildly_decreasing...
intros. rewrite H0...
rewrite <- (Radd_0_l CR_ring_theory t) at 2.
apply t9.
rewrite inv_inv.
assert ('0 == -'0).
rewrite CRopp_Qopp.
apply inject_Q_wd.
reflexivity.
rewrite H0.
apply t8.
apply i0...
apply CRle_refl.
Qed.
Lemma inv_le_left a x x': mle x x' -> inv x' a <= inv x a.
Proof with auto.
intros.
rewrite (inv_inv x'). rewrite (inv_inv x).
apply t8. apply inv_le...
Qed.
Lemma mle_flow t x: '0 <= t -> mle x (f x t).
Proof with auto.
intros.
apply mle_trans with (f x ('0)).
unfold mle.
destruct fmono; rewrite flow_zero; apply CRle_refl.
apply mono_opp...
Qed.
End single_inverses.