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
75518c9a
Commit
75518c9a
authored
Nov 22, 2016
by
Ralf Jung
Browse files
use OFEs instead of COFEs everywhere
Use COFEs only for the recursive domain equation solver
parent
cde5b548
Changes
24
Expand all
Hide whitespace changes
Inline
Side-by-side
CHANGELOG.md
View file @
75518c9a
...
...
@@ -9,6 +9,9 @@ Coq development, but not every API-breaking change is listed. Changes marked
updates. Weakestpre is defined inside the logic, and invariants and view
shifts with masks are also coded up inside Iris. Adequacy of weakestpre
is proven in the logic.
*
Use OFEs instead of COFEs everywhere. COFEs are only used for solving the
recursive domain equation. As a consequence, CMRAs no longer need a proof
of completeness.
*
Renaming and moving things around: uPred and the rest of the base logic are
in [base_logic], while [program_logic] is for everything involving the
general Iris notion of a language.
...
...
_CoqProject
View file @
75518c9a
...
...
@@ -43,7 +43,7 @@ algebra/cmra_tactics.v
algebra/sts.v
algebra/auth.v
algebra/gmap.v
algebra/
c
ofe.v
algebra/ofe.v
algebra/base.v
algebra/dra.v
algebra/cofe_solver.v
...
...
algebra/agree.v
View file @
75518c9a
...
...
@@ -12,7 +12,7 @@ Arguments agree_car {_} _ _.
Arguments
agree_is_valid
{
_
}
_
_
.
Section
agree
.
Context
{
A
:
c
ofeT
}.
Context
{
A
:
ofeT
}.
Instance
agree_validN
:
ValidN
(
agree
A
)
:
=
λ
n
x
,
agree_is_valid
x
n
∧
∀
n'
,
n'
≤
n
→
agree_car
x
n
≡
{
n'
}
≡
agree_car
x
n'
.
...
...
@@ -28,13 +28,7 @@ Instance agree_equiv : Equiv (agree A) := λ x y,
Instance
agree_dist
:
Dist
(
agree
A
)
:
=
λ
n
x
y
,
(
∀
n'
,
n'
≤
n
→
agree_is_valid
x
n'
↔
agree_is_valid
y
n'
)
∧
(
∀
n'
,
n'
≤
n
→
agree_is_valid
x
n'
→
agree_car
x
n'
≡
{
n'
}
≡
agree_car
y
n'
).
Program
Instance
agree_compl
:
Compl
(
agree
A
)
:
=
λ
c
,
{|
agree_car
n
:
=
agree_car
(
c
n
)
n
;
agree_is_valid
n
:
=
agree_is_valid
(
c
n
)
n
|}.
Next
Obligation
.
intros
c
n
?.
apply
(
chain_cauchy
c
n
(
S
n
)),
agree_valid_S
;
auto
.
Qed
.
Definition
agree_cofe_mixin
:
CofeMixin
(
agree
A
).
Definition
agree_ofe_mixin
:
OfeMixin
(
agree
A
).
Proof
.
split
.
-
intros
x
y
;
split
.
...
...
@@ -47,10 +41,21 @@ Proof.
*
trans
(
agree_is_valid
y
n'
).
by
apply
Hxy
.
by
apply
Hyz
.
*
trans
(
agree_car
y
n'
).
by
apply
Hxy
.
by
apply
Hyz
,
Hxy
.
-
intros
n
x
y
Hxy
;
split
;
intros
;
apply
Hxy
;
auto
.
-
intros
n
c
;
apply
and_wlog_r
;
intros
;
symmetry
;
apply
(
chain_cauchy
c
)
;
naive_solver
.
Qed
.
Canonical
Structure
agreeC
:
=
CofeT
(
agree
A
)
agree_cofe_mixin
.
Canonical
Structure
agreeC
:
=
OfeT
(
agree
A
)
agree_ofe_mixin
.
Program
Definition
agree_compl
:
Compl
agreeC
:
=
λ
c
,
{|
agree_car
n
:
=
agree_car
(
c
n
)
n
;
agree_is_valid
n
:
=
agree_is_valid
(
c
n
)
n
|}.
Next
Obligation
.
intros
c
n
?.
apply
(
chain_cauchy
c
n
(
S
n
)),
agree_valid_S
;
auto
.
Qed
.
Global
Program
Instance
agree_cofe
:
Cofe
agreeC
:
=
{|
compl
:
=
agree_compl
|}.
Next
Obligation
.
intros
n
c
;
apply
and_wlog_r
;
intros
;
symmetry
;
apply
(
chain_cauchy
c
)
;
naive_solver
.
Qed
.
Program
Instance
agree_op
:
Op
(
agree
A
)
:
=
λ
x
y
,
{|
agree_car
:
=
agree_car
x
;
...
...
@@ -113,7 +118,7 @@ Proof.
+
by
move
:
Hval
;
rewrite
Hx
;
move
=>
/
agree_op_inv
->
;
rewrite
agree_idemp
.
Qed
.
Canonical
Structure
agreeR
:
cmraT
:
=
CMRAT
(
agree
A
)
agree_
c
ofe_mixin
agree_cmra_mixin
.
CMRAT
(
agree
A
)
agree_ofe_mixin
agree_cmra_mixin
.
Global
Instance
agree_total
:
CMRATotal
agreeR
.
Proof
.
rewrite
/
CMRATotal
;
eauto
.
Qed
.
...
...
@@ -159,7 +164,7 @@ Lemma agree_map_compose {A B C} (f : A → B) (g : B → C) (x : agree A) :
Proof
.
done
.
Qed
.
Section
agree_map
.
Context
{
A
B
:
c
ofeT
}
(
f
:
A
→
B
)
`
{
Hf
:
∀
n
,
Proper
(
dist
n
==>
dist
n
)
f
}.
Context
{
A
B
:
ofeT
}
(
f
:
A
→
B
)
`
{
Hf
:
∀
n
,
Proper
(
dist
n
==>
dist
n
)
f
}.
Instance
agree_map_ne
n
:
Proper
(
dist
n
==>
dist
n
)
(
agree_map
f
).
Proof
.
by
intros
x1
x2
Hx
;
split
;
simpl
;
intros
;
[
apply
Hx
|
apply
Hf
,
Hx
].
Qed
.
Instance
agree_map_proper
:
Proper
((
≡
)
==>
(
≡
))
(
agree_map
f
)
:
=
ne_proper
_
.
...
...
algebra/auth.v
View file @
75518c9a
...
...
@@ -14,7 +14,7 @@ Notation "● a" := (Auth (Excl' a) ∅) (at level 20).
(* COFE *)
Section
cofe
.
Context
{
A
:
c
ofeT
}.
Context
{
A
:
ofeT
}.
Implicit
Types
a
:
excl'
A
.
Implicit
Types
b
:
A
.
Implicit
Types
x
y
:
auth
A
.
...
...
@@ -37,9 +37,7 @@ Proof. by destruct 1. Qed.
Global
Instance
own_proper
:
Proper
((
≡
)
==>
(
≡
))
(@
auth_own
A
).
Proof
.
by
destruct
1
.
Qed
.
Instance
auth_compl
:
Compl
(
auth
A
)
:
=
λ
c
,
Auth
(
compl
(
chain_map
authoritative
c
))
(
compl
(
chain_map
auth_own
c
)).
Definition
auth_cofe_mixin
:
CofeMixin
(
auth
A
).
Definition
auth_ofe_mixin
:
OfeMixin
(
auth
A
).
Proof
.
split
.
-
intros
x
y
;
unfold
dist
,
auth_dist
,
equiv
,
auth_equiv
.
...
...
@@ -49,10 +47,17 @@ Proof.
+
by
intros
??
[??]
;
split
;
symmetry
.
+
intros
???
[??]
[??]
;
split
;
etrans
;
eauto
.
-
by
intros
?
[??]
[??]
[??]
;
split
;
apply
dist_S
.
-
intros
n
c
;
split
.
apply
(
conv_compl
n
(
chain_map
authoritative
c
)).
apply
(
conv_compl
n
(
chain_map
auth_own
c
)).
Qed
.
Canonical
Structure
authC
:
=
CofeT
(
auth
A
)
auth_cofe_mixin
.
Canonical
Structure
authC
:
=
OfeT
(
auth
A
)
auth_ofe_mixin
.
Definition
auth_compl
`
{
Cofe
A
}
:
Compl
authC
:
=
λ
c
,
Auth
(
compl
(
chain_map
authoritative
c
))
(
compl
(
chain_map
auth_own
c
)).
Global
Program
Instance
auth_cofe
`
{
Cofe
A
}
:
Cofe
authC
:
=
{|
compl
:
=
auth_compl
|}.
Next
Obligation
.
intros
?
n
c
;
split
.
apply
(
conv_compl
n
(
chain_map
authoritative
c
)).
apply
(
conv_compl
n
(
chain_map
auth_own
c
)).
Qed
.
Global
Instance
Auth_timeless
a
b
:
Timeless
a
→
Timeless
b
→
Timeless
(
Auth
a
b
).
...
...
@@ -151,7 +156,7 @@ Proof.
as
(
b1
&
b2
&?&?&?)
;
auto
using
auth_own_validN
.
by
exists
(
Auth
ea1
b1
),
(
Auth
ea2
b2
).
Qed
.
Canonical
Structure
authR
:
=
CMRAT
(
auth
A
)
auth_
c
ofe_mixin
auth_cmra_mixin
.
Canonical
Structure
authR
:
=
CMRAT
(
auth
A
)
auth_ofe_mixin
auth_cmra_mixin
.
Global
Instance
auth_cmra_discrete
:
CMRADiscrete
A
→
CMRADiscrete
authR
.
Proof
.
...
...
@@ -171,7 +176,7 @@ Proof.
-
do
2
constructor
;
simpl
;
apply
(
persistent_core
_
).
Qed
.
Canonical
Structure
authUR
:
=
UCMRAT
(
auth
A
)
auth_
c
ofe_mixin
auth_cmra_mixin
auth_ucmra_mixin
.
UCMRAT
(
auth
A
)
auth_ofe_mixin
auth_cmra_mixin
auth_ucmra_mixin
.
Global
Instance
auth_frag_persistent
a
:
Persistent
a
→
Persistent
(
◯
a
).
Proof
.
do
2
constructor
;
simpl
;
auto
.
by
apply
persistent_core
.
Qed
.
...
...
@@ -235,13 +240,13 @@ Proof. by destruct x as [[[]|]]. Qed.
Lemma
auth_map_compose
{
A
B
C
}
(
f
:
A
→
B
)
(
g
:
B
→
C
)
(
x
:
auth
A
)
:
auth_map
(
g
∘
f
)
x
=
auth_map
g
(
auth_map
f
x
).
Proof
.
by
destruct
x
as
[[[]|]].
Qed
.
Lemma
auth_map_ext
{
A
B
:
c
ofeT
}
(
f
g
:
A
→
B
)
x
:
Lemma
auth_map_ext
{
A
B
:
ofeT
}
(
f
g
:
A
→
B
)
x
:
(
∀
x
,
f
x
≡
g
x
)
→
auth_map
f
x
≡
auth_map
g
x
.
Proof
.
constructor
;
simpl
;
auto
.
apply
option_fmap_setoid_ext
=>
a
;
by
apply
excl_map_ext
.
Qed
.
Instance
auth_map_ne
{
A
B
:
c
ofeT
}
n
:
Instance
auth_map_ne
{
A
B
:
ofeT
}
n
:
Proper
((
dist
n
==>
dist
n
)
==>
dist
n
==>
dist
n
)
(@
auth_map
A
B
).
Proof
.
intros
f
g
Hf
[??]
[??]
[??]
;
split
;
simpl
in
*
;
[|
by
apply
Hf
].
...
...
algebra/cmra.v
View file @
75518c9a
From
iris
.
algebra
Require
Export
c
ofe
.
From
iris
.
algebra
Require
Export
ofe
.
Class
PCore
(
A
:
Type
)
:
=
pcore
:
A
→
option
A
.
Instance
:
Params
(@
pcore
)
2
.
...
...
@@ -61,34 +61,32 @@ Structure cmraT := CMRAT' {
cmra_car
:
>
Type
;
cmra_equiv
:
Equiv
cmra_car
;
cmra_dist
:
Dist
cmra_car
;
cmra_compl
:
Compl
cmra_car
;
cmra_pcore
:
PCore
cmra_car
;
cmra_op
:
Op
cmra_car
;
cmra_valid
:
Valid
cmra_car
;
cmra_validN
:
ValidN
cmra_car
;
cmra_
c
ofe_mixin
:
Co
feMixin
cmra_car
;
cmra_ofe_mixin
:
O
feMixin
cmra_car
;
cmra_mixin
:
CMRAMixin
cmra_car
;
_
:
Type
}.
Arguments
CMRAT'
_
{
_
_
_
_
_
_
_
}
_
_
_
.
Arguments
CMRAT'
_
{
_
_
_
_
_
_
}
_
_
_
.
Notation
CMRAT
A
m
m'
:
=
(
CMRAT'
A
m
m'
A
).
Arguments
cmra_car
:
simpl
never
.
Arguments
cmra_equiv
:
simpl
never
.
Arguments
cmra_dist
:
simpl
never
.
Arguments
cmra_compl
:
simpl
never
.
Arguments
cmra_pcore
:
simpl
never
.
Arguments
cmra_op
:
simpl
never
.
Arguments
cmra_valid
:
simpl
never
.
Arguments
cmra_validN
:
simpl
never
.
Arguments
cmra_
c
ofe_mixin
:
simpl
never
.
Arguments
cmra_ofe_mixin
:
simpl
never
.
Arguments
cmra_mixin
:
simpl
never
.
Add
Printing
Constructor
cmraT
.
Hint
Extern
0
(
PCore
_
)
=>
eapply
(@
cmra_pcore
_
)
:
typeclass_instances
.
Hint
Extern
0
(
Op
_
)
=>
eapply
(@
cmra_op
_
)
:
typeclass_instances
.
Hint
Extern
0
(
Valid
_
)
=>
eapply
(@
cmra_valid
_
)
:
typeclass_instances
.
Hint
Extern
0
(
ValidN
_
)
=>
eapply
(@
cmra_validN
_
)
:
typeclass_instances
.
Coercion
cmra_
c
ofeC
(
A
:
cmraT
)
:
c
ofeT
:
=
Co
feT
A
(
cmra_
c
ofe_mixin
A
).
Canonical
Structure
cmra_
c
ofeC
.
Coercion
cmra_ofeC
(
A
:
cmraT
)
:
ofeT
:
=
O
feT
A
(
cmra_ofe_mixin
A
).
Canonical
Structure
cmra_ofeC
.
(** Lifting properties from the mixin *)
Section
cmra_mixin
.
...
...
@@ -160,36 +158,34 @@ Structure ucmraT := UCMRAT' {
ucmra_car
:
>
Type
;
ucmra_equiv
:
Equiv
ucmra_car
;
ucmra_dist
:
Dist
ucmra_car
;
ucmra_compl
:
Compl
ucmra_car
;
ucmra_pcore
:
PCore
ucmra_car
;
ucmra_op
:
Op
ucmra_car
;
ucmra_valid
:
Valid
ucmra_car
;
ucmra_validN
:
ValidN
ucmra_car
;
ucmra_empty
:
Empty
ucmra_car
;
ucmra_
c
ofe_mixin
:
Co
feMixin
ucmra_car
;
ucmra_ofe_mixin
:
O
feMixin
ucmra_car
;
ucmra_cmra_mixin
:
CMRAMixin
ucmra_car
;
ucmra_mixin
:
UCMRAMixin
ucmra_car
;
_
:
Type
;
}.
Arguments
UCMRAT'
_
{
_
_
_
_
_
_
_
_
}
_
_
_
_
.
Arguments
UCMRAT'
_
{
_
_
_
_
_
_
_
}
_
_
_
_
.
Notation
UCMRAT
A
m
m'
m''
:
=
(
UCMRAT'
A
m
m'
m''
A
).
Arguments
ucmra_car
:
simpl
never
.
Arguments
ucmra_equiv
:
simpl
never
.
Arguments
ucmra_dist
:
simpl
never
.
Arguments
ucmra_compl
:
simpl
never
.
Arguments
ucmra_pcore
:
simpl
never
.
Arguments
ucmra_op
:
simpl
never
.
Arguments
ucmra_valid
:
simpl
never
.
Arguments
ucmra_validN
:
simpl
never
.
Arguments
ucmra_
c
ofe_mixin
:
simpl
never
.
Arguments
ucmra_ofe_mixin
:
simpl
never
.
Arguments
ucmra_cmra_mixin
:
simpl
never
.
Arguments
ucmra_mixin
:
simpl
never
.
Add
Printing
Constructor
ucmraT
.
Hint
Extern
0
(
Empty
_
)
=>
eapply
(@
ucmra_empty
_
)
:
typeclass_instances
.
Coercion
ucmra_
c
ofeC
(
A
:
ucmraT
)
:
c
ofeT
:
=
Co
feT
A
(
ucmra_
c
ofe_mixin
A
).
Canonical
Structure
ucmra_
c
ofeC
.
Coercion
ucmra_ofeC
(
A
:
ucmraT
)
:
ofeT
:
=
O
feT
A
(
ucmra_ofe_mixin
A
).
Canonical
Structure
ucmra_ofeC
.
Coercion
ucmra_cmraR
(
A
:
ucmraT
)
:
cmraT
:
=
CMRAT
A
(
ucmra_
c
ofe_mixin
A
)
(
ucmra_cmra_mixin
A
).
CMRAT
A
(
ucmra_ofe_mixin
A
)
(
ucmra_cmra_mixin
A
).
Canonical
Structure
ucmra_cmraR
.
(** Lifting properties from the mixin *)
...
...
@@ -687,7 +683,7 @@ Proof. split. apply _. by rewrite /= !ucmra_homomorphism_unit. Qed.
(** Functors *)
Structure
rFunctor
:
=
RFunctor
{
rFunctor_car
:
c
ofeT
→
c
ofeT
→
cmraT
;
rFunctor_car
:
ofeT
→
ofeT
→
cmraT
;
rFunctor_map
{
A1
A2
B1
B2
}
:
((
A2
-
n
>
A1
)
*
(
B1
-
n
>
B2
))
→
rFunctor_car
A1
B1
-
n
>
rFunctor_car
A2
B2
;
rFunctor_ne
A1
A2
B1
B2
n
:
...
...
@@ -705,7 +701,7 @@ Instance: Params (@rFunctor_map) 5.
Class
rFunctorContractive
(
F
:
rFunctor
)
:
=
rFunctor_contractive
A1
A2
B1
B2
:
>
Contractive
(@
rFunctor_map
F
A1
A2
B1
B2
).
Definition
rFunctor_diag
(
F
:
rFunctor
)
(
A
:
c
ofeT
)
:
cmraT
:
=
rFunctor_car
F
A
A
.
Definition
rFunctor_diag
(
F
:
rFunctor
)
(
A
:
ofeT
)
:
cmraT
:
=
rFunctor_car
F
A
A
.
Coercion
rFunctor_diag
:
rFunctor
>->
Funclass
.
Program
Definition
constRF
(
B
:
cmraT
)
:
rFunctor
:
=
...
...
@@ -716,7 +712,7 @@ Instance constRF_contractive B : rFunctorContractive (constRF B).
Proof
.
rewrite
/
rFunctorContractive
;
apply
_
.
Qed
.
Structure
urFunctor
:
=
URFunctor
{
urFunctor_car
:
c
ofeT
→
c
ofeT
→
ucmraT
;
urFunctor_car
:
ofeT
→
ofeT
→
ucmraT
;
urFunctor_map
{
A1
A2
B1
B2
}
:
((
A2
-
n
>
A1
)
*
(
B1
-
n
>
B2
))
→
urFunctor_car
A1
B1
-
n
>
urFunctor_car
A2
B2
;
urFunctor_ne
A1
A2
B1
B2
n
:
...
...
@@ -734,7 +730,7 @@ Instance: Params (@urFunctor_map) 5.
Class
urFunctorContractive
(
F
:
urFunctor
)
:
=
urFunctor_contractive
A1
A2
B1
B2
:
>
Contractive
(@
urFunctor_map
F
A1
A2
B1
B2
).
Definition
urFunctor_diag
(
F
:
urFunctor
)
(
A
:
c
ofeT
)
:
ucmraT
:
=
urFunctor_car
F
A
A
.
Definition
urFunctor_diag
(
F
:
urFunctor
)
(
A
:
ofeT
)
:
ucmraT
:
=
urFunctor_car
F
A
A
.
Coercion
urFunctor_diag
:
urFunctor
>->
Funclass
.
Program
Definition
constURF
(
B
:
ucmraT
)
:
urFunctor
:
=
...
...
@@ -790,7 +786,7 @@ Record RAMixin A `{Equiv A, PCore A, Op A, Valid A} := {
Section
discrete
.
Context
`
{
Equiv
A
,
PCore
A
,
Op
A
,
Valid
A
,
@
Equivalence
A
(
≡
)}.
Context
(
ra_mix
:
RAMixin
A
).
Existing
Instances
discrete_dist
discrete_compl
.
Existing
Instances
discrete_dist
.
Instance
discrete_validN
:
ValidN
A
:
=
λ
n
x
,
✓
x
.
Definition
discrete_cmra_mixin
:
CMRAMixin
A
.
...
...
@@ -802,9 +798,9 @@ Section discrete.
End
discrete
.
Notation
discreteR
A
ra_mix
:
=
(
CMRAT
A
discrete_
c
ofe_mixin
(
discrete_cmra_mixin
ra_mix
)).
(
CMRAT
A
discrete_ofe_mixin
(
discrete_cmra_mixin
ra_mix
)).
Notation
discreteUR
A
ra_mix
ucmra_mix
:
=
(
UCMRAT
A
discrete_
c
ofe_mixin
(
discrete_cmra_mixin
ra_mix
)
ucmra_mix
).
(
UCMRAT
A
discrete_ofe_mixin
(
discrete_cmra_mixin
ra_mix
)
ucmra_mix
).
Global
Instance
discrete_cmra_discrete
`
{
Equiv
A
,
PCore
A
,
Op
A
,
Valid
A
,
@
Equivalence
A
(
≡
)}
(
ra_mix
:
RAMixin
A
)
:
CMRADiscrete
(
discreteR
A
ra_mix
).
...
...
@@ -843,13 +839,13 @@ Section unit.
Instance
unit_op
:
Op
()
:
=
λ
x
y
,
().
Lemma
unit_cmra_mixin
:
CMRAMixin
().
Proof
.
apply
discrete_cmra_mixin
,
ra_total_mixin
;
by
eauto
.
Qed
.
Canonical
Structure
unitR
:
cmraT
:
=
CMRAT
()
unit_
c
ofe_mixin
unit_cmra_mixin
.
Canonical
Structure
unitR
:
cmraT
:
=
CMRAT
()
unit_ofe_mixin
unit_cmra_mixin
.
Instance
unit_empty
:
Empty
()
:
=
().
Lemma
unit_ucmra_mixin
:
UCMRAMixin
().
Proof
.
done
.
Qed
.
Canonical
Structure
unitUR
:
ucmraT
:
=
UCMRAT
()
unit_
c
ofe_mixin
unit_cmra_mixin
unit_ucmra_mixin
.
UCMRAT
()
unit_ofe_mixin
unit_cmra_mixin
unit_ucmra_mixin
.
Global
Instance
unit_cmra_discrete
:
CMRADiscrete
unitR
.
Proof
.
done
.
Qed
.
...
...
@@ -993,7 +989,7 @@ Section prod.
by
exists
(
z11
,
z21
),
(
z12
,
z22
).
Qed
.
Canonical
Structure
prodR
:
=
CMRAT
(
A
*
B
)
prod_
c
ofe_mixin
prod_cmra_mixin
.
CMRAT
(
A
*
B
)
prod_ofe_mixin
prod_cmra_mixin
.
Lemma
pair_op
(
a
a'
:
A
)
(
b
b'
:
B
)
:
(
a
,
b
)
⋅
(
a'
,
b'
)
=
(
a
⋅
a'
,
b
⋅
b'
).
Proof
.
done
.
Qed
.
...
...
@@ -1032,7 +1028,7 @@ Section prod_unit.
-
rewrite
prod_pcore_Some'
;
split
;
apply
(
persistent
_
).
Qed
.
Canonical
Structure
prodUR
:
=
UCMRAT
(
A
*
B
)
prod_
c
ofe_mixin
prod_cmra_mixin
prod_ucmra_mixin
.
UCMRAT
(
A
*
B
)
prod_ofe_mixin
prod_cmra_mixin
prod_ucmra_mixin
.
Lemma
pair_split
(
x
:
A
)
(
y
:
B
)
:
(
x
,
y
)
≡
(
x
,
∅
)
⋅
(
∅
,
y
).
Proof
.
by
rewrite
pair_op
left_id
right_id
.
Qed
.
...
...
@@ -1166,7 +1162,7 @@ Section option.
+
exists
None
,
None
;
repeat
constructor
.
Qed
.
Canonical
Structure
optionR
:
=
CMRAT
(
option
A
)
option_
c
ofe_mixin
option_cmra_mixin
.
CMRAT
(
option
A
)
option_ofe_mixin
option_cmra_mixin
.
Global
Instance
option_cmra_discrete
:
CMRADiscrete
A
→
CMRADiscrete
optionR
.
Proof
.
split
;
[
apply
_
|].
by
intros
[
x
|]
;
[
apply
(
cmra_discrete_valid
x
)|].
Qed
.
...
...
@@ -1175,7 +1171,7 @@ Section option.
Lemma
option_ucmra_mixin
:
UCMRAMixin
optionR
.
Proof
.
split
.
done
.
by
intros
[].
done
.
Qed
.
Canonical
Structure
optionUR
:
=
UCMRAT
(
option
A
)
option_
c
ofe_mixin
option_cmra_mixin
option_ucmra_mixin
.
UCMRAT
(
option
A
)
option_ofe_mixin
option_cmra_mixin
option_ucmra_mixin
.
(** Misc *)
Global
Instance
Some_cmra_monotone
:
CMRAMonotone
Some
.
...
...
algebra/cofe_solver.v
View file @
75518c9a
From
iris
.
algebra
Require
Export
c
ofe
.
From
iris
.
algebra
Require
Export
ofe
.
Record
solution
(
F
:
cFunctor
)
:
=
Solution
{
solution_car
:
>
cofeT
;
solution_car
:
>
ofeT
;
solution_cofe
:
Cofe
solution_car
;
solution_unfold
:
solution_car
-
n
>
F
solution_car
;
solution_fold
:
F
solution_car
-
n
>
solution_car
;
solution_fold_unfold
X
:
solution_fold
(
solution_unfold
X
)
≡
X
;
...
...
@@ -9,14 +10,17 @@ Record solution (F : cFunctor) := Solution {
}.
Arguments
solution_unfold
{
_
}
_
.
Arguments
solution_fold
{
_
}
_
.
Existing
Instance
solution_cofe
.
Module
solver
.
Section
solver
.
Context
(
F
:
cFunctor
)
`
{
Fcontr
:
cFunctorContractive
F
}
`
{
Finh
ab
:
Inhabited
(
F
unitC
)}.
`
{
Fcofe
:
∀
T
:
ofeT
,
Cofe
T
→
Cofe
(
F
T
)}
`
{
Finh
:
Inhabited
(
F
unitC
)}.
Notation
map
:
=
(
cFunctor_map
F
).
Fixpoint
A
(
k
:
nat
)
:
c
ofeT
:
=
Fixpoint
A
(
k
:
nat
)
:
ofeT
:
=
match
k
with
0
=>
unitC
|
S
k
=>
F
(
A
k
)
end
.
Local
Instance
:
∀
k
,
Cofe
(
A
k
).
Proof
.
induction
0
;
apply
_
.
Defined
.
Fixpoint
f
(
k
:
nat
)
:
A
k
-
n
>
A
(
S
k
)
:
=
match
k
with
0
=>
CofeMor
(
λ
_
,
inhabitant
)
|
S
k
=>
map
(
g
k
,
f
k
)
end
with
g
(
k
:
nat
)
:
A
(
S
k
)
-
n
>
A
k
:
=
...
...
@@ -47,17 +51,7 @@ Record tower := {
}.
Instance
tower_equiv
:
Equiv
tower
:
=
λ
X
Y
,
∀
k
,
X
k
≡
Y
k
.
Instance
tower_dist
:
Dist
tower
:
=
λ
n
X
Y
,
∀
k
,
X
k
≡
{
n
}
≡
Y
k
.
Program
Definition
tower_chain
(
c
:
chain
tower
)
(
k
:
nat
)
:
chain
(
A
k
)
:
=
{|
chain_car
i
:
=
c
i
k
|}.
Next
Obligation
.
intros
c
k
n
i
?
;
apply
(
chain_cauchy
c
n
)
;
lia
.
Qed
.
Program
Instance
tower_compl
:
Compl
tower
:
=
λ
c
,
{|
tower_car
n
:
=
compl
(
tower_chain
c
n
)
|}.
Next
Obligation
.
intros
c
k
;
apply
equiv_dist
=>
n
.
by
rewrite
(
conv_compl
n
(
tower_chain
c
k
))
(
conv_compl
n
(
tower_chain
c
(
S
k
)))
/=
(
g_tower
(
c
_
)
k
).
Qed
.
Definition
tower_cofe_mixin
:
CofeMixin
tower
.
Definition
tower_ofe_mixin
:
OfeMixin
tower
.
Proof
.
split
.
-
intros
X
Y
;
split
;
[
by
intros
HXY
n
k
;
apply
equiv_dist
|].
...
...
@@ -68,10 +62,24 @@ Proof.
+
by
intros
X
Y
Z
??
n
;
trans
(
Y
n
).
-
intros
k
X
Y
HXY
n
;
apply
dist_S
.
by
rewrite
-(
g_tower
X
)
(
HXY
(
S
n
))
g_tower
.
-
intros
n
c
k
;
rewrite
/=
(
conv_compl
n
(
tower_chain
c
k
)).
apply
(
chain_cauchy
c
)
;
lia
.
Qed
.
Definition
T
:
cofeT
:
=
CofeT
tower
tower_cofe_mixin
.
Definition
T
:
ofeT
:
=
OfeT
tower
tower_ofe_mixin
.
Program
Definition
tower_chain
(
c
:
chain
T
)
(
k
:
nat
)
:
chain
(
A
k
)
:
=
{|
chain_car
i
:
=
c
i
k
|}.
Next
Obligation
.
intros
c
k
n
i
?
;
apply
(
chain_cauchy
c
n
)
;
lia
.
Qed
.
Program
Definition
tower_compl
:
Compl
T
:
=
λ
c
,
{|
tower_car
n
:
=
compl
(
tower_chain
c
n
)
|}.
Next
Obligation
.
intros
c
k
;
apply
equiv_dist
=>
n
.
by
rewrite
(
conv_compl
n
(
tower_chain
c
k
))
(
conv_compl
n
(
tower_chain
c
(
S
k
)))
/=
(
g_tower
(
c
_
)
k
).
Qed
.
Global
Program
Instance
tower_cofe
:
Cofe
T
:
=
{
compl
:
=
tower_compl
}.
Next
Obligation
.
intros
n
c
k
;
rewrite
/=
(
conv_compl
n
(
tower_chain
c
k
)).
apply
(
chain_cauchy
c
)
;
lia
.
Qed
.
Fixpoint
ff
{
k
}
(
i
:
nat
)
:
A
k
-
n
>
A
(
i
+
k
)
:
=
match
i
with
0
=>
cid
|
S
i
=>
f
(
i
+
k
)
◎
ff
i
end
.
...
...
@@ -197,7 +205,7 @@ Proof. by intros n X Y HXY k; rewrite /fold /= HXY. Qed.
Theorem
result
:
solution
F
.
Proof
.
apply
(
Solution
F
T
(
CofeMor
unfold
)
(
CofeMor
fold
)).
apply
(
Solution
F
T
_
(
CofeMor
unfold
)
(
CofeMor
fold
)).
-
move
=>
X
/=.
rewrite
equiv_dist
=>
n
k
;
rewrite
/
unfold
/
fold
/=.
rewrite
-
g_tower
-(
gg_tower
_
n
)
;
apply
(
_
:
Proper
(
_
==>
_
)
(
g
_
)).
trans
(
map
(
ff
n
,
gg
n
)
(
X
(
S
(
n
+
k
)))).
...
...
algebra/csum.v
View file @
75518c9a
...
...
@@ -22,7 +22,7 @@ Instance maybe_Cinr {A B} : Maybe (@Cinr A B) := λ x,
match
x
with
Cinr
b
=>
Some
b
|
_
=>
None
end
.
Section
cofe
.
Context
{
A
B
:
c
ofeT
}.
Context
{
A
B
:
ofeT
}.
Implicit
Types
a
:
A
.
Implicit
Types
b
:
B
.
...
...
@@ -55,19 +55,7 @@ Proof. by inversion_clear 1. Qed.
Global
Instance
Cinr_inj_dist
n
:
Inj
(
dist
n
)
(
dist
n
)
(@
Cinr
A
B
).
Proof
.
by
inversion_clear
1
.
Qed
.
Program
Definition
csum_chain_l
(
c
:
chain
(
csum
A
B
))
(
a
:
A
)
:
chain
A
:
=
{|
chain_car
n
:
=
match
c
n
return
_
with
Cinl
a'
=>
a'
|
_
=>
a
end
|}.
Next
Obligation
.
intros
c
a
n
i
?
;
simpl
.
by
destruct
(
chain_cauchy
c
n
i
).
Qed
.
Program
Definition
csum_chain_r
(
c
:
chain
(
csum
A
B
))
(
b
:
B
)
:
chain
B
:
=
{|
chain_car
n
:
=
match
c
n
return
_
with
Cinr
b'
=>
b'
|
_
=>
b
end
|}.
Next
Obligation
.
intros
c
b
n
i
?
;
simpl
.
by
destruct
(
chain_cauchy
c
n
i
).
Qed
.
Instance
csum_compl
:
Compl
(
csum
A
B
)
:
=
λ
c
,
match
c
0
with
|
Cinl
a
=>
Cinl
(
compl
(
csum_chain_l
c
a
))
|
Cinr
b
=>
Cinr
(
compl
(
csum_chain_r
c
b
))
|
CsumBot
=>
CsumBot
end
.
Definition
csum_cofe_mixin
:
CofeMixin
(
csum
A
B
).
Definition
csum_ofe_mixin
:
OfeMixin
(
csum
A
B
).
Proof
.
split
.
-
intros
mx
my
;
split
.
...
...
@@ -79,12 +67,30 @@ Proof.
+
by
destruct
1
;
constructor
.
+
destruct
1
;
inversion_clear
1
;
constructor
;
etrans
;
eauto
.
-
by
inversion_clear
1
;
constructor
;
apply
dist_S
.
-
intros
n
c
;
rewrite
/
compl
/
csum_compl
.
feed
inversion
(
chain_cauchy
c
0
n
)
;
first
auto
with
lia
;
constructor
.
+
rewrite
(
conv_compl
n
(
csum_chain_l
c
a'
))
/=.
destruct
(
c
n
)
;
naive_solver
.
+
rewrite
(
conv_compl
n
(
csum_chain_r
c
b'
))
/=.
destruct
(
c
n
)
;
naive_solver
.
Qed
.
Canonical
Structure
csumC
:
cofeT
:
=
CofeT
(
csum
A
B
)
csum_cofe_mixin
.
Canonical
Structure
csumC
:
ofeT
:
=
OfeT
(
csum
A
B
)
csum_ofe_mixin
.
Program
Definition
csum_chain_l
(
c
:
chain
csumC
)
(
a
:
A
)
:
chain
A
:
=
{|
chain_car
n
:
=
match
c
n
return
_
with
Cinl
a'
=>
a'
|
_
=>
a
end
|}.
Next
Obligation
.
intros
c
a
n
i
?
;
simpl
.
by
destruct
(
chain_cauchy
c
n
i
).
Qed
.
Program
Definition
csum_chain_r
(
c
:
chain
csumC
)
(
b
:
B
)
:
chain
B
:
=
{|
chain_car
n
:
=
match
c
n
return
_
with
Cinr
b'
=>
b'
|
_
=>
b
end
|}.
Next
Obligation
.
intros
c
b
n
i
?
;
simpl
.
by
destruct
(
chain_cauchy
c
n
i
).
Qed
.
Definition
csum_compl
`
{
Cofe
A
,
Cofe
B
}
:
Compl
csumC
:
=
λ
c
,
match
c
0
with
|
Cinl
a
=>
Cinl
(
compl
(
csum_chain_l
c
a
))
|
Cinr
b
=>
Cinr
(
compl
(
csum_chain_r
c
b
))
|
CsumBot
=>
CsumBot
end
.
Global
Program
Instance
csum_cofe
`
{
Cofe
A
,
Cofe
B
}
:
Cofe
csumC
:
=
{|
compl
:
=
csum_compl
|}.
Next
Obligation
.
intros
??
n
c
;
rewrite
/
compl
/
csum_compl
.
feed
inversion
(
chain_cauchy
c
0
n
)
;
first
auto
with
lia
;
constructor
.
+
rewrite
(
conv_compl
n
(
csum_chain_l
c
a'
))
/=.
destruct
(
c
n
)
;
naive_solver
.
+
rewrite
(
conv_compl
n
(
csum_chain_r
c
b'
))
/=.
destruct
(
c
n
)
;
naive_solver
.
Qed
.
Global
Instance
csum_discrete
:
Discrete
A
→
Discrete
B
→
Discrete
csumC
.
Proof
.
by
inversion_clear
3
;
constructor
;
apply
(
timeless
_
).
Qed
.
Global
Instance
csum_leibniz
:
...
...
@@ -115,10 +121,10 @@ Lemma csum_map_compose {A A' A'' B B' B''} (f : A → A') (f' : A' → A'')
(
g
:
B
→
B'
)
(
g'
:
B'
→
B''
)
(
x
:
csum
A
B
)
:
csum_map
(
f'
∘
f
)
(
g'
∘
g
)
x
=
csum_map
f'
g'
(
csum_map
f
g
x
).
Proof
.
by
destruct
x
.
Qed
.
Lemma
csum_map_ext
{
A
A'
B
B'
:
c
ofeT
}
(
f
f'
:
A
→
A'
)
(
g
g'
:
B
→
B'
)
x
:
Lemma
csum_map_ext
{
A
A'
B
B'
:
ofeT
}
(
f
f'
:
A
→
A'
)
(
g
g'
:
B
→
B'
)
x
:
(
∀
x
,
f
x
≡
f'
x
)
→
(
∀
x
,
g
x
≡
g'
x
)
→
csum_map
f
g
x
≡
csum_map
f'
g'
x
.
Proof
.
by
destruct
x
;
constructor
.
Qed
.
Instance
csum_map_cmra_ne
{
A
A'
B
B'
:
c
ofeT
}
n
:
Instance
csum_map_cmra_ne
{
A
A'
B
B'
:
ofeT
}
n
:
Proper
((
dist
n
==>
dist
n
)
==>
(
dist
n
==>
dist
n
)
==>
dist
n
==>
dist
n
)
(@
csum_map
A
A'
B
B'
).
Proof
.
intros
f
f'
Hf
g
g'
Hg
[]
;
destruct
1
;
constructor
;
by
apply
Hf
||
apply
Hg
.
Qed
.
...
...
@@ -224,7 +230,7 @@ Proof.
+
by
exists
CsumBot
,
CsumBot
;
destruct
y1
,
y2
;
inversion_clear
Hx'
.
Qed
.
Canonical
Structure
csumR
:
=
CMRAT
(
csum
A
B
)
csum_
c
ofe_mixin
csum_cmra_mixin
.
CMRAT
(
csum
A
B
)
csum_ofe_mixin
csum_cmra_mixin
.
Global
Instance
csum_cmra_discrete
:
CMRADiscrete
A
→
CMRADiscrete
B
→
CMRADiscrete
csumR
.
...
...
algebra/dec_agree.v
View file @
75518c9a
...
...
@@ -20,7 +20,7 @@ Implicit Types x y : dec_agree A.
Instance
dec_agree_valid
:
Valid
(
dec_agree
A
)
:
=
λ
x
,
if
x
is
DecAgree
_
then
True
else
False
.
Canonical
Structure
dec_agreeC
:
c
ofeT
:
=
leibnizC
(
dec_agree
A
).
Canonical
Structure
dec_agreeC
:
ofeT
:
=
leibnizC
(
dec_agree
A
).
Instance
dec_agree_op
:
Op
(
dec_agree
A
)
:
=
λ
x
y
,
match
x
,
y
with
...
...
algebra/dra.v
View file @
75518c9a
...
...
@@ -114,7 +114,7 @@ Proof.
-
intros
[
x
px
?]
[
y
py
?]
[
z
pz
?]
[?
Hxy
]
[?
Hyz
]
;
simpl
in
*.
split
;
[|
intros
;
trans
y
]
;
tauto
.
Qed
.
Canonical
Structure
validityC
:
c
ofeT
:
=
discreteC
(
validity
A
).
Canonical
Structure
validityC
:
ofeT
:
=
discreteC
(
validity
A
).
Instance
dra_valid_proper'
:
Proper
((
≡
)
==>
iff
)
(
valid
:
A
→
Prop
).
Proof
.
by
split
;
apply
:
dra_valid_proper
.
Qed
.
...
...
algebra/excl.v