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
George Pirlea
Iris
Commits
3013536d
Commit
3013536d
authored
Feb 18, 2016
by
Ralf Jung
Browse files
use ssreflect's apply where it saves underscores
parent
4763600e
Changes
7
Hide whitespace changes
Inline
Side-by-side
algebra/fin_maps.v
View file @
3013536d
...
...
@@ -62,7 +62,7 @@ Proof.
Qed
.
Global
Instance
map_timeless
`
{
∀
a
:
A
,
Timeless
a
}
m
:
Timeless
m
.
Proof
.
by
intros
m'
?
i
;
apply
(
timeless
_
)
.
Qed
.
Proof
.
by
intros
m'
?
i
;
apply
:
timeless
.
Qed
.
Instance
map_empty_timeless
:
Timeless
(
∅
:
gmap
K
A
).
Proof
.
...
...
@@ -71,7 +71,7 @@ Proof.
Qed
.
Global
Instance
map_lookup_timeless
m
i
:
Timeless
m
→
Timeless
(
m
!!
i
).
Proof
.
intros
?
[
x
|]
Hx
;
[|
by
symmetry
;
apply
(
timeless
_
)
].
intros
?
[
x
|]
Hx
;
[|
by
symmetry
;
apply
:
timeless
].
assert
(
m
≡
{
0
}
≡
<[
i
:
=
x
]>
m
)
by
(
by
symmetry
in
Hx
;
inversion
Hx
;
cofe_subst
;
rewrite
insert_id
).
by
rewrite
(
timeless
m
(<[
i
:
=
x
]>
m
))
//
lookup_insert
.
...
...
@@ -80,8 +80,8 @@ Global Instance map_insert_timeless m i x :
Timeless
x
→
Timeless
m
→
Timeless
(<[
i
:
=
x
]>
m
).
Proof
.
intros
??
m'
Hm
j
;
destruct
(
decide
(
i
=
j
))
;
simplify_map_eq
.
{
by
apply
(
timeless
_
)
;
rewrite
-
Hm
lookup_insert
.
}
by
apply
(
timeless
_
)
;
rewrite
-
Hm
lookup_insert_ne
.
{
by
apply
:
timeless
;
rewrite
-
Hm
lookup_insert
.
}
by
apply
:
timeless
;
rewrite
-
Hm
lookup_insert_ne
.
Qed
.
Global
Instance
map_singleton_timeless
i
x
:
Timeless
x
→
Timeless
({[
i
:
=
x
]}
:
gmap
K
A
)
:
=
_
.
...
...
algebra/iprod.v
View file @
3013536d
...
...
@@ -49,7 +49,7 @@ Section iprod_cofe.
Definition
iprod_lookup_empty
x
:
∅
x
=
∅
:
=
eq_refl
.
Global
Instance
iprod_empty_timeless
:
(
∀
x
:
A
,
Timeless
(
∅
:
B
x
))
→
Timeless
(
∅
:
iprod
B
).
Proof
.
intros
?
f
Hf
x
.
by
apply
(
timeless
_
)
.
Qed
.
Proof
.
intros
?
f
Hf
x
.
by
apply
:
timeless
.
Qed
.
End
empty
.
(** Properties of iprod_insert. *)
...
...
@@ -78,7 +78,7 @@ Section iprod_cofe.
intros
?
y
?.
cut
(
f
≡
iprod_insert
x
y
f
).
{
by
move
=>
/(
_
x
)->
;
rewrite
iprod_lookup_insert
.
}
by
apply
(
timeless
_
)
=>
x'
;
destruct
(
decide
(
x
=
x'
))
as
[->|]
;
by
apply
:
timeless
=>
x'
;
destruct
(
decide
(
x
=
x'
))
as
[->|]
;
rewrite
?iprod_lookup_insert
?iprod_lookup_insert_ne
.
Qed
.
Global
Instance
iprod_insert_timeless
f
x
y
:
...
...
@@ -86,9 +86,9 @@ Section iprod_cofe.
Proof
.
intros
??
g
Heq
x'
;
destruct
(
decide
(
x
=
x'
))
as
[->|].
-
rewrite
iprod_lookup_insert
.
apply
(
timeless
_
)
.
by
rewrite
-(
Heq
x'
)
iprod_lookup_insert
.
apply
:
timeless
.
by
rewrite
-(
Heq
x'
)
iprod_lookup_insert
.
-
rewrite
iprod_lookup_insert_ne
//.
apply
(
timeless
_
)
.
by
rewrite
-(
Heq
x'
)
iprod_lookup_insert_ne
.
apply
:
timeless
.
by
rewrite
-(
Heq
x'
)
iprod_lookup_insert_ne
.
Qed
.
(** Properties of iprod_singletom. *)
...
...
program_logic/ghost_ownership.v
View file @
3013536d
...
...
@@ -80,7 +80,7 @@ Proof.
by
destruct
inG_prf
.
Qed
.
Lemma
own_valid_r
γ
a
:
own
γ
a
⊑
(
own
γ
a
★
✓
a
).
Proof
.
apply
(
uPred
.
always_entails_r
_
_
),
own_valid
.
Qed
.
Proof
.
apply
:
uPred
.
always_entails_r
.
apply
own_valid
.
Qed
.
Lemma
own_valid_l
γ
a
:
own
γ
a
⊑
(
✓
a
★
own
γ
a
).
Proof
.
by
rewrite
comm
-
own_valid_r
.
Qed
.
Global
Instance
own_timeless
γ
a
:
Timeless
a
→
TimelessP
(
own
γ
a
).
...
...
program_logic/hoare.v
View file @
3013536d
...
...
@@ -31,7 +31,7 @@ Proof. by intros P P' HP e ? <- Φ Φ' HΦ; apply ht_mono. Qed.
Lemma
ht_alt
E
P
Φ
e
:
(
P
⊑
wp
E
e
Φ
)
→
{{
P
}}
e
@
E
{{
Φ
}}.
Proof
.
intros
;
rewrite
-{
1
}
always_const
.
apply
(
always_intro
_
_
),
impl_intro_l
.
intros
;
rewrite
-{
1
}
always_const
.
apply
:
always_intro
.
apply
impl_intro_l
.
by
rewrite
always_const
right_id
.
Qed
.
...
...
@@ -43,7 +43,7 @@ Lemma ht_vs E P P' Φ Φ' e :
((
P
={
E
}=>
P'
)
∧
{{
P'
}}
e
@
E
{{
Φ
'
}}
∧
∀
v
,
Φ
'
v
={
E
}=>
Φ
v
)
⊑
{{
P
}}
e
@
E
{{
Φ
}}.
Proof
.
apply
(
always_intro
_
_
),
impl_intro_l
.
apply
:
always_intro
.
apply
impl_intro_l
.
rewrite
(
assoc
_
P
)
{
1
}/
vs
always_elim
impl_elim_r
.
rewrite
assoc
pvs_impl_r
pvs_always_r
wp_always_r
.
rewrite
-(
pvs_wp
E
e
Φ
)
-(
wp_pvs
E
e
Φ
)
;
apply
pvs_mono
,
wp_mono
=>
v
.
...
...
@@ -55,7 +55,7 @@ Lemma ht_atomic E1 E2 P P' Φ Φ' e :
((
P
={
E1
,
E2
}=>
P'
)
∧
{{
P'
}}
e
@
E2
{{
Φ
'
}}
∧
∀
v
,
Φ
'
v
={
E2
,
E1
}=>
Φ
v
)
⊑
{{
P
}}
e
@
E1
{{
Φ
}}.
Proof
.
intros
??
;
apply
(
always_intro
_
_
),
impl_intro_l
.
intros
??
;
apply
:
always_intro
.
apply
impl_intro_l
.
rewrite
(
assoc
_
P
)
{
1
}/
vs
always_elim
impl_elim_r
.
rewrite
assoc
pvs_impl_r
pvs_always_r
wp_always_r
.
rewrite
-(
wp_atomic
E1
E2
)
//
;
apply
pvs_mono
,
wp_mono
=>
v
.
...
...
@@ -66,7 +66,7 @@ Lemma ht_bind `{LanguageCtx Λ K} E P Φ Φ' e :
({{
P
}}
e
@
E
{{
Φ
}}
∧
∀
v
,
{{
Φ
v
}}
K
(
of_val
v
)
@
E
{{
Φ
'
}})
⊑
{{
P
}}
K
e
@
E
{{
Φ
'
}}.
Proof
.
intros
;
apply
(
always_intro
_
_
),
impl_intro_l
.
intros
;
apply
:
always_intro
.
apply
impl_intro_l
.
rewrite
(
assoc
_
P
)
{
1
}/
ht
always_elim
impl_elim_r
.
rewrite
wp_always_r
-
wp_bind
//
;
apply
wp_mono
=>
v
.
by
rewrite
(
forall_elim
v
)
/
ht
always_elim
impl_elim_r
.
...
...
program_logic/hoare_lifting.v
View file @
3013536d
...
...
@@ -26,7 +26,7 @@ Lemma ht_lift_step E1 E2
{{
Φ
2 e2
σ
2
ef
}}
ef
?@
⊤
{{
λ
_
,
True
}})
⊑
{{
P
}}
e1
@
E2
{{
Ψ
}}.
Proof
.
intros
??
Hsafe
Hstep
;
apply
(
always_intro
_
_
),
impl_intro_l
.
intros
??
Hsafe
Hstep
;
apply
:
always_intro
.
apply
impl_intro_l
.
rewrite
(
assoc
_
P
)
{
1
}/
vs
always_elim
impl_elim_r
pvs_always_r
.
rewrite
-(
wp_lift_step
E1
E2
φ
_
e1
σ
1
)
//
;
apply
pvs_mono
.
rewrite
always_and_sep_r
-
assoc
;
apply
sep_mono
;
first
done
.
...
...
@@ -62,8 +62,8 @@ Proof.
apply
and_intro
;
[
by
rewrite
-
vs_reflexive
;
apply
const_intro
|].
apply
forall_mono
=>
e2
;
apply
forall_mono
=>
σ
2
;
apply
forall_mono
=>
ef
.
apply
and_intro
;
[|
apply
and_intro
;
[|
done
]].
-
rewrite
-
vs_impl
;
apply
(
always_intro
_
_
),
impl_intro_l
;
rewrite
and_elim_l
.
rewrite
!
assoc
;
apply
sep_mono
;
last
done
.
-
rewrite
-
vs_impl
;
apply
:
always_intro
.
apply
impl_intro_l
.
rewrite
and_elim_l
!
assoc
;
apply
sep_mono
;
last
done
.
rewrite
-!
always_and_sep_l
-!
always_and_sep_r
;
apply
const_elim_l
=>-[??].
by
repeat
apply
and_intro
;
try
apply
const_intro
.
-
apply
(
always_intro
_
_
),
impl_intro_l
;
rewrite
and_elim_l
.
...
...
@@ -82,7 +82,7 @@ Lemma ht_lift_pure_step E (φ : expr Λ → option (expr Λ) → Prop) P P' Ψ e
{{
■
φ
e2
ef
★
P'
}}
ef
?@
⊤
{{
λ
_
,
True
}})
⊑
{{
▷
(
P
★
P'
)
}}
e1
@
E
{{
Ψ
}}.
Proof
.
intros
?
Hsafe
Hstep
;
apply
(
always_intro
_
_
),
impl_intro_l
.
intros
?
Hsafe
Hstep
;
apply
:
always_intro
.
apply
impl_intro_l
.
rewrite
-(
wp_lift_pure_step
E
φ
_
e1
)
//.
rewrite
(
later_intro
(
∀
_
,
_
))
-
later_and
;
apply
later_mono
.
apply
forall_intro
=>
e2
;
apply
forall_intro
=>
ef
;
apply
impl_intro_l
.
...
...
@@ -110,11 +110,11 @@ Proof.
intros
?
Hsafe
Hdet
.
rewrite
-(
ht_lift_pure_step
_
(
λ
e2'
ef'
,
e2
=
e2'
∧
ef
=
ef'
))
;
eauto
.
apply
forall_intro
=>
e2'
;
apply
forall_intro
=>
ef'
;
apply
and_mono
.
-
apply
(
always_intro
'
_
_
),
impl_intro_l
.
-
apply
:
always_intro
.
apply
impl_intro_l
.
rewrite
-
always_and_sep_l
-
assoc
;
apply
const_elim_l
=>-[??]
;
subst
.
by
rewrite
/
ht
always_elim
impl_elim_r
.
-
destruct
ef'
as
[
e'
|]
;
simpl
;
[|
by
apply
const_intro
].
apply
(
always_intro
_
_
),
impl_intro_l
.
apply
:
always_intro
.
apply
impl_intro_l
.
rewrite
-
always_and_sep_l
-
assoc
;
apply
const_elim_l
=>-[??]
;
subst
.
by
rewrite
/=
/
ht
always_elim
impl_elim_r
.
Qed
.
...
...
program_logic/resources.v
View file @
3013536d
...
...
@@ -40,7 +40,7 @@ Proof. by destruct 1. Qed.
Global
Instance
pst_ne
n
:
Proper
(
dist
n
==>
dist
n
)
(@
pst
Λ
Σ
A
).
Proof
.
by
destruct
1
.
Qed
.
Global
Instance
pst_ne'
n
:
Proper
(
dist
n
==>
(
≡
))
(@
pst
Λ
Σ
A
).
Proof
.
destruct
1
;
apply
(
timeless
_
),
dist_le
with
n
;
auto
with
lia
.
Qed
.
Proof
.
destruct
1
;
apply
:
timeless
;
apply
dist_le
with
n
;
auto
with
lia
.
Qed
.
Global
Instance
pst_proper
:
Proper
((
≡
)
==>
(=))
(@
pst
Λ
Σ
A
).
Proof
.
by
destruct
1
;
unfold_leibniz
.
Qed
.
Global
Instance
gst_ne
n
:
Proper
(
dist
n
==>
dist
n
)
(@
gst
Λ
Σ
A
).
...
...
@@ -69,7 +69,7 @@ Qed.
Canonical
Structure
resC
:
cofeT
:
=
CofeT
res_cofe_mixin
.
Global
Instance
res_timeless
r
:
Timeless
(
wld
r
)
→
Timeless
(
gst
r
)
→
Timeless
r
.
Proof
.
by
destruct
3
;
constructor
;
try
apply
(
timeless
_
)
.
Qed
.
Proof
.
by
destruct
3
;
constructor
;
try
apply
:
timeless
.
Qed
.
Instance
res_op
:
Op
(
res
Λ
Σ
A
)
:
=
λ
r1
r2
,
Res
(
wld
r1
⋅
wld
r2
)
(
pst
r1
⋅
pst
r2
)
(
gst
r1
⋅
gst
r2
).
...
...
@@ -157,7 +157,7 @@ Lemma lookup_wld_op_r n r1 r2 i P :
✓
{
n
}
(
r1
⋅
r2
)
→
wld
r2
!!
i
≡
{
n
}
≡
Some
P
→
(
wld
r1
⋅
wld
r2
)
!!
i
≡
{
n
}
≡
Some
P
.
Proof
.
rewrite
(
comm
_
r1
)
(
comm
_
(
wld
r1
))
;
apply
lookup_wld_op_l
.
Qed
.
Global
Instance
Res_timeless
e
σ
m
:
Timeless
m
→
Timeless
(
Res
∅
e
σ
m
).
Proof
.
by
intros
?
?
[???]
;
constructor
;
apply
(
timeless
_
)
.
Qed
.
Proof
.
by
intros
?
?
[???]
;
constructor
;
apply
:
timeless
.
Qed
.
(** Internalized properties *)
Lemma
res_equivI
{
M
}
r1
r2
:
...
...
program_logic/viewshifts.v
View file @
3013536d
...
...
@@ -24,7 +24,7 @@ Implicit Types N : namespace.
Lemma
vs_alt
E1
E2
P
Q
:
(
P
⊑
pvs
E1
E2
Q
)
→
P
={
E1
,
E2
}=>
Q
.
Proof
.
intros
;
rewrite
-{
1
}
always_const
.
apply
(
always_intro
_
_
),
impl_intro_l
.
intros
;
rewrite
-{
1
}
always_const
.
apply
:
always_intro
.
apply
impl_intro_l
.
by
rewrite
always_const
right_id
.
Qed
.
...
...
@@ -51,7 +51,7 @@ Proof. by intros ?; apply vs_alt, pvs_timeless. Qed.
Lemma
vs_transitive
E1
E2
E3
P
Q
R
:
E2
⊆
E1
∪
E3
→
((
P
={
E1
,
E2
}=>
Q
)
∧
(
Q
={
E2
,
E3
}=>
R
))
⊑
(
P
={
E1
,
E3
}=>
R
).
Proof
.
intros
;
rewrite
-
always_and
;
apply
(
always_intro
_
_
),
impl_intro_l
.
intros
;
rewrite
-
always_and
;
apply
:
always_intro
.
apply
impl_intro_l
.
rewrite
always_and
assoc
(
always_elim
(
P
→
_
))
impl_elim_r
.
by
rewrite
pvs_impl_r
;
apply
pvs_trans
.
Qed
.
...
...
@@ -91,7 +91,7 @@ Lemma vs_open_close N E P Q R :
nclose
N
⊆
E
→
(
inv
N
R
★
(
▷
R
★
P
={
E
∖
nclose
N
}=>
▷
R
★
Q
))
⊑
(
P
={
E
}=>
Q
).
Proof
.
intros
;
apply
(
always_intro
_
_
),
impl_intro_l
.
intros
;
apply
:
always_intro
.
apply
impl_intro_l
.
rewrite
always_and_sep_r
assoc
[(
P
★
_
)%
I
]
comm
-
assoc
.
eapply
pvs_open_close
;
[
by
eauto
with
I
..|].
rewrite
sep_elim_r
.
apply
wand_intro_l
.
...
...
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