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
Iris
stdpp
Commits
668baa2b
Commit
668baa2b
authored
Nov 29, 2018
by
Robbert Krebbers
Browse files
Function `map_seq` to turn a list into a finite map of consequentive elements.
parent
2cf0cd35
Changes
1
Hide whitespace changes
Inline
Sidebyside
theories/fin_maps.v
View file @
668baa2b
...
...
@@ 137,6 +137,12 @@ Definition map_fold `{FinMapToList K A M} {B}
Instance
map_filter
`
{
FinMapToList
K
A
M
,
Insert
K
A
M
,
Empty
M
}
:
Filter
(
K
*
A
)
M
:
=
λ
P
_
,
map_fold
(
λ
k
v
m
,
if
decide
(
P
(
k
,
v
))
then
<[
k
:
=
v
]>
m
else
m
)
∅
.
Fixpoint
map_seq
`
{
Insert
nat
A
M
,
Empty
M
}
(
start
:
nat
)
(
xs
:
list
A
)
:
M
:
=
match
xs
with

[]
=>
∅

x
::
xs
=>
<[
start
:
=
x
]>
(
map_seq
(
S
start
)
xs
)
end
.
(** * Theorems *)
Section
theorems
.
Context
`
{
FinMap
K
M
}.
...
...
@@ 1911,6 +1917,82 @@ Proof.
Qed
.
End
theorems
.
(** ** The seq operation *)
Section
map_seq
.
Context
`
{
FinMap
nat
M
}
{
A
:
Type
}.
Implicit
Types
x
:
A
.
Implicit
Types
xs
:
list
A
.
Lemma
lookup_map_seq_Some_inv
start
xs
i
x
:
xs
!!
i
=
Some
x
↔
map_seq
(
M
:
=
M
A
)
start
xs
!!
(
start
+
i
)
=
Some
x
.
Proof
.
revert
start
i
.
induction
xs
as
[
x'
xs
IH
]
;
intros
start
i
;
simpl
.
{
by
rewrite
lookup_empty
,
lookup_nil
.
}
destruct
i
as
[
i
]
;
simpl
.
{
by
rewrite
Nat
.
add_0_r
,
lookup_insert
.
}
rewrite
lookup_insert_ne
by
lia
.
by
rewrite
(
IH
(
S
start
)),
Nat
.
add_succ_r
.
Qed
.
Lemma
lookup_map_seq_Some
start
xs
i
x
:
map_seq
(
M
:
=
M
A
)
start
xs
!!
i
=
Some
x
↔
start
≤
i
∧
xs
!!
(
i

start
)
=
Some
x
.
Proof
.
destruct
(
decide
(
start
≤
i
))
as
[
Hsi
].
{
rewrite
(
lookup_map_seq_Some_inv
start
).
replace
(
start
+
(
i

start
))
with
i
by
lia
.
naive_solver
.
}
split
;
[
naive_solver
].
intros
Hi
;
destruct
Hsi
.
revert
start
i
Hi
.
induction
xs
as
[
x'
xs
IH
]
;
intros
start
i
;
simpl
.
{
by
rewrite
lookup_empty
.
}
rewrite
lookup_insert_Some
;
intros
[[>
>][?
?%
IH
]]
;
lia
.
Qed
.
Lemma
lookup_map_seq_None
start
xs
i
:
map_seq
(
M
:
=
M
A
)
start
xs
!!
i
=
None
↔
i
<
start
∨
start
+
length
xs
≤
i
.
Proof
.
trans
(
¬
start
≤
i
∨
¬
is_Some
(
xs
!!
(
i

start
))).

rewrite
eq_None_not_Some
,
<
not_and_l
.
unfold
is_Some
.
setoid_rewrite
lookup_map_seq_Some
.
naive_solver
.

rewrite
lookup_lt_is_Some
.
lia
.
Qed
.
Lemma
lookup_map_seq_0
xs
i
:
map_seq
(
M
:
=
M
A
)
0
xs
!!
i
=
xs
!!
i
.
Proof
.
apply
option_eq
;
intros
x
.
by
rewrite
(
lookup_map_seq_Some_inv
0
).
Qed
.
Lemma
map_seq_singleton
start
x
:
map_seq
(
M
:
=
M
A
)
start
[
x
]
=
{[
start
:
=
x
]}.
Proof
.
done
.
Qed
.
Lemma
map_seq_app_disjoint
start
xs1
xs2
:
map_seq
(
M
:
=
M
A
)
start
xs1
##
ₘ
map_seq
(
start
+
length
xs1
)
xs2
.
Proof
.
apply
map_disjoint_spec
;
intros
i
x1
x2
.
rewrite
!
lookup_map_seq_Some
.
intros
[??%
lookup_lt_Some
]
[??%
lookup_lt_Some
]
;
lia
.
Qed
.
Lemma
map_seq_app
start
xs1
xs2
:
map_seq
start
(
xs1
++
xs2
)
=@{
M
A
}
map_seq
start
xs1
∪
map_seq
(
start
+
length
xs1
)
xs2
.
Proof
.
revert
start
.
induction
xs1
as
[
x1
xs1
IH
]
;
intros
start
;
simpl
.

by
rewrite
(
left_id_L
_
_
),
Nat
.
add_0_r
.

by
rewrite
IH
,
Nat
.
add_succ_r
,
!
insert_union_singleton_l
,
(
assoc_L
_
).
Qed
.
Lemma
map_seq_cons_disjoint
start
xs
x
:
map_seq
(
M
:
=
M
A
)
(
S
start
)
xs
!!
start
=
None
.
Proof
.
rewrite
lookup_map_seq_None
.
lia
.
Qed
.
Lemma
map_seq_cons
start
xs
x
:
map_seq
start
(
x
::
xs
)
=@{
M
A
}
<[
start
:
=
x
]>
(
map_seq
(
S
start
)
xs
).
Proof
.
done
.
Qed
.
Lemma
map_seq_snoc_disjoint
start
xs
x
:
map_seq
(
M
:
=
M
A
)
start
xs
!!
(
start
+
length
xs
)
=
None
.
Proof
.
rewrite
lookup_map_seq_None
.
lia
.
Qed
.
Lemma
map_seq_snoc
start
xs
x
:
map_seq
start
(
xs
++
[
x
])
=@{
M
A
}
<[
start
+
length
xs
:
=
x
]>
(
map_seq
start
xs
).
Proof
.
rewrite
map_seq_app
,
map_seq_singleton
.
by
rewrite
insert_union_singleton_r
by
(
by
rewrite
map_seq_snoc_disjoint
).
Qed
.
End
map_seq
.
(** * Tactics *)
(** The tactic [decompose_map_disjoint] simplifies occurrences of [disjoint]
in the hypotheses that involve the empty map [∅], the union [(∪)] or insert
...
...
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