blob: 64d1f955559244f89ad0f61acdbcd59dac2bd5ca (
plain)
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
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
|
(*s The decision procedure is instantiated for Z *)
Require cgraph.
Require ZArith.
Require Addr.
Require Addec.
Inductive ZCGForm : Set :=
ZCGle : ad -> ad -> ZCGForm (* x<=y *)
| ZCGge : ad -> ad -> ZCGForm (* x>=y *)
| ZCGlt : ad -> ad -> ZCGForm (* x<y *)
| ZCGgt : ad -> ad -> ZCGForm (* x>y *)
| ZCGlep : ad -> ad -> Z -> ZCGForm (* x<=y+k *)
| ZCGgep : ad -> ad -> Z -> ZCGForm (* x>=y+k *)
| ZCGltp : ad -> ad -> Z -> ZCGForm (* x<y+k *)
| ZCGgtp : ad -> ad -> Z -> ZCGForm (* x>y+k *)
| ZCGlem : ad -> ad -> Z -> ZCGForm (* x+k<=y *)
| ZCGgem : ad -> ad -> Z -> ZCGForm (* x+k>=y *)
| ZCGltm : ad -> ad -> Z -> ZCGForm (* x+k<y *)
| ZCGgtm : ad -> ad -> Z -> ZCGForm (* x+k>y *)
| ZCGlepm : ad -> ad -> Z -> Z -> ZCGForm (* x+k<=y+k' *)
| ZCGgepm : ad -> ad -> Z -> Z -> ZCGForm (* x+k>=y+k' *)
| ZCGltpm : ad -> ad -> Z -> Z -> ZCGForm (* x+k<y+k' *)
| ZCGgtpm : ad -> ad -> Z -> Z -> ZCGForm (* x+k>y+k' *)
| ZCGeq : ad -> ad -> ZCGForm (* x=y *)
| ZCGeqp : ad -> ad -> Z -> ZCGForm (* x=y+k *)
| ZCGeqm : ad -> ad -> Z -> ZCGForm (* x+k=y *)
| ZCGeqpm : ad -> ad -> Z -> Z -> ZCGForm (* x+k=y+k' *)
| ZCGzylem : ad -> Z -> ZCGForm (* k<=y *)
| ZCGzygem : ad -> Z -> ZCGForm (* k>=y *)
| ZCGzyltm : ad -> Z -> ZCGForm (* k<y *)
| ZCGzygtm : ad -> Z -> ZCGForm (* k>y *)
| ZCGzylepm : ad -> Z -> Z -> ZCGForm (* k<=y+k' *)
| ZCGzygepm : ad -> Z -> Z -> ZCGForm (* k>=y+k' *)
| ZCGzyltpm : ad -> Z -> Z -> ZCGForm (* k<y+k' *)
| ZCGzygtpm : ad -> Z -> Z -> ZCGForm (* k>y+k' *)
| ZCGzyeqm : ad -> Z -> ZCGForm (* k=y *)
| ZCGzyeqpm : ad -> Z -> Z -> ZCGForm (* k=y+k' *)
| ZCGxzlep : ad -> Z -> ZCGForm (* x<=k *)
| ZCGxzgep : ad -> Z -> ZCGForm (* x>=k *)
| ZCGxzltp : ad -> Z -> ZCGForm (* x<k *)
| ZCGxzgtp : ad -> Z -> ZCGForm (* x>k *)
| ZCGxzlepm : ad -> Z -> Z -> ZCGForm (* x+k<=k' *)
| ZCGxzgepm : ad -> Z -> Z -> ZCGForm (* x+k>=k' *)
| ZCGxzltpm : ad -> Z -> Z -> ZCGForm (* x+k<k' *)
| ZCGxzgtpm : ad -> Z -> Z -> ZCGForm (* x+k>k' *)
| ZCGxzeqp : ad -> Z -> ZCGForm (* x=k *)
| ZCGxzeqpm : ad -> Z -> Z -> ZCGForm (* x+k=k' *)
| ZCGzzlep : Z -> Z -> ZCGForm (* k<=k' *)
| ZCGzzltp : Z -> Z -> ZCGForm (* k<k' *)
| ZCGzzgep : Z -> Z -> ZCGForm (* k>=k' *)
| ZCGzzgtp : Z -> Z -> ZCGForm (* k>k' *)
| ZCGzzeq : Z -> Z -> ZCGForm (* k=k' *)
| ZCGand : ZCGForm -> ZCGForm -> ZCGForm
| ZCGor : ZCGForm -> ZCGForm -> ZCGForm
| ZCGimp : ZCGForm -> ZCGForm -> ZCGForm
| ZCGnot : ZCGForm -> ZCGForm
| ZCGiff : ZCGForm -> ZCGForm -> ZCGForm.
Definition ZCG_eval := (CGeval Z Zplus Zle_bool).
(*s Translation of formula on Z into a constraint graph formula.
we reserve [ad_z] as the "zero" variable,
i.e., the one that is anchored at the value `0`. *)
Fixpoint ZCGtranslate [f:ZCGForm] : (CGForm Z) :=
Cases f of
(ZCGle x y) => (CGleq Z x y `0`)
| (ZCGge x y) => (CGleq Z y x `0`)
| (ZCGlt x y) => (CGleq Z x y `-1`)
| (ZCGgt x y) => (CGleq Z y x `-1`)
| (ZCGlep x y k) => (CGleq Z x y k)
| (ZCGgep x y k) => (CGleq Z y x (Zopp k))
| (ZCGltp x y k) => (CGleq Z x y `k-1`)
| (ZCGgtp x y k) => (CGleq Z y x (Zopp `k+1`))
| (ZCGlem x y k) => (CGleq Z x y (Zopp k))
| (ZCGgem x y k) => (CGleq Z y x k)
| (ZCGltm x y k) => (CGleq Z x y (Zopp `k+1`))
| (ZCGgtm x y k) => (CGleq Z y x `k-1`)
| (ZCGlepm x y k k') => (CGleq Z x y `k'-k`)
| (ZCGgepm x y k k') => (CGleq Z y x `k-k'`)
| (ZCGltpm x y k k') => (CGleq Z x y `k'-k-1`)
| (ZCGgtpm x y k k') => (CGleq Z y x `k-k'-1`)
| (ZCGeq x y) => (CGeq Z x y `0`)
| (ZCGeqp x y k) => (CGeq Z x y k)
| (ZCGeqm x y k) => (CGeq Z y x k)
| (ZCGeqpm x y k k') => (CGeq Z x y `k'-k`)
| (ZCGzylem y k) => (CGleq Z ad_z y (Zopp k))
| (ZCGzygem y k) => (CGleq Z y ad_z k)
| (ZCGzyltm y k) => (CGleq Z ad_z y (Zopp `k+1`))
| (ZCGzygtm y k) => (CGleq Z y ad_z `k-1`)
| (ZCGzylepm y k k') => (CGleq Z ad_z y `k'-k`)
| (ZCGzygepm y k k') => (CGleq Z y ad_z `k-k'`)
| (ZCGzyltpm y k k') => (CGleq Z ad_z y `k'-k-1`)
| (ZCGzygtpm y k k') => (CGleq Z y ad_z `k-k'-1`)
| (ZCGzyeqm y k) => (CGeq Z y ad_z k)
| (ZCGzyeqpm y k k') => (CGeq Z y ad_z `k-k'`)
| (ZCGxzlep x k) => (CGleq Z x ad_z k)
| (ZCGxzgep x k) => (CGleq Z ad_z x (Zopp k))
| (ZCGxzltp x k) => (CGleq Z x ad_z `k-1`)
| (ZCGxzgtp x k) => (CGleq Z ad_z x (Zopp `k+1`))
| (ZCGxzlepm x k k') => (CGleq Z x ad_z `k'-k`)
| (ZCGxzgepm x k k') => (CGleq Z ad_z x `k-k'`)
| (ZCGxzltpm x k k') => (CGleq Z x ad_z `k'-k-1`)
| (ZCGxzgtpm x k k') => (CGleq Z ad_z x `k-k'-1`)
| (ZCGxzeqp x k) => (CGeq Z x ad_z k)
| (ZCGxzeqpm x k k') => (CGeq Z x ad_z `k'-k`)
| (ZCGzzlep k k') => (CGleq Z ad_z ad_z `k'-k`)
| (ZCGzzltp k k') => (CGleq Z ad_z ad_z `k'-k-1`)
| (ZCGzzgep k k') => (CGleq Z ad_z ad_z `k-k'`)
| (ZCGzzgtp k k') => (CGleq Z ad_z ad_z `k-k'-1`)
| (ZCGzzeq k k') => (CGeq Z ad_z ad_z `k-k'`)
| (ZCGand f0 f1) => (CGand Z (ZCGtranslate f0) (ZCGtranslate f1))
| (ZCGor f0 f1) => (CGor Z (ZCGtranslate f0) (ZCGtranslate f1))
| (ZCGimp f0 f1) => (CGimp Z (ZCGtranslate f0) (ZCGtranslate f1))
| (ZCGnot f0) => (CGnot Z (ZCGtranslate f0))
| (ZCGiff f0 f1) => (CGand Z (CGimp Z (ZCGtranslate f0) (ZCGtranslate f1))
(CGimp Z (ZCGtranslate f1) (ZCGtranslate f0)))
end.
Section ZCGevalDef.
Variable rho : ad -> Z.
Fixpoint ZCGeval [f:ZCGForm] : Prop :=
Cases f of
(ZCGle x y) => `(rho x)<=(rho y)`
| (ZCGge x y) => `(rho x)>=(rho y)`
| (ZCGlt x y) => `(rho x)<(rho y)`
| (ZCGgt x y) => `(rho x)>(rho y)`
| (ZCGlep x y k) => `(rho x)<=(rho y)+k`
| (ZCGgep x y k) => `(rho x)>=(rho y)+k`
| (ZCGltp x y k) => `(rho x)<(rho y)+k`
| (ZCGgtp x y k) => `(rho x)>(rho y)+k`
| (ZCGlem x y k) => `(rho x)+k<=(rho y)`
| (ZCGgem x y k) => `(rho x)+k>=(rho y)`
| (ZCGltm x y k) => `(rho x)+k<(rho y)`
| (ZCGgtm x y k) => `(rho x)+k>(rho y)`
| (ZCGlepm x y k k') => `(rho x)+k<=(rho y)+k'`
| (ZCGgepm x y k k') => `(rho x)+k>=(rho y)+k'`
| (ZCGltpm x y k k') => `(rho x)+k<(rho y)+k'`
| (ZCGgtpm x y k k') => `(rho x)+k>(rho y)+k'`
| (ZCGeq x y) => `(rho x)=(rho y)`
| (ZCGeqp x y k) => `(rho x)=(rho y)+k`
| (ZCGeqm x y k) => `(rho x)+k=(rho y)`
| (ZCGeqpm x y k k') => `(rho x)+k=(rho y)+k'`
| (ZCGzylem y k) => `k<=(rho y)`
| (ZCGzygem y k) => `k>=(rho y)`
| (ZCGzyltm y k) => `k<(rho y)`
| (ZCGzygtm y k) => `k>(rho y)`
| (ZCGzylepm y k k') => `k<=(rho y)+k'`
| (ZCGzygepm y k k') => `k>=(rho y)+k'`
| (ZCGzyltpm y k k') => `k<(rho y)+k'`
| (ZCGzygtpm y k k') => `k>(rho y)+k'`
| (ZCGzyeqm y k) => `k=(rho y)`
| (ZCGzyeqpm y k k') => `k=(rho y)+k'`
| (ZCGxzlep x k) => `(rho x)<=k`
| (ZCGxzgep x k) => `(rho x)>=k`
| (ZCGxzltp x k) => `(rho x)<k`
| (ZCGxzgtp x k) => `(rho x)>k`
| (ZCGxzlepm x k k') => `(rho x)+k<=k'`
| (ZCGxzgepm x k k') => `(rho x)+k>=k'`
| (ZCGxzltpm x k k') => `(rho x)+k<k'`
| (ZCGxzgtpm x k k') => `(rho x)+k>k'`
| (ZCGxzeqp x k) => `(rho x)=k`
| (ZCGxzeqpm x k k') => `(rho x)+k=k'`
| (ZCGzzlep k k') => `k<=k'`
| (ZCGzzltp k k') => `k<k'`
| (ZCGzzgep k k') => `k>=k'`
| (ZCGzzgtp k k') => `k>k'`
| (ZCGzzeq k k') => `k=k'`
| (ZCGand f0 f1) => (ZCGeval f0) /\ (ZCGeval f1)
| (ZCGor f0 f1) => (ZCGeval f0) \/ (ZCGeval f1)
| (ZCGimp f0 f1) => (ZCGeval f0) -> (ZCGeval f1)
| (ZCGnot f0) => ~(ZCGeval f0)
| (ZCGiff f0 f1) => (ZCGeval f0) <-> (ZCGeval f1)
end.
Variable Zrho_zero : (rho ad_z)=ZERO.
Lemma ZCGeval_correct
: (f:ZCGForm) (ZCGeval f) <-> (ZCG_eval rho (ZCGtranslate f)).
Proof.
Induction f; Simpl. Intros. Rewrite Zero_right. Apply Zle_is_le_bool.
Intros. Rewrite Zero_right. Apply Zge_is_le_bool.
Intros. Exact (Zlt_is_le_bool (rho a) (rho a0)).
Intros. Exact (Zgt_is_le_bool (rho a) (rho a0)).
Intros. Apply Zle_is_le_bool.
Intros. Apply iff_trans with b:=`(rho a0)+z <= (rho a)`. Apply Zge_iff_le.
Apply iff_trans with b:=`(rho a0) <= (rho a)-z`. Apply Zle_plus_swap.
Unfold Zminus. Apply Zle_is_le_bool.
Intros. Apply iff_trans with b:=(Zle_bool (rho a) `(rho a0)+z-1`)=true. Apply Zlt_is_le_bool.
Unfold 1 Zminus. Rewrite Zplus_assoc_r. Split; Intro; Assumption.
Intros. Apply iff_trans with b:=`(rho a0)+z < (rho a)`. Apply Zgt_iff_lt.
Apply iff_trans with `(rho a0) < (rho a)-z`. Apply Zlt_plus_swap.
Rewrite Zopp_Zplus. Rewrite Zplus_assoc_l. Exact (Zlt_is_le_bool (rho a0) `(rho a)-z`).
Intros. Apply iff_trans with b:=`(rho a) <= (rho a0)-z`. Apply Zle_plus_swap.
Unfold Zminus. Apply Zle_is_le_bool.
Intros. Apply Zge_is_le_bool.
Intros. Apply iff_trans with b:=`(rho a) < (rho a0)-z`. Apply Zlt_plus_swap.
Rewrite Zopp_Zplus. Rewrite Zplus_assoc_l. Exact (Zlt_is_le_bool (rho a) `(rho a0)-z`).
Intros. Unfold Zminus. Rewrite Zplus_assoc_l. Exact (Zgt_is_le_bool `(rho a)+z` (rho a0)).
Intros. Apply iff_trans with b:=`(rho a) <= (rho a0)+z0-z`. Apply Zle_plus_swap.
Unfold 1 Zminus. Rewrite Zplus_assoc_r. Unfold Zminus. Apply Zle_is_le_bool.
Intros. Apply iff_trans with b:=`(rho a0)+z0 <= (rho a)+z`. Apply Zge_iff_le.
Apply iff_trans with b:=`(rho a0) <= (rho a)+z-z0`. Apply Zle_plus_swap.
Unfold 1 Zminus. Rewrite Zplus_assoc_r. Unfold Zminus. Apply Zle_is_le_bool.
Intros. Apply iff_trans with b:=`(rho a) < (rho a0)+z0-z`. Apply Zlt_plus_swap.
Unfold 2 Zminus. Rewrite Zplus_assoc_l. Unfold 1 Zminus. Rewrite Zplus_assoc_r.
Exact (Zlt_is_le_bool (rho a) `(rho a0)+(z0+ -z)`).
Intros. Apply iff_trans with b:=`(rho a0)+z0 < (rho a)+z`. Apply Zgt_iff_lt.
Apply iff_trans with b:=`(rho a0) < (rho a)+z-z0`. Apply Zlt_plus_swap.
Unfold 2 Zminus. Rewrite Zplus_assoc_l. Unfold 1 Zminus. Rewrite Zplus_assoc_r.
Exact (Zlt_is_le_bool (rho a0) `(rho a)+(z+ -z0)`).
Intros. Rewrite Zero_right. Split; Intro; Assumption.
Split; Intro; Assumption.
Split; Intro; Apply sym_eq; Assumption.
Intros. Unfold Zminus. Rewrite Zplus_assoc_l. Exact (Zeq_plus_swap (rho a) `(rho a0)+z0` z).
Rewrite Zrho_zero. Intros. Apply iff_trans with b:=`0+z <= (rho a)`. Rewrite Zero_left.
Split; Intro; Assumption.
Apply iff_trans with b:=`0 <= (rho a)-z`. Apply Zle_plus_swap.
Unfold Zminus. Apply Zle_is_le_bool.
Rewrite Zrho_zero. Intros. Rewrite Zero_left. Apply Zge_is_le_bool.
Rewrite Zrho_zero. Intros. Apply iff_trans with b:=`0+z < (rho a)`. Rewrite Zero_left.
Split; Intro; Assumption.
Apply iff_trans with b:=`0 < (rho a)-z`. Apply Zlt_plus_swap.
Rewrite Zopp_Zplus. Rewrite Zplus_assoc_l. Exact (Zlt_is_le_bool `0` `(rho a)-z`).
Rewrite Zrho_zero. Intros. Rewrite Zero_left. Apply Zgt_is_le_bool.
Rewrite Zrho_zero. Intros. Apply iff_trans with b:=`0+z <= (rho a)+z0`. Rewrite Zero_left.
Split; Intro; Assumption.
Apply iff_trans with b:=`0 <= (rho a)+z0-z`. Apply Zle_plus_swap.
Unfold 2 Zminus. Rewrite Zplus_assoc_l. Exact (Zle_is_le_bool `0` `(rho a)+z0-z`).
Rewrite Zrho_zero. Intros. Rewrite Zero_left. Apply iff_trans with b:=`(rho a)+z0 <= z`.
Apply Zge_iff_le.
Apply iff_trans with b:=`(rho a) <= z-z0`. Apply Zle_plus_swap.
Apply Zle_is_le_bool.
Rewrite Zrho_zero. Intros. Apply iff_trans with `0+z < (rho a)+z0`. Rewrite Zero_left.
Split; Intro; Assumption.
Apply iff_trans with b:=`0 < (rho a)+z0-z`. Apply Zlt_plus_swap.
Unfold 2 Zminus. Rewrite Zplus_assoc_l. Unfold Zminus. Rewrite Zplus_assoc_l.
Exact (Zlt_is_le_bool `0` `(rho a)+z0+ -z`).
Rewrite Zrho_zero. Intros. Rewrite Zero_left. Apply iff_trans with b:=`(rho a)+z0 < z`.
Apply Zgt_iff_lt.
Apply iff_trans with b:=`(rho a) < z-z0`. Apply Zlt_plus_swap.
Apply Zlt_is_le_bool.
Rewrite Zrho_zero. Intros. Rewrite Zero_left. Split; Intro; Apply sym_eq; Assumption.
Rewrite Zrho_zero. Intros. Rewrite Zero_left. Apply iff_trans with `(rho a)+z0 = z`.
Split; Intro; Apply sym_eq; Assumption.
Apply Zeq_plus_swap.
Rewrite Zrho_zero. Intros. Rewrite Zero_left. Apply Zle_is_le_bool.
Rewrite Zrho_zero. Intros. Apply iff_trans with b:=`0+z <= (rho a)`. Rewrite Zero_left.
Apply Zge_iff_le.
Apply iff_trans with b:=`0 <= (rho a)-z`. Apply Zle_plus_swap.
Exact (Zle_is_le_bool `0` `(rho a)-z`).
Rewrite Zrho_zero. Intros. Rewrite Zero_left. Apply Zlt_is_le_bool.
Rewrite Zrho_zero. Intros. Apply iff_trans with b:=`0+z < (rho a)`. Rewrite Zero_left.
Apply Zgt_iff_lt.
Apply iff_trans with b:=`0 < (rho a)-z`. Apply Zlt_plus_swap.
Rewrite Zopp_Zplus. Rewrite Zplus_assoc_l. Exact (Zlt_is_le_bool `0` `(rho a)-z`).
Rewrite Zrho_zero. Intros. Rewrite Zero_left. Apply iff_trans with b:=`(rho a) <= z0-z`.
Apply Zle_plus_swap.
Apply Zle_is_le_bool.
Rewrite Zrho_zero. Intros. Apply iff_trans with b:=`0+z0 <= (rho a)+z`. Rewrite Zero_left.
Apply Zge_iff_le.
Apply iff_trans with b:=`0 <= (rho a)+z-z0`. Apply Zle_plus_swap.
Unfold 2 Zminus. Rewrite Zplus_assoc_l. Exact (Zle_is_le_bool `0` `(rho a)+z-z0`).
Rewrite Zrho_zero. Intros. Rewrite Zero_left. Apply iff_trans with b:=`(rho a) < z0-z`.
Apply Zlt_plus_swap.
Apply Zlt_is_le_bool.
Rewrite Zrho_zero. Intros. Apply iff_trans with b:=`0+z0 < (rho a)+z`. Rewrite Zero_left.
Apply Zgt_iff_lt.
Apply iff_trans with b:=`0 < (rho a)+z-z0`. Apply Zlt_plus_swap.
Unfold 2 Zminus. Rewrite Zplus_assoc_l. Unfold Zminus. Rewrite Zplus_assoc_l.
Exact (Zlt_is_le_bool `0` `(rho a)+z+ -z0`).
Rewrite Zrho_zero. Intros. Rewrite Zero_left. Split; Intro; Assumption.
Rewrite Zrho_zero. Intros. Rewrite Zero_left. Apply Zeq_plus_swap.
Rewrite Zrho_zero. Intros. Rewrite Zero_left. Apply iff_trans with b:=`0+z <= z0`.
Rewrite Zero_left. Split; Intro; Assumption.
Apply iff_trans with b:=`0 <= z0-z`. Apply Zle_plus_swap.
Apply Zle_is_le_bool.
Rewrite Zrho_zero. Intros. Rewrite Zero_left. Apply iff_trans with b:=`0+z < z0`.
Rewrite Zero_left. Split; Intro; Assumption.
Apply iff_trans with b:=`0 < z0-z`. Apply Zlt_plus_swap.
Apply Zlt_is_le_bool.
Rewrite Zrho_zero. Intros. Rewrite Zero_left. Apply iff_trans with b:=`0+z0 <= z`.
Rewrite Zero_left. Apply Zge_iff_le.
Apply iff_trans with b:=`0 <= z-z0`. Apply Zle_plus_swap.
Apply Zle_is_le_bool.
Rewrite Zrho_zero. Intros. Rewrite Zero_left. Apply iff_trans with b:=`0+z0 < z`.
Rewrite Zero_left. Apply Zgt_iff_lt.
Apply iff_trans with b:=`0 < z-z0`. Apply Zlt_plus_swap.
Apply Zlt_is_le_bool.
Rewrite Zrho_zero. Intros. Rewrite Zero_left. Split. Intro. Rewrite H. Apply Zminus_n_n.
Intro. Rewrite <- (Zero_left z0). Rewrite H. Unfold Zminus. Rewrite Zplus_assoc_r.
Rewrite Zplus_inverse_l. Rewrite Zero_right. Reflexivity.
Intros. Elim H. Intros. Elim H0. Intros. Split. Intro. Elim H5. Intros. Split. Apply H1.
Assumption.
Apply H3. Assumption.
Intro. Elim H5. Intros. Split. Apply H2. Assumption.
Apply H4. Assumption.
Intros. Elim H. Intros. Elim H0. Intros. Split. Intro. Elim H5. Intro. Left . Apply H1.
Assumption.
Intro. Right . Apply H3. Assumption.
Intro. Elim H5. Intro. Left . Apply H2. Assumption.
Intro. Right . Apply H4. Assumption.
Intros. Elim H. Intros. Elim H0. Intros. Split. Intros. Apply H3. Apply H5. Apply H2.
Assumption.
Intros. Apply H4. Apply H5. Apply H1. Assumption.
Unfold not. Intros. Elim H. Intros. Split. Intros. Apply H2. Apply H1. Assumption.
Intros. Apply H2. Apply H0. Assumption.
Intros. Fold (ZCG_eval rho (ZCGtranslate z))<->(ZCG_eval rho (ZCGtranslate z0)). Split.
Intro. Apply iff_trans with b:=(ZCGeval z). Apply iff_sym. Assumption.
Apply iff_trans with b:=(ZCGeval z0). Assumption.
Assumption.
Intro. Apply iff_trans with b:=(ZCG_eval rho (ZCGtranslate z)). Assumption.
Apply iff_trans with b:=(ZCG_eval rho (ZCGtranslate z0)). Assumption.
Apply iff_sym. Assumption.
Qed.
End ZCGevalDef.
Definition ZCG_solve
:= [f:ZCGForm] (CG_solve Z ZERO Zplus Zopp Zle_bool `1` (ZCGtranslate f)).
Theorem ZCG_solve_correct :
(f:ZCGForm) (ZCG_solve f)=true ->
{rho:ad->Z | (ZCGeval rho f) /\ (rho ad_z)=`0`}.
Proof.
Intros.
Elim (CG_solve_correct_anchored Z ZERO Zplus Zopp Zle_bool Zero_right
Zero_left Zplus_assoc_r Zplus_inverse_r Zle_bool_refl
Zle_bool_antisym Zle_bool_trans Zle_bool_total
Zle_bool_plus_mono `1` Zone_pos Zone_min_pos ad_z `0` ? H).
Intros rho H0. Split with rho. Elim H0. Intros. Split.
Apply (proj2 ? ? (ZCGeval_correct rho H2 f)). Assumption.
Assumption.
Qed.
Theorem ZCG_solve_complete
: (f:ZCGForm) (rho:ad->Z)
(ZCGeval rho f) -> (rho ad_z)=`0` -> (ZCG_solve f)=true.
Proof.
Intros. Unfold ZCG_solve.
Apply (CG_solve_complete Z ZERO Zplus Zopp Zle_bool Zero_right
Zero_left Zplus_assoc_r Zplus_inverse_r Zle_bool_refl
Zle_bool_antisym Zle_bool_trans Zle_bool_total
Zle_bool_plus_mono `1` Zone_pos Zone_min_pos (ZCGtranslate f)
rho).
Apply (proj1 ? ? (ZCGeval_correct rho H0 f)). Assumption.
Qed.
Definition ZCG_prove
:= [f:ZCGForm] (CG_prove Z ZERO Zplus Zopp Zle_bool `1` (ZCGtranslate f)).
Theorem ZCG_prove_correct
: (f:ZCGForm) (ZCG_prove f)=true ->
(rho:ad->Z) (rho ad_z)=`0` -> (ZCGeval rho f).
Proof.
Intros. Apply (proj2 ? ? (ZCGeval_correct rho H0 f)).
Exact (CG_prove_correct Z ZERO Zplus Zopp Zle_bool Zero_right Zero_left
Zplus_assoc_r Zplus_inverse_r Zle_bool_refl Zle_bool_antisym
Zle_bool_trans Zle_bool_total Zle_bool_plus_mono `1` Zone_pos
Zone_min_pos ? H rho).
Qed.
Theorem ZCG_prove_complete
: (f:ZCGForm)
((rho:ad->Z) (rho ad_z)=`0` -> (ZCGeval rho f)) -> (ZCG_prove f)=true.
Proof.
Intros. Unfold ZCG_prove.
Apply (CG_prove_complete_anchored Z ZERO Zplus Zopp Zle_bool Zero_right
Zero_left Zplus_assoc_r Zplus_inverse_r Zle_bool_refl
Zle_bool_antisym Zle_bool_trans Zle_bool_total
Zle_bool_plus_mono `1` Zone_pos Zone_min_pos (ZCGtranslate f)
ad_z `0`).
Intros. Exact (proj1 ? ? (ZCGeval_correct rho H0 f) (H rho H0)).
Qed.
(*i Tests:
Definition v := [n:Z] Cases n of
(POS p) => (ad_x p)
| _ => ad_z
end.
Lemma test1 : (x,y:Z) `x<=y` -> `x<=y+1`.
Proof.
Intros.
Cut (rho:ad->Z) (rho ad_z)=`0` ->
(ZCGeval rho (ZCGimp (ZCGle (v`1`) (v`2`)) (ZCGlep (v`1`) (v`2`) `1`))).
Intro.
Exact (H0 [a:ad]Case (ad_eq a (v`1`)) of x
Case (ad_eq a (v`2`)) of y
`0` end end
(refl_equal ? ?)
H).
Intros. Apply ZCG_prove_correct. Compute. Reflexivity.
Assumption.
Qed.
Lemma test2 : (x,y:Z) ~(`x<=y` -> `x<=y-1`).
Proof.
Intros.
Cut (rho:ad->Z) (rho ad_z)=`0` ->
(ZCGeval rho (ZCGnot (ZCGimp (ZCGle (v `1`) (v `2`)) (ZCGlep (v `1`) (v `2`) `-1`)))).
Intro.
Exact (H [a:ad] Case (ad_eq a (v `1`)) of x
Case (ad_eq a (v `2`)) of y
`0` end end (refl_equal ? ?)).
Intros. Apply ZCG_prove_correct. Compute. (* fails: remains to prove false=true; indeed,
test2 is not provable. *)
<Your Tactic Text here>
<Your Tactic Text here>
i*)
|
