Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / optim / StreamsLib.v @ 6a93d814

History | View | Annotate | Download (18.1 KB)

1
Require Export Streams.
2
Require List.
3
Require Import Setoid.
4
Require Import Relation_Definitions.
5
Require Import Program.Wf.
6
Require Import Wf_nat.
7
Require Import Wellfounded.
8

    
9
Definition mapT (F : Type -> Type) {A B} := (A -> B) -> (F A) -> (F B).
10

    
11
Definition applyT (F : Type -> Type) {A B} := (F (A -> B)) -> (F A) -> (F B).
12

    
13
Definition option_apply {A B} : @applyT option A B :=
14
 fun f a =>
15
 match f, a with
16
 | Some f, Some a => Some (f a)
17
 | _     , _      => None
18
 end.
19

    
20

    
21
Axiom eqst_eq : forall {A} (s s' : Stream A), EqSt s s' -> s = s'.
22

    
23
Theorem inv_inv : forall {A} (P : Stream A -> Prop) (s : Stream A), ForAll P s -> ForAll (fun s' => ForAll P s') s.
24
Proof.
25
intros A P.
26
cofix proof.
27
destruct s as (s0, s').
28
intro H.
29
apply HereAndFurther.
30
 exact H.
31

    
32
 simpl.
33
 apply proof.
34
 inversion H.
35
 assumption.
36
Qed.
37

    
38
Theorem evt_inv : forall {A} (P Q : Stream A -> Prop) (s : Stream A),
39
  ForAll P s -> Exists Q s -> Exists (fun s' => P s' /\ Q s') s.
40
Proof.
41
induction 2.
42
 apply Here.
43
 inversion H.
44
 intuition.
45

    
46
 apply Further.
47
 apply IHExists.
48
 inversion H.
49
 assumption.
50
Qed.
51

    
52
CoFixpoint ForAll_apply {A} {P Q : (Stream A -> Prop)} : forall s, (ForAll P s) -> (ForAll (fun s => P s -> Q s) s) -> (ForAll Q s) :=
53
 fun s always_p always_pq =>
54
 match always_p, always_pq with
55
 | (HereAndFurther p_s always_p'), (HereAndFurther pq_s always_pq') => HereAndFurther s (pq_s p_s) (ForAll_apply (tl s) always_p' always_pq')
56
 end.
57

    
58
CoFixpoint necessitation {A} {P : Stream A -> Prop} (I : forall s, P s) s : ForAll P s :=
59
 HereAndFurther s (I s) (necessitation I (tl s)).
60

    
61
Definition ForAll_reinforce {A} {P Q : (Stream A -> Prop)} : forall s, (ForAll (fun s => P s /\ Q s) s) -> (ForAll Q s).
62
Proof.
63
intros.
64
eapply ForAll_apply.
65
 apply H.
66

    
67
 apply necessitation.
68
 intuition.
69
Defined.
70

    
71
Definition concat {A} (prefix : list A) (suffix : Stream A) : Stream A :=
72
 List.fold_left (fun q t => Cons t q) prefix suffix.
73

    
74
Theorem eqst_concat : forall {A} pfx (sfx sfx' : Stream A), EqSt sfx sfx' -> EqSt (concat pfx sfx) (concat pfx sfx').
75
Proof.
76
induction pfx.
77
 auto.
78

    
79
 simpl.
80
 intros.
81
 apply IHpfx.
82
 apply eqst.
83
  reflexivity.
84

    
85
  exact H.
86
Qed.
87

    
88
Theorem concat_eqst : forall {A} pfx pfx' (sfx sfx' : Stream A), List.length pfx = List.length pfx' -> EqSt (concat pfx sfx) (concat pfx' sfx') -> pfx = pfx' /\ EqSt sfx sfx'.
89
Proof.
90
induction pfx.
91
 destruct pfx'.
92
  intuition.
93

    
94
  discriminate.
95

    
96
 destruct pfx'.
97
  discriminate.
98

    
99
  simpl.
100
  intros.
101
  injection H.
102
  clear H; intro H.
103
  generalize (IHpfx _ _ _ H H0).
104
  destruct 1.
105
  inversion H2.
106
  simpl in H3.
107
  simpl in H4.
108
  subst.
109
  intuition.
110
Qed.
111

    
112
Theorem evt_id : forall {A} (s : Stream A), Exists (fun s' => s = s') s.
113
Proof.
114
intros.
115
apply Here.
116
reflexivity.
117
Qed.
118

    
119
Theorem evt_concat : forall {A} (P : Stream A -> Prop) p (s : Stream A), Exists P s -> Exists P (concat p s).
120
Proof.
121
induction p.
122
 trivial.
123

    
124
 intros s H.
125
 apply (IHp (Cons a s)).
126
 apply Further.
127
 exact H.
128
Qed.
129

    
130
Theorem inv_concat : forall {A} (P : Stream A -> Prop) p (s : Stream A), ForAll P (concat p s) -> ForAll P s.
131
Proof.
132
induction p.
133
 trivial.
134

    
135
 simpl.
136
 intros s H.
137
 generalize (IHp (Cons a s) H).
138
 intro H'.
139
 inversion H'.
140
 assumption.
141
Qed.
142

    
143
CoFixpoint lift {A} (v : A) := Cons v (lift v).
144

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

    
150
Lemma tl_lift : forall {A} {v : A}, tl (lift v) = lift v.
151
Proof.
152
reflexivity.
153
Qed.
154

    
155
CoFixpoint apply {A B} : @applyT Stream A B :=
156
 fun f a =>
157
 match f, a with
158
 | (Cons f0 f'), (Cons a0 a') => Cons (f0 a0) (apply f' a')
159
 end.
160

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

    
167
Lemma tl_apply : forall {A B} {f : Stream (A -> B)} {a : Stream A}, tl (apply f a) = apply (tl f) (tl a).
168
Proof.
169
destruct f; destruct a.
170
reflexivity.
171
Qed.
172

    
173
Lemma cons_apply : forall {A B} {f0 : A -> B} {f' : Stream (A -> B)} {a0 : A} {a' : Stream A}, EqSt (apply (Cons f0 f') (Cons a0 a')) (Cons (f0 a0) (apply f' a')).
174
Proof.
175
intros.
176
apply eqst.
177
 reflexivity.
178

    
179
 apply EqSt_reflex.
180
Qed.
181

    
182
Lemma eqst_apply : forall {A B} {f f' : Stream (A -> B)} {a a' : Stream A},
183
  EqSt f f' -> EqSt a a' -> EqSt (apply f a) (apply f' a').
184
Proof.
185
intros A B.
186
cofix proof.
187
intros.
188
inversion H.
189
inversion H0.
190
apply eqst.
191
 rewrite hd_apply.
192
 rewrite hd_apply.
193
 congruence.
194

    
195
 rewrite tl_apply.
196
 rewrite tl_apply.
197
 apply proof.
198
  assumption.
199

    
200
  assumption.
201
Qed.
202

    
203
Theorem inv_map : forall {A B} (f : A -> B) P (s : Stream A), ForAll P (apply (lift f) s) -> ForAll (fun s' => P (apply (lift f) s')) s.
204
Proof.
205
intros A B f P.
206
cofix proof.
207
destruct s as (s0, s').
208
intro H.
209
inversion H.
210
apply HereAndFurther.
211
 assumption.
212

    
213
 simpl.
214
 apply proof.
215
 assumption.
216
Qed.
217

    
218
Theorem map_inv : forall {A B} (f : A -> B) P (s : Stream A), ForAll (fun s' => P (apply (lift f) s')) s -> ForAll P (apply (lift f) s).
219
Proof.
220
intros A B f P.
221
cofix proof.
222
destruct s as (s0, s').
223
intro H.
224
inversion H.
225
apply HereAndFurther.
226
 assumption.
227

    
228
 simpl.
229
 apply proof.
230
 assumption.
231
Qed.
232

    
233
Theorem evt_map : forall {A B} (f : A -> B) P (s : Stream A), Exists P (apply (lift f) s) -> Exists (fun s' => P (apply (lift f) s')) s.
234
Proof.
235
intros A B f P s.
236
remember (apply (lift f) s) as ss.
237
intro H.
238
revert s Heqss.
239
induction H.
240
 intros.
241
 apply Here.
242
 rewrite <- Heqss.
243
 exact H.
244

    
245
 intros.
246
 apply Further.
247
 apply (IHExists (tl s)).
248
 rewrite <- tl_lift.
249
 rewrite <- tl_apply.
250
 apply f_equal.
251
 exact Heqss.
252
Qed.
253

    
254
Theorem map_evt : forall {A B} (f : A -> B) P (s : Stream A), Exists (fun s' => P (apply (lift f) s')) s -> Exists P (apply (lift f) s).
255
Proof.
256
intros A B f P s.
257
intro H.
258
induction H.
259
 apply Here.
260
 exact H.
261

    
262
 apply Further.
263
 rewrite tl_apply.
264
 rewrite tl_lift.
265
 exact IHExists.
266
Qed.
267

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

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

    
286
 eapply proof.
287
 apply H1.
288
Qed.
289

    
290
Lemma zip_fst : forall {A B}, forall (s1 s1' : Stream A) (s2 s2' : Stream B),
291
  zip (s1, s2) = zip (s1', s2') -> s1 = s1'.
292
Proof.
293
intros.
294
apply eqst_eq.
295
apply (zip_fst_eqst s1 s1' s2 s2').
296
rewrite H.
297
apply EqSt_reflex.
298
Qed.
299

    
300
Lemma zip_snd_eqst : forall {A B}, forall (s1 s1' : Stream A) (s2 s2' : Stream B),
301
  EqSt (zip (s1, s2)) (zip (s1', s2')) -> EqSt s2 s2'.
302
Proof.
303
intros A B.
304
cofix proof.
305
destruct s1; destruct s1'; destruct s2; destruct s2'.
306
intro.
307
inversion H.
308
apply eqst.
309
 simpl in H0.
310
 simpl in H1.
311
 injection H0.
312
 intros.
313
 subst.
314
 reflexivity.
315

    
316
 eapply proof.
317
 apply H1.
318
Qed.
319

    
320
Lemma zip_snd : forall {A B}, forall (s1 s1' : Stream A) (s2 s2' : Stream B),
321
  zip (s1, s2) = zip (s1', s2') -> s2 = s2'.
322
Proof.
323
intros.
324
apply eqst_eq.
325
apply (zip_snd_eqst s1 s1' s2 s2').
326
rewrite H.
327
apply EqSt_reflex.
328
Qed.
329

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

    
332
Lemma fst_zip_eqst : forall {A B} (s1 : Stream A) (s2 : Stream B), EqSt (apply (lift (@fst _ _)) (zip (s1, s2))) s1.
333
Proof.
334
intros A B.
335
cofix proof.
336
destruct s1; destruct s2.
337
apply eqst.
338
 reflexivity.
339

    
340
 apply proof.
341
Qed.
342

    
343
Lemma fst_zip : forall {A B} (s1 : Stream A) (s2 : Stream B), apply (lift (@fst _ _)) (zip (s1, s2)) = s1.
344
Proof.
345
intros.
346
apply eqst_eq.
347
apply fst_zip_eqst.
348
Qed.
349

    
350
Lemma snd_zip_eqst : forall {A B} (s1 : Stream A) (s2 : Stream B), EqSt (apply (lift (@snd _ _)) (zip (s1, s2))) s2.
351
Proof.
352
intros A B.
353
cofix proof.
354
destruct s1; destruct s2.
355
apply eqst.
356
 reflexivity.
357

    
358
 apply proof.
359
Qed.
360

    
361
Lemma snd_zip : forall {A B} (s1 : Stream A) (s2 : Stream B), apply (lift (@snd _ _)) (zip (s1, s2)) = s2.
362
Proof.
363
intros.
364
apply eqst_eq.
365
apply snd_zip_eqst.
366
Qed.
367

    
368
Lemma zip_unzip_eqst : forall {A B} (s : Stream (A*B)), EqSt (zip (unzip s)) s.
369
Proof.
370
intros A B.
371
cofix proof.
372
destruct s.
373
apply eqst.
374
 simpl.
375
 destruct p.
376
 reflexivity.
377

    
378
 simpl.
379
 apply proof.
380
Qed.
381

    
382
Lemma zip_unzip : forall {A B} (s : Stream (A*B)), zip (unzip s) = s.
383
Proof.
384
intros.
385
apply eqst_eq.
386
apply zip_unzip_eqst.
387
Qed.
388

    
389
Theorem inv_eq_eqst : forall {A} (s s' : Stream A),
390
 ForAll (fun ss' => fst (hd ss') = snd (hd ss')) (zip (s, s')) -> EqSt s s'.
391
Proof.
392
intro A.
393
cofix proof.
394
destruct s as (s0, s').
395
destruct 0 as (t0, t').
396
intro H.
397
inversion H.
398
apply eqst.
399
 assumption.
400

    
401
 apply proof.
402
 assumption.
403
Qed.
404

    
405
Theorem eqst_inv_eq : forall {A} (s s' : Stream A),
406
  EqSt s s' -> ForAll (fun ss' => fst (hd ss') = snd (hd ss')) (zip (s, s')).
407
Proof.
408
intro A.
409
cofix proof.
410
destruct s as (s0, s').
411
destruct 0 as (t0, t').
412
intro H.
413
inversion H.
414
apply HereAndFurther.
415
 assumption.
416

    
417
 apply proof.
418
 assumption.
419
Qed.
420

    
421

    
422
CoFixpoint history_rec {A} (past : list A) (s : Stream A) : Stream (list A * A) :=
423
 match s with
424
 | Cons s0 s' => Cons (past, s0) (history_rec (cons s0 past) s')
425
 end.
426

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

    
429
Theorem eqst_history_rec : forall {A} (pfx : list A) (sfx sfx' : Stream A),
430
  EqSt sfx sfx' -> EqSt (history_rec pfx sfx) (history_rec pfx sfx').
431
Proof.
432
intros A.
433
cofix proof.
434
destruct sfx as (sfx0, sfxq).
435
destruct sfx' as (sfx0', sfxq').
436
intro H.
437
inversion H.
438
simpl in H0.
439
rewrite H0.
440
apply eqst.
441
 reflexivity.
442

    
443
 apply (proof _ sfxq sfxq').
444
 assumption.
445
Qed.
446

    
447
Theorem eqst_history : forall {A} (sfx sfx' : Stream A),
448
  EqSt sfx sfx' -> EqSt (history sfx) (history sfx').
449
Proof.
450
intros.
451
apply eqst_history_rec.
452
assumption.
453
Qed.
454

    
455
Theorem unzip_history_rec : forall {A} (pfx : list A) (sfx : Stream A), EqSt (snd (unzip (history_rec pfx sfx))) sfx.
456
Proof.
457
intro A.
458
cofix proof.
459
destruct sfx as (sfx0, sfx').
460
apply eqst.
461
 reflexivity.
462

    
463
 apply proof.
464
Qed.
465

    
466
Theorem unzip_history : forall {A} (s : Stream A), EqSt (snd (unzip (history s))) s.
467
Proof.
468
unfold history.
469
intros.
470
apply unzip_history_rec.
471
Qed.
472

    
473
Definition History_Spec {A} (s : Stream A) s' :=
474
     fst (hd (tl s')) = cons (snd (hd s')) (fst (hd s'))
475
  /\ EqSt (concat (fst (hd s')) (apply (lift (@snd _ _)) s')) s.
476

    
477
Theorem history_rec_spec : forall {A} p (s : Stream A),
478
     fst (hd (history_rec p s)) = p 
479
  /\ ForAll (fun s' => History_Spec (concat p s) s') (history_rec p s).
480
Proof.
481
intros.
482
split.
483
 destruct s.
484
 reflexivity.
485

    
486
 revert p s.
487
 cofix proof.
488
 destruct s as (s0, s').
489
 apply HereAndFurther.
490
  split.
491
   simpl.
492
   destruct s'.
493
   reflexivity.
494

    
495
   apply eqst_concat.
496
   apply unzip_history_rec.
497

    
498
  apply (proof (cons s0 p) s').
499
Qed.
500

    
501
Theorem history_spec : forall {A} (s : Stream A),
502
     fst (hd (history s)) = nil
503
  /\ ForAll (fun s' => History_Spec s s') (history s).
504
Proof.
505
intros.
506
generalize (history_rec_spec nil s).
507
intuition.
508
Qed.
509

    
510
Theorem history_rec_spec_complete : forall {A} p (s : Stream A) ps,
511
  fst (hd ps) = p -> ForAll (fun s' => History_Spec (concat p s) s') ps -> EqSt ps (history_rec p s).
512
Proof.
513
intro A.
514
cofix proof.
515
intros.
516
destruct s as (s0, s').
517
destruct ps as ((p_ps0, s_ps0), ps').
518
simpl in H.
519
subst.
520
inversion H0.
521
unfold History_Spec in H.
522
destruct H.
523
simpl in H.
524
apply eqst.
525
 simpl.
526
 intros.
527
 simpl in H.
528
 subst.
529
 inversion H0.
530
 unfold History_Spec in H.
531
 destruct H.
532
 simpl.
533
 simpl in H2.
534
 destruct (concat_eqst _ _ _ _ refl_equal H2).
535
 inversion H5.
536
 simpl in H6.
537
 subst.
538
 reflexivity.
539

    
540
 simpl.
541
 apply proof.
542
  simpl in H2.
543
  destruct (concat_eqst _ _ _ _ refl_equal H2).
544
  inversion H4.
545
  simpl in H5.
546
  subst.
547
  assumption.
548

    
549
  assumption.
550
Qed.
551

    
552
Theorem history_spec_complete : forall {A} (s : Stream A) ps,
553
  fst (hd ps) = nil -> ForAll (fun s' => History_Spec s s') ps -> EqSt ps (history s).
554
Proof.
555
intros.
556
apply history_rec_spec_complete.
557
 assumption.
558

    
559
 assumption.
560
Qed.
561

    
562
Theorem inv_snd_history_rec_intro : forall {A} (P : Stream A -> Prop) p (s : Stream A),
563
  ForAll P s -> ForAll (fun s' => P (apply (lift (@snd _ _)) s')) (history_rec p s).
564
Proof.
565
intros.
566
apply inv_map.
567
generalize (eqst_eq _ _ (unzip_history_rec p s)).
568
simpl.
569
intro Hs.
570
rewrite Hs.
571
exact H.
572
Qed.
573

    
574
Theorem inv_snd_history_intro : forall {A} (P : Stream A -> Prop) (s : Stream A),
575
  ForAll P s -> ForAll (fun s' => P (apply (lift (@snd _ _)) s')) (history s).
576
Proof.
577
intros.
578
apply inv_snd_history_rec_intro.
579
assumption.
580
Qed.
581

    
582
Theorem inv_snd_history_rec_elim : forall {A} (P : Stream A -> Prop) p (s : Stream A),
583
  ForAll (fun s' => P (apply (lift (@snd _ _)) s')) (history_rec p s) -> ForAll P s.
584
Proof.
585
intros.
586
rewrite <- (eqst_eq _ _ (unzip_history_rec p s)).
587
apply map_inv.
588
exact H.
589
Qed.
590

    
591
Theorem inv_snd_history_elim : forall {A} (P : Stream A -> Prop) (s : Stream A),
592
  ForAll (fun s' => P (apply (lift (@snd _ _)) s')) (history s) -> ForAll P s.
593
Proof.
594
intros.
595
apply inv_snd_history_rec_elim with (p := nil).
596
assumption.
597
Qed.
598

    
599
Fixpoint prefix {A} (I : A -> Prop) (T : A -> A -> Prop) (k : nat) : list A -> Prop :=
600
  match k with
601
  | 0    => fun p     => True
602
  | S k' => fun p =>
603
   match p with
604
   | List.nil         => True
605
   | List.cons t q =>
606
    match q with
607
    | List.nil        => (I t)
608
    | List.cons t' q' => (T t' t) /\ (prefix I T k' q)
609
    end
610
   end
611
  end.
612

    
613
Theorem prefix_mono_k : forall {A} I T k (p : list A), prefix I T (S k) p -> prefix I T k p.
614
Proof.
615
induction k.
616
 simpl.
617
 trivial.
618

    
619
 simpl.
620
 intuition.
621
 destruct p.
622
  trivial.
623

    
624
  intuition.
625
  destruct p.
626
   intuition.
627

    
628
   intuition.
629
Qed.
630

    
631
Theorem prefix_apply : forall {A} (I I' : A -> Prop) (T T' : A -> A -> Prop) k (p : list A),
632
  prefix I T k p -> prefix (fun s => I s -> I' s) (fun s s' => T s s' -> T' s s') k p -> prefix I' T' k p.
633
Proof.
634
intros A I I' T T'.
635
induction k.
636
 trivial.
637

    
638
 simpl.
639
 destruct p.
640
  trivial.
641

    
642
  destruct p.
643
   intuition.
644

    
645
   intuition.
646
Qed.
647

    
648
Theorem kinduction : forall {A} (P : A -> Prop) k (s : Stream A),
649
    ForAll (fun s' => prefix (fun st => P st) (fun st st' => P st') k (fst (hd s')) -> P (snd (hd s'))) (history s)
650
 -> ForAll (fun s' => P (hd s')) s.
651
Proof.
652
intros.
653
apply inv_snd_history_elim.
654
apply @ForAll_apply with (P := fun s' => P (snd (hd s'))).
655
 apply
656
  @ForAll_apply
657
   with
658
     (P := fun s' =>
659
           prefix (fun st => P st) (fun st st' => P st') k (fst (hd s'))).
660
  apply
661
   @ForAll_reinforce
662
    with
663
      (P := ForAll
664
              (fun s' : Stream (list A * A) =>
665
               prefix (fun st : A => P st) (fun _ st' : A => P st') k
666
                 (fst (hd s')) -> P (snd (hd s')))).
667
  apply
668
   @ForAll_reinforce
669
    with (P := ForAll (fun s' : Stream (list A * A) => History_Spec s s')).
670
  eapply ForAll_coind.
671
   intro.
672
   exact (fun x => x).
673

    
674
   destruct x as ((p0, s0), ((p1, s1), x'')).
675
   simpl.
676
   intuition.
677
    inversion H1.
678
    assumption.
679

    
680
    inversion H0.
681
    assumption.
682

    
683
    inversion H1.
684
    unfold History_Spec in H2.
685
    simpl in H2.
686
    destruct H2.
687
    rewrite H2.
688
    destruct k.
689
     simpl.
690
     trivial.
691

    
692
     simpl.
693
     inversion H0.
694
     simpl in H6.
695
     destruct p0.
696
      intuition.
697

    
698
      split.
699
       simpl in H3.
700
       apply H6.
701
       exact H3.
702

    
703
       apply prefix_mono_k.
704
       exact H3.
705

    
706
   simpl.
707
   intuition.
708
    generalize (history_spec s).
709
    intuition.
710

    
711
    destruct s.
712
    simpl.
713
    destruct k.
714
     simpl.
715
     trivial.
716

    
717
     simpl.
718
     trivial.
719

    
720
  exact H.
721

    
722
 apply necessitation.
723
 destruct s0.
724
 simpl.
725
 trivial.
726
Qed.
727

    
728
Theorem kinduction' :  forall {A} (P : A -> Prop) k ps (s : Stream A),
729
    fst (hd ps) = nil
730
 -> ForAll (fun s' => History_Spec s s') ps
731
 -> ForAll (fun s' => prefix (fun st => P st) (fun st st' => P st') k (fst (hd s')) -> P (snd (hd s'))) ps
732
 -> ForAll (fun s' => P (hd s')) s.
733
Proof.
734
intros.
735
rewrite (eqst_eq _ _ (history_spec_complete _ _ H H0)) in H1.
736
eapply kinduction.
737
apply H1.
738
Qed.
739

    
740
Theorem inv_prefix_history_rec : forall {A} (I : A -> Prop) (T : A -> A -> Prop) p (s : Stream A),
741
 ForAll (fun s' => T (hd s') (hd (tl s'))) (concat p s) ->
742
 forall k,
743
   prefix I T k (cons (hd s) p) ->
744
   ForAll (fun s' => prefix I T k (cons (snd (hd s')) (fst (hd s')))) (history_rec p s).
745
Proof.
746
intros A I T.
747
cofix proof.
748
intros.
749
inversion H.
750
destruct s as (s0, s').
751
apply HereAndFurther.
752
 assumption.
753

    
754
 simpl.
755
 apply proof.
756
  assumption.
757

    
758
  destruct k; simpl.
759
   trivial.
760

    
761
   split.
762
    generalize (inv_concat _ _ _ H).
763
    clear H; intro H.
764
    inversion H.
765
    assumption.
766

    
767
    apply prefix_mono_k.
768
    assumption.
769
Qed.
770

    
771
Theorem inv_prefix_history : forall {A} (I : A -> Prop) (T : A -> A -> Prop) (s : Stream A),
772
 I (hd s) -> ForAll (fun s' => T (hd s') (hd (tl s'))) s ->
773
 forall k,
774
 ForAll (fun s' => prefix I T k (cons (snd (hd s')) (fst (hd s')))) (history s).
775
Proof.
776
intros.
777
apply inv_prefix_history_rec.
778
 assumption.
779

    
780
 destruct k; simpl.
781
  trivial.
782

    
783
  assumption.
784
Qed.
785

    
786
Theorem inv_prefix_history' : forall {A} (I : A -> Prop) (T : A -> A -> Prop) (s : Stream A),
787
 I (hd s) -> ForAll (fun s' => T (hd s') (hd (tl s'))) s ->
788
 forall k,
789
 ForAll (fun s' => prefix I T k (fst (hd s'))) (history s).
790
Proof.
791
intros.
792
destruct k.
793
 apply necessitation.
794
 simpl.
795
 trivial.
796

    
797
 eapply ForAll_apply.
798
  apply (fun i n => inv_prefix_history I T s i n (S (S k))).
799
   apply H.
800

    
801
   apply H0.
802

    
803
  apply necessitation.
804
  destruct s0 as ((p0, s0), s').
805
  simpl.
806
  destruct p0.
807
   trivial.
808

    
809
   intuition.
810
Qed.
811

    
812

    
813
Definition effective {A : Type} (r : relation A) :=
814
 forall a1 a2, { r a1 a2 } + { ~ r a1 a2 }.
815

    
816
Definition lift_hd {A : Type} (r : relation A) : relation (Stream A) :=
817
 fun s1 => fun s2 => r (hd s1) (hd s2).
818

    
819
Theorem lift_hd_effective : forall {A : Type} {r : relation A},
820
 effective r -> effective (lift_hd r).
821
Proof.
822
unfold effective, lift_hd in |- *.
823
intros A r H s1 s2.
824
destruct s1; destruct s2.
825
apply H.
826
Defined.
827

    
828
Section FixedPoint.
829

    
830
Variable A : Type.
831

    
832
Variable union : A -> A -> A.
833

    
834
Variable le : relation A.
835

    
836
Hypothesis le_mono : forall x y, le x (union x y).
837

    
838
Hypothesis le_eff : effective le.
839

    
840
Definition gt x y := le y x /\ ~ le x y.
841

    
842
Hypothesis gt_wf : well_founded gt.
843

    
844
Program Fixpoint rec_hd (f : Stream A -> Stream A) (s : Stream A) { wf (lift_hd gt) s } : Stream A :=
845
 let s' := apply (apply (lift union) s) (f s) in
846
 if (lift_hd_effective le_eff s' s)
847
 then s'
848
 else rec_hd f s'.
849

    
850
Obligation 1.
851
Proof.
852
unfold lift_hd.
853
rewrite hd_apply.
854
rewrite hd_apply.
855
rewrite hd_lift.
856
unfold gt.
857
split.
858
 apply le_mono.
859

    
860
 unfold lift_hd in H.
861
 rewrite hd_apply in H.
862
 rewrite hd_apply in H.
863
 rewrite hd_lift in H.
864
 exact H.
865
Qed.
866

    
867
Obligation 2.
868
Proof.
869
unfold MR.
870
apply wf_inverse_image.
871
unfold lift_hd.
872
apply wf_inverse_image.
873
assumption.
874
Defined.
875

    
876
CoFixpoint rec (f : Stream A -> Stream A) (s : Stream A) : Stream A :=
877
 let s' := rec_hd f s in Cons (hd s') (rec f (tl s')).
878

    
879
End FixedPoint.
880

    
881
Arguments gt {A} _ _ _.
882

    
883
Arguments rec {A} _ _ _ _ _ _ _.