phanerozoic/Coq-Stdpp huggingface dataset:
(* stdpp/fin_maps.v *)
Lemma map_kmap_compose {A} (m : M1 A) :
    kmap (g ∘ f) m =@{M3 A} kmap g (M1:=M2) (kmap f m).
Proof.
    apply map_eq; intros i. apply option_eq; intros x.
    repeat setoid_rewrite (lookup_kmap_Some _). naive_solver.
  Qed.
(* stdpp/fin_maps.v *)
Notation map_preimg
:=
    (map_preimg (K:=K) (A:=A) (MKA:=MK A) (MASK:=MA SK) (SK:=SK)).
(* stdpp/fin_maps.v *)
Lemma map_preimg_empty : map_preimg ∅ = ∅.
Proof. apply map_fold_empty. Qed.
(* stdpp/fin_maps.v *)
Lemma map_preimg_insert m i x :
    m !! i = None →
    map_preimg (<[i:=x]> m) =
      partial_alter (λ mX, Some ({[ i ]} ∪ default ∅ mX)) x (map_preimg m).
Proof.
    intros Hi. refine (map_fold_insert_L _ _ i x m _ Hi).
    intros j1 j2 x1 x2 m' ? _ _. destruct (decide (x1 = x2)) as [->|?].
    - rewrite !partial_alter_partial_alter_eq.
      apply partial_alter_ext; intros ? _; f_equal/=. set_solver.
    - by apply partial_alter_partial_alter_ne.
  Qed.
(* stdpp/fin_maps.v *)
(* The [map_preimg] function never returns an empty set (we represent that
  case via [None]). *)
Lemma lookup_preimg_Some_non_empty m x :
    map_preimg m !! x ≠ Some ∅.
Proof.
    induction m as [|i x' m ? IH] using map_ind.
    { by rewrite map_preimg_empty, lookup_empty. }
    rewrite map_preimg_insert by done. destruct (decide (x = x')) as [->|].
    - rewrite lookup_partial_alter_eq. intros [=]. set_solver.
    - rewrite lookup_partial_alter_ne by done. set_solver.
  Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_preimg_None_1 m x i :
    map_preimg m !! x = None → m !! i ≠ Some x.
Proof.
    induction m as [|i' x' m ? IH] using map_ind; [by rewrite lookup_empty|].
    rewrite map_preimg_insert by done. destruct (decide (x = x')) as [->|].
    - by rewrite lookup_partial_alter_eq.
    - rewrite lookup_partial_alter_ne, lookup_insert_Some by done. naive_solver.
  Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_preimg_Some_1 m X x i :
    map_preimg m !! x = Some X →
    i ∈ X ↔ m !! i = Some x.
Proof.
    revert X. induction m as [|i' x' m ? IH] using map_ind; intros X.
    { by rewrite map_preimg_empty, lookup_empty. }
    rewrite map_preimg_insert by done. destruct (decide (x = x')) as [->|].
    - rewrite lookup_partial_alter_eq. intros [= <-].
      rewrite elem_of_union, elem_of_singleton, lookup_insert_Some.
      destruct (map_preimg m !! x') as [X'|] eqn:Hx'; simpl.
      + rewrite IH by done. naive_solver.
      + apply (lookup_preimg_None_1 _ _ i) in Hx'. set_solver.
    - rewrite lookup_partial_alter_ne, lookup_insert_Some by done. naive_solver.
  Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_preimg_None m x :
    map_preimg m !! x = None ↔ ∀ i, m !! i ≠ Some x.
Proof.
    split; [by eauto using lookup_preimg_None_1|].
    intros Hm. apply eq_None_not_Some; intros [X ?].
    destruct (set_choose_L X) as [i ?].
    { intros ->. by eapply lookup_preimg_Some_non_empty. }
    by eapply (Hm i), lookup_preimg_Some_1.
  Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_preimg_Some m x X :
    map_preimg m !! x = Some X ↔ X ≠ ∅ ∧ ∀ i, i ∈ X ↔ m !! i = Some x.
Proof.
    split.
    - intros HxX. split; [intros ->; by eapply lookup_preimg_Some_non_empty|].
      intros j. by apply lookup_preimg_Some_1.
    - intros [HXne HX]. destruct (map_preimg m !! x) as [X'|] eqn:HX'.
      + f_equal; apply set_eq; intros i. rewrite HX.
        by apply lookup_preimg_Some_1.
      + apply set_choose_L in HXne as [j ?].
        apply (lookup_preimg_None_1 _ _ j) in HX'. naive_solver.
  Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_total_preimg m x i :
    i ∈ map_preimg m !!! x ↔ m !! i = Some x.
Proof.
    rewrite lookup_total_alt. destruct (map_preimg m !! x) as [X|] eqn:HX.
    - by apply lookup_preimg_Some.
    - rewrite lookup_preimg_None in HX. set_solver.
  Qed.
(* stdpp/fin_maps.v *)
(* avoid writing ≡@{D} everywhere... *)
Notation map_img
:= (map_img (M:=M A) (SA:=SA)).
(* stdpp/fin_maps.v *)
Lemma elem_of_map_img m x : x ∈ map_img m ↔ ∃ i, m !! i = Some x.
Proof. unfold map_img. rewrite elem_of_map_to_set. naive_solver. Qed.
(* stdpp/fin_maps.v *)
Lemma elem_of_map_img_1 m x : x ∈ map_img m → ∃ i, m !! i = Some x.
Proof. apply elem_of_map_img. Qed.
(* stdpp/fin_maps.v *)
Lemma elem_of_map_img_2 m i x : m !! i = Some x → x ∈ map_img m.
Proof. rewrite elem_of_map_img. eauto. Qed.
(* stdpp/fin_maps.v *)
Lemma not_elem_of_map_img m x : x ∉ map_img m ↔ ∀ i, m !! i ≠ Some x.
Proof. rewrite elem_of_map_img. naive_solver. Qed.
(* stdpp/fin_maps.v *)
Lemma not_elem_of_map_img_1 m i x : x ∉ map_img m → m !! i ≠ Some x.
Proof. rewrite not_elem_of_map_img. eauto. Qed.
(* stdpp/fin_maps.v *)
Lemma not_elem_of_map_img_2 m x : (∀ i, m !! i ≠ Some x) → x ∉ map_img m.
Proof. apply not_elem_of_map_img. Qed.
(* stdpp/fin_maps.v *)
Lemma map_subseteq_img m1 m2 : m1 ⊆ m2 → map_img m1 ⊆ map_img m2.
Proof.
    rewrite map_subseteq_spec. intros ? x.
    rewrite !elem_of_map_img. naive_solver.
  Qed.
(* stdpp/fin_maps.v *)
Lemma map_img_filter (P : K * A → Prop) `{!∀ ix, Decision (P ix)} m X :
    (∀ x, x ∈ X ↔ ∃ i, m !! i = Some x ∧ P (i, x)) →
    map_img (filter P m) ≡ X.
Proof.
    intros HX x. rewrite elem_of_map_img, HX.
    unfold is_Some. by setoid_rewrite map_lookup_filter_Some.
  Qed.
(* stdpp/fin_maps.v *)
Lemma map_img_filter_subseteq (P : K * A → Prop) `{!∀ ix, Decision (P ix)} m :
    map_img (filter P m) ⊆ map_img m.
Proof. apply map_subseteq_img, map_filter_subseteq. Qed.
(* stdpp/fin_maps.v *)
Lemma map_img_empty : map_img ∅ ≡ ∅.
Proof.
    rewrite set_equiv. intros x. rewrite elem_of_map_img, elem_of_empty.
    setoid_rewrite lookup_empty. naive_solver.
  Qed.
(* stdpp/fin_maps.v *)
Lemma map_img_empty_iff m : map_img m ≡ ∅ ↔ m = ∅.
Proof.
    split; [|intros ->; by rewrite map_img_empty].
    intros Hm. apply map_empty; intros i.
    apply eq_None_ne_Some; intros x ?%elem_of_map_img_2. set_solver.
  Qed.
(* stdpp/fin_maps.v *)
Lemma map_img_empty_inv m : map_img m ≡ ∅ → m = ∅.
Proof. apply map_img_empty_iff. Qed.
(* stdpp/fin_maps.v *)
Lemma map_img_delete_subseteq i m : map_img (delete i m) ⊆ map_img m.
Proof. apply map_subseteq_img, delete_subseteq. Qed.
(* stdpp/fin_maps.v *)
Lemma map_img_insert m i x :
    map_img (<[i:=x]> m) ≡ {[ x ]} ∪ map_img (delete i m).
Proof.
    intros y. rewrite elem_of_union, !elem_of_map_img, elem_of_singleton.
    setoid_rewrite lookup_delete_Some. setoid_rewrite lookup_insert_Some.
    naive_solver.
  Qed.
(* stdpp/fin_maps.v *)
Lemma map_img_insert_notin m i x :
    m !! i = None → map_img (<[i:=x]> m) ≡ {[ x ]} ∪ map_img m.
Proof. intros. by rewrite map_img_insert, delete_id. Qed.
(* stdpp/fin_maps.v *)
Lemma map_img_insert_subseteq m i x :
    map_img (<[i:=x]> m) ⊆ {[ x ]} ∪ map_img m.
Proof.
    rewrite map_img_insert. apply union_mono_l, map_img_delete_subseteq.
  Qed.
(* stdpp/fin_maps.v *)
Lemma elem_of_map_img_insert m i x : x ∈ map_img (<[i:=x]> m).
Proof. apply elem_of_map_img. exists i. apply lookup_insert_eq. Qed.
(* stdpp/fin_maps.v *)
Lemma elem_of_map_img_insert_ne m i x y :
    x ≠ y → x ∈ map_img (<[i:=y]> m) → x ∈ map_img m.
Proof. intros ? ?%map_img_insert_subseteq. set_solver. Qed.
(* stdpp/fin_maps.v *)
Lemma map_img_singleton i x : map_img {[i:=x]} ≡ {[ x ]}.
Proof.
    apply set_equiv. intros y.
    rewrite elem_of_map_img. setoid_rewrite lookup_singleton_Some. set_solver.
  Qed.
(* stdpp/fin_maps.v *)
Lemma elem_of_map_img_union m1 m2 x :
    x ∈ map_img (m1 ∪ m2) →
    x ∈ map_img m1 ∨ x ∈ map_img m2.
Proof.
    rewrite !elem_of_map_img. setoid_rewrite lookup_union_Some_raw. naive_solver.
  Qed.
(* stdpp/fin_maps.v *)
Lemma elem_of_map_img_union_l m1 m2 x :
    x ∈ map_img m1 → x ∈ map_img (m1 ∪ m2).
Proof.
    rewrite !elem_of_map_img. setoid_rewrite lookup_union_Some_raw. naive_solver.
  Qed.
(* stdpp/fin_maps.v *)
Lemma elem_of_map_img_union_r m1 m2 x :
    m1 ##ₘ m2 → x ∈ map_img m2 → x ∈ map_img (m1 ∪ m2).
Proof.
    intros. rewrite map_union_comm by done. by apply elem_of_map_img_union_l.
  Qed.
(* stdpp/fin_maps.v *)
Lemma elem_of_map_img_union_disjoint m1 m2 x :
    m1 ##ₘ m2 → x ∈ map_img (m1 ∪ m2) ↔ x ∈ map_img m1 ∨ x ∈ map_img m2.
Proof.
    naive_solver eauto using elem_of_map_img_union,
      elem_of_map_img_union_l, elem_of_map_img_union_r.
  Qed.
(* stdpp/fin_maps.v *)
Lemma map_img_union_subseteq m1 m2 :
    map_img (m1 ∪ m2) ⊆ map_img m1 ∪ map_img m2.
Proof. intros v Hv. apply elem_of_union, elem_of_map_img_union. exact Hv. Qed.
(* stdpp/fin_maps.v *)
Lemma map_img_union_subseteq_l m1 m2 : map_img m1 ⊆ map_img (m1 ∪ m2).
Proof. intros v Hv. by apply elem_of_map_img_union_l. Qed.
(* stdpp/fin_maps.v *)
Lemma map_img_union_subseteq_r m1 m2 :
    m1 ##ₘ m2 → map_img m2 ⊆ map_img (m1 ∪ m2).
Proof. intros Hdisj v Hv. by apply elem_of_map_img_union_r. Qed.
(* stdpp/fin_maps.v *)
Lemma map_img_union_disjoint m1 m2 :
    m1 ##ₘ m2 → map_img (m1 ∪ m2) ≡ map_img m1 ∪ map_img m2.
Proof.
    intros Hdisj. apply set_equiv. intros x.
    rewrite elem_of_union. by apply elem_of_map_img_union_disjoint.
  Qed.
(* stdpp/fin_maps.v *)
Lemma map_img_finite m : set_finite (map_img m).
Proof.
    induction m as [|i x m ? IH] using map_ind.
    - rewrite map_img_empty. apply empty_finite.
    - eapply set_finite_subseteq; [by apply map_img_insert_subseteq|].
      apply union_finite; [apply singleton_finite | apply IH].
  Qed.
(* stdpp/fin_maps.v *)
(* Alternative definition of [img] in terms of [map_to_list]. *)
Lemma map_img_alt m : map_img m ≡ list_to_set (map_to_list m).*2.
Proof.
    induction m as [|i x m ? IH] using map_ind.
    { by rewrite map_img_empty, map_to_list_empty. }
    by rewrite map_img_insert_notin, map_to_list_insert by done.
  Qed.
(* stdpp/fin_maps.v *)
Lemma map_img_singleton_inv m i x :
    map_img m ≡ {[ x ]} → m !! i = None ∨ m !! i = Some x.
Proof.
    intros Hm. destruct (m !! i) eqn:Hmk; [|by auto].
    apply elem_of_map_img_2 in Hmk. set_solver.
  Qed.
(* stdpp/fin_maps.v *)
Lemma map_img_union_inv `{!RelDecision (∈@{SA})} X Y m :
    X ## Y →
    map_img m ≡ X ∪ Y →
    ∃ m1 m2, m = m1 ∪ m2 ∧ m1 ##ₘ m2 ∧ map_img m1 ≡ X ∧ map_img m2 ≡ Y.
Proof.
    intros Hsep Himg.
    exists (filter (λ '(_,x), x ∈ X) m), (filter (λ '(_,x), x ∉ X) m).
    assert (filter (λ '(_,x), x ∈ X) m ##ₘ filter (λ '(_,x), x ∉ X) m).
    { apply map_disjoint_filter_complement. }
    split_and!.
    - symmetry. apply map_filter_union_complement.
    - done.
    - apply map_img_filter; intros x. split; [|naive_solver].
      intros. destruct (elem_of_map_img_1 m x); set_solver.
    - apply map_img_filter; intros x; split.
      + intros. destruct (elem_of_map_img_1 m x); set_solver.
      + intros (i & ?%elem_of_map_img_2 & ?). set_solver.
  Qed.
(* stdpp/fin_maps.v *)
Lemma map_img_empty_L : map_img ∅ = ∅.
Proof. unfold_leibniz. exact map_img_empty. Qed.
(* stdpp/fin_maps.v *)
Lemma map_img_empty_iff_L m : map_img m = ∅ ↔ m = ∅.
Proof. unfold_leibniz. apply map_img_empty_iff. Qed.
(* stdpp/fin_maps.v *)
Lemma map_img_empty_inv_L m : map_img m = ∅ → m = ∅.
Proof. apply map_img_empty_iff_L. Qed.
(* stdpp/fin_maps.v *)
Lemma map_img_singleton_L i x : map_img {[i:=x]} = {[ x ]}.
Proof. unfold_leibniz. apply map_img_singleton. Qed.
(* stdpp/fin_maps.v *)
Lemma map_img_insert_notin_L m i x :
      m !! i = None → map_img (<[i:=x]> m) = {[ x ]} ∪ map_img m.
Proof. unfold_leibniz. apply map_img_insert_notin. Qed.
(* stdpp/fin_maps.v *)
Lemma map_img_union_disjoint_L m1 m2 :
      m1 ##ₘ m2 → map_img (m1 ∪ m2) = map_img m1 ∪ map_img m2.
Proof. unfold_leibniz. apply map_img_union_disjoint. Qed.
(* stdpp/fin_maps.v *)
Lemma map_img_alt_L m : map_img m = list_to_set (map_to_list m).*2.
Proof. unfold_leibniz. apply map_img_alt. Qed.
(* stdpp/fin_maps.v *)
Lemma map_img_singleton_inv_L m i x :
      map_img m = {[ x ]} → m !! i = None ∨ m !! i = Some x.
Proof. unfold_leibniz. apply map_img_singleton_inv. Qed.
(* stdpp/fin_maps.v *)
Lemma map_img_union_inv_L `{!RelDecision (∈@{SA})} X Y m :
      X ## Y →
      map_img m = X ∪ Y →
      ∃ m1 m2, m = m1 ∪ m2 ∧ m1 ##ₘ m2 ∧ map_img m1 = X ∧ map_img m2 = Y.
Proof. unfold_leibniz. apply map_img_union_inv. Qed.
(* stdpp/fin_maps.v *)
(* Set solver instances *)
Instance set_unfold_map_img_empty x :
    SetUnfoldElemOf x (map_img (∅:M A)) False.
Proof. constructor. by rewrite map_img_empty, elem_of_empty. Qed.
(* stdpp/fin_maps.v *)
Instance set_unfold_map_img_singleton x i y :
    SetUnfoldElemOf x (map_img ({[i:=y]}:M A)) (x = y).
Proof. constructor. by rewrite map_img_singleton, elem_of_singleton. Qed.
(* stdpp/fin_maps.v *)
Lemma map_img_fmap `{FinMap K M, FinSet A SA, SemiSet B SB} (f : A → B) (m : M A) :
  map_img (f <$> m) ≡@{SB} set_map (C:=SA) f (map_img m).
Proof.
  apply set_equiv. intros y. rewrite elem_of_map_img, elem_of_map.
  setoid_rewrite lookup_fmap. setoid_rewrite fmap_Some.
  setoid_rewrite elem_of_map_img. naive_solver.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_img_fmap_L `{FinMap K M, FinSet A SA, SemiSet B SB, !LeibnizEquiv SB}
    (f : A → B) (m : M A) :
  map_img (f <$> m) =@{SB} set_map (C:=SA) f (map_img m).
Proof. unfold_leibniz. apply map_img_fmap. Qed.
(* stdpp/fin_maps.v *)
Lemma map_img_kmap `{FinMap K M, FinMap K2 M2, SemiSet A SA}
    (f : K → K2) `{!Inj (=) (=) f} m :
  map_img (kmap (M2:=M2) f m) ≡@{SA} map_img m.
Proof.
  apply set_equiv. intros x. rewrite !elem_of_map_img.
  setoid_rewrite (lookup_kmap_Some f). naive_solver.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_img_kmap_L `{FinMap K M, FinMap K2 M2, SemiSet A SA, !LeibnizEquiv SA}
    (f : K → K2) `{!Inj (=) (=) f} m :
  map_img (kmap (M2:=M2) f m) =@{SA} map_img m.
Proof. unfold_leibniz. by apply map_img_kmap. Qed.
(* stdpp/fin_maps.v *)
Instance set_unfold_map_img_kmap `{FinMap K M, FinMap K2 M2, SemiSet A SA}
    (f : K → K2) `{!Inj (=) (=) f} (m : M A) x Q :
  SetUnfoldElemOf x (map_img (SA:=SA) m) Q →
  SetUnfoldElemOf x (map_img (SA:=SA) (kmap (M2:=M2) f m)) Q.
Proof.
  constructor. rewrite map_img_kmap; [|done].
  by setoid_rewrite (set_unfold_elem_of _ (map_img m)).
Qed.
(* stdpp/fin_maps.v *)
Lemma map_lookup_compose m n a : (m ∘ₘ n) !! a = n !! a ≫= (m !!.).
Proof. apply lookup_omap. Qed.
(* stdpp/fin_maps.v *)
Lemma map_lookup_compose_Some m n a c :
    (m ∘ₘ n) !! a = Some c ↔ ∃ b, n !! a = Some b ∧ m !! b = Some c.
Proof. rewrite map_lookup_compose. destruct (n !! a) eqn:?; naive_solver. Qed.
(* stdpp/fin_maps.v *)
Lemma map_lookup_compose_Some_1 m n a c :
    (m ∘ₘ n) !! a = Some c → ∃ b, n !! a = Some b ∧ m !! b = Some c.
Proof. by rewrite map_lookup_compose_Some. Qed.
(* stdpp/fin_maps.v *)
Lemma map_lookup_compose_Some_2 m n a b c :
    n !! a = Some b → m !! b = Some c → (m ∘ₘ n) !! a = Some c.
Proof. intros. apply map_lookup_compose_Some. by exists b. Qed.
(* stdpp/fin_maps.v *)
Lemma map_lookup_compose_None m n a :
    (m ∘ₘ n) !! a = None ↔
    n !! a = None ∨ ∃ b, n !! a = Some b ∧ m !! b = None.
Proof. rewrite map_lookup_compose. destruct (n !! a) eqn:?; naive_solver. Qed.
(* stdpp/fin_maps.v *)
Lemma map_lookup_compose_None_1 m n a :
    (m ∘ₘ n) !! a = None → n !! a = None ∨ ∃ b, n !! a = Some b ∧ m !! b = None.
Proof. apply map_lookup_compose_None. Qed.
(* stdpp/fin_maps.v *)
Lemma map_lookup_compose_None_2_1 m n a : n !! a = None → (m ∘ₘ n) !! a = None.
Proof. intros. apply map_lookup_compose_None. by left. Qed.
(* stdpp/fin_maps.v *)
Lemma map_lookup_compose_None_2_2 m n a b :
    n !! a = Some b → m !! b = None → (m ∘ₘ n) !! a = None.
Proof. intros. apply map_lookup_compose_None. naive_solver. Qed.
(* stdpp/fin_maps.v *)
Lemma map_compose_img_subseteq `{SemiSet C D} m n :
    map_img (m ∘ₘ n) ⊆@{D} map_img m.
Proof.
    intros c. rewrite !elem_of_map_img.
    setoid_rewrite map_lookup_compose_Some. naive_solver.
  Qed.
(* stdpp/fin_maps.v *)
Lemma map_compose_empty_r m : m ∘ₘ ∅ =@{MA C} ∅.
Proof. apply omap_empty. Qed.
(* stdpp/fin_maps.v *)
Lemma map_compose_empty_l n : (∅ : MB C) ∘ₘ n =@{MA C} ∅.
Proof.
    apply map_eq. intros k. rewrite map_lookup_compose, lookup_empty.
    destruct (n !! k); simpl; [|done]. apply lookup_empty.
  Qed.
(* stdpp/fin_maps.v *)
Lemma map_compose_empty_iff m n :
    m ∘ₘ n = ∅ ↔ ∀ a b, n !! a = Some b → m !! b = None.
Proof.
    rewrite map_empty. setoid_rewrite map_lookup_compose_None.
    apply forall_proper; intros a. destruct (n !! a); naive_solver.
  Qed.
(* stdpp/fin_maps.v *)
Lemma map_disjoint_compose_l m1 m2 n : m1 ##ₘ m2 → m1 ∘ₘ n ##ₘ m2 ∘ₘ n.
Proof.
    rewrite !map_disjoint_spec; intros Hdisj a c1 c2.
    rewrite !map_lookup_compose. destruct (n !! a); naive_solver.
  Qed.
(* stdpp/fin_maps.v *)
Lemma map_disjoint_compose_r m n1 n2 : n1 ##ₘ n2 → m ∘ₘ n1 ##ₘ m ∘ₘ n2.
Proof. apply map_disjoint_omap. Qed.
(* stdpp/fin_maps.v *)
Lemma map_compose_union_l m1 m2 n : (m1 ∪ m2) ∘ₘ n = (m1 ∘ₘ n) ∪ (m2 ∘ₘ n).
Proof.
    apply map_eq; intros a. rewrite lookup_union, !map_lookup_compose.
    destruct (n !! a) as [b|] eqn:?; simpl; [|done]. by rewrite lookup_union.
  Qed.
(* stdpp/fin_maps.v *)
Lemma map_compose_union_r m n1 n2 :
    n1 ##ₘ n2 → m ∘ₘ (n1 ∪ n2) = (m ∘ₘ n1) ∪ (m ∘ₘ n2).
Proof. intros Hs. by apply map_omap_union. Qed.
(* stdpp/fin_maps.v *)
Lemma map_compose_mono_l m n1 n2 : n1 ⊆ n2 → m ∘ₘ n1 ⊆ m ∘ₘ n2.
Proof. by apply map_omap_mono. Qed.
(* stdpp/fin_maps.v *)
Lemma map_compose_mono_r m1 m2 n : m1 ⊆ m2 → m1 ∘ₘ n ⊆ m2 ∘ₘ n.
Proof.
    rewrite !map_subseteq_spec; intros ? a c.
    rewrite !map_lookup_compose_Some. naive_solver.
  Qed.
(* stdpp/fin_maps.v *)
Lemma map_compose_mono m1 m2 n1 n2 :
    m1 ⊆ m2 → n1 ⊆ n2 → m1 ∘ₘ n1 ⊆ m2 ∘ₘ n2.
Proof.
    intros. transitivity (m1 ∘ₘ n2);
      [by apply map_compose_mono_l|by apply map_compose_mono_r].
  Qed.
(* stdpp/fin_maps.v *)
Lemma map_compose_as_omap m n : m ∘ₘ n = omap (m !!.) n.
Proof. done. Qed.
(* stdpp/fin_maps.v *)
(* Alternative definition of [m ∘ₘ n] by recursion on [n] *)
Lemma map_compose_as_fold m n :
    m ∘ₘ n = map_fold (λ a b,
               match m !! b with
               | Some c => <[a:=c]>
               | None => id
               end) ∅ n.
Proof.
    apply (map_fold_weak_ind (λ mn n, omap (m !!.) n = mn)).
    { apply map_compose_empty_r. }
    intros k b n' mn Hn' IH. rewrite omap_insert, <-IH.
    destruct (m !! b); [done|].
    by apply delete_id, map_lookup_compose_None_2_1.
  Qed.
(* stdpp/fin_maps.v *)
Lemma map_compose_min_l `{SemiSet B D, !RelDecision (∈@{D})} m n :
    m ∘ₘ n = filter (λ '(b,_), b ∈ map_img (SA:=D) n) m ∘ₘ n.
Proof.
    apply map_eq; intros a. rewrite !map_lookup_compose.
    destruct (n !! a) as [b|] eqn:?; simpl; [|done].
    rewrite map_lookup_filter. destruct (m !! b) eqn:?; simpl; [|done].
    by rewrite option_guard_True by (by eapply elem_of_map_img_2).
  Qed.
(* stdpp/fin_maps.v *)
Lemma map_compose_min_r m n :
    m ∘ₘ n = m ∘ₘ filter (λ '(_,b), is_Some (m !! b)) n.
Proof.
    apply map_eq; intros a. rewrite !map_lookup_compose, map_lookup_filter.
    destruct (n !! a) as [b|] eqn:?; simpl; [|done]. by destruct (m !! b) eqn:?.
  Qed.
(* stdpp/fin_maps.v *)
Lemma map_compose_insert_Some m n a b c :
    m !! b = Some c →
    m ∘ₘ <[a:=b]> n =@{MA C} <[a:=c]> (m ∘ₘ n).
Proof. intros. by apply omap_insert_Some. Qed.
(* stdpp/fin_maps.v *)
Lemma map_compose_insert_None m n a b :
    m !! b = None →
    m ∘ₘ <[a:=b]> n =@{MA C} delete a (m ∘ₘ n).
Proof. intros. by apply omap_insert_None. Qed.
(* stdpp/fin_maps.v *)
Lemma map_compose_delete m n a :
    m ∘ₘ delete a n =@{MA C} delete a (m ∘ₘ n).
Proof. intros. by apply omap_delete. Qed.
(* stdpp/fin_maps.v *)
Lemma map_compose_singleton_Some m a b c :
    m !! b = Some c →
    m ∘ₘ {[a:=b]} =@{MA C} {[a:=c]}.
Proof. intros. by apply omap_singleton_Some. Qed.
(* stdpp/fin_maps.v *)
Lemma map_compose_singleton_None m a b :
    m !! b = None →
    m ∘ₘ {[a:=b]} =@{MA C} ∅.
Proof. intros. by apply omap_singleton_None. Qed.
(* stdpp/fin_maps.v *)
Lemma map_compose_singletons a b c :
    ({[b:=c]} : MB C) ∘ₘ {[a:=b]} =@{MA C} {[a:=c]}.
Proof. by apply map_compose_singleton_Some, lookup_insert_eq. Qed.
(* stdpp/fin_maps.v *)
Lemma map_compose_assoc `{FinMap A MA, FinMap B MB, FinMap C MC} {D}
    (m : MC D) (n : MB C) (o : MA B) :
  m ∘ₘ (n ∘ₘ o) = (m ∘ₘ n) ∘ₘ o.
Proof.
  apply map_eq; intros a. rewrite !map_lookup_compose.
  destruct (o !! a); simpl; [|done]. by rewrite map_lookup_compose.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_fmap_map_compose `{FinMap A MA, FinMap B MB} {C1 C2} (f : C1 → C2)
    (m : MB C1) (n : MA B) :
  f <$> (m ∘ₘ n) = (f <$> m) ∘ₘ n.
Proof.
  apply map_eq; intros a. rewrite lookup_fmap, !map_lookup_compose.
  destruct (n !! a); simpl; [|done]. by rewrite lookup_fmap.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_omap_map_compose `{FinMap A MA, FinMap B MB} {C1 C2} (f : C1 → option C2)
    (m : MB C1) (n : MA B) :
  omap f (m ∘ₘ n) = omap f m ∘ₘ n.
Proof.
  apply map_eq; intros a. rewrite lookup_omap, !map_lookup_compose.
  destruct (n !! a); simpl; [|done]. by rewrite lookup_omap.
Qed.
(* stdpp/fin_maps.v *)
Notation map_curry
:= (map_curry (M1:=M1) (M2:=M2)).
(* stdpp/fin_maps.v *)
Notation map_uncurry
:= (map_uncurry (M12:=MC)).
(* stdpp/fin_maps.v *)
Lemma lookup_map_uncurry (m : M1 (M2 A)) i j :
    map_uncurry m !! (i,j) = m !! i ≫= (.!! j).
Proof.
    apply (map_fold_weak_ind (λ mr m, mr !! (i,j) = m !! i ≫= (.!! j))).
    { by rewrite !lookup_empty. }
    clear m; intros i' m2 m m12 Hi' IH.
    apply (map_fold_weak_ind (λ m2r m2, m2r !! (i,j) = <[i':=m2]> m !! i ≫= (.!! j))).
    { rewrite IH. rewrite lookup_insert.
      destruct (decide (i' = i)) as [->|]; [|done].
      rewrite Hi'; simpl; by rewrite lookup_empty. }
    intros j' y m2' m12' Hj' IH'. destruct (decide (i = i')) as [->|].
    - rewrite lookup_insert_eq; simpl. destruct (decide (j = j')) as [->|].
      + by rewrite !lookup_insert_eq.
      + by rewrite !lookup_insert_ne, IH', lookup_insert_eq by congruence.
    - by rewrite !lookup_insert_ne, IH', lookup_insert_ne by congruence.
  Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_map_curry (m : MC A) i j :
    map_curry m !! i ≫= (.!! j) = m !! (i, j).
Proof.
    apply (map_fold_weak_ind (λ mr m, mr !! i ≫= (.!! j) = m !! (i, j))).
    { by rewrite !lookup_empty. }
    clear m; intros [i' j'] x m12 mr Hij' IH.
    destruct (decide (i = i')) as [->|].
    - rewrite lookup_partial_alter_eq. destruct (decide (j = j')) as [->|].
      + destruct (mr !! i'); simpl; by rewrite !lookup_insert_eq.
      + destruct (mr !! i'); simpl; rewrite !lookup_insert_ne by congruence; first done.
        by rewrite <-IH, lookup_empty.
    - by rewrite lookup_partial_alter_ne, lookup_insert_ne by congruence.
  Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_map_curry_None (m : MC A) i :
    map_curry m !! i = None ↔ (∀ j, m !! (i, j) = None).
Proof.
    apply (map_fold_weak_ind
      (λ mr m, mr !! i = None ↔ (∀ j, m !! (i, j) = None))).
    { split; intros; by rewrite !lookup_empty. }
    clear m; intros [i' j'] x m12 mr Hij' IH.
    destruct (decide (i = i')) as [->|].
    - split; [by rewrite lookup_partial_alter_eq|].
      intros Hi. specialize (Hi j'). by rewrite lookup_insert_eq in Hi.
    - rewrite lookup_partial_alter_ne, IH; [|done]. apply forall_proper.
      intros j. rewrite lookup_insert_ne; [done|congruence].
  Qed.
(* stdpp/fin_maps.v *)
Lemma map_uncurry_curry (m : MC A) :
    map_uncurry (map_curry m) = m.
Proof.
   apply map_eq; intros [i j]. by rewrite lookup_map_uncurry, lookup_map_curry.
  Qed.
(* stdpp/fin_maps.v *)
Lemma map_curry_non_empty (m : MC A) i x :
    map_curry m !! i = Some x → x ≠ ∅.
Proof.
    intros Hm ->. eapply eq_None_not_Some; [|by eexists].
    eapply lookup_map_curry_None; intros j.
    rewrite <-lookup_map_curry, Hm.
    simpl. by rewrite lookup_empty.
  Qed.
(* stdpp/fin_maps.v *)
Lemma map_curry_uncurry_non_empty (m : M1 (M2 A)) :
    (∀ i x, m !! i = Some x → x ≠ ∅) →
    map_curry (map_uncurry m) = m.
Proof.
    intros Hne. apply map_eq; intros i. destruct (m !! i) as [m2|] eqn:Hm.
    - destruct (map_curry (map_uncurry m) !! i) as [m2'|] eqn:Hcurry.
      + f_equal. apply map_eq. intros j.
        replace (m2 !! j) with (Some m2 ≫= (.!! j)); last by simpl.
        replace (m2' !! j) with (Some m2' ≫= (.!! j)); last by simpl.
        by rewrite <-Hcurry, lookup_map_curry, lookup_map_uncurry, Hm.
      + rewrite lookup_map_curry_None in Hcurry.
        exfalso; apply (Hne i m2), map_eq; [done|intros j].
        by rewrite lookup_empty, <-(Hcurry j), lookup_map_uncurry, Hm.
   - apply lookup_map_curry_None; intros j. by rewrite lookup_map_uncurry, Hm.
  Qed.