Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / optim / oversampling / streams2_lus.v @ 6a93d814

History | View | Annotate | Download (17.8 KB)

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