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
Iris
Fairis
Commits
c59e1f85
Commit
c59e1f85
authored
Feb 25, 2016
by
Robbert Krebbers
Browse files
More solve_propers.
parent
9589d1ba
Changes
5
Hide whitespace changes
Inline
Side-by-side
program_logic/auth.v
View file @
c59e1f85
...
...
@@ -42,7 +42,7 @@ Section auth.
Global
Instance
auth_own_ne
n
γ
:
Proper
(
dist
n
==>
dist
n
)
(
auth_own
γ
).
Proof
.
rewrite
auth_own_eq
;
solve_proper
.
Qed
.
Global
Instance
auth_own_proper
γ
:
Proper
((
≡
)
==>
(
≡
))
(
auth_own
γ
).
Proof
.
by
rewrite
auth_own_eq
/
auth_own_def
=>
a
b
->
.
Qed
.
Proof
.
by
rewrite
auth_own_eq
;
solve_proper
.
Qed
.
Global
Instance
auth_own_timeless
γ
a
:
TimelessP
(
auth_own
γ
a
).
Proof
.
rewrite
auth_own_eq
.
apply
_.
Qed
.
...
...
program_logic/ghost_ownership.v
View file @
c59e1f85
...
...
@@ -64,7 +64,7 @@ Qed.
(
**
*
Properties
of
own
*
)
Global
Instance
own_ne
γ
n
:
Proper
(
dist
n
==>
dist
n
)
(
own
γ
).
Proof
.
by
intros
m
m
'
Hm
;
rewrite
/
own
Hm
.
Qed
.
Proof
.
solve_proper
.
Qed
.
Global
Instance
own_proper
γ
:
Proper
((
≡
)
==>
(
≡
))
(
own
γ
)
:=
ne_proper
_.
Lemma
own_op
γ
a1
a2
:
own
γ
(
a1
⋅
a2
)
≡
(
own
γ
a1
★
own
γ
a2
)
%
I
.
...
...
program_logic/hoare.v
View file @
c59e1f85
...
...
@@ -30,13 +30,13 @@ Global Instance ht_ne E n :
Proof
.
solve_proper
.
Qed
.
Global
Instance
ht_proper
E
:
Proper
((
≡
)
==>
eq
==>
pointwise_relation
_
(
≡
)
==>
(
≡
))
(
@
ht
Λ
Σ
E
).
Proof
.
by
intros
P
P
'
HP
e
?
<-
Φ
Φ'
H
Φ
;
rewrite
/
ht
HP
;
setoid_rewrite
H
Φ
.
Qed
.
Proof
.
solve_proper
.
Qed
.
Lemma
ht_mono
E
P
P
'
Φ
Φ'
e
:
P
⊑
P
'
→
(
∀
v
,
Φ'
v
⊑
Φ
v
)
→
{{
P
'
}}
e
@
E
{{
Φ'
}}
⊑
{{
P
}}
e
@
E
{{
Φ
}}
.
Proof
.
by
intros
;
apply
always_mono
,
impl_mono
,
wp_mono
.
Qed
.
Global
Instance
ht_mono
'
E
:
Proper
(
flip
(
⊑
)
==>
eq
==>
pointwise_relation
_
(
⊑
)
==>
(
⊑
))
(
@
ht
Λ
Σ
E
).
Proof
.
by
intros
P
P
'
HP
e
?
<-
Φ
Φ'
H
Φ
;
apply
ht_mono
.
Qed
.
Proof
.
solve_proper
.
Qed
.
Lemma
ht_alt
E
P
Φ
e
:
(
P
⊑
||
e
@
E
{{
Φ
}}
)
→
{{
P
}}
e
@
E
{{
Φ
}}
.
Proof
.
...
...
program_logic/ownership.v
View file @
c59e1f85
...
...
@@ -46,7 +46,7 @@ Proof. rewrite /ownP; apply _. Qed.
(
*
ghost
state
*
)
Global
Instance
ownG_ne
n
:
Proper
(
dist
n
==>
dist
n
)
(
@
ownG
Λ
Σ
).
Proof
.
by
intros
m
m
'
Hm
;
unfold
ownG
;
rewrite
Hm
.
Qed
.
Proof
.
solve_proper
.
Qed
.
Global
Instance
ownG_proper
:
Proper
((
≡
)
==>
(
≡
))
(
@
ownG
Λ
Σ
)
:=
ne_proper
_.
Lemma
ownG_op
m1
m2
:
ownG
(
m1
⋅
m2
)
≡
(
ownG
m1
★
ownG
m2
)
%
I
.
Proof
.
by
rewrite
/
ownG
-
uPred
.
ownM_op
Res_op
!
left_id
.
Qed
.
...
...
program_logic/viewshifts.v
View file @
c59e1f85
...
...
@@ -41,7 +41,7 @@ Proof. by intros HP HQ; rewrite /vs -HP HQ. Qed.
Global
Instance
vs_mono
'
E1
E2
:
Proper
(
flip
(
⊑
)
==>
(
⊑
)
==>
(
⊑
))
(
@
vs
Λ
Σ
E1
E2
).
Proof
.
by
intros
until
2
;
apply
vs_mono
.
Qed
.
Proof
.
solve_proper
.
Qed
.
Lemma
vs_false_elim
E1
E2
P
:
False
={
E1
,
E2
}=>
P
.
Proof
.
apply
vs_alt
,
False_elim
.
Qed
.
...
...
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