Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
7
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Open sidebar
George Pirlea
Iris
Commits
685148ab
Commit
685148ab
authored
Feb 17, 2016
by
Robbert Krebbers
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Use scheme - then + then * for bullets.
parent
a8591b70
Changes
48
Expand all
Hide whitespace changes
Inline
Side-by-side
Showing
48 changed files
with
881 additions
and
881 deletions
+881
-881
algebra/agree.v
algebra/agree.v
+15
-15
algebra/auth.v
algebra/auth.v
+21
-21
algebra/cmra.v
algebra/cmra.v
+23
-23
algebra/cmra_big_op.v
algebra/cmra_big_op.v
+7
-7
algebra/cofe.v
algebra/cofe.v
+23
-23
algebra/cofe_solver.v
algebra/cofe_solver.v
+18
-18
algebra/dra.v
algebra/dra.v
+16
-16
algebra/excl.v
algebra/excl.v
+18
-18
algebra/fin_maps.v
algebra/fin_maps.v
+30
-30
algebra/iprod.v
algebra/iprod.v
+29
-29
algebra/option.v
algebra/option.v
+24
-24
algebra/sts.v
algebra/sts.v
+30
-30
algebra/upred.v
algebra/upred.v
+22
-22
algebra/upred_big_op.v
algebra/upred_big_op.v
+6
-6
barrier/barrier.v
barrier/barrier.v
+1
-1
heap_lang/heap_lang.v
heap_lang/heap_lang.v
+3
-3
prelude/bsets.v
prelude/bsets.v
+5
-5
prelude/co_pset.v
prelude/co_pset.v
+17
-17
prelude/collections.v
prelude/collections.v
+12
-12
prelude/fin_collections.v
prelude/fin_collections.v
+17
-17
prelude/fin_maps.v
prelude/fin_maps.v
+59
-59
prelude/finite.v
prelude/finite.v
+23
-23
prelude/gmap.v
prelude/gmap.v
+14
-14
prelude/hashset.v
prelude/hashset.v
+9
-9
prelude/lexico.v
prelude/lexico.v
+6
-6
prelude/list.v
prelude/list.v
+182
-182
prelude/listset.v
prelude/listset.v
+17
-17
prelude/listset_nodup.v
prelude/listset_nodup.v
+8
-8
prelude/mapset.v
prelude/mapset.v
+10
-10
prelude/natmap.v
prelude/natmap.v
+15
-15
prelude/nmap.v
prelude/nmap.v
+18
-18
prelude/numbers.v
prelude/numbers.v
+10
-10
prelude/option.v
prelude/option.v
+3
-3
prelude/orders.v
prelude/orders.v
+21
-21
prelude/pmap.v
prelude/pmap.v
+45
-45
prelude/relations.v
prelude/relations.v
+3
-3
prelude/streams.v
prelude/streams.v
+3
-3
prelude/vector.v
prelude/vector.v
+10
-10
prelude/zmap.v
prelude/zmap.v
+13
-13
program_logic/adequacy.v
program_logic/adequacy.v
+5
-5
program_logic/ghost_ownership.v
program_logic/ghost_ownership.v
+9
-9
program_logic/hoare_lifting.v
program_logic/hoare_lifting.v
+4
-4
program_logic/model.v
program_logic/model.v
+3
-3
program_logic/ownership.v
program_logic/ownership.v
+2
-2
program_logic/pviewshifts.v
program_logic/pviewshifts.v
+4
-4
program_logic/resources.v
program_logic/resources.v
+29
-29
program_logic/weakestpre.v
program_logic/weakestpre.v
+8
-8
program_logic/wsat.v
program_logic/wsat.v
+11
-11
No files found.
algebra/agree.v
View file @
685148ab
...
...
@@ -33,17 +33,17 @@ Qed.
Definition
agree_cofe_mixin
:
CofeMixin
(
agree
A
).
Proof
.
split
.
*
intros
x
y
;
split
.
-
intros
x
y
;
split
.
+
by
intros
Hxy
n
;
split
;
intros
;
apply
Hxy
.
+
by
intros
Hxy
;
split
;
intros
;
apply
Hxy
with
n
.
*
split
.
-
split
.
+
by
split
.
+
by
intros
x
y
Hxy
;
split
;
intros
;
symmetry
;
apply
Hxy
;
auto
;
apply
Hxy
.
+
intros
x
y
z
Hxy
Hyz
;
split
;
intros
n'
;
intros
.
-
transitivity
(
agree_is_valid
y
n'
).
by
apply
Hxy
.
by
apply
Hyz
.
-
transitivity
(
y
n'
).
by
apply
Hxy
.
by
apply
Hyz
,
Hxy
.
*
intros
n
x
y
Hxy
;
split
;
intros
;
apply
Hxy
;
auto
.
*
intros
c
n
;
apply
and_wlog_r
;
intros
;
*
transitivity
(
agree_is_valid
y
n'
).
by
apply
Hxy
.
by
apply
Hyz
.
*
transitivity
(
y
n'
).
by
apply
Hxy
.
by
apply
Hyz
,
Hxy
.
-
intros
n
x
y
Hxy
;
split
;
intros
;
apply
Hxy
;
auto
.
-
intros
c
n
;
apply
and_wlog_r
;
intros
;
symmetry
;
apply
(
chain_cauchy
c
)
;
naive_solver
.
Qed
.
Canonical
Structure
agreeC
:
=
CofeT
agree_cofe_mixin
.
...
...
@@ -74,8 +74,8 @@ Proof.
intros
n
x
y1
y2
[
Hy'
Hy
]
;
split
;
[|
done
].
split
;
intros
(?&?&
Hxy
)
;
repeat
(
intro
||
split
)
;
try
apply
Hy'
;
eauto
using
agree_valid_le
.
*
etransitivity
;
[
apply
Hxy
|
apply
Hy
]
;
eauto
using
agree_valid_le
.
*
etransitivity
;
[
apply
Hxy
|
symmetry
;
apply
Hy
,
Hy'
]
;
-
etransitivity
;
[
apply
Hxy
|
apply
Hy
]
;
eauto
using
agree_valid_le
.
-
etransitivity
;
[
apply
Hxy
|
symmetry
;
apply
Hy
,
Hy'
]
;
eauto
using
agree_valid_le
.
Qed
.
Instance
:
Proper
(
dist
n
==>
dist
n
==>
dist
n
)
(@
op
(
agree
A
)
_
).
...
...
@@ -95,13 +95,13 @@ Qed.
Definition
agree_cmra_mixin
:
CMRAMixin
(
agree
A
).
Proof
.
split
;
try
(
apply
_
||
done
).
*
by
intros
n
x1
x2
Hx
y1
y2
Hy
.
*
intros
n
x
[?
Hx
]
;
split
;
[
by
apply
agree_valid_S
|
intros
n'
?].
-
by
intros
n
x1
x2
Hx
y1
y2
Hy
.
-
intros
n
x
[?
Hx
]
;
split
;
[
by
apply
agree_valid_S
|
intros
n'
?].
rewrite
(
Hx
n'
)
;
last
auto
.
symmetry
;
apply
dist_le
with
n
;
try
apply
Hx
;
auto
.
*
intros
x
;
apply
agree_idemp
.
*
by
intros
x
y
n
[(?&?&?)
?].
*
by
intros
x
y
n
;
rewrite
agree_includedN
.
-
intros
x
;
apply
agree_idemp
.
-
by
intros
x
y
n
[(?&?&?)
?].
-
by
intros
x
y
n
;
rewrite
agree_includedN
.
Qed
.
Lemma
agree_op_inv
(
x1
x2
:
agree
A
)
n
:
✓
{
n
}
(
x1
⋅
x2
)
→
x1
≡
{
n
}
≡
x2
.
Proof
.
intros
Hxy
;
apply
Hxy
.
Qed
.
...
...
@@ -113,8 +113,8 @@ Qed.
Definition
agree_cmra_extend_mixin
:
CMRAExtendMixin
(
agree
A
).
Proof
.
intros
n
x
y1
y2
Hval
Hx
;
exists
(
x
,
x
)
;
simpl
;
split
.
*
by
rewrite
agree_idemp
.
*
by
move
:
Hval
;
rewrite
Hx
;
move
=>
/
agree_op_inv
->
;
rewrite
agree_idemp
.
-
by
rewrite
agree_idemp
.
-
by
move
:
Hval
;
rewrite
Hx
;
move
=>
/
agree_op_inv
->
;
rewrite
agree_idemp
.
Qed
.
Canonical
Structure
agreeRA
:
cmraT
:
=
CMRAT
agree_cofe_mixin
agree_cmra_mixin
agree_cmra_extend_mixin
.
...
...
algebra/auth.v
View file @
685148ab
...
...
@@ -39,14 +39,14 @@ Instance auth_compl : Compl (auth A) := λ c,
Definition
auth_cofe_mixin
:
CofeMixin
(
auth
A
).
Proof
.
split
.
*
intros
x
y
;
unfold
dist
,
auth_dist
,
equiv
,
auth_equiv
.
-
intros
x
y
;
unfold
dist
,
auth_dist
,
equiv
,
auth_equiv
.
rewrite
!
equiv_dist
;
naive_solver
.
*
intros
n
;
split
.
-
intros
n
;
split
.
+
by
intros
?
;
split
.
+
by
intros
??
[??]
;
split
;
symmetry
.
+
intros
???
[??]
[??]
;
split
;
etransitivity
;
eauto
.
*
by
intros
?
[??]
[??]
[??]
;
split
;
apply
dist_S
.
*
intros
c
n
;
split
.
apply
(
conv_compl
(
chain_map
authoritative
c
)
n
).
-
by
intros
?
[??]
[??]
[??]
;
split
;
apply
dist_S
.
-
intros
c
n
;
split
.
apply
(
conv_compl
(
chain_map
authoritative
c
)
n
).
apply
(
conv_compl
(
chain_map
own
c
)
n
).
Qed
.
Canonical
Structure
authC
:
=
CofeT
auth_cofe_mixin
.
...
...
@@ -99,24 +99,24 @@ Proof. destruct x as [[]]; naive_solver eauto using cmra_validN_includedN. Qed.
Definition
auth_cmra_mixin
:
CMRAMixin
(
auth
A
).
Proof
.
split
.
*
by
intros
n
x
y1
y2
[
Hy
Hy'
]
;
split
;
simpl
;
rewrite
?Hy
?Hy'
.
*
by
intros
n
y1
y2
[
Hy
Hy'
]
;
split
;
simpl
;
rewrite
?Hy
?Hy'
.
*
intros
n
[
x
a
]
[
y
b
]
[
Hx
Ha
]
;
simpl
in
*
;
-
by
intros
n
x
y1
y2
[
Hy
Hy'
]
;
split
;
simpl
;
rewrite
?Hy
?Hy'
.
-
by
intros
n
y1
y2
[
Hy
Hy'
]
;
split
;
simpl
;
rewrite
?Hy
?Hy'
.
-
intros
n
[
x
a
]
[
y
b
]
[
Hx
Ha
]
;
simpl
in
*
;
destruct
Hx
;
intros
?
;
cofe_subst
;
auto
.
*
by
intros
n
x1
x2
[
Hx
Hx'
]
y1
y2
[
Hy
Hy'
]
;
-
by
intros
n
x1
x2
[
Hx
Hx'
]
y1
y2
[
Hy
Hy'
]
;
split
;
simpl
;
rewrite
?Hy
?Hy'
?Hx
?Hx'
.
*
intros
n
[[]
?]
?
;
naive_solver
eauto
using
cmra_includedN_S
,
cmra_validN_S
.
*
by
split
;
simpl
;
rewrite
assoc
.
*
by
split
;
simpl
;
rewrite
comm
.
*
by
split
;
simpl
;
rewrite
?cmra_unit_l
.
*
by
split
;
simpl
;
rewrite
?cmra_unit_idemp
.
*
intros
n
??
;
rewrite
!
auth_includedN
;
intros
[??].
-
intros
n
[[]
?]
?
;
naive_solver
eauto
using
cmra_includedN_S
,
cmra_validN_S
.
-
by
split
;
simpl
;
rewrite
assoc
.
-
by
split
;
simpl
;
rewrite
comm
.
-
by
split
;
simpl
;
rewrite
?cmra_unit_l
.
-
by
split
;
simpl
;
rewrite
?cmra_unit_idemp
.
-
intros
n
??
;
rewrite
!
auth_includedN
;
intros
[??].
by
split
;
simpl
;
apply
cmra_unit_preservingN
.
*
assert
(
∀
n
(
a
b1
b2
:
A
),
b1
⋅
b2
≼
{
n
}
a
→
b1
≼
{
n
}
a
).
-
assert
(
∀
n
(
a
b1
b2
:
A
),
b1
⋅
b2
≼
{
n
}
a
→
b1
≼
{
n
}
a
).
{
intros
n
a
b1
b2
<-
;
apply
cmra_includedN_l
.
}
intros
n
[[
a1
|
|]
b1
]
[[
a2
|
|]
b2
]
;
naive_solver
eauto
using
cmra_validN_op_l
,
cmra_validN_includedN
.
*
by
intros
n
??
;
rewrite
auth_includedN
;
-
by
intros
n
??
;
rewrite
auth_includedN
;
intros
[??]
;
split
;
simpl
;
apply
cmra_op_minus
.
Qed
.
Definition
auth_cmra_extend_mixin
:
CMRAExtendMixin
(
auth
A
).
...
...
@@ -150,9 +150,9 @@ Context `{Empty A, !CMRAIdentity A}.
Global
Instance
auth_cmra_identity
:
CMRAIdentity
authRA
.
Proof
.
split
;
simpl
.
*
by
apply
(@
cmra_empty_valid
A
_
).
*
by
intros
x
;
constructor
;
rewrite
/=
left_id
.
*
apply
_
.
-
by
apply
(@
cmra_empty_valid
A
_
).
-
by
intros
x
;
constructor
;
rewrite
/=
left_id
.
-
apply
_
.
Qed
.
Lemma
auth_frag_op
a
b
:
◯
(
a
⋅
b
)
≡
◯
a
⋅
◯
b
.
Proof
.
done
.
Qed
.
...
...
@@ -221,9 +221,9 @@ Instance auth_map_cmra_monotone {A B : cmraT} (f : A → B) :
CMRAMonotone
f
→
CMRAMonotone
(
auth_map
f
).
Proof
.
split
.
*
by
intros
n
[
x
a
]
[
y
b
]
;
rewrite
!
auth_includedN
/=
;
-
by
intros
n
[
x
a
]
[
y
b
]
;
rewrite
!
auth_includedN
/=
;
intros
[??]
;
split
;
simpl
;
apply
:
includedN_preserving
.
*
intros
n
[[
a
|
|]
b
]
;
rewrite
/=
/
cmra_validN
;
-
intros
n
[[
a
|
|]
b
]
;
rewrite
/=
/
cmra_validN
;
naive_solver
eauto
using
@
includedN_preserving
,
@
validN_preserving
.
Qed
.
Definition
authC_map
{
A
B
}
(
f
:
A
-
n
>
B
)
:
authC
A
-
n
>
authC
B
:
=
...
...
algebra/cmra.v
View file @
685148ab
...
...
@@ -243,8 +243,8 @@ Qed.
Global
Instance
cmra_includedN_preorder
n
:
PreOrder
(@
includedN
A
_
_
n
).
Proof
.
split
.
*
by
intros
x
;
exists
(
unit
x
)
;
rewrite
cmra_unit_r
.
*
intros
x
y
z
[
z1
Hy
]
[
z2
Hz
]
;
exists
(
z1
⋅
z2
).
-
by
intros
x
;
exists
(
unit
x
)
;
rewrite
cmra_unit_r
.
-
intros
x
y
z
[
z1
Hy
]
[
z2
Hz
]
;
exists
(
z1
⋅
z2
).
by
rewrite
assoc
-
Hy
-
Hz
.
Qed
.
Global
Instance
cmra_included_preorder
:
PreOrder
(@
included
A
_
_
).
...
...
@@ -349,8 +349,8 @@ Proof. split. by intros x y. intros x y y' ?? z ?; naive_solver. Qed.
Lemma
cmra_update_updateP
x
y
:
x
~~>
y
↔
x
~~>
:
(
y
=).
Proof
.
split
.
*
by
intros
Hx
z
?
;
exists
y
;
split
;
[
done
|
apply
(
Hx
z
)].
*
by
intros
Hx
z
n
?
;
destruct
(
Hx
z
n
)
as
(?&<-&?).
-
by
intros
Hx
z
?
;
exists
y
;
split
;
[
done
|
apply
(
Hx
z
)].
-
by
intros
Hx
z
n
?
;
destruct
(
Hx
z
n
)
as
(?&<-&?).
Qed
.
Lemma
cmra_updateP_id
(
P
:
A
→
Prop
)
x
:
P
x
→
x
~~>
:
P
.
Proof
.
by
intros
?
z
n
?
;
exists
x
.
Qed
.
...
...
@@ -402,8 +402,8 @@ Instance cmra_monotone_compose {A B C : cmraT} (f : A → B) (g : B → C) :
CMRAMonotone
f
→
CMRAMonotone
g
→
CMRAMonotone
(
g
∘
f
).
Proof
.
split
.
*
move
=>
n
x
y
Hxy
/=.
by
apply
includedN_preserving
,
includedN_preserving
.
*
move
=>
n
x
Hx
/=.
by
apply
validN_preserving
,
validN_preserving
.
-
move
=>
n
x
y
Hxy
/=.
by
apply
includedN_preserving
,
includedN_preserving
.
-
move
=>
n
x
Hx
/=.
by
apply
validN_preserving
,
validN_preserving
.
Qed
.
Section
cmra_monotone
.
...
...
@@ -527,20 +527,20 @@ Section prod.
Definition
prod_cmra_mixin
:
CMRAMixin
(
A
*
B
).
Proof
.
split
;
try
apply
_
.
*
by
intros
n
x
y1
y2
[
Hy1
Hy2
]
;
split
;
rewrite
/=
?Hy1
?Hy2
.
*
by
intros
n
y1
y2
[
Hy1
Hy2
]
;
split
;
rewrite
/=
?Hy1
?Hy2
.
*
by
intros
n
y1
y2
[
Hy1
Hy2
]
[??]
;
split
;
rewrite
/=
-
?Hy1
-
?Hy2
.
*
by
intros
n
x1
x2
[
Hx1
Hx2
]
y1
y2
[
Hy1
Hy2
]
;
-
by
intros
n
x
y1
y2
[
Hy1
Hy2
]
;
split
;
rewrite
/=
?Hy1
?Hy2
.
-
by
intros
n
y1
y2
[
Hy1
Hy2
]
;
split
;
rewrite
/=
?Hy1
?Hy2
.
-
by
intros
n
y1
y2
[
Hy1
Hy2
]
[??]
;
split
;
rewrite
/=
-
?Hy1
-
?Hy2
.
-
by
intros
n
x1
x2
[
Hx1
Hx2
]
y1
y2
[
Hy1
Hy2
]
;
split
;
rewrite
/=
?Hx1
?Hx2
?Hy1
?Hy2
.
*
by
intros
n
x
[??]
;
split
;
apply
cmra_validN_S
.
*
by
split
;
rewrite
/=
assoc
.
*
by
split
;
rewrite
/=
comm
.
*
by
split
;
rewrite
/=
cmra_unit_l
.
*
by
split
;
rewrite
/=
cmra_unit_idemp
.
*
intros
n
x
y
;
rewrite
!
prod_includedN
.
-
by
intros
n
x
[??]
;
split
;
apply
cmra_validN_S
.
-
by
split
;
rewrite
/=
assoc
.
-
by
split
;
rewrite
/=
comm
.
-
by
split
;
rewrite
/=
cmra_unit_l
.
-
by
split
;
rewrite
/=
cmra_unit_idemp
.
-
intros
n
x
y
;
rewrite
!
prod_includedN
.
by
intros
[??]
;
split
;
apply
cmra_unit_preservingN
.
*
intros
n
x
y
[??]
;
split
;
simpl
in
*
;
eauto
using
cmra_validN_op_l
.
*
intros
x
y
n
;
rewrite
prod_includedN
;
intros
[??].
-
intros
n
x
y
[??]
;
split
;
simpl
in
*
;
eauto
using
cmra_validN_op_l
.
-
intros
x
y
n
;
rewrite
prod_includedN
;
intros
[??].
by
split
;
apply
cmra_op_minus
.
Qed
.
Definition
prod_cmra_extend_mixin
:
CMRAExtendMixin
(
A
*
B
).
...
...
@@ -556,9 +556,9 @@ Section prod.
CMRAIdentity
A
→
CMRAIdentity
B
→
CMRAIdentity
prodRA
.
Proof
.
split
.
*
split
;
apply
cmra_empty_valid
.
*
by
split
;
rewrite
/=
left_id
.
*
by
intros
?
[??]
;
split
;
apply
(
timeless
_
).
-
split
;
apply
cmra_empty_valid
.
-
by
split
;
rewrite
/=
left_id
.
-
by
intros
?
[??]
;
split
;
apply
(
timeless
_
).
Qed
.
Lemma
prod_update
x
y
:
x
.
1
~~>
y
.
1
→
x
.
2
~~>
y
.
2
→
x
~~>
y
.
Proof
.
intros
??
z
n
[??]
;
split
;
simpl
in
*
;
auto
.
Qed
.
...
...
@@ -579,7 +579,7 @@ 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
).
Proof
.
split
.
*
intros
n
x
y
;
rewrite
!
prod_includedN
;
intros
[??]
;
simpl
.
-
intros
n
x
y
;
rewrite
!
prod_includedN
;
intros
[??]
;
simpl
.
by
split
;
apply
includedN_preserving
.
*
by
intros
n
x
[??]
;
split
;
simpl
;
apply
validN_preserving
.
-
by
intros
n
x
[??]
;
split
;
simpl
;
apply
validN_preserving
.
Qed
.
algebra/cmra_big_op.v
View file @
685148ab
...
...
@@ -21,9 +21,9 @@ Proof. done. Qed.
Global
Instance
big_op_permutation
:
Proper
((
≡
ₚ
)
==>
(
≡
))
big_op
.
Proof
.
induction
1
as
[|
x
xs1
xs2
?
IH
|
x
y
xs
|
xs1
xs2
xs3
]
;
simpl
;
auto
.
*
by
rewrite
IH
.
*
by
rewrite
!
assoc
(
comm
_
x
).
*
by
transitivity
(
big_op
xs2
).
-
by
rewrite
IH
.
-
by
rewrite
!
assoc
(
comm
_
x
).
-
by
transitivity
(
big_op
xs2
).
Qed
.
Global
Instance
big_op_proper
:
Proper
((
≡
)
==>
(
≡
))
big_op
.
Proof
.
by
induction
1
;
simpl
;
repeat
apply
(
_
:
Proper
(
_
==>
_
==>
_
)
op
).
Qed
.
...
...
@@ -35,10 +35,10 @@ Qed.
Lemma
big_op_contains
xs
ys
:
xs
`
contains
`
ys
→
big_op
xs
≼
big_op
ys
.
Proof
.
induction
1
as
[|
x
xs
ys
|
x
y
xs
|
x
xs
ys
|
xs
ys
zs
]
;
rewrite
//=.
*
by
apply
cmra_preserving_l
.
*
by
rewrite
!
assoc
(
comm
_
y
).
*
by
transitivity
(
big_op
ys
)
;
last
apply
cmra_included_r
.
*
by
transitivity
(
big_op
ys
).
-
by
apply
cmra_preserving_l
.
-
by
rewrite
!
assoc
(
comm
_
y
).
-
by
transitivity
(
big_op
ys
)
;
last
apply
cmra_included_r
.
-
by
transitivity
(
big_op
ys
).
Qed
.
Lemma
big_op_delete
xs
i
x
:
xs
!!
i
=
Some
x
→
x
⋅
big_op
(
delete
i
xs
)
≡
big_op
xs
.
...
...
algebra/cofe.v
View file @
685148ab
...
...
@@ -97,15 +97,15 @@ Section cofe.
Global
Instance
cofe_equivalence
:
Equivalence
((
≡
)
:
relation
A
).
Proof
.
split
.
*
by
intros
x
;
rewrite
equiv_dist
.
*
by
intros
x
y
;
rewrite
!
equiv_dist
.
*
by
intros
x
y
z
;
rewrite
!
equiv_dist
;
intros
;
transitivity
y
.
-
by
intros
x
;
rewrite
equiv_dist
.
-
by
intros
x
y
;
rewrite
!
equiv_dist
.
-
by
intros
x
y
z
;
rewrite
!
equiv_dist
;
intros
;
transitivity
y
.
Qed
.
Global
Instance
dist_ne
n
:
Proper
(
dist
n
==>
dist
n
==>
iff
)
(@
dist
A
_
n
).
Proof
.
intros
x1
x2
?
y1
y2
?
;
split
;
intros
.
*
by
transitivity
x1
;
[|
transitivity
y1
].
*
by
transitivity
x2
;
[|
transitivity
y2
].
-
by
transitivity
x1
;
[|
transitivity
y1
].
-
by
transitivity
x2
;
[|
transitivity
y2
].
Qed
.
Global
Instance
dist_proper
n
:
Proper
((
≡
)
==>
(
≡
)
==>
iff
)
(@
dist
A
_
n
).
Proof
.
...
...
@@ -158,8 +158,8 @@ Program Definition fixpoint_chain {A : cofeT} `{Inhabited A} (f : A → A)
`
{!
Contractive
f
}
:
chain
A
:
=
{|
chain_car
i
:
=
Nat
.
iter
(
S
i
)
f
inhabitant
|}.
Next
Obligation
.
intros
A
?
f
?
n
.
induction
n
as
[|
n
IH
]
;
intros
[|
i
]
?
;
simpl
;
try
omega
.
*
apply
(
contractive_0
f
).
*
apply
(
contractive_S
f
),
IH
;
auto
with
omega
.
-
apply
(
contractive_0
f
).
-
apply
(
contractive_S
f
),
IH
;
auto
with
omega
.
Qed
.
Program
Definition
fixpoint
{
A
:
cofeT
}
`
{
Inhabited
A
}
(
f
:
A
→
A
)
`
{!
Contractive
f
}
:
A
:
=
compl
(
fixpoint_chain
f
).
...
...
@@ -212,14 +212,14 @@ Section cofe_mor.
Definition
cofe_mor_cofe_mixin
:
CofeMixin
(
cofeMor
A
B
).
Proof
.
split
.
*
intros
f
g
;
split
;
[
intros
Hfg
n
k
;
apply
equiv_dist
,
Hfg
|].
-
intros
f
g
;
split
;
[
intros
Hfg
n
k
;
apply
equiv_dist
,
Hfg
|].
intros
Hfg
k
;
apply
equiv_dist
;
intros
n
;
apply
Hfg
.
*
intros
n
;
split
.
-
intros
n
;
split
.
+
by
intros
f
x
.
+
by
intros
f
g
?
x
.
+
by
intros
f
g
h
??
x
;
transitivity
(
g
x
).
*
by
intros
n
f
g
?
x
;
apply
dist_S
.
*
intros
c
n
x
;
simpl
.
-
by
intros
n
f
g
?
x
;
apply
dist_S
.
-
intros
c
n
x
;
simpl
.
by
rewrite
(
conv_compl
(
fun_chain
c
x
)
n
)
/=.
Qed
.
Canonical
Structure
cofe_mor
:
cofeT
:
=
CofeT
cofe_mor_cofe_mixin
.
...
...
@@ -274,11 +274,11 @@ Section product.
Definition
prod_cofe_mixin
:
CofeMixin
(
A
*
B
).
Proof
.
split
.
*
intros
x
y
;
unfold
dist
,
prod_dist
,
equiv
,
prod_equiv
,
prod_relation
.
-
intros
x
y
;
unfold
dist
,
prod_dist
,
equiv
,
prod_equiv
,
prod_relation
.
rewrite
!
equiv_dist
;
naive_solver
.
*
apply
_
.
*
by
intros
n
[
x1
y1
]
[
x2
y2
]
[??]
;
split
;
apply
dist_S
.
*
intros
c
n
;
split
.
apply
(
conv_compl
(
chain_map
fst
c
)
n
).
-
apply
_
.
-
by
intros
n
[
x1
y1
]
[
x2
y2
]
[??]
;
split
;
apply
dist_S
.
-
intros
c
n
;
split
.
apply
(
conv_compl
(
chain_map
fst
c
)
n
).
apply
(
conv_compl
(
chain_map
snd
c
)
n
).
Qed
.
Canonical
Structure
prodC
:
cofeT
:
=
CofeT
prod_cofe_mixin
.
...
...
@@ -308,10 +308,10 @@ Section discrete_cofe.
Definition
discrete_cofe_mixin
:
CofeMixin
A
.
Proof
.
split
.
*
intros
x
y
;
split
;
[
done
|
intros
Hn
;
apply
(
Hn
0
)].
*
done
.
*
done
.
*
intros
c
n
.
rewrite
/
compl
/
discrete_compl
/=.
-
intros
x
y
;
split
;
[
done
|
intros
Hn
;
apply
(
Hn
0
)].
-
done
.
-
done
.
-
intros
c
n
.
rewrite
/
compl
/
discrete_compl
/=.
symmetry
;
apply
(
chain_cauchy
c
0
(
S
n
))
;
omega
.
Qed
.
Definition
discreteC
:
cofeT
:
=
CofeT
discrete_cofe_mixin
.
...
...
@@ -347,14 +347,14 @@ Section later.
Definition
later_cofe_mixin
:
CofeMixin
(
later
A
).
Proof
.
split
.
*
intros
x
y
;
unfold
equiv
,
later_equiv
;
rewrite
!
equiv_dist
.
-
intros
x
y
;
unfold
equiv
,
later_equiv
;
rewrite
!
equiv_dist
.
split
.
intros
Hxy
[|
n
]
;
[
done
|
apply
Hxy
].
intros
Hxy
n
;
apply
(
Hxy
(
S
n
)).
*
intros
[|
n
]
;
[
by
split
|
split
]
;
unfold
dist
,
later_dist
.
-
intros
[|
n
]
;
[
by
split
|
split
]
;
unfold
dist
,
later_dist
.
+
by
intros
[
x
].
+
by
intros
[
x
]
[
y
].
+
by
intros
[
x
]
[
y
]
[
z
]
??
;
transitivity
y
.
*
intros
[|
n
]
[
x
]
[
y
]
?
;
[
done
|]
;
unfold
dist
,
later_dist
;
by
apply
dist_S
.
*
intros
c
[|
n
]
;
[
done
|
by
apply
(
conv_compl
(
later_chain
c
)
n
)].
-
intros
[|
n
]
[
x
]
[
y
]
?
;
[
done
|]
;
unfold
dist
,
later_dist
;
by
apply
dist_S
.
-
intros
c
[|
n
]
;
[
done
|
by
apply
(
conv_compl
(
later_chain
c
)
n
)].
Qed
.
Canonical
Structure
laterC
:
cofeT
:
=
CofeT
later_cofe_mixin
.
Global
Instance
Next_contractive
:
Contractive
(@
Next
A
).
...
...
algebra/cofe_solver.v
View file @
685148ab
...
...
@@ -43,8 +43,8 @@ Qed.
Lemma
fg
{
k
}
(
x
:
A
(
S
(
S
k
)))
:
f
(
S
k
)
(
g
(
S
k
)
x
)
≡
{
k
}
≡
x
.
Proof
.
induction
k
as
[|
k
IH
]
;
simpl
.
*
rewrite
f_S
g_S
-{
2
}(
map_id
_
_
x
)
-
map_comp
.
apply
(
contractive_0
map
).
*
rewrite
f_S
g_S
-{
2
}(
map_id
_
_
x
)
-
map_comp
.
by
apply
(
contractive_S
map
).
-
rewrite
f_S
g_S
-{
2
}(
map_id
_
_
x
)
-
map_comp
.
apply
(
contractive_0
map
).
-
rewrite
f_S
g_S
-{
2
}(
map_id
_
_
x
)
-
map_comp
.
by
apply
(
contractive_S
map
).
Qed
.
Record
tower
:
=
{
...
...
@@ -66,15 +66,15 @@ Qed.
Definition
tower_cofe_mixin
:
CofeMixin
tower
.
Proof
.
split
.
*
intros
X
Y
;
split
;
[
by
intros
HXY
n
k
;
apply
equiv_dist
|].
-
intros
X
Y
;
split
;
[
by
intros
HXY
n
k
;
apply
equiv_dist
|].
intros
HXY
k
;
apply
equiv_dist
;
intros
n
;
apply
HXY
.
*
intros
k
;
split
.
-
intros
k
;
split
.
+
by
intros
X
n
.
+
by
intros
X
Y
?
n
.
+
by
intros
X
Y
Z
??
n
;
transitivity
(
Y
n
).
*
intros
k
X
Y
HXY
n
;
apply
dist_S
.
-
intros
k
X
Y
HXY
n
;
apply
dist_S
.
by
rewrite
-(
g_tower
X
)
(
HXY
(
S
n
))
g_tower
.
*
intros
c
n
k
;
rewrite
/=
(
conv_compl
(
tower_chain
c
k
)
n
).
-
intros
c
n
k
;
rewrite
/=
(
conv_compl
(
tower_chain
c
k
)
n
).
apply
(
chain_cauchy
c
)
;
lia
.
Qed
.
Definition
T
:
cofeT
:
=
CofeT
tower_cofe_mixin
.
...
...
@@ -136,12 +136,12 @@ Lemma g_embed_coerce {k i} (x : A k) :
g
i
(
embed_coerce
(
S
i
)
x
)
≡
embed_coerce
i
x
.
Proof
.
unfold
embed_coerce
;
destruct
(
le_lt_dec
(
S
i
)
k
),
(
le_lt_dec
i
k
)
;
simpl
.
*
symmetry
;
by
erewrite
(@
gg_gg
_
_
1
(
k
-
S
i
))
;
simpl
.
*
exfalso
;
lia
.
*
assert
(
i
=
k
)
by
lia
;
subst
.
-
symmetry
;
by
erewrite
(@
gg_gg
_
_
1
(
k
-
S
i
))
;
simpl
.
-
exfalso
;
lia
.
-
assert
(
i
=
k
)
by
lia
;
subst
.
rewrite
(
ff_ff
_
(
eq_refl
(
1
+
(
0
+
k
))))
/=
gf
.
by
rewrite
(
gg_gg
_
(
eq_refl
(
0
+
(
0
+
k
)))).
*
assert
(
H
:
1
+
((
i
-
k
)
+
k
)
=
S
i
)
by
lia
.
-
assert
(
H
:
1
+
((
i
-
k
)
+
k
)
=
S
i
)
by
lia
.
rewrite
(
ff_ff
_
H
)
/=
-{
2
}(
gf
(
ff
(
i
-
k
)
x
))
g_coerce
.
by
erewrite
coerce_proper
by
done
.
Qed
.
...
...
@@ -156,22 +156,22 @@ Lemma embed_f k (x : A k) : embed (S k) (f k x) ≡ embed k x.
Proof
.
rewrite
equiv_dist
=>
n
i
;
rewrite
/
embed
/=
/
embed_coerce
.
destruct
(
le_lt_dec
i
(
S
k
)),
(
le_lt_dec
i
k
)
;
simpl
.
*
assert
(
H
:
S
k
=
S
(
k
-
i
)
+
(
0
+
i
))
by
lia
;
rewrite
(
gg_gg
_
H
)
/=.
-
assert
(
H
:
S
k
=
S
(
k
-
i
)
+
(
0
+
i
))
by
lia
;
rewrite
(
gg_gg
_
H
)
/=.
by
erewrite
g_coerce
,
gf
,
coerce_proper
by
done
.
*
assert
(
S
k
=
0
+
(
0
+
i
))
as
H
by
lia
.
-
assert
(
S
k
=
0
+
(
0
+
i
))
as
H
by
lia
.
rewrite
(
gg_gg
_
H
)
;
simplify_equality'
.
by
rewrite
(
ff_ff
_
(
eq_refl
(
1
+
(
0
+
k
)))).
*
exfalso
;
lia
.
*
assert
(
H
:
(
i
-
S
k
)
+
(
1
+
k
)
=
i
)
by
lia
;
rewrite
(
ff_ff
_
H
)
/=.
-
exfalso
;
lia
.
-
assert
(
H
:
(
i
-
S
k
)
+
(
1
+
k
)
=
i
)
by
lia
;
rewrite
(
ff_ff
_
H
)
/=.
by
erewrite
coerce_proper
by
done
.
Qed
.
Lemma
embed_tower
k
(
X
:
T
)
:
embed
(
S
k
)
(
X
(
S
k
))
≡
{
k
}
≡
X
.
Proof
.
intros
i
;
rewrite
/=
/
embed_coerce
.
destruct
(
le_lt_dec
i
(
S
k
))
as
[
H
|
H
]
;
simpl
.
*
rewrite
-(
gg_tower
i
(
S
k
-
i
)
X
).
-
rewrite
-(
gg_tower
i
(
S
k
-
i
)
X
).
apply
(
_
:
Proper
(
_
==>
_
)
(
gg
_
))
;
by
destruct
(
eq_sym
_
).
*
rewrite
(
ff_tower
k
(
i
-
S
k
)
X
).
by
destruct
(
Nat
.
sub_add
_
_
_
).
-
rewrite
(
ff_tower
k
(
i
-
S
k
)
X
).
by
destruct
(
Nat
.
sub_add
_
_
_
).
Qed
.
Program
Definition
unfold_chain
(
X
:
T
)
:
chain
(
F
T
T
)
:
=
...
...
@@ -206,7 +206,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
)).
*
move
=>
X
/=.
-
move
=>
X
/=.
rewrite
equiv_dist
;
intros
n
k
;
unfold
unfold
,
fold
;
simpl
.
rewrite
-
g_tower
-(
gg_tower
_
n
)
;
apply
(
_
:
Proper
(
_
==>
_
)
(
g
_
)).
transitivity
(
map
(
ff
n
,
gg
n
)
(
X
(
S
(
n
+
k
)))).
...
...
@@ -228,7 +228,7 @@ Proof.
assert
(
H
:
S
n
+
k
=
n
+
S
k
)
by
lia
.
rewrite
(
map_ff_gg
_
_
_
H
).
apply
(
_
:
Proper
(
_
==>
_
)
(
gg
_
))
;
by
destruct
H
.
*
intros
X
;
rewrite
equiv_dist
=>
n
/=.
-
intros
X
;
rewrite
equiv_dist
=>
n
/=.
rewrite
/
unfold
/=
(
conv_compl
(
unfold_chain
(
fold
X
))
n
)
/=.
rewrite
g_S
-!
map_comp
-{
2
}(
map_id
_
_
X
).
apply
(
contractive_ne
map
)
;
split
=>
Y
/=.
...
...
algebra/dra.v
View file @
685148ab
...
...
@@ -57,9 +57,9 @@ Instance validity_equiv : Equiv T := λ x y,
Instance
validity_equivalence
:
Equivalence
((
≡
)
:
relation
T
).
Proof
.
split
;
unfold
equiv
,
validity_equiv
.
*
by
intros
[
x
px
?]
;
simpl
.
*
intros
[
x
px
?]
[
y
py
?]
;
naive_solver
.
*
intros
[
x
px
?]
[
y
py
?]
[
z
pz
?]
[?
Hxy
]
[?
Hyz
]
;
simpl
in
*.
-
by
intros
[
x
px
?]
;
simpl
.
-
intros
[
x
px
?]
[
y
py
?]
;
naive_solver
.
-
intros
[
x
px
?]
[
y
py
?]
[
z
pz
?]
[?
Hxy
]
[?
Hyz
]
;
simpl
in
*.
split
;
[|
intros
;
transitivity
y
]
;
tauto
.
Qed
.
Instance
dra_valid_proper'
:
Proper
((
≡
)
==>
iff
)
(
valid
:
A
→
Prop
).
...
...
@@ -69,8 +69,8 @@ Proof. by intros x1 x2 Hx; split; rewrite /= Hx. Qed.
Instance
:
Proper
((
≡
)
==>
(
≡
)
==>
iff
)
(
⊥
).
Proof
.
intros
x1
x2
Hx
y1
y2
Hy
;
split
.
*
by
rewrite
Hy
(
symmetry_iff
(
⊥
)
x1
)
(
symmetry_iff
(
⊥
)
x2
)
Hx
.
*
by
rewrite
-
Hy
(
symmetry_iff
(
⊥
)
x2
)
(
symmetry_iff
(
⊥
)
x1
)
-
Hx
.
-
by
rewrite
Hy
(
symmetry_iff
(
⊥
)
x1
)
(
symmetry_iff
(
⊥
)
x2
)
Hx
.
-
by
rewrite
-
Hy
(
symmetry_iff
(
⊥
)
x2
)
(
symmetry_iff
(
⊥
)
x1
)
-
Hx
.
Qed
.
Lemma
dra_disjoint_rl
x
y
z
:
✓
x
→
✓
y
→
✓
z
→
y
⊥
z
→
x
⊥
y
⋅
z
→
x
⊥
y
.
Proof
.
intros
???.
rewrite
!(
symmetry_iff
_
x
).
by
apply
dra_disjoint_ll
.
Qed
.
...
...
@@ -103,31 +103,31 @@ Solve Obligations with naive_solver auto using dra_minus_valid.
Definition
validity_ra
:
RA
(
discreteC
T
).
Proof
.
split
.
*
intros
???
[?
Heq
]
;
split
;
simpl
;
[|
by
intros
(?&?&?)
;
rewrite
Heq
].
-
intros
???
[?
Heq
]
;
split
;
simpl
;
[|
by
intros
(?&?&?)
;
rewrite
Heq
].
split
;
intros
(?&?&?)
;
split_ands'
;
first
[
rewrite
?Heq
;
tauto
|
rewrite
-
?Heq
;
tauto
|
tauto
].
*
by
intros
??
[?
Heq
]
;
split
;
[
done
|]
;
simpl
;
intros
?
;
rewrite
Heq
.
*
intros
??
[??]
;
naive_solver
.
*
intros
x1
x2
[?
Hx
]
y1
y2
[?
Hy
]
;
-
by
intros
??
[?
Heq
]
;
split
;
[
done
|]
;
simpl
;
intros
?
;
rewrite
Heq
.
-
intros
??
[??]
;
naive_solver
.
-
intros
x1
x2
[?
Hx
]
y1
y2
[?
Hy
]
;
split
;
simpl
;
[|
by
intros
(?&?&?)
;
rewrite
Hx
//
Hy
].
split
;
intros
(?&?&
z
&?&?)
;
split_ands'
;
try
tauto
.
+
exists
z
.
by
rewrite
-
Hy
//
-
Hx
.
+
exists
z
.
by
rewrite
Hx
?Hy
;
tauto
.
*
intros
[
x
px
?]
[
y
py
?]
[
z
pz
?]
;
split
;
simpl
;
-
intros
[
x
px
?]
[
y
py
?]
[
z
pz
?]
;
split
;
simpl
;
[
intuition
eauto
2
using
dra_disjoint_lr
,
dra_disjoint_rl
|
by
intros
;
rewrite
assoc
].
*
intros
[
x
px
?]
[
y
py
?]
;
split
;
naive_solver
eauto
using
dra_comm
.
*
intros
[
x
px
?]
;
split
;
-
intros
[
x
px
?]
[
y
py
?]
;
split
;
naive_solver
eauto
using
dra_comm
.
-
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
px
?]
;
split
;
naive_solver
eauto
using
dra_unit_idemp
.