phanerozoic/Coq-Stdpp huggingface dataset:
(* stdpp/fin_maps.v *)
Lemma map_Forall2_impl (R' : K → A → B → Prop) (m1 : M A) (m2 : M B) :
    map_Forall2 R m1 m2 →
    (∀ i x1 x2, R i x1 x2 → R' i x1 x2) →
    map_Forall2 R' m1 m2.
Proof. intros Hm ? i. destruct (Hm i); constructor; eauto. Qed.
(* stdpp/fin_maps.v *)
Lemma map_Forall2_empty : map_Forall2 R (∅ : M A) ∅.
Proof. intros i. rewrite !lookup_empty. constructor. Qed.
(* stdpp/fin_maps.v *)
Lemma map_Forall2_empty_inv_l (m2 : M B) : map_Forall2 R ∅ m2 → m2 = ∅.
Proof.
    intros Hm. apply map_eq; intros i. rewrite lookup_empty, eq_None_not_Some.
    intros [x Hi]. specialize (Hm i). rewrite lookup_empty, Hi in Hm. inv Hm.
  Qed.
(* stdpp/fin_maps.v *)
Lemma map_Forall2_empty_inv_r (m1 : M A) : map_Forall2 R m1 ∅ → m1 = ∅.
Proof.
    intros Hm. apply map_eq; intros i. rewrite lookup_empty, eq_None_not_Some.
    intros [x Hi]. specialize (Hm i). rewrite lookup_empty, Hi in Hm. inv Hm.
  Qed.
(* stdpp/fin_maps.v *)
Lemma map_Forall2_delete (m1 : M A) (m2 : M B) i :
    map_Forall2 R m1 m2 → map_Forall2 R (delete i m1) (delete i m2).
Proof.
    intros Hm j. rewrite !lookup_delete.
    destruct (decide (i = j)) as [->|]; [|done]. constructor.
  Qed.
(* stdpp/fin_maps.v *)
Lemma map_Forall2_insert_2 (m1 : M A) (m2 : M B) i x1 x2 :
    R i x1 x2 → map_Forall2 R m1 m2 → map_Forall2 R (<[i:=x1]> m1) (<[i:=x2]> m2).
Proof.
    intros Hx Hm j. rewrite !lookup_insert.
    destruct (decide (i = j)) as [->|]; [|done]. by constructor.
  Qed.
(* stdpp/fin_maps.v *)
Lemma map_Forall2_insert (m1 : M A) (m2 : M B) i x1 x2 :
    m1 !! i = None → m2 !! i = None →
    map_Forall2 R (<[i:=x1]> m1) (<[i:=x2]> m2) ↔ R i x1 x2 ∧ map_Forall2 R m1 m2.
Proof.
    intros Hi1 Hi2. split; [|naive_solver eauto using map_Forall2_insert_2].
    intros Hm. split.
    - specialize (Hm i). rewrite !lookup_insert_eq in Hm. by inv Hm.
    - intros j. destruct (decide (i = j)) as [->|].
      + rewrite Hi1, Hi2. constructor.
      + specialize (Hm j). by rewrite !lookup_insert_ne in Hm by done.
  Qed.
(* stdpp/fin_maps.v *)
Lemma map_Forall2_insert_inv_l (m1 : M A) (m2 : M B) i x1 :
    m1 !! i = None →
    map_Forall2 R (<[i:=x1]> m1) m2 →
    ∃ x2 m2', m2 = <[i:=x2]> m2' ∧ m2' !! i = None ∧ R i x1 x2 ∧ map_Forall2 R m1 m2'.
Proof.
    intros ? Hm. pose proof (Hm i) as Hi. rewrite lookup_insert_eq in Hi.
    destruct (m2 !! i) as [x2|] eqn:?; inv Hi.
    exists x2, (delete i m2). split; [by rewrite insert_delete_id|].
    split; [by rewrite lookup_delete_eq|]. split; [done|].
    rewrite <-(delete_insert_id m1 i x1) by done. by apply map_Forall2_delete.
  Qed.
(* stdpp/fin_maps.v *)
Lemma map_Forall2_insert_inv_r (m1 : M A) (m2 : M B) i x2 :
    m2 !! i = None →
    map_Forall2 R m1 (<[i:=x2]> m2) →
    ∃ x1 m1', m1 = <[i:=x1]> m1' ∧ m1' !! i = None ∧ R i x1 x2 ∧ map_Forall2 R m1' m2.
Proof.
    intros ? Hm. pose proof (Hm i) as Hi. rewrite lookup_insert_eq in Hi.
    destruct (m1 !! i) as [x1|] eqn:?; inv Hi.
    exists x1, (delete i m1). split; [by rewrite insert_delete_id|].
    split; [by rewrite lookup_delete_eq|]. split; [done|].
    rewrite <-(delete_insert_id m2 i x2) by done. by apply map_Forall2_delete.
  Qed.
(* stdpp/fin_maps.v *)
Lemma map_Forall2_singleton i x1 x2 :
    map_Forall2 R ({[i:=x1]} : M A) {[i:=x2]} ↔ R i x1 x2.
Proof.
    rewrite <-!insert_empty, map_Forall2_insert by (by rewrite lookup_empty).
    naive_solver eauto using map_Forall2_empty.
  Qed.
(* stdpp/fin_maps.v *)
Lemma map_Forall2_flip {A B} (R : K → A → B → Prop) (m1 : M A) m2 :
  map_Forall2 (flip ∘ R) m2 m1 ↔ map_Forall2 R m1 m2.
Proof. apply forall_proper=> k. apply option_Forall2_flip. Qed.
(* stdpp/fin_maps.v *)
(* ** Properties of the [map_agree] relation *)
Lemma map_agree_spec {A} (m1 m2 : M A) :
  map_agree m1 m2 ↔ ∀ i x y, m1 !! i = Some x → m2 !! i = Some y → x = y.
Proof.
  apply forall_proper; intros i; destruct (m1 !! i), (m2 !! i); naive_solver.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_agree_alt {A} (m1 m2 : M A) :
  map_agree m1 m2 ↔ ∀ i, m1 !! i = None ∨ m2 !! i = None ∨ m1 !! i = m2 !! i.
Proof.
  apply forall_proper; intros i; destruct (m1 !! i), (m2 !! i); naive_solver.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_not_agree {A} (m1 m2 : M A) `{!EqDecision A}:
  ¬map_agree m1 m2 ↔ ∃ i x1 x2, m1 !! i = Some x1 ∧ m2 !! i = Some x2 ∧ x1 ≠ x2.
Proof.
  unfold map_agree. rewrite map_not_relation by solve_decision. naive_solver.
Qed.
(* stdpp/fin_maps.v *)
Instance map_agree_refl {A} : Reflexive (map_agree : relation (M A)).
Proof. intros ?. rewrite !map_agree_spec. naive_solver. Qed.
(* stdpp/fin_maps.v *)
Instance map_agree_sym {A} : Symmetric (map_agree : relation (M A)).
Proof.
  intros m1 m2. rewrite !map_agree_spec.
  intros Hm i x y Hm1 Hm2. symmetry. naive_solver.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_agree_empty_l {A} (m : M A) : map_agree ∅ m.
Proof. rewrite !map_agree_spec. intros i x y. by rewrite lookup_empty. Qed.
(* stdpp/fin_maps.v *)
Lemma map_agree_empty_r {A} (m : M A) : map_agree m ∅.
Proof. rewrite !map_agree_spec. intros i x y. by rewrite lookup_empty. Qed.
(* stdpp/fin_maps.v *)
Lemma map_agree_weaken {A} (m1 m1' m2 m2' : M A) :
  map_agree m1' m2' → m1 ⊆ m1' → m2 ⊆ m2' → map_agree m1 m2.
Proof. rewrite !map_subseteq_spec, !map_agree_spec. eauto. Qed.
(* stdpp/fin_maps.v *)
Lemma map_agree_weaken_l {A} (m1 m1' m2  : M A) :
  map_agree m1' m2 → m1 ⊆ m1' → map_agree m1 m2.
Proof. eauto using map_agree_weaken. Qed.
(* stdpp/fin_maps.v *)
Lemma map_agree_weaken_r {A} (m1 m2 m2' : M A) :
  map_agree m1 m2' → m2 ⊆ m2' → map_agree m1 m2.
Proof. eauto using map_agree_weaken. Qed.
(* stdpp/fin_maps.v *)
Lemma map_agree_Some_l {A} (m1 m2 : M A) i x:
  map_agree m1 m2 → m1 !! i = Some x → m2 !! i = Some x ∨ m2 !! i = None.
Proof. rewrite map_agree_spec. destruct (m2 !! i) eqn: ?; naive_solver. Qed.
(* stdpp/fin_maps.v *)
Lemma map_agree_Some_r {A} (m1 m2 : M A) i x:
  map_agree m1 m2 → m2 !! i = Some x → m1 !! i = Some x ∨ m1 !! i = None.
Proof. rewrite (symmetry_iff map_agree). apply map_agree_Some_l. Qed.
(* stdpp/fin_maps.v *)
Lemma map_agree_singleton_l {A} (m: M A) i x :
  map_agree {[i:=x]} m ↔ m !! i = Some x ∨ m !! i = None.
Proof.
  rewrite map_agree_spec. setoid_rewrite lookup_singleton_Some.
  destruct (m !! i) eqn:?; naive_solver.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_agree_singleton_r {A} (m : M A) i x :
  map_agree m {[i:=x]} ↔ m !! i = Some x ∨ m !! i = None.
Proof. by rewrite (symmetry_iff map_agree), map_agree_singleton_l. Qed.
(* stdpp/fin_maps.v *)
Lemma map_agree_delete_l {A} (m1 m2 : M A) i :
  map_agree m1 m2 → map_agree (delete i m1) m2.
Proof.
  rewrite !map_agree_alt. intros Hagree j. rewrite lookup_delete_None.
  destruct (Hagree j) as [|[|<-]]; auto.
  destruct (decide (i = j)); [naive_solver|].
  rewrite lookup_delete_ne; naive_solver.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_agree_delete_r {A} (m1 m2 : M A) i :
  map_agree m1 m2 → map_agree m1 (delete i m2).
Proof. symmetry. by apply map_agree_delete_l. Qed.
(* stdpp/fin_maps.v *)
Lemma map_agree_filter {A} (P : K * A → Prop)
    `{!∀ x, Decision (P x)} (m1 m2 : M A) :
  map_agree m1 m2 → map_agree (filter P m1) (filter P m2).
Proof.
  rewrite !map_agree_spec. intros ? i x y.
  rewrite !map_lookup_filter_Some. naive_solver.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_agree_fmap_1 {A B} (f : A → B) (m1 m2 : M A) `{!Inj (=) (=) f}:
  map_agree (f <$> m1) (f <$> m2) → map_agree m1 m2.
Proof.
  rewrite !map_agree_spec. setoid_rewrite lookup_fmap_Some. naive_solver.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_agree_fmap_2 {A B} (f : A → B) (m1 m2 : M A):
  map_agree m1 m2 → map_agree (f <$> m1) (f <$> m2).
Proof.
  rewrite !map_agree_spec. setoid_rewrite lookup_fmap_Some. naive_solver.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_agree_fmap {A B} (f : A → B) (m1 m2 : M A) `{!Inj (=) (=) f}:
  map_agree (f <$> m1) (f <$> m2) ↔ map_agree m1 m2.
Proof. naive_solver eauto using map_agree_fmap_1, map_agree_fmap_2. Qed.
(* stdpp/fin_maps.v *)
Lemma map_agree_omap {A B} (f : A → option B) (m1 m2 : M A) :
  map_agree m1 m2 → map_agree (omap f m1) (omap f m2).
Proof. rewrite !map_agree_spec. setoid_rewrite lookup_omap_Some. naive_solver. Qed.
(* stdpp/fin_maps.v *)
(* ** Properties on the disjoint maps *)
Lemma map_disjoint_spec {A} (m1 m2 : M A) :
  m1 ##ₘ m2 ↔ ∀ i x y, m1 !! i = Some x → m2 !! i = Some y → False.
Proof.
  apply forall_proper; intros i; destruct (m1 !! i), (m2 !! i); naive_solver.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_disjoint_alt {A} (m1 m2 : M A) :
  m1 ##ₘ m2 ↔ ∀ i, m1 !! i = None ∨ m2 !! i = None.
Proof.
  apply forall_proper; intros i; destruct (m1 !! i), (m2 !! i); naive_solver.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_not_disjoint {A} (m1 m2 : M A) :
  ¬m1 ##ₘ m2 ↔ ∃ i x1 x2, m1 !! i = Some x1 ∧ m2 !! i = Some x2.
Proof.
  unfold disjoint, map_disjoint. rewrite map_not_relation by solve_decision.
  naive_solver.
Qed.
(* stdpp/fin_maps.v *)
Instance map_disjoint_sym {A} : Symmetric (map_disjoint : relation (M A)).
Proof. intros m1 m2. rewrite !map_disjoint_spec. naive_solver. Qed.
(* stdpp/fin_maps.v *)
Lemma map_disjoint_empty_l {A} (m : M A) : ∅ ##ₘ m.
Proof. rewrite !map_disjoint_spec. intros i x y. by rewrite lookup_empty. Qed.
(* stdpp/fin_maps.v *)
Lemma map_disjoint_empty_r {A} (m : M A) : m ##ₘ ∅.
Proof. rewrite !map_disjoint_spec. intros i x y. by rewrite lookup_empty. Qed.
(* stdpp/fin_maps.v *)
Lemma map_disjoint_weaken {A} (m1 m1' m2 m2' : M A) :
  m1' ##ₘ m2' → m1 ⊆ m1' → m2 ⊆ m2' → m1 ##ₘ m2.
Proof. rewrite !map_subseteq_spec, !map_disjoint_spec. eauto. Qed.
(* stdpp/fin_maps.v *)
Lemma map_disjoint_weaken_l {A} (m1 m1' m2  : M A) :
  m1' ##ₘ m2 → m1 ⊆ m1' → m1 ##ₘ m2.
Proof. eauto using map_disjoint_weaken. Qed.
(* stdpp/fin_maps.v *)
Lemma map_disjoint_weaken_r {A} (m1 m2 m2' : M A) :
  m1 ##ₘ m2' → m2 ⊆ m2' → m1 ##ₘ m2.
Proof. eauto using map_disjoint_weaken. Qed.
(* stdpp/fin_maps.v *)
Lemma map_disjoint_Some_l {A} (m1 m2 : M A) i x:
  m1 ##ₘ m2 → m1 !! i = Some x → m2 !! i = None.
Proof. rewrite map_disjoint_spec, eq_None_not_Some. intros ?? [??]; eauto. Qed.
(* stdpp/fin_maps.v *)
Lemma map_disjoint_Some_r {A} (m1 m2 : M A) i x:
  m1 ##ₘ m2 → m2 !! i = Some x → m1 !! i = None.
Proof. rewrite (symmetry_iff map_disjoint). apply map_disjoint_Some_l. Qed.
(* stdpp/fin_maps.v *)
Lemma map_disjoint_singleton_l {A} (m: M A) i x : {[i:=x]} ##ₘ m ↔ m !! i = None.
Proof.
  rewrite !map_disjoint_spec. setoid_rewrite lookup_singleton_Some.
  destruct (m !! i) eqn:?; naive_solver.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_disjoint_singleton_r {A} (m : M A) i x :
  m ##ₘ {[i:=x]} ↔ m !! i = None.
Proof. by rewrite (symmetry_iff map_disjoint), map_disjoint_singleton_l. Qed.
(* stdpp/fin_maps.v *)
Lemma map_disjoint_singleton_l_2 {A} (m : M A) i x :
  m !! i = None → {[i:=x]} ##ₘ m.
Proof. by rewrite map_disjoint_singleton_l. Qed.
(* stdpp/fin_maps.v *)
Lemma map_disjoint_singleton_r_2 {A} (m : M A) i x :
  m !! i = None → m ##ₘ {[i:=x]}.
Proof. by rewrite map_disjoint_singleton_r. Qed.
(* stdpp/fin_maps.v *)
Lemma map_disjoint_delete_l {A} (m1 m2 : M A) i : m1 ##ₘ m2 → delete i m1 ##ₘ m2.
Proof.
  rewrite !map_disjoint_alt. intros Hdisjoint j. destruct (Hdisjoint j); auto.
  rewrite lookup_delete_None. tauto.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_disjoint_delete_r {A} (m1 m2 : M A) i : m1 ##ₘ m2 → m1 ##ₘ delete i m2.
Proof. symmetry. by apply map_disjoint_delete_l. Qed.
(* stdpp/fin_maps.v *)
Lemma map_disjoint_filter {A} (P : K * A → Prop)
    `{!∀ x, Decision (P x)} (m1 m2 : M A) :
  m1 ##ₘ m2 → filter P m1 ##ₘ filter P m2.
Proof.
  rewrite !map_disjoint_spec. intros ? i x y.
  rewrite !map_lookup_filter_Some. naive_solver.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_disjoint_filter_complement {A} (P : K * A → Prop)
    `{!∀ x, Decision (P x)} (m : M A) :
  filter P m ##ₘ filter (λ v, ¬ P v) m.
Proof.
  apply map_disjoint_spec. intros i x y.
  rewrite !map_lookup_filter_Some. naive_solver.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_disjoint_fmap {A B} (f1 f2 : A → B) (m1 m2 : M A) :
  f1 <$> m1 ##ₘ f2 <$> m2 ↔ m1 ##ₘ m2.
Proof.
  rewrite !map_disjoint_spec. setoid_rewrite lookup_fmap_Some. naive_solver.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_disjoint_omap {A B} (f1 f2 : A → option B) (m1 m2 : M A) :
  m1 ##ₘ m2 → omap f1 m1 ##ₘ omap f2 m2.
Proof.
  rewrite !map_disjoint_spec. setoid_rewrite lookup_omap_Some. naive_solver.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_disjoint_agree {A} (m1 m2 : M A) :
  m1 ##ₘ m2 → map_agree m1 m2.
Proof. rewrite !map_disjoint_spec, !map_agree_spec. naive_solver. Qed.
(* stdpp/fin_maps.v *)
Lemma map_disjoint_set_to_map {A} `{FinSet K C} (f : K → A) (X Y : C) :
  set_to_map (M:=M A) f X ##ₘ set_to_map f Y ↔ X ## Y.
Proof.
  rewrite map_disjoint_spec. setoid_rewrite lookup_set_to_map_Some. set_solver.
Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_union_with m1 m2 i :
    union_with f m1 m2 !! i = union_with f (m1 !! i) (m2 !! i).
Proof.
    unfold union_with, map_union_with. rewrite lookup_merge.
    by destruct (m1 !! i), (m2 !! i).
  Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_union_with_Some m1 m2 i z :
    union_with f m1 m2 !! i = Some z ↔
      (m1 !! i = Some z ∧ m2 !! i = None) ∨
      (m1 !! i = None ∧ m2 !! i = Some z) ∨
      (∃ x y, m1 !! i = Some x ∧ m2 !! i = Some y ∧ f x y = Some z).
Proof.
    rewrite lookup_union_with.
    destruct (m1 !! i), (m2 !! i); compute; naive_solver.
  Qed.
(* stdpp/fin_maps.v *)
Instance : LeftId (=@{M A}) ∅ (union_with f).
Proof. unfold union_with, map_union_with. apply _. Qed.
(* stdpp/fin_maps.v *)
Instance : RightId (=@{M A}) ∅ (union_with f).
Proof. unfold union_with, map_union_with. apply _. Qed.
(* stdpp/fin_maps.v *)
Lemma union_with_comm m1 m2 :
    (∀ i x y, m1 !! i = Some x → m2 !! i = Some y → f x y = f y x) →
    union_with f m1 m2 = union_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}) (union_with f).
Proof. intros ???. apply union_with_comm. eauto. Qed.
(* stdpp/fin_maps.v *)
Lemma union_with_idemp m :
    (∀ i x, m !! i = Some x → f x x = Some x) → union_with f m m = m.
Proof.
    intros. apply merge_idemp. intros i.
    destruct (m !! i) eqn:?; simpl; eauto.
  Qed.
(* stdpp/fin_maps.v *)
Lemma alter_union_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 (union_with f m1 m2) =
      union_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 alter_union_with_l (g : A → A) m1 m2 i :
    (∀ x y, m1 !! i = Some x → m2 !! i = Some y → g <$> f x y = f (g x) y) →
    (∀ y, m1 !! i = None → m2 !! i = Some y → g y = y) →
    alter g i (union_with f m1 m2) = union_with f (alter g i m1) m2.
Proof.
    intros. apply partial_alter_merge_l.
    destruct (m1 !! i) eqn:?, (m2 !! i) eqn:?; f_equal/=; auto.
  Qed.
(* stdpp/fin_maps.v *)
Lemma alter_union_with_r (g : A → A) m1 m2 i :
    (∀ x y, m1 !! i = Some x → m2 !! i = Some y → g <$> f x y = f x (g y)) →
    (∀ x, m1 !! i = Some x → m2 !! i = None → g x = x) →
    alter g i (union_with f m1 m2) = union_with f m1 (alter g i m2).
Proof.
    intros. apply partial_alter_merge_r.
    destruct (m1 !! i) eqn:?, (m2 !! i) eqn:?; f_equal/=; auto.
  Qed.
(* stdpp/fin_maps.v *)
Lemma delete_union_with m1 m2 i :
    delete i (union_with f m1 m2) = union_with f (delete i m1) (delete i m2).
Proof. by apply partial_alter_merge. Qed.
(* stdpp/fin_maps.v *)
Lemma foldr_delete_union_with (m1 m2 : M A) js :
    foldr delete (union_with f m1 m2) js =
      union_with f (foldr delete m1 js) (foldr delete m2 js).
Proof.
    induction js as [|?? IHjs]; simpl; [done|].
    by rewrite IHjs, delete_union_with.
  Qed.
(* stdpp/fin_maps.v *)
Lemma insert_union_with m1 m2 i x y z :
    f x y = Some z →
    <[i:=z]>(union_with f m1 m2) = union_with f (<[i:=x]> m1) (<[i:=y]> m2).
Proof. by intros; apply (partial_alter_merge _). Qed.
(* stdpp/fin_maps.v *)
Lemma insert_union_with_l m1 m2 i x :
    m2 !! i = None → <[i:=x]>(union_with f m1 m2) = union_with f (<[i:=x]> m1) m2.
Proof.
    intros Hm2. unfold union_with, map_union_with.
    by erewrite insert_merge_l by (by rewrite Hm2).
  Qed.
(* stdpp/fin_maps.v *)
Lemma insert_union_with_r m1 m2 i x :
    m1 !! i = None → <[i:=x]>(union_with f m1 m2) = union_with f m1 (<[i:=x]> m2).
Proof.
    intros Hm1. unfold union_with, map_union_with.
    by erewrite insert_merge_r by (by rewrite Hm1).
  Qed.
(* stdpp/fin_maps.v *)
(* ** Properties of the [union] operation *)
Instance map_empty_union {A} : LeftId (=@{M A}) ∅ (∪)
:= _.
(* stdpp/fin_maps.v *)
Instance map_union_empty {A} : RightId (=@{M A}) ∅ (∪)
:= _.
(* stdpp/fin_maps.v *)
Instance map_union_assoc {A} : Assoc (=@{M A}) (∪).
Proof.
  intros m1 m2 m3. unfold union, map_union, union_with, map_union_with.
  apply merge_assoc. intros i.
  by destruct (m1 !! i), (m2 !! i), (m3 !! i).
Qed.
(* stdpp/fin_maps.v *)
Instance map_union_idemp {A} : IdemP (=@{M A}) (∪).
Proof. intros ?. by apply union_with_idemp. Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_union {A} (m1 m2 : M A) i :
  (m1 ∪ m2) !! i = (m1 !! i) ∪ (m2 !! i).
Proof. apply lookup_union_with. Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_union_r {A} (m1 m2 : M A) i :
  m1 !! i = None → (m1 ∪ m2) !! i = m2 !! i.
Proof. intros Hi. by rewrite lookup_union, Hi, (left_id_L _ _).  Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_union_l {A} (m1 m2 : M A) i :
  m2 !! i = None → (m1 ∪ m2) !! i = m1 !! i.
Proof. intros Hi. rewrite lookup_union, Hi. by destruct (m1 !! i). Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_union_l' {A} (m1 m2 : M A) i :
  is_Some (m1 !! i) → (m1 ∪ m2) !! i = m1 !! i.
Proof. intros [x Hi]. rewrite lookup_union, Hi. by destruct (m2 !! i). Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_union_Some_raw {A} (m1 m2 : M A) i x :
  (m1 ∪ m2) !! i = Some x ↔
    m1 !! i = Some x ∨ (m1 !! i = None ∧ m2 !! i = Some x).
Proof. rewrite lookup_union. destruct (m1 !! i), (m2 !! i); naive_solver. Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_union_None {A} (m1 m2 : M A) i :
  (m1 ∪ m2) !! i = None ↔ m1 !! i = None ∧ m2 !! i = None.
Proof. rewrite lookup_union.  destruct (m1 !! i), (m2 !! i); naive_solver. Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_union_None_1 {A} (m1 m2 : M A) i :
  (m1 ∪ m2) !! i = None → m1 !! i = None ∧ m2 !! i = None.
Proof. apply lookup_union_None. Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_union_None_2 {A} (m1 m2 : M A) i :
  m1 !! i = None → m2 !! i = None → (m1 ∪ m2) !! i = None.
Proof. intros. by apply lookup_union_None. Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_union_Some {A} (m1 m2 : M A) i x :
  m1 ##ₘ m2 → (m1 ∪ m2) !! i = Some x ↔ m1 !! i = Some x ∨ m2 !! i = Some x.
Proof.
  intros Hdisjoint. rewrite lookup_union_Some_raw.
  intuition eauto using map_disjoint_Some_r.
Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_union_Some_l {A} (m1 m2 : M A) i x :
  m1 !! i = Some x → (m1 ∪ m2) !! i = Some x.
Proof. intro. rewrite lookup_union_Some_raw; intuition. Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_union_Some_r {A} (m1 m2 : M A) i x :
  m1 ##ₘ m2 → m2 !! i = Some x → (m1 ∪ m2) !! i = Some x.
Proof. intro. rewrite lookup_union_Some; intuition. Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_union_Some_inv_l {A} (m1 m2 : M A) i x :
  (m1 ∪ m2) !! i = Some x → m2 !! i = None → m1 !! i = Some x.
Proof. rewrite lookup_union_Some_raw. naive_solver. Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_union_Some_inv_r {A} (m1 m2 : M A) i x :
  (m1 ∪ m2) !! i = Some x → m1 !! i = None → m2 !! i = Some x.
Proof. rewrite lookup_union_Some_raw. naive_solver. Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_union_is_Some {A} (m1 m2 : M A) i :
  is_Some ((m1 ∪ m2) !! i) ↔ is_Some (m1 !! i) ∨ is_Some (m2 !! i).
Proof.
  rewrite <-!not_eq_None_Some, !lookup_union_None.
  destruct (m1 !! i); naive_solver.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_union_comm {A} (m1 m2 : M A) : m1 ##ₘ m2 → m1 ∪ m2 = m2 ∪ m1.
Proof.
  intros Hdisjoint. apply (merge_comm (union_with (λ x _, Some x))).
  intros i. specialize (Hdisjoint i).
  destruct (m1 !! i), (m2 !! i); compute; naive_solver.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_positive_l {A} (m1 m2 : M A) : m1 ∪ m2 = ∅ → m1 = ∅.
Proof.
  intros Hm. apply map_empty. intros i. apply (f_equal (.!! i)) in Hm.
  rewrite lookup_empty, lookup_union_None in Hm; tauto.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_positive_l_alt {A} (m1 m2 : M A) : m1 ≠ ∅ → m1 ∪ m2 ≠ ∅.
Proof. eauto using map_positive_l. Qed.
(* stdpp/fin_maps.v *)
Lemma map_subseteq_union {A} (m1 m2 : M A) : m1 ⊆ m2 → m1 ∪ m2 = m2.
Proof.
  rewrite map_subseteq_spec.
  intros Hm1m2. apply map_eq. intros i. apply option_eq. intros x.
  rewrite lookup_union_Some_raw. split; [by intuition |].
  intros Hm2. specialize (Hm1m2 i). destruct (m1 !! i) as [y|]; [| by auto].
  rewrite (Hm1m2 y eq_refl) in Hm2. intuition congruence.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_union_subseteq_l {A} (m1 m2 : M A) : m1 ⊆ m1 ∪ m2.
Proof.
  rewrite map_subseteq_spec. intros ? i x. rewrite lookup_union_Some_raw. tauto.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_union_subseteq_r {A} (m1 m2 : M A) : m1 ##ₘ m2 → m2 ⊆ m1 ∪ m2.
Proof.
  intros. rewrite map_union_comm by done. by apply map_union_subseteq_l.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_union_subseteq_l' {A} (m1 m2 m3 : M A) : m1 ⊆ m2 → m1 ⊆ m2 ∪ m3.
Proof. intros. trans m2; auto using map_union_subseteq_l. Qed.
(* stdpp/fin_maps.v *)
Lemma map_union_subseteq_r' {A} (m1 m2 m3 : M A) :
  m2 ##ₘ m3 → m1 ⊆ m3 → m1 ⊆ m2 ∪ m3.
Proof. intros. trans m3; auto using map_union_subseteq_r. Qed.
(* stdpp/fin_maps.v *)
Lemma map_union_least {A} (m1 m2 m3 : M A) :
  m1 ⊆ m3 → m2 ⊆ m3 → m1 ∪ m2 ⊆ m3.
Proof.
  intros ??. apply map_subseteq_spec.
  intros ?? [?|[_ ?]]%lookup_union_Some_raw; by eapply lookup_weaken.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_union_mono_l {A} (m1 m2 m3 : M A) : m1 ⊆ m2 → m3 ∪ m1 ⊆ m3 ∪ m2.
Proof.
  rewrite !map_subseteq_spec. intros ???.
  rewrite !lookup_union_Some_raw. naive_solver.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_union_mono_r {A} (m1 m2 m3 : M A) :
  m2 ##ₘ m3 → m1 ⊆ m2 → m1 ∪ m3 ⊆ m2 ∪ m3.
Proof.
  intros. rewrite !(map_union_comm _ m3)
    by eauto using map_disjoint_weaken_l.
  by apply map_union_mono_l.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_union_reflecting_l {A} (m1 m2 m3 : M A) :
  m3 ##ₘ m1 → m3 ##ₘ m2 → m3 ∪ m1 ⊆ m3 ∪ m2 → m1 ⊆ m2.
Proof.
  rewrite !map_subseteq_spec. intros Hm31 Hm32 Hm i x ?. specialize (Hm i x).
  rewrite !lookup_union_Some in Hm by done. destruct Hm; auto.
  by rewrite map_disjoint_spec in Hm31; destruct (Hm31 i x x).
Qed.
(* stdpp/fin_maps.v *)
Lemma map_union_reflecting_r {A} (m1 m2 m3 : M A) :
  m1 ##ₘ m3 → m2 ##ₘ m3 → m1 ∪ m3 ⊆ m2 ∪ m3 → m1 ⊆ m2.
Proof.
  intros ??. rewrite !(map_union_comm _ m3) by done.
  by apply map_union_reflecting_l.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_union_cancel_l {A} (m1 m2 m3 : M A) :
  m1 ##ₘ m3 → m2 ##ₘ m3 → m3 ∪ m1 = m3 ∪ m2 → m1 = m2.
Proof.
  intros. apply (anti_symm (⊆)); apply map_union_reflecting_l with m3;
    by try apply reflexive_eq.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_union_cancel_r {A} (m1 m2 m3 : M A) :
  m1 ##ₘ m3 → m2 ##ₘ m3 → m1 ∪ m3 = m2 ∪ m3 → m1 = m2.
Proof.
  intros. apply (anti_symm (⊆)); apply map_union_reflecting_r with m3;
    by try apply reflexive_eq.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_disjoint_union_l {A} (m1 m2 m3 : M A) :
  m1 ∪ m2 ##ₘ m3 ↔ m1 ##ₘ m3 ∧ m2 ##ₘ m3.
Proof.
  rewrite !map_disjoint_alt. setoid_rewrite lookup_union_None. naive_solver.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_disjoint_union_r {A} (m1 m2 m3 : M A) :
  m1 ##ₘ m2 ∪ m3 ↔ m1 ##ₘ m2 ∧ m1 ##ₘ m3.
Proof.
  rewrite !map_disjoint_alt. setoid_rewrite lookup_union_None. naive_solver.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_disjoint_union_l_2 {A} (m1 m2 m3 : M A) :
  m1 ##ₘ m3 → m2 ##ₘ m3 → m1 ∪ m2 ##ₘ m3.
Proof. by rewrite map_disjoint_union_l. Qed.
(* stdpp/fin_maps.v *)
Lemma map_disjoint_union_r_2 {A} (m1 m2 m3 : M A) :
  m1 ##ₘ m2 → m1 ##ₘ m3 → m1 ##ₘ m2 ∪ m3.
Proof. by rewrite map_disjoint_union_r. Qed.
(* stdpp/fin_maps.v *)
Lemma insert_union_singleton_l {A} (m : M A) i x : <[i:=x]> m = {[i:=x]} ∪ m.
Proof.
  apply map_eq. intros j. apply option_eq. intros y.
  rewrite lookup_union_Some_raw, lookup_singleton, lookup_insert.
  case_decide; naive_solver.
Qed.