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
d42d844a
Commit
d42d844a
authored
Aug 26, 2019
by
Robbert Krebbers
Browse files
Options
Browse Files
Download
Plain Diff
Merge branch 'big_op2_swap' into 'master'
Add `big_sepL2_swap` See merge request
iris/iris!307
parents
b6b9d739
edfdba15
Pipeline
#19346
passed with stage
in 23 minutes and 42 seconds
Changes
1
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
with
15 additions
and
0 deletions
+15
-0
theories/bi/big_op.v
theories/bi/big_op.v
+15
-0
No files found.
theories/bi/big_op.v
View file @
d42d844a
...
...
@@ -1475,6 +1475,13 @@ Section list2.
auto
using
and_mono
,
laterN_intro
.
Qed
.
Lemma
big_sepL2_flip
Φ
l1
l2
:
([
∗
list
]
k
↦
y1
;
y2
∈
l2
;
l1
,
Φ
k
y2
y1
)
⊣
⊢
([
∗
list
]
k
↦
y1
;
y2
∈
l1
;
l2
,
Φ
k
y1
y2
).
Proof
.
revert
Φ
l2
.
induction
l1
as
[|
x1
l1
IH
]=>
Φ
-[|
x2
l2
]//=
;
simplify_eq
.
by
rewrite
IH
.
Qed
.
Global
Instance
big_sepL2_nil_timeless
`
{!
Timeless
(
emp
%
I
:
PROP
)}
Φ
:
Timeless
([
∗
list
]
k
↦
y1
;
y2
∈
[]
;
[],
Φ
k
y1
y2
).
Proof
.
simpl
;
apply
_
.
Qed
.
...
...
@@ -1541,6 +1548,14 @@ Section gmap2.
apply
big_sepM2_mono
.
eauto
.
Qed
.
Lemma
big_sepM2_flip
Φ
m1
m2
:
([
∗
map
]
k
↦
y1
;
y2
∈
m2
;
m1
,
Φ
k
y2
y1
)
⊣
⊢
([
∗
map
]
k
↦
y1
;
y2
∈
m1
;
m2
,
Φ
k
y1
y2
).
Proof
.
rewrite
/
big_sepM2
.
apply
and_proper
;
[
apply
pure_proper
;
naive_solver
|].
rewrite
-
map_zip_with_flip
map_zip_with_map_zip
big_sepM_fmap
.
apply
big_sepM_proper
.
by
intros
k
[
b
a
].
Qed
.
Global
Instance
big_sepM2_empty_timeless
`
{!
Timeless
(
emp
%
I
:
PROP
)}
Φ
:
Timeless
([
∗
map
]
k
↦
x1
;
x2
∈
∅
;
∅
,
Φ
k
x1
x2
).
Proof
.
rewrite
/
big_sepM2
map_zip_with_empty
.
apply
_
.
Qed
.
...
...
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