phanerozoic/Coq-Stdpp huggingface dataset:
(* stdpp/fin_maps.v *)
Lemma alter_intersection_with (g : A → A) m1 m2 i :
    (∀ x y, m1 !! i = Some x → m2 !! i = Some y → g <$> f x y = f (g x) (g y)) →
    alter g i (intersection_with f m1 m2) =
      intersection_with f (alter g i m1) (alter g i m2).
Proof.
    intros. apply (partial_alter_merge _).
    destruct (m1 !! i) eqn:?, (m2 !! i) eqn:?; simpl; eauto.
  Qed.
(* stdpp/fin_maps.v *)
Lemma delete_intersection_with m1 m2 i :
    delete i (intersection_with f m1 m2) =
      intersection_with f (delete i m1) (delete i m2).
Proof. by apply (partial_alter_merge _). Qed.
(* stdpp/fin_maps.v *)
Lemma foldr_delete_intersection_with (m1 m2 : M A) js :
    foldr delete (intersection_with f m1 m2) js =
      intersection_with f (foldr delete m1 js) (foldr delete m2 js).
Proof.
    induction js as [|?? IHjs]; simpl; [done|].
    by rewrite IHjs, delete_intersection_with.
  Qed.
(* stdpp/fin_maps.v *)
Lemma insert_intersection_with m1 m2 i x y z :
    f x y = Some z →
    <[i:=z]>(intersection_with f m1 m2) =
      intersection_with f (<[i:=x]> m1) (<[i:=y]> m2).
Proof. by intros; apply (partial_alter_merge _). Qed.
(* stdpp/fin_maps.v *)
(* ** Properties of the [intersection] operation *)
Instance map_empty_intersection {A} : LeftAbsorb (=@{M A}) ∅ (∩)
:= _.
(* stdpp/fin_maps.v *)
Instance map_intersection_empty {A} : RightAbsorb (=@{M A}) ∅ (∩)
:= _.
(* stdpp/fin_maps.v *)
Instance map_intersection_assoc {A} : Assoc (=@{M A}) (∩).
Proof.
  intros m1 m2 m3.
  unfold intersection, map_intersection, intersection_with, map_intersection_with.
  apply (merge_assoc _). intros i.
  by destruct (m1 !! i), (m2 !! i), (m3 !! i).
Qed.
(* stdpp/fin_maps.v *)
Instance map_intersection_idemp {A} : IdemP (=@{M A}) (∩).
Proof. intros ?. by apply intersection_with_idemp. Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_intersection {A} (m1 m2 : M A) i :
  (m1 ∩ m2) !! i = m1 !! i ∩ m2 !! i.
Proof.
  apply lookup_intersection_with.
Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_intersection_Some {A} (m1 m2 : M A) i x :
  (m1 ∩ m2) !! i = Some x ↔ m1 !! i = Some x ∧ is_Some (m2 !! i).
Proof.
  unfold intersection, map_intersection. rewrite lookup_intersection_with.
  destruct (m1 !! i), (m2 !! i); compute; naive_solver.
Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_intersection_None {A} (m1 m2 : M A) i :
  (m1 ∩ m2) !! i = None ↔ m1 !! i = None ∨ m2 !! i = None.
Proof.
  unfold intersection, map_intersection. rewrite lookup_intersection_with.
  destruct (m1 !! i), (m2 !! i); compute; naive_solver.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_intersection_filter {A} (m1 m2 : M A) :
  m1 ∩ m2 = filter (λ kx, is_Some (m1 !! kx.1) ∧ is_Some (m2 !! kx.1)) (m1 ∪ m2).
Proof.
  apply map_eq; intros i. apply option_eq; intros x.
  rewrite lookup_intersection_Some, map_lookup_filter_Some, lookup_union; simpl.
  unfold is_Some. destruct (m1 !! i), (m2 !! i); naive_solver.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_filter_and {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_intersection. rewrite !map_lookup_filter.
  destruct (m !! k); simpl; repeat case_guard; naive_solver.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_fmap_intersection {A B} (f : A → B) (m1 m2 : M A) :
  f <$> (m1 ∩ m2) = (f <$> m1) ∩ (f <$> m2).
Proof.
  apply map_eq. intros i.
  rewrite !lookup_intersection, !lookup_fmap, !lookup_intersection.
  destruct (m1 !! i), (m2 !! i); done.
Qed.
(* stdpp/fin_maps.v *)
(* ** Properties of the [difference_with] operation *)
Lemma lookup_difference_with {A} (f : A → A → option A) (m1 m2 : M A) i :
  difference_with f m1 m2 !! i = difference_with f (m1 !! i) (m2 !! i).
Proof.
  unfold difference_with, map_difference_with. rewrite lookup_merge.
  by destruct (m1 !! i), (m2 !! i).
Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_difference_with_Some {A} (f : A → A → option A) (m1 m2 : M A) i z :
  difference_with f m1 m2 !! i = Some z ↔
    (m1 !! i = Some z ∧ m2 !! i = None) ∨
    (∃ x y, m1 !! i = Some x ∧ m2 !! i = Some y ∧ f x y = Some z).
Proof.
  rewrite lookup_difference_with.
  destruct (m1 !! i), (m2 !! i); compute; naive_solver.
Qed.
(* stdpp/fin_maps.v *)
Lemma set_to_map_intersection {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_intersection_Some,
    !lookup_set_to_map_Some, lookup_set_to_map_is_Some.
  set_solver.
Qed.
(* stdpp/fin_maps.v *)
(* ** Properties of the [difference] operation *)
Lemma lookup_difference {A} (m1 m2 : M A) i :
  (m1 ∖ m2) !! i = match m2 !! i with None => m1 !! i | _ => None end.
Proof.
  unfold difference, map_difference; rewrite lookup_difference_with.
  destruct (m1 !! i), (m2 !! i); done.
Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_difference_Some {A} (m1 m2 : M A) i x :
  (m1 ∖ m2) !! i = Some x ↔ m1 !! i = Some x ∧ m2 !! i = None.
Proof. rewrite lookup_difference. destruct (m1 !! i), (m2 !! i); naive_solver. Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_difference_is_Some {A} (m1 m2 : M A) i :
  is_Some ((m1 ∖ m2) !! i) ↔ is_Some (m1 !! i) ∧ m2 !! i = None.
Proof. unfold is_Some. setoid_rewrite lookup_difference_Some. naive_solver. Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_difference_None {A} (m1 m2 : M A) i :
  (m1 ∖ m2) !! i = None ↔ m1 !! i = None ∨ is_Some (m2 !! i).
Proof.
  rewrite lookup_difference.
  destruct (m1 !! i), (m2 !! i); compute; naive_solver.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_disjoint_difference_l1 {A} (m1 m2 m3 : M A) : m3 ⊆ m2 → m1 ∖ m2 ##ₘ m3.
Proof.
  intros Hm i; specialize (Hm i).
  unfold difference, map_difference; rewrite lookup_difference_with.
  by destruct (m1 !! i), (m2 !! i), (m3 !! i).
Qed.
(* stdpp/fin_maps.v *)
Lemma map_disjoint_difference_r1 {A} (m1 m2 m3 : M A) : m3 ⊆ m2 → m3 ##ₘ m1 ∖ m2.
Proof. intros. symmetry. by apply map_disjoint_difference_l1. Qed.
(* stdpp/fin_maps.v *)
Lemma map_subseteq_difference_l {A} (m1 m2 m : M A) : m1 ⊆ m → m1 ∖ m2 ⊆ m.
Proof.
  rewrite !map_subseteq_spec. setoid_rewrite lookup_difference_Some. naive_solver.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_difference_union {A} (m1 m2 : M A) :
  m1 ⊆ m2 → m1 ∪ m2 ∖ m1 = m2.
Proof.
  rewrite map_subseteq_spec. intro Hm1m2. apply map_eq. intros i.
  apply option_eq. intros v. specialize (Hm1m2 i).
  unfold difference, map_difference, difference_with, map_difference_with.
  rewrite lookup_union_Some_raw, lookup_merge.
  destruct (m1 !! i) as [x'|], (m2 !! i);
    try specialize (Hm1m2 x'); compute; intuition congruence.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_difference_union_distr_l {A} (m1 m2 m3 : M A) :
  (m1 ∪ m2) ∖ m3 = m1 ∖ m3 ∪ m2 ∖ m3.
Proof.
  apply map_eq. intros i.
  rewrite !lookup_union, !lookup_difference, !lookup_union.
  by repeat destruct (_ !! _).
Qed.
(* stdpp/fin_maps.v *)
Lemma map_difference_union_distr_r {A} (m1 m2 m3 : M A) :
  m1 ∖ (m2 ∪ m3) = (m1 ∖ m2) ∩ (m1 ∖ m3).
Proof.
  apply map_eq. intros i.
  rewrite lookup_intersection, !lookup_difference, !lookup_union.
  by repeat destruct (_ !! _).
Qed.
(* stdpp/fin_maps.v *)
Lemma map_empty_difference {A} (m : M A) :
  ∅ ∖ m = ∅.
Proof.
  apply map_eq. intros i.
  rewrite lookup_difference, !lookup_empty.
  by repeat destruct (_ !! _).
Qed.
(* stdpp/fin_maps.v *)
Lemma map_difference_disjoint {A} (m1 m2 : M A) :
  m1 ##ₘ m2 → m1 ∖ m2 = m1.
Proof.
  intros Hdisj. rewrite map_disjoint_spec in Hdisj. apply map_eq. intros i.
  specialize (Hdisj i). rewrite lookup_difference.
  repeat destruct (_ !! _); naive_solver.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_disjoint_difference_l2 {A} (m1 m2 m3 : M A):
  m1 ##ₘ m2 → m1 ∖ m3 ##ₘ m2.
Proof.
  rewrite !map_disjoint_spec. intros Hdisj k x1 x2 Hx1 Hx2.
  rewrite lookup_difference in Hx1. destruct (m3 !! k); naive_solver.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_disjoint_difference_r2 {A} (m1 m2 m3 : M A):
  m1 ##ₘ m2 → m1 ##ₘ m2 ∖ m3.
Proof. intros. symmetry. by apply map_disjoint_difference_l2. Qed.
(* stdpp/fin_maps.v *)
Lemma map_difference_diag {A} (m : M A) : m ∖ m = ∅.
Proof.
  apply map_empty; intros i. rewrite lookup_difference_None.
  destruct (m !! i); eauto.
Qed.
(* stdpp/fin_maps.v *)
Instance map_difference_right_id {A} : RightId (=@{M A}) ∅ (∖)
:= _.
(* stdpp/fin_maps.v *)
Lemma map_difference_empty {A} (m : M A) : m ∖ ∅ = m.
Proof. by rewrite (right_id _ _). Qed.
(* stdpp/fin_maps.v *)
Lemma map_fmap_difference {A B} (f : A → B) (m1 m2 : M A) :
  f <$> (m1 ∖ m2) = (f <$> m1) ∖ (f <$> m2).
Proof.
  apply map_eq. intros i.
  rewrite !lookup_difference, !lookup_fmap, !lookup_difference.
  destruct (m1 !! i), (m2 !! i); done.
Qed.
(* stdpp/fin_maps.v *)
Lemma insert_difference {A} (m1 m2 : M A) i x :
  <[i:=x]> (m1 ∖ m2) = <[i:=x]> m1 ∖ delete i m2.
Proof.
  intros. apply map_eq. intros j. apply option_eq. intros y.
  rewrite lookup_insert_Some, !lookup_difference_Some,
    lookup_insert_Some, lookup_delete_None.
  naive_solver.
Qed.
(* stdpp/fin_maps.v *)
Lemma insert_difference' {A} (m1 m2 : M A) i x :
  m2 !! i = None → <[i:=x]> (m1 ∖ m2) = <[i:=x]> m1 ∖ m2.
Proof. intros. by rewrite insert_difference, delete_id. Qed.
(* stdpp/fin_maps.v *)
Lemma difference_insert {A} (m1 m2 : M A) i x1 x2 x3 :
  <[i:=x1]> m1 ∖ <[i:=x2]> m2 = m1 ∖ <[i:=x3]> m2.
Proof.
  apply map_eq. intros i'. apply option_eq. intros x'.
  rewrite !lookup_difference_Some, !lookup_insert_Some, !lookup_insert_None.
  naive_solver.
Qed.
(* stdpp/fin_maps.v *)
Lemma difference_insert_subseteq {A} (m1 m2 : M A) i x1 x2 :
  <[i:=x1]> m1 ∖ <[i:=x2]> m2 ⊆ m1 ∖ m2.
Proof.
  apply map_subseteq_spec. intros i' x'.
  rewrite !lookup_difference_Some, lookup_insert_Some, lookup_insert_None.
  naive_solver.
Qed.
(* stdpp/fin_maps.v *)
Lemma delete_difference {A} (m1 m2 : M A) i x :
  delete i (m1 ∖ m2) = m1 ∖ <[i:=x]> m2.
Proof.
  apply map_eq. intros j. apply option_eq. intros y.
  rewrite lookup_delete_Some, !lookup_difference_Some, lookup_insert_None.
  naive_solver.
Qed.
(* stdpp/fin_maps.v *)
Lemma difference_delete {A} (m1 m2 : M A) i x :
  m1 !! i = Some x →
  m1 ∖ delete i m2 = <[i:=x]> (m1 ∖ m2).
Proof.
  intros. apply map_eq. intros j. apply option_eq. intros y.
  rewrite lookup_insert_Some, !lookup_difference_Some, lookup_delete_None.
  destruct (decide (i = j)); naive_solver.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_difference_filter {A} (m1 m2 : M A) :
  m1 ∖ m2 = filter (λ kx, m2 !! kx.1 = None) m1.
Proof.
  apply map_eq; intros i. apply option_eq; intros x.
  by rewrite lookup_difference_Some, map_lookup_filter_Some.
Qed.
(* stdpp/fin_maps.v *)
Lemma set_to_map_difference {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_difference_Some,
    !lookup_set_to_map_Some, lookup_set_to_map_None.
  set_solver.
Qed.
(* stdpp/fin_maps.v *)
(* ** Misc properties about the order *)
Lemma map_subseteq_inv {A} (m1 m2 : M A) : m1 ⊆ m2 → m1 ⊂ m2 ∨ m1 = m2.
Proof.
  intros. destruct (decide (m2 ∖ m1 = ∅)) as [Hm21|(i&x&Hi)%map_choose].
  - right. by rewrite <-(map_difference_union m1 m2), Hm21, (right_id_L _ _).
  - left. apply lookup_difference_Some in Hi as [??].
    apply map_subset_alt; eauto.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_equiv_iff (m1 m2 : M A) : m1 ≡ m2 ↔ ∀ i, m1 !! i ≡ m2 !! i.
Proof. done. Qed.
(* stdpp/fin_maps.v *)
Lemma map_equiv_lookup_l (m1 m2 : M A) i x :
    m1 ≡ m2 → m1 !! i = Some x → ∃ y, m2 !! i = Some y ∧ x ≡ y.
Proof. intros Hm Hi. destruct (Hm i); naive_solver. Qed.
(* stdpp/fin_maps.v *)
Lemma map_equiv_lookup_r (m1 m2 : M A) i y :
    m1 ≡ m2 → m2 !! i = Some y → ∃ x, m1 !! i = Some x ∧ x ≡ y.
Proof. intros Hm Hi. destruct (Hm i); naive_solver. Qed.
(* stdpp/fin_maps.v *)
Instance map_equivalence : Equivalence (≡@{A}) → Equivalence (≡@{M A}).
Proof.
    split.
    - by intros m i.
    - by intros m1 m2 ? i.
    - by intros m1 m2 m3 ?? i; trans (m2 !! i).
  Qed.
(* stdpp/fin_maps.v *)
Instance map_leibniz `{!LeibnizEquiv A} : LeibnizEquiv (M A).
Proof. intros m1 m2 Hm; apply map_eq; intros i. apply leibniz_equiv, Hm. Qed.
(* stdpp/fin_maps.v *)
Instance lookup_proper (i : K) : Proper ((≡@{M A}) ==> (≡)) (lookup i).
Proof. by intros m1 m2 Hm. Qed.
(* stdpp/fin_maps.v *)
Instance lookup_total_proper (i : K) `{!Inhabited A} :
    Proper (≡@{A}) inhabitant →
    Proper ((≡@{M A}) ==> (≡)) (.!!! i).
Proof.
    intros ? m1 m2 Hm. unfold lookup_total, map_lookup_total.
    apply from_option_proper; auto. by intros ??.
  Qed.
(* stdpp/fin_maps.v *)
Instance partial_alter_proper :
    Proper (((≡) ==> (≡)) ==> (=) ==> (≡) ==> (≡@{M A})) partial_alter.
Proof.
    intros f1 f2 Hf i ? <- m1 m2 Hm j.
    rewrite !lookup_partial_alter; case_decide;
      try apply Hf; by apply lookup_proper.
  Qed.
(* stdpp/fin_maps.v *)
Instance insert_proper (i : K) :
    Proper ((≡) ==> (≡) ==> (≡@{M A})) (insert i).
Proof. by intros ???; apply partial_alter_proper; [constructor|]. Qed.
(* stdpp/fin_maps.v *)
Instance singletonM_proper k : Proper ((≡) ==> (≡@{M A})) (singletonM k).
Proof.
    intros ???; apply insert_proper; [done|].
    intros ?. rewrite lookup_empty; constructor.
  Qed.
(* stdpp/fin_maps.v *)
Instance delete_proper (i : K) : Proper ((≡) ==> (≡@{M A})) (delete i).
Proof. by apply partial_alter_proper; [constructor|]. Qed.
(* stdpp/fin_maps.v *)
Instance alter_proper :
    Proper (((≡) ==> (≡)) ==> (=) ==> (≡) ==> (≡@{M A})) alter.
Proof.
    intros ?? Hf; apply partial_alter_proper.
    by destruct 1; constructor; apply Hf.
  Qed.
(* stdpp/fin_maps.v *)
Instance merge_proper `{Equiv B, Equiv C} :
    Proper (((≡) ==> (≡) ==> (≡)) ==> (≡@{M A}) ==> (≡@{M B}) ==> (≡@{M C})) merge.
Proof.
    intros ?? Hf ?? Hm1 ?? Hm2 i. rewrite !lookup_merge.
    destruct (Hm1 i), (Hm2 i); try apply Hf; by constructor.
  Qed.
(* stdpp/fin_maps.v *)
Instance union_with_proper :
    Proper (((≡) ==> (≡) ==> (≡)) ==> (≡) ==> (≡) ==>(≡@{M A})) union_with.
Proof.
    intros ?? Hf. apply merge_proper.
    by do 2 destruct 1; first [apply Hf | constructor].
  Qed.
(* stdpp/fin_maps.v *)
Instance intersection_with_proper :
    Proper (((≡) ==> (≡) ==> (≡)) ==> (≡) ==> (≡) ==>(≡@{M A})) intersection_with.
Proof.
    intros ?? Hf. apply merge_proper.
    by do 2 destruct 1; first [apply Hf | constructor].
  Qed.
(* stdpp/fin_maps.v *)
Instance difference_with_proper :
    Proper (((≡) ==> (≡) ==> (≡)) ==> (≡) ==> (≡) ==>(≡@{M A})) difference_with.
Proof.
    intros ?? Hf. apply merge_proper.
    by do 2 destruct 1; first [apply Hf | constructor].
  Qed.
(* stdpp/fin_maps.v *)
Instance union_proper : Proper ((≡) ==> (≡) ==>(≡@{M A})) union.
Proof. apply union_with_proper; solve_proper. Qed.
(* stdpp/fin_maps.v *)
Instance intersection_proper : Proper ((≡) ==> (≡) ==>(≡@{M A})) intersection.
Proof. apply intersection_with_proper; solve_proper. Qed.
(* stdpp/fin_maps.v *)
Instance difference_proper : Proper ((≡) ==> (≡) ==>(≡@{M A})) difference.
Proof. apply difference_with_proper. constructor. Qed.
(* stdpp/fin_maps.v *)
Instance map_zip_with_proper `{Equiv B, Equiv C} :
    Proper (((≡) ==> (≡) ==> (≡)) ==> (≡@{M A}) ==> (≡@{M B}) ==> (≡@{M C}))
      map_zip_with.
Proof.
    intros f1 f2 Hf. apply merge_proper.
    destruct 1; destruct 1; repeat f_equiv; constructor || by apply Hf.
  Qed.
(* stdpp/fin_maps.v *)
Instance map_disjoint_proper :
    Proper ((≡@{M A}) ==> (≡@{M A}) ==> iff) map_disjoint.
Proof.
    intros m1 m1' Hm1 m2 m2' Hm2; split;
      intros Hm i; specialize (Hm i); by destruct (Hm1 i), (Hm2 i).
  Qed.
(* stdpp/fin_maps.v *)
Instance map_fmap_proper `{Equiv B} :
    Proper (((≡) ==> (≡)) ==> (≡@{M A}) ==> (≡@{M B})) fmap.
Proof.
    intros f f' Hf m m' ? k; rewrite !lookup_fmap. by apply option_fmap_proper.
  Qed.
(* stdpp/fin_maps.v *)
Instance map_omap_proper `{Equiv B} :
    Proper (((≡) ==> (≡)) ==> (≡@{M A}) ==> (≡@{M B})) omap.
Proof.
    intros f f' ? m m' ? k; rewrite !lookup_omap. by apply option_bind_proper.
  Qed.
(* stdpp/fin_maps.v *)
Instance map_filter_proper (P : K * A → Prop) `{!∀ kx, Decision (P kx)} :
    (∀ k, Proper ((≡) ==> iff) (curry P k)) →
    Proper ((≡@{M A}) ==> (≡)) (filter P).
Proof.
    intros ? m1 m2 Hm i. rewrite !map_lookup_filter.
    destruct (Hm i); simpl; repeat case_guard; try constructor; naive_solver.
  Qed.
(* stdpp/fin_maps.v *)
Instance map_singleton_equiv_inj :
    Inj2 (=) (≡) (≡) (singletonM (M:=M A)).
Proof.
    intros i1 x1 i2 x2 Heq. specialize (Heq i1).
    rewrite !lookup_singleton in Heq.
    repeat case_decide; try inversion Heq; naive_solver.
  Qed.
(* stdpp/fin_maps.v *)
Instance map_fmap_equiv_inj `{Equiv B} (f : A → B) :
    Inj (≡) (≡) f → Inj (≡@{M A}) (≡@{M B}) (fmap f).
Proof.
    intros ? m1 m2 Hm i. apply (inj (fmap (M:=option) f)).
    rewrite <-!lookup_fmap. by apply Hm.
  Qed.
(* stdpp/fin_maps.v *)
Lemma map_fmap_equiv_ext `{Equiv B} (f1 f2 : A → B) (m : M A) :
    (∀ i x, m !! i = Some x → f1 x ≡ f2 x) → f1 <$> m ≡ f2 <$> m.
Proof.
    intros Hi i; rewrite !lookup_fmap.
    destruct (m !! i) eqn:?; constructor; eauto.
  Qed.
(* stdpp/fin_maps.v *)
Lemma map_empty_equiv_eq m : m ≡ ∅ ↔ m = ∅.
Proof.
    split; [intros Hm; apply map_eq; intros i|intros ->].
    - generalize (Hm i). by rewrite lookup_empty, None_equiv_eq.
    - intros ?. rewrite lookup_empty; constructor.
  Qed.
(* stdpp/fin_maps.v *)
Lemma partial_alter_equiv_eq (f : option A → option A) (m1 m2 : M A) i :
    Proper ((≡) ==> (≡)) f →
    (∀ x1 mx2, Some x1 ≡ f mx2 → ∃ mx2', Some x1 = f mx2' ∧ mx2' ≡ mx2) →
    m1 ≡ partial_alter f i m2 ↔ ∃ m2', m1 = partial_alter f i m2' ∧ m2' ≡ m2.
Proof.
    intros ? Hf. split; [|by intros (?&->&<-)]. intros Hm.
    assert (∃ mx2', m1 !! i = f mx2' ∧ mx2' ≡ m2 !! i) as (mx2'&?&?).
    { destruct (m1 !! i) as [x1|] eqn:Hix1.
      - apply (Hf x1 (m2 !! i)). by rewrite <-Hix1, Hm, lookup_partial_alter_eq.
      - exists (m2 !! i). split; [|done]. apply symmetry, None_equiv_eq.
        by rewrite <-Hix1, Hm, lookup_partial_alter_eq. }
    exists (partial_alter (λ _, mx2') i m1). split.
    - apply map_eq; intros j. rewrite !lookup_partial_alter.
      repeat case_decide; naive_solver.
    - intros j. destruct (decide (i = j)) as [->|?].
      + by rewrite lookup_partial_alter_eq.
      + by rewrite Hm, !lookup_partial_alter_ne.
  Qed.
(* stdpp/fin_maps.v *)
Lemma alter_equiv_eq (f : A → A) (m1 m2 : M A) i :
    Proper ((≡) ==> (≡)) f →
    (∀ x1 x2, x1 ≡ f x2 → ∃ x2', x1 = f x2' ∧ x2' ≡ x2) →
    m1 ≡ alter f i m2 ↔ ∃ m2', m1 = alter f i m2' ∧ m2' ≡ m2.
Proof.
    intros ? Hf. apply (partial_alter_equiv_eq _ _ _ _ _). intros mx1 [x2|]; simpl.
    - intros (x2'&->&?)%(inj _)%Hf. exists (Some x2'). by repeat constructor.
    - intros ->%None_equiv_eq. by exists None.
  Qed.
(* stdpp/fin_maps.v *)
Lemma delete_equiv_eq m1 m2 i :
    m1 ≡ delete i m2 ↔ ∃ m2', m1 = delete i m2' ∧ m2' ≡ m2.
Proof. apply (partial_alter_equiv_eq _ _ _ _ _). intros ?? [=]%None_equiv_eq. Qed.
(* stdpp/fin_maps.v *)
Lemma insert_equiv_eq m1 m2 i x :
    m1 ≡ <[i:=x]> m2 ↔ ∃ x' m2', m1 = <[i:=x']> m2' ∧ x' ≡ x ∧ m2' ≡ m2.
Proof.
    split; [|by intros (?&?&->&<-&<-)]. intros Hm.
    assert (is_Some (m1 !! i)) as [x' Hix'].
    { rewrite Hm, lookup_insert_eq. eauto. }
    destruct (m2 !! i) as [y|] eqn:?.
    - exists x', (<[i:=y]> m1). split_and!.
      + by rewrite insert_insert_eq, insert_id by done.
      + apply (inj Some). by rewrite <-Hix', Hm, lookup_insert_eq.
      + by rewrite Hm, insert_insert_eq, insert_id by done.
    - exists x', (delete i m1). split_and!.
      + by rewrite insert_delete_id by done.
      + apply (inj Some). by rewrite <-Hix', Hm, lookup_insert_eq.
      + by rewrite Hm, delete_insert_id by done.
  Qed.
(* stdpp/fin_maps.v *)
Lemma map_singleton_equiv_eq m i x :
    m ≡ {[i:=x]} ↔ ∃ x', m = {[i:=x']} ∧ x' ≡ x.
Proof.
    rewrite <-!insert_empty, insert_equiv_eq.
    setoid_rewrite map_empty_equiv_eq. naive_solver.
  Qed.
(* stdpp/fin_maps.v *)
Lemma map_filter_equiv_eq (P : K * A → Prop) `{!∀ kx, Decision (P kx)} (m1 m2 : M A):
    (∀ k, Proper ((≡) ==> iff) (curry P k)) →
    m1 ≡ filter P m2 ↔ ∃ m2', m1 = filter P m2' ∧ m2' ≡ m2.
Proof.
    intros HP. split; [|by intros (?&->&->)].
    revert m1. induction m2 as [|i x m2 ? IH] using map_ind; intros m1 Hm.
    { rewrite map_filter_empty in Hm. exists ∅.
      by rewrite map_filter_empty, <-map_empty_equiv_eq. }
    rewrite map_filter_insert in Hm. case_decide.
    - apply insert_equiv_eq in Hm as (x'&m2'&->&?&(m2''&->&?)%IH).
      exists (<[i:=x']> m2''). split; [|by f_equiv].
      by rewrite map_filter_insert_True by (by eapply HP).
    - rewrite delete_id in Hm by done.
      apply IH in Hm as (m2'&->&Hm2). exists (<[i:=x]> m2'). split; [|by f_equiv].
      assert (m2' !! i = None).
      { by rewrite <-None_equiv_eq, Hm2, None_equiv_eq. }
      by rewrite map_filter_insert_not' by naive_solver.
  Qed.
(* stdpp/fin_maps.v *)
Lemma map_omap_equiv_eq `{Equiv A, !Equivalence (≡@{A}),
      Equiv B, !Equivalence (≡@{B})}
    (f : A → option B) (m1 : M B) (m2 : M A) :
  Proper ((≡) ==> (≡)) f →
  (∀ y x, Some y ≡ f x → ∃ x', Some y = f x' ∧ x' ≡ x) →
  m1 ≡ omap f m2 ↔ ∃ m2', m1 = omap f m2' ∧ m2' ≡ m2.
Proof.
  intros ? Hf. split; [|by intros (?&->&->)].
  revert m1. induction m2 as [|i x m2 ? IH] using map_ind; intros m1 Hm.
  { rewrite omap_empty, map_empty_equiv_eq in Hm. subst m1.
    exists ∅. by rewrite omap_empty. }
  rewrite omap_insert in Hm. destruct (f x) as [y|] eqn:Hfx.
  - apply insert_equiv_eq in Hm as (y'&m1'&->&Hy&(m2'&->&?)%IH).
    destruct (Hf y' x) as (x'&Hfx'&?).
    { by rewrite Hfx, Hy. }
    exists (<[i:=x']> m2'). split; [|by f_equiv].
    by rewrite omap_insert, <-Hfx'.
  - apply delete_equiv_eq in Hm as (m1'&->&(m2'&->&?)%IH).
    exists (<[i:=x]> m2'). split; [|by f_equiv]. by rewrite omap_insert, Hfx.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_fmap_equiv_eq `{Equiv A, !Equivalence (≡@{A}),
      Equiv B, !Equivalence (≡@{B})} (f : A → B) (m1 : M B) (m2 : M A) :
  Proper ((≡) ==> (≡)) f →
  (∀ y x, y ≡ f x → ∃ x', y = f x' ∧ x' ≡ x) →
  m1 ≡ f <$> m2 ↔ ∃ m2', m1 = f <$> m2' ∧ m2' ≡ m2.
Proof.
  intros ? Hf. rewrite map_fmap_alt; setoid_rewrite map_fmap_alt.
  apply map_omap_equiv_eq; [solve_proper|].
  intros ?? (?&->&?)%(inj _)%Hf; eauto.
Qed.
(* stdpp/fin_maps.v *)
Lemma merge_equiv_eq `{Equiv A, !Equivalence (≡@{A}),
    Equiv B, !Equivalence (≡@{B}), Equiv C, !Equivalence (≡@{C})}
    (f : option A → option B → option C) (m1 : M C) (m2a : M A) (m2b : M B) :
  Proper ((≡) ==> (≡) ==> (≡)) f →
  (∀ y mx1 mx2,
    Some y ≡ f mx1 mx2 →
    ∃ mx1' mx2', Some y = f mx1' mx2' ∧ mx1' ≡ mx1 ∧ mx2' ≡ mx2) →
  m1 ≡ merge f m2a m2b ↔
    ∃ m2a' m2b', m1 = merge f m2a' m2b' ∧ m2a' ≡ m2a ∧ m2b' ≡ m2b.
Proof.
  intros ? Hf. split; [|by intros (?&?&->&->&->)].
  revert m1. induction m2a as [|i x m2a ? IH] using map_ind; intros m1.
  { assert (∀ y x,
      Some y ≡ f None (Some x) → ∃ x', Some y = f None (Some x') ∧ x' ≡ x).
    { intros ?? (?&?&?&->%None_equiv_eq&(?&->&?)%Some_equiv_eq)%Hf; eauto. }
    rewrite merge_empty_l, map_omap_equiv_eq by (done || solve_proper).
    intros (m2'&->&?). exists ∅, m2'. by rewrite merge_empty_l. }
  unfold insert at 1, map_insert at 1.
  rewrite <-(partial_alter_merge_l _ (λ _, f (Some x) (m2b !! i))) by done.
  destruct (f (Some x) (m2b !! i)) as [y|] eqn:Hfi.
  - intros (y'&m'&->&Hy&(m2a'&m2b'&->&Hm2a&Hm2b)%IH)%insert_equiv_eq.
    destruct (Hf y' (Some x) (m2b !! i)) as (mx1&mx2&?&(x'&->&?)%Some_equiv_eq&?).
    { by rewrite Hy, Hfi. }
    exists (<[i:=x']> m2a'), (partial_alter (λ _, mx2) i m2b').
    split_and!; [by apply partial_alter_merge|by f_equiv|].
    intros j. destruct (decide (i = j)) as [->|?].
    + by rewrite lookup_partial_alter_eq.
    + by rewrite Hm2b, lookup_partial_alter_ne.
  - intros (m'&->&(m2a'&m2b'&->&Hm2a&Hm2b)%IH)%delete_equiv_eq.
    exists (<[i:=x]> m2a'), m2b'. split_and!; [|by f_equiv|done].
    apply partial_alter_merge_l, symmetry, None_equiv_eq; simpl.
    by rewrite Hm2b, Hfi.
Qed.