Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / optim / lustre.v @ 6a93d814

History | View | Annotate | Download (11.8 KB)

1
Require Import Arith.
2
Require Import Omega.
3
Require Import Bool.
4
Require Import Compare_dec.
5
Require Import Wf_nat.
6
Require Import Wellfounded.
7
Require Import Relation_Definitions.
8
Require Import Recdef.
9
Require Import StreamsLib.
10

    
11
Lemma eq_Z_effective : effective (fun (x y : Z) => x = y).
12
Proof.
13
unfold effective.
14
repeat decide equality.
15
Qed.
16

    
17
Lemma eq_bool_effective : effective (fun (x y : bool) => x = y).
18
Proof.
19
unfold effective.
20
repeat decide equality.
21
Qed.
22

    
23
Lemma eq_unit_effective : effective (fun (x y : unit) => x = y).
24
Proof.
25
unfold effective.
26
repeat decide equality.
27
Qed.
28

    
29
Lemma eq_pair_effective : forall {A B},
30
 effective (fun (x y : A) => x = y) -> effective (fun (x y : B) => x = y) -> effective (fun (x y : A * B) => x = y).
31
Proof.
32
unfold effective.
33
repeat decide equality.
34
Qed.
35

    
36
Definition par {A B} (rA : relation A) (rB : relation B) := fun ab ab' => rA (fst ab) (fst ab') /\ rB (snd ab) (snd ab').
37

    
38
Theorem gt_par_comm : forall {A B} (leA : relation A) (leB : relation B),
39
 inclusion _ (par (gt leA) (gt leB)) (gt (par leA leB)) .
40
Proof.
41
unfold gt, par, inclusion.
42
intuition.
43
Qed.
44

    
45
Theorem wf_par : forall {A B} (rA : relation A) (rB : relation B),
46
 well_founded rA -> well_founded rB -> well_founded (par rA rB).
47
Proof.
48
unfold well_founded, par.
49
intros A B rA rB.
50
intros Ha Hb ab.
51
destruct ab as (a, b).
52
revert Hb b.
53
induction (Ha a).
54
intros.
55
apply Acc_intro.
56
intros.
57
destruct y.
58
apply H0.
59
 intuition.
60

    
61
 assumption.
62
Qed.
63

    
64
Theorem wf_gt_par : forall {A B} (rA : relation A) (rB : relation B),
65
 well_founded (gt rA) -> well_founded (gt rB) -> well_founded (par (gt rA) (gt rB)).
66
Proof.
67
unfold well_founded, par, gt.
68
intros A B rA rB.
69
intros Ha Hb ab.
70
destruct ab as (a, b).
71
revert Hb b.
72
induction (Ha a).
73
intros.
74
apply Acc_intro.
75
destruct y.
76
intuition.
77
Qed.
78

    
79
Definition cross {A B C D} (f : A -> B) (g : C -> D) : A * C -> B * D := fun ac => (f (fst ac), g (snd ac)).
80

    
81
Theorem le_par : forall {A B} (leA : relation A) (leB : relation B) (f : A -> A) (g : B -> B) a b,
82
 leA a (f a) -> leB b (g b) -> (par leA leB) (a, b) ((cross f g) (a, b)).
83
Proof.
84
unfold par, cross.
85
intuition.
86
Qed.
87

    
88
Lemma rel_pair_effective : forall {A B} {rA : relation A} {rB : relation B},
89
 effective rA -> effective rB -> effective (par rA rB).
90
Proof.
91
unfold effective.
92
intros.
93
unfold par.
94
destruct a1.
95
destruct a2.
96
destruct (X a a0).
97
 destruct (X0 b b0).
98
  intuition.
99

    
100
  intuition.
101

    
102
 intuition.
103
Qed.
104

    
105
Inductive element {A : Type} : Type :=
106
| Bot : @element A
107
| Elt : A -> @element A
108
| Top : @element A.
109

    
110
Definition measure_elt {A} (e : @element A) : nat :=
111
 match e with
112
 | Bot   => 2
113
 | Elt _ => 1
114
 | Top   => 0
115
 end.
116

    
117
Definition union_elt {A} (eqA : effective (fun x y => x = y)) (e1 e2 : @element A) : @element A :=
118
 match (e1, e2) with
119
 | (Bot   , _     ) => e2
120
 | (_     , Bot   ) => e1
121
 | (Elt a1, Elt a2) => if eqA a1 a2 then Elt a1 else Top
122
 | (_     , _     ) => Top
123
 end.
124

    
125
Definition apply_elt {A B} (ef : @element (A -> B)) (ex : @element A) : @element B :=
126
 match (ef, ex) with
127
 | (Top  , _    ) => Top
128
 | (_    , Top  ) => Top
129
 | (Bot  , _    ) => Bot
130
 | (_    , Bot  ) => Bot
131
 | (Elt f, Elt x) => Elt (f x)
132
 end.
133

    
134
Definition merge_elt {A} (ec : @element bool) (e1 e2 : @element A) : @element A :=
135
 match (e1, e2) with
136
 | (Bot   , _     ) => e2
137
 | (_     , Bot   ) => e1
138
 | (_     , _     ) => Top
139
 end.
140

    
141
Definition when_elt {A} (e1 : @element A) (e2 : @element bool) : @element A :=
142
 match (e1, e2) with
143
 | (_     , Top     ) => Top
144
 | (Top   , _       ) => Top
145
 | (_     , Elt true) => e1
146
 | (_     , _       ) => Bot
147
 end.
148

    
149
Definition ite_elt {A} (e1 : @element bool) (e2 : @element A) (e3 : @element A) : @element A :=
150
 match (e1, e2, e3) with
151
 | (Top      , _  , _  ) => Top
152
 | (_        , Top, _  ) => Top
153
 | (_        , _  , Top) => Top
154
 | (Elt true , _  , _  ) => e2
155
 | (Elt false, _  , _  ) => e3
156
 | (Bot      , _  , _  ) => Bot
157
 end.
158

    
159
Definition undef {A} := lift (@Bot A).
160

    
161
Fixpoint slice {A} (s : Stream (@element A)) (n : nat) {struct n} : Stream (@element A) :=
162
 match n with
163
 | O   => undef
164
 | S p => Cons (hd s) (slice (tl s) p)
165
 end.
166

    
167
Theorem slice_bisim : forall {A} (s1 s2 : Stream (@element A)), EqSt s1 s2 -> forall n, EqSt (slice s1 n) (slice s2 n).
168
Proof.
169
cofix proof.
170
destruct s1; destruct s2; intros.
171
destruct n; simpl.
172
 apply EqSt_reflex.
173
 
174
 inversion H.
175
 apply eqst.
176
  exact H0.
177
  
178
  apply proof.
179
  exact H1.
180
Qed.
181

    
182
Definition bisim_upto {A} (n : nat) : relation (Stream (@element A)) :=
183
 fun s1 => fun s2 => EqSt (slice s1 n) (slice s2 n).
184

    
185
Theorem bisim_bisim_upto : forall {A} (s1 s2 : Stream (@element A)), 
186
 EqSt s1 s2 -> forall n, bisim_upto n s1 s2.
187
Proof.
188
unfold bisim_upto.
189
cofix proof.
190
intros.
191
destruct s1; destruct s2.
192
destruct n; simpl.
193
 apply EqSt_reflex.
194
 
195
 inversion H.
196
 apply eqst.
197
  exact H0.
198
  
199
  apply proof.
200
  exact H1.
201
Qed.
202

    
203
Theorem bisim_upto_bisim : forall {A} (s1 s2 : Stream (@element A)), 
204
 (forall n, bisim_upto n s1 s2) -> EqSt s1 s2.
205
Proof.
206
unfold bisim_upto.
207
cofix proof.
208
intros.
209
destruct s1; destruct s2.
210
apply eqst.
211
 destruct (H 1).
212
 exact H0.
213
 
214
 apply proof.
215
 intro n.
216
 destruct (H (S n)).
217
 assumption.
218
Qed.
219

    
220
Definition le_elt {A} (e1 e2 : @element A) :=
221
 measure_elt e1 >= measure_elt e2.
222

    
223
Theorem le_elt_mono : forall {A} eqA (x y : @element A), le_elt x (union_elt eqA x y).
224
Proof.
225
unfold le_elt.
226
destruct x; destruct y; simpl; auto with arith.
227
unfold union_elt.
228
destruct eqA; auto with arith.
229
Qed.
230

    
231
Theorem le_elt_effective : forall {A}, effective (@le_elt A).
232
Proof.
233
unfold effective, le_elt.
234
intros A a1 a2.
235
apply ge_dec.
236
Qed.
237

    
238
Theorem gt_elt_acc : forall {A}, well_founded (gt (@le_elt A)).
239
Proof.
240
unfold gt, le_elt.
241
intro A.
242
eapply wf_incl.
243
 intros x y H.
244
 destruct H.
245
 apply not_ge.
246
 apply H0.
247

    
248
 eapply well_founded_lt_compat.
249
 intros x y H.
250
 apply H.
251
Qed.
252

    
253
(*
254
Definition lt_elt {A} (e1 e2 : @element A) :=
255
 measure_elt e1 > measure_elt e2.
256

    
257
Theorem not_le_lt_elt : forall {A} (e1 e2 : @element A),
258
 ~ le_elt e1 e2 -> lt_elt e2 e1.
259
Proof.
260
unfold le_elt, lt_elt.
261
intros.
262
omega.
263
Qed.
264

    
265
Theorem lt_not_le_elt : forall {A} (e1 e2 : @element A),
266
 lt_elt e1 e2 -> ~ le_elt e2 e1.
267
Proof.
268
unfold le_elt, lt_elt.
269
intros.
270
omega.
271
Qed.
272

    
273
Definition gt_elt {A} (e1 e2 : @element A) := lt_elt e2 e1.
274

    
275
Theorem le_elt_dec : forall {A} (e1 e2 : @element A), { le_elt e1 e2 } + { lt_elt e2 e1 }.
276
Proof.
277
unfold lt_elt, le_elt, ge in |- *.
278
intros.
279
apply le_lt_dec.
280
Qed.
281

    
282
Theorem le_elt_effective : forall {A}, effective (@element A) le_elt.
283
Proof.
284
unfold effective in |- *.
285
intros A a1 a2.
286
destruct (le_elt_dec a1 a2).
287
 left; assumption.
288
 
289
 right; apply lt_not_le_elt; assumption.
290
Defined.
291

    
292
Theorem gt_elt_acc : forall {A}, well_founded (gt (@le_elt A)).
293
Proof.
294
unfold gt_elt, lt_elt in |- *.
295
intro A.
296
eapply well_founded_lt_compat.
297
unfold gt in |- *.
298
intros x y H.
299
apply H.
300
Qed.
301

    
302
Theorem gt_hd_acc : forall {A}, well_founded (lift_hd (@element A) gt_elt).
303
Proof.
304
intro A.
305
unfold lift_hd.
306
apply wf_inverse_image.
307
exact gt_elt_acc.
308
Qed.
309
*)
310

    
311
Fixpoint list2type (l : list Set) : Set :=
312
 match l with
313
 | nil => unit
314
 | cons t q => (t * list2type q)%type
315
 end.
316

    
317
Module Signal.
318

    
319
Definition t A := Stream (@element A).
320

    
321
Definition clock := Stream bool.
322

    
323
(*
324
Variable A : Set.
325

    
326
Variable eqA_effective : effective A (fun x y => x=y).
327

    
328
Theorem eq_elt_effective : effective element (fun x y => x=y).
329
Proof.
330
unfold effective in |- *.
331
unfold effective in eqA_effective.
332
decide equality.
333
Defined.
334
*)
335

    
336
Definition union {A} eqA (s1 s2 : t A) := apply (apply (lift (union_elt eqA)) s1) s2.
337

    
338

    
339

    
340
Definition loop {A} eqA (f : t A -> t A) : t A :=
341
 rec eqA f undef.
342

    
343
Definition lift {A} (v : A) : t A := lift (Elt v).
344

    
345
Definition apply {A B} (f : t (A -> B)) (a : t A) : t B :=
346
 StreamsLib.apply (StreamsLib.apply (StreamsLib.lift (@apply_elt A B)) f) a.
347

    
348
Definition when {A} (s : t A) (w : t bool) : t A := StreamsLib.apply (StreamsLib.apply (StreamsLib.lift (@when_elt A)) s) w.
349

    
350
CoFixpoint pre {A} (old : @element A) (s : t A) : t A := 
351
 Cons old (pre (hd s) (tl s)).
352

    
353
Definition _arrow : t bool := Cons (Elt true) (lift false).
354

    
355
Definition ite {A} (s_if : t bool) (s_then s_else : t A) : t A :=
356
 StreamsLib.apply (StreamsLib.apply (StreamsLib.apply (StreamsLib.lift (@ite_elt A)) s_if) s_then) s_else.
357

    
358
Lemma hd_ite : forall {A}, forall (cs : t bool) (ts es : t A),
359
 hd (ite cs ts es) = ite_elt (hd cs) (hd ts) (hd es).
360
Proof.
361
destruct cs; destruct ts; destruct es.
362
reflexivity.
363
Qed.
364

    
365
Lemma tl_ite : forall {A}, forall (cs : t bool) (ts es : t A),
366
 tl (ite cs ts es) = ite (tl cs) (tl ts) (tl es).
367
Proof.
368
destruct cs; destruct ts; destruct es.
369
reflexivity.
370
Qed.
371

    
372
Theorem eqst_ite : forall {A}, forall (c1 c2 : t bool) (t1 t2 e1 e2 : t A),
373
 EqSt c1 c2 -> EqSt t1 t2 -> EqSt e1 e2 -> EqSt (ite c1 t1 e1) (ite c2 t2 e2).
374
Proof.
375
intros.
376
apply eqst_apply.
377
 apply eqst_apply.
378
  apply eqst_apply.
379
   apply EqSt_reflex.
380

    
381
   assumption.
382

    
383
  assumption.
384

    
385
 assumption.
386
Qed.
387

    
388
Definition correct {A} (s : t A) := ForAll (fun s => ~ hd s = Top) s.
389

    
390
Definition causal {A B} (f : t A -> t B) :=
391
 forall (s1 s2 : t A) n, bisim_upto n s1 s2 -> bisim_upto n (f s1) (f s2).
392

    
393
End Signal.
394

    
395
Require Import Bool.
396

    
397
Definition bnot (s : Stream bool) := apply (lift negb) s.
398

    
399
Definition band (s1 s2 : Stream bool) := apply (apply (lift andb) s1) s2.
400

    
401
Definition bor (s1 s2 : Stream bool) := apply (apply (lift orb) s1) s2.
402

    
403
Require Import ZArith.
404

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

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

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

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

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

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

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

    
419
(* sémantiques du noeud f:
420

    
421
 node f(x : int) returns (y, cpt : int)
422
 let
423
   y = x + 1;
424
   cpt = (0 -> pre cpt)+ 1;
425
 tel
426
*)
427

    
428
Definition denot_f (x : Signal.t Z) :=
429
  Signal.loop
430
    (eq_pair_effective eq_Z_effective eq_Z_effective)
431
    (fun y_cpt => let (y , cpt)  := unzip y_cpt in
432
                  let y'   := iplus x (Signal.lift 1%Z) in
433
                  let cpt' := iplus (Signal.ite Signal._arrow (lift 0%Z) (Signal.pre cpt)) (lift 1%Z) in
434
                  zip (y', cpt')).
435

    
436
(* sémantique dénotationnelle de f *)
437
Definition denot_f (x cpt y : Stream Z) :=
438
 (EqSt y (iplus x (lift 1%Z))) /\ (EqSt cpt (iplus (ite _arrow (lift 0%Z) (pre cpt)) (lift 1%Z))).
439

    
440
(* sémantique axiomatique de f, simplifiée *)
441

    
442
Definition mem_f := (bool * Z)%type.
443

    
444
Definition ni_2 (mem : mem_f) := fst mem.
445

    
446
Definition __f_2 (mem : mem_f) := snd mem.
447

    
448
Definition init_f (mem : mem_f) := ni_2 mem = true.
449

    
450
Definition trans_f (x cpt y : Z) (mem_in mem_out : mem_f) :=
451
    (cpt = ((if bool_dec (ni_2 mem_in) true then 0 else (__f_2 mem_in)) + 1)%Z)
452
 /\ (y   = (x + 1)%Z)
453
 /\ (ni_2 mem_out) = false
454
 /\ (__f_2 mem_out) = cpt.
455

    
456
Definition trans_f' (s s' : (Z * (Z * Z)) * mem_f) :=
457
 match s, s' with
458
 | ((x, (cpt, y)), mem), ((x', (cpt', y')), mem') => trans_f x cpt y mem mem'
459
 end.
460

    
461
Lemma Cons_inj : forall {A}, forall a a' (s s' : Stream A), Cons a s = Cons a' s' -> a = a' /\ s = s'.
462
Proof.
463
intros.
464
injection H.
465
intuition.
466
Qed.
467

    
468
Theorem raffinement : forall (x cpt y : Stream Z) (mem : Stream mem_f),
469
         (init_f (hd mem) /\ transition trans_f' (zip ((zip (x, (zip (cpt, y)))), mem)))
470
         ->
471
         denot_f x cpt y.
472
Proof.
473
intros.
474
apply zip_pair.
475
revert x cpt y mem H.
476
cofix proof.
477
intros.
478

    
479

    
480

    
481
intros.
482
split.
483
 revert x cpt y mem H.
484
 cofix proof.
485
 intros.
486
 destruct H.
487
 destruct x as (x0, x'); destruct cpt as (cpt0, cpt'); destruct y as (y0, y').
488
 destruct mem as (mem0, mem').
489
 inversion H0.
490
 apply eqst.
491
  simpl.
492
  unfold zip in H1.
493
  simpl in H1.
494
  generalize (f_equal (@hd _) H1).
495
  simpl.
496
  intro.
497
  subst.
498
  generalize (f_equal (@tl _) H1).
499
  simpl.
500

    
501
Qed. 
502

    
503