Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
10
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Open sidebar
Iris
Iris
Commits
45954c6f
Commit
45954c6f
authored
Oct 06, 2016
by
Robbert Krebbers
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
More properties about Some _ ≼ Some _.
These are very useful when dealing with the authoritative CMRA.
parent
143fbc52
Pipeline
#2775
passed with stage
in 9 minutes and 18 seconds
Changes
2
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
Showing
2 changed files
with
35 additions
and
24 deletions
+35
-24
algebra/cmra.v
algebra/cmra.v
+20
-1
algebra/gmap.v
algebra/gmap.v
+15
-23
No files found.
algebra/cmra.v
View file @
45954c6f
...
...
@@ -1208,8 +1208,14 @@ Section option.
Lemma
Some_included
x
y
:
Some
x
≼
Some
y
↔
x
≡
y
∨
x
≼
y
.
Proof
.
rewrite
option_included
;
naive_solver
.
Qed
.
Lemma
Some_included'
`
{
CMRATotal
A
}
x
y
:
Some
x
≼
Some
y
↔
x
≼
y
.
Lemma
Some_included_2
x
y
:
x
≼
y
→
Some
x
≼
Some
y
.
Proof
.
rewrite
Some_included
;
eauto
.
Qed
.
Lemma
Some_included_total
`
{
CMRATotal
A
}
x
y
:
Some
x
≼
Some
y
↔
x
≼
y
.
Proof
.
rewrite
Some_included
.
split
.
by
intros
[->|?].
eauto
.
Qed
.
Lemma
Some_included_exclusive
x
`
{!
Exclusive
x
}
y
:
Some
x
≼
Some
y
→
✓
y
→
x
≡
y
.
Proof
.
move
=>
/
Some_included
[//|/
exclusive_included
]
;
tauto
.
Qed
.
Lemma
is_Some_included
mx
my
:
mx
≼
my
→
is_Some
mx
→
is_Some
my
.
Proof
.
rewrite
-!
not_eq_None_Some
option_included
.
naive_solver
.
Qed
.
End
option
.
...
...
@@ -1217,6 +1223,19 @@ End option.
Arguments
optionR
:
clear
implicits
.
Arguments
optionUR
:
clear
implicits
.
Section
option_prod
.
Context
{
A
B
:
cmraT
}.
Lemma
Some_pair_included
(
x1
x2
:
A
)
(
y1
y2
:
B
)
:
Some
(
x1
,
y1
)
≼
Some
(
x2
,
y2
)
→
Some
x1
≼
Some
x2
∧
Some
y1
≼
Some
y2
.
Proof
.
rewrite
!
Some_included
.
intros
[[??]|[??]%
prod_included
]
;
eauto
.
Qed
.
Lemma
Some_pair_included_total_1
`
{
CMRATotal
A
}
(
x1
x2
:
A
)
(
y1
y2
:
B
)
:
Some
(
x1
,
y1
)
≼
Some
(
x2
,
y2
)
→
x1
≼
x2
∧
Some
y1
≼
Some
y2
.
Proof
.
intros
?%
Some_pair_included
.
by
rewrite
-(
Some_included_total
x1
).
Qed
.
Lemma
Some_pair_included_total_2
`
{
CMRATotal
B
}
(
x1
x2
:
A
)
(
y1
y2
:
B
)
:
Some
(
x1
,
y1
)
≼
Some
(
x2
,
y2
)
→
Some
x1
≼
Some
x2
∧
y1
≼
y2
.
Proof
.
intros
?%
Some_pair_included
.
by
rewrite
-(
Some_included_total
y1
).
Qed
.
End
option_prod
.
Instance
option_fmap_cmra_monotone
{
A
B
:
cmraT
}
(
f
:
A
→
B
)
`
{!
CMRAMonotone
f
}
:
CMRAMonotone
(
fmap
f
:
option
A
→
option
B
).
Proof
.
...
...
algebra/gmap.v
View file @
45954c6f
...
...
@@ -256,37 +256,29 @@ Global Instance gmap_singleton_persistent i (x : A) :
Proof
.
intros
.
by
apply
persistent_total
,
core_singleton'
.
Qed
.
Lemma
singleton_includedN
n
m
i
x
:
{[
i
:
=
x
]}
≼
{
n
}
m
↔
∃
y
,
m
!!
i
≡
{
n
}
≡
Some
y
∧
(
x
≼
{
n
}
y
∨
x
≡
{
n
}
≡
y
)
.
{[
i
:
=
x
]}
≼
{
n
}
m
↔
∃
y
,
m
!!
i
≡
{
n
}
≡
Some
y
∧
Some
x
≼
{
n
}
Some
y
.
Proof
.
split
.
-
move
=>
[
m'
/(
_
i
)]
;
rewrite
lookup_op
lookup_singleton
.
case
(
m'
!!
i
)=>
[
y
|]=>
Hm
.
+
exists
(
x
⋅
y
)
;
eauto
using
cmra_includedN_l
.
+
exists
x
;
eauto
.
-
intros
(
y
&
Hi
&[[
z
?]|
->]).
+
exists
(<[
i
:
=
z
]>
m
)=>
j
;
destruct
(
decide
(
i
=
j
))
as
[->|].
*
rewrite
Hi
lookup_op
lookup_singleton
lookup_insert
.
by
constructor
.
*
by
rewrite
lookup_op
lookup_singleton_ne
//
lookup_insert_ne
//
left_id
.
+
exists
(
delete
i
m
)=>
j
;
destruct
(
decide
(
i
=
j
))
as
[->|].
*
by
rewrite
Hi
lookup_op
lookup_singleton
lookup_delete
.
*
by
rewrite
lookup_op
lookup_singleton_ne
//
lookup_delete_ne
//
left_id
.
-
move
=>
[
m'
/(
_
i
)]
;
rewrite
lookup_op
lookup_singleton
=>
Hi
.
exists
(
x
⋅
?
m'
!!
i
).
rewrite
-
Some_op_opM
.
split
.
done
.
apply
cmra_includedN_l
.
-
intros
(
y
&
Hi
&[
mz
Hy
]).
exists
(
partial_alter
(
λ
_
,
mz
)
i
m
).
intros
j
;
destruct
(
decide
(
i
=
j
))
as
[->|].
+
by
rewrite
lookup_op
lookup_singleton
lookup_partial_alter
Hi
.
+
by
rewrite
lookup_op
lookup_singleton_ne
//
lookup_partial_alter_ne
//
left_id
.
Qed
.
(* We do not have [x ≼ y ↔ ∀ n, x ≼{n} y], so we cannot use the previous lemma *)
Lemma
singleton_included
m
i
x
:
{[
i
:
=
x
]}
≼
m
↔
∃
y
,
m
!!
i
≡
Some
y
∧
(
x
≼
y
∨
x
≡
y
)
.
{[
i
:
=
x
]}
≼
m
↔
∃
y
,
m
!!
i
≡
Some
y
∧
Some
x
≼
Some
y
.
Proof
.
split
.
-
move
=>
[
m'
/(
_
i
)]
;
rewrite
lookup_op
lookup_singleton
.
case
(
m'
!!
i
)=>
[
y
|]=>
Hm
.
+
exists
(
x
⋅
y
)
;
eauto
using
cmra_included_l
.
+
exists
x
;
eauto
.
-
intros
(
y
&
Hi
&[[
z
?]|
->]).
+
exists
(<[
i
:
=
z
]>
m
)=>
j
;
destruct
(
decide
(
i
=
j
))
as
[->|].
*
rewrite
Hi
lookup_op
lookup_singleton
lookup_insert
.
by
constructor
.
*
by
rewrite
lookup_op
lookup_singleton_ne
//
lookup_insert_ne
//
left_id
.
+
exists
(
delete
i
m
)=>
j
;
destruct
(
decide
(
i
=
j
))
as
[->|].
*
by
rewrite
Hi
lookup_op
lookup_singleton
lookup_delete
.
*
by
rewrite
lookup_op
lookup_singleton_ne
//
lookup_delete_ne
//
left_id
.
exists
(
x
⋅
?
m'
!!
i
).
rewrite
-
Some_op_opM
.
split
.
done
.
apply
cmra_included_l
.
-
intros
(
y
&
Hi
&[
mz
Hy
]).
exists
(
partial_alter
(
λ
_
,
mz
)
i
m
).
intros
j
;
destruct
(
decide
(
i
=
j
))
as
[->|].
+
by
rewrite
lookup_op
lookup_singleton
lookup_partial_alter
Hi
.
+
by
rewrite
lookup_op
lookup_singleton_ne
//
lookup_partial_alter_ne
//
left_id
.
Qed
.
Lemma
insert_updateP
(
P
:
A
→
Prop
)
(
Q
:
gmap
K
A
→
Prop
)
m
i
x
:
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a 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