phanerozoic/Coq-Stdpp huggingface dataset:
(* stdpp/fin_maps.v *)
Lemma map_lookup_filter m i :
    filter P m !! i = x ← m !! i; guard (P (i,x));; Some x.
Proof.
    revert m i. apply (map_fold_weak_ind (λ m1 m2,
      ∀ i, m1 !! i = x ← m2 !! i; guard (P (i,x));; Some x)); intros i.
    { by rewrite lookup_empty. }
    intros y m m' Hm IH j. case (decide (j = i))as [->|?].
    - case_decide.
      + rewrite !lookup_insert_eq. simpl. by rewrite option_guard_True.
      + rewrite lookup_insert_eq. simpl. by rewrite option_guard_False, IH, Hm.
    - case_decide.
      + by rewrite !lookup_insert_ne by done.
      + by rewrite !lookup_insert_ne.
  Qed.
(* stdpp/fin_maps.v *)
Lemma map_lookup_filter_Some m i x :
    filter P m !! i = Some x ↔ m !! i = Some x ∧ P (i, x).
Proof.
    rewrite map_lookup_filter.
    destruct (m !! i); simpl; repeat case_guard; naive_solver.
  Qed.
(* stdpp/fin_maps.v *)
Lemma map_lookup_filter_Some_1_1 m i x :
    filter P m !! i = Some x → m !! i = Some x.
Proof. apply map_lookup_filter_Some. Qed.
(* stdpp/fin_maps.v *)
Lemma map_lookup_filter_Some_1_2 m i x :
    filter P m !! i = Some x → P (i, x).
Proof. apply map_lookup_filter_Some. Qed.
(* stdpp/fin_maps.v *)
Lemma map_lookup_filter_Some_2 m i x :
    m !! i = Some x →
    P (i, x) →
    filter P m !! i = Some x.
Proof. intros. by apply map_lookup_filter_Some. Qed.
(* stdpp/fin_maps.v *)
Lemma map_lookup_filter_None m i :
    filter P m !! i = None ↔ m !! i = None ∨ ∀ x, m !! i = Some x → ¬ P (i, x).
Proof.
    rewrite eq_None_not_Some. unfold is_Some.
    setoid_rewrite map_lookup_filter_Some. naive_solver.
  Qed.
(* stdpp/fin_maps.v *)
Lemma map_lookup_filter_None_1 m i :
    filter P m !! i = None →
    m !! i = None ∨ ∀ x, m !! i = Some x → ¬ P (i, x).
Proof. apply map_lookup_filter_None. Qed.
(* stdpp/fin_maps.v *)
Lemma map_lookup_filter_None_2 m i :
    m !! i = None ∨ (∀ x : A, m !! i = Some x → ¬ P (i, x)) →
    filter P m !! i = None.
Proof. apply map_lookup_filter_None. Qed.
(* stdpp/fin_maps.v *)
Lemma map_filter_empty_not_lookup m i x :
    filter P m = ∅ → P (i,x) → m !! i ≠ Some x.
Proof.
    rewrite map_empty. setoid_rewrite map_lookup_filter_None. intros Hm ?.
    destruct (Hm i); naive_solver.
  Qed.
(* stdpp/fin_maps.v *)
Lemma map_filter_strong_ext (m1 m2 : M A) :
    filter P m1 = filter Q m2 ↔
    (∀ i x, (P (i, x) ∧ m1 !! i = Some x) ↔ (Q (i, x) ∧ m2 !! i = Some x)).
Proof.
    intros. rewrite map_eq_iff. setoid_rewrite option_eq.
    setoid_rewrite map_lookup_filter_Some. naive_solver.
  Qed.
(* stdpp/fin_maps.v *)
Lemma map_filter_strong_ext_1 (m1 m2 : M A) :
    (∀ i x, (P (i, x) ∧ m1 !! i = Some x) ↔ (Q (i, x) ∧ m2 !! i = Some x)) →
    filter P m1 = filter Q m2.
Proof. by rewrite map_filter_strong_ext. Qed.
(* stdpp/fin_maps.v *)
Lemma map_filter_strong_ext_2 (m1 m2 : M A) i x :
    filter P m1 = filter Q m2 →
    (P (i, x) ∧ m1 !! i = Some x) ↔ (Q (i, x) ∧ m2 !! i = Some x).
Proof. by rewrite map_filter_strong_ext. Qed.
(* stdpp/fin_maps.v *)
Lemma map_filter_ext (m : M A) :
    (∀ i x, m !! i = Some x → P (i, x) ↔ Q (i, x)) ↔
    filter P m = filter Q m.
Proof. rewrite map_filter_strong_ext. naive_solver. Qed.
(* stdpp/fin_maps.v *)
Lemma map_filter_strong_subseteq_ext (m1 m2 : M A) :
    filter P m1 ⊆ filter Q m2 ↔
    (∀ i x, (P (i, x) ∧ m1 !! i = Some x) → (Q (i, x) ∧ m2 !! i = Some x)).
Proof.
    rewrite map_subseteq_spec.
    setoid_rewrite map_lookup_filter_Some. naive_solver.
  Qed.
(* stdpp/fin_maps.v *)
Lemma map_filter_subseteq_ext (m : M A) :
    filter P m ⊆ filter Q m ↔
    (∀ i x, m !! i = Some x → P (i, x) → Q (i, x)).
Proof. rewrite map_filter_strong_subseteq_ext. naive_solver. Qed.
(* stdpp/fin_maps.v *)
Lemma map_filter_empty : filter P ∅ =@{M A} ∅.
Proof. apply map_fold_empty. Qed.
(* stdpp/fin_maps.v *)
Lemma map_empty_filter m :
    filter P m = ∅ ↔ map_Forall (λ i x, ¬P (i,x)) m.
Proof.
    rewrite map_empty. setoid_rewrite map_lookup_filter_None. split.
    - intros Hm i x Hi. destruct (Hm i); naive_solver.
    - intros Hm i. destruct (m !! i) as [x|] eqn:?; [|by auto].
      right; intros ? [= <-]. by apply Hm.
  Qed.
(* stdpp/fin_maps.v *)
Lemma map_empty_filter_1 m :
    filter P m = ∅ →
    map_Forall (λ i x, ¬P (i,x)) m.
Proof. apply map_empty_filter. Qed.
(* stdpp/fin_maps.v *)
Lemma map_empty_filter_2 m :
    map_Forall (λ i x, ¬P (i,x)) m →
    filter P m = ∅.
Proof. apply map_empty_filter. Qed.
(* stdpp/fin_maps.v *)
Lemma map_filter_delete m i : filter P (delete i m) = delete i (filter P m).
Proof.
    apply map_eq. intros j. apply option_eq; intros y.
    destruct (decide (j = i)) as [->|?].
    - rewrite map_lookup_filter_Some, !lookup_delete_eq. naive_solver.
    - rewrite lookup_delete_ne, !map_lookup_filter_Some, lookup_delete_ne by done.
      naive_solver.
  Qed.
(* stdpp/fin_maps.v *)
Lemma map_filter_delete_not m i:
    (∀ y, m !! i = Some y → ¬ P (i, y)) →
    filter P (delete i m) = filter P m.
Proof.
    intros. apply map_filter_strong_ext. intros j y.
    rewrite lookup_delete_Some. naive_solver.
  Qed.
(* stdpp/fin_maps.v *)
Lemma map_filter_insert m i x :
    filter P (<[i:=x]> m)
    = if decide (P (i, x)) then <[i:=x]> (filter P m) else filter P (delete i m).
Proof.
    apply map_eq. intros j. apply option_eq; intros y.
    rewrite map_lookup_filter_Some, lookup_insert_Some. case_decide.
    - rewrite lookup_insert_Some, map_lookup_filter_Some. naive_solver.
    - rewrite map_lookup_filter_Some, lookup_delete_Some. naive_solver.
  Qed.
(* stdpp/fin_maps.v *)
Lemma map_filter_insert_True m i x :
    P (i, x) → filter P (<[i:=x]> m) = <[i:=x]> (filter P m).
Proof. intros. by rewrite map_filter_insert, decide_True. Qed.
(* stdpp/fin_maps.v *)
Lemma map_filter_insert_False m i x :
    ¬ P (i, x) → filter P (<[i:=x]> m) = filter P (delete i m).
Proof. intros. by rewrite map_filter_insert, decide_False. Qed.
(* stdpp/fin_maps.v *)
Lemma map_filter_insert_not' m i x :
    ¬ P (i, x) → (∀ y, m !! i = Some y → ¬ P (i, y)) →
    filter P (<[i:=x]> m) = filter P m.
Proof.
    intros. rewrite map_filter_insert, decide_False by done.
    by rewrite map_filter_delete_not.
  Qed.
(* stdpp/fin_maps.v *)
Lemma map_filter_insert_not m i x :
    (∀ y, ¬ P (i, y)) → filter P (<[i:=x]> m) = filter P m.
Proof. intros. by apply map_filter_insert_not'. Qed.
(* stdpp/fin_maps.v *)
Lemma map_filter_singleton i x :
    filter P {[i:=x]} =@{M A} if decide (P (i, x)) then {[i:=x]} else ∅.
Proof.
    by rewrite <-!insert_empty, map_filter_insert, delete_empty, map_filter_empty.
  Qed.
(* stdpp/fin_maps.v *)
Lemma map_filter_singleton_True i x :
    P (i, x) → filter P {[i:=x]} =@{M A} {[i:=x]}.
Proof. intros. by rewrite map_filter_singleton, decide_True. Qed.
(* stdpp/fin_maps.v *)
Lemma map_filter_singleton_False i x :
    ¬ P (i, x) → filter P {[i:=x]} =@{M A} ∅.
Proof. intros. by rewrite map_filter_singleton, decide_False. Qed.
(* stdpp/fin_maps.v *)
Lemma map_filter_alt m : filter P m = list_to_map (filter P (map_to_list m)).
Proof.
    apply list_to_map_flip. induction m as [|k x m ? IH] using map_ind.
    { by rewrite map_to_list_empty, map_filter_empty, map_to_list_empty. }
    rewrite map_to_list_insert, filter_cons by done. destruct (decide (P _)).
    - rewrite map_filter_insert_True by done.
      by rewrite map_to_list_insert, IH by (rewrite map_lookup_filter_None; auto).
    - by rewrite map_filter_insert_not' by naive_solver.
  Qed.
(* stdpp/fin_maps.v *)
Lemma map_filter_fmap {B} (f : B → A) (m : M B) :
    filter P (f <$> m) = f <$> filter (λ '(i, x), P (i, (f x))) m.
Proof.
    apply map_eq. intros i. apply option_eq; intros x.
    repeat (rewrite lookup_fmap, fmap_Some || setoid_rewrite map_lookup_filter_Some).
    naive_solver.
  Qed.
(* stdpp/fin_maps.v *)
Lemma map_filter_filter Q `{!∀ x, Decision (Q x)} m :
    filter P (filter Q m) = filter (λ '(i, x), P (i, x) ∧ Q (i, x)) m.
Proof.
    apply map_filter_strong_ext. intros ??.
    rewrite map_lookup_filter_Some. naive_solver.
  Qed.
(* stdpp/fin_maps.v *)
Lemma map_filter_filter_l Q `{!∀ x, Decision (Q x)} m :
    (∀ i x, m !! i = Some x → P (i, x) → Q (i, x)) →
    filter P (filter Q m) = filter P m.
Proof. intros ?. rewrite map_filter_filter. apply map_filter_ext. naive_solver. Qed.
(* stdpp/fin_maps.v *)
Lemma map_filter_filter_r Q `{!∀ x, Decision (Q x)} m :
    (∀ i x, m !! i = Some x → Q (i, x) → P (i, x)) →
    filter P (filter Q m) = filter Q m.
Proof. intros ?. rewrite map_filter_filter. apply map_filter_ext. naive_solver. Qed.
(* stdpp/fin_maps.v *)
Lemma map_filter_id m :
    (∀ i x, m !! i = Some x → P (i, x)) → filter P m = m.
Proof.
    intros Hi. apply map_eq. intros i. rewrite map_lookup_filter.
    destruct (m !! i) eqn:Hlook; [|done].
    apply option_guard_True, Hi, Hlook.
  Qed.
(* stdpp/fin_maps.v *)
Lemma map_filter_subseteq m : filter P m ⊆ m.
Proof. apply map_subseteq_spec, map_lookup_filter_Some_1_1. Qed.
(* stdpp/fin_maps.v *)
Lemma map_filter_subseteq_mono m1 m2 : m1 ⊆ m2 → filter P m1 ⊆ filter P m2.
Proof.
    rewrite map_subseteq_spec. intros Hm1m2.
    apply map_filter_strong_subseteq_ext. naive_solver.
  Qed.
(* stdpp/fin_maps.v *)
Lemma map_size_filter m :
    size (filter P m) ≤ size m.
Proof. apply map_subseteq_size. apply map_filter_subseteq. Qed.
(* stdpp/fin_maps.v *)
Lemma map_filter_comm {A}
    (P Q : K * A → Prop) `{!∀ x, Decision (P x), !∀ x, Decision (Q x)} (m : M A) :
  filter P (filter Q m) = filter Q (filter P m).
Proof. rewrite !map_filter_filter. apply map_filter_ext. naive_solver. Qed.
(* stdpp/fin_maps.v *)
(* These instances can in many cases not be applied automatically due to Coq
  unification bug #6294. Hence there are many explicit derived instances for
  specific operations such as union or difference in the rest of this file. *)
Instance : LeftId (=) None f → LeftId (=@{M A}) ∅ (merge f).
Proof.
    intros ? m. apply map_eq; intros i.
    rewrite !lookup_merge, lookup_empty. destruct (m !! i); by simpl.
  Qed.
(* stdpp/fin_maps.v *)
Instance : RightId (=) None f → RightId (=@{M A}) ∅ (merge f).
Proof.
    intros ? m. apply map_eq; intros i.
    rewrite !lookup_merge, lookup_empty. destruct (m !! i); by simpl.
  Qed.
(* stdpp/fin_maps.v *)
Instance : LeftAbsorb (=) None f → LeftAbsorb (=@{M A}) ∅ (merge f).
Proof.
    intros ? m. apply map_eq; intros i.
    rewrite !lookup_merge, lookup_empty. destruct (m !! i); by simpl.
  Qed.
(* stdpp/fin_maps.v *)
Instance : RightAbsorb (=) None f → RightAbsorb (=@{M A}) ∅ (merge f).
Proof.
    intros ? m. apply map_eq; intros i.
    rewrite !lookup_merge, lookup_empty. destruct (m !! i); by simpl.
  Qed.
(* stdpp/fin_maps.v *)
Lemma merge_comm m1 m2 :
    (∀ i, f (m1 !! i) (m2 !! i) = f (m2 !! i) (m1 !! i)) →
    merge f m1 m2 = merge f m2 m1.
Proof.
    intros Hm. apply map_eq; intros i. specialize (Hm i).
    rewrite !lookup_merge. by destruct (m1 !! i), (m2 !! i).
  Qed.
(* stdpp/fin_maps.v *)
Instance merge_comm' : Comm (=) f → Comm (=@{M A}) (merge f).
Proof. intros ???. apply merge_comm. intros. by apply (comm f). Qed.
(* stdpp/fin_maps.v *)
Lemma merge_assoc m1 m2 m3 :
    (∀ i, diag_None f (m1 !! i) (diag_None f (m2 !! i) (m3 !! i)) =
          diag_None f (diag_None f (m1 !! i) (m2 !! i)) (m3 !! i)) →
    merge f m1 (merge f m2 m3) = merge f (merge f m1 m2) m3.
Proof.
    intros Hm. apply map_eq; intros i. specialize (Hm i).
    by rewrite !lookup_merge.
  Qed.
(* stdpp/fin_maps.v *)
Lemma merge_idemp m1 :
    (∀ i, f (m1 !! i) (m1 !! i) = m1 !! i) → merge f m1 m1 = m1.
Proof.
    intros Hm. apply map_eq; intros i. specialize (Hm i).
    rewrite !lookup_merge. by destruct (m1 !! i).
  Qed.
(* stdpp/fin_maps.v *)
Instance merge_idemp' : IdemP (=) f → IdemP (=@{M A}) (merge f).
Proof. intros ??. apply merge_idemp. intros. by apply (idemp f). Qed.
(* stdpp/fin_maps.v *)
Lemma merge_Some (m1 : M A) (m2 : M B) (m : M C) :
    f None None = None →
    (∀ i, m !! i = f (m1 !! i) (m2 !! i)) ↔ merge f m1 m2 = m.
Proof.
   intros. rewrite map_eq_iff. apply forall_proper; intros i.
   rewrite lookup_merge. destruct (m1 !! i), (m2 !! i); naive_solver congruence.
  Qed.
(* stdpp/fin_maps.v *)
Lemma merge_empty : merge f ∅ ∅ =@{M C} ∅.
Proof. apply map_eq. intros. by rewrite !lookup_merge, !lookup_empty. Qed.
(* stdpp/fin_maps.v *)
Lemma partial_alter_merge g g1 g2 (m1 : M A) (m2 : M B) i :
    g (diag_None f (m1 !! i) (m2 !! i)) = diag_None f (g1 (m1 !! i)) (g2 (m2 !! i)) →
    partial_alter g i (merge f m1 m2) =
      merge f (partial_alter g1 i m1) (partial_alter g2 i m2).
Proof.
    intro. apply map_eq. intros j. destruct (decide (i = j)); subst.
    - by rewrite lookup_merge, !lookup_partial_alter_eq, !lookup_merge.
    - by rewrite lookup_merge, !lookup_partial_alter_ne, lookup_merge.
  Qed.
(* stdpp/fin_maps.v *)
Lemma partial_alter_merge_l g g1 (m1 : M A) (m2 : M B) i :
    g (diag_None f (m1 !! i) (m2 !! i)) = diag_None f (g1 (m1 !! i)) (m2 !! i) →
    partial_alter g i (merge f m1 m2) = merge f (partial_alter g1 i m1) m2.
Proof.
    intro. apply map_eq. intros j. destruct (decide (i = j)); subst.
    - by rewrite lookup_merge, !lookup_partial_alter_eq, !lookup_merge.
    - by rewrite lookup_merge, !lookup_partial_alter_ne, lookup_merge.
  Qed.
(* stdpp/fin_maps.v *)
Lemma partial_alter_merge_r g g2 (m1 : M A) (m2 : M B) i :
    g (diag_None f (m1 !! i) (m2 !! i)) = diag_None f (m1 !! i) (g2 (m2 !! i)) →
    partial_alter g i (merge f m1 m2) = merge f m1 (partial_alter g2 i m2).
Proof.
    intro. apply map_eq. intros j. destruct (decide (i = j)); subst.
    - by rewrite lookup_merge, !lookup_partial_alter_eq, !lookup_merge.
    - by rewrite lookup_merge, !lookup_partial_alter_ne, lookup_merge.
  Qed.
(* stdpp/fin_maps.v *)
Lemma insert_merge (m1 : M A) (m2 : M B) i x y z :
    f (Some y) (Some z) = Some x →
    <[i:=x]>(merge f m1 m2) = merge f (<[i:=y]> m1) (<[i:=z]> m2).
Proof. intros; by apply partial_alter_merge. Qed.
(* stdpp/fin_maps.v *)
Lemma delete_merge (m1 : M A) (m2 : M B) i :
    delete i (merge f m1 m2) = merge f (delete i m1) (delete i m2).
Proof. intros; by apply partial_alter_merge. Qed.
(* stdpp/fin_maps.v *)
Lemma merge_singleton i x y z :
    f (Some y) (Some z) = Some x →
    merge f {[i:=y]} {[i:=z]} =@{M C} {[i:=x]}.
Proof.
    intros. by erewrite <-!insert_empty, <-insert_merge, merge_empty by eauto.
  Qed.
(* stdpp/fin_maps.v *)
Lemma insert_merge_l (m1 : M A) (m2 : M B) i x y :
    f (Some y) (m2 !! i) = Some x →
    <[i:=x]>(merge f m1 m2) = merge f (<[i:=y]> m1) m2.
Proof. by intros; apply partial_alter_merge_l. Qed.
(* stdpp/fin_maps.v *)
Lemma insert_merge_r (m1 : M A) (m2 : M B) i x z :
    f (m1 !! i) (Some z) = Some x →
    <[i:=x]>(merge f m1 m2) = merge f m1 (<[i:=z]> m2).
Proof. intros; apply partial_alter_merge_r. by destruct (m1 !! i). Qed.
(* stdpp/fin_maps.v *)
Lemma fmap_merge {D} (g : C → D) (m1 : M A) (m2 : M B) :
    g <$> merge f m1 m2 = merge (λ mx1 mx2, g <$> f mx1 mx2) m1 m2.
Proof.
    apply map_eq; intros i. rewrite lookup_fmap, !lookup_merge.
    by destruct (m1 !! i), (m2 !! i).
  Qed.
(* stdpp/fin_maps.v *)
Lemma omap_merge {D} (g : C → option D) (m1 : M A) (m2 : M B) :
    omap g (merge f m1 m2) = merge (λ mx1 mx2, f mx1 mx2 ≫= g) m1 m2.
Proof.
    apply map_eq; intros i. rewrite lookup_omap, !lookup_merge.
    by destruct (m1 !! i), (m2 !! i).
  Qed.
(* stdpp/fin_maps.v *)
Lemma merge_empty_l {A B C} (f : option A → option B → option C) (m2 : M B) :
  merge f ∅ m2 = omap (f None ∘ Some) m2.
Proof.
  apply map_eq; intros i. rewrite lookup_merge, lookup_omap, lookup_empty.
  by destruct (m2 !! i).
Qed.
(* stdpp/fin_maps.v *)
Lemma merge_empty_r {A B C} (f : option A → option B → option C) (m1 : M A) :
  merge f m1 ∅ = omap (flip f None ∘ Some) m1.
Proof.
  apply map_eq; intros i. rewrite lookup_merge, lookup_omap, lookup_empty.
  by destruct (m1 !! i).
Qed.
(* stdpp/fin_maps.v *)
Lemma merge_diag {A C} (f : option A → option A → option C) (m : M A) :
  merge f m m = omap (λ x, f (Some x) (Some x)) m.
Proof.
  apply map_eq. intros i.
  rewrite lookup_merge, lookup_omap. by destruct (m !! i).
Qed.
(* stdpp/fin_maps.v *)
(* Properties of the [map_zip_with] and [map_zip] functions *)
Lemma map_lookup_zip_with {A B C} (f : A → B → C) (m1 : M A) (m2 : M B) i :
  map_zip_with f m1 m2 !! i = (x ← m1 !! i; y ← m2 !! i; Some (f x y)).
Proof.
  unfold map_zip_with. rewrite lookup_merge.
  by destruct (m1 !! i), (m2 !! i).
Qed.
(* stdpp/fin_maps.v *)
Lemma map_lookup_zip_with_Some {A B C} (f : A → B → C) (m1 : M A) (m2 : M B) i z :
  map_zip_with f m1 m2 !! i = Some z ↔
    ∃ x y, z = f x y ∧ m1 !! i = Some x ∧ m2 !! i = Some y.
Proof. rewrite map_lookup_zip_with. destruct (m1 !! i), (m2 !! i); naive_solver. Qed.
(* stdpp/fin_maps.v *)
Lemma map_lookup_zip_with_None {A B C} (f : A → B → C) (m1 : M A) (m2 : M B) i :
  map_zip_with f m1 m2 !! i = None ↔ m1 !! i = None ∨ m2 !! i = None.
Proof. rewrite map_lookup_zip_with. destruct (m1 !! i), (m2 !! i); naive_solver. Qed.
(* stdpp/fin_maps.v *)
Lemma map_lookup_zip_Some {A B} (m1 : M A) (m2 : M B) i p :
  map_zip m1 m2 !! i = Some p ↔ m1 !! i = Some p.1 ∧ m2 !! i = Some p.2.
Proof. rewrite map_lookup_zip_with_Some. destruct p. naive_solver. Qed.
(* stdpp/fin_maps.v *)
Lemma map_zip_with_empty {A B C} (f : A → B → C) :
  map_zip_with f ∅ ∅ =@{M C} ∅.
Proof. unfold map_zip_with. by rewrite merge_empty by done. Qed.
(* stdpp/fin_maps.v *)
Lemma map_zip_with_empty_l {A B C} (f : A → B → C) m2 :
  map_zip_with f ∅ m2 =@{M C} ∅.
Proof.
  unfold map_zip_with. apply map_eq; intros i.
  rewrite lookup_merge, !lookup_empty. destruct (m2 !! i); done.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_zip_with_empty_r {A B C} (f : A → B → C) m1 :
  map_zip_with f m1 ∅ =@{M C} ∅.
Proof.
  unfold map_zip_with. apply map_eq; intros i.
  rewrite lookup_merge, !lookup_empty. destruct (m1 !! i); done.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_insert_zip_with {A B C} (f : A → B → C) (m1 : M A) (m2 : M B) i y z :
  <[i:=f y z]>(map_zip_with f m1 m2) = map_zip_with f (<[i:=y]> m1) (<[i:=z]> m2).
Proof. unfold map_zip_with. by erewrite insert_merge by done. Qed.
(* stdpp/fin_maps.v *)
Lemma map_delete_zip_with {A B C} (f : A → B → C) (m1 : M A) (m2 : M B) i :
  delete i (map_zip_with f m1 m2) = map_zip_with f (delete i m1) (delete i m2).
Proof. unfold map_zip_with. by rewrite delete_merge. Qed.
(* stdpp/fin_maps.v *)
Lemma map_zip_with_singleton {A B C} (f : A → B → C) i x y :
  map_zip_with f {[i:=x]} {[i:=y]} =@{M C} {[i:=f x y]}.
Proof. unfold map_zip_with. by erewrite merge_singleton. Qed.
(* stdpp/fin_maps.v *)
Lemma map_zip_with_fmap {A' A B' B C} (f : A → B → C)
    (g1 : A' → A) (g2 : B' → B) (m1 : M A') (m2 : M B') :
  map_zip_with f (g1 <$> m1) (g2 <$> m2) = map_zip_with (λ x y, f (g1 x) (g2 y)) m1 m2.
Proof.
  apply map_eq; intro i. rewrite !map_lookup_zip_with, !lookup_fmap.
  by destruct (m1 !! i), (m2 !! i).
Qed.
(* stdpp/fin_maps.v *)
Lemma map_zip_with_fmap_1 {A' A B C} (f : A → B → C)
    (g : A' → A) (m1 : M A') (m2 : M B) :
  map_zip_with f (g <$> m1) m2 = map_zip_with (λ x y, f (g x) y) m1 m2.
Proof.
  rewrite <- (map_fmap_id m2) at 1. by rewrite map_zip_with_fmap.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_zip_with_fmap_2 {A B' B C} (f : A → B → C)
    (g : B' → B) (m1 : M A) (m2 : M B') :
  map_zip_with f m1 (g <$> m2) = map_zip_with (λ x y, f x (g y)) m1 m2.
Proof.
  rewrite <-(map_fmap_id m1) at 1. by rewrite map_zip_with_fmap.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_fmap_zip_with {A B C D} (f : A → B → C) (g : C → D)
    (m1 : M A) (m2 : M B) :
  g <$> map_zip_with f m1 m2 = map_zip_with (λ x y, g (f x y)) m1 m2.
Proof.
  apply map_eq; intro i. rewrite lookup_fmap, !map_lookup_zip_with.
  by destruct (m1 !! i), (m2 !! i).
Qed.
(* stdpp/fin_maps.v *)
Lemma map_zip_with_flip {A B C} (f : A → B → C) (m1 : M A) (m2 : M B) :
  map_zip_with (flip f) m2 m1 = map_zip_with f m1 m2.
Proof.
  apply map_eq; intro i. rewrite !map_lookup_zip_with.
  by destruct (m1 !! i), (m2 !! i).
Qed.
(* stdpp/fin_maps.v *)
Lemma map_zip_with_map_zip {A B C} (f : A → B → C) (m1 : M A) (m2 : M B) :
  map_zip_with f m1 m2 = uncurry f <$> map_zip m1 m2.
Proof.
  apply map_eq; intro i. rewrite lookup_fmap, !map_lookup_zip_with.
  by destruct (m1 !! i), (m2 !! i).
Qed.
(* stdpp/fin_maps.v *)
Lemma map_fmap_zip {A' A B' B} (g1 : A' → A)
    (g2 : B' → B) (m1 : M A') (m2 : M B') :
  map_zip (fmap g1 m1) (fmap g2 m2) = prod_map g1 g2 <$> map_zip m1 m2.
Proof.
  rewrite map_zip_with_fmap, map_zip_with_map_zip.
  generalize (map_zip m1 m2); intro m. apply map_eq; intro i.
  by rewrite !lookup_fmap; destruct (m !! i) as [[x1 x2]|].
Qed.
(* stdpp/fin_maps.v *)
Lemma map_fmap_zip_with_l
    {A B C} (f : A → B → C) (g : C → A) (m1 : M A) (m2 : M B) :
  (∀ x y, g (f x y) = x) →
  (∀ k, is_Some (m1 !! k) → is_Some (m2 !! k)) →
  g <$> map_zip_with f m1 m2 = m1.
Proof.
  intros ? Hm. apply map_eq; intros k. rewrite lookup_fmap, map_lookup_zip_with.
  destruct (m1 !! _) as [x|] eqn:?; simpl; [|done].
  destruct (Hm k) as [y ->]; [by eauto|]. by f_equal/=.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_fmap_zip_with_r
    {A B C} (f : A → B → C) (g : C → B) (m1 : M A) (m2 : M B) :
  (∀ x y, g (f x y) = y) →
  (∀ k, is_Some (m2 !! k) → is_Some (m1 !! k)) →
  g <$> map_zip_with f m1 m2 = m2.
Proof.
  intros ? Hm. apply map_eq; intros k. rewrite lookup_fmap, map_lookup_zip_with.
  destruct (m2 !! _) as [x|] eqn:?; simpl; [|by destruct (m1 !! _)].
  destruct (Hm k) as [y ->]; [by eauto|]. by f_equal/=.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_zip_with_diag {A C} (f : A → A → C) (m : M A) :
  map_zip_with f m m = (λ x, f x x) <$> m.
Proof. unfold map_zip_with. by rewrite merge_diag, map_fmap_alt. Qed.
(* stdpp/fin_maps.v *)
Lemma map_zip_diag {A} (m : M A) :
  map_zip m m = (λ x, (x, x)) <$> m.
Proof. apply map_zip_with_diag. Qed.
(* stdpp/fin_maps.v *)
Lemma fst_map_zip {A B} (m1 : M A) (m2 : M B) :
  (∀ k : K, is_Some (m1 !! k) → is_Some (m2 !! k)) →
  fst <$> map_zip m1 m2 = m1.
Proof. intros ?. by apply map_fmap_zip_with_l. Qed.
(* stdpp/fin_maps.v *)
Lemma snd_map_zip {A B} (m1 : M A) (m2 : M B) :
  (∀ k : K, is_Some (m2 !! k) → is_Some (m1 !! k)) →
  snd <$> map_zip m1 m2 = m2.
Proof. intros ?. by apply map_fmap_zip_with_r. Qed.
(* stdpp/fin_maps.v *)
Lemma map_zip_fst_snd {A B} (m : M (A * B)) :
  map_zip (fst <$> m) (snd <$> m) = m.
Proof.
  apply map_eq; intros k.
  rewrite map_lookup_zip_with, !lookup_fmap. by destruct (m !! k) as [[]|].
Qed.
(* stdpp/fin_maps.v *)
(* The function [f] and lemma [map_relation_alt] are helpers to prove the
  [Decision] instance. These should not be used elsewhere. *)
Let f (mx : option A) (my : option B) : option (K → bool)
:=
    match mx, my with
    | Some x, Some y => Some (λ i, bool_decide (R i x y))
    | Some x, None => Some (λ i, bool_decide (P i x))
    | None, Some y => Some (λ i, bool_decide (Q i y))
    | None, None => None
    end.
(* stdpp/fin_maps.v *)
Lemma map_relation_alt (m1 : M A) (m2 : M B) :
    map_relation R P Q m1 m2 ↔ map_Forall (λ i b, Is_true (b i)) (merge f m1 m2).
Proof.
    split.
    - intros Hm i P'; rewrite lookup_merge; intros.
      specialize (Hm i). destruct (m1 !! i), (m2 !! i);
        simplify_eq/=; auto using bool_decide_pack.
    - intros Hm i. specialize (Hm i). rewrite lookup_merge in Hm.
      destruct (m1 !! i), (m2 !! i); simplify_eq/=; auto;
        eapply bool_decide_unpack, (Hm _ eq_refl).
  Qed.
(* stdpp/fin_maps.v *)
Instance map_relation_dec : RelDecision (map_relation (M:=M) R P Q).
Proof.
    refine (λ m1 m2,
      cast_if (decide (map_Forall (λ i b, Is_true (b i)) (merge f m1 m2))));
      abstract by rewrite map_relation_alt.
  Defined.
(* stdpp/fin_maps.v *)
(* Due to the finiteness of finite maps, we can extract a witness if the
  relation does not hold. *)
Lemma map_not_relation (m1 : M A) (m2 : M B) :
    ¬map_relation R P Q m1 m2 ↔ ∃ i,
      (∃ x y, m1 !! i = Some x ∧ m2 !! i = Some y ∧ ¬R i x y)
      ∨ (∃ x, m1 !! i = Some x ∧ m2 !! i = None ∧ ¬P i x)
      ∨ (∃ y, m1 !! i = None ∧ m2 !! i = Some y ∧ ¬Q i y).
Proof.
    split.
    - rewrite map_relation_alt, (map_not_Forall _). intros (i&?&Hm&?); exists i.
      rewrite lookup_merge in Hm.
      destruct (m1 !! i), (m2 !! i); naive_solver auto 2 using bool_decide_pack.
    - unfold map_relation, option_relation.
      by intros [i[(x&y&?&?&?)|[(x&?&?&?)|(y&?&?&?)]]] Hm;
        specialize (Hm i); simplify_option_eq.
  Qed.