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
Rice Wine
Iris
Commits
4886e15f
Commit
4886e15f
authored
Oct 22, 2017
by
Robbert Krebbers
Browse files
Rename `Timeless` → `Discrete` (discrete OFE elements).
parent
b05660a6
Changes
16
Hide whitespace changes
Inline
Side-by-side
theories/algebra/agree.v
View file @
4886e15f
...
...
@@ -149,12 +149,12 @@ Proof. rewrite /CMRATotal; eauto. Qed.
Global
Instance
agree_persistent
(
x
:
agree
A
)
:
Persistent
x
.
Proof
.
by
constructor
.
Qed
.
Global
Instance
agree_
ofe
_discrete
:
OFEDiscrete
A
→
CMRADiscrete
agreeR
.
Global
Instance
agree_
cmra
_discrete
:
OFEDiscrete
A
→
CMRADiscrete
agreeR
.
Proof
.
intros
HD
.
split
.
-
intros
x
y
[
H
H'
]
n
;
split
=>
a
;
setoid_rewrite
<-(
timeless
_iff_0
_
_
)
;
auto
.
-
intros
x
y
[
H
H'
]
n
;
split
=>
a
;
setoid_rewrite
<-(
discrete
_iff_0
_
_
)
;
auto
.
-
intros
x
;
rewrite
agree_validN_def
=>
Hv
n
.
apply
agree_validN_def
=>
a
b
??.
apply
timeless
_iff_0
;
auto
.
apply
discrete
_iff_0
;
auto
.
Qed
.
Program
Definition
to_agree
(
a
:
A
)
:
agree
A
:
=
...
...
theories/algebra/auth.v
View file @
4886e15f
...
...
@@ -49,9 +49,9 @@ Proof.
(
λ
x
,
(
authoritative
x
,
auth_own
x
)))
;
by
repeat
intro
.
Qed
.
Global
Instance
Auth_
timeless
a
b
:
Timeless
a
→
Timeless
b
→
Timeless
(
Auth
a
b
).
Proof
.
by
intros
??
[??]
[??]
;
split
;
apply
:
timeless
.
Qed
.
Global
Instance
Auth_
discrete
a
b
:
Discrete
a
→
Discrete
b
→
Discrete
(
Auth
a
b
).
Proof
.
by
intros
??
[??]
[??]
;
split
;
apply
:
discrete
.
Qed
.
Global
Instance
auth_ofe_discrete
:
OFEDiscrete
A
→
OFEDiscrete
authC
.
Proof
.
intros
?
[??]
;
apply
_
.
Qed
.
Global
Instance
auth_leibniz
:
LeibnizEquiv
A
→
LeibnizEquiv
(
auth
A
).
...
...
theories/algebra/cmra.v
View file @
4886e15f
...
...
@@ -530,22 +530,22 @@ Section total_core.
Qed
.
End
total_core
.
(** **
Timeless
*)
Lemma
cmra_
timeless
_included_l
x
y
:
Timeless
x
→
✓
{
0
}
y
→
x
≼
{
0
}
y
→
x
≼
y
.
(** **
Discrete
*)
Lemma
cmra_
discrete
_included_l
x
y
:
Discrete
x
→
✓
{
0
}
y
→
x
≼
{
0
}
y
→
x
≼
y
.
Proof
.
intros
??
[
x'
?].
destruct
(
cmra_extend
0
y
x
x'
)
as
(
z
&
z'
&
Hy
&
Hz
&
Hz'
)
;
auto
;
simpl
in
*.
by
exists
z'
;
rewrite
Hy
(
timeless
x
z
).
by
exists
z'
;
rewrite
Hy
(
discrete
x
z
).
Qed
.
Lemma
cmra_
timeless
_included_r
x
y
:
Timeless
y
→
x
≼
{
0
}
y
→
x
≼
y
.
Proof
.
intros
?
[
x'
?].
exists
x'
.
by
apply
(
timeless
y
).
Qed
.
Lemma
cmra_op_
timeless
x1
x2
:
✓
(
x1
⋅
x2
)
→
Timeless
x1
→
Timeless
x2
→
Timeless
(
x1
⋅
x2
).
Lemma
cmra_
discrete
_included_r
x
y
:
Discrete
y
→
x
≼
{
0
}
y
→
x
≼
y
.
Proof
.
intros
?
[
x'
?].
exists
x'
.
by
apply
(
discrete
y
).
Qed
.
Lemma
cmra_op_
discrete
x1
x2
:
✓
(
x1
⋅
x2
)
→
Discrete
x1
→
Discrete
x2
→
Discrete
(
x1
⋅
x2
).
Proof
.
intros
???
z
Hz
.
destruct
(
cmra_extend
0
z
x1
x2
)
as
(
y1
&
y2
&
Hz'
&?&?)
;
auto
;
simpl
in
*.
{
rewrite
-
?Hz
.
by
apply
cmra_valid_validN
.
}
by
rewrite
Hz'
(
timeless
x1
y1
)
//
(
timeless
x2
y2
).
by
rewrite
Hz'
(
discrete
x1
y1
)
//
(
discrete
x2
y2
).
Qed
.
(** ** Discrete *)
...
...
@@ -557,7 +557,7 @@ Qed.
Lemma
cmra_discrete_included_iff
`
{
OFEDiscrete
A
}
n
x
y
:
x
≼
y
↔
x
≼
{
n
}
y
.
Proof
.
split
;
first
by
apply
cmra_included_includedN
.
intros
[
z
->%(
timeless
_iff
_
_
)]
;
eauto
using
cmra_included_l
.
intros
[
z
->%(
discrete
_iff
_
_
)]
;
eauto
using
cmra_included_l
.
Qed
.
(** Cancelable elements *)
...
...
@@ -567,7 +567,7 @@ Lemma cancelable x `{!Cancelable x} y z : ✓(x ⋅ y) → x ⋅ y ≡ x ⋅ z
Proof
.
rewrite
!
equiv_dist
cmra_valid_validN
.
intros
.
by
apply
(
cancelableN
x
).
Qed
.
Lemma
discrete_cancelable
x
`
{
CMRADiscrete
A
}
:
(
∀
y
z
,
✓
(
x
⋅
y
)
→
x
⋅
y
≡
x
⋅
z
→
y
≡
z
)
→
Cancelable
x
.
Proof
.
intros
????.
rewrite
-!
timeless
_iff
-
cmra_discrete_valid_iff
.
auto
.
Qed
.
Proof
.
intros
????.
rewrite
-!
discrete
_iff
-
cmra_discrete_valid_iff
.
auto
.
Qed
.
Global
Instance
cancelable_op
x
y
:
Cancelable
x
→
Cancelable
y
→
Cancelable
(
x
⋅
y
).
Proof
.
...
...
@@ -598,7 +598,7 @@ Proof. rewrite comm. eauto using id_free_r. Qed.
Lemma
discrete_id_free
x
`
{
CMRADiscrete
A
}
:
(
∀
y
,
✓
x
→
x
⋅
y
≡
x
→
False
)
→
IdFree
x
.
Proof
.
intros
Hx
y
??.
apply
(
Hx
y
),
(
timeless
_
)
;
eauto
using
cmra_discrete_valid
.
intros
Hx
y
??.
apply
(
Hx
y
),
(
discrete
_
)
;
eauto
using
cmra_discrete_valid
.
Qed
.
Global
Instance
id_free_op_r
x
y
:
IdFree
y
→
Cancelable
x
→
IdFree
(
x
⋅
y
).
Proof
.
...
...
@@ -845,7 +845,7 @@ Section cmra_transport.
Proof
.
by
destruct
H
.
Qed
.
Lemma
cmra_transport_valid
x
:
✓
T
x
↔
✓
x
.
Proof
.
by
destruct
H
.
Qed
.
Global
Instance
cmra_transport_
timeless
x
:
Timeless
x
→
Timeless
(
T
x
).
Global
Instance
cmra_transport_
discrete
x
:
Discrete
x
→
Discrete
(
T
x
).
Proof
.
by
destruct
H
.
Qed
.
Global
Instance
cmra_transport_persistent
x
:
Persistent
x
→
Persistent
(
T
x
).
Proof
.
by
destruct
H
.
Qed
.
...
...
theories/algebra/csum.v
View file @
4886e15f
...
...
@@ -97,15 +97,15 @@ Next Obligation.
Qed
.
Global
Instance
csum_ofe_discrete
:
OFEDiscrete
A
→
OFEDiscrete
B
→
OFEDiscrete
csumC
.
Proof
.
by
inversion_clear
3
;
constructor
;
apply
(
timeless
_
).
Qed
.
Proof
.
by
inversion_clear
3
;
constructor
;
apply
(
discrete
_
).
Qed
.
Global
Instance
csum_leibniz
:
LeibnizEquiv
A
→
LeibnizEquiv
B
→
LeibnizEquiv
(
csumC
A
B
).
Proof
.
by
destruct
3
;
f_equal
;
apply
leibniz_equiv
.
Qed
.
Global
Instance
Cinl_
timeless
a
:
Timeless
a
→
Timeless
(
Cinl
a
).
Proof
.
by
inversion_clear
2
;
constructor
;
apply
(
timeless
_
).
Qed
.
Global
Instance
Cinr_
timeless
b
:
Timeless
b
→
Timeless
(
Cinr
b
).
Proof
.
by
inversion_clear
2
;
constructor
;
apply
(
timeless
_
).
Qed
.
Global
Instance
Cinl_
discrete
a
:
Discrete
a
→
Discrete
(
Cinl
a
).
Proof
.
by
inversion_clear
2
;
constructor
;
apply
(
discrete
_
).
Qed
.
Global
Instance
Cinr_
discrete
b
:
Discrete
b
→
Discrete
(
Cinr
b
).
Proof
.
by
inversion_clear
2
;
constructor
;
apply
(
discrete
_
).
Qed
.
End
cofe
.
Arguments
csumC
:
clear
implicits
.
...
...
theories/algebra/excl.v
View file @
4886e15f
...
...
@@ -60,13 +60,13 @@ Proof.
Qed
.
Global
Instance
excl_ofe_discrete
:
OFEDiscrete
A
→
OFEDiscrete
exclC
.
Proof
.
by
inversion_clear
2
;
constructor
;
apply
(
timeless
_
).
Qed
.
Proof
.
by
inversion_clear
2
;
constructor
;
apply
(
discrete
_
).
Qed
.
Global
Instance
excl_leibniz
:
LeibnizEquiv
A
→
LeibnizEquiv
(
excl
A
).
Proof
.
by
destruct
2
;
f_equal
;
apply
leibniz_equiv
.
Qed
.
Global
Instance
Excl_
timeless
a
:
Timeless
a
→
Timeless
(
Excl
a
).
Proof
.
by
inversion_clear
2
;
constructor
;
apply
(
timeless
_
).
Qed
.
Global
Instance
ExclBot_
timeless
:
Timeless
(@
ExclBot
A
).
Global
Instance
Excl_
discrete
a
:
Discrete
a
→
Discrete
(
Excl
a
).
Proof
.
by
inversion_clear
2
;
constructor
;
apply
(
discrete
_
).
Qed
.
Global
Instance
ExclBot_
discrete
:
Discrete
(@
ExclBot
A
).
Proof
.
by
inversion_clear
1
;
constructor
.
Qed
.
(* CMRA *)
...
...
theories/algebra/frac_auth.v
View file @
4886e15f
...
...
@@ -34,10 +34,10 @@ Section frac_auth.
Global
Instance
frac_auth_frag_proper
q
:
Proper
((
≡
)
==>
(
≡
))
(@
frac_auth_frag
A
q
).
Proof
.
solve_proper
.
Qed
.
Global
Instance
frac_auth_auth_
timeless
a
:
Timeless
a
→
Timeless
(
●
!
a
).
Proof
.
intros
;
apply
Auth_
timeless
;
apply
_
.
Qed
.
Global
Instance
frac_auth_frag_
timeless
a
:
Timeless
a
→
Timeless
(
◯
!
a
).
Proof
.
intros
;
apply
Auth_
timeless
,
Some_timeless
;
apply
_
.
Qed
.
Global
Instance
frac_auth_auth_
discrete
a
:
Discrete
a
→
Discrete
(
●
!
a
).
Proof
.
intros
;
apply
Auth_
discrete
;
apply
_
.
Qed
.
Global
Instance
frac_auth_frag_
discrete
a
:
Discrete
a
→
Discrete
(
◯
!
a
).
Proof
.
intros
;
apply
Auth_
discrete
,
Some_discrete
;
apply
_
.
Qed
.
Lemma
frac_auth_validN
n
a
:
✓
{
n
}
a
→
✓
{
n
}
(
●
!
a
⋅
◯
!
a
).
Proof
.
done
.
Qed
.
...
...
theories/algebra/gmap.v
View file @
4886e15f
...
...
@@ -38,7 +38,7 @@ Next Obligation.
Qed
.
Global
Instance
gmap_ofe_discrete
:
OFEDiscrete
A
→
OFEDiscrete
gmapC
.
Proof
.
intros
?
m
m'
?
i
.
by
apply
(
timeless
_
).
Qed
.
Proof
.
intros
?
m
m'
?
i
.
by
apply
(
discrete
_
).
Qed
.
(* why doesn't this go automatic? *)
Global
Instance
gmapC_leibniz
:
LeibnizEquiv
A
→
LeibnizEquiv
gmapC
.
Proof
.
intros
;
change
(
LeibnizEquiv
(
gmap
K
A
))
;
apply
_
.
Qed
.
...
...
@@ -70,27 +70,27 @@ Proof.
[
by
constructor
|
by
apply
lookup_ne
].
Qed
.
Global
Instance
gmap_empty_
timeless
:
Timeless
(
∅
:
gmap
K
A
).
Global
Instance
gmap_empty_
discrete
:
Discrete
(
∅
:
gmap
K
A
).
Proof
.
intros
m
Hm
i
;
specialize
(
Hm
i
)
;
rewrite
lookup_empty
in
Hm
|-
*.
inversion_clear
Hm
;
constructor
.
Qed
.
Global
Instance
gmap_lookup_
timeless
m
i
:
Timeless
m
→
Timeless
(
m
!!
i
).
Global
Instance
gmap_lookup_
discrete
m
i
:
Discrete
m
→
Discrete
(
m
!!
i
).
Proof
.
intros
?
[
x
|]
Hx
;
[|
by
symmetry
;
apply
:
timeless
].
intros
?
[
x
|]
Hx
;
[|
by
symmetry
;
apply
:
discrete
].
assert
(
m
≡
{
0
}
≡
<[
i
:
=
x
]>
m
)
by
(
by
symmetry
in
Hx
;
inversion
Hx
;
ofe_subst
;
rewrite
insert_id
).
by
rewrite
(
timeless
m
(<[
i
:
=
x
]>
m
))
//
lookup_insert
.
by
rewrite
(
discrete
m
(<[
i
:
=
x
]>
m
))
//
lookup_insert
.
Qed
.
Global
Instance
gmap_insert_
timeless
m
i
x
:
Timeless
x
→
Timeless
m
→
Timeless
(<[
i
:
=
x
]>
m
).
Global
Instance
gmap_insert_
discrete
m
i
x
:
Discrete
x
→
Discrete
m
→
Discrete
(<[
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
:
discrete
;
rewrite
-
Hm
lookup_insert
.
}
by
apply
:
discrete
;
rewrite
-
Hm
lookup_insert_ne
.
Qed
.
Global
Instance
gmap_singleton_
timeless
i
x
:
Timeless
x
→
Timeless
({[
i
:
=
x
]}
:
gmap
K
A
)
:
=
_
.
Global
Instance
gmap_singleton_
discrete
i
x
:
Discrete
x
→
Discrete
({[
i
:
=
x
]}
:
gmap
K
A
)
:
=
_
.
End
cofe
.
Arguments
gmapC
_
{
_
_
}
_
.
...
...
theories/algebra/iprod.v
View file @
4886e15f
...
...
@@ -61,22 +61,22 @@ Section iprod_cofe.
x
≠
x'
→
(
iprod_insert
x
y
f
)
x'
=
f
x'
.
Proof
.
by
rewrite
/
iprod_insert
;
destruct
(
decide
_
).
Qed
.
Global
Instance
iprod_lookup_
timeless
f
x
:
Timeless
f
→
Timeless
(
f
x
).
Global
Instance
iprod_lookup_
discrete
f
x
:
Discrete
f
→
Discrete
(
f
x
).
Proof
.
intros
?
y
?.
cut
(
f
≡
iprod_insert
x
y
f
).
{
by
move
=>
/(
_
x
)->
;
rewrite
iprod_lookup_insert
.
}
apply
(
timeless
_
)=>
x'
;
destruct
(
decide
(
x
=
x'
))
as
[->|]
;
apply
(
discrete
_
)=>
x'
;
destruct
(
decide
(
x
=
x'
))
as
[->|]
;
by
rewrite
?iprod_lookup_insert
?iprod_lookup_insert_ne
.
Qed
.
Global
Instance
iprod_insert_
timeless
f
x
y
:
Timeless
f
→
Timeless
y
→
Timeless
(
iprod_insert
x
y
f
).
Global
Instance
iprod_insert_
discrete
f
x
y
:
Discrete
f
→
Discrete
y
→
Discrete
(
iprod_insert
x
y
f
).
Proof
.
intros
??
g
Heq
x'
;
destruct
(
decide
(
x
=
x'
))
as
[->|].
-
rewrite
iprod_lookup_insert
.
apply
:
timeless
.
by
rewrite
-(
Heq
x'
)
iprod_lookup_insert
.
apply
:
discrete
.
by
rewrite
-(
Heq
x'
)
iprod_lookup_insert
.
-
rewrite
iprod_lookup_insert_ne
//.
apply
:
timeless
.
by
rewrite
-(
Heq
x'
)
iprod_lookup_insert_ne
.
apply
:
discrete
.
by
rewrite
-(
Heq
x'
)
iprod_lookup_insert_ne
.
Qed
.
End
iprod_cofe
.
...
...
@@ -140,9 +140,9 @@ Section iprod_cmra.
Qed
.
Canonical
Structure
iprodUR
:
=
UCMRAT
(
iprod
B
)
iprod_ucmra_mixin
.
Global
Instance
iprod_empty_
timeless
:
(
∀
i
,
Timeless
(
ε
:
B
i
))
→
Timeless
(
ε
:
iprod
B
).
Proof
.
intros
?
f
Hf
x
.
by
apply
:
timeless
.
Qed
.
Global
Instance
iprod_empty_
discrete
:
(
∀
i
,
Discrete
(
ε
:
B
i
))
→
Discrete
(
ε
:
iprod
B
).
Proof
.
intros
?
f
Hf
x
.
by
apply
:
discrete
.
Qed
.
(** Internalized properties *)
Lemma
iprod_equivI
{
M
}
g1
g2
:
g1
≡
g2
⊣
⊢
(
∀
i
,
g1
i
≡
g2
i
:
uPred
M
).
...
...
@@ -198,8 +198,8 @@ Section iprod_singleton.
x
≠
x'
→
(
iprod_singleton
x
y
)
x'
=
ε
.
Proof
.
intros
;
by
rewrite
/
iprod_singleton
iprod_lookup_insert_ne
.
Qed
.
Global
Instance
iprod_singleton_
timeless
x
(
y
:
B
x
)
:
(
∀
i
,
Timeless
(
ε
:
B
i
))
→
Timeless
y
→
Timeless
(
iprod_singleton
x
y
).
Global
Instance
iprod_singleton_
discrete
x
(
y
:
B
x
)
:
(
∀
i
,
Discrete
(
ε
:
B
i
))
→
Discrete
y
→
Discrete
(
iprod_singleton
x
y
).
Proof
.
apply
_
.
Qed
.
Lemma
iprod_singleton_validN
n
x
(
y
:
B
x
)
:
✓
{
n
}
iprod_singleton
x
y
↔
✓
{
n
}
y
.
...
...
theories/algebra/list.v
View file @
4886e15f
...
...
@@ -78,12 +78,12 @@ Next Obligation.
Qed
.
Global
Instance
list_ofe_discrete
:
OFEDiscrete
A
→
OFEDiscrete
listC
.
Proof
.
induction
2
;
constructor
;
try
apply
(
timeless
_
)
;
auto
.
Qed
.
Proof
.
induction
2
;
constructor
;
try
apply
(
discrete
_
)
;
auto
.
Qed
.
Global
Instance
nil_
timeless
:
Timeless
(@
nil
A
).
Global
Instance
nil_
discrete
:
Discrete
(@
nil
A
).
Proof
.
inversion_clear
1
;
constructor
.
Qed
.
Global
Instance
cons_
timeless
x
l
:
Timeless
x
→
Timeless
l
→
Timeless
(
x
::
l
).
Proof
.
intros
??
;
inversion_clear
1
;
constructor
;
by
apply
timeless
.
Qed
.
Global
Instance
cons_
discrete
x
l
:
Discrete
x
→
Discrete
l
→
Discrete
(
x
::
l
).
Proof
.
intros
??
;
inversion_clear
1
;
constructor
;
by
apply
discrete
.
Qed
.
End
cofe
.
Arguments
listC
:
clear
implicits
.
...
...
theories/algebra/local_updates.v
View file @
4886e15f
...
...
@@ -56,8 +56,8 @@ Section updates.
(
x
,
y
)
~l
~>
(
x'
,
y'
)
↔
∀
mz
,
✓
x
→
x
≡
y
⋅
?
mz
→
✓
x'
∧
x'
≡
y'
⋅
?
mz
.
Proof
.
rewrite
/
local_update
/=.
setoid_rewrite
<-
cmra_discrete_valid_iff
.
setoid_rewrite
<-(
λ
n
,
timeless
_iff
n
x
).
setoid_rewrite
<-(
λ
n
,
timeless
_iff
n
x'
).
naive_solver
eauto
using
0
.
setoid_rewrite
<-(
λ
n
,
discrete
_iff
n
x
).
setoid_rewrite
<-(
λ
n
,
discrete
_iff
n
x'
).
naive_solver
eauto
using
0
.
Qed
.
Lemma
local_update_valid0
x
y
x'
y'
:
...
...
@@ -76,7 +76,7 @@ Section updates.
(
✓
x
→
✓
y
→
x
≡
y
∨
y
≼
x
→
(
x
,
y
)
~l
~>
(
x'
,
y'
))
→
(
x
,
y
)
~l
~>
(
x'
,
y'
).
Proof
.
rewrite
!(
cmra_discrete_valid_iff
0
)
(
cmra_discrete_included_iff
0
)
(
timeless
_iff
0
).
(
cmra_discrete_included_iff
0
)
(
discrete
_iff
0
).
apply
local_update_valid0
.
Qed
.
...
...
theories/algebra/ofe.v
View file @
4886e15f
...
...
@@ -99,15 +99,13 @@ End ofe_mixin.
Hint
Extern
1
(
_
≡
{
_
}
≡
_
)
=>
apply
equiv_dist
;
assumption
.
(** Discrete OFEs and Timeless elements *)
(* TODO: On paper, We called these "discrete elements". I think that makes
more sense. *)
Class
Timeless
{
A
:
ofeT
}
(
x
:
A
)
:
=
timeless
y
:
x
≡
{
0
}
≡
y
→
x
≡
y
.
Arguments
timeless
{
_
}
_
{
_
}
_
_
.
Hint
Mode
Timeless
+
!
:
typeclass_instances
.
Instance
:
Params
(@
Timeless
)
1
.
Class
OFEDiscrete
(
A
:
ofeT
)
:
=
ofe_discrete_timeless
(
x
:
A
)
:
>
Timeless
x
.
(** Discrete OFEs and discrete OFE elements *)
Class
Discrete
{
A
:
ofeT
}
(
x
:
A
)
:
=
discrete
y
:
x
≡
{
0
}
≡
y
→
x
≡
y
.
Arguments
discrete
{
_
}
_
{
_
}
_
_
.
Hint
Mode
Discrete
+
!
:
typeclass_instances
.
Instance
:
Params
(@
Discrete
)
1
.
Class
OFEDiscrete
(
A
:
ofeT
)
:
=
ofe_discrete_discrete
(
x
:
A
)
:
>
Discrete
x
.
Hint
Mode
OFEDiscrete
!
:
typeclass_instances
.
(** OFEs with a completion *)
...
...
@@ -165,8 +163,8 @@ Section ofe.
Qed
.
Global
Instance
dist_proper_2
n
x
:
Proper
((
≡
)
==>
iff
)
(
dist
n
x
).
Proof
.
by
apply
dist_proper
.
Qed
.
Global
Instance
Timeless
_proper
:
Proper
((
≡
)
==>
iff
)
(@
Timeless
A
).
Proof
.
intros
x
y
Hxy
.
rewrite
/
Timeless
.
by
setoid_rewrite
Hxy
.
Qed
.
Global
Instance
Discrete
_proper
:
Proper
((
≡
)
==>
iff
)
(@
Discrete
A
).
Proof
.
intros
x
y
Hxy
.
rewrite
/
Discrete
.
by
setoid_rewrite
Hxy
.
Qed
.
Lemma
dist_le
n
n'
x
y
:
x
≡
{
n
}
≡
y
→
n'
≤
n
→
x
≡
{
n'
}
≡
y
.
Proof
.
induction
2
;
eauto
using
dist_S
.
Qed
.
...
...
@@ -188,13 +186,13 @@ Section ofe.
apply
chain_cauchy
.
omega
.
Qed
.
Lemma
timeless
_iff
n
(
x
:
A
)
`
{!
Timeless
x
}
y
:
x
≡
y
↔
x
≡
{
n
}
≡
y
.
Lemma
discrete
_iff
n
(
x
:
A
)
`
{!
Discrete
x
}
y
:
x
≡
y
↔
x
≡
{
n
}
≡
y
.
Proof
.
split
;
intros
;
auto
.
apply
(
timeless
_
),
dist_le
with
n
;
auto
with
lia
.
split
;
intros
;
auto
.
apply
(
discrete
_
),
dist_le
with
n
;
auto
with
lia
.
Qed
.
Lemma
timeless
_iff_0
n
(
x
:
A
)
`
{!
Timeless
x
}
y
:
x
≡
{
0
}
≡
y
↔
x
≡
{
n
}
≡
y
.
Lemma
discrete
_iff_0
n
(
x
:
A
)
`
{!
Discrete
x
}
y
:
x
≡
{
0
}
≡
y
↔
x
≡
{
n
}
≡
y
.
Proof
.
split
=>
?.
by
apply
equiv_dist
,
(
timeless
_
).
eauto
using
dist_le
with
lia
.
split
=>
?.
by
apply
equiv_dist
,
(
discrete
_
).
eauto
using
dist_le
with
lia
.
Qed
.
End
ofe
.
...
...
@@ -273,7 +271,7 @@ Section limit_preserving.
Global
Instance
limit_preserving_const
(
P
:
Prop
)
:
LimitPreserving
(
λ
_
,
P
).
Proof
.
intros
c
HP
.
apply
(
HP
0
).
Qed
.
Lemma
limit_preserving_
timeless
(
P
:
A
→
Prop
)
:
Lemma
limit_preserving_
discrete
(
P
:
A
→
Prop
)
:
Proper
(
dist
0
==>
impl
)
P
→
LimitPreserving
P
.
Proof
.
intros
PH
c
Hc
.
by
rewrite
(
conv_compl
0
).
Qed
.
...
...
@@ -683,9 +681,9 @@ Section product.
apply
(
conv_compl
n
(
chain_map
snd
c
)).
Qed
.
Global
Instance
prod_
timeless
(
x
:
A
*
B
)
:
Timeless
(
x
.
1
)
→
Timeless
(
x
.
2
)
→
Timeless
x
.
Proof
.
by
intros
???[??]
;
split
;
apply
(
timeless
_
).
Qed
.
Global
Instance
prod_
discrete
(
x
:
A
*
B
)
:
Discrete
(
x
.
1
)
→
Discrete
(
x
.
2
)
→
Discrete
x
.
Proof
.
by
intros
???[??]
;
split
;
apply
(
discrete
_
).
Qed
.
Global
Instance
prod_ofe_discrete
:
OFEDiscrete
A
→
OFEDiscrete
B
→
OFEDiscrete
prodC
.
Proof
.
intros
??
[??]
;
apply
_
.
Qed
.
End
product
.
...
...
@@ -864,10 +862,10 @@ Section sum.
-
rewrite
(
conv_compl
n
(
inr_chain
c
_
))
/=.
destruct
(
c
n
)
;
naive_solver
.
Qed
.
Global
Instance
inl_
timeless
(
x
:
A
)
:
Timeless
x
→
Timeless
(
inl
x
).
Proof
.
inversion_clear
2
;
constructor
;
by
apply
(
timeless
_
).
Qed
.
Global
Instance
inr_
timeless
(
y
:
B
)
:
Timeless
y
→
Timeless
(
inr
y
).
Proof
.
inversion_clear
2
;
constructor
;
by
apply
(
timeless
_
).
Qed
.
Global
Instance
inl_
discrete
(
x
:
A
)
:
Discrete
x
→
Discrete
(
inl
x
).
Proof
.
inversion_clear
2
;
constructor
;
by
apply
(
discrete
_
).
Qed
.
Global
Instance
inr_
discrete
(
y
:
B
)
:
Discrete
y
→
Discrete
(
inr
y
).
Proof
.
inversion_clear
2
;
constructor
;
by
apply
(
discrete
_
).
Qed
.
Global
Instance
sum_ofe_discrete
:
OFEDiscrete
A
→
OFEDiscrete
B
→
OFEDiscrete
sumC
.
Proof
.
intros
??
[?|?]
;
apply
_
.
Qed
.
End
sum
.
...
...
@@ -993,7 +991,7 @@ Section option.
Qed
.
Global
Instance
option_ofe_discrete
:
OFEDiscrete
A
→
OFEDiscrete
optionC
.
Proof
.
destruct
2
;
constructor
;
by
apply
(
timeless
_
).
Qed
.
Proof
.
destruct
2
;
constructor
;
by
apply
(
discrete
_
).
Qed
.
Global
Instance
Some_ne
:
NonExpansive
(@
Some
A
).
Proof
.
by
constructor
.
Qed
.
...
...
@@ -1005,10 +1003,10 @@ Section option.
Proper
(
dist
n
==>
R
)
f
→
Proper
(
R
==>
dist
n
==>
R
)
(
from_option
f
).
Proof
.
destruct
3
;
simpl
;
auto
.
Qed
.
Global
Instance
None_
timeless
:
Timeless
(@
None
A
).
Global
Instance
None_
discrete
:
Discrete
(@
None
A
).
Proof
.
inversion_clear
1
;
constructor
.
Qed
.
Global
Instance
Some_
timeless
x
:
Timeless
x
→
Timeless
(
Some
x
).
Proof
.
by
intros
?
;
inversion_clear
1
;
constructor
;
apply
timeless
.
Qed
.
Global
Instance
Some_
discrete
x
:
Discrete
x
→
Discrete
(
Some
x
).
Proof
.
by
intros
?
;
inversion_clear
1
;
constructor
;
apply
discrete
.
Qed
.
Lemma
dist_None
n
mx
:
mx
≡
{
n
}
≡
None
↔
mx
=
None
.
Proof
.
split
;
[
by
inversion_clear
1
|
by
intros
->].
Qed
.
...
...
@@ -1224,8 +1222,8 @@ Section sigma.
Global
Instance
sig_cofe
`
{
Cofe
A
,
!
LimitPreserving
P
}
:
Cofe
sigC
.
Proof
.
apply
(
iso_cofe_subtype'
P
(
exist
P
)
proj1_sig
)=>
//.
by
intros
[].
Qed
.
Global
Instance
sig_
timeless
(
x
:
sig
P
)
:
Timeless
(
`
x
)
→
Timeless
x
.
Proof
.
intros
?
y
.
rewrite
sig_dist_alt
sig_equiv_alt
.
apply
(
timeless
_
).
Qed
.
Global
Instance
sig_
discrete
(
x
:
sig
P
)
:
Discrete
(
`
x
)
→
Discrete
x
.
Proof
.
intros
?
y
.
rewrite
sig_dist_alt
sig_equiv_alt
.
apply
(
discrete
_
).
Qed
.
Global
Instance
sig_ofe_discrete
:
OFEDiscrete
A
→
OFEDiscrete
sigC
.
Proof
.
intros
??.
apply
_
.
Qed
.
End
sigma
.
...
...
theories/algebra/vector.v
View file @
4886e15f
...
...
@@ -21,13 +21,13 @@ Section ofe.
-
intros
c
.
by
rewrite
(
conv_compl
0
(
chain_map
_
c
))
/=
vec_to_list_length
.
Qed
.
Global
Instance
vnil_
timeless
:
Timeless
(@
vnil
A
).
Global
Instance
vnil_
discrete
:
Discrete
(@
vnil
A
).
Proof
.
intros
v
_
.
by
inv_vec
v
.
Qed
.
Global
Instance
vcons_
timeless
n
x
(
v
:
vec
A
n
)
:
Timeless
x
→
Timeless
v
→
Timeless
(
x
:::
v
).
Global
Instance
vcons_
discrete
n
x
(
v
:
vec
A
n
)
:
Discrete
x
→
Discrete
v
→
Discrete
(
x
:::
v
).
Proof
.
intros
??
v'
?.
inv_vec
v'
=>
x'
v'
.
inversion_clear
1
.
constructor
.
by
apply
timeless
.
change
(
v
≡
v'
).
by
apply
timeless
.
constructor
.
by
apply
discrete
.
change
(
v
≡
v'
).
by
apply
discrete
.
Qed
.
Global
Instance
vec_ofe_discrete
m
:
OFEDiscrete
A
→
OFEDiscrete
(
vecC
m
).
Proof
.
intros
?
v
.
induction
v
;
apply
_
.
Qed
.
...
...
theories/base_logic/derived.v
View file @
4886e15f
...
...
@@ -794,7 +794,7 @@ Proof.
by
rewrite
-
bupd_intro
-
or_intro_l
.
Qed
.
(*
Timeless
instances *)
(*
Discrete
instances *)
Global
Instance
TimelessP_proper
:
Proper
((
≡
)
==>
iff
)
(@
TimelessP
M
).
Proof
.
solve_proper
.
Qed
.
Global
Instance
pure_timeless
φ
:
TimelessP
(
⌜φ⌝
:
uPred
M
)%
I
.
...
...
@@ -848,9 +848,9 @@ Proof. intros; rewrite /TimelessP except_0_always -always_later; auto. Qed.
Global
Instance
always_if_timeless
p
P
:
TimelessP
P
→
TimelessP
(
□
?p
P
).
Proof
.
destruct
p
;
apply
_
.
Qed
.
Global
Instance
eq_timeless
{
A
:
ofeT
}
(
a
b
:
A
)
:
Timeless
a
→
TimelessP
(
a
≡
b
:
uPred
M
)%
I
.
Proof
.
intros
.
rewrite
/
TimelessP
!
timeless
_eq
.
apply
(
timelessP
_
).
Qed
.
Global
Instance
ownM_timeless
(
a
:
M
)
:
Timeless
a
→
TimelessP
(
uPred_ownM
a
).
Discrete
a
→
TimelessP
(
a
≡
b
:
uPred
M
)%
I
.
Proof
.
intros
.
rewrite
/
TimelessP
!
discrete
_eq
.
apply
(
timelessP
_
).
Qed
.
Global
Instance
ownM_timeless
(
a
:
M
)
:
Discrete
a
→
TimelessP
(
uPred_ownM
a
).
Proof
.
intros
?.
rewrite
/
TimelessP
later_ownM
.
apply
exist_elim
=>
b
.
rewrite
(
timelessP
(
a
≡
b
))
(
except_0_intro
(
uPred_ownM
b
))
-
except_0_and
.
...
...
theories/base_logic/lib/own.v
View file @
4886e15f
...
...
@@ -106,7 +106,7 @@ 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
).
Global
Instance
own_timeless
γ
a
:
Discrete
a
→
TimelessP
(
own
γ
a
).
Proof
.
rewrite
!
own_eq
/
own_def
;
apply
_
.
Qed
.
Global
Instance
own_core_persistent
γ
a
:
Persistent
a
→
PersistentP
(
own
γ
a
).
Proof
.
rewrite
!
own_eq
/
own_def
;
apply
_
.
Qed
.
...
...
theories/base_logic/primitive.v
View file @
4886e15f
...
...
@@ -563,9 +563,9 @@ Proof. by unseal. Qed.
(* Discrete *)
Lemma
discrete_valid
{
A
:
cmraT
}
`
{!
CMRADiscrete
A
}
(
a
:
A
)
:
✓
a
⊣
⊢
⌜✓
a
⌝
.
Proof
.
unseal
;
split
=>
n
x
_
.
by
rewrite
/=
-
cmra_discrete_valid_iff
.
Qed
.
Lemma
timeless
_eq
{
A
:
ofeT
}
(
a
b
:
A
)
:
Timeless
a
→
a
≡
b
⊣
⊢
⌜
a
≡
b
⌝
.
Lemma
discrete
_eq
{
A
:
ofeT
}
(
a
b
:
A
)
:
Discrete
a
→
a
≡
b
⊣
⊢
⌜
a
≡
b
⌝
.
Proof
.
unseal
=>
?.
apply
(
anti_symm
(
⊢
))
;
split
=>
n
x
?
;
by
apply
(
timeless
_iff
n
).
unseal
=>
?.
apply
(
anti_symm
(
⊢
))
;
split
=>
n
x
?
;
by
apply
(
discrete
_iff
n
).
Qed
.
(* Option *)
...
...
theories/proofmode/class_instances.v
View file @
4886e15f
...
...
@@ -42,8 +42,8 @@ Proof. rewrite /FromAssumption=> <-. by rewrite forall_elim. Qed.
Global
Instance
into_pure_pure
φ
:
@
IntoPure
M
⌜φ⌝
φ
.
Proof
.
done
.
Qed
.
Global
Instance
into_pure_eq
{
A
:
ofeT
}
(
a
b
:
A
)
:
Timeless
a
→
@
IntoPure
M
(
a
≡
b
)
(
a
≡
b
).
Proof
.
intros
.
by
rewrite
/
IntoPure
timeless
_eq
.
Qed
.
Discrete
a
→
@
IntoPure
M
(
a
≡
b
)
(
a
≡
b
).
Proof
.
intros
.
by
rewrite
/
IntoPure
discrete
_eq
.
Qed
.
Global
Instance
into_pure_cmra_valid
`
{
CMRADiscrete
A
}
(
a
:
A
)
:
@
IntoPure
M
(
✓
a
)
(
✓
a
).
Proof
.
by
rewrite
/
IntoPure
discrete_valid
.
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