Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Dan Frumin
iriscoq
Commits
764f0e4b
Commit
764f0e4b
authored
Nov 18, 2015
by
Robbert Krebbers
Browse files
Big ops on RAs.
parent
dd061dcf
Changes
1
Hide whitespace changes
Inline
Sidebyside
iris/ra.v
View file @
764f0e4b
Require
Export
prelude
.
collections
prelude
.
relations
.
Require
Export
prelude
.
collections
prelude
.
relations
prelude
.
fin_maps
.
Class
Valid
(
A
:
Type
)
:=
valid
:
A
→
Prop
.
Instance:
Params
(
@
valid
)
2.
...
...
@@ 11,6 +11,14 @@ Instance: Params (@op) 2.
Infix
"⋅"
:=
op
(
at
level
50
,
left
associativity
)
:
C_scope
.
Notation
"(⋅)"
:=
op
(
only
parsing
)
:
C_scope
.
Fixpoint
big_op
`
{
Op
A
,
Empty
A
}
(
xs
:
list
A
)
:
A
:=
match
xs
with
[]
=>
∅

x
::
xs
=>
x
⋅
big_op
xs
end
.
Arguments
big_op
_
_
_
!
_
/
.
Instance:
Params
(
@
big_op
)
3.
Definition
big_opM
`
{
FinMapToList
K
A
M
,
Op
A
,
Empty
A
}
(
m
:
M
)
:
A
:=
big_op
(
snd
<
$
>
map_to_list
m
).
Instance:
Params
(
@
big_opM
)
4.
Class
Included
(
A
:
Type
)
:=
included
:
relation
A
.
Instance:
Params
(
@
included
)
2.
Infix
"≼"
:=
included
(
at
level
70
)
:
C_scope
.
...
...
@@ 58,6 +66,7 @@ Instance: Params (@ra_update) 3.
Section
ra
.
Context
`
{
RA
A
}
.
Implicit
Types
x
y
z
:
A
.
Implicit
Types
xs
ys
zs
:
list
A
.
Global
Instance
ra_valid_proper
'
:
Proper
((
≡
)
==>
iff
)
valid
.
Proof
.
by
intros
???
;
split
;
apply
ra_valid_proper
.
Qed
.
...
...
@@ 120,4 +129,43 @@ Lemma ra_unit_empty x : unit ∅ ≡ ∅.
Proof
.
by
rewrite
<
(
ra_unit_l
∅
)
at
2
;
rewrite
(
right_id
_
_
).
Qed
.
Lemma
ra_empty_least
x
:
∅
≼
x
.
Proof
.
by
rewrite
ra_included_spec
;
exists
x
;
rewrite
(
left_id
_
_
).
Qed
.
(
**
*
Big
ops
*
)
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
!
(
associative
_
),
(
commutative
_
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
.
Lemma
big_op_app
xs
ys
:
big_op
(
xs
++
ys
)
≡
big_op
xs
⋅
big_op
ys
.
Proof
.
induction
xs
as
[

x
xs
IH
];
simpl
;
[
by
rewrite
?
(
left_id
_
_
)

].
by
rewrite
IH
,
(
associative
_
).
Qed
.
Context
`
{
FinMap
K
M
}
.
Lemma
big_opM_empty
:
big_opM
(
∅
:
M
A
)
≡
∅
.
Proof
.
unfold
big_opM
.
by
rewrite
map_to_list_empty
.
Qed
.
Lemma
big_opM_insert
(
m
:
M
A
)
i
x
:
m
!!
i
=
None
→
big_opM
(
<
[
i
:=
x
]
>
m
)
≡
x
⋅
big_opM
m
.
Proof
.
intros
?
;
unfold
big_opM
.
by
rewrite
map_to_list_insert
by
done
.
Qed
.
Lemma
big_opM_singleton
i
x
:
big_opM
(
{
[
i
,
x
]
}
:
M
A
)
≡
x
.
Proof
.
unfold
singleton
,
map_singleton
.
rewrite
big_opM_insert
by
auto
using
lookup_empty
;
simpl
.
by
rewrite
big_opM_empty
,
(
right_id
_
_
).
Qed
.
Global
Instance
big_opM_proper
:
Proper
((
≡
)
==>
(
≡
))
(
big_opM
:
M
A
→
_
).
Proof
.
intros
m1
;
induction
m1
as
[

i
x
m1
?
IH
]
using
map_ind
.
{
by
intros
m2
;
rewrite
(
symmetry_iff
(
≡
)),
map_equiv_empty
;
intros
>
.
}
intros
m2
Hm2
;
rewrite
big_opM_insert
by
done
.
rewrite
(
IH
(
delete
i
m2
))
by
(
by
rewrite
<
Hm2
,
delete_insert
).
destruct
(
map_equiv_lookup
(
<
[
i
:=
x
]
>
m1
)
m2
i
x
)
as
(
y
&?&
Hxy
);
auto
using
lookup_insert
.
by
rewrite
Hxy
,
<
big_opM_insert
,
insert_delete
by
auto
using
lookup_delete
.
Qed
.
End
ra
.
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