Commit 71214d32 authored by Robbert Krebbers's avatar Robbert Krebbers

Misc definitions/lemmas on finite maps/lists.

parent 2dc8dc84
......@@ -58,8 +58,11 @@ Instance map_delete `{PartialAlter K A M} : Delete K M :=
Instance map_singleton `{PartialAlter K A M, Empty M} :
Singleton (K * A) M := λ p, <[p.1:=p.2]> .
Definition map_of_list `{Insert K A M} `{Empty M} : list (K * A) M :=
Definition map_of_list `{Insert K A M, Empty M} : list (K * A) M :=
fold_right (λ p, <[p.1:=p.2]>) .
Definition map_of_collection `{Elements K C, Insert K A M, Empty M}
(f : K option A) (X : C) : M :=
map_of_list (omap (λ i, (i,) <$> f i) (elements X)).
Instance map_union_with `{Merge M} {A} : UnionWith A (M A) :=
λ f, merge (union_with f).
......@@ -539,7 +542,23 @@ Proof.
exists i x. rewrite <-elem_of_map_to_list, Hm. by left.
Qed.
(** * Induction principles *)
(** ** Properties of conversion from collections *)
Lemma lookup_map_of_collection {A} `{FinCollection K C}
(f : K option A) X i x :
map_of_collection f X !! i = Some x i X f i = Some x.
Proof.
assert (NoDup (fst <$> omap (λ i, (i,) <$> f i) (elements X))).
{ induction (NoDup_elements X) as [|i' l]; csimpl; [constructor|].
destruct (f i') as [x'|]; csimpl; auto; constructor; auto.
rewrite elem_of_list_fmap. setoid_rewrite elem_of_list_omap.
by intros (?&?&?&?&?); simplify_option_equality. }
unfold map_of_collection; rewrite <-elem_of_map_of_list by done.
rewrite elem_of_list_omap. setoid_rewrite elem_of_elements; split.
* intros (?&?&?); simplify_option_equality; eauto.
* intros [??]; exists i; simplify_option_equality; eauto.
Qed.
(** ** Induction principles *)
Lemma map_ind {A} (P : M A Prop) :
P ( i x m, m !! i = None P m P (<[i:=x]>m)) m, P m.
Proof.
......@@ -572,7 +591,7 @@ Proof.
* by apply lt_wf.
Qed.
(** ** Properties of the [map_forall] predicate *)
(** ** Properties of the [map_Forall] predicate *)
Section map_Forall.
Context {A} (P : K A Prop).
......
......@@ -141,6 +141,12 @@ Definition foldl {A B} (f : A → B → A) : A → list B → A :=
Instance list_ret: MRet list := λ A x, x :: @nil A.
Instance list_fmap : FMap list := λ A B f,
fix go (l : list A) := match l with [] => [] | x :: l => f x :: go l end.
Instance list_omap : OMap list := λ A B f,
fix go (l : list A) :=
match l with
| [] => []
| x :: l => match f x with Some y => y :: go l | None => go l end
end.
Instance list_bind : MBind list := λ A B f,
fix go (l : list A) := match l with [] => [] | x :: l => f x ++ go l end.
Instance list_join: MJoin list :=
......@@ -533,6 +539,15 @@ Proof.
Qed.
Lemma elem_of_list_lookup l x : x l i, l !! i = Some x.
Proof. firstorder eauto using elem_of_list_lookup_1, elem_of_list_lookup_2. Qed.
Lemma elem_of_list_omap {B} (f : A option B) l (y : B) :
y omap f l x, x l f x = Some y.
Proof.
split.
* induction l as [|x l]; csimpl; repeat case_match; inversion 1; subst;
setoid_rewrite elem_of_cons; naive_solver.
* intros (x&Hx&?). induction Hx; csimpl; repeat case_match;
simplify_equality; auto; constructor (by auto).
Qed.
(** ** Properties of the [NoDup] predicate *)
Lemma NoDup_nil : NoDup (@nil A) True.
......@@ -2067,6 +2082,11 @@ Section Forall2.
Implicit Types l : list A.
Implicit Types k : list B.
Lemma Forall2_true l k :
( x y, P x y) length l = length k Forall2 P l k.
Proof.
intro. revert k. induction l; intros [|??] ?; simplify_equality'; auto.
Qed.
Lemma Forall2_same_length l k :
Forall2 (λ _ _, True) l k length l = length k.
Proof.
......
......@@ -77,23 +77,20 @@ Proof.
apply NoDup_fst_map_to_list.
Qed.
Definition mapset_map_with {A B} (f: bool A B)
Definition mapset_map_with {A B} (f : bool A option B)
(X : mapset (M unit)) : M A M B :=
let (m) := X in merge (λ x y,
let (mX) := X in merge (λ x y,
match x, y with
| Some _, Some a => Some (f true a)
| None, Some a => Some (f false a)
| _, None => None
end) m.
| Some _, Some a => f true a | None, Some a => f false a | _, None => None
end) mX.
Definition mapset_dom_with {A} (f : A bool) (m : M A) : mapset (M unit) :=
Mapset $ merge (λ x _,
match x with
| Some a => if f a then Some () else None
| None => None
| Some a => if f a then Some () else None | None => None
end) m (@empty (M A) _).
Lemma lookup_mapset_map_with {A B} (f : bool A B) X m i :
mapset_map_with f X m !! i = f (bool_decide (i X)) <$> m !! i.
Lemma lookup_mapset_map_with {A B} (f : bool A option B) X m i :
mapset_map_with f X m !! i = m !! i = f (bool_decide (i X)).
Proof.
destruct X as [mX]. unfold mapset_map_with, elem_of, mapset_elem_of.
rewrite lookup_merge by done. simpl.
......@@ -107,13 +104,12 @@ Proof.
* destruct (Is_true_reflect (f a)); naive_solver.
* naive_solver.
Qed.
Instance mapset_dom {A} : Dom (M A) (mapset (M unit)) :=
mapset_dom_with (λ _, true).
Instance mapset_dom_spec: FinMapDom K M (mapset (M unit)).
Proof.
split; try apply _. intros. unfold dom, mapset_dom.
rewrite elem_of_mapset_dom_with. unfold is_Some. naive_solver.
split; try apply _. intros. unfold dom, mapset_dom, is_Some.
rewrite elem_of_mapset_dom_with; naive_solver.
Qed.
End mapset.
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment