summaryrefslogtreecommitdiff
path: root/common/Behaviors.v
blob: 454ea341c1094684c28d1a6e2c015296e0914fe9 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
(* *********************************************************************)
(*                                                                     *)
(*              The Compcert verified compiler                         *)
(*                                                                     *)
(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
(*                                                                     *)
(*  Copyright Institut National de Recherche en Informatique et en     *)
(*  Automatique.  All rights reserved.  This file is distributed       *)
(*  under the terms of the GNU General Public License as published by  *)
(*  the Free Software Foundation, either version 2 of the License, or  *)
(*  (at your option) any later version.  This file is also distributed *)
(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
(*                                                                     *)
(* *********************************************************************)

(** Whole-program behaviors *)

Require Import Classical.
Require Import ClassicalEpsilon.
Require Import Coqlib.
Require Import AST.
Require Import Events.
Require Import Globalenvs.
Require Import Integers.
Require Import Smallstep.

Set Implicit Arguments.

(** * Behaviors for program executions *)

(** The four possible outcomes for the execution of a program:
- Termination, with a finite trace of observable events
  and an integer value that stands for the process exit code
  (the return value of the main function).
- Divergence with a finite trace of observable events.
  (At some point, the program runs forever without doing any I/O.)
- Reactive divergence with an infinite trace of observable events.
  (The program performs infinitely many I/O operations separated
   by finite amounts of internal computations.)
- Going wrong, with a finite trace of observable events
  performed before the program gets stuck.
*)

Inductive program_behavior: Type :=
  | Terminates: trace -> int -> program_behavior
  | Diverges: trace -> program_behavior
  | Reacts: traceinf -> program_behavior
  | Goes_wrong: trace -> program_behavior.

(** Operations and relations on behaviors *)

Definition not_wrong (beh: program_behavior) : Prop :=
  match beh with
  | Terminates _ _ => True
  | Diverges _ => True
  | Reacts _ => True
  | Goes_wrong _ => False
  end.

Definition behavior_app (t: trace) (beh: program_behavior): program_behavior :=
  match beh with
  | Terminates t1 r => Terminates (t ** t1) r
  | Diverges t1 => Diverges (t ** t1)
  | Reacts T => Reacts (t *** T)
  | Goes_wrong t1 => Goes_wrong (t ** t1)
  end.

Lemma behavior_app_assoc:
  forall t1 t2 beh,
  behavior_app (t1 ** t2) beh = behavior_app t1 (behavior_app t2 beh).
Proof.
  intros. destruct beh; simpl; f_equal; traceEq. 
Qed.

Lemma behavior_app_E0:
  forall beh, behavior_app E0 beh = beh.
Proof.
  destruct beh; auto.
Qed.

Definition behavior_prefix (t: trace) (beh: program_behavior) : Prop :=
  exists beh', beh = behavior_app t beh'.

Definition behavior_improves (beh1 beh2: program_behavior) : Prop :=
  beh1 = beh2 \/ exists t, beh1 = Goes_wrong t /\ behavior_prefix t beh2.

Lemma behavior_improves_refl:
  forall beh, behavior_improves beh beh.
Proof.
  intros; red; auto.
Qed.

Lemma behavior_improves_trans:
  forall beh1 beh2 beh3, 
  behavior_improves beh1 beh2 -> behavior_improves beh2 beh3 ->
  behavior_improves beh1 beh3.
Proof.
  intros. red. destruct H; destruct H0; subst; auto. 
  destruct H as [t1 [EQ1 [beh2' EQ1']]].
  destruct H0 as [t2 [EQ2 [beh3' EQ2']]].
  subst. destruct beh2'; simpl in EQ2; try discriminate. inv EQ2. 
  right. exists t1; split; auto. exists (behavior_app t beh3'). apply behavior_app_assoc.
Qed.

Lemma behavior_improves_bot:
  forall beh, behavior_improves (Goes_wrong E0) beh.
Proof.
  intros. right. exists E0; split; auto. exists beh. rewrite behavior_app_E0; auto.
Qed.

Lemma behavior_improves_app:
  forall t beh1 beh2,
  behavior_improves beh1 beh2 ->
  behavior_improves (behavior_app t beh1) (behavior_app t beh2).
Proof.
  intros. red; destruct H. left; congruence. 
  destruct H as [t' [A [beh' B]]]. subst.
  right; exists (t ** t'); split; auto. exists beh'. rewrite behavior_app_assoc; auto.
Qed.

(** Associating behaviors to programs. *)

Section PROGRAM_BEHAVIORS.

Variable L: semantics.

Inductive state_behaves (s: state L): program_behavior -> Prop :=
  | state_terminates: forall t s' r,
      Star L s t s' ->
      final_state L s' r ->
      state_behaves s (Terminates t r)
  | state_diverges: forall t s',
      Star L s t s' -> Forever_silent L s' ->
      state_behaves s (Diverges t)
  | state_reacts: forall T,
      Forever_reactive L s T ->
      state_behaves s (Reacts T)
  | state_goes_wrong: forall t s',
      Star L s t s' ->
      Nostep L s' ->
      (forall r, ~final_state L s' r) ->
      state_behaves s (Goes_wrong t).

Inductive program_behaves: program_behavior -> Prop :=
  | program_runs: forall s beh,
      initial_state L s -> state_behaves s beh ->
      program_behaves beh
  | program_goes_initially_wrong:
      (forall s, ~initial_state L s) ->
      program_behaves (Goes_wrong E0).

Lemma state_behaves_app:
  forall s1 t s2 beh,
  Star L s1 t s2 -> state_behaves s2 beh -> state_behaves s1 (behavior_app t beh).
Proof.
  intros. inv H0; simpl; econstructor; eauto; try (eapply star_trans; eauto). 
  eapply star_forever_reactive; eauto.
Qed.

(** * Existence of behaviors *)

(** We now show that any program admits at least one behavior.
  The proof requires classical logic: the axiom of excluded middle
  and an axiom of description. *)

(** The most difficult part of the proof is to show the existence
  of an infinite trace in the case of reactive divergence. *)

Section TRACEINF_REACTS.

Variable s0: state L.

Hypothesis reacts:
  forall s1 t1, Star L s0 t1 s1 ->
  exists s2, exists t2, Star L s1 t2 s2 /\ t2 <> E0.

Lemma reacts':
  forall s1 t1, Star L s0 t1 s1 ->
  { s2 : state L & { t2 : trace | Star L s1 t2 s2 /\ t2 <> E0 } }.
Proof.
  intros. 
  destruct (constructive_indefinite_description _ (reacts H)) as [s2 A].
  destruct (constructive_indefinite_description _ A) as [t2 [B C]].
  exists s2; exists t2; auto.
Qed.

CoFixpoint build_traceinf' (s1: state L) (t1: trace) (ST: Star L s0 t1 s1) : traceinf' :=
  match reacts' ST with
  | existT s2 (exist t2 (conj A B)) =>
      Econsinf' t2 
                (build_traceinf' (star_trans ST A (refl_equal _)))
                B
  end.

Lemma reacts_forever_reactive_rec:
  forall s1 t1 (ST: Star L s0 t1 s1),
  Forever_reactive L s1 (traceinf_of_traceinf' (build_traceinf' ST)).
Proof.
  cofix COINDHYP; intros.
  rewrite (unroll_traceinf' (build_traceinf' ST)). simpl. 
  destruct (reacts' ST) as [s2 [t2 [A B]]]. 
  rewrite traceinf_traceinf'_app. 
  econstructor. eexact A. auto. apply COINDHYP. 
Qed.

Lemma reacts_forever_reactive:
  exists T, Forever_reactive L s0 T.
Proof.
  exists (traceinf_of_traceinf' (build_traceinf' (star_refl (step L) (globalenv L) s0))).
  apply reacts_forever_reactive_rec.
Qed.

End TRACEINF_REACTS.

Lemma diverges_forever_silent:
  forall s0,
  (forall s1 t1, Star L s0 t1 s1 -> exists s2, Step L s1 E0 s2) ->
  Forever_silent L s0.
Proof.
  cofix COINDHYP; intros. 
  destruct (H s0 E0) as [s1 ST]. constructor. 
  econstructor. eexact ST. apply COINDHYP. 
  intros. eapply H. eapply star_left; eauto.
Qed.

Lemma state_behaves_exists:
  forall s, exists beh, state_behaves s beh.
Proof.
  intros s0.
  destruct (classic (forall s1 t1, Star L s0 t1 s1 -> exists s2, exists t2, Step L s1 t2 s2)).
(* 1 Divergence (silent or reactive) *)
  destruct (classic (exists s1, exists t1, Star L s0 t1 s1 /\
                       (forall s2 t2, Star L s1 t2 s2 ->
                        exists s3, Step L s2 E0 s3))).
(* 1.1 Silent divergence *)
  destruct H0 as [s1 [t1 [A B]]].
  exists (Diverges t1); econstructor; eauto. 
  apply diverges_forever_silent; auto.
(* 1.2 Reactive divergence *)
  destruct (@reacts_forever_reactive s0) as [T FR].
  intros.
  generalize (not_ex_all_not _ _ H0 s1). intro A; clear H0.
  generalize (not_ex_all_not _ _ A t1). intro B; clear A.
  destruct (not_and_or _ _ B). contradiction. 
  destruct (not_all_ex_not _ _ H0) as [s2 C]; clear H0. 
  destruct (not_all_ex_not _ _ C) as [t2 D]; clear C.
  destruct (imply_to_and _ _ D) as [E F]; clear D.
  destruct (H s2 (t1 ** t2)) as [s3 [t3 G]]. eapply star_trans; eauto. 
  exists s3; exists (t2 ** t3); split.
  eapply star_right; eauto. 
  red; intros. destruct (app_eq_nil t2 t3 H0). subst. elim F. exists s3; auto.
  exists (Reacts T); econstructor; eauto.
(* 2 Termination (normal or by going wrong) *)
  destruct (not_all_ex_not _ _ H) as [s1 A]; clear H.
  destruct (not_all_ex_not _ _ A) as [t1 B]; clear A.
  destruct (imply_to_and _ _ B) as [C D]; clear B.
  destruct (classic (exists r, final_state L s1 r)) as [[r FINAL] | NOTFINAL].
(* 2.1 Normal termination *)
  exists (Terminates t1 r); econstructor; eauto.
(* 2.2 Going wrong *)
  exists (Goes_wrong t1); econstructor; eauto. red. intros. 
  generalize (not_ex_all_not _ _ D s'); intros. 
  generalize (not_ex_all_not _ _ H t); intros. 
  auto.
Qed.

Theorem program_behaves_exists:
  exists beh, program_behaves beh.
Proof.
  destruct (classic (exists s, initial_state L s)) as [[s0 INIT] | NOTINIT].
(* 1. Initial state is defined. *)
  destruct (state_behaves_exists s0) as [beh SB].
  exists beh; econstructor; eauto. 
(* 2. Initial state is undefined *)
  exists (Goes_wrong E0). apply program_goes_initially_wrong. 
  intros. eapply not_ex_all_not; eauto. 
Qed.

End PROGRAM_BEHAVIORS.

(** * Forward simulations and program behaviors *)

Section FORWARD_SIMULATIONS.

Variable L1: semantics.
Variable L2: semantics.
Variable S: forward_simulation L1 L2.

Lemma forward_simulation_state_behaves:
  forall i s1 s2 beh1,
  S i s1 s2 -> state_behaves L1 s1 beh1 ->
  exists beh2, state_behaves L2 s2 beh2 /\ behavior_improves beh1 beh2.
Proof.
  intros. inv H0. 
(* termination *)
  exploit simulation_star; eauto. intros [i' [s2' [A B]]].
  exists (Terminates t r); split.
  econstructor; eauto. eapply fsim_match_final_states; eauto.
  apply behavior_improves_refl.
(* silent divergence *)
  exploit simulation_star; eauto. intros [i' [s2' [A B]]].
  exists (Diverges t); split.
  econstructor; eauto. eapply simulation_forever_silent; eauto.
  apply behavior_improves_refl.
(* reactive divergence *)
  exists (Reacts T); split.
  econstructor. eapply simulation_forever_reactive; eauto.
  apply behavior_improves_refl.
(* going wrong *)
  exploit simulation_star; eauto. intros [i' [s2' [A B]]].
  destruct (state_behaves_exists L2 s2') as [beh' SB].
  exists (behavior_app t beh'); split. 
  eapply state_behaves_app; eauto. 
  replace (Goes_wrong t) with (behavior_app t (Goes_wrong E0)).
  apply behavior_improves_app. apply behavior_improves_bot. 
  simpl. decEq. traceEq.
Qed.

Theorem forward_simulation_behavior_improves:
  forall beh1, program_behaves L1 beh1 ->
  exists beh2, program_behaves L2 beh2 /\ behavior_improves beh1 beh2.
Proof.
  intros. inv H.
(* initial state defined *)
  exploit (fsim_match_initial_states S); eauto. intros [i [s' [INIT MATCH]]].
  exploit forward_simulation_state_behaves; eauto. intros [beh2 [A B]].
  exists beh2; split; auto. econstructor; eauto.
(* initial state undefined *)
  destruct (classic (exists s', initial_state L2 s')).
  destruct H as [s' INIT]. 
  destruct (state_behaves_exists L2 s') as [beh' SB].
  exists beh'; split. econstructor; eauto. apply behavior_improves_bot.
  exists (Goes_wrong E0); split.
  apply program_goes_initially_wrong. 
  intros; red; intros. elim H; exists s; auto.
  apply behavior_improves_refl.
Qed.

Corollary forward_simulation_same_safe_behavior:
  forall beh,
  program_behaves L1 beh -> not_wrong beh ->
  program_behaves L2 beh.
Proof.
  intros. exploit forward_simulation_behavior_improves; eauto. 
  intros [beh' [A B]]. destruct B. 
  congruence.
  destruct H1 as [t [C D]]. subst. contradiction.
Qed.

End FORWARD_SIMULATIONS.

(** * Backward simulations and program behaviors *)

Section BACKWARD_SIMULATIONS.

Variable L1: semantics.
Variable L2: semantics.
Variable S: backward_simulation L1 L2.

Definition safe_along_behavior (s: state L1) (b: program_behavior) : Prop :=
  forall t1 s' b2, Star L1 s t1 s' -> b = behavior_app t1 b2 ->
     (exists r, final_state L1 s' r)
  \/ (exists t2, exists s'', Step L1 s' t2 s'').

Remark safe_along_safe:
  forall s b, safe_along_behavior s b -> safe L1 s.
Proof.
  intros; red; intros. eapply H; eauto. symmetry; apply behavior_app_E0. 
Qed.

Remark star_safe_along:
  forall s b t1 s' b2,
  safe_along_behavior s b ->
  Star L1 s t1 s' -> b = behavior_app t1 b2 ->
  safe_along_behavior s' b2.
Proof.
  intros; red; intros. eapply H. eapply star_trans; eauto.
  subst. rewrite behavior_app_assoc. eauto.
Qed.

Remark not_safe_along_behavior:
  forall s b,
  ~ safe_along_behavior s b ->
  exists t, exists s',
     behavior_prefix t b 
  /\ Star L1 s t s'
  /\ Nostep L1 s'
  /\ (forall r, ~(final_state L1 s' r)).
Proof.
  intros. 
  destruct (not_all_ex_not _ _ H) as [t1 A]; clear H.
  destruct (not_all_ex_not _ _ A) as [s' B]; clear A.
  destruct (not_all_ex_not _ _ B) as [b2 C]; clear B.
  destruct (imply_to_and _ _ C) as [D E]; clear C.
  destruct (imply_to_and _ _ E) as [F G]; clear E.
  destruct (not_or_and _ _ G) as [P Q]; clear G.
  exists t1; exists s'. 
  split. exists b2; auto. 
  split. auto. 
  split. red; intros; red; intros. elim Q. exists t; exists s'0; auto.
  intros; red; intros. elim P. exists r; auto.
Qed.

Lemma backward_simulation_star:
  forall s2 t s2', Star L2 s2 t s2' ->
  forall i s1 b, S i s1 s2 -> safe_along_behavior s1 (behavior_app t b) ->
  exists i', exists s1', Star L1 s1 t s1' /\ S i' s1' s2'.
Proof.
  induction 1; intros.
  exists i; exists s1; split; auto. apply star_refl.
  exploit (bsim_simulation S); eauto. eapply safe_along_safe; eauto. 
  intros [i' [s1' [A B]]].
  assert (Star L1 s0 t1 s1'). intuition. apply plus_star; auto.
  exploit IHstar; eauto. eapply star_safe_along; eauto.
  subst t; apply behavior_app_assoc.
  intros [i'' [s2'' [C D]]].
  exists i''; exists s2''; split; auto. eapply star_trans; eauto.
Qed.

Lemma backward_simulation_forever_silent:
  forall i s1 s2,
  Forever_silent L2 s2 -> S i s1 s2 -> safe L1 s1 ->
  Forever_silent L1 s1.
Proof.
  assert (forall i s1 s2,
         Forever_silent L2 s2 -> S i s1 s2 -> safe L1 s1 ->
         forever_silent_N (step L1) (bsim_order S) (globalenv L1) i s1).
    cofix COINDHYP; intros.
    inv H.  destruct (bsim_simulation S _ _ _ H2 _ H0 H1) as [i' [s2' [A B]]].
    destruct A as [C | [C D]].
    eapply forever_silent_N_plus; eauto. eapply COINDHYP; eauto.
      eapply star_safe; eauto. apply plus_star; auto.
    eapply forever_silent_N_star; eauto. eapply COINDHYP; eauto.
      eapply star_safe; eauto.
  intros. eapply forever_silent_N_forever; eauto. apply bsim_order_wf.
Qed.

Lemma backward_simulation_forever_reactive:
  forall i s1 s2 T,
  Forever_reactive L2 s2 T -> S i s1 s2 -> safe_along_behavior s1 (Reacts T) ->
  Forever_reactive L1 s1 T.
Proof.
  cofix COINDHYP; intros. inv H. 
  destruct (backward_simulation_star H2 _ (Reacts T0) H0) as [i' [s1' [A B]]]; eauto.
  econstructor; eauto. eapply COINDHYP; eauto. eapply star_safe_along; eauto. 
Qed.

Lemma backward_simulation_state_behaves:
  forall i s1 s2 beh2,
  S i s1 s2 -> state_behaves L2 s2 beh2 ->
  exists beh1, state_behaves L1 s1 beh1 /\ behavior_improves beh1 beh2.
Proof.
  intros. destruct (classic (safe_along_behavior s1 beh2)).
(* 1. Safe along *)
  exists beh2; split; [idtac|apply behavior_improves_refl].
  inv H0. 
(* termination *)
  assert (Terminates t r = behavior_app t (Terminates E0 r)).
    simpl. rewrite E0_right; auto.
  rewrite H0 in H1. 
  exploit backward_simulation_star; eauto.
  intros [i' [s1' [A B]]].
  exploit (bsim_match_final_states S); eauto.
    eapply safe_along_safe. eapply star_safe_along; eauto. 
  intros [s1'' [C D]].
  econstructor. eapply star_trans; eauto. traceEq. auto.
(* silent divergence *)
  assert (Diverges t = behavior_app t (Diverges E0)).
    simpl. rewrite E0_right; auto.
  rewrite H0 in H1. 
  exploit backward_simulation_star; eauto.
  intros [i' [s1' [A B]]].
  econstructor. eauto. eapply backward_simulation_forever_silent; eauto. 
  eapply safe_along_safe. eapply star_safe_along; eauto. 
(* reactive divergence *)
  econstructor. eapply backward_simulation_forever_reactive; eauto. 
(* goes wrong *)
  assert (Goes_wrong t = behavior_app t (Goes_wrong E0)).
    simpl. rewrite E0_right; auto.
  rewrite H0 in H1. 
  exploit backward_simulation_star; eauto.
  intros [i' [s1' [A B]]].
  exploit (bsim_progress S); eauto. eapply safe_along_safe. eapply star_safe_along; eauto. 
  intros [[r FIN] | [t' [s2' STEP2]]]. 
  elim (H4 _ FIN).
  elim (H3 _ _ STEP2).

(* 2. Not safe along *)
  exploit not_safe_along_behavior; eauto. 
  intros [t [s1' [PREF [STEPS [NOSTEP NOFIN]]]]].
  exists (Goes_wrong t); split.
  econstructor; eauto. 
  right. exists t; auto.
Qed.

Theorem backward_simulation_behavior_improves:
  forall beh2, program_behaves L2 beh2 ->
  exists beh1, program_behaves L1 beh1 /\ behavior_improves beh1 beh2.
Proof.
  intros. inv H.
(* L2's initial state is defined. *)
  destruct (classic (exists s1, initial_state L1 s1)) as [[s1 INIT] | NOINIT].
(* L1's initial state is defined too. *)
  exploit (bsim_match_initial_states S); eauto. intros [i [s1' [INIT1' MATCH]]].
  exploit backward_simulation_state_behaves; eauto. intros [beh1 [A B]].
  exists beh1; split; auto. econstructor; eauto.
(* L1 has no initial state *)
  exists (Goes_wrong E0); split.
  apply program_goes_initially_wrong. 
  intros; red; intros. elim NOINIT; exists s0; auto.
  apply behavior_improves_bot.
(* L2 has no initial state *)
  exists (Goes_wrong E0); split.
  apply program_goes_initially_wrong. 
  intros; red; intros.
  exploit (bsim_initial_states_exist S); eauto. intros [s2 INIT2]. 
  elim (H0 s2); auto.
  apply behavior_improves_refl.
Qed.

Corollary backward_simulation_same_safe_behavior:
  (forall beh, program_behaves L1 beh -> not_wrong beh) ->
  (forall beh, program_behaves L2 beh -> program_behaves L1 beh).
Proof.
  intros. exploit backward_simulation_behavior_improves; eauto. 
  intros [beh' [A B]]. destruct B. 
  congruence.
  destruct H1 as [t [C D]]. subst. elim (H (Goes_wrong t)). auto.
Qed.

End BACKWARD_SIMULATIONS.

(** * Program behaviors for the "atomic" construction *)

Section ATOMIC.

Variable L: semantics.
Hypothesis Lwb: well_behaved_traces L.

Remark atomic_finish: forall s t, output_trace t -> Star (atomic L) (t, s) t (E0, s).
Proof.
  induction t; intros.
  apply star_refl.
  simpl in H; destruct H. eapply star_left; eauto.
  simpl. apply atomic_step_continue; auto. simpl; auto. auto.
Qed.

Lemma step_atomic_plus:
  forall s1 t s2, Step L s1 t s2 -> Plus (atomic L) (E0,s1) t (E0,s2).
Proof.
  intros.  destruct t.
  apply plus_one. simpl; apply atomic_step_silent; auto.
  exploit Lwb; eauto. simpl; intros. 
  eapply plus_left. eapply atomic_step_start; eauto. eapply atomic_finish; eauto. auto.
Qed.

Lemma star_atomic_star:
  forall s1 t s2, Star L s1 t s2 -> Star (atomic L) (E0,s1) t (E0,s2).
Proof.
  induction 1. apply star_refl. eapply star_trans with (s2 := (E0,s2)).
  apply plus_star. eapply step_atomic_plus; eauto. eauto. auto.
Qed.
 
Lemma atomic_forward_simulation: forward_simulation L (atomic L).
Proof.
  set (ms := fun (s: state L) (ts: state (atomic L)) => ts = (E0,s)).
  apply forward_simulation_plus with ms; intros.
  auto.
  exists (E0,s1); split. simpl; auto. red; auto. 
  red in H. subst s2. simpl; auto. 
  red in H0. subst s2. exists (E0,s1'); split.
  apply step_atomic_plus; auto. red; auto.
Qed.

Lemma atomic_star_star_gen:
  forall ts1 t ts2, Star (atomic L) ts1 t ts2 ->
  exists t', Star L (snd ts1) t' (snd ts2) /\ fst ts1 ** t' = t ** fst ts2.
Proof.
  induction 1. 
  exists E0; split. apply star_refl. traceEq.
  destruct IHstar as [t' [A B]].
  simpl in H; inv H; simpl in *.
  exists t'; split. eapply star_left; eauto. auto.
  exists (ev :: t0 ** t'); split. eapply star_left; eauto. rewrite B; auto. 
  exists t'; split. auto. rewrite B; auto.
Qed.

Lemma atomic_star_star:
  forall s1 t s2, Star (atomic L) (E0,s1) t (E0,s2) -> Star L s1 t s2.
Proof.
  intros. exploit atomic_star_star_gen; eauto. intros [t' [A B]]. 
  simpl in *. replace t with t'. auto. subst; traceEq. 
Qed.

Lemma atomic_forever_silent_forever_silent:
  forall s, Forever_silent (atomic L) s -> Forever_silent L (snd s).
Proof.
  cofix COINDHYP; intros. inv H. inv H0. 
  apply forever_silent_intro with (snd (E0, s')). auto. apply COINDHYP; auto. 
Qed.

Remark star_atomic_output_trace:
  forall s t t' s',
  Star (atomic L) (E0, s) t (t', s') -> output_trace t'.
Proof.
  assert (forall ts1 t ts2, Star (atomic L) ts1 t ts2 ->
          output_trace (fst ts1) -> output_trace (fst ts2)).
  induction 1; intros. auto. inv H; simpl in *.
  apply IHstar. auto.
  apply IHstar. exploit Lwb; eauto.
  destruct H2. apply IHstar. auto.
  intros. change t' with (fst (t',s')). eapply H; eauto. simpl; auto. 
Qed.

Lemma atomic_forever_reactive_forever_reactive:
  forall s T, Forever_reactive (atomic L) (E0,s) T -> Forever_reactive L s T.
Proof.
  assert (forall t s T, Forever_reactive (atomic L) (t,s) T ->
          exists T', Forever_reactive (atomic L) (E0,s) T' /\ T = t *** T').
  induction t; intros. exists T; auto.
  inv H. inv H0. congruence. simpl in H; inv H. 
  destruct (IHt s (t2***T0)) as [T' [A B]]. eapply star_forever_reactive; eauto.
  exists T'; split; auto. simpl. congruence. 

  cofix COINDHYP; intros. inv H0. destruct s2 as [t2 s2]. 
  destruct (H _ _ _ H3) as [T' [A B]].  
  assert (Star (atomic L) (E0, s) (t**t2) (E0, s2)).
    eapply star_trans. eauto. apply atomic_finish. eapply star_atomic_output_trace; eauto. auto. 
  replace (t *** T0) with ((t ** t2) *** T'). apply forever_reactive_intro with s2. 
  apply atomic_star_star; auto. destruct t; simpl in *; unfold E0 in *; congruence.
  apply COINDHYP. auto.
  subst T0; traceEq.
Qed.

Theorem atomic_behaviors:
  forall beh, program_behaves L beh <-> program_behaves (atomic L) beh.
Proof.
  intros; split; intros.
  (* L -> atomic L *)
  exploit forward_simulation_behavior_improves. eapply atomic_forward_simulation. eauto. 
  intros [beh2 [A B]]. red in B. destruct B as [EQ | [t [C D]]].
  congruence.
  subst beh. inv H. inv H1.
  apply program_runs with (E0,s). simpl; auto. 
  apply state_goes_wrong with (E0,s'). apply star_atomic_star; auto. 
  red; intros; red; intros. inv H. eelim H3; eauto. eelim H3; eauto. 
  intros; red; intros. simpl in H. destruct H. eelim H4; eauto. 
  apply program_goes_initially_wrong. 
  intros; red; intros. simpl in H; destruct H. eelim H1; eauto. 
  (* atomic L -> L *)
  inv H.
  (* initial state defined *)
  destruct s as [t s]. simpl in H0. destruct H0; subst t. 
  apply program_runs with s; auto. 
  inv H1.
  (* termination *)
  destruct s' as [t' s']. simpl in H2; destruct H2; subst t'. 
  econstructor. eapply atomic_star_star; eauto. auto. 
  (* silent divergence *)
  destruct s' as [t' s'].
  assert (t' = E0). inv H2. inv H1; auto. subst t'. 
  econstructor. eapply atomic_star_star; eauto. 
  change s' with (snd (E0,s')). apply atomic_forever_silent_forever_silent. auto.
  (* reactive divergence *)
  econstructor. apply atomic_forever_reactive_forever_reactive. auto. 
  (* going wrong *)
  destruct s' as [t' s'].
  assert (t' = E0).
    destruct t'; auto. eelim H2. simpl. apply atomic_step_continue.
    eapply star_atomic_output_trace; eauto.
  subst t'. econstructor. apply atomic_star_star; eauto. 
  red; intros; red; intros. destruct t0.
  elim (H2 E0 (E0,s'0)). constructor; auto. 
  elim (H2 (e::nil) (t0,s'0)). constructor; auto.
  intros; red; intros. elim (H3 r). simpl; auto. 
  (* initial state undefined *)
  apply program_goes_initially_wrong. 
  intros; red; intros. elim (H0 (E0,s)); simpl; auto.
Qed.

End ATOMIC.

(** * Additional results about infinite reduction sequences *)

(** We now show that any infinite sequence of reductions is either of
  the "reactive" kind or of the "silent" kind (after a finite number
  of non-silent transitions).  The proof necessitates the axiom of
  excluded middle.  This result is used below to relate
  the coinductive big-step semantics for divergence with the
  small-step notions of divergence. *)

Unset Implicit Arguments.

Section INF_SEQ_DECOMP.

Variable genv: Type.
Variable state: Type.
Variable step: genv -> state -> trace -> state -> Prop.

Variable ge: genv.

Inductive tstate: Type :=
  ST: forall (s: state) (T: traceinf), forever step ge s T -> tstate.

Definition state_of_tstate (S: tstate): state :=
  match S with ST s T F => s end.
Definition traceinf_of_tstate (S: tstate) : traceinf :=
  match S with ST s T F => T end.

Inductive tstep: trace -> tstate -> tstate -> Prop :=
  | tstep_intro: forall s1 t T s2 S F,
      tstep t (ST s1 (t *** T) (@forever_intro genv state step ge s1 t s2 T S F))
              (ST s2 T F).

Inductive tsteps: tstate -> tstate -> Prop :=
  | tsteps_refl: forall S, tsteps S S
  | tsteps_left: forall t S1 S2 S3, tstep t S1 S2 -> tsteps S2 S3 -> tsteps S1 S3.

Remark tsteps_trans:
  forall S1 S2, tsteps S1 S2 -> forall S3, tsteps S2 S3 -> tsteps S1 S3.
Proof.
  induction 1; intros. auto. econstructor; eauto.
Qed.

Let treactive (S: tstate) : Prop :=
  forall S1, 
  tsteps S S1 ->
  exists S2, exists S3, exists t, tsteps S1 S2 /\ tstep t S2 S3 /\ t <> E0.

Let tsilent (S: tstate) : Prop :=
  forall S1 t S2, tsteps S S1 -> tstep t S1 S2 -> t = E0.

Lemma treactive_or_tsilent:
  forall S, treactive S \/ (exists S', tsteps S S' /\ tsilent S').
Proof.
  intros. destruct (classic (exists S', tsteps S S' /\ tsilent S')).
  auto.
  left. red; intros. 
  generalize (not_ex_all_not _ _ H S1). intros.
  destruct (not_and_or _ _ H1). contradiction. 
  unfold tsilent in H2. 
  generalize (not_all_ex_not _ _ H2). intros [S2 A].
  generalize (not_all_ex_not _ _ A). intros [t B].
  generalize (not_all_ex_not _ _ B). intros [S3 C].
  generalize (imply_to_and _ _ C). intros [D F].
  generalize (imply_to_and _ _ F). intros [G J].
  exists S2; exists S3; exists t. auto.  
Qed.

Lemma tsteps_star:
  forall S1 S2, tsteps S1 S2 ->
  exists t, star step ge (state_of_tstate S1) t (state_of_tstate S2)
         /\ traceinf_of_tstate S1 = t *** traceinf_of_tstate S2.
Proof.
  induction 1.
  exists E0; split. apply star_refl. auto.
  inv H. destruct IHtsteps as [t' [A B]].
  exists (t ** t'); split.
  simpl; eapply star_left; eauto.
  simpl in *. subst T. traceEq.
Qed.

Lemma tsilent_forever_silent:
  forall S,
  tsilent S -> forever_silent step ge (state_of_tstate S).
Proof.
  cofix COINDHYP; intro S. case S. intros until f. simpl. case f. intros.
  assert (tstep t (ST s1 (t *** T0) (forever_intro s1 t s0 f0))
                  (ST s2 T0 f0)). 
    constructor.
  assert (t = E0). 
    red in H. eapply H; eauto. apply tsteps_refl.
  apply forever_silent_intro with (state_of_tstate (ST s2 T0 f0)).
  rewrite <- H1. assumption. 
  apply COINDHYP. 
  red; intros. eapply H. eapply tsteps_left; eauto. eauto. 
Qed.

Lemma treactive_forever_reactive:
  forall S,
  treactive S -> forever_reactive step ge (state_of_tstate S) (traceinf_of_tstate S).
Proof.
  cofix COINDHYP; intros.
  destruct (H S) as [S1 [S2 [t [A [B C]]]]]. apply tsteps_refl. 
  destruct (tsteps_star _ _ A) as [t' [P Q]].
  inv B. simpl in *. rewrite Q. rewrite <- Eappinf_assoc. 
  apply forever_reactive_intro with s2. 
  eapply star_right; eauto. 
  red; intros. destruct (Eapp_E0_inv _ _ H0). contradiction.
  change (forever_reactive step ge (state_of_tstate (ST s2 T F)) (traceinf_of_tstate (ST s2 T F))).
  apply COINDHYP. 
  red; intros. apply H.
  eapply tsteps_trans. eauto.
  eapply tsteps_left. constructor. eauto.
Qed.

Theorem forever_silent_or_reactive:
  forall s T,
  forever step ge s T ->
  forever_reactive step ge s T \/
  exists t, exists s', exists T',
  star step ge s t s' /\ forever_silent step ge s' /\ T = t *** T'.
Proof.
  intros. 
  destruct (treactive_or_tsilent (ST s T H)).
  left. 
  change (forever_reactive step ge (state_of_tstate (ST s T H)) (traceinf_of_tstate (ST s T H))).
  apply treactive_forever_reactive. auto.
  destruct H0 as [S' [A B]].
  exploit tsteps_star; eauto. intros [t [C D]]. simpl in *.
  right. exists t; exists (state_of_tstate S'); exists (traceinf_of_tstate S').
  split. auto. 
  split. apply tsilent_forever_silent. auto.
  auto.
Qed.

End INF_SEQ_DECOMP.

Set Implicit Arguments.

(** * Big-step semantics and program behaviors *)

Section BIGSTEP_BEHAVIORS.

Variable B: bigstep_semantics.
Variable L: semantics.
Hypothesis sound: bigstep_sound B L.

Lemma behavior_bigstep_terminates:
  forall t r,
  bigstep_terminates B t r -> program_behaves L (Terminates t r).
Proof.
  intros. exploit (bigstep_terminates_sound sound); eauto. 
  intros [s1 [s2 [P [Q R]]]].
  econstructor; eauto. econstructor; eauto.
Qed.

Lemma behavior_bigstep_diverges:
  forall T,
  bigstep_diverges B T ->
  program_behaves L (Reacts T)
  \/ exists t, program_behaves L (Diverges t) /\ traceinf_prefix t T.
Proof.
  intros. exploit (bigstep_diverges_sound sound); eauto. intros [s1 [P Q]].
  exploit forever_silent_or_reactive; eauto. intros [X | [t [s' [T' [X [Y Z]]]]]].
  left. econstructor; eauto. constructor; auto.
  right. exists t; split. econstructor; eauto. econstructor; eauto. exists T'; auto.
Qed.

End BIGSTEP_BEHAVIORS.