|
1
|
Definition mapT (F : Type -> Type) {A B} := (A -> B) -> (F A) -> (F B).
|
|
2
|
|
|
3
|
Definition applyT (F : Type -> Type) {A B} := (F (A -> B)) -> (F A) -> (F B).
|
|
4
|
|
|
5
|
Definition option_apply {A B} : @applyT option A B :=
|
|
6
|
fun f a =>
|
|
7
|
match f, a with
|
|
8
|
| Some f, Some a => Some (f a)
|
|
9
|
| _ , _ => None
|
|
10
|
end.
|
|
11
|
|
|
12
|
Require Import Streams.
|
|
13
|
Require List.
|
|
14
|
Require Import Setoid.
|
|
15
|
|
|
16
|
Axiom eqst_eq : forall {A} (s s' : Stream A), EqSt s s' -> s = s'.
|
|
17
|
|
|
18
|
Theorem inv_inv : forall {A} (P : Stream A -> Prop) (s : Stream A), ForAll P s -> ForAll (fun s' => ForAll P s') s.
|
|
19
|
Proof.
|
|
20
|
intros A P.
|
|
21
|
cofix proof.
|
|
22
|
destruct s as (s0, s').
|
|
23
|
intro H.
|
|
24
|
apply HereAndFurther.
|
|
25
|
exact H.
|
|
26
|
|
|
27
|
simpl.
|
|
28
|
apply proof.
|
|
29
|
inversion H.
|
|
30
|
assumption.
|
|
31
|
Qed.
|
|
32
|
|
|
33
|
Theorem evt_inv : forall {A} (P Q : Stream A -> Prop) (s : Stream A),
|
|
34
|
ForAll P s -> Exists Q s -> Exists (fun s' => P s' /\ Q s') s.
|
|
35
|
Proof.
|
|
36
|
induction 2.
|
|
37
|
apply Here.
|
|
38
|
inversion H.
|
|
39
|
intuition.
|
|
40
|
|
|
41
|
apply Further.
|
|
42
|
apply IHExists.
|
|
43
|
inversion H.
|
|
44
|
assumption.
|
|
45
|
Qed.
|
|
46
|
|
|
47
|
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) :=
|
|
48
|
fun s always_p always_pq =>
|
|
49
|
match always_p, always_pq with
|
|
50
|
| (HereAndFurther p_s always_p'), (HereAndFurther pq_s always_pq') => HereAndFurther s (pq_s p_s) (ForAll_apply (tl s) always_p' always_pq')
|
|
51
|
end.
|
|
52
|
|
|
53
|
CoFixpoint necessitation {A} {P : Stream A -> Prop} (I : forall s, P s) s : ForAll P s :=
|
|
54
|
HereAndFurther s (I s) (necessitation I (tl s)).
|
|
55
|
|
|
56
|
Definition concat {A} (prefix : list A) (suffix : Stream A) : Stream A :=
|
|
57
|
List.fold_left (fun q t => Cons t q) prefix suffix.
|
|
58
|
|
|
59
|
Theorem eqst_concat : forall {A} pfx (sfx sfx' : Stream A), EqSt sfx sfx' -> EqSt (concat pfx sfx) (concat pfx sfx').
|
|
60
|
Proof.
|
|
61
|
induction pfx.
|
|
62
|
auto.
|
|
63
|
|
|
64
|
simpl.
|
|
65
|
intros.
|
|
66
|
apply IHpfx.
|
|
67
|
apply eqst.
|
|
68
|
reflexivity.
|
|
69
|
|
|
70
|
exact H.
|
|
71
|
Qed.
|
|
72
|
|
|
73
|
Theorem evt_id : forall {A} (s : Stream A), Exists (fun s' => s = s') s.
|
|
74
|
Proof.
|
|
75
|
intros.
|
|
76
|
apply Here.
|
|
77
|
reflexivity.
|
|
78
|
Qed.
|
|
79
|
|
|
80
|
Theorem evt_concat : forall {A} (P : Stream A -> Prop) p (s : Stream A), Exists P s -> Exists P (concat p s).
|
|
81
|
Proof.
|
|
82
|
induction p.
|
|
83
|
trivial.
|
|
84
|
|
|
85
|
intros s H.
|
|
86
|
apply (IHp (Cons a s)).
|
|
87
|
apply Further.
|
|
88
|
exact H.
|
|
89
|
Qed.
|
|
90
|
|
|
91
|
Theorem inv_concat : forall {A} (P : Stream A -> Prop) p (s : Stream A), ForAll P (concat p s) -> ForAll P s.
|
|
92
|
Proof.
|
|
93
|
induction p.
|
|
94
|
trivial.
|
|
95
|
|
|
96
|
simpl.
|
|
97
|
intros s H.
|
|
98
|
generalize (IHp (Cons a s) H).
|
|
99
|
intro H'.
|
|
100
|
inversion H'.
|
|
101
|
assumption.
|
|
102
|
Qed.
|
|
103
|
|
|
104
|
|
|
105
|
CoFixpoint lift {A} (v : A) := Cons v (lift v).
|
|
106
|
|
|
107
|
Lemma hd_lift : forall {A} {v : A}, hd (lift v) = v.
|
|
108
|
Proof.
|
|
109
|
reflexivity.
|
|
110
|
Qed.
|
|
111
|
|
|
112
|
Lemma tl_lift : forall {A} {v : A}, tl (lift v) = lift v.
|
|
113
|
Proof.
|
|
114
|
reflexivity.
|
|
115
|
Qed.
|
|
116
|
|
|
117
|
CoFixpoint apply {A B} : @applyT Stream A B :=
|
|
118
|
fun f a =>
|
|
119
|
match f, a with
|
|
120
|
| (Cons f0 f'), (Cons a0 a') => Cons (f0 a0) (apply f' a')
|
|
121
|
end.
|
|
122
|
|
|
123
|
Lemma hd_apply : forall {A B} {f : Stream (A -> B)} {a : Stream A}, hd (apply f a) = (hd f) (hd a).
|
|
124
|
Proof.
|
|
125
|
destruct f; destruct a.
|
|
126
|
reflexivity.
|
|
127
|
Qed.
|
|
128
|
|
|
129
|
Lemma tl_apply : forall {A B} {f : Stream (A -> B)} {a : Stream A}, tl (apply f a) = apply (tl f) (tl a).
|
|
130
|
Proof.
|
|
131
|
destruct f; destruct a.
|
|
132
|
reflexivity.
|
|
133
|
Qed.
|
|
134
|
|
|
135
|
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')).
|
|
136
|
Proof.
|
|
137
|
intros.
|
|
138
|
apply eqst.
|
|
139
|
reflexivity.
|
|
140
|
|
|
141
|
apply EqSt_reflex.
|
|
142
|
Qed.
|
|
143
|
|
|
144
|
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.
|
|
145
|
Proof.
|
|
146
|
intros A B f P.
|
|
147
|
cofix proof.
|
|
148
|
destruct s as (s0, s').
|
|
149
|
intro H.
|
|
150
|
inversion H.
|
|
151
|
apply HereAndFurther.
|
|
152
|
assumption.
|
|
153
|
|
|
154
|
simpl.
|
|
155
|
apply proof.
|
|
156
|
assumption.
|
|
157
|
Qed.
|
|
158
|
|
|
159
|
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).
|
|
160
|
Proof.
|
|
161
|
intros A B f P.
|
|
162
|
cofix proof.
|
|
163
|
destruct s as (s0, s').
|
|
164
|
intro H.
|
|
165
|
inversion H.
|
|
166
|
apply HereAndFurther.
|
|
167
|
assumption.
|
|
168
|
|
|
169
|
simpl.
|
|
170
|
apply proof.
|
|
171
|
assumption.
|
|
172
|
Qed.
|
|
173
|
|
|
174
|
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.
|
|
175
|
Proof.
|
|
176
|
intros A B f P s.
|
|
177
|
remember (apply (lift f) s) as ss.
|
|
178
|
intro H.
|
|
179
|
revert s Heqss.
|
|
180
|
induction H.
|
|
181
|
intros.
|
|
182
|
apply Here.
|
|
183
|
rewrite <- Heqss.
|
|
184
|
exact H.
|
|
185
|
|
|
186
|
intros.
|
|
187
|
apply Further.
|
|
188
|
apply (IHExists (tl s)).
|
|
189
|
rewrite <- tl_lift.
|
|
190
|
rewrite <- tl_apply.
|
|
191
|
apply f_equal.
|
|
192
|
exact Heqss.
|
|
193
|
Qed.
|
|
194
|
|
|
195
|
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).
|
|
196
|
Proof.
|
|
197
|
intros A B f P s.
|
|
198
|
intro H.
|
|
199
|
induction H.
|
|
200
|
apply Here.
|
|
201
|
exact H.
|
|
202
|
|
|
203
|
apply Further.
|
|
204
|
rewrite tl_apply.
|
|
205
|
rewrite tl_lift.
|
|
206
|
exact IHExists.
|
|
207
|
Qed.
|
|
208
|
|
|
209
|
Definition zip {A B} (s : Stream A * Stream B) := apply (apply (lift (fun a b => (a, b))) (fst s)) (snd s).
|
|
210
|
|
|
211
|
Lemma zip_fst_eqst : forall {A B}, forall (s1 s1' : Stream A) (s2 s2' : Stream B),
|
|
212
|
EqSt (zip (s1, s2)) (zip (s1', s2')) -> EqSt s1 s1'.
|
|
213
|
Proof.
|
|
214
|
intros A B.
|
|
215
|
cofix proof.
|
|
216
|
destruct s1; destruct s1'; destruct s2; destruct s2'.
|
|
217
|
intro.
|
|
218
|
inversion H.
|
|
219
|
apply eqst.
|
|
220
|
simpl in H0.
|
|
221
|
simpl in H1.
|
|
222
|
injection H0.
|
|
223
|
intros.
|
|
224
|
subst.
|
|
225
|
reflexivity.
|
|
226
|
|
|
227
|
eapply proof.
|
|
228
|
apply H1.
|
|
229
|
Qed.
|
|
230
|
|
|
231
|
Lemma zip_fst : forall {A B}, forall (s1 s1' : Stream A) (s2 s2' : Stream B),
|
|
232
|
zip (s1, s2) = zip (s1', s2') -> s1 = s1'.
|
|
233
|
Proof.
|
|
234
|
intros.
|
|
235
|
apply eqst_eq.
|
|
236
|
apply (zip_fst_eqst s1 s1' s2 s2').
|
|
237
|
rewrite H.
|
|
238
|
apply EqSt_reflex.
|
|
239
|
Qed.
|
|
240
|
|
|
241
|
Lemma zip_snd_eqst : forall {A B}, forall (s1 s1' : Stream A) (s2 s2' : Stream B),
|
|
242
|
EqSt (zip (s1, s2)) (zip (s1', s2')) -> EqSt s2 s2'.
|
|
243
|
Proof.
|
|
244
|
intros A B.
|
|
245
|
cofix proof.
|
|
246
|
destruct s1; destruct s1'; destruct s2; destruct s2'.
|
|
247
|
intro.
|
|
248
|
inversion H.
|
|
249
|
apply eqst.
|
|
250
|
simpl in H0.
|
|
251
|
simpl in H1.
|
|
252
|
injection H0.
|
|
253
|
intros.
|
|
254
|
subst.
|
|
255
|
reflexivity.
|
|
256
|
|
|
257
|
eapply proof.
|
|
258
|
apply H1.
|
|
259
|
Qed.
|
|
260
|
|
|
261
|
Lemma zip_snd : forall {A B}, forall (s1 s1' : Stream A) (s2 s2' : Stream B),
|
|
262
|
zip (s1, s2) = zip (s1', s2') -> s2 = s2'.
|
|
263
|
Proof.
|
|
264
|
intros.
|
|
265
|
apply eqst_eq.
|
|
266
|
apply (zip_snd_eqst s1 s1' s2 s2').
|
|
267
|
rewrite H.
|
|
268
|
apply EqSt_reflex.
|
|
269
|
Qed.
|
|
270
|
|
|
271
|
Definition unzip {A B} (s : Stream (A*B)) := (apply (lift (@fst _ _)) s, apply (lift (@snd _ _)) s).
|
|
272
|
|
|
273
|
Lemma fst_zip_eqst : forall {A B} (s1 : Stream A) (s2 : Stream B), EqSt (apply (lift (@fst _ _)) (zip (s1, s2))) s1.
|
|
274
|
Proof.
|
|
275
|
intros A B.
|
|
276
|
cofix proof.
|
|
277
|
destruct s1; destruct s2.
|
|
278
|
apply eqst.
|
|
279
|
reflexivity.
|
|
280
|
|
|
281
|
apply proof.
|
|
282
|
Qed.
|
|
283
|
|
|
284
|
Lemma fst_zip : forall {A B} (s1 : Stream A) (s2 : Stream B), apply (lift (@fst _ _)) (zip (s1, s2)) = s1.
|
|
285
|
Proof.
|
|
286
|
intros.
|
|
287
|
apply eqst_eq.
|
|
288
|
apply fst_zip_eqst.
|
|
289
|
Qed.
|
|
290
|
|
|
291
|
Lemma snd_zip_eqst : forall {A B} (s1 : Stream A) (s2 : Stream B), EqSt (apply (lift (@snd _ _)) (zip (s1, s2))) s2.
|
|
292
|
Proof.
|
|
293
|
intros A B.
|
|
294
|
cofix proof.
|
|
295
|
destruct s1; destruct s2.
|
|
296
|
apply eqst.
|
|
297
|
reflexivity.
|
|
298
|
|
|
299
|
apply proof.
|
|
300
|
Qed.
|
|
301
|
|
|
302
|
Lemma snd_zip : forall {A B} (s1 : Stream A) (s2 : Stream B), apply (lift (@snd _ _)) (zip (s1, s2)) = s2.
|
|
303
|
Proof.
|
|
304
|
intros.
|
|
305
|
apply eqst_eq.
|
|
306
|
apply snd_zip_eqst.
|
|
307
|
Qed.
|
|
308
|
|
|
309
|
Lemma zip_unzip_eqst : forall {A B} (s : Stream (A*B)), EqSt (zip (unzip s)) s.
|
|
310
|
Proof.
|
|
311
|
intros A B.
|
|
312
|
cofix proof.
|
|
313
|
destruct s.
|
|
314
|
apply eqst.
|
|
315
|
simpl.
|
|
316
|
destruct p.
|
|
317
|
reflexivity.
|
|
318
|
|
|
319
|
simpl.
|
|
320
|
apply proof.
|
|
321
|
Qed.
|
|
322
|
|
|
323
|
Lemma zip_unzip : forall {A B} (s : Stream (A*B)), zip (unzip s) = s.
|
|
324
|
Proof.
|
|
325
|
intros.
|
|
326
|
apply eqst_eq.
|
|
327
|
apply zip_unzip_eqst.
|
|
328
|
Qed.
|
|
329
|
|
|
330
|
(*
|
|
331
|
CoInductive transition {A} (T : A -> A -> Prop) : Stream A -> Prop :=
|
|
332
|
| Tick : forall a0 a1 s'', T a0 a1 -> transition T (Cons a1 s'') -> transition T (Cons a0 (Cons a1 s'')).
|
|
333
|
|
|
334
|
Fixpoint prefix {A} (I : A -> Prop) (T : A -> A -> Prop) (k : nat) : Stream A -> Prop :=
|
|
335
|
match k with
|
|
336
|
| 0 => fun s => True
|
|
337
|
| S k' => fun s => (I (hd s) \/ (T (hd s) (hd (tl s)) /\ prefix I T k' (tl s)))
|
|
338
|
end.
|
|
339
|
|
|
340
|
Lemma I_prefix : forall {A} (I : A -> Prop) (T : A -> A -> Prop) k (s : Stream A), I (hd s) -> prefix I T k s.
|
|
341
|
Proof.
|
|
342
|
destruct k.
|
|
343
|
simpl.
|
|
344
|
trivial.
|
|
345
|
|
|
346
|
simpl.
|
|
347
|
left.
|
|
348
|
trivial.
|
|
349
|
Qed.
|
|
350
|
|
|
351
|
Lemma T_prefix : forall {A} (I : A -> Prop) (T : A -> A -> Prop) k (s : Stream A), T (hd s) (hd (tl s)) -> prefix I T k (tl s) -> prefix I T k s.
|
|
352
|
Proof.
|
|
353
|
destruct k.
|
|
354
|
simpl.
|
|
355
|
trivial.
|
|
356
|
|
|
357
|
simpl.
|
|
358
|
right.
|
|
359
|
trivial.
|
|
360
|
Qed.
|
|
361
|
|
|
362
|
Lemma prefix_mono_k : forall {A} I T k (s : Stream A), prefix I T (S k) s -> prefix I T k s.
|
|
363
|
Proof.
|
|
364
|
|
|
365
|
Qed.
|
|
366
|
*)
|
|
367
|
|
|
368
|
CoFixpoint history_rec {A} (past : list A) (s : Stream A) : Stream (list A * A) :=
|
|
369
|
match s with
|
|
370
|
| Cons s0 s' => Cons (past, s0) (history_rec (cons s0 past) s')
|
|
371
|
end.
|
|
372
|
|
|
373
|
Definition history {A} (s : Stream A) : Stream (list A * A) := history_rec nil s.
|
|
374
|
|
|
375
|
Theorem eqst_history_rec : forall {A} (pfx : list A) (sfx sfx' : Stream A),
|
|
376
|
EqSt sfx sfx' -> EqSt (history_rec pfx sfx) (history_rec pfx sfx').
|
|
377
|
Proof.
|
|
378
|
intros A.
|
|
379
|
cofix proof.
|
|
380
|
destruct sfx as (sfx0, sfxq).
|
|
381
|
destruct sfx' as (sfx0', sfxq').
|
|
382
|
intro H.
|
|
383
|
inversion H.
|
|
384
|
simpl in H0.
|
|
385
|
rewrite H0.
|
|
386
|
apply eqst.
|
|
387
|
reflexivity.
|
|
388
|
|
|
389
|
apply (proof _ sfxq sfxq').
|
|
390
|
assumption.
|
|
391
|
Qed.
|
|
392
|
|
|
393
|
Theorem eqst_history : forall {A} (sfx sfx' : Stream A),
|
|
394
|
EqSt sfx sfx' -> EqSt (history sfx) (history sfx').
|
|
395
|
Proof.
|
|
396
|
intros.
|
|
397
|
apply eqst_history_rec.
|
|
398
|
assumption.
|
|
399
|
Qed.
|
|
400
|
|
|
401
|
Theorem unzip_history_rec : forall {A} (pfx : list A) (sfx : Stream A), EqSt (snd (unzip (history_rec pfx sfx))) sfx.
|
|
402
|
Proof.
|
|
403
|
intro A.
|
|
404
|
cofix proof.
|
|
405
|
destruct sfx as (sfx0, sfx').
|
|
406
|
apply eqst.
|
|
407
|
reflexivity.
|
|
408
|
|
|
409
|
apply proof.
|
|
410
|
Qed.
|
|
411
|
|
|
412
|
Theorem unzip_history : forall {A} (s : Stream A), EqSt (snd (unzip (history s))) s.
|
|
413
|
Proof.
|
|
414
|
unfold history.
|
|
415
|
intros.
|
|
416
|
apply unzip_history_rec.
|
|
417
|
Qed.
|
|
418
|
|
|
419
|
Theorem hd_history_rec : forall {A} p (s : Stream A), hd (history_rec p s) = (p, hd s).
|
|
420
|
Proof.
|
|
421
|
destruct s.
|
|
422
|
reflexivity.
|
|
423
|
Qed.
|
|
424
|
|
|
425
|
Theorem hd_history : forall {A} (s : Stream A), hd (history s) = (nil, hd s).
|
|
426
|
Proof.
|
|
427
|
destruct s.
|
|
428
|
reflexivity.
|
|
429
|
Qed.
|
|
430
|
|
|
431
|
Definition snoc {A} (a : A) (l : list A) := app l (cons a nil).
|
|
432
|
|
|
433
|
Theorem tl_history_rec : forall {A} p (s : Stream A), tl (history_rec p s) = history_rec (cons (hd s) p) (tl s).
|
|
434
|
Proof.
|
|
435
|
intros.
|
|
436
|
destruct s.
|
|
437
|
reflexivity.
|
|
438
|
Qed.
|
|
439
|
|
|
440
|
Theorem tl_history_rec : forall {A} p (s : Stream A), EqSt (tl (history_rec p s)) (apply (lift (fun pfx_sfx => (app (fst pfx_sfx) (cons (hd s) p), (snd pfx_sfx)))) (history_rec p (tl s))).
|
|
441
|
Proof.
|
|
442
|
intros.
|
|
443
|
Qed.
|
|
444
|
|
|
445
|
Theorem tl_history : forall {A} (s : Stream A), EqSt (tl (history s)) (apply (lift (fun pfx_sfx => (snoc (hd s) (fst pfx_sfx), (snd pfx_sfx)))) (history (tl s))).
|
|
446
|
Proof.
|
|
447
|
intros.
|
|
448
|
Qed.
|
|
449
|
|
|
450
|
CoFixpoint cojoin {A} (s : Stream A) : Stream (Stream A) :=
|
|
451
|
match s with
|
|
452
|
| Cons _ s' => Cons s (cojoin s')
|
|
453
|
end.
|
|
454
|
(*
|
|
455
|
Theorem eqst_cojoin : forall {A} (s s' : Stream A), EqSt s s' -> EqSt (cojoin s) (cojoin s').
|
|
456
|
Proof.
|
|
457
|
|
|
458
|
intros A.
|
|
459
|
cofix proof.
|
|
460
|
destruct s as (s0, sq).
|
|
461
|
destruct s' as (s0', sq').
|
|
462
|
intro H.
|
|
463
|
inversion H.
|
|
464
|
simpl in H0.
|
|
465
|
rewrite H0.
|
|
466
|
Qed.
|
|
467
|
|
|
468
|
Theorem inv_history_rec : forall {A} p (s : Stream A),
|
|
469
|
let (fst_s, snd_s) := unzip (history_rec p s) in ForAll (fun s' => EqSt (hd s') (concat p s)) (apply (apply (lift concat) fst_s) (cojoin snd_s)).
|
|
470
|
Proof.
|
|
471
|
intro A.
|
|
472
|
cofix proof.
|
|
473
|
destruct s as (s0, s').
|
|
474
|
apply HereAndFurther.
|
|
475
|
apply eqst_concat.
|
|
476
|
apply unzip_history_rec.
|
|
477
|
|
|
478
|
apply (proof (cons s0 p) s').
|
|
479
|
Qed.
|
|
480
|
|
|
481
|
Theorem inv_history : forall {A} (s : Stream A),
|
|
482
|
let (fst_s, snd_s) := unzip (history s) in ForAll (fun s' => EqSt (hd s') s) (apply (apply (lift concat) fst_s) (cojoin snd_s)).
|
|
483
|
Proof.
|
|
484
|
intros.
|
|
485
|
apply inv_history_rec.
|
|
486
|
Qed.
|
|
487
|
*)
|
|
488
|
|
|
489
|
Theorem inv_history_rec : forall {A} p (s : Stream A),
|
|
490
|
ForAll (fun s' => EqSt (concat (fst (hd s')) (apply (lift (@snd _ _)) s')) (concat p s)) (history_rec p s).
|
|
491
|
Proof.
|
|
492
|
intro A.
|
|
493
|
cofix proof.
|
|
494
|
destruct s as (s0, s').
|
|
495
|
apply HereAndFurther.
|
|
496
|
apply eqst_concat.
|
|
497
|
apply unzip_history_rec.
|
|
498
|
|
|
499
|
apply (proof (cons s0 p) s').
|
|
500
|
Qed.
|
|
501
|
|
|
502
|
Theorem inv_history : forall {A} (s : Stream A),
|
|
503
|
ForAll (fun s' => EqSt (concat (fst (hd s')) (apply (lift (@snd _ _)) s')) s) (history s).
|
|
504
|
Proof.
|
|
505
|
intros.
|
|
506
|
assert (s = concat nil s).
|
|
507
|
reflexivity.
|
|
508
|
|
|
509
|
rewrite H.
|
|
510
|
rewrite <- H in |- * at 1.
|
|
511
|
apply inv_history_rec.
|
|
512
|
Qed.
|
|
513
|
|
|
514
|
Theorem inv_mono_history_rec : forall {A} (P : Stream A -> Prop) p (s : Stream A),
|
|
515
|
ForAll P s -> ForAll (fun s' => P (apply (lift (@snd _ _)) s')) (history_rec p s).
|
|
516
|
Proof.
|
|
517
|
intros.
|
|
518
|
apply inv_map.
|
|
519
|
generalize (eqst_eq _ _ (unzip_history_rec p s)).
|
|
520
|
simpl.
|
|
521
|
intro Hs.
|
|
522
|
rewrite Hs.
|
|
523
|
exact H.
|
|
524
|
Qed.
|
|
525
|
|
|
526
|
Theorem inv_mono_history : forall {A} (P : Stream A -> Prop) (s : Stream A),
|
|
527
|
ForAll P s -> ForAll (fun s' => P (apply (lift (@snd _ _)) s')) (history s).
|
|
528
|
Proof.
|
|
529
|
intros.
|
|
530
|
apply inv_mono_history_rec.
|
|
531
|
assumption.
|
|
532
|
Qed.
|
|
533
|
|
|
534
|
Theorem history_rec_mono_inv : forall {A} (P : Stream A -> Prop) p (s : Stream A),
|
|
535
|
ForAll (fun s' => P (apply (lift (@snd _ _)) s')) (history_rec p s) -> ForAll P s.
|
|
536
|
Proof.
|
|
537
|
intros.
|
|
538
|
rewrite <- (eqst_eq _ _ (unzip_history_rec p s)).
|
|
539
|
apply map_inv.
|
|
540
|
exact H.
|
|
541
|
Qed.
|
|
542
|
|
|
543
|
Theorem history_mono_inv : forall {A} (P : Stream A -> Prop) (s : Stream A),
|
|
544
|
ForAll (fun s' => P (apply (lift (@snd _ _)) s')) (history s) -> ForAll P s.
|
|
545
|
Proof.
|
|
546
|
intros.
|
|
547
|
apply history_rec_mono_inv with (p := nil).
|
|
548
|
assumption.
|
|
549
|
Qed.
|
|
550
|
|
|
551
|
Fixpoint prefix {A} (I : A -> Prop) (T : A -> A -> Prop) (k : nat) : list A -> Prop :=
|
|
552
|
match k with
|
|
553
|
| 0 => fun p => True
|
|
554
|
| S k' => fun p =>
|
|
555
|
match p with
|
|
556
|
| List.nil => True
|
|
557
|
| List.cons t q =>
|
|
558
|
match q with
|
|
559
|
| List.nil => (I t)
|
|
560
|
| List.cons t' q' => (T t' t) /\ (prefix I T k' q)
|
|
561
|
end
|
|
562
|
end
|
|
563
|
end.
|
|
564
|
|
|
565
|
Theorem prefix_mono_k : forall {A} I T k (p : list A), prefix I T (S k) p -> prefix I T k p.
|
|
566
|
Proof.
|
|
567
|
induction k.
|
|
568
|
simpl.
|
|
569
|
trivial.
|
|
570
|
|
|
571
|
simpl.
|
|
572
|
intuition.
|
|
573
|
destruct p.
|
|
574
|
trivial.
|
|
575
|
|
|
576
|
intuition.
|
|
577
|
destruct p.
|
|
578
|
intuition.
|
|
579
|
|
|
580
|
intuition.
|
|
581
|
Qed.
|
|
582
|
|
|
583
|
Theorem prefix_mono : forall {A} (I I' : A -> Prop) (T T' : A -> A -> Prop) k (p : list A), (forall s, I s -> I' s) -> (forall s s', T s s' -> T' s s') -> prefix I T k p -> prefix I' T' k p.
|
|
584
|
Proof.
|
|
585
|
induction k.
|
|
586
|
trivial.
|
|
587
|
|
|
588
|
simpl.
|
|
589
|
destruct p.
|
|
590
|
trivial.
|
|
591
|
|
|
592
|
intros.
|
|
593
|
destruct p.
|
|
594
|
intuition.
|
|
595
|
|
|
596
|
intuition.
|
|
597
|
Qed.
|
|
598
|
|
|
599
|
Theorem kinduction : forall {A} (P : A -> Prop) k (s : Stream A),
|
|
600
|
ForAll (fun s' => prefix (fun st => P st) (fun st st' => P st') k (fst (hd s')) -> P (snd (hd s'))) (history s)
|
|
601
|
-> ForAll (fun s' => P (hd s')) s.
|
|
602
|
Proof.
|
|
603
|
induction k.
|
|
604
|
simpl.
|
|
605
|
intros.
|
|
606
|
apply history_mono_inv.
|
|
607
|
eapply ForAll_apply.
|
|
608
|
apply H.
|
|
609
|
|
|
610
|
apply necessitation.
|
|
611
|
intros.
|
|
612
|
rewrite hd_apply.
|
|
613
|
rewrite hd_lift.
|
|
614
|
intuition.
|
|
615
|
|
|
616
|
intros.
|
|
617
|
apply IHk.
|
|
618
|
eapply ForAll_apply.
|
|
619
|
apply H.
|
|
620
|
|
|
621
|
apply necessitation.
|
|
622
|
intros.
|
|
623
|
apply H0.
|
|
624
|
simpl.
|
|
625
|
Qed.
|
|
626
|
|
|
627
|
Theorem inv_prefix_history_rec : forall {A} (I : A -> Prop) (T : A -> A -> Prop) (s : Stream A),
|
|
628
|
I (hd s) -> ForAll (fun s' => T (hd s') (hd (tl s'))) (concat p s) ->
|
|
629
|
forall k,
|
|
630
|
ForAll (fun s' => prefix I T k (fst (hd s'))) (history_rec p s).
|
|
631
|
Proof.
|
|
632
|
|
|
633
|
Qed.
|
|
634
|
|
|
635
|
Theorem inv_prefix_history : forall {A} (I : A -> Prop) (T : A -> A -> Prop) (s : Stream A),
|
|
636
|
I (hd s) -> ForAll (fun s' => T (hd s') (hd (tl s'))) s ->
|
|
637
|
forall k,
|
|
638
|
ForAll (fun s' => prefix I T k (fst (hd s'))) (history s).
|
|
639
|
Proof.
|
|
640
|
intros A I T.
|
|
641
|
cofix proof.
|
|
642
|
intros.
|
|
643
|
Qed.
|
|
644
|
|
|
645
|
|
|
646
|
Definition _arrow := Cons true (lift false).
|
|
647
|
|
|
648
|
Definition ite {A} (s_if : Stream bool) (s_then s_else : Stream A) :=
|
|
649
|
apply (apply (apply (lift (fun (c : bool) (t e : A) => if c then t else e)) s_if) s_then) s_else.
|
|
650
|
|
|
651
|
Lemma hd_ite : forall {A}, forall (c : Stream bool) (t e : Stream A),
|
|
652
|
hd (ite c t e) = if (hd c) then (hd t) else (hd e).
|
|
653
|
Proof.
|
|
654
|
destruct c; destruct t; destruct e.
|
|
655
|
reflexivity.
|
|
656
|
Qed.
|
|
657
|
|
|
658
|
Lemma tl_ite : forall {A}, forall (c : Stream bool) (t e : Stream A),
|
|
659
|
tl (ite c t e) = ite (tl c) (tl t) (tl e).
|
|
660
|
Proof.
|
|
661
|
destruct c; destruct t; destruct e.
|
|
662
|
reflexivity.
|
|
663
|
Qed.
|
|
664
|
|
|
665
|
Theorem eqst_ite : forall {A}, forall (c1 c2 : Stream bool) (t1 t2 e1 e2 : Stream A),
|
|
666
|
EqSt c1 c2 -> EqSt t1 t2 -> EqSt e1 e2 -> EqSt (ite c1 t1 e1) (ite c2 t2 e2).
|
|
667
|
Proof.
|
|
668
|
intros.
|
|
669
|
apply eqst_apply.
|
|
670
|
apply eqst_apply.
|
|
671
|
apply eqst_apply.
|
|
672
|
apply EqSt_reflex.
|
|
673
|
|
|
674
|
assumption.
|
|
675
|
|
|
676
|
assumption.
|
|
677
|
|
|
678
|
assumption.
|
|
679
|
Qed.
|
|
680
|
|
|
681
|
Variable pre : forall {A}, Stream A -> Stream A.
|
|
682
|
|
|
683
|
Axiom pre_spec : forall {A}, forall (s : Stream A), EqSt (tl (pre s)) s.
|
|
684
|
|
|
685
|
Variable when : forall {A}, Stream bool -> Stream A -> Stream A.
|
|
686
|
|
|
687
|
Axiom when_spec : forall {A}, forall (c : Stream bool) (s : Stream A), forall n, hd (Str_nth_tl n c) = true -> hd (Str_nth_tl n (when c s)) = hd (Str_nth_tl n s).
|
|
688
|
|
|
689
|
|
|
690
|
Require Import Bool.
|
|
691
|
|
|
692
|
Definition bnot (s : Stream bool) := apply (lift negb) s.
|
|
693
|
|
|
694
|
Definition band (s1 s2 : Stream bool) := apply (apply (lift andb) s1) s2.
|
|
695
|
|
|
696
|
Definition bor (s1 s2 : Stream bool) := apply (apply (lift orb) s1) s2.
|
|
697
|
|
|
698
|
Require Import ZArith.
|
|
699
|
|
|
700
|
Definition iplus (s1 s2 : Stream Z) := apply (apply (lift (fun i1 i2 => (i1 + i2)%Z)) s1) s2.
|
|
701
|
|
|
702
|
Definition iminus (s1 s2 : Stream Z) := apply (apply (lift (fun i1 i2 => (i1 - i2)%Z)) s1) s2.
|
|
703
|
|
|
704
|
Definition imult (s1 s2 : Stream Z) := apply (apply (lift (fun i1 i2 => (i1 * i2)%Z)) s1) s2.
|
|
705
|
|
|
706
|
Definition idiv (s1 s2 : Stream Z) := apply (apply (lift (fun i1 i2 => (i1 / i2)%Z)) s1) s2.
|
|
707
|
|
|
708
|
Definition imod (s1 s2 : Stream Z) := apply (apply (lift (fun i1 i2 => Zmod i1 i2)) s1) s2.
|
|
709
|
|
|
710
|
Definition ieq (s1 s2 : Stream Z) := apply (apply (lift (fun i1 i2 => match (i1 ?= i2)%Z with Eq => true | _ => false end)) s1) s2.
|
|
711
|
|
|
712
|
Definition ilt (s1 s2 : Stream Z) := apply (apply (lift (fun i1 i2 => match (i1 ?= i2)%Z with Lt => true | _ => false end)) s1) s2.
|
|
713
|
|
|
714
|
(* sémantique dénotationnelle de f *)
|
|
715
|
Definition denot_f (x cpt y : Stream Z) :=
|
|
716
|
(EqSt y (iplus x (lift 1%Z))) /\ (EqSt cpt (iplus (ite _arrow (lift 0%Z) (pre cpt)) (lift 1%Z))).
|
|
717
|
|
|
718
|
(* sémantique axiomatique de f, simplifiée *)
|
|
719
|
|
|
720
|
Definition mem_f := (bool * Z)%type.
|
|
721
|
|
|
722
|
Definition ni_2 (mem : mem_f) := fst mem.
|
|
723
|
|
|
724
|
Definition __f_2 (mem : mem_f) := snd mem.
|
|
725
|
|
|
726
|
Definition init_f (mem : mem_f) := ni_2 mem = true.
|
|
727
|
|
|
728
|
Definition trans_f (x cpt y : Z) (mem_in mem_out : mem_f) :=
|
|
729
|
(cpt = ((if bool_dec (ni_2 mem_in) true then 0 else (__f_2 mem_in)) + 1)%Z)
|
|
730
|
/\ (y = (x + 1)%Z)
|
|
731
|
/\ (ni_2 mem_out) = false
|
|
732
|
/\ (__f_2 mem_out) = cpt.
|
|
733
|
|
|
734
|
Definition trans_f' (s s' : (Z * (Z * Z)) * mem_f) :=
|
|
735
|
match s, s' with
|
|
736
|
| ((x, (cpt, y)), mem), ((x', (cpt', y')), mem') => trans_f x cpt y mem mem'
|
|
737
|
end.
|
|
738
|
|
|
739
|
Lemma Cons_inj : forall {A}, forall a a' (s s' : Stream A), Cons a s = Cons a' s' -> a = a' /\ s = s'.
|
|
740
|
Proof.
|
|
741
|
intros.
|
|
742
|
injection H.
|
|
743
|
intuition.
|
|
744
|
Qed.
|
|
745
|
|
|
746
|
Theorem raffinement : forall (x cpt y : Stream Z) (mem : Stream mem_f),
|
|
747
|
(init_f (hd mem) /\ transition trans_f' (zip ((zip (x, (zip (cpt, y)))), mem)))
|
|
748
|
->
|
|
749
|
denot_f x cpt y.
|
|
750
|
Proof.
|
|
751
|
intros.
|
|
752
|
apply zip_pair.
|
|
753
|
revert x cpt y mem H.
|
|
754
|
cofix proof.
|
|
755
|
intros.
|
|
756
|
|
|
757
|
|
|
758
|
|
|
759
|
intros.
|
|
760
|
split.
|
|
761
|
revert x cpt y mem H.
|
|
762
|
cofix proof.
|
|
763
|
intros.
|
|
764
|
destruct H.
|
|
765
|
destruct x as (x0, x'); destruct cpt as (cpt0, cpt'); destruct y as (y0, y').
|
|
766
|
destruct mem as (mem0, mem').
|
|
767
|
inversion H0.
|
|
768
|
apply eqst.
|
|
769
|
simpl.
|
|
770
|
unfold zip in H1.
|
|
771
|
simpl in H1.
|
|
772
|
generalize (f_equal (@hd _) H1).
|
|
773
|
simpl.
|
|
774
|
intro.
|
|
775
|
subst.
|
|
776
|
generalize (f_equal (@tl _) H1).
|
|
777
|
simpl.
|
|
778
|
|
|
779
|
Qed.
|
|
780
|
|
|
781
|
|