Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / optim / streams2_lus.v @ 6a93d814

History | View | Annotate | Download (22.6 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 ForAll_reinforce {A} {P Q : (Stream A -> Prop)} : forall s, (ForAll (fun s => P s /\ Q s) s) -> (ForAll Q s).
57
Proof.
58
intros.
59
eapply ForAll_apply.
60
 apply H.
61

    
62
 apply necessitation.
63
 intuition.
64
Defined.
65

    
66
Definition concat {A} (prefix : list A) (suffix : Stream A) : Stream A :=
67
 List.fold_left (fun q t => Cons t q) prefix suffix.
68

    
69
Theorem eqst_concat : forall {A} pfx (sfx sfx' : Stream A), EqSt sfx sfx' -> EqSt (concat pfx sfx) (concat pfx sfx').
70
Proof.
71
induction pfx.
72
 auto.
73

    
74
 simpl.
75
 intros.
76
 apply IHpfx.
77
 apply eqst.
78
  reflexivity.
79

    
80
  exact H.
81
Qed.
82

    
83
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'.
84
Proof.
85
induction pfx.
86
 destruct pfx'.
87
  intuition.
88

    
89
  discriminate.
90

    
91
 destruct pfx'.
92
  discriminate.
93

    
94
  simpl.
95
  intros.
96
  injection H.
97
  clear H; intro H.
98
  generalize (IHpfx _ _ _ H H0).
99
  destruct 1.
100
  inversion H2.
101
  simpl in H3.
102
  simpl in H4.
103
  subst.
104
  intuition.
105
Qed.
106

    
107
Theorem evt_id : forall {A} (s : Stream A), Exists (fun s' => s = s') s.
108
Proof.
109
intros.
110
apply Here.
111
reflexivity.
112
Qed.
113

    
114
Theorem evt_concat : forall {A} (P : Stream A -> Prop) p (s : Stream A), Exists P s -> Exists P (concat p s).
115
Proof.
116
induction p.
117
 trivial.
118

    
119
 intros s H.
120
 apply (IHp (Cons a s)).
121
 apply Further.
122
 exact H.
123
Qed.
124

    
125
Theorem inv_concat : forall {A} (P : Stream A -> Prop) p (s : Stream A), ForAll P (concat p s) -> ForAll P s.
126
Proof.
127
induction p.
128
 trivial.
129

    
130
 simpl.
131
 intros s H.
132
 generalize (IHp (Cons a s) H).
133
 intro H'.
134
 inversion H'.
135
 assumption.
136
Qed.
137

    
138
CoFixpoint lift {A} (v : A) := Cons v (lift v).
139

    
140
Lemma hd_lift : forall {A} {v : A}, hd (lift v) = v.
141
Proof.
142
reflexivity.
143
Qed.
144

    
145
Lemma tl_lift : forall {A} {v : A}, tl (lift v) = lift v.
146
Proof.
147
reflexivity.
148
Qed.
149

    
150
CoFixpoint apply {A B} : @applyT Stream A B :=
151
 fun f a =>
152
 match f, a with
153
 | (Cons f0 f'), (Cons a0 a') => Cons (f0 a0) (apply f' a')
154
 end.
155

    
156
Lemma hd_apply : forall {A B} {f : Stream (A -> B)} {a : Stream A}, hd (apply f a) = (hd f) (hd a).
157
Proof.
158
destruct f; destruct a.
159
reflexivity.
160
Qed.
161

    
162
Lemma tl_apply : forall {A B} {f : Stream (A -> B)} {a : Stream A}, tl (apply f a) = apply (tl f) (tl a).
163
Proof.
164
destruct f; destruct a.
165
reflexivity.
166
Qed.
167

    
168
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')).
169
Proof.
170
intros.
171
apply eqst.
172
 reflexivity.
173

    
174
 apply EqSt_reflex.
175
Qed.
176

    
177
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.
178
Proof.
179
intros A B f P.
180
cofix proof.
181
destruct s as (s0, s').
182
intro H.
183
inversion H.
184
apply HereAndFurther.
185
 assumption.
186

    
187
 simpl.
188
 apply proof.
189
 assumption.
190
Qed.
191

    
192
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).
193
Proof.
194
intros A B f P.
195
cofix proof.
196
destruct s as (s0, s').
197
intro H.
198
inversion H.
199
apply HereAndFurther.
200
 assumption.
201

    
202
 simpl.
203
 apply proof.
204
 assumption.
205
Qed.
206

    
207
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.
208
Proof.
209
intros A B f P s.
210
remember (apply (lift f) s) as ss.
211
intro H.
212
revert s Heqss.
213
induction H.
214
 intros.
215
 apply Here.
216
 rewrite <- Heqss.
217
 exact H.
218

    
219
 intros.
220
 apply Further.
221
 apply (IHExists (tl s)).
222
 rewrite <- tl_lift.
223
 rewrite <- tl_apply.
224
 apply f_equal.
225
 exact Heqss.
226
Qed.
227

    
228
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).
229
Proof.
230
intros A B f P s.
231
intro H.
232
induction H.
233
 apply Here.
234
 exact H.
235

    
236
 apply Further.
237
 rewrite tl_apply.
238
 rewrite tl_lift.
239
 exact IHExists.
240
Qed.
241

    
242
Definition zip {A B} (s : Stream A * Stream B) := apply (apply (lift (fun a b => (a, b))) (fst s)) (snd s).
243

    
244
Lemma zip_fst_eqst : forall {A B}, forall (s1 s1' : Stream A) (s2 s2' : Stream B),
245
  EqSt (zip (s1, s2)) (zip (s1', s2')) -> EqSt s1 s1'.
246
Proof.
247
intros A B.
248
cofix proof.
249
destruct s1; destruct s1'; destruct s2; destruct s2'.
250
intro.
251
inversion H.
252
apply eqst.
253
 simpl in H0.
254
 simpl in H1.
255
 injection H0.
256
 intros.
257
 subst.
258
 reflexivity.
259

    
260
 eapply proof.
261
 apply H1.
262
Qed.
263

    
264
Lemma zip_fst : forall {A B}, forall (s1 s1' : Stream A) (s2 s2' : Stream B),
265
  zip (s1, s2) = zip (s1', s2') -> s1 = s1'.
266
Proof.
267
intros.
268
apply eqst_eq.
269
apply (zip_fst_eqst s1 s1' s2 s2').
270
rewrite H.
271
apply EqSt_reflex.
272
Qed.
273

    
274
Lemma zip_snd_eqst : forall {A B}, forall (s1 s1' : Stream A) (s2 s2' : Stream B),
275
  EqSt (zip (s1, s2)) (zip (s1', s2')) -> EqSt s2 s2'.
276
Proof.
277
intros A B.
278
cofix proof.
279
destruct s1; destruct s1'; destruct s2; destruct s2'.
280
intro.
281
inversion H.
282
apply eqst.
283
 simpl in H0.
284
 simpl in H1.
285
 injection H0.
286
 intros.
287
 subst.
288
 reflexivity.
289

    
290
 eapply proof.
291
 apply H1.
292
Qed.
293

    
294
Lemma zip_snd : forall {A B}, forall (s1 s1' : Stream A) (s2 s2' : Stream B),
295
  zip (s1, s2) = zip (s1', s2') -> s2 = s2'.
296
Proof.
297
intros.
298
apply eqst_eq.
299
apply (zip_snd_eqst s1 s1' s2 s2').
300
rewrite H.
301
apply EqSt_reflex.
302
Qed.
303

    
304
Definition unzip {A B} (s : Stream (A*B)) := (apply (lift (@fst _ _)) s, apply (lift (@snd _ _)) s).
305

    
306
Lemma fst_zip_eqst : forall {A B} (s1 : Stream A) (s2 : Stream B), EqSt (apply (lift (@fst _ _)) (zip (s1, s2))) s1.
307
Proof.
308
intros A B.
309
cofix proof.
310
destruct s1; destruct s2.
311
apply eqst.
312
 reflexivity.
313

    
314
 apply proof.
315
Qed.
316

    
317
Lemma fst_zip : forall {A B} (s1 : Stream A) (s2 : Stream B), apply (lift (@fst _ _)) (zip (s1, s2)) = s1.
318
Proof.
319
intros.
320
apply eqst_eq.
321
apply fst_zip_eqst.
322
Qed.
323

    
324
Lemma snd_zip_eqst : forall {A B} (s1 : Stream A) (s2 : Stream B), EqSt (apply (lift (@snd _ _)) (zip (s1, s2))) s2.
325
Proof.
326
intros A B.
327
cofix proof.
328
destruct s1; destruct s2.
329
apply eqst.
330
 reflexivity.
331

    
332
 apply proof.
333
Qed.
334

    
335
Lemma snd_zip : forall {A B} (s1 : Stream A) (s2 : Stream B), apply (lift (@snd _ _)) (zip (s1, s2)) = s2.
336
Proof.
337
intros.
338
apply eqst_eq.
339
apply snd_zip_eqst.
340
Qed.
341

    
342
Lemma zip_unzip_eqst : forall {A B} (s : Stream (A*B)), EqSt (zip (unzip s)) s.
343
Proof.
344
intros A B.
345
cofix proof.
346
destruct s.
347
apply eqst.
348
 simpl.
349
 destruct p.
350
 reflexivity.
351

    
352
 simpl.
353
 apply proof.
354
Qed.
355

    
356
Lemma zip_unzip : forall {A B} (s : Stream (A*B)), zip (unzip s) = s.
357
Proof.
358
intros.
359
apply eqst_eq.
360
apply zip_unzip_eqst.
361
Qed.
362

    
363
Theorem inv_eq_eqst : forall {A} (s s' : Stream A),
364
 ForAll (fun ss' => fst (hd ss') = snd (hd ss')) (zip (s, s')) -> EqSt s s'.
365
Proof.
366
intro A.
367
cofix proof.
368
destruct s as (s0, s').
369
destruct 0 as (t0, t').
370
intro H.
371
inversion H.
372
apply eqst.
373
 assumption.
374

    
375
 apply proof.
376
 assumption.
377
Qed.
378

    
379
Theorem eqst_inv_eq : forall {A} (s s' : Stream A),
380
  EqSt s s' -> ForAll (fun ss' => fst (hd ss') = snd (hd ss')) (zip (s, s')).
381
Proof.
382
intro A.
383
cofix proof.
384
destruct s as (s0, s').
385
destruct 0 as (t0, t').
386
intro H.
387
inversion H.
388
apply HereAndFurther.
389
 assumption.
390

    
391
 apply proof.
392
 assumption.
393
Qed.
394

    
395

    
396

    
397

    
398

    
399
(*
400
CoInductive transition {A} (T : A -> A -> Prop) : Stream A -> Prop :=
401
| Tick : forall a0 a1 s'', T a0 a1 -> transition T (Cons a1 s'') -> transition T (Cons a0 (Cons a1 s'')).
402

    
403
Fixpoint prefix {A} (I : A -> Prop) (T : A -> A -> Prop) (k : nat) : Stream A -> Prop :=
404
  match k with
405
  | 0    => fun s => True
406
  | S k' => fun s => (I (hd s) \/ (T (hd s) (hd (tl s)) /\ prefix I T k' (tl s)))
407
  end.
408

    
409
Lemma I_prefix : forall {A} (I : A -> Prop) (T : A -> A -> Prop) k (s : Stream A), I (hd s) -> prefix I T k s.
410
Proof.
411
destruct k.
412
 simpl.
413
 trivial.
414

    
415
 simpl.
416
 left.
417
 trivial.
418
Qed.
419

    
420
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.
421
Proof.
422
destruct k.
423
 simpl.
424
 trivial.
425

    
426
 simpl.
427
 right.
428
 trivial.
429
Qed.
430

    
431
Lemma prefix_mono_k : forall {A} I T k (s : Stream A), prefix I T (S k) s -> prefix I T k s.
432
Proof.
433

    
434
Qed.
435
*)
436

    
437
CoFixpoint history_rec {A} (past : list A) (s : Stream A) : Stream (list A * A) :=
438
 match s with
439
 | Cons s0 s' => Cons (past, s0) (history_rec (cons s0 past) s')
440
 end.
441

    
442
Definition history {A} (s : Stream A) : Stream (list A * A) := history_rec nil s. 
443

    
444
Theorem eqst_history_rec : forall {A} (pfx : list A) (sfx sfx' : Stream A),
445
  EqSt sfx sfx' -> EqSt (history_rec pfx sfx) (history_rec pfx sfx').
446
Proof.
447
intros A.
448
cofix proof.
449
destruct sfx as (sfx0, sfxq).
450
destruct sfx' as (sfx0', sfxq').
451
intro H.
452
inversion H.
453
simpl in H0.
454
rewrite H0.
455
apply eqst.
456
 reflexivity.
457

    
458
 apply (proof _ sfxq sfxq').
459
 assumption.
460
Qed.
461

    
462
Theorem eqst_history : forall {A} (sfx sfx' : Stream A),
463
  EqSt sfx sfx' -> EqSt (history sfx) (history sfx').
464
Proof.
465
intros.
466
apply eqst_history_rec.
467
assumption.
468
Qed.
469

    
470
Theorem unzip_history_rec : forall {A} (pfx : list A) (sfx : Stream A), EqSt (snd (unzip (history_rec pfx sfx))) sfx.
471
Proof.
472
intro A.
473
cofix proof.
474
destruct sfx as (sfx0, sfx').
475
apply eqst.
476
 reflexivity.
477

    
478
 apply proof.
479
Qed.
480

    
481
Theorem unzip_history : forall {A} (s : Stream A), EqSt (snd (unzip (history s))) s.
482
Proof.
483
unfold history.
484
intros.
485
apply unzip_history_rec.
486
Qed.
487
(*
488
Theorem hd_history_rec : forall {A} p (s : Stream A), hd (history_rec p s) = (p, hd s).
489
Proof.
490
destruct s.
491
reflexivity.
492
Qed.
493

    
494
Theorem hd_history : forall {A} (s : Stream A), hd (history s) = (nil, hd s).
495
Proof.
496
destruct s.
497
reflexivity.
498
Qed.
499

    
500
Definition snoc {A} (a : A) (l : list A) := app l (cons a nil).
501

    
502
Theorem tl_history_rec : forall {A} p (s : Stream A), tl (history_rec p s) = history_rec (cons (hd s) p) (tl s).
503
Proof.
504
intros.
505
destruct s.
506
reflexivity.
507
Qed.
508

    
509
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))).
510
Proof.
511
intros.
512
Qed.
513

    
514
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))).
515
Proof.
516
intros.
517
Qed.
518
*)
519
CoFixpoint cojoin {A} (s : Stream A) : Stream (Stream A) :=
520
 match s with
521
 | Cons _ s' => Cons s (cojoin s')
522
 end.
523
(*
524
Theorem eqst_cojoin : forall {A} (s s' : Stream A), EqSt s s' -> EqSt (cojoin s) (cojoin s').
525
Proof.
526

    
527
intros A.
528
cofix proof.
529
destruct s as (s0, sq).
530
destruct s' as (s0', sq').
531
intro H.
532
inversion H.
533
simpl in H0.
534
rewrite H0.
535
Qed.
536

    
537
Theorem inv_history_rec : forall {A} p (s : Stream A),
538
  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)).
539
Proof.
540
intro A.
541
cofix proof.
542
destruct s as (s0, s').
543
apply HereAndFurther.
544
 apply eqst_concat.
545
 apply unzip_history_rec.
546

    
547
 apply (proof (cons s0 p) s').
548
Qed.
549

    
550
Theorem inv_history : forall {A} (s : Stream A),
551
  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)).
552
Proof.
553
intros.
554
apply inv_history_rec.
555
Qed.
556
*)
557

    
558
Definition History_Spec {A} (s : Stream A) s' :=
559
     fst (hd (tl s')) = cons (snd (hd s')) (fst (hd s'))
560
  /\ EqSt (concat (fst (hd s')) (apply (lift (@snd _ _)) s')) s.
561

    
562
Theorem history_rec_spec : forall {A} p (s : Stream A),
563
     fst (hd (history_rec p s)) = p 
564
  /\ ForAll (fun s' => History_Spec (concat p s) s') (history_rec p s).
565
Proof.
566
intros.
567
split.
568
 destruct s.
569
 reflexivity.
570

    
571
 revert p s.
572
 cofix proof.
573
 destruct s as (s0, s').
574
 apply HereAndFurther.
575
  split.
576
   simpl.
577
   destruct s'.
578
   reflexivity.
579

    
580
   apply eqst_concat.
581
   apply unzip_history_rec.
582

    
583
  apply (proof (cons s0 p) s').
584
Qed.
585

    
586
Theorem history_spec : forall {A} (s : Stream A),
587
     fst (hd (history s)) = nil
588
  /\ ForAll (fun s' => History_Spec s s') (history s).
589
Proof.
590
intros.
591
generalize (history_rec_spec nil s).
592
intuition.
593
Qed.
594

    
595
Theorem history_rec_spec_complete : forall {A} p (s : Stream A) ps,
596
  fst (hd ps) = p -> ForAll (fun s' => History_Spec (concat p s) s') ps -> EqSt ps (history_rec p s).
597
Proof.
598
intro A.
599
cofix proof.
600
intros.
601
destruct s as (s0, s').
602
destruct ps as ((p_ps0, s_ps0), ps').
603
simpl in H.
604
subst.
605
inversion H0.
606
unfold History_Spec in H.
607
destruct H.
608
simpl in H.
609
apply eqst.
610
 simpl.
611
 intros.
612
 simpl in H.
613
 subst.
614
 inversion H0.
615
 unfold History_Spec in H.
616
 destruct H.
617
 simpl.
618
 simpl in H2.
619
 destruct (concat_eqst _ _ _ _ refl_equal H2).
620
 inversion H5.
621
 simpl in H6.
622
 subst.
623
 reflexivity.
624

    
625
 simpl.
626
 apply proof.
627
  simpl in H2.
628
  destruct (concat_eqst _ _ _ _ refl_equal H2).
629
  inversion H4.
630
  simpl in H5.
631
  subst.
632
  assumption.
633

    
634
  assumption.
635
Qed.
636

    
637
Theorem history_spec_complete : forall {A} (s : Stream A) ps,
638
  fst (hd ps) = nil -> ForAll (fun s' => History_Spec s s') ps -> EqSt ps (history s).
639
Proof.
640
intros.
641
apply history_rec_spec_complete.
642
 assumption.
643

    
644
 assumption.
645
Qed.
646

    
647
Theorem inv_snd_history_rec_intro : forall {A} (P : Stream A -> Prop) p (s : Stream A),
648
  ForAll P s -> ForAll (fun s' => P (apply (lift (@snd _ _)) s')) (history_rec p s).
649
Proof.
650
intros.
651
apply inv_map.
652
generalize (eqst_eq _ _ (unzip_history_rec p s)).
653
simpl.
654
intro Hs.
655
rewrite Hs.
656
exact H.
657
Qed.
658

    
659
Theorem inv_snd_history_intro : forall {A} (P : Stream A -> Prop) (s : Stream A),
660
  ForAll P s -> ForAll (fun s' => P (apply (lift (@snd _ _)) s')) (history s).
661
Proof.
662
intros.
663
apply inv_snd_history_rec_intro.
664
assumption.
665
Qed.
666

    
667
Theorem inv_snd_history_rec_elim : forall {A} (P : Stream A -> Prop) p (s : Stream A),
668
  ForAll (fun s' => P (apply (lift (@snd _ _)) s')) (history_rec p s) -> ForAll P s.
669
Proof.
670
intros.
671
rewrite <- (eqst_eq _ _ (unzip_history_rec p s)).
672
apply map_inv.
673
exact H.
674
Qed.
675

    
676
Theorem inv_snd_history_elim : forall {A} (P : Stream A -> Prop) (s : Stream A),
677
  ForAll (fun s' => P (apply (lift (@snd _ _)) s')) (history s) -> ForAll P s.
678
Proof.
679
intros.
680
apply inv_snd_history_rec_elim with (p := nil).
681
assumption.
682
Qed.
683

    
684
Fixpoint prefix {A} (I : A -> Prop) (T : A -> A -> Prop) (k : nat) : list A -> Prop :=
685
  match k with
686
  | 0    => fun p     => True
687
  | S k' => fun p =>
688
   match p with
689
   | List.nil         => True
690
   | List.cons t q =>
691
    match q with
692
    | List.nil        => (I t)
693
    | List.cons t' q' => (T t' t) /\ (prefix I T k' q)
694
    end
695
   end
696
  end.
697

    
698
Theorem prefix_mono_k : forall {A} I T k (p : list A), prefix I T (S k) p -> prefix I T k p.
699
Proof.
700
induction k.
701
 simpl.
702
 trivial.
703

    
704
 simpl.
705
 intuition.
706
 destruct p.
707
  trivial.
708

    
709
  intuition.
710
  destruct p.
711
   intuition.
712

    
713
   intuition.
714
Qed.
715

    
716
Theorem prefix_apply : forall {A} (I I' : A -> Prop) (T T' : A -> A -> Prop) k (p : list A),
717
  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.
718
Proof.
719
intros A I I' T T'.
720
induction k.
721
 trivial.
722

    
723
 simpl.
724
 destruct p.
725
  trivial.
726

    
727
  destruct p.
728
   intuition.
729

    
730
   intuition.
731
Qed.
732

    
733
Theorem kinduction : forall {A} (P : A -> Prop) k (s : Stream A),
734
    ForAll (fun s' => prefix (fun st => P st) (fun st st' => P st') k (fst (hd s')) -> P (snd (hd s'))) (history s)
735
 -> ForAll (fun s' => P (hd s')) s.
736
Proof.
737
intros.
738
apply inv_snd_history_elim.
739
apply @ForAll_apply with (P := fun s' => P (snd (hd s'))).
740
 apply
741
  @ForAll_apply
742
   with
743
     (P := fun s' =>
744
           prefix (fun st => P st) (fun st st' => P st') k (fst (hd s'))).
745
  apply
746
   @ForAll_reinforce
747
    with
748
      (P := ForAll
749
              (fun s' : Stream (list A * A) =>
750
               prefix (fun st : A => P st) (fun _ st' : A => P st') k
751
                 (fst (hd s')) -> P (snd (hd s')))).
752
  apply
753
   @ForAll_reinforce
754
    with (P := ForAll (fun s' : Stream (list A * A) => History_Spec s s')).
755
  eapply ForAll_coind.
756
   intro.
757
   exact (fun x => x).
758

    
759
   destruct x as ((p0, s0), ((p1, s1), x'')).
760
   simpl.
761
   intuition.
762
    inversion H1.
763
    assumption.
764

    
765
    inversion H0.
766
    assumption.
767

    
768
    inversion H1.
769
    unfold History_Spec in H2.
770
    simpl in H2.
771
    destruct H2.
772
    rewrite H2.
773
    destruct k.
774
     simpl.
775
     trivial.
776

    
777
     simpl.
778
     inversion H0.
779
     simpl in H6.
780
     destruct p0.
781
      intuition.
782

    
783
      split.
784
       simpl in H3.
785
       apply H6.
786
       exact H3.
787

    
788
       apply prefix_mono_k.
789
       exact H3.
790

    
791
   simpl.
792
   intuition.
793
    generalize (history_spec s).
794
    intuition.
795

    
796
    destruct s.
797
    simpl.
798
    destruct k.
799
     simpl.
800
     trivial.
801

    
802
     simpl.
803
     trivial.
804

    
805
  exact H.
806

    
807
 apply necessitation.
808
 destruct s0.
809
 simpl.
810
 trivial.
811
Qed.
812

    
813
Theorem kinduction' :  forall {A} (P : A -> Prop) k ps (s : Stream A),
814
    fst (hd ps) = nil
815
 -> ForAll (fun s' => History_Spec s s') ps
816
 -> ForAll (fun s' => prefix (fun st => P st) (fun st st' => P st') k (fst (hd s')) -> P (snd (hd s'))) ps
817
 -> ForAll (fun s' => P (hd s')) s.
818
Proof.
819
intros.
820
rewrite (eqst_eq _ _ (history_spec_complete _ _ H H0)) in H1.
821
eapply kinduction.
822
apply H1.
823
Qed.
824

    
825
Theorem inv_prefix_history_rec : forall {A} (I : A -> Prop) (T : A -> A -> Prop) p (s : Stream A),
826
 ForAll (fun s' => T (hd s') (hd (tl s'))) (concat p s) ->
827
 forall k,
828
   prefix I T k (cons (hd s) p) ->
829
   ForAll (fun s' => prefix I T k (cons (snd (hd s')) (fst (hd s')))) (history_rec p s).
830
Proof.
831
intros A I T.
832
cofix proof.
833
intros.
834
inversion H.
835
destruct s as (s0, s').
836
apply HereAndFurther.
837
 assumption.
838

    
839
 simpl.
840
 apply proof.
841
  assumption.
842

    
843
  destruct k; simpl.
844
   trivial.
845

    
846
   split.
847
    generalize (inv_concat _ _ _ H).
848
    clear H; intro H.
849
    inversion H.
850
    assumption.
851

    
852
    apply prefix_mono_k.
853
    assumption.
854
Qed.
855

    
856
Theorem inv_prefix_history : forall {A} (I : A -> Prop) (T : A -> A -> Prop) (s : Stream A),
857
 I (hd s) -> ForAll (fun s' => T (hd s') (hd (tl s'))) s ->
858
 forall k,
859
 ForAll (fun s' => prefix I T k (cons (snd (hd s')) (fst (hd s')))) (history s).
860
Proof.
861
intros.
862
apply inv_prefix_history_rec.
863
 assumption.
864

    
865
 destruct k; simpl.
866
  trivial.
867

    
868
  assumption.
869
Qed.
870

    
871
Theorem inv_prefix_history' : forall {A} (I : A -> Prop) (T : A -> A -> Prop) (s : Stream A),
872
 I (hd s) -> ForAll (fun s' => T (hd s') (hd (tl s'))) s ->
873
 forall k,
874
 ForAll (fun s' => prefix I T k (fst (hd s'))) (history s).
875
Proof.
876
intros.
877
destruct k.
878
 apply necessitation.
879
 simpl.
880
 trivial.
881

    
882
 eapply ForAll_apply.
883
  apply (fun i n => inv_prefix_history I T s i n (S (S k))).
884
   apply H.
885

    
886
   apply H0.
887

    
888
  apply necessitation.
889
  destruct s0 as ((p0, s0), s').
890
  simpl.
891
  destruct p0.
892
   trivial.
893

    
894
   intuition.
895
Qed.
896

    
897
Definition _arrow := Cons true (lift false).
898

    
899
Definition ite {A} (s_if : Stream bool) (s_then s_else : Stream A) :=
900
 apply (apply (apply (lift (fun (c : bool) (t e : A) => if c then t else e)) s_if) s_then) s_else.
901

    
902
Lemma hd_ite : forall {A}, forall (c : Stream bool) (t e : Stream A),
903
 hd (ite c t e) = if (hd c) then (hd t) else (hd e).
904
Proof.
905
destruct c; destruct t; destruct e.
906
reflexivity.
907
Qed.
908

    
909
Lemma tl_ite : forall {A}, forall (c : Stream bool) (t e : Stream A),
910
 tl (ite c t e) = ite (tl c) (tl t) (tl e).
911
Proof.
912
destruct c; destruct t; destruct e.
913
reflexivity.
914
Qed.
915

    
916
Theorem eqst_ite : forall {A}, forall (c1 c2 : Stream bool) (t1 t2 e1 e2 : Stream A),
917
 EqSt c1 c2 -> EqSt t1 t2 -> EqSt e1 e2 -> EqSt (ite c1 t1 e1) (ite c2 t2 e2).
918
Proof.
919
intros.
920
apply eqst_apply.
921
 apply eqst_apply.
922
  apply eqst_apply.
923
   apply EqSt_reflex.
924

    
925
   assumption.
926

    
927
  assumption.
928

    
929
 assumption.
930
Qed.
931

    
932
Variable pre : forall {A}, Stream A -> Stream A.
933

    
934
Axiom pre_spec : forall {A}, forall (s : Stream A), EqSt (tl (pre s)) s.
935

    
936
Variable when : forall {A}, Stream bool -> Stream A -> Stream A.
937

    
938
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).
939

    
940

    
941
Require Import Bool.
942

    
943
Definition bnot (s : Stream bool) := apply (lift negb) s.
944

    
945
Definition band (s1 s2 : Stream bool) := apply (apply (lift andb) s1) s2.
946

    
947
Definition bor (s1 s2 : Stream bool) := apply (apply (lift orb) s1) s2.
948

    
949
Require Import ZArith.
950

    
951
Definition iplus (s1 s2 : Stream Z) := apply (apply (lift (fun i1 i2 => (i1 + i2)%Z)) s1) s2.
952

    
953
Definition iminus (s1 s2 : Stream Z) := apply (apply (lift (fun i1 i2 => (i1 - i2)%Z)) s1) s2.
954

    
955
Definition imult (s1 s2 : Stream Z) := apply (apply (lift (fun i1 i2 => (i1 * i2)%Z)) s1) s2.
956

    
957
Definition idiv (s1 s2 : Stream Z) := apply (apply (lift (fun i1 i2 => (i1 / i2)%Z)) s1) s2.
958

    
959
Definition imod (s1 s2 : Stream Z) := apply (apply (lift (fun i1 i2 => Zmod i1 i2)) s1) s2.
960

    
961
Definition ieq (s1 s2 : Stream Z) := apply (apply (lift (fun i1 i2 => match (i1 ?= i2)%Z with Eq => true | _ => false end)) s1) s2.
962

    
963
Definition ilt (s1 s2 : Stream Z) := apply (apply (lift (fun i1 i2 => match (i1 ?= i2)%Z with Lt => true | _ => false end)) s1) s2.
964

    
965
(* sémantique dénotationnelle de f *)
966
Definition denot_f (x cpt y : Stream Z) :=
967
 (EqSt y (iplus x (lift 1%Z))) /\ (EqSt cpt (iplus (ite _arrow (lift 0%Z) (pre cpt)) (lift 1%Z))).
968

    
969
(* sémantique axiomatique de f, simplifiée *)
970

    
971
Definition mem_f := (bool * Z)%type.
972

    
973
Definition ni_2 (mem : mem_f) := fst mem.
974

    
975
Definition __f_2 (mem : mem_f) := snd mem.
976

    
977
Definition init_f (mem : mem_f) := ni_2 mem = true.
978

    
979
Definition trans_f (x cpt y : Z) (mem_in mem_out : mem_f) :=
980
    (cpt = ((if bool_dec (ni_2 mem_in) true then 0 else (__f_2 mem_in)) + 1)%Z)
981
 /\ (y   = (x + 1)%Z)
982
 /\ (ni_2 mem_out) = false
983
 /\ (__f_2 mem_out) = cpt.
984

    
985
Definition trans_f' (s s' : (Z * (Z * Z)) * mem_f) :=
986
 match s, s' with
987
 | ((x, (cpt, y)), mem), ((x', (cpt', y')), mem') => trans_f x cpt y mem mem'
988
 end.
989

    
990
Lemma Cons_inj : forall {A}, forall a a' (s s' : Stream A), Cons a s = Cons a' s' -> a = a' /\ s = s'.
991
Proof.
992
intros.
993
injection H.
994
intuition.
995
Qed.
996

    
997
Theorem raffinement : forall (x cpt y : Stream Z) (mem : Stream mem_f),
998
         (init_f (hd mem) /\ transition trans_f' (zip ((zip (x, (zip (cpt, y)))), mem)))
999
         ->
1000
         denot_f x cpt y.
1001
Proof.
1002
intros.
1003
apply zip_pair.
1004
revert x cpt y mem H.
1005
cofix proof.
1006
intros.
1007

    
1008

    
1009

    
1010
intros.
1011
split.
1012
 revert x cpt y mem H.
1013
 cofix proof.
1014
 intros.
1015
 destruct H.
1016
 destruct x as (x0, x'); destruct cpt as (cpt0, cpt'); destruct y as (y0, y').
1017
 destruct mem as (mem0, mem').
1018
 inversion H0.
1019
 apply eqst.
1020
  simpl.
1021
  unfold zip in H1.
1022
  simpl in H1.
1023
  generalize (f_equal (@hd _) H1).
1024
  simpl.
1025
  intro.
1026
  subst.
1027
  generalize (f_equal (@tl _) H1).
1028
  simpl.
1029

    
1030
Qed. 
1031

    
1032