From mathcomp Require Import all_ssreflect.
From mathcomp Require Import finmap.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Open Scope fmap_scope.
Open Scope fset_scope.
General utility lemmas for finite maps
Section CheckAllFmap.
Variables (
V :
Type) (
I :
choiceType).
Variable P :
pred V.
Variable f : {
fmap I ->
V}.
Section AllFs.
Variable s : {
fset I}.
Check the predicate P on given domain elements in the map f.
Definition allfs :=
\
big[
andb/
true]
_(
i <-
s) (
if f.[?
i]
is Some v then P v else true).
Lemma allfsP :
reflect (
forall (
i :
I) (
h :
i \
in domf f),
i \
in s ->
P f.[
h])
allfs.
Proof.
apply: (
iffP idP);
last first.
rewrite /
allfs big_seq.
elim/
big_ind:
_ => //;
last first.
move =>
i Hs Hi.
case Hf: (
i \
in domf f);
last by rewrite not_fnd //
Hf.
rewrite (
in_fnd Hf).
exact:
Hi.
move =>
x y Hx Hy Hp.
by apply/
andP;
split; [
apply Hx|
apply Hy].
move =>
Hb i Hi Hs.
case Hp: (
P _) => //.
have Hip:
f.[?
i] =
Some f.[
Hi]
by apply:
in_fnd.
move:
Hb.
set B :
pred I :=
fun j =>
j ==
i.
rewrite /
allfs (
big_fsetID _ B) /=.
move/
andP => [
Ha Hb].
move:
Ha.
rewrite /
B /=.
suff Hsuff: [
fset x |
x in s &
x ==
i] = [
fset i].
by rewrite Hsuff big_seq_fset1 (
in_fnd Hi)
Hp.
apply/
fsetP =>
x.
rewrite inE in_fsetE /=
inE.
apply/
idP/
idP;
first by move/
andP;
case.
by move/
eqP =>->;
rewrite Hs;
apply/
andP.
Qed.
End AllFs.
Definition allf :=
allfs (
domf f).
Lemma allfP :
reflect (
forall (
i :
I) (
h :
i \
in domf f),
P f.[
h])
allf.
Proof.
End CheckAllFmap.
Section UpdateAllFmap.
Variables (
V :
Type) (
I :
choiceType).
Variable P :
pred V.
Variable f : {
fmap I ->
V}.
Variable s : {
fset I}.
Update function parameter for individual values.
Variable upd :
I ->
V ->
V.
Update values for given elements in map domain.
Definition updf' :=
\
big[(@
catf _ _)/[
fmap]]
_(
i <-
s)
(
if f.[?
i]
is Some v then [
fmap].[
i <-
upd i v]
else [
fmap]).
Lemma updf'
_update :
forall (
i :
I) (
h :
i \
in domf f),
i \
in domf updf' ->
updf'.[?
i] =
Some (
upd i f.[
h]).
Proof.
Lemma updf'
_domf :
forall i,
i \
in domf updf' ->
i \
in domf f.
Proof.
Lemma updf'
_s :
forall i,
i \
in domf updf' ->
i \
in s.
Proof.
rewrite /
updf'.
have ->: (\
big[
catf (
V:=
V)/[
fmap]]
_(
i0 <-
s)
match f.[?
i0]
with |
Some v => [
fmap].[
i0 <-
upd i0 v] |
None => [
fmap]
end) =
(\
big[
catf (
V:=
V)/[
fmap]]
_(
i0 <-
s |
i0 \
in s)
match f.[?
i0]
with |
Some v => [
fmap].[
i0 <-
upd i0 v] |
None => [
fmap]
end).
by rewrite big_seq.
elim/
big_rec:
_ => //.
move =>
i x Ht IH i0.
case Hi0: (
i0 \
in domf x);
first by move =>
Hi0';
apply:
IH.
move/
negP/
negP:
Hi0 =>
Hi0.
case Hi: (
i \
in domf f).
rewrite (
in_fnd Hi) /=.
rewrite fsetU0 /=.
rewrite in_fsetU.
case/
orP;
last by move =>
Hi0';
case/
negP:
Hi0.
rewrite in_fsetD.
move/
andP => [
Ha Ha'].
move:
Ha'.
rewrite in_fset1.
by move/
eqP =>->.
move/
negP/
negP:
Hi =>
Hi.
rewrite (
not_fnd Hi).
rewrite mem_catf.
case/
orP => //.
move =>
Hi0'.
exact:
IH.
Qed.
Update given domain elements while retaining original mapping for other elements.
Definition updf :=
f +
updf'.
Lemma domf_s_updf' :
forall i,
i \
in domf f -> (
i \
in enum_fset s) = (
i \
in domf updf').
Proof.
Lemma updf_update :
forall (
i :
I) (
h :
i \
in domf f),
i \
in s ->
updf.[?
i] =
Some (
upd i f.[
h]).
Proof.
move =>
i h Hi.
rewrite /
updf fnd_cat.
case:
ifP;
first by move =>
Hi';
apply:
updf'
_update.
move/
negP;
case.
by rewrite -
domf_s_updf'.
Qed.
Lemma updf_update' :
forall (
i :
I) (
h :
i \
in domf f),
i \
notin s ->
updf.[?
i] =
Some f.[
h].
Proof.
move =>
i h Hi.
rewrite /
updf.
rewrite fnd_cat.
case:
ifP;
first by move/
updf'
_s;
move/
negP:
Hi.
move/
negP/
negP.
rewrite -
domf_s_updf' // =>
Hs.
by rewrite in_fnd.
Qed.
Lemma updf_domf :
domf f =
domf updf.
Proof.
End UpdateAllFmap.