Module SmallstepC
Require
Import
Relations
.
Require
Import
Wellfounded
.
Require
Import
CoqlibC
.
Require
Import
Events
.
Require
Import
Globalenvs
.
Require
Import
Integers
.
Require
Import
AxiomsC
.
newly added *
Require
Export
Smallstep
.
Set
Implicit
Arguments
.
Closures of transitions relations
Definition
PStep
(
L
:
semantics
) (
P
:
L
.(
state
) ->
Prop
) :=
(
fun
s1
t
s2
=>
P
s1
/\
Step
L
s1
t
s2
).
Definition
PStar
(
L
:
semantics
) (
P
:
L
.(
state
) ->
Prop
) :=
(
star
(
fun
_
_
=>
PStep
L
P
))
L
.(
symbolenv
)
L
.(
globalenv
).
Definition
PStarN
(
L
:
semantics
) (
P
:
L
.(
state
) ->
Prop
) :=
(
starN
(
fun
_
_
=>
PStep
L
P
))
L
.(
symbolenv
)
L
.(
globalenv
).
Definition
PPlus
(
L
:
semantics
) (
P
:
L
.(
state
) ->
Prop
) :=
(
plus
(
fun
_
_
=>
PStep
L
P
))
L
.(
symbolenv
)
L
.(
globalenv
).
Lemma
PStep_iff
L
P
Q
(
IFF
:
all1
(
P
<1>
Q
)):
PStep
L
P
=
PStep
L
Q
.
Proof.
repeat
(
eapply
functional_extensionality
;
i
).
eapply
prop_ext
.
split
;
i
;
inv
H
;
econs
;
eauto
;
eapply
IFF
;
eauto
.
Qed.
Lemma
star_inv
G
ST
(
step
:
Senv.t
->
G
->
ST
->
trace
->
ST
->
Prop
)
se
(
ge
:
G
)
st0
tr
st1
(
STAR
:
star
step
se
ge
st0
tr
st1
):
<<
EQ
:
st0
=
st1
/\
tr
= []>> \/ <<
PLUS
:
plus
step
se
ge
st0
tr
st1
>>.
Proof.
inv
STAR
;
eauto
.
right
.
econs
;
eauto
. Qed.
Lemma
plus_or_star_inv
G
ST
(
step
:
Senv.t
->
G
->
ST
->
trace
->
ST
->
Prop
)
se
(
ge
:
G
)
st0
tr
st1
(
STAR
:
plus
step
se
ge
st0
tr
st1
\/
star
step
se
ge
st0
tr
st1
):
<<
EQ
:
st0
=
st1
/\
tr
= []>> \/ <<
PLUS
:
plus
step
se
ge
st0
tr
st1
>>.
Proof.
des
;
eauto
.
eapply
star_inv
;
eauto
. Qed.
Lemma
Pstar_non_E0_split
'
_strong
L
P
st0
tr
st1
(
SINGLE
:
single_events
L
)
(
STAR
:
PStar
L
P
st0
tr
st1
):
match
tr
with
| [] =>
True
|
ev
::
tr
' =>
exists
st0x
,
PPlus
L
P
st0
[
ev
]
st0x
/\
((
tr
' <>
E0
/\
PPlus
L
P
st0x
tr
'
st1
) \/ (
tr
' =
E0
/\
st0x
=
st1
))
end
.
Proof.
ginduction
STAR
;
ii
;
ss
.
des_ifs
.
{
destruct
t1
;
ss
.
clarify
.
rr
in
H
.
des
.
exploit
SINGLE
;
eauto
.
i
;
des
.
ss
.
destruct
t1
;
ss
;
try
xomega
.
esplits
;
try
(
right
;
ss
).
{
eapply
plus_star_trans
;
eauto
;
traceEq
.
apply
plus_one
.
rr
.
eauto
. }
}
exploit
IHSTAR
;
eauto
.
i
;
des_safe
.
destruct
t1
;
ss
;
clarify
.
-
esplits
;
eauto
.
+
eapply
star_plus_trans
;
eauto
.
apply
star_one
;
eauto
.
traceEq
.
-
rr
in
H
.
des_safe
.
exploit
SINGLE
;
eauto
.
i
.
ss
.
destruct
t1
;
ss
;
try
xomega
.
esplits
;
eauto
.
+
eapply
plus_one
;
eauto
.
rr
.
eauto
.
+
des
.
*
left
.
split
;
ss
.
eapply
plus_star_trans
;
eauto
.
eapply
plus_star
;
eauto
.
ss
.
*
clarify
.
left
.
split
;
ss
.
Qed.
Lemma
PStar_top_Star
:
forall
L
,
Star
L
=
PStar
L
top1
.
Proof.
i
.
repeat
(
apply
func_ext1
;
i
).
apply
prop_ext
.
split
;
intro
STAR
.
-
ginduction
STAR
;
ii
;
ss
.
{
econs
;
eauto
. }
clarify
.
eapply
star_trans
;
try
eapply
star_refl
;
traceEq
.
eapply
star_left
;
eauto
.
rr
.
esplits
;
eauto
.
-
ginduction
STAR
;
ii
;
ss
.
{
econs
;
eauto
. }
clarify
.
eapply
star_trans
;
try
eapply
star_refl
;
traceEq
.
eapply
star_left
;
eauto
.
rr
in
H
.
des
;
eauto
.
Qed.
Lemma
PPlus_top_Plus
:
forall
L
,
Plus
L
=
PPlus
L
top1
.
Proof.
i
.
repeat
(
apply
func_ext1
;
i
).
apply
prop_ext
.
split
;
intro
PLUS
.
-
inv
PLUS
;
ss
.
econs
;
eauto
.
{
rr
.
eauto
. }
rewrite
PStar_top_Star
in
H0
;
eauto
.
-
inv
PLUS
;
ss
.
rr
in
H
.
des
.
econs
;
eauto
.
rewrite
PStar_top_Star
;
eauto
.
Qed.
Lemma
star_non_E0_split
'
_strong
L
st0
tr
st1
(
SINGLE
:
single_events
L
)
(
STAR
:
Star
L
st0
tr
st1
):
match
tr
with
| [] =>
True
|
ev
::
tr
' =>
exists
st0x
,
Plus
L
st0
[
ev
]
st0x
/\
((
tr
' <>
E0
/\
Plus
L
st0x
tr
'
st1
) \/ (
tr
' =
E0
/\
st0x
=
st1
))
end
.
Proof.
exploit
(@
Pstar_non_E0_split
'
_strong
L
top1
);
eauto
.
{
erewrite
<-
PStar_top_Star
;
eauto
. }
i
;
des
.
des_ifs
.
des_safe
.
erewrite
<-
PPlus_top_Plus
in
*;
eauto
.
Qed.
Lemma
starN_plus_iff
G
ST
(
step
:
Senv.t
->
G
->
ST
->
trace
->
ST
->
Prop
)
se
ge
st0
tr
st1
:
(
exists
n
,
starN
step
se
ge
n
st0
tr
st1
/\ (
n
> 0)%
nat
) <->
plus
step
se
ge
st0
tr
st1
.
Proof.
split
;
i
;
des
.
-
destruct
n
;
ss
;
try
xomega
.
ginduction
H
;
ii
;
ss
;
try
xomega
.
clarify
.
inv
H0
.
+
eapply
plus_star_trans
;
et
;
try
eapply
star_refl
.
apply
plus_one
;
et
.
+
eapply
plus_trans
;
et
.
{
apply
plus_one
;
et
. }
eapply
IHstarN
;
et
.
xomega
.
-
inv
H
.
apply
star_starN
in
H1
.
des
.
exists
(
Datatypes.S
n
).
esplits
;
et
;
try
xomega
.
econs
;
et
.
Qed.