|
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
|
CoFixpoint lift {A} (v : A) := Cons v (lift v).
|
|
17
|
|
|
18
|
Lemma hd_lift : forall {A} {v : A}, hd (lift v) = v.
|
|
19
|
Proof.
|
|
20
|
reflexivity.
|
|
21
|
Qed.
|
|
22
|
|
|
23
|
Lemma tl_lift : forall {A} {v : A}, tl (lift v) = lift v.
|
|
24
|
Proof.
|
|
25
|
reflexivity.
|
|
26
|
Qed.
|
|
27
|
|
|
28
|
CoFixpoint apply {A B} : @applyT Stream A B :=
|
|
29
|
fun f a =>
|
|
30
|
match f, a with
|
|
31
|
| (Cons f0 f'), (Cons a0 a') => Cons (f0 a0) (apply f' a')
|
|
32
|
end.
|
|
33
|
|
|
34
|
Lemma hd_apply : forall {A B} {f : Stream (A -> B)} {a : Stream A}, hd (apply f a) = (hd f) (hd a).
|
|
35
|
Proof.
|
|
36
|
destruct f; destruct a.
|
|
37
|
reflexivity.
|
|
38
|
Qed.
|
|
39
|
|
|
40
|
Lemma tl_apply : forall {A B} {f : Stream (A -> B)} {a : Stream A}, tl (apply f a) = apply (tl f) (tl a).
|
|
41
|
Proof.
|
|
42
|
destruct f; destruct a.
|
|
43
|
reflexivity.
|
|
44
|
Qed.
|
|
45
|
|
|
46
|
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')).
|
|
47
|
Proof.
|
|
48
|
intros.
|
|
49
|
apply eqst.
|
|
50
|
reflexivity.
|
|
51
|
|
|
52
|
apply EqSt_reflex.
|
|
53
|
Qed.
|
|
54
|
|
|
55
|
Theorem eqst_apply : forall {A B}, forall (f1 f2 : Stream (A -> B)), forall (a1 a2 : Stream A),
|
|
56
|
EqSt f1 f2 -> EqSt a1 a2 -> EqSt (apply f1 a1) (apply f2 a2).
|
|
57
|
Proof.
|
|
58
|
intros A B.
|
|
59
|
cofix Hcoind.
|
|
60
|
destruct f1 as (vf1, f1').
|
|
61
|
destruct f2 as (vf2, f2').
|
|
62
|
destruct a1 as (va1, a1').
|
|
63
|
destruct a2 as (va2, a2').
|
|
64
|
intros Hf Ha.
|
|
65
|
destruct Hf.
|
|
66
|
destruct Ha.
|
|
67
|
apply eqst.
|
|
68
|
simpl.
|
|
69
|
simpl in H.
|
|
70
|
simpl in H0.
|
|
71
|
subst.
|
|
72
|
reflexivity.
|
|
73
|
|
|
74
|
apply Hcoind.
|
|
75
|
exact Hf.
|
|
76
|
|
|
77
|
exact Ha.
|
|
78
|
Qed.
|
|
79
|
|
|
80
|
Definition zip {A B} (s : Stream A * Stream B) := apply (apply (lift (fun a b => (a, b))) (fst s)) (snd s).
|
|
81
|
|
|
82
|
Lemma eqst_zip : forall {A B}, forall (s1 s1' : Stream A) (s2 s2' : Stream B),
|
|
83
|
EqSt s1 s1' -> EqSt s2 s2' -> EqSt (zip (s1, s2)) (zip (s1', s2')).
|
|
84
|
Proof.
|
|
85
|
intros A B.
|
|
86
|
cofix proof.
|
|
87
|
intros.
|
|
88
|
destruct s1; destruct s1'; destruct s2; destruct s2'.
|
|
89
|
apply eqst.
|
|
90
|
simpl.
|
|
91
|
inversion H.
|
|
92
|
inversion H0.
|
|
93
|
simpl in H1.
|
|
94
|
simpl in H3.
|
|
95
|
subst.
|
|
96
|
reflexivity.
|
|
97
|
|
|
98
|
apply proof.
|
|
99
|
inversion H.
|
|
100
|
exact H2.
|
|
101
|
|
|
102
|
inversion H0.
|
|
103
|
exact H2.
|
|
104
|
Qed.
|
|
105
|
|
|
106
|
|
|
107
|
Lemma zip_fst : forall {A B}, forall (s1 s1' : Stream A) (s2 s2' : Stream B),
|
|
108
|
EqSt (zip (s1, s2)) (zip (s1', s2')) -> EqSt s1 s1'.
|
|
109
|
Proof.
|
|
110
|
intros A B.
|
|
111
|
cofix proof.
|
|
112
|
destruct s1; destruct s1'; destruct s2; destruct s2'.
|
|
113
|
intro.
|
|
114
|
inversion H.
|
|
115
|
apply eqst.
|
|
116
|
simpl in H0.
|
|
117
|
simpl in H1.
|
|
118
|
injection H0.
|
|
119
|
intros.
|
|
120
|
subst.
|
|
121
|
reflexivity.
|
|
122
|
|
|
123
|
eapply proof.
|
|
124
|
apply H1.
|
|
125
|
Qed.
|
|
126
|
|
|
127
|
Lemma zip_snd : forall {A B}, forall (s1 s1' : Stream A) (s2 s2' : Stream B),
|
|
128
|
EqSt (zip (s1, s2)) (zip (s1', s2')) -> EqSt s2 s2'.
|
|
129
|
Proof.
|
|
130
|
intros A B.
|
|
131
|
cofix proof.
|
|
132
|
destruct s1; destruct s1'; destruct s2; destruct s2'.
|
|
133
|
intro.
|
|
134
|
inversion H.
|
|
135
|
apply eqst.
|
|
136
|
simpl in H0.
|
|
137
|
simpl in H1.
|
|
138
|
injection H0.
|
|
139
|
intros.
|
|
140
|
subst.
|
|
141
|
reflexivity.
|
|
142
|
|
|
143
|
eapply proof.
|
|
144
|
apply H1.
|
|
145
|
Qed.
|
|
146
|
|
|
147
|
Lemma zip_pair : forall {A B}, forall (s1 s1' : Stream A) (s2 s2' : Stream B),
|
|
148
|
EqSt (zip (s1, s2)) (zip (s1', s2')) -> EqSt s1 s1' /\ EqSt s2 s2'.
|
|
149
|
Proof.
|
|
150
|
intros.
|
|
151
|
split.
|
|
152
|
eapply zip_fst.
|
|
153
|
apply H.
|
|
154
|
|
|
155
|
eapply zip_snd.
|
|
156
|
apply H.
|
|
157
|
Qed.
|
|
158
|
|
|
159
|
Definition unzip {A B} (s : Stream (A*B)) := (apply (lift (@fst _ _)) s, apply (lift (@snd _ _)) s).
|
|
160
|
|
|
161
|
Lemma fst_unzip_zip : forall {A B} (s1 : Stream A) (s2 : Stream B), EqSt (apply (lift (@fst _ _)) (zip (s1, s2))) s1.
|
|
162
|
Proof.
|
|
163
|
intros A B.
|
|
164
|
cofix proof.
|
|
165
|
destruct s1; destruct s2.
|
|
166
|
apply eqst.
|
|
167
|
reflexivity.
|
|
168
|
|
|
169
|
apply proof.
|
|
170
|
Qed.
|
|
171
|
|
|
172
|
Lemma snd_unzip_zip : forall {A B} (s1 : Stream A) (s2 : Stream B), EqSt (apply (lift (@snd _ _)) (zip (s1, s2))) s2.
|
|
173
|
Proof.
|
|
174
|
intros A B.
|
|
175
|
cofix proof.
|
|
176
|
destruct s1; destruct s2.
|
|
177
|
apply eqst.
|
|
178
|
reflexivity.
|
|
179
|
|
|
180
|
apply proof.
|
|
181
|
Qed.
|
|
182
|
|
|
183
|
Lemma zip_unzip : forall {A B} (s : Stream (A*B)), EqSt (zip (unzip s)) s.
|
|
184
|
Proof.
|
|
185
|
intros A B.
|
|
186
|
cofix proof.
|
|
187
|
destruct s.
|
|
188
|
apply eqst.
|
|
189
|
simpl.
|
|
190
|
destruct p.
|
|
191
|
reflexivity.
|
|
192
|
|
|
193
|
simpl.
|
|
194
|
apply proof.
|
|
195
|
Qed.
|
|
196
|
(*
|
|
197
|
CoInductive transition {A} (T : A -> A -> Prop) : Stream A -> Prop :=
|
|
198
|
| Tick : forall a0 a1 s'', T a0 a1 -> transition T (Cons a1 s'') -> transition T (Cons a0 (Cons a1 s'')).
|
|
199
|
|
|
200
|
Fixpoint prefix {A} (I : A -> Prop) (T : A -> A -> Prop) (k : nat) : Stream A -> Prop :=
|
|
201
|
match k with
|
|
202
|
| 0 => fun s => True
|
|
203
|
| S k' => fun s => (I (hd s) \/ (T (hd s) (hd (tl s)) /\ prefix I T k' (tl s)))
|
|
204
|
end.
|
|
205
|
|
|
206
|
Lemma I_prefix : forall {A} (I : A -> Prop) (T : A -> A -> Prop) k (s : Stream A), I (hd s) -> prefix I T k s.
|
|
207
|
Proof.
|
|
208
|
destruct k.
|
|
209
|
simpl.
|
|
210
|
trivial.
|
|
211
|
|
|
212
|
simpl.
|
|
213
|
left.
|
|
214
|
trivial.
|
|
215
|
Qed.
|
|
216
|
|
|
217
|
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.
|
|
218
|
Proof.
|
|
219
|
destruct k.
|
|
220
|
simpl.
|
|
221
|
trivial.
|
|
222
|
|
|
223
|
simpl.
|
|
224
|
right.
|
|
225
|
trivial.
|
|
226
|
Qed.
|
|
227
|
|
|
228
|
Lemma prefix_mono_k : forall {A} I T k (s : Stream A), prefix I T (S k) s -> prefix I T k s.
|
|
229
|
Proof.
|
|
230
|
|
|
231
|
Qed.
|
|
232
|
*)
|
|
233
|
|
|
234
|
Theorem eqst_ForAll : forall {A} {P : Stream A -> Prop}, (forall s s', EqSt s s' -> P s -> P s') -> forall {s s'}, EqSt s s' -> ForAll P s -> ForAll P s'.
|
|
235
|
Proof.
|
|
236
|
intros A P HP.
|
|
237
|
cofix proof.
|
|
238
|
destruct s as (s0, sq).
|
|
239
|
destruct s' as (s0', sq').
|
|
240
|
intros Heq H.
|
|
241
|
inversion H.
|
|
242
|
apply HereAndFurther.
|
|
243
|
exact (HP _ _ Heq H0).
|
|
244
|
|
|
245
|
apply (proof sq sq').
|
|
246
|
inversion Heq.
|
|
247
|
assumption.
|
|
248
|
|
|
249
|
assumption.
|
|
250
|
Qed.
|
|
251
|
|
|
252
|
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) :=
|
|
253
|
fun s always_p always_pq =>
|
|
254
|
match always_p, always_pq with
|
|
255
|
| (HereAndFurther p_s always_p'), (HereAndFurther pq_s always_pq') => HereAndFurther s (pq_s p_s) (ForAll_apply (tl s) always_p' always_pq')
|
|
256
|
end.
|
|
257
|
|
|
258
|
CoFixpoint necessitation {A} {P : Stream A -> Prop} (I : forall s, P s) s : ForAll P s :=
|
|
259
|
HereAndFurther s (I s) (necessitation I (tl s)).
|
|
260
|
|
|
261
|
CoFixpoint history_rec {A} (past : list A) (s : Stream A) : Stream (list A * A) :=
|
|
262
|
match s with
|
|
263
|
| Cons s0 s' => Cons (past, s0) (history_rec (cons s0 past) s')
|
|
264
|
end.
|
|
265
|
|
|
266
|
Definition history {A} (s : Stream A) : Stream (list A * A) := history_rec nil s.
|
|
267
|
|
|
268
|
Definition concat {A} (prefix : list A) (suffix : Stream A) : Stream A :=
|
|
269
|
List.fold_left (fun q t => Cons t q) prefix suffix.
|
|
270
|
|
|
271
|
Theorem eqst_history_rec : forall {A} (pfx : list A) (sfx sfx' : Stream A),
|
|
272
|
EqSt sfx sfx' -> EqSt (history_rec pfx sfx) (history_rec pfx sfx').
|
|
273
|
Proof.
|
|
274
|
intros A.
|
|
275
|
cofix proof.
|
|
276
|
destruct sfx as (sfx0, sfxq).
|
|
277
|
destruct sfx' as (sfx0', sfxq').
|
|
278
|
intro H.
|
|
279
|
inversion H.
|
|
280
|
simpl in H0.
|
|
281
|
rewrite H0.
|
|
282
|
apply eqst.
|
|
283
|
reflexivity.
|
|
284
|
|
|
285
|
apply (proof _ sfxq sfxq').
|
|
286
|
assumption.
|
|
287
|
Qed.
|
|
288
|
|
|
289
|
Theorem eqst_history : forall {A} (sfx sfx' : Stream A),
|
|
290
|
EqSt sfx sfx' -> EqSt (history sfx) (history sfx').
|
|
291
|
Proof.
|
|
292
|
intros.
|
|
293
|
apply eqst_history_rec.
|
|
294
|
assumption.
|
|
295
|
Qed.
|
|
296
|
|
|
297
|
Theorem eqst_concat : forall {A} pfx (sfx sfx' : Stream A), EqSt sfx sfx' -> EqSt (concat pfx sfx) (concat pfx sfx').
|
|
298
|
Proof.
|
|
299
|
induction pfx.
|
|
300
|
auto.
|
|
301
|
|
|
302
|
simpl.
|
|
303
|
intros.
|
|
304
|
apply IHpfx.
|
|
305
|
apply eqst.
|
|
306
|
reflexivity.
|
|
307
|
|
|
308
|
exact H.
|
|
309
|
Qed.
|
|
310
|
|
|
311
|
Theorem unzip_history_rec : forall {A} (pfx : list A) (sfx : Stream A), EqSt (snd (unzip (history_rec pfx sfx))) sfx.
|
|
312
|
Proof.
|
|
313
|
intro A.
|
|
314
|
cofix proof.
|
|
315
|
destruct sfx as (sfx0, sfx').
|
|
316
|
apply eqst.
|
|
317
|
reflexivity.
|
|
318
|
|
|
319
|
apply proof.
|
|
320
|
Qed.
|
|
321
|
|
|
322
|
Theorem unzip_history : forall {A} (s : Stream A), EqSt (snd (unzip (history s))) s.
|
|
323
|
Proof.
|
|
324
|
unfold history.
|
|
325
|
intros.
|
|
326
|
apply unzip_history_rec.
|
|
327
|
Qed.
|
|
328
|
|
|
329
|
CoFixpoint cojoin {A} (s : Stream A) : Stream (Stream A) :=
|
|
330
|
match s with
|
|
331
|
| Cons _ s' => Cons s (cojoin s')
|
|
332
|
end.
|
|
333
|
|
|
334
|
Theorem eqst_cojoin : forall {A} (s s' : Stream A), EqSt s s' -> EqSt (cojoin s) (cojoin s').
|
|
335
|
Proof.
|
|
336
|
admit.
|
|
337
|
(*intros A.
|
|
338
|
cofix proof.
|
|
339
|
destruct s as (s0, sq).
|
|
340
|
destruct s' as (s0', sq').
|
|
341
|
intro H.
|
|
342
|
inversion H.
|
|
343
|
simpl in H0.
|
|
344
|
rewrite H0.*)
|
|
345
|
Qed.
|
|
346
|
|
|
347
|
Theorem inv_history_rec : forall {A} p (s : Stream A),
|
|
348
|
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)).
|
|
349
|
Proof.
|
|
350
|
intro A.
|
|
351
|
cofix proof.
|
|
352
|
destruct s as (s0, s').
|
|
353
|
apply HereAndFurther.
|
|
354
|
apply eqst_concat.
|
|
355
|
apply unzip_history_rec.
|
|
356
|
|
|
357
|
apply (proof (cons s0 p) s').
|
|
358
|
Qed.
|
|
359
|
|
|
360
|
Theorem inv_history : forall {A} (s : Stream A),
|
|
361
|
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)).
|
|
362
|
Proof.
|
|
363
|
intros.
|
|
364
|
apply inv_history_rec.
|
|
365
|
Qed.
|
|
366
|
|
|
367
|
Theorem inv_history_rec' : forall {A} p (s : Stream A),
|
|
368
|
ForAll (fun s' => EqSt (concat (fst (hd s')) (apply (lift (@snd _ _)) s')) (concat p s)) (history_rec p s).
|
|
369
|
Proof.
|
|
370
|
intro A.
|
|
371
|
cofix proof.
|
|
372
|
destruct s as (s0, s').
|
|
373
|
apply HereAndFurther.
|
|
374
|
apply eqst_concat.
|
|
375
|
apply unzip_history_rec.
|
|
376
|
|
|
377
|
apply (proof (cons s0 p) s').
|
|
378
|
Qed.
|
|
379
|
|
|
380
|
Theorem inv_history' : forall {A} (s : Stream A),
|
|
381
|
ForAll (fun s' => EqSt (concat (fst (hd s')) (apply (lift (@snd _ _)) s')) s) (history s).
|
|
382
|
Proof.
|
|
383
|
intros.
|
|
384
|
assert (s = concat nil s).
|
|
385
|
reflexivity.
|
|
386
|
|
|
387
|
rewrite H.
|
|
388
|
rewrite <- H in |- * at 1.
|
|
389
|
apply inv_history_rec'.
|
|
390
|
Qed.
|
|
391
|
|
|
392
|
|
|
393
|
Theorem inv_mono_history : forall {A} (P : Stream A -> Prop) (s : Stream A),
|
|
394
|
ForAll P s -> ForAll (fun s' => P (apply (lift (@snd _ _)) s')) (history s).
|
|
395
|
Proof.
|
|
396
|
|
|
397
|
Qed.
|
|
398
|
|
|
399
|
Fixpoint prefix {A} (I : A -> Prop) (T : A -> A -> Prop) (k : nat) : list A -> Prop :=
|
|
400
|
match k with
|
|
401
|
| 0 => fun p => True
|
|
402
|
| S k' => fun p =>
|
|
403
|
match p with
|
|
404
|
| List.nil => True
|
|
405
|
| List.cons t q => (I t) \/
|
|
406
|
match q with
|
|
407
|
| List.nil => False
|
|
408
|
| List.cons t' q' => (T t t') /\ (prefix I T k' q)
|
|
409
|
end
|
|
410
|
end
|
|
411
|
end.
|
|
412
|
|
|
413
|
Theorem inv_prefix : forall {A} (I : A -> Prop) (T : A -> A -> Prop) (s : Stream A),
|
|
414
|
I (hd s) -> ForAll (fun s' => T (hd s') (hd (tl s'))) s ->
|
|
415
|
forall k,
|
|
416
|
ForAll (fun s' => prefix I T k (fst (hd s'))) (history s).
|
|
417
|
Proof.
|
|
418
|
|
|
419
|
Qed.
|
|
420
|
|
|
421
|
Definition _arrow := Cons true (lift false).
|
|
422
|
|
|
423
|
Definition ite {A} (s_if : Stream bool) (s_then s_else : Stream A) :=
|
|
424
|
apply (apply (apply (lift (fun (c : bool) (t e : A) => if c then t else e)) s_if) s_then) s_else.
|
|
425
|
|
|
426
|
Lemma hd_ite : forall {A}, forall (c : Stream bool) (t e : Stream A),
|
|
427
|
hd (ite c t e) = if (hd c) then (hd t) else (hd e).
|
|
428
|
Proof.
|
|
429
|
destruct c; destruct t; destruct e.
|
|
430
|
reflexivity.
|
|
431
|
Qed.
|
|
432
|
|
|
433
|
Lemma tl_ite : forall {A}, forall (c : Stream bool) (t e : Stream A),
|
|
434
|
tl (ite c t e) = ite (tl c) (tl t) (tl e).
|
|
435
|
Proof.
|
|
436
|
destruct c; destruct t; destruct e.
|
|
437
|
reflexivity.
|
|
438
|
Qed.
|
|
439
|
|
|
440
|
Theorem eqst_ite : forall {A}, forall (c1 c2 : Stream bool) (t1 t2 e1 e2 : Stream A),
|
|
441
|
EqSt c1 c2 -> EqSt t1 t2 -> EqSt e1 e2 -> EqSt (ite c1 t1 e1) (ite c2 t2 e2).
|
|
442
|
Proof.
|
|
443
|
intros.
|
|
444
|
apply eqst_apply.
|
|
445
|
apply eqst_apply.
|
|
446
|
apply eqst_apply.
|
|
447
|
apply EqSt_reflex.
|
|
448
|
|
|
449
|
assumption.
|
|
450
|
|
|
451
|
assumption.
|
|
452
|
|
|
453
|
assumption.
|
|
454
|
Qed.
|
|
455
|
|
|
456
|
Variable pre : forall {A}, Stream A -> Stream A.
|
|
457
|
|
|
458
|
Axiom pre_spec : forall {A}, forall (s : Stream A), EqSt (tl (pre s)) s.
|
|
459
|
|
|
460
|
Variable when : forall {A}, Stream bool -> Stream A -> Stream A.
|
|
461
|
|
|
462
|
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).
|
|
463
|
|
|
464
|
|
|
465
|
Require Import Bool.
|
|
466
|
|
|
467
|
Definition bnot (s : Stream bool) := apply (lift negb) s.
|
|
468
|
|
|
469
|
Definition band (s1 s2 : Stream bool) := apply (apply (lift andb) s1) s2.
|
|
470
|
|
|
471
|
Definition bor (s1 s2 : Stream bool) := apply (apply (lift orb) s1) s2.
|
|
472
|
|
|
473
|
Require Import ZArith.
|
|
474
|
|
|
475
|
Definition iplus (s1 s2 : Stream Z) := apply (apply (lift (fun i1 i2 => (i1 + i2)%Z)) s1) s2.
|
|
476
|
|
|
477
|
Definition iminus (s1 s2 : Stream Z) := apply (apply (lift (fun i1 i2 => (i1 - i2)%Z)) s1) s2.
|
|
478
|
|
|
479
|
Definition imult (s1 s2 : Stream Z) := apply (apply (lift (fun i1 i2 => (i1 * i2)%Z)) s1) s2.
|
|
480
|
|
|
481
|
Definition idiv (s1 s2 : Stream Z) := apply (apply (lift (fun i1 i2 => (i1 / i2)%Z)) s1) s2.
|
|
482
|
|
|
483
|
Definition imod (s1 s2 : Stream Z) := apply (apply (lift (fun i1 i2 => Zmod i1 i2)) s1) s2.
|
|
484
|
|
|
485
|
Definition ieq (s1 s2 : Stream Z) := apply (apply (lift (fun i1 i2 => match (i1 ?= i2)%Z with Eq => true | _ => false end)) s1) s2.
|
|
486
|
|
|
487
|
Definition ilt (s1 s2 : Stream Z) := apply (apply (lift (fun i1 i2 => match (i1 ?= i2)%Z with Lt => true | _ => false end)) s1) s2.
|
|
488
|
|
|
489
|
(* sémantique dénotationnelle de f *)
|
|
490
|
Definition denot_f (x cpt y : Stream Z) :=
|
|
491
|
(EqSt y (iplus x (lift 1%Z))) /\ (EqSt cpt (iplus (ite _arrow (lift 0%Z) (pre cpt)) (lift 1%Z))).
|
|
492
|
|
|
493
|
(* sémantique axiomatique de f, simplifiée *)
|
|
494
|
|
|
495
|
Definition mem_f := (bool * Z)%type.
|
|
496
|
|
|
497
|
Definition ni_2 (mem : mem_f) := fst mem.
|
|
498
|
|
|
499
|
Definition __f_2 (mem : mem_f) := snd mem.
|
|
500
|
|
|
501
|
Definition init_f (mem : mem_f) := ni_2 mem = true.
|
|
502
|
|
|
503
|
Definition trans_f (x cpt y : Z) (mem_in mem_out : mem_f) :=
|
|
504
|
(cpt = ((if bool_dec (ni_2 mem_in) true then 0 else (__f_2 mem_in)) + 1)%Z)
|
|
505
|
/\ (y = (x + 1)%Z)
|
|
506
|
/\ (ni_2 mem_out) = false
|
|
507
|
/\ (__f_2 mem_out) = cpt.
|
|
508
|
|
|
509
|
Definition trans_f' (s s' : (Z * (Z * Z)) * mem_f) :=
|
|
510
|
match s, s' with
|
|
511
|
| ((x, (cpt, y)), mem), ((x', (cpt', y')), mem') => trans_f x cpt y mem mem'
|
|
512
|
end.
|
|
513
|
|
|
514
|
Lemma Cons_inj : forall {A}, forall a a' (s s' : Stream A), Cons a s = Cons a' s' -> a = a' /\ s = s'.
|
|
515
|
Proof.
|
|
516
|
intros.
|
|
517
|
injection H.
|
|
518
|
intuition.
|
|
519
|
Qed.
|
|
520
|
|
|
521
|
Theorem raffinement : forall (x cpt y : Stream Z) (mem : Stream mem_f),
|
|
522
|
(init_f (hd mem) /\ transition trans_f' (zip ((zip (x, (zip (cpt, y)))), mem)))
|
|
523
|
->
|
|
524
|
denot_f x cpt y.
|
|
525
|
Proof.
|
|
526
|
intros.
|
|
527
|
apply zip_pair.
|
|
528
|
revert x cpt y mem H.
|
|
529
|
cofix proof.
|
|
530
|
intros.
|
|
531
|
|
|
532
|
|
|
533
|
|
|
534
|
intros.
|
|
535
|
split.
|
|
536
|
revert x cpt y mem H.
|
|
537
|
cofix proof.
|
|
538
|
intros.
|
|
539
|
destruct H.
|
|
540
|
destruct x as (x0, x'); destruct cpt as (cpt0, cpt'); destruct y as (y0, y').
|
|
541
|
destruct mem as (mem0, mem').
|
|
542
|
inversion H0.
|
|
543
|
apply eqst.
|
|
544
|
simpl.
|
|
545
|
unfold zip in H1.
|
|
546
|
simpl in H1.
|
|
547
|
generalize (f_equal (@hd _) H1).
|
|
548
|
simpl.
|
|
549
|
intro.
|
|
550
|
subst.
|
|
551
|
generalize (f_equal (@tl _) H1).
|
|
552
|
simpl.
|
|
553
|
|
|
554
|
Qed.
|
|
555
|
|
|
556
|
|