Module EventsC
Require
Import
String
.
Require
Import
CoqlibC
.
Require
Intv
.
Require
Import
AST
.
Require
Import
Integers
.
Require
Import
Floats
.
Require
Import
Values
.
Require
Import
Memory
.
Require
Import
Globalenvs
.
newly added *
Require
Export
Events
.
Set
Implicit
Arguments
.
Lemma
eventval_valid_le
se_small
ev
se_big
(
VALID
:
eventval_valid
se_small
ev
)
(
LE
:
se_small
.(
Senv.public_symbol
) <1=
se_big
.(
Senv.public_symbol
)):
<<
VALID
:
eventval_valid
se_big
ev
>>.
Proof.
u
in
*.
unfold
eventval_valid
in
*.
des_ifs
.
erewrite
LE
;
eauto
. Qed.
Lemma
match_traces_le
se_small
tr0
tr1
se_big
(
MATCH
:
match_traces
se_small
tr0
tr1
)
(
LE
:
se_small
.(
Senv.public_symbol
) <1=
se_big
.(
Senv.public_symbol
)):
<<
MATCH
:
match_traces
se_big
tr0
tr1
>>.
Proof.
u
in
*.
inv
MATCH
;
econs
;
eauto
;
eapply
eventval_valid_le
;
eauto
. Qed.
Ltac
inv_match_traces
:=
match
goal
with
| [
H
:
match_traces
_
_
_
|-
_
] =>
inv
H
end
.