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
Iris
stdpp
Commits
5b7d0bf6
Commit
5b7d0bf6
authored
May 30, 2022
by
Robbert Krebbers
Browse files
Merge branch 'robbert/preimage' into 'master'
Preimage function for finite maps. See merge request
!382
parents
411eb445
28af1927
Pipeline
#66695
passed with stage
in 12 minutes and 53 seconds
Changes
2
Pipelines
1
Hide whitespace changes
Inline
Sidebyside
CHANGELOG.md
View file @
5b7d0bf6
...
...
@@ 20,6 +20,7 @@ Coq 8.11 is no longer supported.
not rely on them.

Declare
`Hint Mode`
for
`FinSet A C`
so that
`C`
is input, and
`A`
is output
(i.e., inferred from
`C`
).

Add function
`map_preimage`
to compute the preimage of a finite map.
## std++ 1.7.0 (20220122)
...
...
theories/fin_maps.v
View file @
5b7d0bf6
...
...
@@ 168,6 +168,17 @@ Global Instance map_lookup_total `{!Lookup K A (M A), !Inhabited A} :
LookupTotal
K
A
(
M
A
)

20
:
=
λ
i
m
,
default
inhabitant
(
m
!!
i
).
Typeclasses
Opaque
map_lookup_total
.
(** Given a finite map [m] with keys [K] and values [A], the preimage
[map_preimage m] gives a finite map with keys [A] and values being sets of [K].
The type of [map_preimage] is very generic to support different map and set
implementations. A possible instance is [MKA:=gmap K A], [MASK:=gmap A (gset K)],
and [SK:=gset K]. *)
Definition
map_preimage
`
{
FinMapToList
K
A
MKA
,
Empty
MASK
,
PartialAlter
A
SK
MASK
,
Empty
SK
,
Singleton
K
SK
,
Union
SK
}
(
m
:
MKA
)
:
MASK
:
=
map_fold
(
λ
i
,
partial_alter
(
λ
mX
,
Some
$
{[
i
]}
∪
default
∅
mX
))
∅
m
.
Typeclasses
Opaque
map_preimage
.
(** * Theorems *)
Section
theorems
.
Context
`
{
FinMap
K
M
}.
...
...
@@ 3264,6 +3275,98 @@ Section kmap.
Proof
.
unfold
strict
.
by
rewrite
!
map_disjoint_subseteq
.
Qed
.
End
kmap
.
Section
preimage
.
(** We restrict the theory to finite sets with Leibniz equality, which is
sufficient for [gset], but not for [boolset] or [propset]. The result of the
preimage is a map of sets. To support general sets, we would need setoid
equality on sets, and thus setoid equality on maps. *)
Context
`
{
FinMap
K
MK
,
FinMap
A
MA
,
FinSet
K
SK
,
!
LeibnizEquiv
SK
}.
Local
Notation
map_preimage
:
=
(
map_preimage
(
K
:
=
K
)
(
A
:
=
A
)
(
MKA
:
=
MK
A
)
(
MASK
:
=
MA
SK
)
(
SK
:
=
SK
)).
Implicit
Types
m
:
MK
A
.
Lemma
map_preimage_empty
:
map_preimage
∅
=
∅
.
Proof
.
apply
map_fold_empty
.
Qed
.
Lemma
map_preimage_insert
m
i
x
:
m
!!
i
=
None
→
map_preimage
(<[
i
:
=
x
]>
m
)
=
partial_alter
(
λ
mX
,
Some
({[
i
]}
∪
default
∅
mX
))
x
(
map_preimage
m
).
Proof
.
intros
Hi
.
refine
(
map_fold_insert_L
_
_
i
x
m
_
Hi
).
intros
j1
j2
x1
x2
m'
?
_
_
.
destruct
(
decide
(
x1
=
x2
))
as
[>?].

rewrite
<!
partial_alter_compose
.
apply
partial_alter_ext
;
intros
?
_;
f_equal
/=.
set_solver
.

by
apply
partial_alter_commute
.
Qed
.
(** The [preimage] function never returns an empty set (we represent that case
via [None]). *)
Lemma
lookup_preimage_Some_non_empty
m
x
:
map_preimage
m
!!
x
≠
Some
∅
.
Proof
.
induction
m
as
[
i
x'
m
?
IH
]
using
map_ind
.
{
by
rewrite
map_preimage_empty
,
lookup_empty
.
}
rewrite
map_preimage_insert
by
done
.
destruct
(
decide
(
x
=
x'
))
as
[>].

rewrite
lookup_partial_alter
.
intros
[=].
set_solver
.

rewrite
lookup_partial_alter_ne
by
done
.
set_solver
.
Qed
.
Lemma
lookup_preimage_None_1
m
x
i
:
map_preimage
m
!!
x
=
None
→
m
!!
i
≠
Some
x
.
Proof
.
induction
m
as
[
i'
x'
m
?
IH
]
using
map_ind
;
[
by
rewrite
lookup_empty
].
rewrite
map_preimage_insert
by
done
.
destruct
(
decide
(
x
=
x'
))
as
[>].

by
rewrite
lookup_partial_alter
.

rewrite
lookup_partial_alter_ne
,
lookup_insert_Some
by
done
.
naive_solver
.
Qed
.
Lemma
lookup_preimage_Some_1
m
X
x
i
:
map_preimage
m
!!
x
=
Some
X
→
i
∈
X
↔
m
!!
i
=
Some
x
.
Proof
.
revert
X
.
induction
m
as
[
i'
x'
m
?
IH
]
using
map_ind
;
intros
X
.
{
by
rewrite
map_preimage_empty
,
lookup_empty
.
}
rewrite
map_preimage_insert
by
done
.
destruct
(
decide
(
x
=
x'
))
as
[>].

rewrite
lookup_partial_alter
.
intros
[=
<].
rewrite
elem_of_union
,
elem_of_singleton
,
lookup_insert_Some
.
destruct
(
map_preimage
m
!!
x'
)
as
[
X'
]
eqn
:
Hx'
;
simpl
.
+
rewrite
IH
by
done
.
naive_solver
.
+
apply
(
lookup_preimage_None_1
_
_
i
)
in
Hx'
.
set_solver
.

rewrite
lookup_partial_alter_ne
,
lookup_insert_Some
by
done
.
naive_solver
.
Qed
.
Lemma
lookup_preimage_None
m
x
:
map_preimage
m
!!
x
=
None
↔
∀
i
,
m
!!
i
≠
Some
x
.
Proof
.
split
;
[
by
eauto
using
lookup_preimage_None_1
].
intros
Hm
.
apply
eq_None_not_Some
;
intros
[
X
?].
destruct
(
set_choose_L
X
)
as
[
i
?].
{
intros
>.
by
eapply
lookup_preimage_Some_non_empty
.
}
by
eapply
(
Hm
i
),
lookup_preimage_Some_1
.
Qed
.
Lemma
lookup_preimage_Some
m
x
X
:
map_preimage
m
!!
x
=
Some
X
↔
X
≠
∅
∧
∀
i
,
i
∈
X
↔
m
!!
i
=
Some
x
.
Proof
.
split
.

intros
HxX
.
split
;
[
intros
>
;
by
eapply
lookup_preimage_Some_non_empty
].
intros
j
.
by
apply
lookup_preimage_Some_1
.

intros
[
HXne
HX
].
destruct
(
map_preimage
m
!!
x
)
as
[
X'
]
eqn
:
HX'
.
+
f_equal
;
apply
set_eq
;
intros
i
.
rewrite
HX
.
by
apply
lookup_preimage_Some_1
.
+
apply
set_choose_L
in
HXne
as
[
j
?].
apply
(
lookup_preimage_None_1
_
_
j
)
in
HX'
.
naive_solver
.
Qed
.
Lemma
lookup_total_preimage
m
x
i
:
i
∈
map_preimage
m
!!!
x
↔
m
!!
i
=
Some
x
.
Proof
.
rewrite
lookup_total_alt
.
destruct
(
map_preimage
m
!!
x
)
as
[
X
]
eqn
:
HX
.

by
apply
lookup_preimage_Some
.

rewrite
lookup_preimage_None
in
HX
.
set_solver
.
Qed
.
End
preimage
.
(** * Tactics *)
(** The tactic [decompose_map_disjoint] simplifies occurrences of [disjoint]
in the hypotheses that involve the empty map [∅], the union [(∪)] or insert
...
...
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