-
Notifications
You must be signed in to change notification settings - Fork 1
/
Section6.v
308 lines (249 loc) · 5.98 KB
/
Section6.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
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
Load Formulas.
Require Import Psatz.
Parameter ineqAdd : forall {a b c d}, (a <= b) -> (c <= d) -> (a + c <= b + d).
Parameter le_trans' : forall {x y z:Z}, x <= y -> y <= z -> x <= z.
Opaque Z.gt.
Opaque Z.lt.
Opaque Z.add.
Opaque Z.sub.
Opaque Z.ge.
Opaque Z.le.
Theorem T220a: Problem220aTrue. cbv.
destruct fast_A as [fast].
intros itelxz isCompy1 pc6083 isCompy2.
split.
lia.
assumption.
Qed.
Theorem T221a: Problem221aTrue. cbv.
destruct fast_A.
Abort All.
Theorem T221a: Problem221aFalse. cbv.
destruct fast_A.
intros.
Abort All.
Theorem T222a: Problem222aTrue. cbv.
destruct fast_A.
Abort All.
Theorem T222a: Problem222aFalse. cbv.
destruct fast_A.
Abort All.
Theorem T223a: Problem223aFalse.
assert (H' := fast_and_slow_opposite_K).
cbv.
intros itelxz isCompy1 pc6083 isCompy2.
intro P.
destruct fast_A as [fastness fastThres].
destruct slow_A as [slowness slowThres].
destruct (H' computer_N pc6083) as [neg disj].
destruct (H' computer_N itelxz) as [neg' disj'].
destruct P.
lia.
Qed.
Theorem T224a: Problem224aTrue. cbv.
intros itelxz isCompy1 pc6083 isCompy2.
intros.
destruct fast_A as [fast].
destruct slow_A as [slow].
intros.
split.
lia.
assumption.
Qed.
Theorem T225a: Problem225aTrue. cbv.
intros itelxz isCompy1 pc6083 isCompy2.
intros.
destruct fast_A as [fast].
destruct slow_A as [slow].
firstorder.
Abort All.
Theorem T225a: Problem225aFalse. cbv.
intros itelxz isCompy1 pc6083 isCompy2.
intros.
destruct fast_A as [fast].
destruct slow_A as [slow].
firstorder.
Abort All.
Theorem T226a: Problem226aTrue. cbv.
intros itelxz isCompy1 pc6083 isCompy2.
intros.
destruct fast_A as [fast].
destruct slow_A as [slow].
split.
lia.
assumption.
Qed. (* Fracas wrong *)
Theorem T227a: Problem227aFalse. cbv.
assert (H' := fast_and_slow_opposite_K).
intros itel_xz isCompy1 pc6083 isCompy2.
intros.
apply slow_and_fast_disjoint_K with (cn := computer_N) (o := pc6083).
destruct fast_A as [fast].
destruct slow_A as [slow].
destruct (H' computer_N pc6083) as [neg disj].
destruct (H' computer_N itel_xz) as [neg' disj'].
intros.
lia.
Qed.
Theorem T228a: Problem228aFalse. cbv.
intros itelxz isCompy1 pc6083 isCompy2.
intros.
apply slow_and_fast_disjoint_K with (cn := computer_N) (o := pc6083).
destruct fast_A as [fast].
destruct slow_A as [slow].
(*firstorder SLoooow *)
Abort All.
Theorem T228a: Problem228aTrue. cbv.
intros itelxz isCompy1 pc6083 isCompy2.
intros.
destruct fast_A as [fast].
destruct slow_A as [slow].
(*firstorder SLoooow *)
Abort All.
Theorem T229a: Problem229aFalse. cbv.
intros itelxz isCompy1 pc6082 isCompy2.
assert (H' := fast_and_slow_opposite_K).
cbv.
destruct fast_A as [fastness fastThres].
destruct slow_A as [slowness slowThres].
destruct (H' computer_N pc6082) as [neg disj].
destruct (H' computer_N itelxz) as [neg' disj'].
intros P1 H.
(* This should work (Coq needs some convincing.)
lia.
Qed.
*)
Abort All.
Theorem T230a: Problem230aTrue. cbv.
intros n [P1a P1b].
firstorder.
Qed.
Theorem T231a: Problem231aTrue. cbv.
intros n [P1a P1b].
firstorder.
Abort All.
Theorem T232a: Problem232aTrue. cbv.
intros n [P1a [[orders P1c] [P1d P1e]]].
exists orders.
split.
firstorder.
split.
firstorder.
lia.
Qed.
Theorem T233a: Problem233aTrue. cbv.
intros n P1.
destruct P1 as [orders P1].
firstorder.
Qed.
Theorem T234a: Problem234aTrue. cbv.
firstorder.
Abort All.
Theorem T235a: Problem235aTrue. cbv.
intros n [P1a [[orders P1c] [P1d P1e]]].
exists orders.
split.
firstorder.
split.
firstorder.
lia.
Qed.
Theorem T236a: Problem236bTrue. cbv.
intros contract isContract P1.
firstorder.
Qed.
Theorem T237a: Problem237bTrue. cbv.
intros contract isContract [P1a [order P1b]].
exists order.
split.
firstorder.
split.
firstorder.
lia.
Qed.
Theorem T238a: Problem238aTrue. cbv.
intros n [P1a [[order [isOrder [won P1]]] [order' [isOrder' [won' P2]]]]].
exists order.
split.
firstorder.
split.
firstorder.
lia.
Qed.
Theorem T239a: Problem239aTrue. cbv.
intros n [P1a P1b].
firstorder.
Qed.
Theorem T240a: Problem240aTrue. cbv.
intros n [P1a [order P1b]].
exists order.
split.
firstorder.
Abort All.
Theorem T241a: Problem241aTrue. cbv.
intros n [P1a [[order [isOrder [won P1]]] [order' [isOrder' [lost P2]]]]].
exists order.
split.
firstorder.
split.
firstorder.
lia.
Qed.
Theorem T242a: Problem242aTrue. cbv.
assert (H' := fast_and_slow_opposite_K).
intros pc6083 isCompy itelxz isItel.
intros [[mips [isMips [P1b P1a]]] [mips' [isMips' [P2b P2a]]]].
destruct fast_A as [fastness fastThres].
destruct slow_A as [slowness slowThres].
destruct (H' computer_N pc6083) as [neg disj].
destruct (H' computer_N itelxz) as [neg' disj'].
Abort All. (* Error: "MIPS" is interpreted as any CN; this is completely wrong. *)
Theorem T243a: Problem243aTrue. cbv.
intros n [P1a [[order [isOrder [won P1]]] [order' [isOrder' [lost P2]]]]].
exists order.
split.
firstorder.
split.
firstorder.
lia.
Qed.
Theorem T246a: Problem246aTrue. cbv.
destruct fast_A as [fast] eqn:fst.
destruct slow_A as [slow] eqn:slw.
firstorder.
Qed.
Theorem T247a: Problem247aTrue. cbv.
destruct fast_A as [fast] eqn:fst.
destruct slow_A as [slow] eqn:slw.
Abort All.
Theorem T247a: Problem247aFalse. cbv.
destruct fast_A as [fast] eqn:fst.
destruct slow_A as [slow] eqn:slw.
(*firstorder. slow *)
Abort All.
Theorem T248a: Problem248aTrue. cbv.
destruct fast_A as [fast] eqn:fst.
destruct slow_A as [slow] eqn:slw.
firstorder.
Qed.
Theorem T249a: Problem249aTrue. cbv.
destruct fast_A as [fast] eqn:fst.
destruct slow_A as [slow] eqn:slw.
firstorder.
Qed.
Theorem T250a: Problem250aTrue. cbv.
intros itelxz isCompy1 itelxy isCompy1' pc6083 isCompy2.
destruct fast_A as [fast] eqn:fst.
destruct slow_A as [slow] eqn:slw.
intro P1.
destruct P1 as [L | R].
(* Left branch *)
assumption.
(* Right branch *)
Abort All.
(* P1 is read as: (The PC-6082 is faster than the ITEL-ZX) or (The
PC-6082 is faster than the ITEL-ZY) Which does not imply the
conclusion.
JP: I disagree with FraCas here! "or" can only be read as "and" for
pragmatic reasons. (that is: saying "or" in this context is usually
wasteful; the listener assumes a mistake and interprets as "and" ) *)