Library zoo.common.fin_maps

From stdpp Require Export
  fin_maps
  fin_map_dom.

From zoo Require Import
  prelude.
From zoo.common Require Import
  option.
From zoo Require Import
  options.

Section dom.
  Context `{FinMapDom K M D}.
  Context {A : Type}.

  Implicit Types m : M A.

  Lemma elem_of_dom_1 m k :
    k ∈ dom m →
    is_Some (m !! k).
End dom.

Section fmap.
  Context `{FinMapDom K M D}.
  Context {A : Type}.

  Implicit Types m : M A.

  Lemma lookup_fmap_None {B} (f : A → B) m k :
    (f <$> m) !! k = None ↔
    m !! k = None.
End fmap.

Section map_Forall.
  Context `{FinMap K M}.
  Context {A : Type}.

  Implicit Types m : M A.

  Lemma map_Forall_impl' P1 P2 m :
    map_Forall P1 m →
    ( ∀ k x,
      m !! k = Some x →
      P1 k x →
      P2 k x
    ) →
    map_Forall P2 m.

  Lemma map_Forall_insert_2' {P m} k x :
    P k x →
    map_Forall P (delete k m) →
    map_Forall P (<[k := x]> m).

  Lemma map_Forall_delete_lookup P m k :
    map_Forall P (delete k m) ↔
      ∀ k' x,
      k ≠ k' →
      m !! k' = Some x →
      P k' x.
  Lemma map_Forall_delete_lookup_1 {P m k} k' x :
    map_Forall P (delete k m) →
    k ≠ k' →
    m !! k' = Some x →
    P k' x.
  Lemma map_Forall_delete_lookup_2 P m k :
    ( ∀ k' x,
      k ≠ k' →
      m !! k' = Some x →
      P k' x
    ) →
    map_Forall P (delete k m).
End map_Forall.

Section map_Forall2.
  Context `{FinMapDom K M D}.

  Lemma map_Forall2_alt {A B R} (m : M A) (𝑚 : M B) :
    map_Forall2 R m 𝑚 ↔
      dom m ≡ dom 𝑚 ∧
        ∀ k x 𝑥,
        m !! k = Some x →
        𝑚 !! k = Some 𝑥 →
        R k x 𝑥.

  Lemma map_Forall2_flip {A B} R (m : M A) (𝑚 : M B) :
    map_Forall2 R m 𝑚 ↔
    map_Forall2 (λ k x 𝑥, R k 𝑥 x) 𝑚 m.

  Lemma map_Forall2_lookup_None_l {A B R} {m : M A} {𝑚 : M B} k :
    map_Forall2 R m 𝑚 →
    m !! k = None →
    𝑚 !! k = None.
  Lemma map_Forall2_lookup_None_r {A B R} {m : M A} {𝑚 : M B} k :
    map_Forall2 R m 𝑚 →
    𝑚 !! k = None →
    m !! k = None.

  Lemma map_Forall2_lookup_Some {A B R} {m : M A} {𝑚 : M B} k x 𝑥 :
    map_Forall2 R m 𝑚 →
    m !! k = Some x →
    𝑚 !! k = Some 𝑥 →
    R k x 𝑥.
  Lemma map_Forall2_lookup_Some_l {A B R} {m : M A} {𝑚 : M B} k x :
    map_Forall2 R m 𝑚 →
    m !! k = Some x →
      ∃ 𝑥,
      𝑚 !! k = Some 𝑥 ∧
      R k x 𝑥.
  Lemma map_Forall2_lookup_Some_r {A B R} {m : M A} {𝑚 : M B} k 𝑥 :
    map_Forall2 R m 𝑚 →
    𝑚 !! k = Some 𝑥 →
      ∃ x,
      m !! k = Some x ∧
      R k x 𝑥.

  Lemma map_Forall2_insert_l {A B R} {m : M A} {𝑚 : M B} k x 𝑥 :
    map_Forall2 R m 𝑚 →
    𝑚 !! k = Some 𝑥 →
    R k x 𝑥 →
    map_Forall2 R (<[k := x]> m) 𝑚.
  Lemma map_Forall2_insert_r {A B R} {m : M A} {𝑚 : M B} k x 𝑥 :
    map_Forall2 R m 𝑚 →
    m !! k = Some x →
    R k x 𝑥 →
    map_Forall2 R m (<[k := 𝑥]> 𝑚).

  Lemma map_Forall2_fmap_l {A B C R} (f : A → C) (m : M A) (𝑚 : M B) :
    map_Forall2 (λ k x 𝑥, R k (f x) 𝑥) m 𝑚 ↔
    map_Forall2 R (f <$> m) 𝑚.
  Lemma map_Forall2_fmap_l_1 {A B C R} (f : A → C) (m : M A) (𝑚 : M B) :
    map_Forall2 (λ k x 𝑥, R k (f x) 𝑥) m 𝑚 →
    map_Forall2 R (f <$> m) 𝑚.
  Lemma map_Forall2_fmap_l_2 {A B C R} (f : A → C) (m : M A) (𝑚 : M B) :
    map_Forall2 R (f <$> m) 𝑚 →
    map_Forall2 (λ k x 𝑥, R k (f x) 𝑥) m 𝑚.
  Lemma map_Forall2_fmap_r {A B C R} (f : B → C) (m : M A) (𝑚 : M B) :
    map_Forall2 (λ k x 𝑥, R k x (f 𝑥)) m 𝑚 ↔
    map_Forall2 R m (f <$> 𝑚).
  Lemma map_Forall2_fmap_r_1 {A B C R} (f : B → C) (m : M A) (𝑚 : M B) :
    map_Forall2 (λ k x 𝑥, R k x (f 𝑥)) m 𝑚 →
    map_Forall2 R m (f <$> 𝑚).
  Lemma map_Forall2_fmap_r_2 {A B C R} (f : B → C) (m : M A) (𝑚 : M B) :
    map_Forall2 R m (f <$> 𝑚) →
    map_Forall2 (λ k x 𝑥, R k x (f 𝑥)) m 𝑚.
End map_Forall2.

Section kmap.
  Context `{FinMap K1 M1} `{FinMap K2 M2}.
  Context (f : K1 → K2) `{!Inj (=) (=) f}.

  Notation kmap := (
    kmap (M1 := M1) (M2 := M2)
  ).

  #[local] Lemma NoDup_fst_prod_map_map_to_list {A} (m : M1 A) :
    NoDup (prod_map f id <$> map_to_list m).*1.
  Lemma map_to_list_kmap {A} (m : M1 A) :
    map_to_list (kmap f m) ≡ₚ prod_map f id <$> map_to_list m.
  Lemma kmap_list_to_map {A} (l : list (K1 × A)) :
    NoDup l.*1 →
    kmap f (list_to_map l) = list_to_map (prod_map f id <$> l).
End kmap.

Section map_oflatten.
  Context `{FinMap K M}.
  Context {A : Type}.

  Definition map_oflatten (m : M (option A)) :=
    omap id m.

  Lemma lookup_map_oflatten_None m k :
    m !! k = None →
    map_oflatten m !! k = None.
  Lemma lookup_map_oflatten_Some_None m k :
    m !! k = Some None →
    map_oflatten m !! k = None.
  Lemma lookup_map_oflatten_Some_Some {m k} a :
    m !! k = Some (Some a) →
    map_oflatten m !! k = Some a.

  Lemma lookup_map_oflatten_Some_inv m k a :
    map_oflatten m !! k = Some a →
    m !! k = Some (Some a).

  Lemma map_oflatten_empty m :
    (∀ k o, m !! k = Some o → o = None) →
    map_oflatten m = ∅.

  Lemma map_oflatten_union m1 m2 :
    m1 ##ₘ m2 →
    map_oflatten (m1 ∪ m2) = map_oflatten m1 ∪ map_oflatten m2.

  Lemma map_oflatten_insert {m} k :
    m !! k = None →
    map_oflatten (<[k := None]> m) = map_oflatten m.
  Lemma map_oflatten_update {m} k a :
    map_oflatten (<[k := Some a]> m) = <[k := a]> (map_oflatten m).
End map_oflatten.