phanerozoic/Coq-Stdpp huggingface dataset:
(* stdpp/fin_maps.v *)
Lemma insert_union_singleton_r {A} (m : M A) i x :
  m !! i = None → <[i:=x]> m = m ∪ {[i:=x]}.
Proof.
  intro. rewrite insert_union_singleton_l, map_union_comm; [done |].
  by apply map_disjoint_singleton_l.
Qed.
(* stdpp/fin_maps.v *)
Lemma union_singleton_r {A} (m : M A) i x y :
  m !! i = Some x → m ∪ {[i:=y]} = m.
Proof.
  intro Hlkup. apply map_eq. intros j.
  rewrite lookup_union, lookup_singleton.
  case_decide; destruct (m !! j) eqn:?; naive_solver.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_disjoint_insert_l {A} (m1 m2 : M A) i x :
  <[i:=x]> m1 ##ₘ m2 ↔ m2 !! i = None ∧ m1 ##ₘ m2.
Proof.
  rewrite insert_union_singleton_l.
  by rewrite map_disjoint_union_l, map_disjoint_singleton_l.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_disjoint_insert_r {A} (m1 m2 : M A) i x :
  m1 ##ₘ <[i:=x]> m2 ↔ m1 !! i = None ∧ m1 ##ₘ m2.
Proof.
  rewrite insert_union_singleton_l.
  by rewrite map_disjoint_union_r, map_disjoint_singleton_r.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_disjoint_insert_l_2 {A} (m1 m2 : M A) i x :
  m2 !! i = None → m1 ##ₘ m2 → <[i:=x]> m1 ##ₘ m2.
Proof. by rewrite map_disjoint_insert_l. Qed.
(* stdpp/fin_maps.v *)
Lemma map_disjoint_insert_r_2 {A} (m1 m2 : M A) i x :
  m1 !! i = None → m1 ##ₘ m2 → m1 ##ₘ <[i:=x]> m2.
Proof. by rewrite map_disjoint_insert_r. Qed.
(* stdpp/fin_maps.v *)
Lemma insert_union_l {A} (m1 m2 : M A) i x :
  <[i:=x]>(m1 ∪ m2) = <[i:=x]> m1 ∪ m2.
Proof. by rewrite !insert_union_singleton_l, (assoc_L (∪)). Qed.
(* stdpp/fin_maps.v *)
Lemma insert_union_r {A} (m1 m2 : M A) i x :
  m1 !! i = None → <[i:=x]>(m1 ∪ m2) = m1 ∪ <[i:=x]> m2.
Proof.
  intro. rewrite !insert_union_singleton_l, !(assoc_L (∪)).
  rewrite (map_union_comm m1); [done |].
  by apply map_disjoint_singleton_r.
Qed.
(* stdpp/fin_maps.v *)
Lemma foldr_insert_union {A} (m : M A) l :
  foldr (λ p, <[p.1:=p.2]>) m l = list_to_map l ∪ m.
Proof.
  induction l as [|i l IH]; simpl; [by rewrite (left_id_L _ _)|].
  by rewrite IH, insert_union_l.
Qed.
(* stdpp/fin_maps.v *)
Lemma delete_union {A} (m1 m2 : M A) i :
  delete i (m1 ∪ m2) = delete i m1 ∪ delete i m2.
Proof. apply delete_union_with. Qed.
(* stdpp/fin_maps.v *)
Lemma union_delete_insert {A} (m1 m2 : M A) i x :
  m1 !! i = Some x →
  delete i m1 ∪ <[i:=x]> m2 = m1 ∪ m2.
Proof.
  intros. rewrite <-insert_union_r by apply lookup_delete_eq.
  by rewrite insert_union_l, insert_delete_id by done.
Qed.
(* stdpp/fin_maps.v *)
Lemma union_insert_delete {A} (m1 m2 : M A) i x :
  m1 !! i = None → m2 !! i = Some x →
  <[i:=x]> m1 ∪ delete i m2 = m1 ∪ m2.
Proof.
  intros. rewrite <-insert_union_l by apply lookup_delete.
  by rewrite insert_union_r, insert_delete_id by done.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_Forall_union_1_1 {A} (m1 m2 : M A) P :
  map_Forall P (m1 ∪ m2) → map_Forall P m1.
Proof. intros HP i x ?. apply HP, lookup_union_Some_raw; auto. Qed.
(* stdpp/fin_maps.v *)
Lemma map_Forall_union_1_2 {A} (m1 m2 : M A) P :
  m1 ##ₘ m2 → map_Forall P (m1 ∪ m2) → map_Forall P m2.
Proof. intros ? HP i x ?. apply HP, lookup_union_Some; auto. Qed.
(* stdpp/fin_maps.v *)
Lemma map_Forall_union_2 {A} (m1 m2 : M A) P :
  map_Forall P m1 → map_Forall P m2 → map_Forall P (m1 ∪ m2).
Proof. intros ???? [|[]]%lookup_union_Some_raw; eauto. Qed.
(* stdpp/fin_maps.v *)
Lemma map_Forall_union {A} (m1 m2 : M A) P :
  m1 ##ₘ m2 →
  map_Forall P (m1 ∪ m2) ↔ map_Forall P m1 ∧ map_Forall P m2.
Proof.
  naive_solver eauto using map_Forall_union_1_1,
    map_Forall_union_1_2, map_Forall_union_2.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_filter_union {A} (P : K * A → Prop) `{!∀ x, Decision (P x)} (m1 m2 : M A) :
  m1 ##ₘ m2 →
  filter P (m1 ∪ m2) = filter P m1 ∪ filter P m2.
Proof.
  intros. apply map_eq; intros i. apply option_eq; intros x.
  rewrite lookup_union_Some, !map_lookup_filter_Some,
    lookup_union_Some by auto using map_disjoint_filter.
  naive_solver.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_filter_union_complement {A} (P : K * A → Prop)
    `{!∀ x, Decision (P x)} (m : M A) :
  filter P m ∪ filter (λ v, ¬ P v) m = m.
Proof.
  apply map_eq; intros i. apply option_eq; intros x.
  rewrite lookup_union_Some, !map_lookup_filter_Some
    by auto using map_disjoint_filter_complement.
  destruct (decide (P (i,x))); naive_solver.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_filter_or {A} (P Q : K * A → Prop)
    `{!∀ x, Decision (P x), !∀ x, Decision (Q x)} (m : M A) :
  filter (λ x, P x ∨ Q x) m = filter P m ∪ filter Q m.
Proof.
  apply map_eq. intros k. rewrite lookup_union. rewrite !map_lookup_filter.
  destruct (m !! k); simpl; repeat case_guard; naive_solver.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_fmap_union {A B} (f : A → B) (m1 m2 : M A) :
  f <$> (m1 ∪ m2) = (f <$> m1) ∪ (f <$> m2).
Proof.
  apply map_eq; intros i. apply option_eq; intros x.
  rewrite lookup_fmap, !lookup_union, !lookup_fmap.
  destruct (m1 !! i), (m2 !! i); auto.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_omap_union {A B} (f : A → option B) (m1 m2 : M A) :
  m1 ##ₘ m2 →
  omap f (m1 ∪ m2) = omap f m1 ∪ omap f m2.
Proof.
  intros Hdisj. apply map_eq; intros i. specialize (Hdisj i).
  apply option_eq; intros x.
  rewrite lookup_omap, !lookup_union, !lookup_omap.
  destruct (m1 !! i), (m2 !! i); simpl; repeat (destruct (f _)); naive_solver.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_size_disj_union {A} (m1 m2 : M A) :
  m1 ##ₘ m2 → size (m1 ∪ m2) = size m1 + size m2.
Proof.
  intros Hdisj. induction m1 as [|k x m1 Hm1 IH] using map_ind.
  { rewrite (left_id _ _), map_size_empty. done. }
  rewrite <-insert_union_l.
  rewrite map_size_insert.
  rewrite lookup_union_r by done.
  apply map_disjoint_insert_l in Hdisj as [-> Hdisj].
  rewrite map_size_insert, Hm1.
  rewrite IH by done. done.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_cross_split {A} (ma mb mc md : M A) :
  ma ##ₘ mb → mc ##ₘ md →
  ma ∪ mb = mc ∪ md →
  ∃ mac mad mbc mbd,
    mac ##ₘ mad ∧ mbc ##ₘ mbd ∧
    mac ##ₘ mbc ∧ mad ##ₘ mbd ∧
    mac ∪ mad = ma ∧ mbc ∪ mbd = mb ∧ mac ∪ mbc = mc ∧ mad ∪ mbd = md.
Proof.
  intros Hab_disj Hcd_disj Hab.
  exists (filter (λ kx, is_Some (mc !! kx.1)) ma),
    (filter (λ kx, ¬is_Some (mc !! kx.1)) ma),
    (filter (λ kx, is_Some (mc !! kx.1)) mb),
    (filter (λ kx, ¬is_Some (mc !! kx.1)) mb).
  split_and!; [auto using map_disjoint_filter_complement, map_disjoint_filter,
    map_filter_union_complement..| |].
  - rewrite <-map_filter_union, Hab by done.
    apply map_eq; intros k. apply option_eq; intros x.
    rewrite map_lookup_filter_Some, lookup_union_Some, <-not_eq_None_Some by done.
    rewrite map_disjoint_alt in Hcd_disj; naive_solver.
  - rewrite <-map_filter_union, Hab by done.
    apply map_eq; intros k. apply option_eq; intros x.
    rewrite map_lookup_filter_Some, lookup_union_Some, <-not_eq_None_Some by done.
    rewrite map_disjoint_alt in Hcd_disj; naive_solver.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_disjoint_merge_as_union {A} (m1 m2 : M A) f :
  m1 ##ₘ m2 →
  (∀ x1, f (Some x1) None = Some x1) →
  (∀ x2, f None (Some x2) = Some x2) →
  merge f m1 m2 = m1 ∪ m2.
Proof.
  intros Hdisj ??. apply map_eq; intros k. specialize (Hdisj k).
  rewrite lookup_union, lookup_merge.
  destruct (m1 !! k), (m2 !! k); naive_solver.
Qed.
(* stdpp/fin_maps.v *)
Lemma set_to_map_union {A} `{FinSet K C} (f : K → A) (X Y : C) :
  set_to_map f (X ∪ Y) =@{M A} set_to_map f X ∪ set_to_map f Y.
Proof.
  apply map_eq=> j. apply option_eq=> x.
  rewrite lookup_union_Some_raw, !lookup_set_to_map_Some.
  destruct (decide ((set_to_map f X : M A) !! j = None)) as [|Hj]; [set_solver|].
  rewrite lookup_set_to_map_None.
  rewrite not_eq_None_Some, lookup_set_to_map_is_Some in Hj. set_solver.
Qed.
(* stdpp/fin_maps.v *)
(* The following lemma shows that folding over two maps separately (using the
result of the first fold as input for the second fold) is equivalent to folding
over the union, *if* the function is idempotent for the elements that will be
processed twice ([m1 ∩ m2]) and does not care about the order in which elements
are processed.

This is a generalization of [map_fold_union] (below) with a.) a relation [R]
instead of equality b.) premises that ensure the elements are in [m1 ∪ m2]. *)
Lemma map_fold_union_strong {A B} (R : relation B) `{!PreOrder R}
    (f : K → A → B → B) (b : B) (m1 m2 : M A) :
  (∀ j z, Proper (R ==> R) (f j z)) →
  (∀ j z1 z2 y,
    (** This is morally idempotence for elements of [m1 ∩ m2] *)
    m1 !! j = Some z1 → m2 !! j = Some z2 →
    (** We cannot write this in the usual direction of idempotence properties
    (i.e., [R (f j z1 (f j z2 y)) (f j z1 y)]) because [R] is not symmetric. *)
    R (f j z1 y) (f j z1 (f j z2 y))) →
  (∀ j1 j2 z1 z2 y,
    (** This is morally commutativity + associativity for elements of [m1 ∪ m2] *)
    j1 ≠ j2 →
    m1 !! j1 = Some z1 ∨ m2 !! j1 = Some z1 →
    m1 !! j2 = Some z2 ∨ m2 !! j2 = Some z2 →
    R (f j1 z1 (f j2 z2 y)) (f j2 z2 (f j1 z1 y))) →
  R (map_fold f b (m1 ∪ m2)) (map_fold f (map_fold f b m2) m1).
Proof.
  intros Hf. revert m2.
  induction m1 as [|j x m Hmj IH] using map_ind; intros m2 Hf_idemp Hf_assoc.
  { by rewrite (left_id_L _ _), map_fold_empty. }
  setoid_rewrite lookup_insert_Some in Hf_assoc.
  setoid_rewrite lookup_insert_Some in Hf_idemp.
  rewrite <-insert_union_l, insert_union_r,
    <-insert_delete_eq, <-insert_union_r by done.
  trans (f j x (map_fold f b (m ∪ delete j m2))).
  { apply (map_fold_insert R f); [solve_proper|..].
    - intros j1 j2 z1 z2 y ? Hj1 Hj2.
      apply Hf_assoc; [done|revert Hj1|revert Hj2];
        rewrite lookup_insert_Some, !lookup_union_Some_raw, lookup_delete_Some;
        naive_solver.
    - by rewrite lookup_union, Hmj, lookup_delete_eq. }
  trans (f j x (map_fold f (map_fold f b (delete j m2)) m)).
  { apply Hf, IH.
    - intros j' z1 z2 y ? Hj'. apply Hf_idemp; revert Hj';
        rewrite lookup_delete_Some, ?lookup_insert_Some; naive_solver.
    - intros j1 j2 z1 z2 y ? Hj1 Hj2.
      apply Hf_assoc; [done|revert Hj1|revert Hj2];
        rewrite lookup_delete_Some; clear Hf_idemp Hf_assoc; naive_solver. }
  trans (f j x (map_fold f (map_fold f b m2) m)).
  - destruct (m2 !! j) as [x'|] eqn:?; [|by rewrite delete_id by done].
    trans (f j x (f j x' (map_fold f (map_fold f b (delete j m2)) m))); [by auto|].
    f_equiv. trans (map_fold f (f j x' (map_fold f b (delete j m2))) m).
    + apply (map_fold_comm_acc_strong (flip R)); [solve_proper|].
      intros; apply Hf_assoc;
        rewrite ?lookup_union_Some_raw, ?lookup_insert_Some; naive_solver.
    + apply map_fold_proper; [solve_proper..|].
      apply (map_fold_delete (flip R)); [solve_proper|naive_solver..].
  - apply (map_fold_insert (flip R)); [solve_proper| |done].
    intros j1 j2 z1 z2 y ? Hj1 Hj2.
    apply Hf_assoc; [done|revert Hj2|revert Hj1];
      rewrite !lookup_insert_Some; naive_solver.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_fold_union {A B} (f : K → A → B → B) (b : B) m1 m2 :
  (∀ j z1 z2 y, f j z1 (f j z2 y) = f j z1 y) →
  (∀ j1 j2 z1 z2 y, f j1 z1 (f j2 z2 y) = f j2 z2 (f j1 z1 y)) →
  map_fold f b (m1 ∪ m2) = map_fold f (map_fold f b m2) m1.
Proof. intros. apply (map_fold_union_strong _); [solve_proper|auto..]. Qed.
(* stdpp/fin_maps.v *)
Lemma map_fold_disj_union_strong {A B} (R : relation B) `{!PreOrder R}
    (f : K → A → B → B) (b : B) (m1 m2 : M A) :
  (∀ j z, Proper (R ==> R) (f j z)) →
  m1 ##ₘ m2 →
  (∀ j1 j2 z1 z2 y,
    j1 ≠ j2 →
    m1 !! j1 = Some z1 ∨ m2 !! j1 = Some z1 →
    m1 !! j2 = Some z2 ∨ m2 !! j2 = Some z2 →
    R (f j1 z1 (f j2 z2 y)) (f j2 z2 (f j1 z1 y))) →
  R (map_fold f b (m1 ∪ m2)) (map_fold f (map_fold f b m2) m1).
Proof.
  rewrite map_disjoint_spec. intros ??.
  apply (map_fold_union_strong _); [solve_proper|naive_solver].
Qed.
(* stdpp/fin_maps.v *)
Lemma map_fold_disj_union {A B} (f : K → A → B → B) (b : B) m1 m2 :
  m1 ##ₘ m2 →
  (∀ j1 j2 z1 z2 y, f j1 z1 (f j2 z2 y) = f j2 z2 (f j1 z1 y)) →
  map_fold f b (m1 ∪ m2) = map_fold f (map_fold f b m2) m1.
Proof. intros. apply (map_fold_disj_union_strong _); [solve_proper|auto..]. Qed.
(* stdpp/fin_maps.v *)
(* ** Properties of [map_disjoint_list]. *)
Lemma map_disjoint_list_nil {A} : map_disjoint_list ([] : list (M A)).
Proof. done. Qed.
(* stdpp/fin_maps.v *)
Lemma map_disjoint_list_cons {A} (ms : list (M A)) m :
  map_disjoint_list (m :: ms) ↔ Forall (.##ₘ m) ms ∧ map_disjoint_list ms.
Proof.
  rewrite Forall_lookup. split.
  - intros Hdisj. split.
    + intros j m' ?. by apply (Hdisj (S j) 0).
    + intros j1 j2 m1 m2 ???. apply (Hdisj (S j1) (S j2)); naive_solver.
  - intros [Hall Hms] [|j1] [|j2] m1 m2 Hj ??; simplify_eq/=;
      first [by eauto|by symmetry; eauto].
Qed.
(* stdpp/fin_maps.v *)
Lemma map_disjoint_list_cons_2 {A} (ms : list (M A)) m :
  Forall (.##ₘ m) ms →
  map_disjoint_list ms →
  map_disjoint_list (m :: ms).
Proof. rewrite map_disjoint_list_cons; auto. Qed.
(* stdpp/fin_maps.v *)
Lemma map_disjoint_list_cons_1 {A} (ms : list (M A)) m :
  map_disjoint_list (m :: ms) →
  Forall (.##ₘ m) ms ∧ map_disjoint_list ms.
Proof. apply map_disjoint_list_cons. Qed.
(* stdpp/fin_maps.v *)
Lemma map_disjoint_list_Permutation {A} (ms1 ms2 : list (M A)) :
  map_disjoint_list ms1 → ms1 ≡ₚ ms2 → map_disjoint_list ms2.
Proof.
  pose proof Permutation_Forall as Hhelp. unfold Proper, respectful in Hhelp.
  intros Hdisj Hperm. revert Hdisj.
  induction Hperm; rewrite ?map_disjoint_list_cons, ?Forall_cons; naive_solver.
Qed.
(* stdpp/fin_maps.v *)
Instance map_disjoint_list_Permutation_proper {A} :
  Proper ((≡ₚ) ==> iff) (map_disjoint_list (K:=K) (M:=M) (A:=A)).
Proof.
  intros ms1 ms2 ?; split; intros ?; by eapply map_disjoint_list_Permutation.
Qed.
(* stdpp/fin_maps.v *)
(* ** Properties of the [union_list] operation *)
Lemma map_disjoint_union_list_l {A} (ms : list (M A)) (m : M A) :
  ⋃ ms ##ₘ m ↔ Forall (.##ₘ m) ms.
Proof.
  split.
  - induction ms; simpl; rewrite ?map_disjoint_union_l; intuition.
  - induction 1; simpl; [apply map_disjoint_empty_l |].
    by rewrite map_disjoint_union_l.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_disjoint_union_list_r {A} (ms : list (M A)) (m : M A) :
  m ##ₘ ⋃ ms ↔ Forall (.##ₘ m) ms.
Proof. by rewrite (symmetry_iff map_disjoint), map_disjoint_union_list_l. Qed.
(* stdpp/fin_maps.v *)
Lemma map_disjoint_union_list_l_2 {A} (ms : list (M A)) (m : M A) :
  Forall (.##ₘ m) ms → ⋃ ms ##ₘ m.
Proof. by rewrite map_disjoint_union_list_l. Qed.
(* stdpp/fin_maps.v *)
Lemma map_disjoint_union_list_r_2 {A} (ms : list (M A)) (m : M A) :
  Forall (.##ₘ m) ms → m ##ₘ ⋃ ms.
Proof. by rewrite map_disjoint_union_list_r. Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_union_list_None {A} (ms : list (M A)) i :
  ⋃ ms !! i = None ↔ Forall (λ m, m !! i = None) ms.
Proof.
  induction ms as [|m ms IH]; simpl.
  { by rewrite lookup_empty, Forall_nil. }
  rewrite lookup_union_None, Forall_cons. naive_solver.
Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_union_list_None_1 {A} (ms : list (M A)) i :
  ⋃ ms !! i = None → Forall (λ m, m !! i = None) ms.
Proof. apply lookup_union_list_None. Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_union_list_None_2 {A} (ms : list (M A)) i :
  Forall (λ m, m !! i = None) ms → ⋃ ms !! i = None.
Proof. apply lookup_union_list_None. Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_union_list_Some_1 {A} (ms : list (M A)) i x :
  ⋃ ms !! i = Some x → ∃ m, m ∈ ms ∧ m !! i = Some x.
Proof.
  rewrite <-Exists_exists. induction ms as [|m ms IH]; simpl.
  { by rewrite lookup_empty, Exists_nil. }
  rewrite lookup_union_Some_raw, Exists_cons. naive_solver.
Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_union_list_Some_2 {A} (ms : list (M A)) m i x :
  m ∈ ms →
  map_disjoint_list ms →
  m !! i = Some x →
  ⋃ ms !! i = Some x.
Proof.
  induction ms as [|m' ms IH]; simpl; [by rewrite elem_of_nil|].
  intros ?%elem_of_cons [?%map_disjoint_union_list_r ?]%map_disjoint_list_cons ?.
  rewrite lookup_union_Some by done. naive_solver.
Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_union_list_Some {A} (ms : list (M A)) i x :
  map_disjoint_list ms →
  ⋃ ms !! i = Some x ↔ ∃ m, m ∈ ms ∧ m !! i = Some x.
Proof.
  naive_solver eauto using lookup_union_list_Some_1, lookup_union_list_Some_2.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_union_list_Permutation {A} (ms1 ms2 : list (M A)) :
  ms1 ≡ₚ ms2 →
  map_disjoint_list ms1 →
  ⋃ ms1 = ⋃ ms2.
Proof.
  induction 1 as [|m ms1 ms2 ? IH|m1 m2 ms|ms1 ms2 ms3 ? IH1 ? IH2]; simpl.
  - done.
  - intros [??]%map_disjoint_list_cons. f_equal; auto.
  - intros [[??]%Forall_cons [??]%map_disjoint_list_cons]%map_disjoint_list_cons.
    by rewrite !(assoc_L _), (map_union_comm m1) by done.
  - intros. trans (⋃ ms2); eauto using map_disjoint_list_Permutation.
Qed.
(* stdpp/fin_maps.v *)
(* ** Properties of the folding the [delete] function *)
Lemma lookup_foldr_delete {A} (m : M A) js j :
  j ∈ js → foldr delete m js !! j = None.
Proof. induction 1; simpl; rewrite lookup_delete; case_decide; naive_solver. Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_foldr_delete_not_elem_of {A} (m : M A) js j :
  j ∉ js → foldr delete m js !! j = m !! j.
Proof.
  induction js; simpl; [done |]. rewrite elem_of_cons; intros.
  rewrite lookup_delete_ne; intuition.
Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_foldr_delete_Some {A} (m : M A) js j y :
  foldr delete m js !! j = Some y ↔ j ∉ js ∧ m !! j = Some y.
Proof. induction js; simpl; rewrite ?lookup_delete_Some; set_solver. Qed.
(* stdpp/fin_maps.v *)
Lemma foldr_delete_id {A} (m : M A) js :
  Forall (λ i, m !! i = None) js → foldr delete m js = m.
Proof. induction 1; simpl; [done |]. rewrite delete_id; congruence. Qed.
(* stdpp/fin_maps.v *)
Lemma delete_foldr_delete {A} (m : M A) js j :
  delete j (foldr delete m js) = foldr delete (delete j m) js.
Proof.
  induction js as [|?? IH]; simpl; [done|]. by rewrite delete_delete, IH.
Qed.
(* stdpp/fin_maps.v *)
Lemma foldr_delete_insert_in {A} (m : M A) js j x :
  j ∈ js → foldr delete (<[j:=x]> m) js = foldr delete m js.
Proof.
  induction 1 as [i js|j i js ? IH]; simpl; [|by rewrite IH].
  by rewrite !delete_foldr_delete, delete_insert_eq.
Qed.
(* stdpp/fin_maps.v *)
Lemma foldr_delete_insert_notin {A} (m : M A) js j x :
  j ∉ js → foldr delete (<[j:=x]> m) js = <[j:=x]>(foldr delete m js).
Proof.
  induction js as [|?? IHjs]; simpl; [done |]. rewrite elem_of_cons. intros.
  rewrite IHjs, delete_insert_ne; intuition.
Qed.
(* stdpp/fin_maps.v *)
Lemma foldr_delete_insert {A} (m : M A) js j x :
  foldr delete (<[j:=x]> m) js =
    if decide (j ∈ js) then foldr delete m js else <[j:=x]>(foldr delete m js).
Proof.
  case_decide; auto using foldr_delete_insert_in, foldr_delete_insert_notin.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_disjoint_foldr_delete_l {A} (m1 m2 : M A) js :
  m1 ##ₘ m2 → foldr delete m1 js ##ₘ m2.
Proof. induction js; simpl; auto using map_disjoint_delete_l. Qed.
(* stdpp/fin_maps.v *)
Lemma map_disjoint_foldr_delete_r {A} (m1 m2 : M A) js :
  m1 ##ₘ m2 → m1 ##ₘ foldr delete m2 js.
Proof. induction js; simpl; auto using map_disjoint_delete_r. Qed.
(* stdpp/fin_maps.v *)
Lemma map_agree_foldr_delete_l {A} (m1 m2 : M A) js :
  map_agree m1 m2 → map_agree (foldr delete m1 js) m2.
Proof. induction js; simpl; auto using map_agree_delete_l. Qed.
(* stdpp/fin_maps.v *)
Lemma map_agree_foldr_delete_r {A} (m1 m2 : M A) js :
  map_agree m1 m2 → map_agree m1 (foldr delete m2 js).
Proof. induction js; simpl; auto using map_agree_delete_r. Qed.
(* stdpp/fin_maps.v *)
Lemma foldr_delete_union {A} (m1 m2 : M A) js :
  foldr delete (m1 ∪ m2) js = foldr delete m1 js ∪ foldr delete m2 js.
Proof. apply foldr_delete_union_with. Qed.
(* stdpp/fin_maps.v *)
(* ** Properties on conversion to lists that depend on [∪] and [##ₘ] *)
Lemma list_to_map_app {A} (l1 l2 : list (K * A)):
  list_to_map (l1 ++ l2) =@{M A} list_to_map l1 ∪ list_to_map l2.
Proof.
  induction l1 as [|[??] ? IH]; simpl.
  { by rewrite (left_id _ _). }
  by rewrite IH, insert_union_l.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_disjoint_list_to_map_l {A} (m : M A) ixs :
  list_to_map ixs ##ₘ m ↔ Forall (λ ix, m !! ix.1 = None) ixs.
Proof.
  split.
  - induction ixs; simpl; rewrite ?map_disjoint_insert_l in *; intuition.
  - induction 1; simpl; [apply map_disjoint_empty_l|].
    rewrite map_disjoint_insert_l. auto.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_disjoint_list_to_map_r {A} (m : M A) ixs :
  m ##ₘ list_to_map ixs ↔ Forall (λ ix, m !! ix.1 = None) ixs.
Proof. by rewrite (symmetry_iff map_disjoint), map_disjoint_list_to_map_l. Qed.
(* stdpp/fin_maps.v *)
Lemma map_disjoint_list_to_map_zip_l {A} (m : M A) js xs :
  length js = length xs →
  list_to_map (zip js xs) ##ₘ m ↔ Forall (λ i, m !! i = None) js.
Proof.
  intro. rewrite map_disjoint_list_to_map_l.
  rewrite <-(fst_zip js xs) at 2 by lia. by rewrite Forall_fmap.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_disjoint_list_to_map_zip_r {A} (m : M A) js xs :
  length js = length xs →
  m ##ₘ list_to_map (zip js xs) ↔ Forall (λ i, m !! i = None) js.
Proof.
  intro. by rewrite (symmetry_iff map_disjoint), map_disjoint_list_to_map_zip_l.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_disjoint_list_to_map_zip_l_2 {A} (m : M A) js xs :
  length js = length xs → Forall (λ i, m !! i = None) js →
  list_to_map (zip js xs) ##ₘ m.
Proof. intro. by rewrite map_disjoint_list_to_map_zip_l. Qed.
(* stdpp/fin_maps.v *)
Lemma map_disjoint_list_to_map_zip_r_2 {A} (m : M A) js xs :
  length js = length xs → Forall (λ i, m !! i = None) js →
  m ##ₘ list_to_map (zip js xs).
Proof. intro. by rewrite map_disjoint_list_to_map_zip_r. Qed.
(* stdpp/fin_maps.v *)
Lemma map_Forall2_union_inv_l {A B} (R : K → A → B → Prop)
    (m1a m1b : M A) (m2 : M B) :
  m1a ##ₘ m1b →
  map_Forall2 R (m1a ∪ m1b) m2 →
  ∃ m2a m2b, m2 = m2a ∪ m2b ∧ map_Forall2 R m1a m2a ∧ map_Forall2 R m1b m2b.
Proof.
  revert m2 m1b.
  induction m1a as [|k x1 m1a ? IH] using map_ind; intros m1 m2b Hdisj Hm.
  { rewrite (left_id_L _ _) in Hm.
    exists ∅, m1. rewrite (left_id_L ∅ _). auto using map_Forall2_empty. }
  apply map_disjoint_insert_l in Hdisj as [? Hdisj].
  rewrite <-insert_union_l in Hm.
  apply map_Forall2_insert_inv_l in Hm as (x2 & m2' & -> & Hk & ? & Hm);
    [|by rewrite lookup_union, union_None].
  apply IH in Hm as (m2a' & m2b' & -> & Hm1 & Hm2); [|done].
  rewrite lookup_union, union_None in Hk; destruct Hk as [??].
  exists (<[k:=x2]> m2a'), m2b'. split_and!.
  - by rewrite insert_union_l.
  - apply map_Forall2_insert; auto.
  - done.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_Forall2_union_inv_r {A B} (R : K → A → B → Prop)
    (m1 : M A) (m2a m2b : M B) :
  m2a ##ₘ m2b → map_Forall2 R m1 (m2a ∪ m2b) →
  ∃ m1a m1b, m1 = m1a ∪ m1b ∧ map_Forall2 R m1a m2a ∧ map_Forall2 R m1b m2b.
Proof. setoid_rewrite <-map_Forall2_flip. apply map_Forall2_union_inv_l. Qed.
(* stdpp/fin_maps.v *)
Instance : LeftAbsorb (=@{M A}) ∅ (intersection_with f).
Proof. unfold intersection_with, map_intersection_with. apply _. Qed.
(* stdpp/fin_maps.v *)
Instance : RightAbsorb (=@{M A}) ∅ (intersection_with f).
Proof. unfold intersection_with, map_intersection_with. apply _. Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_intersection_with m1 m2 i :
    intersection_with f m1 m2 !! i = intersection_with f (m1 !! i) (m2 !! i).
Proof.
    unfold intersection_with, map_intersection_with. rewrite lookup_merge.
    by destruct (m1 !! i), (m2 !! i).
  Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_intersection_with_Some m1 m2 i z :
    intersection_with f m1 m2 !! i = Some z ↔
      (∃ x y, m1 !! i = Some x ∧ m2 !! i = Some y ∧ f x y = Some z).
Proof.
    rewrite lookup_intersection_with.
    destruct (m1 !! i), (m2 !! i); compute; naive_solver.
  Qed.
(* stdpp/fin_maps.v *)
Lemma intersection_with_comm m1 m2 :
    (∀ i x y, m1 !! i = Some x → m2 !! i = Some y → f x y = f y x) →
    intersection_with f m1 m2 = intersection_with f m2 m1.
Proof.
    intros. apply (merge_comm _). intros i.
    destruct (m1 !! i) eqn:?, (m2 !! i) eqn:?; simpl; eauto.
  Qed.
(* stdpp/fin_maps.v *)
Instance : Comm (=) f → Comm (=@{M A}) (intersection_with f).
Proof. intros ???. apply intersection_with_comm. eauto. Qed.
(* stdpp/fin_maps.v *)
Lemma intersection_with_idemp m :
    (∀ i x, m !! i = Some x → f x x = Some x) → intersection_with f m m = m.
Proof.
    intros. apply (merge_idemp _). intros i.
    destruct (m !! i) eqn:?; simpl; eauto.
  Qed.