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
03863370
Commit
03863370
authored
Feb 11, 2016
by
Ralf Jung
Browse files
rename own lemmas in upred to ownM, to avoid overlapping names
parent
c93d1cd0
Changes
3
Hide whitespace changes
Inline
Side-by-side
algebra/upred.v
View file @
03863370
...
...
@@ -784,7 +784,7 @@ Lemma always_entails_r P Q : (P ⊑ □ Q) → P ⊑ (P ★ □ Q).
Proof
.
intros
;
rewrite
-
always_and_sep_r
;
auto
.
Qed
.
(
*
Own
and
valid
*
)
Lemma
own_op
(
a1
a2
:
M
)
:
Lemma
own
M
_op
(
a1
a2
:
M
)
:
uPred_own
(
a1
⋅
a2
)
≡
(
uPred_own
a1
★
uPred_own
a2
)
%
I
.
Proof
.
intros
x
n
?
;
split
.
...
...
@@ -794,19 +794,19 @@ Proof.
by
rewrite
(
associative
op
_
z1
)
-
(
commutative
op
z1
)
(
associative
op
z1
)
-
(
associative
op
_
a2
)
(
commutative
op
z1
)
-
Hy1
-
Hy2
.
Qed
.
Lemma
always_own_unit
(
a
:
M
)
:
(
□
uPred_own
(
unit
a
))
%
I
≡
uPred_own
(
unit
a
).
Lemma
always_own
M
_unit
(
a
:
M
)
:
(
□
uPred_own
(
unit
a
))
%
I
≡
uPred_own
(
unit
a
).
Proof
.
intros
x
n
;
split
;
[
by
apply
always_elim
|
intros
[
a
'
Hx
]];
simpl
.
rewrite
-
(
cmra_unit_idempotent
a
)
Hx
.
apply
cmra_unit_preservingN
,
cmra_includedN_l
.
Qed
.
Lemma
always_own
(
a
:
M
)
:
unit
a
≡
a
→
(
□
uPred_own
a
)
%
I
≡
uPred_own
a
.
Proof
.
by
intros
<-
;
rewrite
always_own_unit
.
Qed
.
Lemma
own_something
:
True
⊑
∃
a
,
uPred_own
a
.
Lemma
always_own
M
(
a
:
M
)
:
unit
a
≡
a
→
(
□
uPred_own
a
)
%
I
≡
uPred_own
a
.
Proof
.
by
intros
<-
;
rewrite
always_own
M
_unit
.
Qed
.
Lemma
own
M
_something
:
True
⊑
∃
a
,
uPred_own
a
.
Proof
.
intros
x
n
??
.
by
exists
x
;
simpl
.
Qed
.
Lemma
own_empty
`
{
Empty
M
,
!
CMRAIdentity
M
}
:
True
⊑
uPred_own
∅
.
Lemma
own
M
_empty
`
{
Empty
M
,
!
CMRAIdentity
M
}
:
True
⊑
uPred_own
∅
.
Proof
.
intros
x
n
??
;
by
exists
x
;
rewrite
(
left_id
_
_
).
Qed
.
Lemma
own_valid
(
a
:
M
)
:
uPred_own
a
⊑
✓
a
.
Lemma
own
M
_valid
(
a
:
M
)
:
uPred_own
a
⊑
✓
a
.
Proof
.
intros
x
n
Hv
[
a
'
?
];
cofe_subst
;
eauto
using
cmra_validN_op_l
.
Qed
.
Lemma
valid_intro
{
A
:
cmraT
}
(
a
:
A
)
:
✓
a
→
True
⊑
✓
a
.
Proof
.
by
intros
?
x
n
?
_
;
simpl
;
apply
cmra_valid_validN
.
Qed
.
...
...
@@ -819,8 +819,8 @@ Lemma always_valid {A : cmraT} (a : A) : (□ (✓ a))%I ≡ (✓ a : uPred M)%I
Proof
.
done
.
Qed
.
(
*
Own
and
valid
derived
*
)
Lemma
own_invalid
(
a
:
M
)
:
¬
✓
{
0
}
a
→
uPred_own
a
⊑
False
.
Proof
.
by
intros
;
rewrite
own_valid
valid_elim
.
Qed
.
Lemma
own
M
_invalid
(
a
:
M
)
:
¬
✓
{
0
}
a
→
uPred_own
a
⊑
False
.
Proof
.
by
intros
;
rewrite
own
M
_valid
valid_elim
.
Qed
.
(
*
Big
ops
*
)
Global
Instance
uPred_big_and_proper
:
Proper
((
≡
)
==>
(
≡
))
(
@
uPred_big_and
M
).
...
...
@@ -935,7 +935,7 @@ Proof. by intros; rewrite /AlwaysStable always_valid. Qed.
Global
Instance
later_always_stable
P
:
AS
P
→
AS
(
▷
P
).
Proof
.
by
intros
;
rewrite
/
AlwaysStable
always_later
;
apply
later_mono
.
Qed
.
Global
Instance
own_unit_always_stable
(
a
:
M
)
:
AS
(
uPred_own
(
unit
a
)).
Proof
.
by
rewrite
/
AlwaysStable
always_own_unit
.
Qed
.
Proof
.
by
rewrite
/
AlwaysStable
always_own
M
_unit
.
Qed
.
Global
Instance
default_always_stable
{
A
}
P
(
Q
:
A
→
uPred
M
)
(
mx
:
option
A
)
:
AS
P
→
(
∀
x
,
AS
(
Q
x
))
→
AS
(
default
P
mx
Q
).
Proof
.
destruct
mx
;
apply
_.
Qed
.
...
...
program_logic/auth.v
View file @
03863370
Require
Export
algebra
.
auth
algebra
.
functor
.
Require
Export
program_logic
.
invariants
program_logic
.
ghost_ownership
.
Import
uPred
ghost_ownership
.
Import
uPred
.
Section
auth
.
Context
{
A
:
cmraT
}
`
{
Empty
A
,
!
CMRAIdentity
A
}
.
...
...
program_logic/ownership.v
View file @
03863370
...
...
@@ -27,7 +27,7 @@ Proof.
Qed
.
Lemma
always_ownI
i
P
:
(
□
ownI
i
P
)
%
I
≡
ownI
i
P
.
Proof
.
apply
uPred
.
always_own
.
apply
uPred
.
always_own
M
.
by
rewrite
Res_unit
!
cmra_unit_empty
map_unit_singleton
.
Qed
.
Global
Instance
ownI_always_stable
i
P
:
AlwaysStable
(
ownI
i
P
).
...
...
@@ -38,8 +38,8 @@ Proof. apply (uPred.always_sep_dup' _). Qed.
(
*
physical
state
*
)
Lemma
ownP_twice
σ
1
σ
2
:
(
ownP
σ
1
★
ownP
σ
2
:
iProp
Λ
Σ
)
⊑
False
.
Proof
.
rewrite
/
ownP
-
uPred
.
own_op
Res_op
.
by
apply
uPred
.
own_invalid
;
intros
(
_
&?&
_
).
rewrite
/
ownP
-
uPred
.
own
M
_op
Res_op
.
by
apply
uPred
.
own
M
_invalid
;
intros
(
_
&?&
_
).
Qed
.
Global
Instance
ownP_timeless
σ
:
TimelessP
(
@
ownP
Λ
Σ
σ
).
Proof
.
rewrite
/
ownP
;
apply
_.
Qed
.
...
...
@@ -49,14 +49,14 @@ Global Instance ownG_ne n : Proper (dist n ==> dist n) (@ownG Λ Σ).
Proof
.
by
intros
m
m
'
Hm
;
unfold
ownG
;
rewrite
Hm
.
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
.
own_op
Res_op
!
(
left_id
_
_
).
Qed
.
Proof
.
by
rewrite
/
ownG
-
uPred
.
own
M
_op
Res_op
!
(
left_id
_
_
).
Qed
.
Lemma
always_ownG_unit
m
:
(
□
ownG
(
unit
m
))
%
I
≡
ownG
(
unit
m
).
Proof
.
apply
uPred
.
always_own
.
apply
uPred
.
always_own
M
.
by
rewrite
Res_unit
!
cmra_unit_empty
-{
2
}
(
cmra_unit_idempotent
m
).
Qed
.
Lemma
ownG_valid
m
:
(
ownG
m
)
⊑
(
✓
m
).
Proof
.
by
rewrite
/
ownG
uPred
.
own_valid
;
apply
uPred
.
valid_mono
=>
n
[
?
[]].
Qed
.
Proof
.
by
rewrite
/
ownG
uPred
.
own
M
_valid
;
apply
uPred
.
valid_mono
=>
n
[
?
[]].
Qed
.
Lemma
ownG_valid_r
m
:
(
ownG
m
)
⊑
(
ownG
m
★
✓
m
).
Proof
.
apply
(
uPred
.
always_entails_r
'
_
_
),
ownG_valid
.
Qed
.
Global
Instance
ownG_timeless
m
:
Timeless
m
→
TimelessP
(
ownG
m
).
...
...
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