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
Dan Frumin
iris-coq
Commits
448a8b62
Commit
448a8b62
authored
Mar 01, 2016
by
Robbert Krebbers
Browse files
Use "R"-suffixes for CMRA instances.
parent
cca77f9f
Changes
19
Hide whitespace changes
Inline
Side-by-side
algebra/agree.v
View file @
448a8b62
...
...
@@ -119,7 +119,7 @@ Proof.
+
by
rewrite
agree_idemp
.
+
by
move
:
Hval
;
rewrite
Hx
;
move
=>
/
agree_op_inv
->
;
rewrite
agree_idemp
.
Qed
.
Canonical
Structure
agreeR
A
:
cmraT
:=
CMRAT
agree_cofe_mixin
agree_cmra_mixin
.
Canonical
Structure
agreeR
:
cmraT
:=
CMRAT
agree_cofe_mixin
agree_cmra_mixin
.
Program
Definition
to_agree
(
x
:
A
)
:
agree
A
:=
{|
agree_car
n
:=
x
;
agree_is_valid
n
:=
True
|}
.
...
...
@@ -142,7 +142,7 @@ Proof. uPred.unseal; split=> r n _ ?; by apply: agree_op_inv. Qed.
End
agree
.
Arguments
agreeC
:
clear
implicits
.
Arguments
agreeR
A
:
clear
implicits
.
Arguments
agreeR
:
clear
implicits
.
Program
Definition
agree_map
{
A
B
}
(
f
:
A
→
B
)
(
x
:
agree
A
)
:
agree
B
:=
{|
agree_car
n
:=
f
(
x
n
);
agree_is_valid
:=
agree_is_valid
x
|}
.
...
...
@@ -181,5 +181,5 @@ Proof.
Qed
.
Program
Definition
agreeF
:
iFunctor
:=
{|
ifunctor_car
:=
agreeR
A
;
ifunctor_map
:=
@
agreeC_map
|}
.
{|
ifunctor_car
:=
agreeR
;
ifunctor_map
:=
@
agreeC_map
|}
.
Solve
Obligations
with
done
.
algebra/auth.v
View file @
448a8b62
...
...
@@ -134,8 +134,8 @@ Proof.
as
(
b
&?&?&?
);
auto
using
own_validN
.
by
exists
(
Auth
(
ea
.1
)
(
b
.1
),
Auth
(
ea
.2
)
(
b
.2
)).
Qed
.
Canonical
Structure
authR
A
:
cmraT
:=
CMRAT
auth_cofe_mixin
auth_cmra_mixin
.
Global
Instance
auth_cmra_discrete
:
CMRADiscrete
A
→
CMRADiscrete
authR
A
.
Canonical
Structure
authR
:
cmraT
:=
CMRAT
auth_cofe_mixin
auth_cmra_mixin
.
Global
Instance
auth_cmra_discrete
:
CMRADiscrete
A
→
CMRADiscrete
authR
.
Proof
.
split
;
first
apply
_.
intros
[[]
?
];
by
rewrite
/=
/
cmra_valid
/
cmra_validN
/=
...
...
@@ -158,7 +158,7 @@ Proof. uPred.unseal. by destruct x as [[]]. Qed.
what
follows
,
we
assume
we
have
an
empty
element
.
*
)
Context
`
{
Empty
A
,
!
CMRAIdentity
A
}
.
Global
Instance
auth_cmra_identity
:
CMRAIdentity
authR
A
.
Global
Instance
auth_cmra_identity
:
CMRAIdentity
authR
.
Proof
.
split
;
simpl
.
-
by
apply
(
@
cmra_empty_valid
A
_
).
...
...
@@ -208,7 +208,7 @@ Proof.
Qed
.
End
cmra
.
Arguments
authR
A
:
clear
implicits
.
Arguments
authR
:
clear
implicits
.
(
*
Functor
*
)
Definition
auth_map
{
A
B
}
(
f
:
A
→
B
)
(
x
:
auth
A
)
:
auth
B
:=
...
...
@@ -241,7 +241,7 @@ Lemma authC_map_ne A B n : Proper (dist n ==> dist n) (@authC_map A B).
Proof
.
intros
f
f
'
Hf
[[
a
|
|
]
b
];
repeat
constructor
;
apply
Hf
.
Qed
.
Program
Definition
authF
(
Σ
:
iFunctor
)
:
iFunctor
:=
{|
ifunctor_car
:=
authR
A
∘
Σ
;
ifunctor_map
A
B
:=
authC_map
∘
ifunctor_map
Σ
ifunctor_car
:=
authR
∘
Σ
;
ifunctor_map
A
B
:=
authC_map
∘
ifunctor_map
Σ
|}
.
Next
Obligation
.
by
intros
Σ
A
B
n
f
g
Hfg
;
apply
authC_map_ne
,
ifunctor_map_ne
.
...
...
algebra/cmra.v
View file @
448a8b62
...
...
@@ -515,8 +515,8 @@ Section discrete.
-
intros
n
x
y1
y2
??
;
exists
(
y1
,
y2
);
split_and
?
;
auto
.
apply
(
timeless
_
),
dist_le
with
n
;
auto
with
lia
.
Qed
.
Definition
discreteR
A
:
cmraT
:=
CMRAT
(
cofe_mixin
A
)
discrete_cmra_mixin
.
Global
Instance
discrete_cmra_discrete
:
CMRADiscrete
discreteR
A
.
Definition
discreteR
:
cmraT
:=
CMRAT
(
cofe_mixin
A
)
discrete_cmra_mixin
.
Global
Instance
discrete_cmra_discrete
:
CMRADiscrete
discreteR
.
Proof
.
split
.
change
(
Discrete
A
);
apply
_.
by
intros
x
?
.
Qed
.
End
discrete
.
...
...
@@ -529,10 +529,10 @@ Section unit.
Global
Instance
unit_empty
:
Empty
()
:=
().
Definition
unit_ra
:
RA
().
Proof
.
by
split
.
Qed
.
Canonical
Structure
unitR
A
:
cmraT
:=
Eval
cbv
[
unitC
discreteR
A
cofe_car
]
in
discreteR
A
unit_ra
.
Global
Instance
unit_cmra_identity
:
CMRAIdentity
unitR
A
.
Global
Instance
unit_cmra_discrete
:
CMRADiscrete
unitR
A
.
Canonical
Structure
unitR
:
cmraT
:=
Eval
cbv
[
unitC
discreteR
cofe_car
]
in
discreteR
unit_ra
.
Global
Instance
unit_cmra_identity
:
CMRAIdentity
unitR
.
Global
Instance
unit_cmra_discrete
:
CMRADiscrete
unitR
.
Proof
.
by
apply
discrete_cmra_discrete
.
Qed
.
End
unit
.
...
...
@@ -581,9 +581,9 @@ Section prod.
destruct
(
cmra_extend
n
(
x
.2
)
(
y1
.2
)
(
y2
.2
))
as
(
z2
&?&?&?
);
auto
.
by
exists
((
z1
.1
,
z2
.1
),(
z1
.2
,
z2
.2
)).
Qed
.
Canonical
Structure
prodR
A
:
cmraT
:=
CMRAT
prod_cofe_mixin
prod_cmra_mixin
.
Canonical
Structure
prodR
:
cmraT
:=
CMRAT
prod_cofe_mixin
prod_cmra_mixin
.
Global
Instance
prod_cmra_identity
`
{
Empty
A
,
Empty
B
}
:
CMRAIdentity
A
→
CMRAIdentity
B
→
CMRAIdentity
prodR
A
.
CMRAIdentity
A
→
CMRAIdentity
B
→
CMRAIdentity
prodR
.
Proof
.
split
.
-
split
;
apply
cmra_empty_valid
.
...
...
@@ -591,7 +591,7 @@ Section prod.
-
by
intros
?
[
??
];
split
;
apply
(
timeless
_
).
Qed
.
Global
Instance
prod_cmra_discrete
:
CMRADiscrete
A
→
CMRADiscrete
B
→
CMRADiscrete
prodR
A
.
CMRADiscrete
A
→
CMRADiscrete
B
→
CMRADiscrete
prodR
.
Proof
.
split
.
apply
_.
by
intros
?
[];
split
;
apply
cmra_discrete_valid
.
Qed
.
Lemma
prod_update
x
y
:
x
.1
~~>
y
.1
→
x
.2
~~>
y
.2
→
x
~~>
y
.
...
...
@@ -607,7 +607,7 @@ Section prod.
x
.1
~~>:
P1
→
x
.2
~~>:
P2
→
x
~~>:
λ
y
,
P1
(
y
.1
)
∧
P2
(
y
.2
).
Proof
.
eauto
using
prod_updateP
.
Qed
.
End
prod
.
Arguments
prodR
A
:
clear
implicits
.
Arguments
prodR
:
clear
implicits
.
Instance
prod_map_cmra_monotone
{
A
A
'
B
B
'
:
cmraT
}
(
f
:
A
→
A
'
)
(
g
:
B
→
B
'
)
:
CMRAMonotone
f
→
CMRAMonotone
g
→
CMRAMonotone
(
prod_map
f
g
).
...
...
algebra/dec_agree.v
View file @
448a8b62
...
...
@@ -46,7 +46,7 @@ Proof.
intros
;
by
repeat
(
simplify_eq
/=
||
case_match
).
Qed
.
Canonical
Structure
dec_agreeR
A
:
cmraT
:=
discreteR
A
dec_agree_ra
.
Canonical
Structure
dec_agreeR
:
cmraT
:=
discreteR
dec_agree_ra
.
(
*
Some
properties
of
this
CMRA
*
)
Lemma
dec_agree_ne
a
b
:
a
≠
b
→
DecAgree
a
⋅
DecAgree
b
=
DecAgreeBot
.
...
...
@@ -59,4 +59,4 @@ Lemma dec_agree_op_inv (x1 x2 : dec_agree A) : ✓ (x1 ⋅ x2) → x1 = x2.
Proof
.
destruct
x1
,
x2
;
by
repeat
(
simplify_eq
/=
||
case_match
).
Qed
.
End
dec_agree
.
Arguments
dec_agreeR
A
_
{
_
}
.
Arguments
dec_agreeR
_
{
_
}
.
algebra/dra.v
View file @
448a8b62
...
...
@@ -130,11 +130,11 @@ Proof.
-
intros
[
x
px
?
]
[
y
py
?
]
[[
z
pz
?
]
[
??
]];
split
;
simpl
in
*
;
intuition
eauto
10
using
dra_disjoint_div
,
dra_op_div
.
Qed
.
Definition
validityR
A
:
cmraT
:=
discreteR
A
validity_ra
.
Definition
validityR
:
cmraT
:=
discreteR
validity_ra
.
Instance
validity_cmra_discrete
:
CMRADiscrete
validityR
A
:=
discrete_cmra_discrete
_.
CMRADiscrete
validityR
:=
discrete_cmra_discrete
_.
Lemma
validity_update
(
x
y
:
validityR
A
)
:
Lemma
validity_update
(
x
y
:
validityR
)
:
(
∀
z
,
✓
x
→
✓
z
→
validity_car
x
⊥
z
→
✓
y
∧
validity_car
y
⊥
z
)
→
x
~~>
y
.
Proof
.
intros
Hxy
;
apply
cmra_discrete_update
=>
z
[
?
[
??
]].
...
...
algebra/excl.v
View file @
448a8b62
...
...
@@ -127,10 +127,10 @@ Proof.
|
ExclUnit
,
_
=>
(
ExclUnit
,
x
)
|
_
,
ExclUnit
=>
(
x
,
ExclUnit
)
end
;
destruct
y1
,
y2
;
inversion_clear
Hx
;
repeat
constructor
.
Qed
.
Canonical
Structure
exclR
A
:
cmraT
:=
CMRAT
excl_cofe_mixin
excl_cmra_mixin
.
Global
Instance
excl_cmra_identity
:
CMRAIdentity
exclR
A
.
Canonical
Structure
exclR
:
cmraT
:=
CMRAT
excl_cofe_mixin
excl_cmra_mixin
.
Global
Instance
excl_cmra_identity
:
CMRAIdentity
exclR
.
Proof
.
split
.
done
.
by
intros
[].
apply
_.
Qed
.
Global
Instance
excl_cmra_discrete
:
Discrete
A
→
CMRADiscrete
exclR
A
.
Global
Instance
excl_cmra_discrete
:
Discrete
A
→
CMRADiscrete
exclR
.
Proof
.
split
.
apply
_.
by
intros
[].
Qed
.
Lemma
excl_validN_inv_l
n
x
a
:
✓
{
n
}
(
Excl
a
⋅
x
)
→
x
=
∅
.
...
...
@@ -170,7 +170,7 @@ Proof. intros ?? n z ?; exists y. by destruct y, z as [?| |]. Qed.
End
excl
.
Arguments
exclC
:
clear
implicits
.
Arguments
exclR
A
:
clear
implicits
.
Arguments
exclR
:
clear
implicits
.
(
*
Functor
*
)
Definition
excl_map
{
A
B
}
(
f
:
A
→
B
)
(
x
:
excl
A
)
:
excl
B
:=
...
...
@@ -202,6 +202,6 @@ Instance exclC_map_ne A B n : Proper (dist n ==> dist n) (@exclC_map A B).
Proof
.
by
intros
f
f
'
Hf
[];
constructor
;
apply
Hf
.
Qed
.
Program
Definition
exclF
:
iFunctor
:=
{|
ifunctor_car
:=
exclR
A
;
ifunctor_map
:=
@
exclC_map
|}
.
{|
ifunctor_car
:=
exclR
;
ifunctor_map
:=
@
exclC_map
|}
.
Next
Obligation
.
by
intros
A
x
;
rewrite
/=
excl_map_id
.
Qed
.
Next
Obligation
.
by
intros
A
B
C
f
g
x
;
rewrite
/=
excl_map_compose
.
Qed
.
algebra/fin_maps.v
View file @
448a8b62
...
...
@@ -158,15 +158,15 @@ Proof.
pose
proof
(
Hm12
'
i
)
as
Hm12
''
;
rewrite
Hx
in
Hm12
''
.
by
symmetry
;
apply
option_op_positive_dist_r
with
(
m1
!!
i
).
Qed
.
Canonical
Structure
mapR
A
:
cmraT
:=
CMRAT
map_cofe_mixin
map_cmra_mixin
.
Global
Instance
map_cmra_identity
:
CMRAIdentity
mapR
A
.
Canonical
Structure
mapR
:
cmraT
:=
CMRAT
map_cofe_mixin
map_cmra_mixin
.
Global
Instance
map_cmra_identity
:
CMRAIdentity
mapR
.
Proof
.
split
.
-
by
intros
i
;
rewrite
lookup_empty
.
-
by
intros
m
i
;
rewrite
/=
lookup_op
lookup_empty
(
left_id_L
None
_
).
-
apply
map_empty_timeless
.
Qed
.
Global
Instance
map_cmra_discrete
:
CMRADiscrete
A
→
CMRADiscrete
mapR
A
.
Global
Instance
map_cmra_discrete
:
CMRADiscrete
A
→
CMRADiscrete
mapR
.
Proof
.
split
;
[
apply
_
|
].
intros
m
?
i
.
by
apply
:
cmra_discrete_valid
.
Qed
.
(
**
Internalized
properties
*
)
...
...
@@ -176,7 +176,7 @@ Lemma map_validI {M} m : (✓ m)%I ≡ (∀ i, ✓ (m !! i) : uPred M)%I.
Proof
.
by
uPred
.
unseal
.
Qed
.
End
cmra
.
Arguments
mapR
A
_
{
_
_
}
_.
Arguments
mapR
_
{
_
_
}
_.
Section
properties
.
Context
`
{
Countable
K
}
{
A
:
cmraT
}
.
...
...
@@ -353,7 +353,7 @@ Proof.
Qed
.
Program
Definition
mapF
K
`
{
Countable
K
}
(
Σ
:
iFunctor
)
:
iFunctor
:=
{|
ifunctor_car
:=
mapR
A
K
∘
Σ
;
ifunctor_map
A
B
:=
mapC_map
∘
ifunctor_map
Σ
ifunctor_car
:=
mapR
K
∘
Σ
;
ifunctor_map
A
B
:=
mapC_map
∘
ifunctor_map
Σ
|}
.
Next
Obligation
.
by
intros
K
??
Σ
A
B
n
f
g
Hfg
;
apply
mapC_map_ne
,
ifunctor_map_ne
.
...
...
algebra/frac.v
View file @
448a8b62
...
...
@@ -171,10 +171,10 @@ Proof.
+
exists
(
∅
,
Frac
q
a
);
inversion_clear
Hx
'
;
by
repeat
constructor
.
+
exfalso
;
inversion_clear
Hx
'
.
Qed
.
Canonical
Structure
fracR
A
:
cmraT
:=
CMRAT
frac_cofe_mixin
frac_cmra_mixin
.
Global
Instance
frac_cmra_identity
:
CMRAIdentity
fracR
A
.
Canonical
Structure
fracR
:
cmraT
:=
CMRAT
frac_cofe_mixin
frac_cmra_mixin
.
Global
Instance
frac_cmra_identity
:
CMRAIdentity
fracR
.
Proof
.
split
.
done
.
by
intros
[].
apply
_.
Qed
.
Global
Instance
frac_cmra_discrete
:
CMRADiscrete
A
→
CMRADiscrete
fracR
A
.
Global
Instance
frac_cmra_discrete
:
CMRADiscrete
A
→
CMRADiscrete
fracR
.
Proof
.
split
;
first
apply
_.
intros
[
q
a
|
];
destruct
1
;
split
;
auto
using
cmra_discrete_valid
.
...
...
@@ -229,7 +229,7 @@ Proof.
Qed
.
End
cmra
.
Arguments
fracR
A
:
clear
implicits
.
Arguments
fracR
:
clear
implicits
.
(
*
Functor
*
)
Instance
frac_map_cmra_monotone
{
A
B
:
cmraT
}
(
f
:
A
→
B
)
:
...
...
@@ -245,7 +245,7 @@ Proof.
Qed
.
Program
Definition
fracF
(
Σ
:
iFunctor
)
:
iFunctor
:=
{|
ifunctor_car
:=
fracR
A
∘
Σ
;
ifunctor_map
A
B
:=
fracC_map
∘
ifunctor_map
Σ
ifunctor_car
:=
fracR
∘
Σ
;
ifunctor_map
A
B
:=
fracC_map
∘
ifunctor_map
Σ
|}
.
Next
Obligation
.
by
intros
Σ
A
B
n
f
g
Hfg
;
apply
fracC_map_ne
,
ifunctor_map_ne
.
...
...
algebra/functor.v
View file @
448a8b62
...
...
@@ -29,7 +29,7 @@ Program Definition constF (B : cmraT) : iFunctor :=
Solve
Obligations
with
done
.
Program
Definition
prodF
(
Σ
1
Σ
2
:
iFunctor
)
:
iFunctor
:=
{|
ifunctor_car
A
:=
prodR
A
(
Σ
1
A
)
(
Σ
2
A
);
ifunctor_car
A
:=
prodR
(
Σ
1
A
)
(
Σ
2
A
);
ifunctor_map
A
B
f
:=
prodC_map
(
ifunctor_map
Σ
1
f
)
(
ifunctor_map
Σ
2
f
)
|}
.
Next
Obligation
.
...
...
algebra/iprod.v
View file @
448a8b62
...
...
@@ -159,9 +159,9 @@ Section iprod_cmra.
exists
((
λ
x
,
(
proj1_sig
(
g
x
))
.1
),
(
λ
x
,
(
proj1_sig
(
g
x
))
.2
)).
split_and
?
;
intros
x
;
apply
(
proj2_sig
(
g
x
)).
Qed
.
Canonical
Structure
iprodR
A
:
cmraT
:=
CMRAT
iprod_cofe_mixin
iprod_cmra_mixin
.
Canonical
Structure
iprodR
:
cmraT
:=
CMRAT
iprod_cofe_mixin
iprod_cmra_mixin
.
Global
Instance
iprod_cmra_identity
`
{
∀
x
,
Empty
(
B
x
)
}
:
(
∀
x
,
CMRAIdentity
(
B
x
))
→
CMRAIdentity
iprodR
A
.
(
∀
x
,
CMRAIdentity
(
B
x
))
→
CMRAIdentity
iprodR
.
Proof
.
intros
?
;
split
.
-
intros
x
;
apply
cmra_empty_valid
.
...
...
@@ -253,7 +253,7 @@ Section iprod_cmra.
Proof
.
eauto
using
iprod_singleton_updateP_empty
.
Qed
.
End
iprod_cmra
.
Arguments
iprodR
A
{
_
}
_.
Arguments
iprodR
{
_
}
_.
(
**
*
Functor
*
)
Definition
iprod_map
{
A
}
{
B1
B2
:
A
→
cofeT
}
(
f
:
∀
x
,
B1
x
→
B2
x
)
...
...
@@ -289,7 +289,7 @@ Instance iprodC_map_ne {A} {B1 B2 : A → cofeT} n :
Proof
.
intros
f1
f2
Hf
g
x
;
apply
Hf
.
Qed
.
Program
Definition
iprodF
{
A
}
(
Σ
:
A
→
iFunctor
)
:
iFunctor
:=
{|
ifunctor_car
B
:=
iprodR
A
(
λ
x
,
Σ
x
B
);
ifunctor_car
B
:=
iprodR
(
λ
x
,
Σ
x
B
);
ifunctor_map
B1
B2
f
:=
iprodC_map
(
λ
x
,
ifunctor_map
(
Σ
x
)
f
);
|}
.
Next
Obligation
.
...
...
algebra/option.v
View file @
448a8b62
...
...
@@ -118,10 +118,10 @@ Proof.
+
by
exists
(
None
,
Some
x
);
inversion
Hx
'
;
repeat
constructor
.
+
exists
(
None
,
None
);
repeat
constructor
.
Qed
.
Canonical
Structure
optionR
A
:=
CMRAT
option_cofe_mixin
option_cmra_mixin
.
Global
Instance
option_cmra_identity
:
CMRAIdentity
optionR
A
.
Canonical
Structure
optionR
:=
CMRAT
option_cofe_mixin
option_cmra_mixin
.
Global
Instance
option_cmra_identity
:
CMRAIdentity
optionR
.
Proof
.
split
.
done
.
by
intros
[].
by
inversion_clear
1.
Qed
.
Global
Instance
option_cmra_discrete
:
CMRADiscrete
A
→
CMRADiscrete
optionR
A
.
Global
Instance
option_cmra_discrete
:
CMRADiscrete
A
→
CMRADiscrete
optionR
.
Proof
.
split
;
[
apply
_
|
].
by
intros
[
x
|
];
[
apply
(
cmra_discrete_valid
x
)
|
].
Qed
.
(
**
Misc
*
)
...
...
@@ -170,7 +170,7 @@ Proof.
auto
using
cmra_empty_validN
.
Qed
.
End
cmra
.
Arguments
optionR
A
:
clear
implicits
.
Arguments
optionR
:
clear
implicits
.
(
**
Functor
*
)
Instance
option_fmap_ne
{
A
B
:
cofeT
}
(
f
:
A
→
B
)
n
:
...
...
@@ -190,7 +190,7 @@ Instance optionC_map_ne A B n : Proper (dist n ==> dist n) (@optionC_map A B).
Proof
.
by
intros
f
f
'
Hf
[];
constructor
;
apply
Hf
.
Qed
.
Program
Definition
optionF
(
Σ
:
iFunctor
)
:
iFunctor
:=
{|
ifunctor_car
:=
optionR
A
∘
Σ
;
ifunctor_map
A
B
:=
optionC_map
∘
ifunctor_map
Σ
ifunctor_car
:=
optionR
∘
Σ
;
ifunctor_map
A
B
:=
optionC_map
∘
ifunctor_map
Σ
|}
.
Next
Obligation
.
by
intros
Σ
A
B
n
f
g
Hfg
;
apply
optionC_map_ne
,
ifunctor_map_ne
.
...
...
algebra/sts.v
View file @
448a8b62
...
...
@@ -287,20 +287,20 @@ Proof.
unfold
up_set
;
rewrite
elem_of_bind
;
intros
(
?&
s1
&?&?&?
).
apply
closed_steps
with
T2
s1
;
auto
with
sts
.
Qed
.
Canonical
Structure
R
A
:
cmraT
:=
validityR
A
(
car
sts
).
Canonical
Structure
R
:
cmraT
:=
validityR
(
car
sts
).
End
sts_dra
.
End
sts_dra
.
(
**
*
The
STS
Resource
Algebra
*
)
(
**
Finally
,
the
general
theory
of
STS
that
should
be
used
by
users
*
)
Notation
stsR
A
:=
(
@
sts_dra
.
R
A
).
Notation
stsR
:=
(
@
sts_dra
.
R
).
Section
sts_definitions
.
Context
{
sts
:
stsT
}
.
Definition
sts_auth
(
s
:
sts
.
state
sts
)
(
T
:
sts
.
tokens
sts
)
:
stsR
A
sts
:=
Definition
sts_auth
(
s
:
sts
.
state
sts
)
(
T
:
sts
.
tokens
sts
)
:
stsR
sts
:=
to_validity
(
sts_dra
.
auth
s
T
).
Definition
sts_frag
(
S
:
sts
.
states
sts
)
(
T
:
sts
.
tokens
sts
)
:
stsR
A
sts
:=
Definition
sts_frag
(
S
:
sts
.
states
sts
)
(
T
:
sts
.
tokens
sts
)
:
stsR
sts
:=
to_validity
(
sts_dra
.
frag
S
T
).
Definition
sts_frag_up
(
s
:
sts
.
state
sts
)
(
T
:
sts
.
tokens
sts
)
:
stsR
A
sts
:=
Definition
sts_frag_up
(
s
:
sts
.
state
sts
)
(
T
:
sts
.
tokens
sts
)
:
stsR
sts
:=
sts_frag
(
sts
.
up
s
T
)
T
.
End
sts_definitions
.
Instance:
Params
(
@
sts_auth
)
2.
...
...
@@ -314,7 +314,7 @@ Implicit Types s : state sts.
Implicit
Types
S
:
states
sts
.
Implicit
Types
T
:
tokens
sts
.
Global
Instance
sts_cmra_discrete
:
CMRADiscrete
(
stsR
A
sts
).
Global
Instance
sts_cmra_discrete
:
CMRADiscrete
(
stsR
sts
).
Proof
.
apply
validity_cmra_discrete
.
Qed
.
(
**
Setoids
*
)
...
...
heap_lang/heap.v
View file @
448a8b62
...
...
@@ -7,18 +7,18 @@ Import uPred.
a
finmap
as
their
state
.
Or
maybe
even
beyond
"as their state"
,
i
.
e
.
arbitrary
predicates
over
finmaps
instead
of
just
ownP
.
*
)
Definition
heapR
A
:
cmraT
:=
mapR
A
loc
(
fracR
A
(
dec_agreeR
A
val
)).
Definition
heapGF
:
iFunctor
:=
authGF
heapR
A
.
Definition
heapR
:
cmraT
:=
mapR
loc
(
fracR
(
dec_agreeR
val
)).
Definition
heapGF
:
iFunctor
:=
authGF
heapR
.
Class
heapG
Σ
:=
HeapG
{
heap_inG
:
inG
heap_lang
Σ
(
authR
A
heapR
A
);
heap_inG
:
inG
heap_lang
Σ
(
authR
heapR
);
heap_name
:
gname
}
.
Instance
heap_authG
`
{
i
:
heapG
Σ
}
:
authG
heap_lang
Σ
heapR
A
:=
Instance
heap_authG
`
{
i
:
heapG
Σ
}
:
authG
heap_lang
Σ
heapR
:=
{|
auth_inG
:=
heap_inG
|}
.
Definition
to_heap
:
state
→
heapR
A
:=
fmap
(
λ
v
,
Frac
1
(
DecAgree
v
)).
Definition
of_heap
:
heapR
A
→
state
:=
Definition
to_heap
:
state
→
heapR
:=
fmap
(
λ
v
,
Frac
1
(
DecAgree
v
)).
Definition
of_heap
:
heapR
→
state
:=
omap
(
mbind
(
maybe
DecAgree
∘
snd
)
∘
maybe2
Frac
).
(
*
heap_mapsto
is
defined
strongly
opaquely
,
to
prevent
unification
from
...
...
@@ -28,7 +28,7 @@ Definition heap_mapsto `{heapG Σ}
auth_own
heap_name
{
[
l
:=
Frac
q
(
DecAgree
v
)
]
}
.
Typeclasses
Opaque
heap_mapsto
.
Definition
heap_inv
`
{
i
:
heapG
Σ
}
(
h
:
heapR
A
)
:
iPropG
heap_lang
Σ
:=
Definition
heap_inv
`
{
i
:
heapG
Σ
}
(
h
:
heapR
)
:
iPropG
heap_lang
Σ
:=
ownP
(
of_heap
h
).
Definition
heap_ctx
`
{
i
:
heapG
Σ
}
(
N
:
namespace
)
:
iPropG
heap_lang
Σ
:=
auth_ctx
heap_name
N
heap_inv
.
...
...
@@ -43,7 +43,7 @@ Section heap.
Implicit
Types
P
Q
:
iPropG
heap_lang
Σ
.
Implicit
Types
Φ
:
val
→
iPropG
heap_lang
Σ
.
Implicit
Types
σ
:
state
.
Implicit
Types
h
g
:
heapR
A
.
Implicit
Types
h
g
:
heapR
.
(
**
Conversion
to
heaps
and
back
*
)
Global
Instance
of_heap_proper
:
Proper
((
≡
)
==>
(
=
))
of_heap
.
...
...
@@ -91,7 +91,7 @@ Section heap.
(
**
Allocation
*
)
Lemma
heap_alloc
E
N
σ
:
authG
heap_lang
Σ
heapR
A
→
nclose
N
⊆
E
→
authG
heap_lang
Σ
heapR
→
nclose
N
⊆
E
→
ownP
σ
⊑
(
|={
E
}=>
∃
_
:
heapG
Σ
,
heap_ctx
N
∧
Π★
{
map
σ
}
(
λ
l
v
,
l
↦
v
)).
Proof
.
intros
.
rewrite
-{
1
}
(
from_to_heap
σ
).
etrans
.
...
...
program_logic/auth.v
View file @
448a8b62
...
...
@@ -3,12 +3,12 @@ From program_logic Require Export invariants global_functor.
Import
uPred
.
Class
authG
Λ
Σ
(
A
:
cmraT
)
`
{
Empty
A
}
:=
AuthG
{
auth_inG
:>
inG
Λ
Σ
(
authR
A
A
);
auth_inG
:>
inG
Λ
Σ
(
authR
A
);
auth_identity
:>
CMRAIdentity
A
;
auth_timeless
:>
CMRADiscrete
A
;
}
.
Definition
authGF
(
A
:
cmraT
)
:
iFunctor
:=
constF
(
authR
A
A
).
Definition
authGF
(
A
:
cmraT
)
:
iFunctor
:=
constF
(
authR
A
).
Instance
authGF_inGF
(
A
:
cmraT
)
`
{
inGF
Λ
Σ
(
authGF
A
)
}
`
{
CMRAIdentity
A
,
CMRADiscrete
A
}
:
authG
Λ
Σ
A
.
Proof
.
split
;
try
apply
_.
apply
:
inGF_inG
.
Qed
.
...
...
program_logic/global_functor.v
View file @
448a8b62
...
...
@@ -18,7 +18,7 @@ Notation "[ F ; .. ; F' ]" :=
(
iFunctors
.
cons
F
..
(
iFunctors
.
cons
F
'
iFunctors
.
nil
)
..)
:
iFunctors_scope
.
Module
iFunctorG
.
Definition
nil
:
iFunctorG
:=
const
(
constF
unitR
A
).
Definition
nil
:
iFunctorG
:=
const
(
constF
unitR
).
Definition
cons
(
F
:
iFunctor
)
(
Σ
:
iFunctorG
)
:
iFunctorG
:=
λ
n
,
match
n
with
O
=>
F
|
S
n
=>
Σ
n
end
.
...
...
program_logic/model.v
View file @
448a8b62
...
...
@@ -10,7 +10,7 @@ propositions using the agreement CMRA. *)
(
*
TODO
RJ
:
Can
we
make
use
of
resF
,
the
resource
functor
?
*
)
Module
iProp
.
Definition
F
(
Λ
:
language
)
(
Σ
:
iFunctor
)
(
A
B
:
cofeT
)
:
cofeT
:=
uPredC
(
resR
A
Λ
Σ
(
laterC
A
)).
uPredC
(
resR
Λ
Σ
(
laterC
A
)).
Definition
map
{
Λ
:
language
}
{
Σ
:
iFunctor
}
{
A1
A2
B1
B2
:
cofeT
}
(
f
:
(
A2
-
n
>
A1
)
*
(
B1
-
n
>
B2
))
:
F
Λ
Σ
A1
B1
-
n
>
F
Λ
Σ
A2
B2
:=
uPredC_map
(
resC_map
(
laterC_map
(
f
.1
))).
...
...
@@ -33,11 +33,11 @@ End iProp.
(
*
Solution
*
)
Definition
iPreProp
(
Λ
:
language
)
(
Σ
:
iFunctor
)
:
cofeT
:=
iProp
.
result
Λ
Σ
.
Definition
iRes
Λ
Σ
:=
res
Λ
Σ
(
laterC
(
iPreProp
Λ
Σ
)).
Definition
iResR
A
Λ
Σ
:=
resR
A
Λ
Σ
(
laterC
(
iPreProp
Λ
Σ
)).
Definition
iWld
Λ
Σ
:=
mapR
A
positive
(
agreeR
A
(
laterC
(
iPreProp
Λ
Σ
))).
Definition
iPst
Λ
:=
exclR
A
(
istateC
Λ
).
Definition
iResR
Λ
Σ
:=
resR
Λ
Σ
(
laterC
(
iPreProp
Λ
Σ
)).
Definition
iWld
Λ
Σ
:=
mapR
positive
(
agreeR
(
laterC
(
iPreProp
Λ
Σ
))).
Definition
iPst
Λ
:=
exclR
(
istateC
Λ
).
Definition
iGst
Λ
Σ
:=
ifunctor_car
Σ
(
laterC
(
iPreProp
Λ
Σ
)).
Definition
iProp
(
Λ
:
language
)
(
Σ
:
iFunctor
)
:
cofeT
:=
uPredC
(
iResR
A
Λ
Σ
).
Definition
iProp
(
Λ
:
language
)
(
Σ
:
iFunctor
)
:
cofeT
:=
uPredC
(
iResR
Λ
Σ
).
Definition
iProp_unfold
{
Λ
Σ
}
:
iProp
Λ
Σ
-
n
>
iPreProp
Λ
Σ
:=
solution_fold
_.
Definition
iProp_fold
{
Λ
Σ
}
:
iPreProp
Λ
Σ
-
n
>
iProp
Λ
Σ
:=
solution_unfold
_.
Lemma
iProp_fold_unfold
{
Λ
Σ
}
(
P
:
iProp
Λ
Σ
)
:
iProp_fold
(
iProp_unfold
P
)
≡
P
.
...
...
program_logic/resources.v
View file @
448a8b62
...
...
@@ -3,9 +3,9 @@ From algebra Require Import upred.
From
program_logic
Require
Export
language
.
Record
res
(
Λ
:
language
)
(
Σ
:
iFunctor
)
(
A
:
cofeT
)
:=
Res
{
wld
:
mapR
A
positive
(
agreeR
A
A
);
pst
:
exclR
A
(
istateC
Λ
);
gst
:
optionR
A
(
Σ
A
);
wld
:
mapR
positive
(
agreeR
A
);
pst
:
exclR
(
istateC
Λ
);
gst
:
optionR
(
Σ
A
);
}
.
Add
Printing
Constructor
res
.
Arguments
Res
{
_
_
_
}
_
_
_.
...
...
@@ -123,8 +123,8 @@ Proof.
(
cmra_extend
n
(
gst
r
)
(
gst
r1
)
(
gst
r2
))
as
([
m
m
'
]
&?&?&?
);
auto
.
by
exists
(
Res
w
σ
m
,
Res
w
'
σ'
m
'
).
Qed
.
Canonical
Structure
resR
A
:
cmraT
:=
CMRAT
res_cofe_mixin
res_cmra_mixin
.
Global
Instance
res_cmra_identity
:
CMRAIdentity
resR
A
.
Canonical
Structure
resR
:
cmraT
:=
CMRAT
res_cofe_mixin
res_cmra_mixin
.
Global
Instance
res_cmra_identity
:
CMRAIdentity
resR
.
Proof
.
split
.
-
split_and
!
;
apply
cmra_empty_valid
.
...
...
@@ -170,7 +170,7 @@ Proof. by uPred.unseal. Qed.
End
res
.
Arguments
resC
:
clear
implicits
.
Arguments
resR
A
:
clear
implicits
.
Arguments
resR
:
clear
implicits
.
Definition
res_map
{
Λ
Σ
A
B
}
(
f
:
A
-
n
>
B
)
(
r
:
res
Λ
Σ
A
)
:
res
Λ
Σ
B
:=
Res
(
agree_map
f
<
$
>
wld
r
)
(
pst
r
)
(
ifunctor_map
Σ
f
<
$
>
gst
r
).
...
...
@@ -211,7 +211,7 @@ Proof.
intros
(
?&?&?
);
split_and
!
;
simpl
;
try
apply
:
included_preserving
.
Qed
.
Definition
resC_map
{
Λ
Σ
A
B
}
(
f
:
A
-
n
>
B
)
:
resC
Λ
Σ
A
-
n
>
resC
Λ
Σ
B
:=
CofeMor
(
res_map
f
:
res
RA
Λ
Σ
A
→
res
RA
Λ
Σ
B
).
CofeMor
(
res_map
f
:
res
C
Λ
Σ
A
→
res
C
Λ
Σ
B
).
Instance
resC_map_ne
{
Λ
Σ
A
B
}
n
:
Proper
(
dist
n
==>
dist
n
)
(
@
resC_map
Λ
Σ
A
B
).
Proof
.
...
...
@@ -221,7 +221,7 @@ Proof.
Qed
.
Program
Definition
resF
{
Λ
Σ
}
:
iFunctor
:=
{|
ifunctor_car
:=
resR
A
Λ
Σ
;
ifunctor_car
:=
resR
Λ
Σ
;
ifunctor_map
A
B
:=
resC_map
|}
.
Next
Obligation
.
intros
Λ
Σ
A
x
.
by
rewrite
/=
res_map_id
.
Qed
.
...
...
program_logic/saved_prop.v
View file @
448a8b62
...
...
@@ -3,7 +3,7 @@ From program_logic Require Export global_functor.
Import
uPred
.
Notation
savedPropG
Λ
Σ
:=
(
inG
Λ
Σ
(
agreeR
A
(
laterC
(
iPreProp
Λ
(
globalF
Σ
))))).
(
inG
Λ
Σ
(
agreeR
(
laterC
(
iPreProp
Λ
(
globalF
Σ
))))).
Instance
inGF_savedPropG
`
{
inGF
Λ
Σ
agreeF
}
:
savedPropG
Λ
Σ
.
Proof
.
apply
:
inGF_inG
.
Qed
.
...
...
program_logic/sts.v
View file @
448a8b62
...
...
@@ -3,12 +3,12 @@ From program_logic Require Export invariants global_functor.
Import
uPred
.
Class
stsG
Λ
Σ
(
sts
:
stsT
)
:=
StsG
{
sts_inG
:>
inG
Λ
Σ
(
stsR
A
sts
);
sts_inG
:>
inG
Λ
Σ
(
stsR
sts
);
sts_inhabited
:>
Inhabited
(
sts
.
state
sts
);
}
.
Coercion
sts_inG
:
stsG
>->
inG
.
Definition
stsGF
(
sts
:
stsT
)
:
iFunctor
:=
constF
(
stsR
A
sts
).
Definition
stsGF
(
sts
:
stsT
)
:
iFunctor
:=
constF
(
stsR
sts
).
Instance
inGF_stsG
sts
`
{
inGF
Λ
Σ
(
stsGF
sts
)
}
`
{
Inhabited
(
sts
.
state
sts
)
}
:
stsG
Λ
Σ
sts
.
Proof
.
split
;
try
apply
_.
apply
:
inGF_inG
.
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