Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

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

History | View | Annotate | Download (13 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
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