From 71214d32aa2dfa082540865a369c20fbff67d20a Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 10 Jul 2014 15:11:08 +0200
Subject: [PATCH] Misc definitions/lemmas on finite maps/lists.

---
 theories/fin_maps.v | 25 ++++++++++++++++++++++---
 theories/list.v     | 20 ++++++++++++++++++++
 theories/mapset.v   | 22 +++++++++-------------
 3 files changed, 51 insertions(+), 16 deletions(-)

diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index a8a59ee8..b66dcc14 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -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).
 
diff --git a/theories/list.v b/theories/list.v
index eb16a6bb..1853423c 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -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.
diff --git a/theories/mapset.v b/theories/mapset.v
index ab11a9f6..68442e1b 100644
--- a/theories/mapset.v
+++ b/theories/mapset.v
@@ -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.
 
-- 
GitLab