|
1
|
Require Export Streams.
|
|
2
|
Require List.
|
|
3
|
Require Import Setoid.
|
|
4
|
Require Import Relation_Definitions.
|
|
5
|
Require Import Program.Wf.
|
|
6
|
Require Import Wf_nat.
|
|
7
|
Require Import Wellfounded.
|
|
8
|
|
|
9
|
Definition mapT (F : Type -> Type) {A B} := (A -> B) -> (F A) -> (F B).
|
|
10
|
|
|
11
|
Definition applyT (F : Type -> Type) {A B} := (F (A -> B)) -> (F A) -> (F B).
|
|
12
|
|
|
13
|
Definition option_apply {A B} : @applyT option A B :=
|
|
14
|
fun f a =>
|
|
15
|
match f, a with
|
|
16
|
| Some f, Some a => Some (f a)
|
|
17
|
| _ , _ => None
|
|
18
|
end.
|
|
19
|
|
|
20
|
|
|
21
|
Axiom eqst_eq : forall {A} (s s' : Stream A), EqSt s s' -> s = s'.
|
|
22
|
|
|
23
|
Theorem inv_inv : forall {A} (P : Stream A -> Prop) (s : Stream A), ForAll P s -> ForAll (fun s' => ForAll P s') s.
|
|
24
|
Proof.
|
|
25
|
intros A P.
|
|
26
|
cofix proof.
|
|
27
|
destruct s as (s0, s').
|
|
28
|
intro H.
|
|
29
|
apply HereAndFurther.
|
|
30
|
exact H.
|
|
31
|
|
|
32
|
simpl.
|
|
33
|
apply proof.
|
|
34
|
inversion H.
|
|
35
|
assumption.
|
|
36
|
Qed.
|
|
37
|
|
|
38
|
Theorem evt_inv : forall {A} (P Q : Stream A -> Prop) (s : Stream A),
|
|
39
|
ForAll P s -> Exists Q s -> Exists (fun s' => P s' /\ Q s') s.
|
|
40
|
Proof.
|
|
41
|
induction 2.
|
|
42
|
apply Here.
|
|
43
|
inversion H.
|
|
44
|
intuition.
|
|
45
|
|
|
46
|
apply Further.
|
|
47
|
apply IHExists.
|
|
48
|
inversion H.
|
|
49
|
assumption.
|
|
50
|
Qed.
|
|
51
|
|
|
52
|
CoFixpoint ForAll_apply {A} {P Q : (Stream A -> Prop)} : forall s, (ForAll P s) -> (ForAll (fun s => P s -> Q s) s) -> (ForAll Q s) :=
|
|
53
|
fun s always_p always_pq =>
|
|
54
|
match always_p, always_pq with
|
|
55
|
| (HereAndFurther p_s always_p'), (HereAndFurther pq_s always_pq') => HereAndFurther s (pq_s p_s) (ForAll_apply (tl s) always_p' always_pq')
|
|
56
|
end.
|
|
57
|
|
|
58
|
CoFixpoint necessitation {A} {P : Stream A -> Prop} (I : forall s, P s) s : ForAll P s :=
|
|
59
|
HereAndFurther s (I s) (necessitation I (tl s)).
|
|
60
|
|
|
61
|
Definition ForAll_reinforce {A} {P Q : (Stream A -> Prop)} : forall s, (ForAll (fun s => P s /\ Q s) s) -> (ForAll Q s).
|
|
62
|
Proof.
|
|
63
|
intros.
|
|
64
|
eapply ForAll_apply.
|
|
65
|
apply H.
|
|
66
|
|
|
67
|
apply necessitation.
|
|
68
|
intuition.
|
|
69
|
Defined.
|
|
70
|
|
|
71
|
Definition concat {A} (prefix : list A) (suffix : Stream A) : Stream A :=
|
|
72
|
List.fold_left (fun q t => Cons t q) prefix suffix.
|
|
73
|
|
|
74
|
Theorem eqst_concat : forall {A} pfx (sfx sfx' : Stream A), EqSt sfx sfx' -> EqSt (concat pfx sfx) (concat pfx sfx').
|
|
75
|
Proof.
|
|
76
|
induction pfx.
|
|
77
|
auto.
|
|
78
|
|
|
79
|
simpl.
|
|
80
|
intros.
|
|
81
|
apply IHpfx.
|
|
82
|
apply eqst.
|
|
83
|
reflexivity.
|
|
84
|
|
|
85
|
exact H.
|
|
86
|
Qed.
|
|
87
|
|
|
88
|
Theorem concat_eqst : forall {A} pfx pfx' (sfx sfx' : Stream A), List.length pfx = List.length pfx' -> EqSt (concat pfx sfx) (concat pfx' sfx') -> pfx = pfx' /\ EqSt sfx sfx'.
|
|
89
|
Proof.
|
|
90
|
induction pfx.
|
|
91
|
destruct pfx'.
|
|
92
|
intuition.
|
|
93
|
|
|
94
|
discriminate.
|
|
95
|
|
|
96
|
destruct pfx'.
|
|
97
|
discriminate.
|
|
98
|
|
|
99
|
simpl.
|
|
100
|
intros.
|
|
101
|
injection H.
|
|
102
|
clear H; intro H.
|
|
103
|
generalize (IHpfx _ _ _ H H0).
|
|
104
|
destruct 1.
|
|
105
|
inversion H2.
|
|
106
|
simpl in H3.
|
|
107
|
simpl in H4.
|
|
108
|
subst.
|
|
109
|
intuition.
|
|
110
|
Qed.
|
|
111
|
|
|
112
|
Theorem evt_id : forall {A} (s : Stream A), Exists (fun s' => s = s') s.
|
|
113
|
Proof.
|
|
114
|
intros.
|
|
115
|
apply Here.
|
|
116
|
reflexivity.
|
|
117
|
Qed.
|
|
118
|
|
|
119
|
Theorem evt_concat : forall {A} (P : Stream A -> Prop) p (s : Stream A), Exists P s -> Exists P (concat p s).
|
|
120
|
Proof.
|
|
121
|
induction p.
|
|
122
|
trivial.
|
|
123
|
|
|
124
|
intros s H.
|
|
125
|
apply (IHp (Cons a s)).
|
|
126
|
apply Further.
|
|
127
|
exact H.
|
|
128
|
Qed.
|
|
129
|
|
|
130
|
Theorem inv_concat : forall {A} (P : Stream A -> Prop) p (s : Stream A), ForAll P (concat p s) -> ForAll P s.
|
|
131
|
Proof.
|
|
132
|
induction p.
|
|
133
|
trivial.
|
|
134
|
|
|
135
|
simpl.
|
|
136
|
intros s H.
|
|
137
|
generalize (IHp (Cons a s) H).
|
|
138
|
intro H'.
|
|
139
|
inversion H'.
|
|
140
|
assumption.
|
|
141
|
Qed.
|
|
142
|
|
|
143
|
CoFixpoint lift {A} (v : A) := Cons v (lift v).
|
|
144
|
|
|
145
|
Lemma hd_lift : forall {A} {v : A}, hd (lift v) = v.
|
|
146
|
Proof.
|
|
147
|
reflexivity.
|
|
148
|
Qed.
|
|
149
|
|
|
150
|
Lemma tl_lift : forall {A} {v : A}, tl (lift v) = lift v.
|
|
151
|
Proof.
|
|
152
|
reflexivity.
|
|
153
|
Qed.
|
|
154
|
|
|
155
|
CoFixpoint apply {A B} : @applyT Stream A B :=
|
|
156
|
fun f a =>
|
|
157
|
match f, a with
|
|
158
|
| (Cons f0 f'), (Cons a0 a') => Cons (f0 a0) (apply f' a')
|
|
159
|
end.
|
|
160
|
|
|
161
|
Lemma hd_apply : forall {A B} {f : Stream (A -> B)} {a : Stream A}, hd (apply f a) = (hd f) (hd a).
|
|
162
|
Proof.
|
|
163
|
destruct f; destruct a.
|
|
164
|
reflexivity.
|
|
165
|
Qed.
|
|
166
|
|
|
167
|
Lemma tl_apply : forall {A B} {f : Stream (A -> B)} {a : Stream A}, tl (apply f a) = apply (tl f) (tl a).
|
|
168
|
Proof.
|
|
169
|
destruct f; destruct a.
|
|
170
|
reflexivity.
|
|
171
|
Qed.
|
|
172
|
|
|
173
|
Lemma cons_apply : forall {A B} {f0 : A -> B} {f' : Stream (A -> B)} {a0 : A} {a' : Stream A}, EqSt (apply (Cons f0 f') (Cons a0 a')) (Cons (f0 a0) (apply f' a')).
|
|
174
|
Proof.
|
|
175
|
intros.
|
|
176
|
apply eqst.
|
|
177
|
reflexivity.
|
|
178
|
|
|
179
|
apply EqSt_reflex.
|
|
180
|
Qed.
|
|
181
|
|
|
182
|
Lemma eqst_apply : forall {A B} {f f' : Stream (A -> B)} {a a' : Stream A},
|
|
183
|
EqSt f f' -> EqSt a a' -> EqSt (apply f a) (apply f' a').
|
|
184
|
Proof.
|
|
185
|
intros A B.
|
|
186
|
cofix proof.
|
|
187
|
intros.
|
|
188
|
inversion H.
|
|
189
|
inversion H0.
|
|
190
|
apply eqst.
|
|
191
|
rewrite hd_apply.
|
|
192
|
rewrite hd_apply.
|
|
193
|
congruence.
|
|
194
|
|
|
195
|
rewrite tl_apply.
|
|
196
|
rewrite tl_apply.
|
|
197
|
apply proof.
|
|
198
|
assumption.
|
|
199
|
|
|
200
|
assumption.
|
|
201
|
Qed.
|
|
202
|
|
|
203
|
Theorem inv_map : forall {A B} (f : A -> B) P (s : Stream A), ForAll P (apply (lift f) s) -> ForAll (fun s' => P (apply (lift f) s')) s.
|
|
204
|
Proof.
|
|
205
|
intros A B f P.
|
|
206
|
cofix proof.
|
|
207
|
destruct s as (s0, s').
|
|
208
|
intro H.
|
|
209
|
inversion H.
|
|
210
|
apply HereAndFurther.
|
|
211
|
assumption.
|
|
212
|
|
|
213
|
simpl.
|
|
214
|
apply proof.
|
|
215
|
assumption.
|
|
216
|
Qed.
|
|
217
|
|
|
218
|
Theorem map_inv : forall {A B} (f : A -> B) P (s : Stream A), ForAll (fun s' => P (apply (lift f) s')) s -> ForAll P (apply (lift f) s).
|
|
219
|
Proof.
|
|
220
|
intros A B f P.
|
|
221
|
cofix proof.
|
|
222
|
destruct s as (s0, s').
|
|
223
|
intro H.
|
|
224
|
inversion H.
|
|
225
|
apply HereAndFurther.
|
|
226
|
assumption.
|
|
227
|
|
|
228
|
simpl.
|
|
229
|
apply proof.
|
|
230
|
assumption.
|
|
231
|
Qed.
|
|
232
|
|
|
233
|
Theorem evt_map : forall {A B} (f : A -> B) P (s : Stream A), Exists P (apply (lift f) s) -> Exists (fun s' => P (apply (lift f) s')) s.
|
|
234
|
Proof.
|
|
235
|
intros A B f P s.
|
|
236
|
remember (apply (lift f) s) as ss.
|
|
237
|
intro H.
|
|
238
|
revert s Heqss.
|
|
239
|
induction H.
|
|
240
|
intros.
|
|
241
|
apply Here.
|
|
242
|
rewrite <- Heqss.
|
|
243
|
exact H.
|
|
244
|
|
|
245
|
intros.
|
|
246
|
apply Further.
|
|
247
|
apply (IHExists (tl s)).
|
|
248
|
rewrite <- tl_lift.
|
|
249
|
rewrite <- tl_apply.
|
|
250
|
apply f_equal.
|
|
251
|
exact Heqss.
|
|
252
|
Qed.
|
|
253
|
|
|
254
|
Theorem map_evt : forall {A B} (f : A -> B) P (s : Stream A), Exists (fun s' => P (apply (lift f) s')) s -> Exists P (apply (lift f) s).
|
|
255
|
Proof.
|
|
256
|
intros A B f P s.
|
|
257
|
intro H.
|
|
258
|
induction H.
|
|
259
|
apply Here.
|
|
260
|
exact H.
|
|
261
|
|
|
262
|
apply Further.
|
|
263
|
rewrite tl_apply.
|
|
264
|
rewrite tl_lift.
|
|
265
|
exact IHExists.
|
|
266
|
Qed.
|
|
267
|
|
|
268
|
Definition zip {A B} (s : Stream A * Stream B) := apply (apply (lift (fun a b => (a, b))) (fst s)) (snd s).
|
|
269
|
|
|
270
|
Lemma zip_fst_eqst : forall {A B}, forall (s1 s1' : Stream A) (s2 s2' : Stream B),
|
|
271
|
EqSt (zip (s1, s2)) (zip (s1', s2')) -> EqSt s1 s1'.
|
|
272
|
Proof.
|
|
273
|
intros A B.
|
|
274
|
cofix proof.
|
|
275
|
destruct s1; destruct s1'; destruct s2; destruct s2'.
|
|
276
|
intro.
|
|
277
|
inversion H.
|
|
278
|
apply eqst.
|
|
279
|
simpl in H0.
|
|
280
|
simpl in H1.
|
|
281
|
injection H0.
|
|
282
|
intros.
|
|
283
|
subst.
|
|
284
|
reflexivity.
|
|
285
|
|
|
286
|
eapply proof.
|
|
287
|
apply H1.
|
|
288
|
Qed.
|
|
289
|
|
|
290
|
Lemma zip_fst : forall {A B}, forall (s1 s1' : Stream A) (s2 s2' : Stream B),
|
|
291
|
zip (s1, s2) = zip (s1', s2') -> s1 = s1'.
|
|
292
|
Proof.
|
|
293
|
intros.
|
|
294
|
apply eqst_eq.
|
|
295
|
apply (zip_fst_eqst s1 s1' s2 s2').
|
|
296
|
rewrite H.
|
|
297
|
apply EqSt_reflex.
|
|
298
|
Qed.
|
|
299
|
|
|
300
|
Lemma zip_snd_eqst : forall {A B}, forall (s1 s1' : Stream A) (s2 s2' : Stream B),
|
|
301
|
EqSt (zip (s1, s2)) (zip (s1', s2')) -> EqSt s2 s2'.
|
|
302
|
Proof.
|
|
303
|
intros A B.
|
|
304
|
cofix proof.
|
|
305
|
destruct s1; destruct s1'; destruct s2; destruct s2'.
|
|
306
|
intro.
|
|
307
|
inversion H.
|
|
308
|
apply eqst.
|
|
309
|
simpl in H0.
|
|
310
|
simpl in H1.
|
|
311
|
injection H0.
|
|
312
|
intros.
|
|
313
|
subst.
|
|
314
|
reflexivity.
|
|
315
|
|
|
316
|
eapply proof.
|
|
317
|
apply H1.
|
|
318
|
Qed.
|
|
319
|
|
|
320
|
Lemma zip_snd : forall {A B}, forall (s1 s1' : Stream A) (s2 s2' : Stream B),
|
|
321
|
zip (s1, s2) = zip (s1', s2') -> s2 = s2'.
|
|
322
|
Proof.
|
|
323
|
intros.
|
|
324
|
apply eqst_eq.
|
|
325
|
apply (zip_snd_eqst s1 s1' s2 s2').
|
|
326
|
rewrite H.
|
|
327
|
apply EqSt_reflex.
|
|
328
|
Qed.
|
|
329
|
|
|
330
|
Definition unzip {A B} (s : Stream (A*B)) := (apply (lift (@fst _ _)) s, apply (lift (@snd _ _)) s).
|
|
331
|
|
|
332
|
Lemma fst_zip_eqst : forall {A B} (s1 : Stream A) (s2 : Stream B), EqSt (apply (lift (@fst _ _)) (zip (s1, s2))) s1.
|
|
333
|
Proof.
|
|
334
|
intros A B.
|
|
335
|
cofix proof.
|
|
336
|
destruct s1; destruct s2.
|
|
337
|
apply eqst.
|
|
338
|
reflexivity.
|
|
339
|
|
|
340
|
apply proof.
|
|
341
|
Qed.
|
|
342
|
|
|
343
|
Lemma fst_zip : forall {A B} (s1 : Stream A) (s2 : Stream B), apply (lift (@fst _ _)) (zip (s1, s2)) = s1.
|
|
344
|
Proof.
|
|
345
|
intros.
|
|
346
|
apply eqst_eq.
|
|
347
|
apply fst_zip_eqst.
|
|
348
|
Qed.
|
|
349
|
|
|
350
|
Lemma snd_zip_eqst : forall {A B} (s1 : Stream A) (s2 : Stream B), EqSt (apply (lift (@snd _ _)) (zip (s1, s2))) s2.
|
|
351
|
Proof.
|
|
352
|
intros A B.
|
|
353
|
cofix proof.
|
|
354
|
destruct s1; destruct s2.
|
|
355
|
apply eqst.
|
|
356
|
reflexivity.
|
|
357
|
|
|
358
|
apply proof.
|
|
359
|
Qed.
|
|
360
|
|
|
361
|
Lemma snd_zip : forall {A B} (s1 : Stream A) (s2 : Stream B), apply (lift (@snd _ _)) (zip (s1, s2)) = s2.
|
|
362
|
Proof.
|
|
363
|
intros.
|
|
364
|
apply eqst_eq.
|
|
365
|
apply snd_zip_eqst.
|
|
366
|
Qed.
|
|
367
|
|
|
368
|
Lemma zip_unzip_eqst : forall {A B} (s : Stream (A*B)), EqSt (zip (unzip s)) s.
|
|
369
|
Proof.
|
|
370
|
intros A B.
|
|
371
|
cofix proof.
|
|
372
|
destruct s.
|
|
373
|
apply eqst.
|
|
374
|
simpl.
|
|
375
|
destruct p.
|
|
376
|
reflexivity.
|
|
377
|
|
|
378
|
simpl.
|
|
379
|
apply proof.
|
|
380
|
Qed.
|
|
381
|
|
|
382
|
Lemma zip_unzip : forall {A B} (s : Stream (A*B)), zip (unzip s) = s.
|
|
383
|
Proof.
|
|
384
|
intros.
|
|
385
|
apply eqst_eq.
|
|
386
|
apply zip_unzip_eqst.
|
|
387
|
Qed.
|
|
388
|
|
|
389
|
Theorem inv_eq_eqst : forall {A} (s s' : Stream A),
|
|
390
|
ForAll (fun ss' => fst (hd ss') = snd (hd ss')) (zip (s, s')) -> EqSt s s'.
|
|
391
|
Proof.
|
|
392
|
intro A.
|
|
393
|
cofix proof.
|
|
394
|
destruct s as (s0, s').
|
|
395
|
destruct 0 as (t0, t').
|
|
396
|
intro H.
|
|
397
|
inversion H.
|
|
398
|
apply eqst.
|
|
399
|
assumption.
|
|
400
|
|
|
401
|
apply proof.
|
|
402
|
assumption.
|
|
403
|
Qed.
|
|
404
|
|
|
405
|
Theorem eqst_inv_eq : forall {A} (s s' : Stream A),
|
|
406
|
EqSt s s' -> ForAll (fun ss' => fst (hd ss') = snd (hd ss')) (zip (s, s')).
|
|
407
|
Proof.
|
|
408
|
intro A.
|
|
409
|
cofix proof.
|
|
410
|
destruct s as (s0, s').
|
|
411
|
destruct 0 as (t0, t').
|
|
412
|
intro H.
|
|
413
|
inversion H.
|
|
414
|
apply HereAndFurther.
|
|
415
|
assumption.
|
|
416
|
|
|
417
|
apply proof.
|
|
418
|
assumption.
|
|
419
|
Qed.
|
|
420
|
|
|
421
|
|
|
422
|
CoFixpoint history_rec {A} (past : list A) (s : Stream A) : Stream (list A * A) :=
|
|
423
|
match s with
|
|
424
|
| Cons s0 s' => Cons (past, s0) (history_rec (cons s0 past) s')
|
|
425
|
end.
|
|
426
|
|
|
427
|
Definition history {A} (s : Stream A) : Stream (list A * A) := history_rec nil s.
|
|
428
|
|
|
429
|
Theorem eqst_history_rec : forall {A} (pfx : list A) (sfx sfx' : Stream A),
|
|
430
|
EqSt sfx sfx' -> EqSt (history_rec pfx sfx) (history_rec pfx sfx').
|
|
431
|
Proof.
|
|
432
|
intros A.
|
|
433
|
cofix proof.
|
|
434
|
destruct sfx as (sfx0, sfxq).
|
|
435
|
destruct sfx' as (sfx0', sfxq').
|
|
436
|
intro H.
|
|
437
|
inversion H.
|
|
438
|
simpl in H0.
|
|
439
|
rewrite H0.
|
|
440
|
apply eqst.
|
|
441
|
reflexivity.
|
|
442
|
|
|
443
|
apply (proof _ sfxq sfxq').
|
|
444
|
assumption.
|
|
445
|
Qed.
|
|
446
|
|
|
447
|
Theorem eqst_history : forall {A} (sfx sfx' : Stream A),
|
|
448
|
EqSt sfx sfx' -> EqSt (history sfx) (history sfx').
|
|
449
|
Proof.
|
|
450
|
intros.
|
|
451
|
apply eqst_history_rec.
|
|
452
|
assumption.
|
|
453
|
Qed.
|
|
454
|
|
|
455
|
Theorem unzip_history_rec : forall {A} (pfx : list A) (sfx : Stream A), EqSt (snd (unzip (history_rec pfx sfx))) sfx.
|
|
456
|
Proof.
|
|
457
|
intro A.
|
|
458
|
cofix proof.
|
|
459
|
destruct sfx as (sfx0, sfx').
|
|
460
|
apply eqst.
|
|
461
|
reflexivity.
|
|
462
|
|
|
463
|
apply proof.
|
|
464
|
Qed.
|
|
465
|
|
|
466
|
Theorem unzip_history : forall {A} (s : Stream A), EqSt (snd (unzip (history s))) s.
|
|
467
|
Proof.
|
|
468
|
unfold history.
|
|
469
|
intros.
|
|
470
|
apply unzip_history_rec.
|
|
471
|
Qed.
|
|
472
|
|
|
473
|
Definition History_Spec {A} (s : Stream A) s' :=
|
|
474
|
fst (hd (tl s')) = cons (snd (hd s')) (fst (hd s'))
|
|
475
|
/\ EqSt (concat (fst (hd s')) (apply (lift (@snd _ _)) s')) s.
|
|
476
|
|
|
477
|
Theorem history_rec_spec : forall {A} p (s : Stream A),
|
|
478
|
fst (hd (history_rec p s)) = p
|
|
479
|
/\ ForAll (fun s' => History_Spec (concat p s) s') (history_rec p s).
|
|
480
|
Proof.
|
|
481
|
intros.
|
|
482
|
split.
|
|
483
|
destruct s.
|
|
484
|
reflexivity.
|
|
485
|
|
|
486
|
revert p s.
|
|
487
|
cofix proof.
|
|
488
|
destruct s as (s0, s').
|
|
489
|
apply HereAndFurther.
|
|
490
|
split.
|
|
491
|
simpl.
|
|
492
|
destruct s'.
|
|
493
|
reflexivity.
|
|
494
|
|
|
495
|
apply eqst_concat.
|
|
496
|
apply unzip_history_rec.
|
|
497
|
|
|
498
|
apply (proof (cons s0 p) s').
|
|
499
|
Qed.
|
|
500
|
|
|
501
|
Theorem history_spec : forall {A} (s : Stream A),
|
|
502
|
fst (hd (history s)) = nil
|
|
503
|
/\ ForAll (fun s' => History_Spec s s') (history s).
|
|
504
|
Proof.
|
|
505
|
intros.
|
|
506
|
generalize (history_rec_spec nil s).
|
|
507
|
intuition.
|
|
508
|
Qed.
|
|
509
|
|
|
510
|
Theorem history_rec_spec_complete : forall {A} p (s : Stream A) ps,
|
|
511
|
fst (hd ps) = p -> ForAll (fun s' => History_Spec (concat p s) s') ps -> EqSt ps (history_rec p s).
|
|
512
|
Proof.
|
|
513
|
intro A.
|
|
514
|
cofix proof.
|
|
515
|
intros.
|
|
516
|
destruct s as (s0, s').
|
|
517
|
destruct ps as ((p_ps0, s_ps0), ps').
|
|
518
|
simpl in H.
|
|
519
|
subst.
|
|
520
|
inversion H0.
|
|
521
|
unfold History_Spec in H.
|
|
522
|
destruct H.
|
|
523
|
simpl in H.
|
|
524
|
apply eqst.
|
|
525
|
simpl.
|
|
526
|
intros.
|
|
527
|
simpl in H.
|
|
528
|
subst.
|
|
529
|
inversion H0.
|
|
530
|
unfold History_Spec in H.
|
|
531
|
destruct H.
|
|
532
|
simpl.
|
|
533
|
simpl in H2.
|
|
534
|
destruct (concat_eqst _ _ _ _ refl_equal H2).
|
|
535
|
inversion H5.
|
|
536
|
simpl in H6.
|
|
537
|
subst.
|
|
538
|
reflexivity.
|
|
539
|
|
|
540
|
simpl.
|
|
541
|
apply proof.
|
|
542
|
simpl in H2.
|
|
543
|
destruct (concat_eqst _ _ _ _ refl_equal H2).
|
|
544
|
inversion H4.
|
|
545
|
simpl in H5.
|
|
546
|
subst.
|
|
547
|
assumption.
|
|
548
|
|
|
549
|
assumption.
|
|
550
|
Qed.
|
|
551
|
|
|
552
|
Theorem history_spec_complete : forall {A} (s : Stream A) ps,
|
|
553
|
fst (hd ps) = nil -> ForAll (fun s' => History_Spec s s') ps -> EqSt ps (history s).
|
|
554
|
Proof.
|
|
555
|
intros.
|
|
556
|
apply history_rec_spec_complete.
|
|
557
|
assumption.
|
|
558
|
|
|
559
|
assumption.
|
|
560
|
Qed.
|
|
561
|
|
|
562
|
Theorem inv_snd_history_rec_intro : forall {A} (P : Stream A -> Prop) p (s : Stream A),
|
|
563
|
ForAll P s -> ForAll (fun s' => P (apply (lift (@snd _ _)) s')) (history_rec p s).
|
|
564
|
Proof.
|
|
565
|
intros.
|
|
566
|
apply inv_map.
|
|
567
|
generalize (eqst_eq _ _ (unzip_history_rec p s)).
|
|
568
|
simpl.
|
|
569
|
intro Hs.
|
|
570
|
rewrite Hs.
|
|
571
|
exact H.
|
|
572
|
Qed.
|
|
573
|
|
|
574
|
Theorem inv_snd_history_intro : forall {A} (P : Stream A -> Prop) (s : Stream A),
|
|
575
|
ForAll P s -> ForAll (fun s' => P (apply (lift (@snd _ _)) s')) (history s).
|
|
576
|
Proof.
|
|
577
|
intros.
|
|
578
|
apply inv_snd_history_rec_intro.
|
|
579
|
assumption.
|
|
580
|
Qed.
|
|
581
|
|
|
582
|
Theorem inv_snd_history_rec_elim : forall {A} (P : Stream A -> Prop) p (s : Stream A),
|
|
583
|
ForAll (fun s' => P (apply (lift (@snd _ _)) s')) (history_rec p s) -> ForAll P s.
|
|
584
|
Proof.
|
|
585
|
intros.
|
|
586
|
rewrite <- (eqst_eq _ _ (unzip_history_rec p s)).
|
|
587
|
apply map_inv.
|
|
588
|
exact H.
|
|
589
|
Qed.
|
|
590
|
|
|
591
|
Theorem inv_snd_history_elim : forall {A} (P : Stream A -> Prop) (s : Stream A),
|
|
592
|
ForAll (fun s' => P (apply (lift (@snd _ _)) s')) (history s) -> ForAll P s.
|
|
593
|
Proof.
|
|
594
|
intros.
|
|
595
|
apply inv_snd_history_rec_elim with (p := nil).
|
|
596
|
assumption.
|
|
597
|
Qed.
|
|
598
|
|
|
599
|
Fixpoint prefix {A} (I : A -> Prop) (T : A -> A -> Prop) (k : nat) : list A -> Prop :=
|
|
600
|
match k with
|
|
601
|
| 0 => fun p => True
|
|
602
|
| S k' => fun p =>
|
|
603
|
match p with
|
|
604
|
| List.nil => True
|
|
605
|
| List.cons t q =>
|
|
606
|
match q with
|
|
607
|
| List.nil => (I t)
|
|
608
|
| List.cons t' q' => (T t' t) /\ (prefix I T k' q)
|
|
609
|
end
|
|
610
|
end
|
|
611
|
end.
|
|
612
|
|
|
613
|
Theorem prefix_mono_k : forall {A} I T k (p : list A), prefix I T (S k) p -> prefix I T k p.
|
|
614
|
Proof.
|
|
615
|
induction k.
|
|
616
|
simpl.
|
|
617
|
trivial.
|
|
618
|
|
|
619
|
simpl.
|
|
620
|
intuition.
|
|
621
|
destruct p.
|
|
622
|
trivial.
|
|
623
|
|
|
624
|
intuition.
|
|
625
|
destruct p.
|
|
626
|
intuition.
|
|
627
|
|
|
628
|
intuition.
|
|
629
|
Qed.
|
|
630
|
|
|
631
|
Theorem prefix_apply : forall {A} (I I' : A -> Prop) (T T' : A -> A -> Prop) k (p : list A),
|
|
632
|
prefix I T k p -> prefix (fun s => I s -> I' s) (fun s s' => T s s' -> T' s s') k p -> prefix I' T' k p.
|
|
633
|
Proof.
|
|
634
|
intros A I I' T T'.
|
|
635
|
induction k.
|
|
636
|
trivial.
|
|
637
|
|
|
638
|
simpl.
|
|
639
|
destruct p.
|
|
640
|
trivial.
|
|
641
|
|
|
642
|
destruct p.
|
|
643
|
intuition.
|
|
644
|
|
|
645
|
intuition.
|
|
646
|
Qed.
|
|
647
|
|
|
648
|
Theorem kinduction : forall {A} (P : A -> Prop) k (s : Stream A),
|
|
649
|
ForAll (fun s' => prefix (fun st => P st) (fun st st' => P st') k (fst (hd s')) -> P (snd (hd s'))) (history s)
|
|
650
|
-> ForAll (fun s' => P (hd s')) s.
|
|
651
|
Proof.
|
|
652
|
intros.
|
|
653
|
apply inv_snd_history_elim.
|
|
654
|
apply @ForAll_apply with (P := fun s' => P (snd (hd s'))).
|
|
655
|
apply
|
|
656
|
@ForAll_apply
|
|
657
|
with
|
|
658
|
(P := fun s' =>
|
|
659
|
prefix (fun st => P st) (fun st st' => P st') k (fst (hd s'))).
|
|
660
|
apply
|
|
661
|
@ForAll_reinforce
|
|
662
|
with
|
|
663
|
(P := ForAll
|
|
664
|
(fun s' : Stream (list A * A) =>
|
|
665
|
prefix (fun st : A => P st) (fun _ st' : A => P st') k
|
|
666
|
(fst (hd s')) -> P (snd (hd s')))).
|
|
667
|
apply
|
|
668
|
@ForAll_reinforce
|
|
669
|
with (P := ForAll (fun s' : Stream (list A * A) => History_Spec s s')).
|
|
670
|
eapply ForAll_coind.
|
|
671
|
intro.
|
|
672
|
exact (fun x => x).
|
|
673
|
|
|
674
|
destruct x as ((p0, s0), ((p1, s1), x'')).
|
|
675
|
simpl.
|
|
676
|
intuition.
|
|
677
|
inversion H1.
|
|
678
|
assumption.
|
|
679
|
|
|
680
|
inversion H0.
|
|
681
|
assumption.
|
|
682
|
|
|
683
|
inversion H1.
|
|
684
|
unfold History_Spec in H2.
|
|
685
|
simpl in H2.
|
|
686
|
destruct H2.
|
|
687
|
rewrite H2.
|
|
688
|
destruct k.
|
|
689
|
simpl.
|
|
690
|
trivial.
|
|
691
|
|
|
692
|
simpl.
|
|
693
|
inversion H0.
|
|
694
|
simpl in H6.
|
|
695
|
destruct p0.
|
|
696
|
intuition.
|
|
697
|
|
|
698
|
split.
|
|
699
|
simpl in H3.
|
|
700
|
apply H6.
|
|
701
|
exact H3.
|
|
702
|
|
|
703
|
apply prefix_mono_k.
|
|
704
|
exact H3.
|
|
705
|
|
|
706
|
simpl.
|
|
707
|
intuition.
|
|
708
|
generalize (history_spec s).
|
|
709
|
intuition.
|
|
710
|
|
|
711
|
destruct s.
|
|
712
|
simpl.
|
|
713
|
destruct k.
|
|
714
|
simpl.
|
|
715
|
trivial.
|
|
716
|
|
|
717
|
simpl.
|
|
718
|
trivial.
|
|
719
|
|
|
720
|
exact H.
|
|
721
|
|
|
722
|
apply necessitation.
|
|
723
|
destruct s0.
|
|
724
|
simpl.
|
|
725
|
trivial.
|
|
726
|
Qed.
|
|
727
|
|
|
728
|
Theorem kinduction' : forall {A} (P : A -> Prop) k ps (s : Stream A),
|
|
729
|
fst (hd ps) = nil
|
|
730
|
-> ForAll (fun s' => History_Spec s s') ps
|
|
731
|
-> ForAll (fun s' => prefix (fun st => P st) (fun st st' => P st') k (fst (hd s')) -> P (snd (hd s'))) ps
|
|
732
|
-> ForAll (fun s' => P (hd s')) s.
|
|
733
|
Proof.
|
|
734
|
intros.
|
|
735
|
rewrite (eqst_eq _ _ (history_spec_complete _ _ H H0)) in H1.
|
|
736
|
eapply kinduction.
|
|
737
|
apply H1.
|
|
738
|
Qed.
|
|
739
|
|
|
740
|
Theorem inv_prefix_history_rec : forall {A} (I : A -> Prop) (T : A -> A -> Prop) p (s : Stream A),
|
|
741
|
ForAll (fun s' => T (hd s') (hd (tl s'))) (concat p s) ->
|
|
742
|
forall k,
|
|
743
|
prefix I T k (cons (hd s) p) ->
|
|
744
|
ForAll (fun s' => prefix I T k (cons (snd (hd s')) (fst (hd s')))) (history_rec p s).
|
|
745
|
Proof.
|
|
746
|
intros A I T.
|
|
747
|
cofix proof.
|
|
748
|
intros.
|
|
749
|
inversion H.
|
|
750
|
destruct s as (s0, s').
|
|
751
|
apply HereAndFurther.
|
|
752
|
assumption.
|
|
753
|
|
|
754
|
simpl.
|
|
755
|
apply proof.
|
|
756
|
assumption.
|
|
757
|
|
|
758
|
destruct k; simpl.
|
|
759
|
trivial.
|
|
760
|
|
|
761
|
split.
|
|
762
|
generalize (inv_concat _ _ _ H).
|
|
763
|
clear H; intro H.
|
|
764
|
inversion H.
|
|
765
|
assumption.
|
|
766
|
|
|
767
|
apply prefix_mono_k.
|
|
768
|
assumption.
|
|
769
|
Qed.
|
|
770
|
|
|
771
|
Theorem inv_prefix_history : forall {A} (I : A -> Prop) (T : A -> A -> Prop) (s : Stream A),
|
|
772
|
I (hd s) -> ForAll (fun s' => T (hd s') (hd (tl s'))) s ->
|
|
773
|
forall k,
|
|
774
|
ForAll (fun s' => prefix I T k (cons (snd (hd s')) (fst (hd s')))) (history s).
|
|
775
|
Proof.
|
|
776
|
intros.
|
|
777
|
apply inv_prefix_history_rec.
|
|
778
|
assumption.
|
|
779
|
|
|
780
|
destruct k; simpl.
|
|
781
|
trivial.
|
|
782
|
|
|
783
|
assumption.
|
|
784
|
Qed.
|
|
785
|
|
|
786
|
Theorem inv_prefix_history' : forall {A} (I : A -> Prop) (T : A -> A -> Prop) (s : Stream A),
|
|
787
|
I (hd s) -> ForAll (fun s' => T (hd s') (hd (tl s'))) s ->
|
|
788
|
forall k,
|
|
789
|
ForAll (fun s' => prefix I T k (fst (hd s'))) (history s).
|
|
790
|
Proof.
|
|
791
|
intros.
|
|
792
|
destruct k.
|
|
793
|
apply necessitation.
|
|
794
|
simpl.
|
|
795
|
trivial.
|
|
796
|
|
|
797
|
eapply ForAll_apply.
|
|
798
|
apply (fun i n => inv_prefix_history I T s i n (S (S k))).
|
|
799
|
apply H.
|
|
800
|
|
|
801
|
apply H0.
|
|
802
|
|
|
803
|
apply necessitation.
|
|
804
|
destruct s0 as ((p0, s0), s').
|
|
805
|
simpl.
|
|
806
|
destruct p0.
|
|
807
|
trivial.
|
|
808
|
|
|
809
|
intuition.
|
|
810
|
Qed.
|
|
811
|
|
|
812
|
|
|
813
|
Definition effective {A : Type} (r : relation A) :=
|
|
814
|
forall a1 a2, { r a1 a2 } + { ~ r a1 a2 }.
|
|
815
|
|
|
816
|
Definition lift_hd {A : Type} (r : relation A) : relation (Stream A) :=
|
|
817
|
fun s1 => fun s2 => r (hd s1) (hd s2).
|
|
818
|
|
|
819
|
Theorem lift_hd_effective : forall {A : Type} {r : relation A},
|
|
820
|
effective r -> effective (lift_hd r).
|
|
821
|
Proof.
|
|
822
|
unfold effective, lift_hd in |- *.
|
|
823
|
intros A r H s1 s2.
|
|
824
|
destruct s1; destruct s2.
|
|
825
|
apply H.
|
|
826
|
Defined.
|
|
827
|
|
|
828
|
Section FixedPoint.
|
|
829
|
|
|
830
|
Variable A : Type.
|
|
831
|
|
|
832
|
Variable union : A -> A -> A.
|
|
833
|
|
|
834
|
Variable le : relation A.
|
|
835
|
|
|
836
|
Hypothesis le_mono : forall x y, le x (union x y).
|
|
837
|
|
|
838
|
Hypothesis le_eff : effective le.
|
|
839
|
|
|
840
|
Definition gt x y := le y x /\ ~ le x y.
|
|
841
|
|
|
842
|
Hypothesis gt_wf : well_founded gt.
|
|
843
|
|
|
844
|
Program Fixpoint rec_hd (f : Stream A -> Stream A) (s : Stream A) { wf (lift_hd gt) s } : Stream A :=
|
|
845
|
let s' := apply (apply (lift union) s) (f s) in
|
|
846
|
if (lift_hd_effective le_eff s' s)
|
|
847
|
then s'
|
|
848
|
else rec_hd f s'.
|
|
849
|
|
|
850
|
Obligation 1.
|
|
851
|
Proof.
|
|
852
|
unfold lift_hd.
|
|
853
|
rewrite hd_apply.
|
|
854
|
rewrite hd_apply.
|
|
855
|
rewrite hd_lift.
|
|
856
|
unfold gt.
|
|
857
|
split.
|
|
858
|
apply le_mono.
|
|
859
|
|
|
860
|
unfold lift_hd in H.
|
|
861
|
rewrite hd_apply in H.
|
|
862
|
rewrite hd_apply in H.
|
|
863
|
rewrite hd_lift in H.
|
|
864
|
exact H.
|
|
865
|
Qed.
|
|
866
|
|
|
867
|
Obligation 2.
|
|
868
|
Proof.
|
|
869
|
unfold MR.
|
|
870
|
apply wf_inverse_image.
|
|
871
|
unfold lift_hd.
|
|
872
|
apply wf_inverse_image.
|
|
873
|
assumption.
|
|
874
|
Defined.
|
|
875
|
|
|
876
|
CoFixpoint rec (f : Stream A -> Stream A) (s : Stream A) : Stream A :=
|
|
877
|
let s' := rec_hd f s in Cons (hd s') (rec f (tl s')).
|
|
878
|
|
|
879
|
End FixedPoint.
|
|
880
|
|
|
881
|
Arguments gt {A} _ _ _.
|
|
882
|
|
|
883
|
Arguments rec {A} _ _ _ _ _ _ _.
|