Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Joshua Yanovski
iris-coq
Commits
e7667215
Commit
e7667215
authored
Feb 24, 2016
by
Ralf Jung
Browse files
fix some naming trouble
parent
1a66d561
Changes
1
Hide whitespace changes
Inline
Side-by-side
program_logic/sts.v
View file @
e7667215
...
...
@@ -25,14 +25,14 @@ Module Type StsOwnSig.
(
S
:
sts
.
states
sts
)
(
T
:
sts
.
tokens
sts
),
iPropG
Λ
Σ
.
Parameter
sts_own
:
∀
`
{
i
:
stsG
Λ
Σ
sts
}
(
γ
:
gname
)
(
s
:
sts
.
state
sts
)
(
T
:
sts
.
tokens
sts
),
iPropG
Λ
Σ
.
Axiom
sts_ownS_
def
:
@
sts_ownS
=
@
sts_ownS_def
.
Axiom
sts_own_
def
:
@
sts_own
=
@
sts_own_def
.
Axiom
sts_ownS_
eq
:
@
sts_ownS
=
@
sts_ownS_def
.
Axiom
sts_own_
eq
:
@
sts_own
=
@
sts_own_def
.
End
StsOwnSig
.
Module
Export
StsOwn
:
StsOwnSig
.
Definition
sts_ownS
:=
@
sts_ownS_def
.
Definition
sts_own
:=
@
sts_own_def
.
Definition
sts_ownS_
def
:=
Logic
.
eq_refl
(
@
sts_ownS_def
).
Definition
sts_own_
def
:=
Logic
.
eq_refl
(
@
sts_own_def
).
Definition
sts_ownS_
eq
:=
Logic
.
eq_refl
(
@
sts_ownS_def
).
Definition
sts_own_
eq
:=
Logic
.
eq_refl
(
@
sts_own_def
).
End
StsOwn
.
Definition
sts_inv
`
{
i
:
stsG
Λ
Σ
sts
}
(
γ
:
gname
)
...
...
@@ -64,10 +64,10 @@ Section sts.
Proof
.
by
intros
φ
1
φ
2
H
φ
;
rewrite
/
sts_inv
;
setoid_rewrite
H
φ
.
Qed
.
Global
Instance
sts_ownS_proper
γ
:
Proper
((
≡
)
==>
(
≡
)
==>
(
≡
))
(
sts_ownS
γ
).
Proof
.
intros
S1
S2
HS
T1
T2
HT
.
by
rewrite
!
sts_ownS_
def
/
Top
.
sts_ownS_def
HS
HT
.
intros
S1
S2
HS
T1
T2
HT
.
by
rewrite
!
sts_ownS_
eq
/
sts_ownS_def
HS
HT
.
Qed
.
Global
Instance
sts_own_proper
γ
s
:
Proper
((
≡
)
==>
(
≡
))
(
sts_own
γ
s
).
Proof
.
intros
T1
T2
HT
.
by
rewrite
!
sts_own_
def
/
Top
.
sts_own_def
HT
.
Qed
.
Proof
.
intros
T1
T2
HT
.
by
rewrite
!
sts_own_
eq
/
sts_own_def
HT
.
Qed
.
Global
Instance
sts_ctx_ne
n
γ
N
:
Proper
(
pointwise_relation
_
(
dist
n
)
==>
dist
n
)
(
sts_ctx
γ
N
).
Proof
.
by
intros
φ
1
φ
2
H
φ
;
rewrite
/
sts_ctx
H
φ
.
Qed
.
...
...
@@ -81,23 +81,21 @@ Section sts.
T2
⊆
T1
→
S1
⊆
S2
→
sts
.
closed
S2
T2
→
sts_ownS
γ
S1
T1
⊑
(
|={
E
}=>
sts_ownS
γ
S2
T2
).
Proof
.
intros
?
?
?
.
rewrite
sts_ownS_
def
.
by
apply
own_update
,
sts_update_frag
.
intros
?
?
?
.
rewrite
sts_ownS_
eq
.
by
apply
own_update
,
sts_update_frag
.
Qed
.
Lemma
sts_own_weaken
E
γ
s
S
T1
T2
:
T2
⊆
T1
→
s
∈
S
→
sts
.
closed
S
T2
→
sts_own
γ
s
T1
⊑
(
|={
E
}=>
sts_ownS
γ
S
T2
).
Proof
.
intros
???
.
rewrite
sts_ownS_
def
sts_own_
def
.
intros
???
.
rewrite
sts_ownS_
eq
sts_own_
eq
.
by
apply
own_update
,
sts_update_frag_up
.
Qed
.
Lemma
sts_ownS_op
γ
S1
S2
T1
T2
:
T1
∩
T2
⊆
∅
→
sts
.
closed
S1
T1
→
sts
.
closed
S2
T2
→
sts_ownS
γ
(
S1
∩
S2
)
(
T1
∪
T2
)
≡
(
sts_ownS
γ
S1
T1
★
sts_ownS
γ
S2
T2
)
%
I
.
Proof
.
intros
.
by
rewrite
sts_ownS_def
/
Top
.
sts_ownS_def
-
own_op
sts_op_frag
.
Qed
.
Proof
.
intros
.
by
rewrite
sts_ownS_eq
/
sts_ownS_def
-
own_op
sts_op_frag
.
Qed
.
Lemma
sts_alloc
E
N
s
:
nclose
N
⊆
E
→
...
...
@@ -111,7 +109,7 @@ Section sts.
rewrite
sep_exist_l
.
apply
exist_elim
=>
γ
.
rewrite
-
(
exist_intro
γ
).
trans
(
▷
sts_inv
γ
φ
★
sts_own
γ
s
(
⊤
∖
sts
.
tok
s
))
%
I
.
{
rewrite
/
sts_inv
-
(
exist_intro
s
)
later_sep
.
ecancel
[
▷
φ
_
]
%
I
.
rewrite
sts_own_
def
.
ecancel
[
▷
φ
_
]
%
I
.
rewrite
sts_own_
eq
.
by
rewrite
-
later_intro
-
own_op
sts_op_auth_frag_up
;
last
set_solver
.
}
rewrite
(
inv_alloc
N
)
/
sts_ctx
pvs_frame_r
.
by
rewrite
always_and_sep_l
.
...
...
@@ -121,7 +119,7 @@ Section sts.
(
▷
sts_inv
γ
φ
★
sts_ownS
γ
S
T
)
⊑
(
|={
E
}=>
∃
s
,
■
(
s
∈
S
)
★
▷
φ
s
★
own
γ
(
sts_auth
s
T
)).
Proof
.
rewrite
/
sts_inv
sts_ownS_
def
later_exist
sep_exist_r
.
apply
exist_elim
=>
s
.
rewrite
/
sts_inv
sts_ownS_
eq
later_exist
sep_exist_r
.
apply
exist_elim
=>
s
.
rewrite
later_sep
pvs_timeless
!
pvs_frame_r
.
apply
pvs_mono
.
rewrite
-
(
exist_intro
s
).
rewrite
[(
_
★
▷φ
_
)
%
I
]
comm
-!
assoc
-
own_op
-
[(
▷φ
_
★
_
)
%
I
]
comm
.
...
...
@@ -138,7 +136,7 @@ Section sts.
sts
.
steps
(
s
,
T
)
(
s
'
,
T
'
)
→
(
▷
φ
s
'
★
own
γ
(
sts_auth
s
T
))
⊑
(
|={
E
}=>
▷
sts_inv
γ
φ
★
sts_own
γ
s
'
T
'
).
Proof
.
intros
Hstep
.
rewrite
/
sts_inv
sts_own_
def
-
(
exist_intro
s
'
)
later_sep
.
intros
Hstep
.
rewrite
/
sts_inv
sts_own_
eq
-
(
exist_intro
s
'
)
later_sep
.
(
*
TODO
it
would
be
really
nice
to
use
cancel
here
*
)
rewrite
[(
_
★
▷
φ
_
)
%
I
]
comm
-
assoc
.
rewrite
-
pvs_frame_l
.
apply
sep_mono_r
.
rewrite
-
later_intro
.
...
...
@@ -189,7 +187,7 @@ Section sts.
(
sts_own
γ
s
'
T
'
-
★
Ψ
x
)))
→
P
⊑
fsa
E
Ψ
.
Proof
.
rewrite
sts_own_
def
.
intros
.
eapply
sts_fsaS
;
try
done
;
[].
by
rewrite
sts_ownS_
def
sts_own_
def
.
rewrite
sts_own_
eq
.
intros
.
eapply
sts_fsaS
;
try
done
;
[].
by
rewrite
sts_ownS_
eq
sts_own_
eq
.
Qed
.
End
sts
.
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment