Remove optionmap and assoc.

These are unused and not very useful anymore now that we have gmap.

prelude/assoc.v

-(* Copyright (c) 2012-2015, Robbert Krebbers. *)
-(* This file is distributed under the terms of the BSD license. *)
-(** An implementation of finite maps and finite sets using association lists
-ordered by keys. Although the lookup and insert operation are linear-time, the
-main advantage of these association lists compared to search trees, is that it
-has canonical representatives and thus extensional Leibniz equality. Compared
-to a naive unordered association list, the merge operation (used for unions,
-intersections, and difference) is also linear-time. *)
-Require Import prelude.mapset.
-Require Export prelude.fin_maps.
-
-(** Because the association list is sorted using [strict lexico] instead of
-[lexico], it automatically guarantees that no duplicates exist. *)
-Definition assoc (K : Type) `{Lexico K, !TrichotomyT lexico,
-    !StrictOrder lexico} (A : Type) : Type :=
-  dsig (λ l : list (K * A), StronglySorted lexico (l.*1)).
-
-Section assoc.
-Context `{Lexico K, !StrictOrder lexico,
-  ∀ x y : K, Decision (x = y), !TrichotomyT lexico}.
-
-Infix "⊂" := lexico.
-Notation assoc_before j l := (Forall (lexico j) (l.*1)) (only parsing).
-Notation assoc_wf l := (StronglySorted (lexico) (l.*1)) (only parsing).
-
-Lemma assoc_before_transitive {A} (l : list (K * A)) i j :
-  i ⊂ j → assoc_before j l → assoc_before i l.
-Proof. intros. eapply Forall_impl; eauto. intros. by transitivity j. Qed.
-Hint Resolve assoc_before_transitive.
-
-Hint Extern 1 (StronglySorted _ []) => constructor.
-Hint Extern 1 (StronglySorted _ (_ :: _)) => constructor.
-Hint Extern 1 (Forall _ []) => constructor.
-Hint Extern 1 (Forall _ (_ :: _)) => constructor.
-Hint Extern 100 => progress simpl.
-
-Ltac simplify_assoc := intros;
-  repeat match goal with
-  | H : Forall _ [] |- _ => clear H
-  | H : Forall _ (_ :: _) |- _ => inversion_clear H
-  | H : StronglySorted _ [] |- _ => clear H
-  | H : StronglySorted _ (_ :: _) |- _ => inversion_clear H
-  | _ => progress decompose_elem_of_list
-  | _ => progress simplify_equality'
-  | _ => match goal with |- context [?o ≫= _] => by destruct o end
-  end;
-  repeat first
-  [ progress simplify_order
-  | progress autorewrite with assoc in *; simplify_equality'
-  | destruct (trichotomyT lexico) as [[?|?]|?]; simplify_equality' ];
-  eauto 9.
-
-Fixpoint assoc_lookup_raw {A} (i : K) (l : list (K * A)) : option A :=
-  match l with
-  | [] => None
-  | (j,x) :: l =>
-    match trichotomyT lexico i j with
-    | (**i i ⊂ j *) inleft (left _) => None
-    | (**i i = j *) inleft (right _) => Some x
-    | (**i j ⊂ i *) inright _ => assoc_lookup_raw i l
-    end
-  end.
-Global Instance assoc_lookup {A} : Lookup K A (assoc K A) := λ k m,
-  assoc_lookup_raw k (`m).
-
-Lemma assoc_lookup_before {A} (l : list (K * A)) i :
-  assoc_before i l → assoc_lookup_raw i l = None.
-Proof. induction l as [|[??]]; simplify_assoc. Qed.
-Hint Rewrite @assoc_lookup_before using (by eauto) : assoc.
-
-Lemma assoc_eq {A} (l1 l2 : list (K * A)) :
-  assoc_wf l1 → assoc_wf l2 →
-  (∀ i, assoc_lookup_raw i l1 = assoc_lookup_raw i l2) → l1 = l2.
-Proof.
-  revert l2. induction l1 as [|[i x] l1 IH]; intros [|[j y] l2]; intros ?? E.
-  { done. }
-  { specialize (E j); simplify_assoc; by repeat constructor. }
-  { specialize (E i); simplify_assoc; by repeat constructor. }
-  pose proof (E i); pose proof (E j); simplify_assoc.
-  f_equal. apply IH; auto. intros i'. specialize (E i'); simplify_assoc.
-Qed.
-Definition assoc_empty_wf {A} : assoc_wf (@nil (K * A)).
-Proof. constructor. Qed.
-Global Instance assoc_empty {A} : Empty (assoc K A) := dexist _ assoc_empty_wf.
-
-Definition assoc_cons {A} (i : K) (o : option A) (l : list (K * A)) :
-  list (K * A) := match o with None => l | Some z => (i,z) :: l end.
-Lemma assoc_cons_before {A} (l : list (K * A)) i j o :
-  assoc_before i l → i ⊂ j → assoc_before i (assoc_cons j o l).
-Proof. destruct o; simplify_assoc. Qed.
-Lemma assoc_cons_wf {A} (l : list (K * A)) i o :
-  assoc_wf l → assoc_before i l → assoc_wf (assoc_cons i o l).
-Proof. destruct o; simplify_assoc. Qed.
-Hint Resolve assoc_cons_before assoc_cons_wf.
-Lemma assoc_lookup_cons {A} (l : list (K * A)) i o :
-  assoc_before i l → assoc_lookup_raw i (assoc_cons i o l) = o.
-Proof. destruct o; simplify_assoc. Qed.
-Lemma assoc_lookup_cons_lt {A} (l : list (K * A)) i j o :
-  i ⊂ j → assoc_before i l → assoc_lookup_raw i (assoc_cons j o l) = None.
-Proof. destruct o; simplify_assoc. Qed.
-Lemma assoc_lookup_cons_gt {A} (l : list (K * A)) i j o :
-  j ⊂ i → assoc_lookup_raw i (assoc_cons j o l) = assoc_lookup_raw i l.
-Proof. destruct o; simplify_assoc. Qed.
-Hint Rewrite @assoc_lookup_cons @assoc_lookup_cons_lt
-  @assoc_lookup_cons_gt using (by eauto 8) : assoc.
-
-Fixpoint assoc_alter_raw {A} (f : option A → option A)
-    (i : K) (l : list (K * A)) : list (K * A) :=
-  match l with
-  | [] => assoc_cons i (f None) []
-  | (j,x) :: l =>
-    match trichotomyT lexico i j with
-    | (**i i ⊂ j *) inleft (left _) => assoc_cons i (f None) ((j,x) :: l)
-    | (**i i = j *) inleft (right _) => assoc_cons j (f (Some x)) l
-    | (**i j ⊂ i *) inright _ => (j,x) :: assoc_alter_raw f i l
-    end
-  end.
-Lemma assoc_alter_wf {A} (f : option A → option A) i l :
-  assoc_wf l → assoc_wf (assoc_alter_raw f i l).
-Proof.
-  revert l. assert (∀ j l,
-    j ⊂ i → assoc_before j l → assoc_before j (assoc_alter_raw f i l)).
-  { intros j l. induction l as [|[??]]; simplify_assoc. }
-  intros l. induction l as [|[??]]; simplify_assoc.
-Qed.
-Global Instance assoc_alter {A} : PartialAlter K A (assoc K A) := λ f i m,
-  dexist _ (assoc_alter_wf f i _ (proj2_dsig m)).
-
-Lemma assoc_lookup_raw_alter {A} f (l : list (K * A)) i :
-  assoc_wf l →
-  assoc_lookup_raw i (assoc_alter_raw f i l) = f (assoc_lookup_raw i l).
-Proof. induction l as [|[??]]; simplify_assoc. Qed.
-Lemma assoc_lookup_raw_alter_ne {A} f (l : list (K * A)) i j :
-  assoc_wf l → i ≠ j →
-  assoc_lookup_raw j (assoc_alter_raw f i l) = assoc_lookup_raw j l.
-Proof.
-  induction l as [|[??]]; simplify_assoc; unfold assoc_cons;
-    destruct (f _); simplify_assoc.
-Qed.
-Lemma assoc_fmap_wf {A B} (f : A → B) (l : list (K * A)) :
-  assoc_wf l → assoc_wf (prod_map id f <$> l).
-Proof.
-  intros. by rewrite <-list_fmap_compose,
-    (list_fmap_ext _ fst l l) by (done; by intros []).
-Qed.
-Global Program Instance assoc_fmap: FMap (assoc K) := λ A B f m,
-  dexist _ (assoc_fmap_wf f _ (proj2_dsig m)).
-Lemma assoc_lookup_fmap {A B} (f : A → B) (l : list (K * A)) i :
-  assoc_lookup_raw i (prod_map id f <$> l) = fmap f (assoc_lookup_raw i l).
-Proof. induction l as [|[??]]; simplify_assoc. Qed.
-
-Fixpoint assoc_omap_raw {A B} (f : A → option B)
-    (l : list (K * A)) : list (K * B) :=
-  match l with
-  | [] => []
-  | (i,x) :: l => assoc_cons i (f x) (assoc_omap_raw f l)
-  end.
-Lemma assoc_omap_raw_before {A B} (f : A → option B) l j :
-  assoc_before j l → assoc_before j (assoc_omap_raw f l).
-Proof. induction l as [|[??]]; simplify_assoc. Qed.
-Hint Resolve assoc_omap_raw_before.
-Lemma assoc_omap_wf {A B} (f : A → option B) l :
-  assoc_wf l → assoc_wf (assoc_omap_raw f l).
-Proof. induction l as [|[??]]; simplify_assoc. Qed.
-Hint Resolve assoc_omap_wf.
-Global Instance assoc_omap: OMap (assoc K) := λ A B f m,
-  dexist _ (assoc_omap_wf f _ (proj2_dsig m)).
-Lemma assoc_omap_spec {A B} (f : A → option B) l i :
-  assoc_wf l →
-  assoc_lookup_raw i (assoc_omap_raw f l) = assoc_lookup_raw i l ≫= f.
-Proof. intros. induction l as [|[??]]; simplify_assoc. Qed.
-Hint Rewrite @assoc_omap_spec using (by eauto) : assoc.
-
-Fixpoint assoc_merge_raw {A B C} (f : option A → option B → option C)
-    (l : list (K * A)) : list (K * B) → list (K * C) :=
-  fix go (k : list (K * B)) :=
-  match l, k with
-  | [], _ => assoc_omap_raw (f None ∘ Some) k
-  | _, [] => assoc_omap_raw (flip f None ∘ Some) l
-  | (i,x) :: l, (j,y) :: k =>
-    match trichotomyT lexico i j with
-    | (**i i ⊂ j *) inleft (left _) =>
-      assoc_cons i (f (Some x) None) (assoc_merge_raw f l ((j,y) :: k))
-    | (**i i = j *) inleft (right _) =>
-      assoc_cons i (f (Some x) (Some y)) (assoc_merge_raw f l k)
-    | (**i j ⊂ i *) inright _ =>
-      assoc_cons j (f None (Some y)) (go k)
-    end
-  end.
-Section assoc_merge_raw.
-  Context {A B C} (f : option A → option B → option C).
-  Lemma assoc_merge_nil_l k :
-    assoc_merge_raw f [] k = assoc_omap_raw (f None ∘ Some) k.
-  Proof. by destruct k. Qed.
-  Lemma assoc_merge_nil_r l :
-    assoc_merge_raw f l [] = assoc_omap_raw (flip f None ∘ Some) l.
-  Proof. by destruct l as [|[??]]. Qed.
-  Lemma assoc_merge_cons i x j y l k :
-    assoc_merge_raw f ((i,x) :: l) ((j,y) :: k) =
-      match trichotomyT lexico i j with
-      | (**i i ⊂ j *) inleft (left _) =>
-        assoc_cons i (f (Some x) None) (assoc_merge_raw f l ((j,y) :: k))
-      | (**i i = j *) inleft (right _) =>
-        assoc_cons i (f (Some x) (Some y)) (assoc_merge_raw f l k)
-      | (**i j ⊂ i *) inright _ =>
-        assoc_cons j (f None (Some y)) (assoc_merge_raw f ((i,x) :: l) k)
-      end.
-  Proof. done. Qed.
-End assoc_merge_raw.
-Arguments assoc_merge_raw _ _ _ _ _ _ : simpl never.
-Hint Rewrite @assoc_merge_nil_l @assoc_merge_nil_r @assoc_merge_cons : assoc.
-Lemma assoc_merge_before {A B C} (f : option A → option B → option C) l1 l2 j :
-  assoc_before j l1 → assoc_before j l2 →
-  assoc_before j (assoc_merge_raw f l1 l2).
-Proof.
-  revert l2. induction l1 as [|[??] l1 IH];
-    intros l2; induction l2 as [|[??] l2 IH2]; simplify_assoc.
-Qed.
-Hint Resolve assoc_merge_before.
-Lemma assoc_merge_wf {A B C} (f : option A → option B → option C) l1 l2 :
-  assoc_wf l1 → assoc_wf l2 → assoc_wf (assoc_merge_raw f l1 l2).
-Proof.
-  revert l2. induction l1 as [|[i x] l1 IH];
-    intros l2; induction l2 as [|[j y] l2 IH2]; simplify_assoc.
-Qed.
-Global Instance assoc_merge: Merge (assoc K) := λ A B C f m1 m2,
-  dexist _ (assoc_merge_wf f _ _ (proj2_dsig m1) (proj2_dsig m2)).
-Lemma assoc_merge_spec {A B C} (f : option A → option B → option C) l1 l2 i :
-  f None None = None → assoc_wf l1 → assoc_wf l2 →
-  assoc_lookup_raw i (assoc_merge_raw f l1 l2) =
-    f (assoc_lookup_raw i l1) (assoc_lookup_raw i l2).
-Proof.
-  intros ?. revert l2. induction l1 as [|[??] l1 IH]; intros l2;
-    induction l2 as [|[??] l2 IH2]; simplify_assoc; rewrite ?IH; simplify_assoc.
-Qed.
-
-Global Instance assoc_to_list {A} : FinMapToList K A (assoc K A) := proj1_sig.
-Lemma assoc_to_list_nodup {A} (l : list (K * A)) : assoc_wf l → NoDup l.
-Proof.
-  revert l. assert (∀ i x (l : list (K * A)), assoc_before i l → (i,x) ∉ l).
-  { intros i x l. rewrite Forall_fmap, Forall_forall. intros Hl Hi.
-    destruct (irreflexivity (lexico) i). by apply (Hl (i,x) Hi). }
-  induction l as [|[??]]; simplify_assoc; constructor; auto.
-Qed.
-Lemma assoc_to_list_elem_of {A} (l : list (K * A)) i x :
-  assoc_wf l → (i,x) ∈ l ↔ assoc_lookup_raw i l = Some x.
-Proof.
-  split.
-  * induction l as [|[??]]; simplify_assoc; naive_solver.
-  * induction l as [|[??]]; simplify_assoc; [left| right]; eauto.
-Qed.
-
-(** * Instantiation of the finite map interface *)
-Hint Extern 1 (assoc_wf _) => by apply (bool_decide_unpack _).
-Global Instance: FinMap K (assoc K).
-Proof.
-  split.
-  * intros ? [l1 ?] [l2 ?] ?. apply (sig_eq_pi _), assoc_eq; auto.
-  * done.
-  * intros ?? [??] ?. apply assoc_lookup_raw_alter; auto. 
-  * intros ?? [??] ???. apply assoc_lookup_raw_alter_ne; auto.
-  * intros ??? [??] ?. apply assoc_lookup_fmap.
-  * intros ? [??]. apply assoc_to_list_nodup; auto.
-  * intros ? [??] ??. apply assoc_to_list_elem_of; auto.
-  * intros ??? [??] ?. apply assoc_omap_spec; auto.
-  * intros ????? [??] [??] ?. apply assoc_merge_spec; auto.
-Qed.
-End assoc.
-
-(** * Finite sets *)
-(** We construct finite sets using the above implementation of maps. *)
-Notation assoc_set K := (mapset (assoc K)).
-Instance assoc_map_dom `{Lexico K, !TrichotomyT (@lexico K _),
-  !StrictOrder lexico} {A} : Dom (assoc K A) (assoc_set K) := mapset_dom.
-Instance assoc_map_dom_spec `{Lexico K} `{!TrichotomyT (@lexico K _)}
-    `{!StrictOrder lexico, ∀ x y : K, Decision (x = y)} :
-  FinMapDom K (assoc K) (assoc_set K) := mapset_dom_spec.

prelude/optionmap.v

-(* Copyright (c) 2012-2015, Robbert Krebbers. *)
-(* This file is distributed under the terms of the BSD license. *)
-Require Import prelude.mapset.
-Require Export prelude.prelude prelude.fin_maps.
-
-Record optionmap (M : Type → Type) (A : Type) : Type :=
-  OptionMap { optionmap_None : option A; optionmap_Some : M A }.
-Arguments optionmap_None {_ _} _.
-Arguments optionmap_Some {_ _} _.
-Arguments OptionMap {_ _} _ _.
-Instance optionmap_eq_dec {M : Type → Type} {A}
-    `{∀ x y : A, Decision (x = y), ∀ m1 m2 : M A, Decision (m1 = m2)}
-  (m1 m2 : optionmap M A) : Decision (m1 = m2).
-Proof. solve_decision. Defined.
-
-Section optionmap.
-Context `{FinMap K M}.
-
-Global Instance optionmap_empty {A} : Empty (optionmap M A) := OptionMap None ∅.
-Global Opaque optionmap_empty.
-Global Instance optionmap_lookup {A} :
-    Lookup (option K) A (optionmap M A) := λ i m,
-  match i with
-  | None => optionmap_None m
-  | Some k => optionmap_Some m !! k
-  end.
-Global Instance optionmap_partial_alter {A} :
-    PartialAlter (option K) A (optionmap M A) := λ f i m,
-  match i, m with
-  | None, OptionMap o m => OptionMap (f o) m
-  | Some k, OptionMap o m => OptionMap o (partial_alter f k m)
-  end.
-Global Instance optionmap_to_list {A} :
-    FinMapToList (option K) A (optionmap M A) := λ m,
-  match m with
-  | OptionMap o m =>
-     default [] o (λ x, [(None,x)]) ++ (prod_map Some id <$> map_to_list m)
-  end.
-Global Instance optionmap_omap: OMap (optionmap M) := λ A B f m,
-  match m with OptionMap o m => OptionMap (o ≫= f) (omap f m) end.
-Global Instance optionmap_merge: Merge (optionmap M) := λ A B C f m1 m2,
-  match m1, m2 with
-  | OptionMap o1 m1, OptionMap o2 m2 => OptionMap (f o1 o2) (merge f m1 m2)
-  end.
-Global Instance optionmap_fmap: FMap (optionmap M) := λ A B f m,
-  match m with OptionMap o m => OptionMap (f <$> o) (f <$> m) end.
-
-Global Instance: FinMap (option K) (optionmap M).
-Proof.
-  split.
-  * intros ? [??] [??] Hlookup. f_equal; [apply (Hlookup None)|].
-    apply map_eq. intros k. apply (Hlookup (Some k)).
-  * intros ? [?|]. apply (lookup_empty k). done.
-  * intros ? f [? t] [k|]; simpl; [|done]. apply lookup_partial_alter.
-  * intros ? f [? t] [k|] [|k']; simpl; try intuition congruence.
-    intros; apply lookup_partial_alter_ne; congruence.
-  * intros ??? [??] []; simpl. apply lookup_fmap. done.
-  * intros ? [[x|] m]; unfold map_to_list; simpl.
-    + constructor.
-      - rewrite elem_of_list_fmap. by intros [[??] [??]].
-      - by apply (NoDup_fmap _), NoDup_map_to_list.
-    + apply (NoDup_fmap _), NoDup_map_to_list.
-  * intros ? m k x. unfold map_to_list. split.
-    + destruct m as [[y|] m]; simpl.
-      - rewrite elem_of_cons, elem_of_list_fmap.
-        intros [? | [[??] [??]]]; simplify_equality'; [done |].
-        by apply elem_of_map_to_list.
-      - rewrite elem_of_list_fmap; intros [[??] [??]]; simplify_equality'.
-        by apply elem_of_map_to_list.
-    + destruct m as [[y|] m]; simpl.
-      - rewrite elem_of_cons, elem_of_list_fmap.
-        destruct k as [k|]; simpl; [|intuition congruence].
-        intros. right. exists (k,x). by rewrite elem_of_map_to_list.
-      - rewrite elem_of_list_fmap.
-        destruct k as [k|]; simpl; [|done].
-        intros. exists (k,x). by rewrite elem_of_map_to_list.
-  * intros ?? f [??] [?|]; simpl; [|done]; apply (lookup_omap f).
-  * intros ??? f ? [??] [??] [?|]; simpl; [|done]; apply (lookup_merge f).
-Qed.
-End optionmap.
-
-(** * Finite sets *)
-Notation optionset M := (mapset (optionmap M)).
-Instance optionmap_dom {M : Type → Type} `{∀ A, Empty (M A), Merge M} {A} :
-  Dom (optionmap M A) (optionset M) := mapset_dom.
-Instance optionmap_domspec `{FinMap K M} :
-  FinMapDom (option K) (optionmap M) (optionset M) := mapset_dom_spec.