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
stdpp
Commits
c2e4e322
Commit
c2e4e322
authored
Feb 14, 2016
by
Robbert Krebbers
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Inserting into a fin_map twice.
parent
e19e8505
Changes
1
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
with
2 additions
and
0 deletions
+2
-0
theories/fin_maps.v
theories/fin_maps.v
+2
-0
No files found.
theories/fin_maps.v
View file @
c2e4e322
...
...
@@ -403,6 +403,8 @@ Lemma lookup_insert_rev {A} (m : M A) i x y : <[i:=x]>m !! i = Some y → x = y
Proof
.
rewrite
lookup_insert
.
congruence
.
Qed
.
Lemma
lookup_insert_ne
{
A
}
(
m
:
M
A
)
i
j
x
:
i
≠
j
→
<[
i
:
=
x
]>
m
!!
j
=
m
!!
j
.
Proof
.
unfold
insert
.
apply
lookup_partial_alter_ne
.
Qed
.
Lemma
insert_insert
{
A
}
(
m
:
M
A
)
i
x
y
:
<[
i
:
=
x
]>(<[
i
:
=
y
]>
m
)
=
<[
i
:
=
x
]>
m
.
Proof
.
unfold
insert
,
map_insert
.
by
rewrite
<-
partial_alter_compose
.
Qed
.
Lemma
insert_commute
{
A
}
(
m
:
M
A
)
i
j
x
y
:
i
≠
j
→
<[
i
:
=
x
]>(<[
j
:
=
y
]>
m
)
=
<[
j
:
=
y
]>(<[
i
:
=
x
]>
m
).
Proof
.
apply
partial_alter_commute
.
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