Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Jonas Kastberg
iris
Commits
4f90bb04
Commit
4f90bb04
authored
Feb 06, 2020
by
Robbert Krebbers
Browse files
Merge branch 'stronger_gen_proper_2' into 'master'
Make `big_op{L,M}_gen_proper_2` stronger See merge request
iris/iris!363
parents
952daeb9
39f0153e
Changes
1
Hide whitespace changes
Inline
Side-by-side
theories/algebra/big_op.v
View file @
4f90bb04
...
...
@@ -101,7 +101,8 @@ Section list.
Lemma
big_opL_unit
l
:
([^
o
list
]
k
↦
y
∈
l
,
monoid_unit
)
≡
(
monoid_unit
:
M
).
Proof
.
induction
l
;
rewrite
/=
?left_id
//.
Qed
.
Lemma
big_opL_gen_proper_2
(
R
:
relation
M
)
f
g
l1
l2
:
Lemma
big_opL_gen_proper_2
{
B
}
(
R
:
relation
M
)
f
(
g
:
nat
→
B
→
M
)
l1
(
l2
:
list
B
)
:
R
monoid_unit
monoid_unit
→
Proper
(
R
==>
R
==>
R
)
o
→
(
∀
k
,
...
...
@@ -207,28 +208,31 @@ Proof.
Qed
.
(** ** Big ops over finite maps *)
Lemma
big_opM_empty
`
{
Countable
K
}
{
B
}
(
f
:
K
→
B
→
M
)
:
([^
o
map
]
k
↦
x
∈
∅
,
f
k
x
)
=
monoid_unit
.
Proof
.
by
rewrite
big_opM_eq
/
big_opM_def
map_to_list_empty
.
Qed
.
Lemma
big_opM_insert
`
{
Countable
K
}
{
B
}
(
f
:
K
→
B
→
M
)
(
m
:
gmap
K
B
)
i
x
:
m
!!
i
=
None
→
([^
o
map
]
k
↦
y
∈
<[
i
:
=
x
]>
m
,
f
k
y
)
≡
f
i
x
`
o
`
[^
o
map
]
k
↦
y
∈
m
,
f
k
y
.
Proof
.
intros
?.
by
rewrite
big_opM_eq
/
big_opM_def
map_to_list_insert
.
Qed
.
Lemma
big_opM_delete
`
{
Countable
K
}
{
B
}
(
f
:
K
→
B
→
M
)
(
m
:
gmap
K
B
)
i
x
:
m
!!
i
=
Some
x
→
([^
o
map
]
k
↦
y
∈
m
,
f
k
y
)
≡
f
i
x
`
o
`
[^
o
map
]
k
↦
y
∈
delete
i
m
,
f
k
y
.
Proof
.
intros
.
rewrite
-
big_opM_insert
?lookup_delete
//.
by
rewrite
insert_delete
insert_id
.
Qed
.
Section
gmap
.
Context
`
{
Countable
K
}
{
A
:
Type
}.
Implicit
Types
m
:
gmap
K
A
.
Implicit
Types
f
g
:
K
→
A
→
M
.
Lemma
big_opM_empty
f
:
([^
o
map
]
k
↦
x
∈
∅
,
f
k
x
)
=
monoid_unit
.
Proof
.
by
rewrite
big_opM_eq
/
big_opM_def
map_to_list_empty
.
Qed
.
Lemma
big_opM_insert
f
m
i
x
:
m
!!
i
=
None
→
([^
o
map
]
k
↦
y
∈
<[
i
:
=
x
]>
m
,
f
k
y
)
≡
f
i
x
`
o
`
[^
o
map
]
k
↦
y
∈
m
,
f
k
y
.
Proof
.
intros
?.
by
rewrite
big_opM_eq
/
big_opM_def
map_to_list_insert
.
Qed
.
Lemma
big_opM_delete
f
m
i
x
:
m
!!
i
=
Some
x
→
([^
o
map
]
k
↦
y
∈
m
,
f
k
y
)
≡
f
i
x
`
o
`
[^
o
map
]
k
↦
y
∈
delete
i
m
,
f
k
y
.
Proof
.
intros
.
rewrite
-
big_opM_insert
?lookup_delete
//.
by
rewrite
insert_delete
insert_id
.
Qed
.
Lemma
big_opM_gen_proper_2
(
R
:
relation
M
)
f
g
m1
m2
:
Lemma
big_opM_gen_proper_2
{
B
}
(
R
:
relation
M
)
f
(
g
:
K
→
B
→
M
)
m1
(
m2
:
gmap
K
B
)
:
subrelation
(
≡
)
R
→
Equivalence
R
→
Proper
(
R
==>
R
==>
R
)
o
→
(
∀
k
,
...
...
Write
Preview
Supports
Markdown
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