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
bf610ff2
Commit
bf610ff2
authored
Feb 29, 2016
by
Ralf Jung
Browse files
rename: minus -> div. Also change notation accordingly.
parent
9ac5d31a
Changes
12
Hide whitespace changes
Inline
Side-by-side
algebra/agree.v
View file @
bf610ff2
...
...
@@ -61,7 +61,7 @@ Program Instance agree_op : Op (agree A) := λ x y,
agree_is_valid
n
:
=
agree_is_valid
x
n
∧
agree_is_valid
y
n
∧
x
≡
{
n
}
≡
y
|}.
Next
Obligation
.
naive_solver
eauto
using
agree_valid_S
,
dist_S
.
Qed
.
Instance
agree_unit
:
Unit
(
agree
A
)
:
=
id
.
Instance
agree_
minus
:
Minus
(
agree
A
)
:
=
λ
x
y
,
x
.
Instance
agree_
div
:
Div
(
agree
A
)
:
=
λ
x
y
,
x
.
Instance
:
Comm
(
≡
)
(@
op
(
agree
A
)
_
).
Proof
.
intros
x
y
;
split
;
[
naive_solver
|
by
intros
n
(?&?&
Hxy
)
;
apply
Hxy
].
Qed
.
...
...
algebra/auth.v
View file @
bf610ff2
...
...
@@ -89,8 +89,8 @@ Instance auth_unit : Unit (auth A) := λ x,
Auth
(
unit
(
authoritative
x
))
(
unit
(
own
x
)).
Instance
auth_op
:
Op
(
auth
A
)
:
=
λ
x
y
,
Auth
(
authoritative
x
⋅
authoritative
y
)
(
own
x
⋅
own
y
).
Instance
auth_
minus
:
Minus
(
auth
A
)
:
=
λ
x
y
,
Auth
(
authoritative
x
⩪
authoritative
y
)
(
own
x
⩪
own
y
).
Instance
auth_
div
:
Div
(
auth
A
)
:
=
λ
x
y
,
Auth
(
authoritative
x
÷
authoritative
y
)
(
own
x
÷
own
y
).
Lemma
auth_included
(
x
y
:
auth
A
)
:
x
≼
y
↔
authoritative
x
≼
authoritative
y
∧
own
x
≼
own
y
.
...
...
@@ -126,7 +126,7 @@ Proof.
intros
n
[[
a1
|
|]
b1
]
[[
a2
|
|]
b2
]
;
naive_solver
eauto
using
cmra_validN_op_l
,
cmra_validN_includedN
.
-
by
intros
??
;
rewrite
auth_included
;
intros
[??]
;
split
;
simpl
;
apply
cmra_op_
minus
.
intros
[??]
;
split
;
simpl
;
apply
cmra_op_
div
.
-
intros
n
x
y1
y2
?
[??]
;
simpl
in
*.
destruct
(
cmra_extend
n
(
authoritative
x
)
(
authoritative
y1
)
(
authoritative
y2
))
as
(
ea
&?&?&?)
;
auto
using
authoritative_validN
.
...
...
algebra/cmra.v
View file @
bf610ff2
...
...
@@ -14,9 +14,9 @@ Notation "(≼)" := included (only parsing) : C_scope.
Hint
Extern
0
(
_
≼
_
)
=>
reflexivity
.
Instance
:
Params
(@
included
)
3
.
Class
Minus
(
A
:
Type
)
:
=
minus
:
A
→
A
→
A
.
Instance
:
Params
(@
minus
)
2
.
Infix
"
⩪
"
:
=
minus
(
at
level
40
)
:
C_scope
.
Class
Div
(
A
:
Type
)
:
=
div
:
A
→
A
→
A
.
Instance
:
Params
(@
div
)
2
.
Infix
"
÷
"
:
=
div
:
C_scope
.
Class
ValidN
(
A
:
Type
)
:
=
validN
:
nat
→
A
→
Prop
.
Instance
:
Params
(@
validN
)
3
.
...
...
@@ -34,12 +34,12 @@ Instance: Params (@includedN) 4.
Hint
Extern
0
(
_
≼
{
_
}
_
)
=>
reflexivity
.
Record
CMRAMixin
A
`
{
Dist
A
,
Equiv
A
,
Unit
A
,
Op
A
,
Valid
A
,
ValidN
A
,
Minus
A
}
:
=
{
`
{
Dist
A
,
Equiv
A
,
Unit
A
,
Op
A
,
Valid
A
,
ValidN
A
,
Div
A
}
:
=
{
(* setoids *)
mixin_cmra_op_ne
n
(
x
:
A
)
:
Proper
(
dist
n
==>
dist
n
)
(
op
x
)
;
mixin_cmra_unit_ne
n
:
Proper
(
dist
n
==>
dist
n
)
unit
;
mixin_cmra_validN_ne
n
:
Proper
(
dist
n
==>
impl
)
(
validN
n
)
;
mixin_cmra_
minus
_ne
n
:
Proper
(
dist
n
==>
dist
n
==>
dist
n
)
minus
;
mixin_cmra_
div
_ne
n
:
Proper
(
dist
n
==>
dist
n
==>
dist
n
)
div
;
(* valid *)
mixin_cmra_valid_validN
x
:
✓
x
↔
∀
n
,
✓
{
n
}
x
;
mixin_cmra_validN_S
n
x
:
✓
{
S
n
}
x
→
✓
{
n
}
x
;
...
...
@@ -50,7 +50,7 @@ Record CMRAMixin A
mixin_cmra_unit_idemp
x
:
unit
(
unit
x
)
≡
unit
x
;
mixin_cmra_unit_preserving
x
y
:
x
≼
y
→
unit
x
≼
unit
y
;
mixin_cmra_validN_op_l
n
x
y
:
✓
{
n
}
(
x
⋅
y
)
→
✓
{
n
}
x
;
mixin_cmra_op_
minus
x
y
:
x
≼
y
→
x
⋅
y
⩪
x
≡
y
;
mixin_cmra_op_
div
x
y
:
x
≼
y
→
x
⋅
y
÷
x
≡
y
;
mixin_cmra_extend
n
x
y1
y2
:
✓
{
n
}
x
→
x
≡
{
n
}
≡
y1
⋅
y2
→
{
z
|
x
≡
z
.
1
⋅
z
.
2
∧
z
.
1
≡
{
n
}
≡
y1
∧
z
.
2
≡
{
n
}
≡
y2
}
...
...
@@ -66,7 +66,7 @@ Structure cmraT := CMRAT {
cmra_op
:
Op
cmra_car
;
cmra_valid
:
Valid
cmra_car
;
cmra_validN
:
ValidN
cmra_car
;
cmra_
minus
:
Minus
cmra_car
;
cmra_
div
:
Div
cmra_car
;
cmra_cofe_mixin
:
CofeMixin
cmra_car
;
cmra_mixin
:
CMRAMixin
cmra_car
}.
...
...
@@ -79,11 +79,11 @@ Arguments cmra_unit : simpl never.
Arguments
cmra_op
:
simpl
never
.
Arguments
cmra_valid
:
simpl
never
.
Arguments
cmra_validN
:
simpl
never
.
Arguments
cmra_
minus
:
simpl
never
.
Arguments
cmra_
div
:
simpl
never
.
Arguments
cmra_cofe_mixin
:
simpl
never
.
Arguments
cmra_mixin
:
simpl
never
.
Add
Printing
Constructor
cmraT
.
Existing
Instances
cmra_unit
cmra_op
cmra_valid
cmra_validN
cmra_
minus
.
Existing
Instances
cmra_unit
cmra_op
cmra_valid
cmra_validN
cmra_
div
.
Coercion
cmra_cofeC
(
A
:
cmraT
)
:
cofeT
:
=
CofeT
(
cmra_cofe_mixin
A
).
Canonical
Structure
cmra_cofeC
.
...
...
@@ -97,9 +97,9 @@ Section cmra_mixin.
Proof
.
apply
(
mixin_cmra_unit_ne
_
(
cmra_mixin
A
)).
Qed
.
Global
Instance
cmra_validN_ne
n
:
Proper
(
dist
n
==>
impl
)
(@
validN
A
_
n
).
Proof
.
apply
(
mixin_cmra_validN_ne
_
(
cmra_mixin
A
)).
Qed
.
Global
Instance
cmra_
minus
_ne
n
:
Proper
(
dist
n
==>
dist
n
==>
dist
n
)
(@
minus
A
_
).
Proof
.
apply
(
mixin_cmra_
minus
_ne
_
(
cmra_mixin
A
)).
Qed
.
Global
Instance
cmra_
div
_ne
n
:
Proper
(
dist
n
==>
dist
n
==>
dist
n
)
(@
div
A
_
).
Proof
.
apply
(
mixin_cmra_
div
_ne
_
(
cmra_mixin
A
)).
Qed
.
Lemma
cmra_valid_validN
x
:
✓
x
↔
∀
n
,
✓
{
n
}
x
.
Proof
.
apply
(
mixin_cmra_valid_validN
_
(
cmra_mixin
A
)).
Qed
.
Lemma
cmra_validN_S
n
x
:
✓
{
S
n
}
x
→
✓
{
n
}
x
.
...
...
@@ -116,8 +116,8 @@ Section cmra_mixin.
Proof
.
apply
(
mixin_cmra_unit_preserving
_
(
cmra_mixin
A
)).
Qed
.
Lemma
cmra_validN_op_l
n
x
y
:
✓
{
n
}
(
x
⋅
y
)
→
✓
{
n
}
x
.
Proof
.
apply
(
mixin_cmra_validN_op_l
_
(
cmra_mixin
A
)).
Qed
.
Lemma
cmra_op_
minus
x
y
:
x
≼
y
→
x
⋅
y
⩪
x
≡
y
.
Proof
.
apply
(
mixin_cmra_op_
minus
_
(
cmra_mixin
A
)).
Qed
.
Lemma
cmra_op_
div
x
y
:
x
≼
y
→
x
⋅
y
÷
x
≡
y
.
Proof
.
apply
(
mixin_cmra_op_
div
_
(
cmra_mixin
A
)).
Qed
.
Lemma
cmra_extend
n
x
y1
y2
:
✓
{
n
}
x
→
x
≡
{
n
}
≡
y1
⋅
y2
→
{
z
|
x
≡
z
.
1
⋅
z
.
2
∧
z
.
1
≡
{
n
}
≡
y1
∧
z
.
2
≡
{
n
}
≡
y2
}.
...
...
@@ -188,7 +188,7 @@ Global Instance cmra_validN_ne' : Proper (dist n ==> iff) (@validN A _ n) | 1.
Proof
.
by
split
;
apply
cmra_validN_ne
.
Qed
.
Global
Instance
cmra_validN_proper
:
Proper
((
≡
)
==>
iff
)
(@
validN
A
_
n
)
|
1
.
Proof
.
by
intros
n
x1
x2
Hx
;
apply
cmra_validN_ne'
,
equiv_dist
.
Qed
.
Global
Instance
cmra_
minus
_proper
:
Proper
((
≡
)
==>
(
≡
)
==>
(
≡
))
(@
minus
A
_
).
Global
Instance
cmra_
div
_proper
:
Proper
((
≡
)
==>
(
≡
)
==>
(
≡
))
(@
div
A
_
).
Proof
.
apply
(
ne_proper_2
_
).
Qed
.
Global
Instance
cmra_valid_proper
:
Proper
((
≡
)
==>
iff
)
(@
valid
A
_
).
...
...
@@ -246,16 +246,16 @@ Proof. rewrite -{1}(cmra_unit_l x); apply cmra_validN_op_l. Qed.
Lemma
cmra_unit_valid
x
:
✓
x
→
✓
unit
x
.
Proof
.
rewrite
-{
1
}(
cmra_unit_l
x
)
;
apply
cmra_valid_op_l
.
Qed
.
(** **
Minus
*)
Lemma
cmra_op_
minus
'
n
x
y
:
x
≼
{
n
}
y
→
x
⋅
y
⩪
x
≡
{
n
}
≡
y
.
Proof
.
intros
[
z
->].
by
rewrite
cmra_op_
minus
;
last
exists
z
.
Qed
.
(** **
Div
*)
Lemma
cmra_op_
div
'
n
x
y
:
x
≼
{
n
}
y
→
x
⋅
y
÷
x
≡
{
n
}
≡
y
.
Proof
.
intros
[
z
->].
by
rewrite
cmra_op_
div
;
last
exists
z
.
Qed
.
(** ** Order *)
Lemma
cmra_included_includedN
x
y
:
x
≼
y
↔
∀
n
,
x
≼
{
n
}
y
.
Proof
.
split
;
[
by
intros
[
z
Hz
]
n
;
exists
z
;
rewrite
Hz
|].
intros
Hxy
;
exists
(
y
⩪
x
)
;
apply
equiv_dist
=>
n
.
by
rewrite
cmra_op_
minus
'
.
intros
Hxy
;
exists
(
y
÷
x
)
;
apply
equiv_dist
=>
n
.
by
rewrite
cmra_op_
div
'
.
Qed
.
Global
Instance
cmra_includedN_preorder
n
:
PreOrder
(@
includedN
A
_
_
n
).
Proof
.
...
...
@@ -486,12 +486,12 @@ End cmra_transport.
(** * Instances *)
(** ** Discrete CMRA *)
Class
RA
A
`
{
Equiv
A
,
Unit
A
,
Op
A
,
Valid
A
,
Minus
A
}
:
=
{
Class
RA
A
`
{
Equiv
A
,
Unit
A
,
Op
A
,
Valid
A
,
Div
A
}
:
=
{
(* setoids *)
ra_op_ne
(
x
:
A
)
:
Proper
((
≡
)
==>
(
≡
))
(
op
x
)
;
ra_unit_ne
:
>
Proper
((
≡
)
==>
(
≡
))
unit
;
ra_validN_ne
:
>
Proper
((
≡
)
==>
impl
)
valid
;
ra_
minus
_ne
:
>
Proper
((
≡
)
==>
(
≡
)
==>
(
≡
))
minus
;
ra_
div
_ne
:
>
Proper
((
≡
)
==>
(
≡
)
==>
(
≡
))
div
;
(* monoid *)
ra_assoc
:
>
Assoc
(
≡
)
(
⋅
)
;
ra_comm
:
>
Comm
(
≡
)
(
⋅
)
;
...
...
@@ -499,12 +499,12 @@ Class RA A `{Equiv A, Unit A, Op A, Valid A, Minus A} := {
ra_unit_idemp
x
:
unit
(
unit
x
)
≡
unit
x
;
ra_unit_preserving
x
y
:
x
≼
y
→
unit
x
≼
unit
y
;
ra_valid_op_l
x
y
:
✓
(
x
⋅
y
)
→
✓
x
;
ra_op_
minus
x
y
:
x
≼
y
→
x
⋅
y
⩪
x
≡
y
ra_op_
div
x
y
:
x
≼
y
→
x
⋅
y
÷
x
≡
y
}.
Section
discrete
.
Context
{
A
:
cofeT
}
`
{
Discrete
A
}.
Context
`
{
Unit
A
,
Op
A
,
Valid
A
,
Minus
A
}
(
ra
:
RA
A
).
Context
`
{
Unit
A
,
Op
A
,
Valid
A
,
Div
A
}
(
ra
:
RA
A
).
Instance
discrete_validN
:
ValidN
A
:
=
λ
n
x
,
✓
x
.
Definition
discrete_cmra_mixin
:
CMRAMixin
A
.
...
...
@@ -525,7 +525,7 @@ Section unit.
Instance
unit_valid
:
Valid
()
:
=
λ
x
,
True
.
Instance
unit_unit
:
Unit
()
:
=
λ
x
,
x
.
Instance
unit_op
:
Op
()
:
=
λ
x
y
,
().
Instance
unit_
minus
:
Minus
()
:
=
λ
x
y
,
().
Instance
unit_
div
:
Div
()
:
=
λ
x
y
,
().
Global
Instance
unit_empty
:
Empty
()
:
=
().
Definition
unit_ra
:
RA
().
Proof
.
by
split
.
Qed
.
...
...
@@ -544,7 +544,7 @@ Section prod.
Instance
prod_unit
:
Unit
(
A
*
B
)
:
=
λ
x
,
(
unit
(
x
.
1
),
unit
(
x
.
2
)).
Instance
prod_valid
:
Valid
(
A
*
B
)
:
=
λ
x
,
✓
x
.
1
∧
✓
x
.
2
.
Instance
prod_validN
:
ValidN
(
A
*
B
)
:
=
λ
n
x
,
✓
{
n
}
x
.
1
∧
✓
{
n
}
x
.
2
.
Instance
prod_
minus
:
Minus
(
A
*
B
)
:
=
λ
x
y
,
(
x
.
1
⩪
y
.
1
,
x
.
2
⩪
y
.
2
).
Instance
prod_
div
:
Div
(
A
*
B
)
:
=
λ
x
y
,
(
x
.
1
÷
y
.
1
,
x
.
2
÷
y
.
2
).
Lemma
prod_included
(
x
y
:
A
*
B
)
:
x
≼
y
↔
x
.
1
≼
y
.
1
∧
x
.
2
≼
y
.
2
.
Proof
.
split
;
[
intros
[
z
Hz
]
;
split
;
[
exists
(
z
.
1
)|
exists
(
z
.
2
)]
;
apply
Hz
|].
...
...
@@ -575,7 +575,7 @@ Section prod.
by
intros
[??]
;
split
;
apply
cmra_unit_preserving
.
-
intros
n
x
y
[??]
;
split
;
simpl
in
*
;
eauto
using
cmra_validN_op_l
.
-
intros
x
y
;
rewrite
prod_included
;
intros
[??].
by
split
;
apply
cmra_op_
minus
.
by
split
;
apply
cmra_op_
div
.
-
intros
n
x
y1
y2
[??]
[??]
;
simpl
in
*.
destruct
(
cmra_extend
n
(
x
.
1
)
(
y1
.
1
)
(
y2
.
1
))
as
(
z1
&?&?&?)
;
auto
.
destruct
(
cmra_extend
n
(
x
.
2
)
(
y1
.
2
)
(
y2
.
2
))
as
(
z2
&?&?&?)
;
auto
.
...
...
algebra/dec_agree.v
View file @
bf610ff2
...
...
@@ -27,7 +27,7 @@ Instance dec_agree_op : Op (dec_agree A) := λ x y,
|
_
,
_
=>
DecAgreeBot
end
.
Instance
dec_agree_unit
:
Unit
(
dec_agree
A
)
:
=
id
.
Instance
dec_agree_
minus
:
Minus
(
dec_agree
A
)
:
=
λ
x
y
,
x
.
Instance
dec_agree_
div
:
Div
(
dec_agree
A
)
:
=
λ
x
y
,
x
.
Definition
dec_agree_ra
:
RA
(
dec_agree
A
).
Proof
.
...
...
algebra/dra.v
View file @
bf610ff2
...
...
@@ -18,18 +18,18 @@ Definition dra_included `{Equiv A, Valid A, Disjoint A, Op A} := λ x y,
Instance
:
Params
(@
dra_included
)
4
.
Local
Infix
"≼"
:
=
dra_included
.
Class
DRA
A
`
{
Equiv
A
,
Valid
A
,
Unit
A
,
Disjoint
A
,
Op
A
,
Minus
A
}
:
=
{
Class
DRA
A
`
{
Equiv
A
,
Valid
A
,
Unit
A
,
Disjoint
A
,
Op
A
,
Div
A
}
:
=
{
(* setoids *)
dra_equivalence
:
>
Equivalence
((
≡
)
:
relation
A
)
;
dra_op_proper
:
>
Proper
((
≡
)
==>
(
≡
)
==>
(
≡
))
(
⋅
)
;
dra_unit_proper
:
>
Proper
((
≡
)
==>
(
≡
))
unit
;
dra_valid_proper
:
>
Proper
((
≡
)
==>
impl
)
valid
;
dra_disjoint_proper
:
>
∀
x
,
Proper
((
≡
)
==>
impl
)
(
disjoint
x
)
;
dra_
minus
_proper
:
>
Proper
((
≡
)
==>
(
≡
)
==>
(
≡
))
minus
;
dra_
div
_proper
:
>
Proper
((
≡
)
==>
(
≡
)
==>
(
≡
))
div
;
(* validity *)
dra_op_valid
x
y
:
✓
x
→
✓
y
→
x
⊥
y
→
✓
(
x
⋅
y
)
;
dra_unit_valid
x
:
✓
x
→
✓
unit
x
;
dra_
minus
_valid
x
y
:
✓
x
→
✓
y
→
x
≼
y
→
✓
(
y
⩪
x
)
;
dra_
div
_valid
x
y
:
✓
x
→
✓
y
→
x
≼
y
→
✓
(
y
÷
x
)
;
(* monoid *)
dra_assoc
:
>
Assoc
(
≡
)
(
⋅
)
;
dra_disjoint_ll
x
y
z
:
✓
x
→
✓
y
→
✓
z
→
x
⊥
y
→
x
⋅
y
⊥
z
→
x
⊥
z
;
...
...
@@ -40,8 +40,8 @@ Class DRA A `{Equiv A, Valid A, Unit A, Disjoint A, Op A, Minus A} := {
dra_unit_l
x
:
✓
x
→
unit
x
⋅
x
≡
x
;
dra_unit_idemp
x
:
✓
x
→
unit
(
unit
x
)
≡
unit
x
;
dra_unit_preserving
x
y
:
✓
x
→
✓
y
→
x
≼
y
→
unit
x
≼
unit
y
;
dra_disjoint_
minus
x
y
:
✓
x
→
✓
y
→
x
≼
y
→
x
⊥
y
⩪
x
;
dra_op_
minus
x
y
:
✓
x
→
✓
y
→
x
≼
y
→
x
⋅
y
⩪
x
≡
y
dra_disjoint_
div
x
y
:
✓
x
→
✓
y
→
x
≼
y
→
x
⊥
y
÷
x
;
dra_op_
div
x
y
:
✓
x
→
✓
y
→
x
≼
y
→
x
⋅
y
÷
x
≡
y
}.
Section
dra
.
...
...
@@ -95,10 +95,10 @@ Program Instance validity_op : Op T := λ x y,
Validity
(
validity_car
x
⋅
validity_car
y
)
(
✓
x
∧
✓
y
∧
validity_car
x
⊥
validity_car
y
)
_
.
Solve
Obligations
with
naive_solver
auto
using
dra_op_valid
.
Program
Instance
validity_
minus
:
Minus
T
:
=
λ
x
y
,
Validity
(
validity_car
x
⩪
validity_car
y
)
Program
Instance
validity_
div
:
Div
T
:
=
λ
x
y
,
Validity
(
validity_car
x
÷
validity_car
y
)
(
✓
x
∧
✓
y
∧
validity_car
y
≼
validity_car
x
)
_
.
Solve
Obligations
with
naive_solver
auto
using
dra_
minus
_valid
.
Solve
Obligations
with
naive_solver
auto
using
dra_
div
_valid
.
Definition
validity_ra
:
RA
(
discreteC
T
).
Proof
.
...
...
@@ -120,15 +120,15 @@ Proof.
-
intros
[
x
px
?]
;
split
;
naive_solver
eauto
using
dra_unit_l
,
dra_unit_disjoint_l
.
-
intros
[
x
px
?]
;
split
;
naive_solver
eauto
using
dra_unit_idemp
.
-
intros
x
y
Hxy
;
exists
(
unit
y
⩪
unit
x
).
-
intros
x
y
Hxy
;
exists
(
unit
y
÷
unit
x
).
destruct
x
as
[
x
px
?],
y
as
[
y
py
?],
Hxy
as
[[
z
pz
?]
[??]]
;
simpl
in
*.
assert
(
py
→
unit
x
≼
unit
y
)
by
intuition
eauto
10
using
dra_unit_preserving
.
constructor
;
[|
symmetry
]
;
simpl
in
*
;
intuition
eauto
using
dra_op_
minus
,
dra_disjoint_
minus
,
dra_unit_valid
.
intuition
eauto
using
dra_op_
div
,
dra_disjoint_
div
,
dra_unit_valid
.
-
by
intros
[
x
px
?]
[
y
py
?]
(?&?&?).
-
intros
[
x
px
?]
[
y
py
?]
[[
z
pz
?]
[??]]
;
split
;
simpl
in
*
;
intuition
eauto
10
using
dra_disjoint_
minus
,
dra_op_
minus
.
intuition
eauto
10
using
dra_disjoint_
div
,
dra_op_
div
.
Qed
.
Definition
validityRA
:
cmraT
:
=
discreteRA
validity_ra
.
Instance
validity_cmra_discrete
:
...
...
algebra/excl.v
View file @
bf610ff2
...
...
@@ -98,7 +98,7 @@ Instance excl_op : Op (excl A) := λ x y,
|
ExclUnit
,
ExclUnit
=>
ExclUnit
|
_
,
_
=>
ExclBot
end
.
Instance
excl_
minus
:
Minus
(
excl
A
)
:
=
λ
x
y
,
Instance
excl_
div
:
Div
(
excl
A
)
:
=
λ
x
y
,
match
x
,
y
with
|
_
,
ExclUnit
=>
x
|
Excl
_
,
Excl
_
=>
ExclUnit
...
...
algebra/fin_maps.v
View file @
bf610ff2
...
...
@@ -96,11 +96,11 @@ Instance map_op : Op (gmap K A) := merge op.
Instance
map_unit
:
Unit
(
gmap
K
A
)
:
=
fmap
unit
.
Instance
map_valid
:
Valid
(
gmap
K
A
)
:
=
λ
m
,
∀
i
,
✓
(
m
!!
i
).
Instance
map_validN
:
ValidN
(
gmap
K
A
)
:
=
λ
n
m
,
∀
i
,
✓
{
n
}
(
m
!!
i
).
Instance
map_
minus
:
Minus
(
gmap
K
A
)
:
=
merge
minus
.
Instance
map_
div
:
Div
(
gmap
K
A
)
:
=
merge
div
.
Lemma
lookup_op
m1
m2
i
:
(
m1
⋅
m2
)
!!
i
=
m1
!!
i
⋅
m2
!!
i
.
Proof
.
by
apply
lookup_merge
.
Qed
.
Lemma
lookup_
minus
m1
m2
i
:
(
m1
⩪
m2
)
!!
i
=
m1
!!
i
⩪
m2
!!
i
.
Lemma
lookup_
div
m1
m2
i
:
(
m1
÷
m2
)
!!
i
=
m1
!!
i
÷
m2
!!
i
.
Proof
.
by
apply
lookup_merge
.
Qed
.
Lemma
lookup_unit
m
i
:
unit
m
!!
i
=
unit
(
m
!!
i
).
Proof
.
by
apply
lookup_fmap
.
Qed
.
...
...
@@ -109,16 +109,16 @@ Lemma map_included_spec (m1 m2 : gmap K A) : m1 ≼ m2 ↔ ∀ i, m1 !! i ≼ m2
Proof
.
split
.
-
by
intros
[
m
Hm
]
;
intros
i
;
exists
(
m
!!
i
)
;
rewrite
-
lookup_op
Hm
.
-
intros
Hm
;
exists
(
m2
⩪
m1
)
;
intros
i
.
by
rewrite
lookup_op
lookup_
minus
cmra_op_
minus
.
-
intros
Hm
;
exists
(
m2
÷
m1
)
;
intros
i
.
by
rewrite
lookup_op
lookup_
div
cmra_op_
div
.
Qed
.
Lemma
map_includedN_spec
(
m1
m2
:
gmap
K
A
)
n
:
m1
≼
{
n
}
m2
↔
∀
i
,
m1
!!
i
≼
{
n
}
m2
!!
i
.
Proof
.
split
.
-
by
intros
[
m
Hm
]
;
intros
i
;
exists
(
m
!!
i
)
;
rewrite
-
lookup_op
Hm
.
-
intros
Hm
;
exists
(
m2
⩪
m1
)
;
intros
i
.
by
rewrite
lookup_op
lookup_
minus
cmra_op_
minus
'
.
-
intros
Hm
;
exists
(
m2
÷
m1
)
;
intros
i
.
by
rewrite
lookup_op
lookup_
div
cmra_op_
div
'
.
Qed
.
Definition
map_cmra_mixin
:
CMRAMixin
(
gmap
K
A
).
...
...
@@ -127,7 +127,7 @@ Proof.
-
by
intros
n
m1
m2
m3
Hm
i
;
rewrite
!
lookup_op
(
Hm
i
).
-
by
intros
n
m1
m2
Hm
i
;
rewrite
!
lookup_unit
(
Hm
i
).
-
by
intros
n
m1
m2
Hm
?
i
;
rewrite
-(
Hm
i
).
-
by
intros
n
m1
m1'
Hm1
m2
m2'
Hm2
i
;
rewrite
!
lookup_
minus
(
Hm1
i
)
(
Hm2
i
).
-
by
intros
n
m1
m1'
Hm1
m2
m2'
Hm2
i
;
rewrite
!
lookup_
div
(
Hm1
i
)
(
Hm2
i
).
-
intros
m
;
split
.
+
by
intros
?
n
i
;
apply
cmra_valid_validN
.
+
intros
Hm
i
;
apply
cmra_valid_validN
=>
n
;
apply
Hm
.
...
...
@@ -141,7 +141,7 @@ Proof.
-
intros
n
m1
m2
Hm
i
;
apply
cmra_validN_op_l
with
(
m2
!!
i
).
by
rewrite
-
lookup_op
.
-
intros
x
y
;
rewrite
map_included_spec
=>
?
i
.
by
rewrite
lookup_op
lookup_
minus
cmra_op_
minus
.
by
rewrite
lookup_op
lookup_
div
cmra_op_
div
.
-
intros
n
m
m1
m2
Hm
Hm12
.
assert
(
∀
i
,
m
!!
i
≡
{
n
}
≡
m1
!!
i
⋅
m2
!!
i
)
as
Hm12'
by
(
by
intros
i
;
rewrite
-
lookup_op
).
...
...
algebra/frac.v
View file @
bf610ff2
...
...
@@ -3,7 +3,7 @@ From algebra Require Export cmra.
From
algebra
Require
Import
functor
upred
.
Local
Arguments
validN
_
_
_
!
_
/.
Local
Arguments
valid
_
_
!
_
/.
Local
Arguments
minus
_
_
!
_
!
_
/.
Local
Arguments
div
_
_
!
_
!
_
/.
Inductive
frac
(
A
:
Type
)
:
=
|
Frac
:
Qp
→
A
→
frac
A
...
...
@@ -129,11 +129,11 @@ Instance frac_op : Op (frac A) := λ x y,
|
Frac
q
a
,
FracUnit
|
FracUnit
,
Frac
q
a
=>
Frac
q
a
|
FracUnit
,
FracUnit
=>
FracUnit
end
.
Instance
frac_
minus
:
Minus
(
frac
A
)
:
=
λ
x
y
,
Instance
frac_
div
:
Div
(
frac
A
)
:
=
λ
x
y
,
match
x
,
y
with
|
_
,
FracUnit
=>
x
|
Frac
q1
a
,
Frac
q2
b
=>
match
q1
-
q2
with
Some
q
=>
Frac
q
(
a
⩪
b
)
|
None
=>
FracUnit
end
%
Qp
match
q1
-
q2
with
Some
q
=>
Frac
q
(
a
÷
b
)
|
None
=>
FracUnit
end
%
Qp
|
FracUnit
,
_
=>
FracUnit
end
.
...
...
@@ -159,7 +159,7 @@ Proof.
rewrite
-{
1
}(
Qcplus_0_r
q1
)
-
Qcplus_le_mono_l
;
auto
using
Qclt_le_weak
.
-
intros
[
q1
a1
|]
[
q2
a2
|]
[[
q3
a3
|]
Hx
]
;
inversion_clear
Hx
;
simplify_eq
/=
;
auto
.
+
rewrite
Qp_op_minus
.
by
constructor
;
[|
apply
cmra_op_
minus
;
exists
a3
].
+
rewrite
Qp_op_minus
.
by
constructor
;
[|
apply
cmra_op_
div
;
exists
a3
].
+
rewrite
Qp_minus_diag
.
by
constructor
.
-
intros
n
[
q
a
|]
y1
y2
Hx
Hx'
;
last
first
.
{
by
exists
(
∅
,
∅
)
;
destruct
y1
,
y2
;
inversion_clear
Hx'
.
}
...
...
algebra/iprod.v
View file @
bf610ff2
...
...
@@ -120,18 +120,18 @@ Section iprod_cmra.
Instance
iprod_unit
:
Unit
(
iprod
B
)
:
=
λ
f
x
,
unit
(
f
x
).
Instance
iprod_valid
:
Valid
(
iprod
B
)
:
=
λ
f
,
∀
x
,
✓
f
x
.
Instance
iprod_validN
:
ValidN
(
iprod
B
)
:
=
λ
n
f
,
∀
x
,
✓
{
n
}
f
x
.
Instance
iprod_
minus
:
Minus
(
iprod
B
)
:
=
λ
f
g
x
,
f
x
⩪
g
x
.
Instance
iprod_
div
:
Div
(
iprod
B
)
:
=
λ
f
g
x
,
f
x
÷
g
x
.
Definition
iprod_lookup_op
f
g
x
:
(
f
⋅
g
)
x
=
f
x
⋅
g
x
:
=
eq_refl
.
Definition
iprod_lookup_unit
f
x
:
(
unit
f
)
x
=
unit
(
f
x
)
:
=
eq_refl
.
Definition
iprod_lookup_
minus
f
g
x
:
(
f
⩪
g
)
x
=
f
x
⩪
g
x
:
=
eq_refl
.
Definition
iprod_lookup_
div
f
g
x
:
(
f
÷
g
)
x
=
f
x
÷
g
x
:
=
eq_refl
.
Lemma
iprod_included_spec
(
f
g
:
iprod
B
)
:
f
≼
g
↔
∀
x
,
f
x
≼
g
x
.
Proof
.
split
.
-
by
intros
[
h
Hh
]
x
;
exists
(
h
x
)
;
rewrite
/
op
/
iprod_op
(
Hh
x
).
-
intros
Hh
;
exists
(
g
⩪
f
)=>
x
;
specialize
(
Hh
x
).
by
rewrite
/
op
/
iprod_op
/
minus
/
iprod_
minus
cmra_op_
minus
.
-
intros
Hh
;
exists
(
g
÷
f
)=>
x
;
specialize
(
Hh
x
).
by
rewrite
/
op
/
iprod_op
/
div
/
iprod_
div
cmra_op_
div
.
Qed
.
Definition
iprod_cmra_mixin
:
CMRAMixin
(
iprod
B
).
...
...
@@ -140,7 +140,7 @@ Section iprod_cmra.
-
by
intros
n
f1
f2
f3
Hf
x
;
rewrite
iprod_lookup_op
(
Hf
x
).
-
by
intros
n
f1
f2
Hf
x
;
rewrite
iprod_lookup_unit
(
Hf
x
).
-
by
intros
n
f1
f2
Hf
?
x
;
rewrite
-(
Hf
x
).
-
by
intros
n
f
f'
Hf
g
g'
Hg
i
;
rewrite
iprod_lookup_
minus
(
Hf
i
)
(
Hg
i
).
-
by
intros
n
f
f'
Hf
g
g'
Hg
i
;
rewrite
iprod_lookup_
div
(
Hf
i
)
(
Hg
i
).
-
intros
g
;
split
.
+
intros
Hg
n
i
;
apply
cmra_valid_validN
,
Hg
.
+
intros
Hg
i
;
apply
cmra_valid_validN
=>
n
;
apply
Hg
.
...
...
@@ -153,7 +153,7 @@ Section iprod_cmra.
by
rewrite
iprod_lookup_unit
;
apply
cmra_unit_preserving
,
Hf
.
-
intros
n
f1
f2
Hf
x
;
apply
cmra_validN_op_l
with
(
f2
x
),
Hf
.
-
intros
f1
f2
;
rewrite
iprod_included_spec
=>
Hf
x
.
by
rewrite
iprod_lookup_op
iprod_lookup_
minus
cmra_op_
minus
;
try
apply
Hf
.
by
rewrite
iprod_lookup_op
iprod_lookup_
div
cmra_op_
div
;
try
apply
Hf
.
-
intros
n
f
f1
f2
Hf
Hf12
.
set
(
g
x
:
=
cmra_extend
n
(
f
x
)
(
f1
x
)
(
f2
x
)
(
Hf
x
)
(
Hf12
x
)).
exists
((
λ
x
,
(
proj1_sig
(
g
x
)).
1
),
(
λ
x
,
(
proj1_sig
(
g
x
)).
2
)).
...
...
algebra/option.v
View file @
bf610ff2
...
...
@@ -69,8 +69,8 @@ Instance option_validN : ValidN (option A) := λ n mx,
Global
Instance
option_empty
:
Empty
(
option
A
)
:
=
None
.
Instance
option_unit
:
Unit
(
option
A
)
:
=
fmap
unit
.
Instance
option_op
:
Op
(
option
A
)
:
=
union_with
(
λ
x
y
,
Some
(
x
⋅
y
)).
Instance
option_
minus
:
Minus
(
option
A
)
:
=
difference_with
(
λ
x
y
,
Some
(
x
⩪
y
)).
Instance
option_
div
:
Div
(
option
A
)
:
=
difference_with
(
λ
x
y
,
Some
(
x
÷
y
)).
Definition
Some_valid
a
:
✓
Some
a
↔
✓
a
:
=
reflexivity
_
.
Definition
Some_op
a
b
:
Some
(
a
⋅
b
)
=
Some
a
⋅
Some
b
:
=
eq_refl
.
...
...
@@ -107,7 +107,7 @@ Proof.
eauto
using
cmra_validN_op_l
.
-
intros
mx
my
;
rewrite
option_included
.
intros
[->|(
x
&
y
&->&->&?)]
;
[
by
destruct
my
|].
by
constructor
;
apply
cmra_op_
minus
.
by
constructor
;
apply
cmra_op_
div
.
-
intros
n
mx
my1
my2
.
destruct
mx
as
[
x
|],
my1
as
[
y1
|],
my2
as
[
y2
|]
;
intros
Hx
Hx'
;
try
(
by
exfalso
;
inversion
Hx'
;
auto
).
...
...
algebra/sts.v
View file @
bf610ff2
...
...
@@ -212,7 +212,7 @@ Global Instance sts_op : Op (car sts) := λ x1 x2,
|
frag
_
T1
,
auth
s
T2
=>
auth
s
(
T1
∪
T2
)
|
auth
s
T1
,
auth
_
T2
=>
auth
s
(
T1
∪
T2
)
(* never happens *)
end
.
Global
Instance
sts_
minus
:
Minus
(
car
sts
)
:
=
λ
x1
x2
,
Global
Instance
sts_
div
:
Div
(
car
sts
)
:
=
λ
x1
x2
,
match
x1
,
x2
with
|
frag
S1
T1
,
frag
S2
T2
=>
frag
(
up_set
S1
(
T1
∖
T2
))
(
T1
∖
T2
)
|
auth
s
T1
,
frag
_
T2
=>
auth
s
(
T1
∖
T2
)
...
...
program_logic/resources.v
View file @
bf610ff2
...
...
@@ -79,8 +79,8 @@ Instance res_unit : Unit (res Λ Σ A) := λ r,
Instance
res_valid
:
Valid
(
res
Λ
Σ
A
)
:
=
λ
r
,
✓
wld
r
∧
✓
pst
r
∧
✓
gst
r
.
Instance
res_validN
:
ValidN
(
res
Λ
Σ
A
)
:
=
λ
n
r
,
✓
{
n
}
wld
r
∧
✓
{
n
}
pst
r
∧
✓
{
n
}
gst
r
.
Instance
res_minus
:
Minus
(
res
Λ
Σ
A
)
:
=
λ
r1
r2
,
Res
(
wld
r1
⩪
wld
r2
)
(
pst
r1
⩪
pst
r2
)
(
gst
r1
⩪
gst
r2
).
Instance
res_minus
:
Div
(
res
Λ
Σ
A
)
:
=
λ
r1
r2
,
Res
(
wld
r1
÷
wld
r2
)
(
pst
r1
÷
pst
r2
)
(
gst
r1
÷
gst
r2
).
Lemma
res_included
(
r1
r2
:
res
Λ
Σ
A
)
:
r1
≼
r2
↔
wld
r1
≼
wld
r2
∧
pst
r1
≼
pst
r2
∧
gst
r1
≼
gst
r2
.
...
...
@@ -116,7 +116,7 @@ Proof.
-
intros
n
r1
r2
(?&?&?)
;
split_and
!
;
simpl
in
*
;
eapply
cmra_validN_op_l
;
eauto
.
-
intros
r1
r2
;
rewrite
res_included
;
intros
(?&?&?).
by
constructor
;
apply
cmra_op_
minus
.
by
constructor
;
apply
cmra_op_
div
.
-
intros
n
r
r1
r2
(?&?&?)
[???]
;
simpl
in
*.
destruct
(
cmra_extend
n
(
wld
r
)
(
wld
r1
)
(
wld
r2
))
as
([
w
w'
]&?&?&?),
(
cmra_extend
n
(
pst
r
)
(
pst
r1
)
(
pst
r2
))
as
([
σ
σ
'
]&?&?&?),
...
...
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