phanerozoic/Coq-Stdpp huggingface dataset:
(* stdpp/fin_maps.v *)
Lemma map_imap_empty {A B} (f : K → A → option B) :
  map_imap f ∅ =@{M B} ∅.
Proof. apply map_eq; intros i. by rewrite map_lookup_imap, !lookup_empty. Qed.
(* stdpp/fin_maps.v *)
Lemma map_fmap_imap {A B C} (f : K → A → option B) (g : B → C) (m : M A) :
  g <$> map_imap f m = map_imap (λ i x, g <$> f i x) m.
Proof.
  apply map_eq. intros i. rewrite lookup_fmap.
  rewrite !map_lookup_imap. by destruct (m !! i).
Qed.
(* stdpp/fin_maps.v *)
(* ** Properties of the size operation *)
Lemma map_size_empty {A} : size (∅ : M A) = 0.
Proof. by rewrite <-length_map_to_list, map_to_list_empty. Qed.
(* stdpp/fin_maps.v *)
Lemma map_size_empty_iff {A} (m : M A) : size m = 0 ↔ m = ∅.
Proof.
  by rewrite <-length_map_to_list, length_zero_iff_nil, map_to_list_empty_iff.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_size_empty_inv {A} (m : M A) : size m = 0 → m = ∅.
Proof. apply map_size_empty_iff. Qed.
(* stdpp/fin_maps.v *)
Lemma map_size_non_empty_iff {A} (m : M A) : size m ≠ 0 ↔ m ≠ ∅.
Proof. by rewrite map_size_empty_iff. Qed.
(* stdpp/fin_maps.v *)
Lemma map_size_singleton {A} i (x : A) : size ({[i:=x]} : M A) = 1.
Proof. by rewrite <-length_map_to_list, map_to_list_singleton. Qed.
(* stdpp/fin_maps.v *)
Lemma map_size_ne_0_lookup {A} (m : M A) :
  size m ≠ 0 ↔ ∃ i, is_Some (m !! i).
Proof.
  rewrite map_size_non_empty_iff. split.
  - intros Hsz. apply map_choose. intros Hemp. done.
  - intros [i [k Hi]] ->. rewrite lookup_empty in Hi. done.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_size_ne_0_lookup_1 {A} (m : M A) :
  size m ≠ 0 → ∃ i, is_Some (m !! i).
Proof. intros. by eapply map_size_ne_0_lookup. Qed.
(* stdpp/fin_maps.v *)
Lemma map_size_ne_0_lookup_2 {A} (m : M A) i :
  is_Some (m !! i) → size m ≠ 0.
Proof. intros. eapply map_size_ne_0_lookup. eauto. Qed.
(* stdpp/fin_maps.v *)
Lemma map_size_insert {A} i x (m : M A) :
  size (<[i:=x]> m) = (match m !! i with Some _ => id | None => S end) (size m).
Proof.
  destruct (m !! i) as [y|] eqn:?; simpl.
  - rewrite <-(insert_id m i y) at 2 by done. rewrite <-!(insert_delete_eq m).
    rewrite <-!length_map_to_list.
    by rewrite !map_to_list_insert by (by rewrite lookup_delete_eq).
  - by rewrite <-!length_map_to_list, map_to_list_insert.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_size_insert_Some {A} i x (m : M A) :
  is_Some (m !! i) → size (<[i:=x]> m) = size m.
Proof. intros [y Hi]. by rewrite map_size_insert, Hi. Qed.
(* stdpp/fin_maps.v *)
Lemma map_size_insert_None {A} i x (m : M A) :
  m !! i = None → size (<[i:=x]> m) = S (size m).
Proof. intros Hi. by rewrite map_size_insert, Hi. Qed.
(* stdpp/fin_maps.v *)
Lemma map_size_delete {A} i (m : M A) :
  size (delete i m) = (match m !! i with Some _ => pred | None => id end) (size m).
Proof.
  destruct (m !! i) as [y|] eqn:?; simpl.
  - by rewrite <-!length_map_to_list, <-(map_to_list_delete m).
  - by rewrite delete_id.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_size_delete_Some {A} i (m : M A) :
  is_Some (m !! i) → size (delete i m) = pred (size m).
Proof. intros [y Hi]. by rewrite map_size_delete, Hi. Qed.
(* stdpp/fin_maps.v *)
Lemma map_size_delete_None {A} i (m : M A) :
  m !! i = None → size (delete i m) = size m.
Proof. intros Hi. by rewrite map_size_delete, Hi. Qed.
(* stdpp/fin_maps.v *)
Lemma map_size_alter {A} i f (m : M A) : size (alter f i m) = size m.
Proof. rewrite alter_alt. case_match; eauto using map_size_insert_Some. Qed.
(* stdpp/fin_maps.v *)
Lemma map_size_fmap {A B} (f : A -> B) (m : M A) : size (f <$> m) = size m.
Proof.
  intros. by rewrite <-!length_map_to_list, map_to_list_fmap_weak, length_fmap.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_size_list_to_map {A} (l : list (K * A)) :
  NoDup l.*1 →
  size (list_to_map l : M A) = length l.
Proof.
  induction l; csimpl; inv 1; simplify_eq/=; [by rewrite map_size_empty|].
  rewrite map_size_insert_None by eauto using not_elem_of_list_to_map_1.
  eauto with f_equal.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_subseteq_size_eq {A} (m1 m2 : M A) :
  m1 ⊆ m2 → size m2 ≤ size m1 → m1 = m2.
Proof.
  intros. apply map_to_list_inj, submseteq_length_Permutation.
  - by apply map_to_list_submseteq.
  - by rewrite !length_map_to_list.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_subseteq_size {A} (m1 m2 : M A) : m1 ⊆ m2 → size m1 ≤ size m2.
Proof.
  intros. rewrite <-!length_map_to_list.
  by apply submseteq_length, map_to_list_submseteq.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_subset_size {A} (m1 m2 : M A) : m1 ⊂ m2 → size m1 < size m2.
Proof.
  intros [Hm12 Hm21]. apply Nat.le_neq. split.
  - by apply map_subseteq_size.
  - intros Hsize. destruct Hm21.
    apply reflexive_eq, symmetry, map_subseteq_size_eq; auto with lia.
Qed.
(* stdpp/fin_maps.v *)
(* ** Induction principles *)
Lemma map_wf {A} : well_founded (⊂@{M A}).
Proof. apply (wf_projected (<) size); auto using map_subset_size, lt_wf. Qed.
(* stdpp/fin_maps.v *)
Lemma map_ind {A} (P : M A → Prop) :
  P ∅ → (∀ i x m, m !! i = None → P m → P (<[i:=x]> m)) → ∀ m, P m.
Proof.
  intros ? Hins m. induction (map_wf m) as [m _ IH].
  destruct (map_choose_or_empty m) as [(i&x&?)| ->]; [|done].
  rewrite <-(insert_delete_id m i x) by done.
  apply Hins; [by rewrite lookup_delete_eq|]. by apply IH, delete_subset.
Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_set_to_map_Some (f : K → A) (Y : C) i x :
    (set_to_map f Y : M A) !! i = Some x ↔ i ∈ Y ∧ f i = x.
Proof.
    unfold set_to_map; rewrite <-elem_of_list_to_map' by set_solver.
    rewrite list_elem_of_fmap. setoid_rewrite elem_of_elements; naive_solver.
  Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_set_to_map_is_Some (f : K → A) (Y : C) i :
    is_Some ((set_to_map f Y : M A) !! i) ↔ i ∈ Y.
Proof. unfold is_Some. setoid_rewrite lookup_set_to_map_Some. naive_solver. Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_set_to_map_None (f : K → A) (Y : C) i :
    ((set_to_map f Y : M A) !! i) = None ↔ i ∉ Y.
Proof. by rewrite !eq_None_not_Some, lookup_set_to_map_is_Some. Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_set_to_map `{!RelDecision (∈@{C})} (f : K → A) (Y : C) i :
    (set_to_map f Y : M A) !! i = (guard (i ∈ Y);; Some (f i)).
Proof.
    apply option_eq; intros x. rewrite lookup_set_to_map_Some.
    case_guard; naive_solver.
  Qed.
(* stdpp/fin_maps.v *)
Instance set_to_map_proper (f : K → A) :
    Proper ((≡@{C}) ==> (=@{M A})) (set_to_map f).
Proof.
    intros X1 X2 HX. apply map_eq; intros i. apply option_eq; intros x.
    by rewrite !lookup_set_to_map_Some, HX.
  Qed.
(* stdpp/fin_maps.v *)
(* [set_to_map_inj_L] has a lower cost than [set_to_map_inj] so that it is
  prefered if the set has [LeibnizEquiv]. *)
Instance set_to_map_inj f : Inj (≡@{C}) (=@{M A}) (set_to_map f) | 10.
Proof.
    intros X1 X2. rewrite map_eq_iff. setoid_rewrite option_eq.
    setoid_rewrite lookup_set_to_map_Some. set_solver.
  Qed.
(* stdpp/fin_maps.v *)
Instance set_to_map_inj_L `{!LeibnizEquiv C} f :
    Inj (=@{C}) (=@{M A}) (set_to_map f) | 0.
Proof. intros X1 X2. unfold_leibniz. apply set_to_map_inj. Qed.
(* stdpp/fin_maps.v *)
Lemma set_to_map_empty (f : K → A) : set_to_map f (∅ : C) =@{M A} ∅.
Proof.
    apply map_eq; intros i. apply option_eq; intros x.
    rewrite lookup_set_to_map_Some, lookup_empty. set_solver.
  Qed.
(* stdpp/fin_maps.v *)
Lemma set_to_map_insert (f : K → A) (Y : C) i :
    set_to_map f ({[ i ]} ∪ Y) =@{M A} <[i:=f i]> (set_to_map f Y).
Proof.
    apply map_eq; intros j. apply option_eq; intros x.
    rewrite lookup_insert_Some, !lookup_set_to_map_Some.
    destruct (decide (i = j)); set_solver.
  Qed.
(* stdpp/fin_maps.v *)
Lemma set_to_map_delete (f : K → A) (Y : C) i :
    set_to_map f (Y ∖ {[ i ]}) =@{M A} delete i (set_to_map f Y).
Proof.
    apply map_eq; intros j. apply option_eq; intros x.
    rewrite lookup_delete_Some, !lookup_set_to_map_Some.
    destruct (decide (i = j)); set_solver.
  Qed.
(* stdpp/fin_maps.v *)
Lemma set_to_map_singleton (f : K → A) i :
    set_to_map f ({[ i ]} : C) =@{M A} {[ i := f i ]}.
Proof.
    by rewrite <-(right_id ∅ (∪) {[ i ]}), set_to_map_insert, set_to_map_empty.
  Qed.
(* stdpp/fin_maps.v *)
Lemma set_to_map_subseteq_ext (f : K → A) (Y1 Y2 : C) :
    set_to_map f Y1 ⊆@{M A} set_to_map f Y2 ↔ Y1 ⊆ Y2.
Proof.
    rewrite map_subseteq_spec.
    setoid_rewrite lookup_set_to_map_Some. set_solver.
  Qed.
(* stdpp/fin_maps.v *)
Lemma set_to_map_mono (f : K → A) (Y1 Y2 : C) :
    Y1 ⊆ Y2 → set_to_map f Y1 ⊆@{M A} set_to_map f Y2.
Proof. apply set_to_map_subseteq_ext. Qed.
(* stdpp/fin_maps.v *)
Lemma set_to_map_strict_mono (f : K → A) (Y1 Y2 : C) :
    Y1 ⊂ Y2 → set_to_map f Y1 ⊂@{M A} set_to_map f Y2.
Proof. unfold strict. by rewrite !(set_to_map_subseteq_ext f). Qed.
(* stdpp/fin_maps.v *)
Lemma elem_of_map_to_set (f : K → A → B) (m : M A) (y : B) :
    y ∈ map_to_set (C:=C) f m ↔ ∃ i x, m !! i = Some x ∧ f i x = y.
Proof.
    unfold map_to_set; simpl.
    rewrite elem_of_list_to_set, list_elem_of_fmap. split.
    - intros ([i x] & ? & ?%elem_of_map_to_list); eauto.
    - intros (i&x&?&?). exists (i,x). by rewrite elem_of_map_to_list.
  Qed.
(* stdpp/fin_maps.v *)
Lemma map_to_set_empty (f : K → A → B) :
    map_to_set f (∅ : M A) = (∅ : C).
Proof. unfold map_to_set; simpl. by rewrite map_to_list_empty. Qed.
(* stdpp/fin_maps.v *)
Lemma map_to_set_insert (f : K → A → B)(m : M A) i x :
    m !! i = None →
    map_to_set f (<[i:=x]> m) ≡@{C} {[f i x]} ∪ map_to_set f m.
Proof.
    intros. unfold map_to_set; simpl. by rewrite map_to_list_insert.
  Qed.
(* stdpp/fin_maps.v *)
Lemma map_to_set_insert_L `{!LeibnizEquiv C} (f : K → A → B) (m : M A) i x :
    m !! i = None →
    map_to_set f (<[i:=x]> m) =@{C} {[f i x]} ∪ map_to_set f m.
Proof. unfold_leibniz. apply map_to_set_insert. Qed.
(* stdpp/fin_maps.v *)
Lemma elem_of_map_to_set_pair `{SemiSet (K * A) C} (m : M A) i x :
  (i,x) ∈@{C} map_to_set pair m ↔ m !! i = Some x.
Proof. rewrite elem_of_map_to_set. naive_solver. Qed.
(* stdpp/fin_maps.v *)
(* ** The fold operation *)
Lemma map_fold_foldr {A B} (f : K → A → B → B) b (m : M A) :
  map_fold f b m = foldr (uncurry f) b (map_to_list m).
Proof.
  unfold map_to_list. induction m as [|i x m ? Hfold IH] using map_fold_ind.
  - by rewrite !map_fold_empty.
  - by rewrite !Hfold, IH.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_fold_fmap {A A' B} (f : K → A' → B → B) (g : A → A') b (m : M A) :
  map_fold f b (g <$> m) = map_fold (λ i, f i ∘ g) b m.
Proof.
  induction m as [|i x m ? Hfold IH] using map_fold_fmap_ind.
  { by rewrite fmap_empty, !map_fold_empty. }
  rewrite fmap_insert. rewrite <-(map_fmap_id m) at 2. rewrite !Hfold.
  by rewrite IH, map_fmap_id.
Qed.
(* stdpp/fin_maps.v *)
(* FIXME (Improve order): Move to [map_to_list] section. Moving requires a
bunch of reordering in this file. *)
Lemma map_to_list_fmap {A B} (f : A → B) (m : M A) :
  map_to_list (f <$> m) = prod_map id f <$> map_to_list m.
Proof.
  unfold map_to_list. rewrite map_fold_fmap, !map_fold_foldr.
  induction (map_to_list m) as [|[]]; f_equal/=; auto.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_fold_singleton {A B} (f : K → A → B → B) (b : B) i x :
  map_fold f b {[i:=x]} = f i x b.
Proof. by rewrite map_fold_foldr, map_to_list_singleton. Qed.
(* stdpp/fin_maps.v *)
Lemma map_fold_delete_first_key {A B} (f : K → A → B → B) b (m : M A) i x :
  m !! i = Some x →
  map_first_key m i →
  map_fold f b m = f i x (map_fold f b (delete i m)).
Proof.
  intros Hi [x' ([] & ixs & Hixs & ?)%list_elem_of_split_length]; simplify_eq/=.
  destruct m as [|j y m ? Hfold _] using map_fold_ind.
  { by rewrite map_to_list_empty in Hixs. }
  unfold map_to_list in Hixs. rewrite Hfold in Hixs. simplify_eq.
  rewrite lookup_insert_eq in Hi. simplify_eq.
  by rewrite Hfold, delete_insert_id.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_fold_insert_first_key {A B} (f : K → A → B → B) b (m : M A) i x :
  m !! i = None →
  map_first_key (<[i:=x]> m) i →
  map_fold f b (<[i:=x]> m) = f i x (map_fold f b m).
Proof.
  intros. rewrite <-(delete_insert_id m i x) at 2 by done.
  apply map_fold_delete_first_key; auto using lookup_insert_eq.
Qed.
(* stdpp/fin_maps.v *)
(* FIXME (Improve order): Move to [map_to_list] section. Moving requires a
bunch of reordering in this file. *)
Lemma map_to_list_delete_first_key {A} (m : M A) i x :
  m !! i = Some x →
  map_first_key m i →
  map_to_list m = (i,x) :: map_to_list (delete i m).
Proof.
  intros. unfold map_to_list. by erewrite map_fold_delete_first_key by done.
Qed.
(* stdpp/fin_maps.v *)
(* FIXME (Improve order): Move to [map_to_list] section. Moving requires a
bunch of reordering in this file. *)
Lemma map_to_list_insert_first_key {A} (m : M A) i x :
  m !! i = None →
  map_first_key (<[i:=x]> m) i →
  map_to_list (<[i:=x]> m) = (i,x) :: map_to_list m.
Proof.
  intros. unfold map_to_list. by rewrite map_fold_insert_first_key by done.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_first_key_fmap {A B} (f : A → B) (m : M A) i :
  map_first_key (f <$> m) i ↔ map_first_key m i.
Proof.
  split.
  - intros [x Hm]. rewrite map_to_list_fmap, list_lookup_fmap, fmap_Some in Hm.
    destruct Hm as ([i' x'] & Hm & ?); simplify_eq/=. by exists x'.
  - intros [x Hm]. exists (f x).
    by rewrite map_to_list_fmap, list_lookup_fmap, Hm.
Qed.
(* stdpp/fin_maps.v *)
(* We do not have [dom] here, [map_first_key_same_dom] from [fin_map_dom] is
typically more convenient. *)
Lemma map_first_key_dom' {A B} (m1 : M A) (m2 : M B) i :
  (∀ j, is_Some (m1 !! j) ↔ is_Some (m2 !! j)) →
  map_first_key m1 i ↔ map_first_key m2 i.
Proof.
  intros Hm. rewrite <-(map_first_key_fmap (λ _, ()) m1).
  rewrite <-(map_first_key_fmap (λ _, ()) m2). f_equiv. apply map_eq; intros j.
  specialize (Hm j). rewrite !lookup_fmap. unfold is_Some in *.
  destruct (m1 !! j), (m2 !! j); naive_solver.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_fold_insert {A B} (R : relation B) `{!PreOrder R}
    (f : K → A → B → B) (b : B) (i : K) (x : A) (m : M A) :
  (∀ j z, Proper (R ==> R) (f j z)) →
  (∀ j1 j2 z1 z2 y,
    j1 ≠ j2 → <[i:=x]> m !! j1 = Some z1 → <[i:=x]> m !! j2 = Some z2 →
    R (f j1 z1 (f j2 z2 y)) (f j2 z2 (f j1 z1 y))) →
  m !! i = None →
  R (map_fold f b (<[i:=x]> m)) (f i x (map_fold f b m)).
Proof.
  intros Hf_proper Hf Hi. rewrite !map_fold_foldr.
  change (f i x) with (uncurry f (i,x)). rewrite <-foldr_cons.
  assert (∀ kz, Proper (R ==> R) (uncurry f kz)) by (intros []; solve_proper).
  eapply (foldr_permutation R (uncurry f) b), map_to_list_insert; [|done].
  intros j1 [k1 y1] j2 [k2 y2] c Hj Hj1 Hj2. apply Hf.
  - intros ->.
    eapply Hj, NoDup_lookup; [apply (NoDup_fst_map_to_list (<[i:=x]> m))| | ].
    + by rewrite list_lookup_fmap, Hj1.
    + by rewrite list_lookup_fmap, Hj2.
  - by eapply elem_of_map_to_list, list_elem_of_lookup_2.
  - by eapply elem_of_map_to_list, list_elem_of_lookup_2.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_fold_insert_L {A B} (f : K → A → B → B) (b : B) (i : K) (x : A) (m : M A) :
  (∀ j1 j2 z1 z2 y,
    j1 ≠ j2 → <[i:=x]> m !! j1 = Some z1 → <[i:=x]> m !! j2 = Some z2 →
    f j1 z1 (f j2 z2 y) = f j2 z2 (f j1 z1 y)) →
  m !! i = None →
  map_fold f b (<[i:=x]> m) = f i x (map_fold f b m).
Proof. apply map_fold_insert; apply _. Qed.
(* stdpp/fin_maps.v *)
Lemma map_fold_delete {A B} (R : relation B) `{!PreOrder R}
    (f : K → A → B → B) (b : B) (i : K) (x : A) (m : M A) :
  (∀ j z, Proper (R ==> R) (f j z)) →
  (∀ j1 j2 z1 z2 y,
    j1 ≠ j2 → m !! j1 = Some z1 → m !! j2 = Some z2 →
    R (f j1 z1 (f j2 z2 y)) (f j2 z2 (f j1 z1 y))) →
  m !! i = Some x →
  R (map_fold f b m) (f i x (map_fold f b (delete i m))).
Proof.
  intros Hf_proper Hf Hi.
  rewrite <-map_fold_insert; [|done|done| |].
  - rewrite insert_delete_id; done.
  - intros j1 j2 z1 z2 y. rewrite insert_delete_id by done. auto.
  - rewrite lookup_delete_eq; done.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_fold_delete_L {A B} (f : K → A → B → B) (b : B) (i : K) (x : A) (m : M A) :
  (∀ j1 j2 z1 z2 y,
    j1 ≠ j2 → m !! j1 = Some z1 → m !! j2 = Some z2 →
    f j1 z1 (f j2 z2 y) = f j2 z2 (f j1 z1 y)) →
  m !! i = Some x →
  map_fold f b m = f i x (map_fold f b (delete i m)).
Proof. apply map_fold_delete; apply _. Qed.
(* stdpp/fin_maps.v *)
Lemma map_fold_comm_acc_strong {A B} (R : relation B) `{!PreOrder R}
    (f : K → A → B → B) (g : B → B) (x : B) (m : M A) :
  (∀ j z, Proper (R ==> R) (f j z)) →
  (∀ j z y, m !! j = Some z → R (f j z (g y)) (g (f j z y))) →
  R (map_fold f (g x) m) (g (map_fold f x m)).
Proof.
  intros ? Hg. induction m as [|i x' m ? Hfold IH] using map_fold_ind.
  { by rewrite !map_fold_empty. }
  rewrite !Hfold.
  rewrite <-Hg by (by rewrite lookup_insert_eq). f_equiv. apply IH.
  intros j z y Hj. apply Hg. rewrite lookup_insert_ne by naive_solver. done.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_fold_comm_acc {A B} (f : K → A → B → B) (g : B → B) (x : B) (m : M A) :
  (∀ j z y, f j z (g y) = g (f j z y)) →
  map_fold f (g x) m = g (map_fold f x m).
Proof. intros. apply (map_fold_comm_acc_strong _); [solve_proper|done..]. Qed.
(* stdpp/fin_maps.v *)
(* Not written using [Instance .. Proper] because it is ambigious to apply due
to the arbitrary [R]. *)
Lemma map_fold_proper {A B} (R : relation B) `{!PreOrder R}
    (f : K → A → B → B) (b1 b2 : B) (m : M A) :
  (∀ j z, Proper (R ==> R) (f j z)) →
  R b1 b2 →
  R (map_fold f b1 m) (map_fold f b2 m).
Proof.
  intros Hf Hb. induction m as [|i x m ?? IH] using map_first_key_ind.
  { by rewrite !map_fold_empty. }
  rewrite !map_fold_insert_first_key by done. by f_equiv.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_Forall_to_list m : map_Forall P m ↔ Forall (uncurry P) (map_to_list m).
Proof.
    rewrite Forall_forall. split.
    - intros Hforall [i x]. rewrite elem_of_map_to_list. by apply (Hforall i x).
    - intros Hforall i x. rewrite <-elem_of_map_to_list. by apply (Hforall (i,x)).
  Qed.
(* stdpp/fin_maps.v *)
Lemma map_Forall_empty : map_Forall P (∅ : M A).
Proof. intros i x. by rewrite lookup_empty. Qed.
(* stdpp/fin_maps.v *)
Lemma map_Forall_impl (Q : K → A → Prop) m :
    map_Forall P m → (∀ i x, P i x → Q i x) → map_Forall Q m.
Proof. intros Hm HQ i x Hi. apply HQ, Hm, Hi. Defined.
(* stdpp/fin_maps.v *)
Lemma map_Forall_insert_1_1 m i x : map_Forall P (<[i:=x]> m) → P i x.
Proof. intros Hm. by apply Hm; rewrite lookup_insert_eq. Qed.
(* stdpp/fin_maps.v *)
Lemma map_Forall_insert_1_2 m i x :
    m !! i = None → map_Forall P (<[i:=x]> m) → map_Forall P m.
Proof.
    intros ? Hm j y ?; apply Hm. by rewrite lookup_insert_ne by congruence.
  Qed.
(* stdpp/fin_maps.v *)
Lemma map_Forall_insert_2 m i x :
    P i x → map_Forall P m → map_Forall P (<[i:=x]> m).
Proof. intros ?? j y; rewrite lookup_insert_Some; naive_solver. Qed.
(* stdpp/fin_maps.v *)
Lemma map_Forall_insert m i x :
    m !! i = None → map_Forall P (<[i:=x]> m) ↔ P i x ∧ map_Forall P m.
Proof.
    naive_solver eauto using map_Forall_insert_1_1,
      map_Forall_insert_1_2, map_Forall_insert_2.
  Qed.
(* stdpp/fin_maps.v *)
Lemma map_Forall_singleton (i : K) (x : A) :
    map_Forall P ({[i:=x]} : M A) ↔ P i x.
Proof.
    unfold map_Forall. setoid_rewrite lookup_singleton_Some. naive_solver.
  Qed.
(* stdpp/fin_maps.v *)
Lemma map_Forall_delete m i : map_Forall P m → map_Forall P (delete i m).
Proof. intros Hm j x; rewrite lookup_delete_Some. naive_solver. Qed.
(* stdpp/fin_maps.v *)
Lemma map_Forall_lookup m :
    map_Forall P m ↔ ∀ i x, m !! i = Some x → P i x.
Proof. done. Qed.
(* stdpp/fin_maps.v *)
Lemma map_Forall_lookup_1 m i x :
    map_Forall P m → m !! i = Some x → P i x.
Proof. intros ?. by apply map_Forall_lookup. Qed.
(* stdpp/fin_maps.v *)
Lemma map_Forall_lookup_2 m :
    (∀ i x, m !! i = Some x → P i x) → map_Forall P m.
Proof. intros ?. by apply map_Forall_lookup. Qed.
(* stdpp/fin_maps.v *)
Lemma map_Forall_fmap {B} (f : B → A) (m : M B) :
    map_Forall P (f <$> m) ↔ map_Forall (λ k, (P k ∘ f)) m.
Proof.
    unfold map_Forall. setoid_rewrite lookup_fmap.
    setoid_rewrite fmap_Some. naive_solver.
  Qed.
(* stdpp/fin_maps.v *)
Lemma map_Forall_foldr_delete m js :
    map_Forall P m → map_Forall P (foldr delete m js).
Proof. induction js; eauto using map_Forall_delete. Qed.
(* stdpp/fin_maps.v *)
Lemma map_Forall_ind (Q : M A → Prop) :
    Q ∅ →
    (∀ m i x, m !! i = None → P i x → map_Forall P m → Q m → Q (<[i:=x]> m)) →
    ∀ m, map_Forall P m → Q m.
Proof.
    intros Hnil Hinsert m. induction m using map_ind; auto.
    rewrite map_Forall_insert by done; intros [??]; eauto.
  Qed.
(* stdpp/fin_maps.v *)
Instance map_Forall_dec m : Decision (map_Forall P m).
Proof.
    refine (cast_if (decide (Forall (uncurry P) (map_to_list m))));
      by rewrite map_Forall_to_list.
  Defined.
(* stdpp/fin_maps.v *)
Lemma map_not_Forall (m : M A) :
    ¬map_Forall P m ↔ ∃ i x, m !! i = Some x ∧ ¬P i x.
Proof.
    split; [|intros (i&x&?&?) Hm; specialize (Hm i x); tauto].
    rewrite map_Forall_to_list. intros Hm.
    apply (not_Forall_Exists _), Exists_exists in Hm.
    destruct Hm as ([i x]&?&?). exists i, x. by rewrite <-elem_of_map_to_list.
  Qed.
(* stdpp/fin_maps.v *)
Lemma map_Exists_to_list m : map_Exists P m ↔ Exists (uncurry P) (map_to_list m).
Proof.
    rewrite Exists_exists. split.
    - intros [? [? [? ?]]]. eexists (_, _). by rewrite elem_of_map_to_list.
    - intros [[??] [??]]. eexists _, _. by rewrite <-elem_of_map_to_list.
  Qed.
(* stdpp/fin_maps.v *)
Lemma map_Exists_empty : ¬ map_Exists P (∅ : M A).
Proof. intros [?[?[Hm ?]]]. by rewrite lookup_empty in Hm. Qed.
(* stdpp/fin_maps.v *)
Lemma map_Exists_impl (Q : K → A → Prop) m :
    map_Exists P m → (∀ i x, P i x → Q i x) → map_Exists Q m.
Proof. unfold map_Exists; naive_solver. Qed.
(* stdpp/fin_maps.v *)
Lemma map_Exists_insert_1 m i x :
    map_Exists P (<[i:=x]> m) → P i x ∨ map_Exists P m.
Proof. intros [j[y[?%lookup_insert_Some ?]]]. unfold map_Exists. naive_solver. Qed.
(* stdpp/fin_maps.v *)
Lemma map_Exists_insert_2_1 m i x : P i x → map_Exists P (<[i:=x]> m).
Proof. intros Hm. exists i, x. by rewrite lookup_insert_eq. Qed.
(* stdpp/fin_maps.v *)
Lemma map_Exists_insert_2_2 m i x :
    m !! i = None → map_Exists P m → map_Exists P (<[i:=x]> m).
Proof.
    intros Hm [j[y[??]]]. exists j, y. by rewrite lookup_insert_ne by congruence.
  Qed.
(* stdpp/fin_maps.v *)
Lemma map_Exists_insert m i x :
    m !! i = None → map_Exists P (<[i:=x]> m) ↔ P i x ∨ map_Exists P m.
Proof.
    naive_solver eauto using map_Exists_insert_1,
      map_Exists_insert_2_1, map_Exists_insert_2_2.
  Qed.
(* stdpp/fin_maps.v *)
Lemma map_Exists_singleton (i : K) (x : A) :
    map_Exists P ({[i:=x]} : M A) ↔ P i x.
Proof.
    unfold map_Exists. setoid_rewrite lookup_singleton_Some. naive_solver.
  Qed.
(* stdpp/fin_maps.v *)
Lemma map_Exists_delete m i : map_Exists P (delete i m) → map_Exists P m.
Proof.
    intros [j [y [Hm ?]]]. rewrite lookup_delete_Some in Hm.
    unfold map_Exists. naive_solver.
  Qed.
(* stdpp/fin_maps.v *)
Lemma map_Exists_lookup m :
    map_Exists P m ↔ ∃ i x, m !! i = Some x ∧ P i x.
Proof. done. Qed.
(* stdpp/fin_maps.v *)
Lemma map_Exists_lookup_1 m :
    map_Exists P m → ∃ i x, m !! i = Some x ∧ P i x.
Proof. by rewrite map_Exists_lookup. Qed.
(* stdpp/fin_maps.v *)
Lemma map_Exists_lookup_2 m i x :
    m !! i = Some x → P i x → map_Exists P m.
Proof. rewrite map_Exists_lookup. by eauto. Qed.
(* stdpp/fin_maps.v *)
Lemma map_Exists_foldr_delete m js :
    map_Exists P (foldr delete m js) → map_Exists P m.
Proof. induction js; eauto using map_Exists_delete. Qed.
(* stdpp/fin_maps.v *)
Lemma map_Exists_ind (Q : M A → Prop) :
    (∀ i x, P i x → Q {[i:=x]}) →
    (∀ m i x, m !! i = None → map_Exists P m → Q m → Q (<[i:=x]> m)) →
    ∀ m, map_Exists P m → Q m.
Proof.
    intros Hsingleton Hinsert m Hm. induction m as [|i x m Hi IH] using map_ind.
    { by destruct map_Exists_empty. }
    apply map_Exists_insert in Hm as [?|?]; [|by eauto..].
    clear IH. induction m as [|j y m Hj IH] using map_ind; [by eauto|].
    apply lookup_insert_None in Hi as [??].
    rewrite insert_insert_ne by done. apply Hinsert.
    - by apply lookup_insert_None.
    - apply map_Exists_insert; by eauto.
    - eauto.
  Qed.
(* stdpp/fin_maps.v *)
Lemma map_not_Exists (m : M A) :
    ¬map_Exists P m ↔ map_Forall (λ i x, ¬ P i x) m.
Proof. unfold map_Exists, map_Forall; naive_solver. Qed.
(* stdpp/fin_maps.v *)
Instance map_Exists_dec m : Decision (map_Exists P m).
Proof.
    refine (cast_if (decide (Exists (uncurry P) (map_to_list m))));
      by rewrite map_Exists_to_list.
  Defined.