phanerozoic/Coq-Stdpp huggingface dataset:
(* stdpp/fin_maps.v *)
Lemma insert_delete_subset {A} (m1 m2 : M A) i x :
  m1 !! i = None → <[i:=x]> m1 ⊂ m2 → m1 ⊂ delete i m2.
Proof.
  intros ? [Hm12 Hm21]; split; [eauto using insert_delete_subseteq|].
  contradict Hm21. apply delete_insert_subseteq; auto.
  eapply lookup_weaken, Hm12. by rewrite lookup_insert_eq.
Qed.
(* stdpp/fin_maps.v *)
Lemma insert_subset_inv {A} (m1 m2 : M A) i x :
  m1 !! i = None → <[i:=x]> m1 ⊂ m2 →
  ∃ m2', m2 = <[i:=x]> m2' ∧ m1 ⊂ m2' ∧ m2' !! i = None.
Proof.
  intros Hi Hm1m2. exists (delete i m2). split_and?.
  - rewrite insert_delete_id; [done|].
    eapply lookup_weaken, strict_include; eauto. by rewrite lookup_insert_eq.
  - eauto using insert_delete_subset.
  - by rewrite lookup_delete_eq.
Qed.
(* stdpp/fin_maps.v *)
(* ** Properties of the singleton maps *)
Lemma lookup_singleton {A} i j (x : A) :
  ({[i:=x]} : M A) !! j = if decide (i = j) then Some x else None.
Proof.
  unfold singletonM, map_singleton. by rewrite lookup_insert, lookup_empty.
Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_singleton_eq {A} i (x : A) : ({[i:=x]} : M A) !! i = Some x.
Proof. apply lookup_partial_alter_eq. Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_singleton_ne {A} i j (x : A) :
  i ≠ j → ({[i:=x]} : M A) !! j = None.
Proof. intros. by rewrite lookup_singleton, decide_False. Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_total_singleton `{!Inhabited A} i j (x : A) :
  ({[i:=x]} : M A) !!! j = if decide (i = j) then x else inhabitant.
Proof. rewrite lookup_total_alt, lookup_singleton. by case_decide. Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_total_singleton_eq `{!Inhabited A} i (x : A) :
  ({[i:=x]} : M A) !!! i = x.
Proof. by rewrite lookup_total_alt, lookup_singleton_eq. Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_total_singleton_ne `{!Inhabited A} i j (x : A) :
  i ≠ j → ({[i:=x]} : M A) !!! j = inhabitant.
Proof. intros. by rewrite lookup_total_alt, lookup_singleton_ne. Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_singleton_Some {A} i j (x y : A) :
  ({[i:=x]} : M A) !! j = Some y ↔ i = j ∧ x = y.
Proof.
  rewrite <-insert_empty,lookup_insert_Some, lookup_empty; intuition congruence.
Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_singleton_is_Some {A} i j (x : A) :
  is_Some (({[i:=x]} : M A) !! j) ↔ i = j.
Proof. unfold is_Some. setoid_rewrite lookup_singleton_Some. naive_solver. Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_singleton_None {A} i j (x : A) :
  ({[i:=x]} : M A) !! j = None ↔ i ≠ j.
Proof. by rewrite eq_None_not_Some, lookup_singleton_is_Some. Qed.
(* stdpp/fin_maps.v *)
Instance map_singleton_inj {A} : Inj2 (=) (=) (=) (singletonM (M:=M A)).
Proof.
  intros i1 x1 i2 x2 Heq%(f_equal (lookup i1)).
  rewrite !lookup_singleton in Heq. repeat case_decide; naive_solver.
Qed.
(* stdpp/fin_maps.v *)
(* TODO: Duplicates, remove one. *)
Lemma singleton_non_empty {A} i (x : A) : {[i:=x]} ≠@{M A} ∅.
Proof. apply insert_non_empty. Qed.
(* stdpp/fin_maps.v *)
Lemma map_non_empty_singleton {A} i (x : A) : {[i:=x]} ≠@{M A} ∅.
Proof. apply insert_non_empty. Qed.
(* stdpp/fin_maps.v *)
(* There is no nice statement for [partial_alter_singleton], so we omit that. *)
Lemma alter_singleton {A} f i j x :
  alter f i {[j:=x]} =@{M A} if decide (i = j) then {[i:=f x]} else {[j:=x]}.
Proof.
  unfold singletonM, map_singleton. by rewrite alter_insert, alter_empty.
Qed.
(* stdpp/fin_maps.v *)
Lemma alter_singleton_eq {A} f i x :
  alter f i {[i:=x]} =@{M A} {[i:=f x]}.
Proof. by rewrite alter_singleton, decide_True. Qed.
(* stdpp/fin_maps.v *)
Lemma alter_singleton_ne {A} f i j x :
  i ≠ j → alter f i {[j:=x]}=@{M A} {[j:=x]}.
Proof. intros. by rewrite alter_singleton, decide_False. Qed.
(* stdpp/fin_maps.v *)
Lemma delete_singleton {A} i j x :
  delete i {[j:=x]} =@{M A} if decide (i = j) then ∅ else {[j:=x]}.
Proof.
  unfold singletonM, map_singleton. by rewrite delete_insert, delete_empty.
Qed.
(* stdpp/fin_maps.v *)
Lemma delete_singleton_eq {A} i (x : A) : delete i {[i:=x]} =@{M A} ∅.
Proof. by rewrite delete_singleton, decide_True. Qed.
(* stdpp/fin_maps.v *)
Lemma delete_singleton_ne {A} i j (x : A) :
  i ≠ j → delete i {[j:=x]} =@{M A} {[j:=x]}.
Proof. intros. by rewrite delete_singleton, decide_False. Qed.
(* stdpp/fin_maps.v *)
Lemma insert_singleton {A} i j x y :
  <[i:=x]> {[j:=y]} =@{M A}
    if decide (i = j) then {[i:=x]} else <[j:=y]> {[i:=x]}.
Proof.
  unfold singletonM, map_singleton. by rewrite insert_insert, !insert_empty.
Qed.
(* stdpp/fin_maps.v *)
Lemma insert_singleton_eq {A} i (x y : A) : <[i:=x]> {[i:=y]} =@{M A} {[i:=x]}.
Proof. by rewrite insert_singleton, decide_True. Qed.
(* stdpp/fin_maps.v *)
Lemma insert_singleton_ne {A} i j (x y : A) :
  i ≠ j → <[i:=x]> {[j:=y]} =@{M A} <[j:=y]> {[i:=x]}.
Proof. intros. by rewrite insert_singleton, decide_False. Qed.
(* stdpp/fin_maps.v *)
Lemma map_singleton_subseteq_l {A} i (x : A) (m : M A) :
  {[i:=x]} ⊆ m ↔ m !! i = Some x.
Proof.
  rewrite map_subseteq_spec. setoid_rewrite lookup_singleton_Some. naive_solver.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_singleton_subseteq {A} i j (x y : A) :
  {[i:=x]} ⊆@{M A} {[j:=y]} ↔ i = j ∧ x = y.
Proof.
  rewrite map_subseteq_spec. setoid_rewrite lookup_singleton_Some. naive_solver.
Qed.
(* stdpp/fin_maps.v *)
(* ** Properties of the map operations *)
Lemma lookup_total_fmap `{!Inhabited A, !Inhabited B} (f : A → B) (m : M A) i :
  (f <$> m) !!! i =
    match m !! i with Some _ => f (m !!! i) | None => inhabitant end.
Proof. rewrite !lookup_total_alt, lookup_fmap. by destruct (m !! i). Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_total_fmap' `{!Inhabited A, !Inhabited B}
    (f : A → B) (m : M A) i :
  is_Some (m !! i) → (f <$> m) !!! i = f (m !!! i).
Proof. intros [x Hi]. by rewrite lookup_total_fmap, Hi. Qed.
(* stdpp/fin_maps.v *)
Instance map_fmap_inj {A B} (f : A → B) :
  Inj (=) (=) f → Inj (=@{M A}) (=@{M B}) (fmap f).
Proof.
  intros ? m1 m2 Hm. apply map_eq; intros i.
  apply (inj (fmap (M:=option) f)). by rewrite <-!lookup_fmap, Hm.
Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_fmap_Some {A B} (f : A → B) (m : M A) i y :
  (f <$> m) !! i = Some y ↔ ∃ x, f x = y ∧ m !! i = Some x.
Proof. rewrite lookup_fmap, fmap_Some. naive_solver. Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_omap_Some {A B} (f : A → option B) (m : M A) i y :
  omap f m !! i = Some y ↔ ∃ x, f x = Some y ∧ m !! i = Some x.
Proof. rewrite lookup_omap, bind_Some. naive_solver. Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_omap_id_Some {A} (m : M (option A)) i x :
  omap id m !! i = Some x ↔ m !! i = Some (Some x).
Proof. rewrite lookup_omap_Some. naive_solver. Qed.
(* stdpp/fin_maps.v *)
Lemma fmap_empty {A B} (f : A → B) : f <$> ∅ =@{M B} ∅.
Proof. apply map_empty; intros i. by rewrite lookup_fmap, lookup_empty. Qed.
(* stdpp/fin_maps.v *)
Lemma omap_empty {A B} (f : A → option B) : omap f ∅ =@{M B} ∅.
Proof. apply map_empty; intros i. by rewrite lookup_omap, lookup_empty. Qed.
(* stdpp/fin_maps.v *)
Lemma fmap_empty_iff {A B} (f : A → B) m : f <$> m =@{M B} ∅ ↔ m = ∅.
Proof.
  split; [|intros ->; by rewrite fmap_empty].
  intros Hm. apply map_eq; intros i. generalize (f_equal (lookup i) Hm).
  by rewrite lookup_fmap, !lookup_empty, fmap_None.
Qed.
(* stdpp/fin_maps.v *)
Lemma fmap_empty_inv {A B} (f : A → B) m : f <$> m =@{M B} ∅ → m = ∅.
Proof. apply fmap_empty_iff. Qed.
(* stdpp/fin_maps.v *)
Lemma fmap_alter {A B} (f : A → B) (g : A → A) (h : B → B) (m : M A) i :
  (∀ x, m !! i = Some x → f (g x) = h (f x)) →
  f <$> alter g i m = alter h i (f <$> m).
Proof.
  intros Hlookup. apply map_eq. intros j.
  rewrite lookup_fmap, !lookup_alter, !lookup_fmap.
  destruct (decide (i = j)) as [<-|Hij]; [|done].
  destruct (m !! i) as [x |]; f_equal/=; eauto.
Qed.
(* stdpp/fin_maps.v *)
Lemma fmap_delete {A B} (f: A → B) (m : M A) i :
  f <$> delete i m = delete i (f <$> m).
Proof.
  apply map_eq; intros i'. rewrite lookup_delete, !lookup_fmap, lookup_delete.
  repeat case_decide; naive_solver.
Qed.
(* stdpp/fin_maps.v *)
Lemma omap_delete {A B} (f: A → option B) (m : M A) i :
  omap f (delete i m) = delete i (omap f m).
Proof.
  apply map_eq; intros i'. rewrite lookup_delete, !lookup_omap, lookup_delete.
  repeat case_decide; naive_solver.
Qed.
(* stdpp/fin_maps.v *)
Lemma fmap_insert {A B} (f : A → B) (m : M A) i x :
  f <$> <[i:=x]> m = <[i:=f x]> (f <$> m).
Proof.
  apply map_eq; intros i'. rewrite !lookup_insert, !lookup_fmap, !lookup_insert.
  repeat case_decide; naive_solver.
Qed.
(* stdpp/fin_maps.v *)
Lemma fmap_insert_inv {A B} (f : A → B) (m1 : M A) (m2 : M B) i y :
  m2 !! i = None →
  f <$> m1 = <[i:=y]> m2 →
  ∃ x m1', y = f x ∧ m1' !! i = None ∧ m1 = <[i:=x]> m1' ∧ m2 = f <$> m1'.
Proof.
  intros ? Hm. pose proof (f_equal (.!! i) Hm) as Hmi.
  rewrite lookup_fmap, lookup_insert_eq, fmap_Some in Hmi.
  destruct Hmi as (x & ? & ->). exists x, (delete i m1). split; [done|].
  split; [by rewrite lookup_delete_eq|].
  split; [by rewrite insert_delete_id|].
  by rewrite fmap_delete, Hm, delete_insert_id by done.
Qed.
(* stdpp/fin_maps.v *)
Lemma omap_insert {A B} (f : A → option B) (m : M A) i x :
  omap f (<[i:=x]> m) =
    (match f x with Some y => <[i:=y]> | None => delete i end) (omap f m).
Proof.
  intros; apply map_eq; intros i'. destruct (f x) eqn:?;
    rewrite !lookup_omap, !lookup_insert, ?lookup_delete, lookup_omap;
    repeat case_decide; naive_solver.
Qed.
(* stdpp/fin_maps.v *)
Lemma omap_insert_Some {A B} (f : A → option B) (m : M A) i x y :
  f x = Some y → omap f (<[i:=x]> m) = <[i:=y]>(omap f m).
Proof. intros Hx. by rewrite omap_insert, Hx. Qed.
(* stdpp/fin_maps.v *)
Lemma omap_insert_None {A B} (f : A → option B) (m : M A) i x :
  f x = None → omap f (<[i:=x]> m) = delete i (omap f m).
Proof. intros Hx. by rewrite omap_insert, Hx. Qed.
(* stdpp/fin_maps.v *)
Lemma map_fmap_singleton {A B} (f : A → B) i x :
  f <$> {[i:=x]} =@{M B} {[i:=f x]}.
Proof.
  by unfold singletonM, map_singleton; rewrite fmap_insert, fmap_empty.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_fmap_singleton_inv {A B} (f : A → B) (m : M A) i y :
  f <$> m = {[i:=y]} → ∃ x, y = f x ∧ m = {[i:=x]}.
Proof.
  intros (x & m' & -> & ? & -> & Hm')%fmap_insert_inv; [|by apply lookup_empty].
  apply symmetry in Hm' as ->%fmap_empty_inv. by exists x.
Qed.
(* stdpp/fin_maps.v *)
Lemma omap_singleton {A B} (f : A → option B) i x :
  omap f {[i:=x]} =@{M B} match f x with Some y => {[i:=y]} | None => ∅ end.
Proof.
  rewrite <-insert_empty, omap_insert, omap_empty. destruct (f x) as [y|]; simpl.
  - by rewrite insert_empty.
  - by rewrite delete_empty.
Qed.
(* stdpp/fin_maps.v *)
Lemma omap_singleton_Some {A B} (f : A → option B) i x y :
  f x = Some y → omap f {[i:=x]} =@{M B} {[i:=y]}.
Proof. intros Hx. by rewrite omap_singleton, Hx. Qed.
(* stdpp/fin_maps.v *)
Lemma omap_singleton_None {A B} (f : A → option B) i x :
  f x = None → omap f {[i:=x]} =@{M B} ∅.
Proof. intros Hx. by rewrite omap_singleton, Hx. Qed.
(* stdpp/fin_maps.v *)
Lemma map_fmap_id {A} (m : M A) : id <$> m = m.
Proof. apply map_eq; intros i; by rewrite lookup_fmap, option_fmap_id. Qed.
(* stdpp/fin_maps.v *)
Lemma map_fmap_compose {A B C} (f : A → B) (g : B → C) (m : M A) :
  g ∘ f <$> m = g <$> (f <$> m).
Proof. apply map_eq; intros i; by rewrite !lookup_fmap,option_fmap_compose. Qed.
(* stdpp/fin_maps.v *)
Lemma map_fmap_ext {A 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; apply map_eq; intros i; rewrite !lookup_fmap.
  by destruct (m !! i) eqn:?; simpl; erewrite ?Hi by eauto.
Qed.
(* stdpp/fin_maps.v *)
Lemma omap_ext {A B} (f1 f2 : A → option B) (m : M A) :
  (∀ i x, m !! i = Some x → f1 x = f2 x) → omap f1 m = omap f2 m.
Proof.
  intros Hi; apply map_eq; intros i; rewrite !lookup_omap.
  by destruct (m !! i) eqn:?; simpl; erewrite ?Hi by eauto.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_fmap_omap {A B C} (f : A → option B) (g : B → C) (m : M A) :
  g <$> omap f m = omap (λ x, g <$> f x) m.
Proof.
  apply map_eq. intros i.
  rewrite !lookup_fmap, !lookup_omap. destruct (m !! i); done.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_fmap_alt {A B} (f : A → B) (m : M A) :
  f <$> m = omap (λ x, Some (f x)) m.
Proof.
  apply map_eq. intros i.
  rewrite lookup_fmap, lookup_omap. destruct (m !! i); done.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_fmap_mono {A B} (f : A → B) (m1 m2 : M A) :
  m1 ⊆ m2 → f <$> m1 ⊆ f <$> m2.
Proof.
  rewrite !map_subseteq_spec; intros Hm i x.
  rewrite !lookup_fmap, !fmap_Some. naive_solver.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_fmap_strict_mono {A B} (f : A → B) (m1 m2 : M A) :
  m1 ⊂ m2 → f <$> m1 ⊂ f <$> m2.
Proof.
  rewrite !map_subset_alt.
  intros [? (j&?&?)]; split; auto using map_fmap_mono.
  exists j. by rewrite !lookup_fmap, fmap_None, fmap_is_Some.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_omap_mono {A B} (f : A → option B) (m1 m2 : M A) :
  m1 ⊆ m2 → omap f m1 ⊆ omap f m2.
Proof.
  rewrite !map_subseteq_spec; intros Hm i x.
  rewrite !lookup_omap, !bind_Some. naive_solver.
Qed.
(* stdpp/fin_maps.v *)
(* ** Properties of conversion to lists *)
Lemma elem_of_map_to_list' {A} (m : M A) ix :
  ix ∈ map_to_list m ↔ m !! ix.1 = Some (ix.2).
Proof. destruct ix as [i x]. apply elem_of_map_to_list. Qed.
(* stdpp/fin_maps.v *)
Lemma map_to_list_unique {A} (m : M A) i x y :
  (i,x) ∈ map_to_list m → (i,y) ∈ map_to_list m → x = y.
Proof. rewrite !elem_of_map_to_list. congruence. Qed.
(* stdpp/fin_maps.v *)
Lemma NoDup_fst_map_to_list {A} (m : M A) : NoDup ((map_to_list m).*1).
Proof. eauto using NoDup_fmap_fst, map_to_list_unique, NoDup_map_to_list. Qed.
(* stdpp/fin_maps.v *)
Lemma elem_of_list_to_map_1' {A} (l : list (K * A)) i x :
  (∀ y, (i,y) ∈ l → x = y) → (i,x) ∈ l → (list_to_map l : M A) !! i = Some x.
Proof.
  induction l as [|[j y] l IH]; csimpl; [by rewrite elem_of_nil|].
  setoid_rewrite elem_of_cons.
  intros Hdup [?|?]; simplify_eq; [by rewrite lookup_insert_eq|].
  destruct (decide (i = j)) as [->|].
  - rewrite lookup_insert_eq; f_equal; eauto using eq_sym.
  - rewrite lookup_insert_ne by done; eauto.
Qed.
(* stdpp/fin_maps.v *)
Lemma elem_of_list_to_map_1 {A} (l : list (K * A)) i x :
  NoDup (l.*1) → (i,x) ∈ l → (list_to_map l : M A) !! i = Some x.
Proof.
  intros ? Hx; apply elem_of_list_to_map_1'; eauto using NoDup_fmap_fst.
  intros y; revert Hx. rewrite !list_elem_of_lookup; intros [i' Hi'] [j' Hj'].
  cut (i' = j'); [naive_solver|]. apply NoDup_lookup with (l.*1) i;
    by rewrite ?list_lookup_fmap, ?Hi', ?Hj'.
Qed.
(* stdpp/fin_maps.v *)
Lemma elem_of_list_to_map_2 {A} (l : list (K * A)) i x :
  (list_to_map l : M A) !! i = Some x → (i,x) ∈ l.
Proof.
  induction l as [|[j y] l IH]; simpl; [by rewrite lookup_empty|].
  rewrite elem_of_cons. destruct (decide (i = j)) as [->|];
    rewrite ?lookup_insert_eq, ?lookup_insert_ne; intuition congruence.
Qed.
(* stdpp/fin_maps.v *)
Lemma elem_of_list_to_map' {A} (l : list (K * A)) i x :
  (∀ x', (i,x) ∈ l → (i,x') ∈ l → x = x') →
  (i,x) ∈ l ↔ (list_to_map l : M A) !! i = Some x.
Proof. split; auto using elem_of_list_to_map_1', elem_of_list_to_map_2. Qed.
(* stdpp/fin_maps.v *)
Lemma elem_of_list_to_map {A} (l : list (K * A)) i x :
  NoDup (l.*1) → (i,x) ∈ l ↔ (list_to_map l : M A) !! i = Some x.
Proof. split; auto using elem_of_list_to_map_1, elem_of_list_to_map_2. Qed.
(* stdpp/fin_maps.v *)
Lemma not_elem_of_list_to_map_1 {A} (l : list (K * A)) i :
  i ∉ l.*1 → (list_to_map l : M A) !! i = None.
Proof.
  rewrite list_elem_of_fmap, eq_None_not_Some. intros Hi [x ?]; destruct Hi.
  exists (i,x); simpl; auto using elem_of_list_to_map_2.
Qed.
(* stdpp/fin_maps.v *)
Lemma not_elem_of_list_to_map_2 {A} (l : list (K * A)) i :
  (list_to_map l : M A) !! i = None → i ∉ l.*1.
Proof.
  induction l as [|[j y] l IH]; csimpl; [rewrite elem_of_nil; tauto|].
  rewrite elem_of_cons, lookup_insert. case_decide; naive_solver.
Qed.
(* stdpp/fin_maps.v *)
Lemma not_elem_of_list_to_map {A} (l : list (K * A)) i :
  i ∉ l.*1 ↔ (list_to_map l : M A) !! i = None.
Proof. red; auto using not_elem_of_list_to_map_1,not_elem_of_list_to_map_2. Qed.
(* stdpp/fin_maps.v *)
Lemma list_to_map_proper {A} (l1 l2 : list (K * A)) :
  NoDup (l1.*1) → l1 ≡ₚ l2 → (list_to_map l1 : M A) = list_to_map l2.
Proof.
  intros ? Hperm. apply map_eq. intros i. apply option_eq. intros x.
  by rewrite <-!elem_of_list_to_map; rewrite <-?Hperm.
Qed.
(* stdpp/fin_maps.v *)
Lemma list_to_map_inj {A} (l1 l2 : list (K * A)) :
  NoDup (l1.*1) → NoDup (l2.*1) →
  (list_to_map l1 : M A) = list_to_map l2 → l1 ≡ₚ l2.
Proof.
  intros ?? Hl1l2. apply NoDup_Permutation; [by eauto using NoDup_fmap_1..|].
  intros [i x]. by rewrite !elem_of_list_to_map, Hl1l2.
Qed.
(* stdpp/fin_maps.v *)
Lemma list_to_map_to_list {A} (m : M A) : list_to_map (map_to_list m) = m.
Proof.
  apply map_eq. intros i. apply option_eq. intros x.
  by rewrite <-elem_of_list_to_map, elem_of_map_to_list
    by auto using NoDup_fst_map_to_list.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_to_list_to_map {A} (l : list (K * A)) :
  NoDup (l.*1) → map_to_list (list_to_map l) ≡ₚ l.
Proof. auto using list_to_map_inj, NoDup_fst_map_to_list, list_to_map_to_list. Qed.
(* stdpp/fin_maps.v *)
Lemma map_to_list_inj {A} (m1 m2 : M A) :
  map_to_list m1 ≡ₚ map_to_list m2 → m1 = m2.
Proof.
  intros. rewrite <-(list_to_map_to_list m1), <-(list_to_map_to_list m2).
  auto using list_to_map_proper, NoDup_fst_map_to_list.
Qed.
(* stdpp/fin_maps.v *)
Lemma list_to_map_flip {A} (m1 : M A) l2 :
  map_to_list m1 ≡ₚ l2 → m1 = list_to_map l2.
Proof.
  intros. rewrite <-(list_to_map_to_list m1).
  auto using list_to_map_proper, NoDup_fst_map_to_list.
Qed.
(* stdpp/fin_maps.v *)
Lemma list_to_map_nil {A} : list_to_map [] =@{M A} ∅.
Proof. done. Qed.
(* stdpp/fin_maps.v *)
Lemma list_to_map_cons {A} (l : list (K * A)) i x :
  list_to_map ((i, x) :: l) =@{M A} <[i:=x]>(list_to_map l).
Proof. done. Qed.
(* stdpp/fin_maps.v *)
Lemma list_to_map_snoc {A} (l : list (K * A)) i x :
  i ∉ l.*1 → list_to_map (l ++ [(i, x)]) =@{M A} <[i:=x]>(list_to_map l).
Proof.
  induction l as [|[k y] l IH]; [done|]. csimpl.
  intros [Hneq Hni]%not_elem_of_cons.
  by rewrite (IH Hni), insert_insert_ne by done.
Qed.
(* stdpp/fin_maps.v *)
Lemma list_to_map_fmap {A B} (f : A → B) l :
  list_to_map (prod_map id f <$> l) = f <$> (list_to_map l : M A).
Proof.
  induction l as [|[i x] l IH]; csimpl; rewrite ?fmap_empty; auto.
  rewrite <-list_to_map_cons; simpl. by rewrite IH, <-fmap_insert.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_to_list_empty {A} : map_to_list ∅ = @nil (K * A).
Proof.
  apply elem_of_nil_inv. intros [i x].
  rewrite elem_of_map_to_list. apply lookup_empty_Some.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_to_list_insert {A} (m : M A) i x :
  m !! i = None → map_to_list (<[i:=x]> m) ≡ₚ (i,x) :: map_to_list m.
Proof.
  intros. apply list_to_map_inj; csimpl.
  - apply NoDup_fst_map_to_list.
  - constructor; [|by auto using NoDup_fst_map_to_list].
    rewrite list_elem_of_fmap. intros [[??] [? Hlookup]]; subst; simpl in *.
    rewrite elem_of_map_to_list in Hlookup. congruence.
  - by rewrite !list_to_map_to_list.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_to_list_singleton {A} i (x : A) :
  map_to_list ({[i:=x]} : M A) = [(i,x)].
Proof.
  apply Permutation_singleton_r. unfold singletonM, map_singleton.
  by rewrite map_to_list_insert, map_to_list_empty by eauto using lookup_empty.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_to_list_delete {A} (m : M A) i x :
  m !! i = Some x → (i,x) :: map_to_list (delete i m) ≡ₚ map_to_list m.
Proof.
  intros. rewrite <-map_to_list_insert by (by rewrite lookup_delete_eq).
  by rewrite insert_delete_id.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_to_list_submseteq {A} (m1 m2 : M A) :
  m1 ⊆ m2 → map_to_list m1 ⊆+ map_to_list m2.
Proof.
  intros; apply NoDup_submseteq; [by eauto using NoDup_map_to_list|].
  intros [i x]. rewrite !elem_of_map_to_list; eauto using lookup_weaken.
Qed.
(* stdpp/fin_maps.v *)
(* FIXME (improve structure): Remove in favor of [map_to_list_fmap] (proved
below), which gives [=] instead of [≡ₚ]. Moving requires a bunch of reordering
in this file. *)
Lemma map_to_list_fmap_weak {A B} (f : A → B) (m : M A) :
  map_to_list (f <$> m) ≡ₚ prod_map id f <$> map_to_list m.
Proof.
  assert (NoDup ((prod_map id f <$> map_to_list m).*1)).
  { erewrite <-list_fmap_compose, (list_fmap_ext _ fst) by done.
    apply NoDup_fst_map_to_list. }
  rewrite <-(list_to_map_to_list m) at 1.
  by rewrite <-list_to_map_fmap, map_to_list_to_map.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_to_list_empty_iff {A} (m : M A) : map_to_list m = [] ↔ m = ∅.
Proof.
  split.
  - rewrite <-Permutation_nil_r, <-map_to_list_empty. apply map_to_list_inj.
  - intros ->. apply map_to_list_empty.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_to_list_insert_inv {A} (m : M A) l i x :
  map_to_list m ≡ₚ (i,x) :: l → m = <[i:=x]>(list_to_map l).
Proof.
  intros Hperm. apply map_to_list_inj.
  assert (i ∉ l.*1 ∧ NoDup (l.*1)) as [].
  { rewrite <-NoDup_cons. change (NoDup (((i,x)::l).*1)). rewrite <-Hperm.
    auto using NoDup_fst_map_to_list. }
  rewrite Hperm, map_to_list_insert, map_to_list_to_map;
    auto using not_elem_of_list_to_map_1.
Qed.
(* stdpp/fin_maps.v *)
Lemma length_map_to_list {A} (m : M A) :
  length (map_to_list m) = size m.
Proof.
  apply (map_fold_weak_ind (λ n m, length (map_to_list m) = n)); clear m.
  { by rewrite map_to_list_empty. }
  intros i x m n ? IH. by rewrite map_to_list_insert, <-IH by done.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_choose {A} (m : M A) : m ≠ ∅ → ∃ i x, m !! i = Some x.
Proof.
  rewrite <-map_to_list_empty_iff.
  intros Hemp. destruct (map_to_list m) as [|[i x] l] eqn:Hm; [done|].
  exists i, x. rewrite <-elem_of_map_to_list, Hm. by left.
Qed.
(* stdpp/fin_maps.v *)
Instance map_eq_dec_empty {A} (m : M A) : Decision (m = ∅) | 20.
Proof.
  refine (cast_if (decide (map_to_list m = [])));
    by rewrite <-?map_to_list_empty_iff.
Defined.
(* stdpp/fin_maps.v *)
Lemma map_choose_or_empty {A} (m : M A) : (∃ i x, m !! i = Some x) ∨ m = ∅.
Proof. destruct (decide (m = ∅)); [right|left]; auto using map_choose. Qed.
(* stdpp/fin_maps.v *)
(* Properties of the imap function *)
Lemma map_lookup_imap {A B} (f : K → A → option B) (m : M A) i :
  map_imap f m !! i = m !! i ≫= f i.
Proof.
  unfold map_imap.
  apply (map_fold_weak_ind (λ r m, r !! i = m !! i ≫= f i)); clear m.
  { by rewrite !lookup_empty. }
  intros j y m m' Hj Hi. rewrite lookup_insert.
  destruct (decide (j = i)) as [->|]; simpl.
  - destruct (f i y).
    + by rewrite lookup_insert_eq.
    + by rewrite Hi, Hj.
  - destruct (f j y); by rewrite ?lookup_insert_ne by done.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_imap_Some {A} (m : M A) : map_imap (λ _, Some) m = m.
Proof.
  apply map_eq. intros i. rewrite map_lookup_imap. by destruct (m !! i).
Qed.
(* stdpp/fin_maps.v *)
Lemma map_imap_insert {A B} (f : K → A → option B) i x (m : M A) :
  map_imap f (<[i:=x]> m) =
    (match f i x with Some y => <[i:=y]> | None => delete i end) (map_imap f m).
Proof.
  apply map_eq. intros k. rewrite map_lookup_imap, lookup_insert.
  destruct (f i x) as [y|] eqn:Hw;
    rewrite ?lookup_insert, ?lookup_delete, ?map_lookup_imap;
    repeat case_decide; naive_solver.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_imap_insert_Some {A B} (f : K → A → option B) i x (m : M A) y :
  f i x = Some y → map_imap f (<[i:=x]> m) = <[i:=y]> (map_imap f m).
Proof. intros Hi. by rewrite map_imap_insert, Hi. Qed.
(* stdpp/fin_maps.v *)
Lemma map_imap_insert_None {A B} (f : K → A → option B) i x (m : M A) :
  f i x = None → map_imap f (<[i:=x]> m) = delete i (map_imap f m).
Proof. intros Hi. by rewrite map_imap_insert, Hi. Qed.
(* stdpp/fin_maps.v *)
Lemma map_imap_delete {A B} (f : K → A → option B) (m : M A) (i : K) :
  map_imap f (delete i m) = delete i (map_imap f m).
Proof.
  apply map_eq. intros k.
  rewrite map_lookup_imap, !lookup_delete, map_lookup_imap.
  repeat case_decide; naive_solver.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_imap_ext {A1 A2 B} (f1 : K → A1 → option B)
    (f2 : K → A2 → option B) (m1 : M A1) (m2 : M A2) :
  (∀ k, f1 k <$> (m1 !! k) = f2 k <$> (m2 !! k)) →
  map_imap f1 m1 = map_imap f2 m2.
Proof.
  intros HExt. apply map_eq. intros i. rewrite !map_lookup_imap.
  specialize (HExt i). destruct (m1 !! i), (m2 !! i); naive_solver.
Qed.
(* stdpp/fin_maps.v *)
Lemma map_imap_compose {A1 A2 B} (f1 : K → A1 → option B)
    (f2 : K → A2 → option A1) (m : M A2) :
  map_imap f1 (map_imap f2 m) = map_imap (λ k x, f2 k x ≫= f1 k) m.
Proof.
  apply map_eq. intros i. rewrite !map_lookup_imap. by destruct (m !! i).
Qed.