Module BehaviorsC
Require
Import
Classical
.
Require
Import
ClassicalEpsilon
.
Require
Import
CoqlibC
.
Require
Import
Events
.
Require
Import
Globalenvs
.
Require
Import
Integers
.
Require
Import
Smallstep
.
newly added *
Require
Export
Behaviors
.
Require
Import
Simulation
.
Set
Implicit
Arguments
.
Definition
improves
(
L1
L2
:
semantics
):
Prop
:=
forall
beh2
(
BEH
:
program_behaves
L2
beh2
),
exists
beh1
, <<
BEH
:
program_behaves
L1
beh1
>> /\ <<
IMPRV
:
behavior_improves
beh1
beh2
>>.
Global
Program
Instance
improves_PreOrder
:
PreOrder
improves
.
Next Obligation.
ii
.
esplits
;
eauto
.
eapply
behavior_improves_refl
.
Qed.
Next Obligation.
ii
.
r
in
H
.
r
in
H0
.
repeat
spc
H0
.
des
.
specialize
(
H
_
BEH0
).
des
.
esplits
;
eauto
.
eapply
behavior_improves_trans
;
eauto
.
Qed.
Lemma
bsim_improves
L1
L2
(
BSIM
:
backward_simulation
L1
L2
):
<<
IMRPV
:
improves
L1
L2
>>.
Proof.
ii
.
eapply
backward_simulation_behavior_improves
;
eauto
.
eapply
backward_to_compcert_backward_simulation
;
eauto
.
Qed.