phanerozoic/Coq-Stdpp huggingface dataset:
(* stdpp/fin_maps.v *)
Lemma map_subset_alt {A} (m1 m2 : M A) :
  m1 ⊂ m2 ↔ m1 ⊆ m2 ∧ ∃ i, m1 !! i = None ∧ is_Some (m2 !! i).
Proof.
  rewrite strict_spec_alt. split.
  - intros [? Heq]; split; [done|].
    destruct (decide (Exists (λ ix, m1 !! ix.1 = None) (map_to_list m2)))
      as [[[i x] [?%elem_of_map_to_list ?]]%Exists_exists
         |Hm%(not_Exists_Forall _)]; [eauto|].
    destruct Heq; apply (anti_symm (⊆)), map_subseteq_spec; [done|intros i x Hi].
    assert (is_Some (m1 !! i)) as [x' ?].
    { by apply not_eq_None_Some,
        (proj1 (Forall_forall _ _) Hm (i,x)), elem_of_map_to_list. }
    by rewrite <-(lookup_weaken_inv m1 m2 i x' x).
  - intros [? (i&?&x&?)]; split; [done|]. congruence.
Qed.
(* stdpp/fin_maps.v *)
(* ** Properties of the [partial_alter] operation *)
Lemma lookup_partial_alter {A} f (m : M A) i j :
  partial_alter f i m !! j = if decide (i = j) then f (m !! i) else m !! j.
Proof.
  case_decide; subst; eauto using lookup_partial_alter_eq, lookup_partial_alter_ne.
Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_total_partial_alter `{!Inhabited A}
    (f : option A → option A) (m : M A) i j :
  partial_alter f i m !!! j =
    if decide (i = j) then default inhabitant (f (m !! i)) else m !!! j.
Proof.
  rewrite lookup_total_alt, lookup_partial_alter. case_decide; naive_solver.
Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_total_partial_alter_eq `{!Inhabited A}
    (f : option A → option A) (m : M A) i :
  partial_alter f i m !!! i = default inhabitant (f (m !! i)).
Proof. by rewrite lookup_total_partial_alter, decide_True. Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_total_partial_alter_ne `{!Inhabited A}
    (f : option A → option A) (m : M A) i j :
  i ≠ j → partial_alter f i m !!! j = m !!! j.
Proof. intros. by rewrite lookup_total_partial_alter, decide_False. Qed.
(* stdpp/fin_maps.v *)
Lemma partial_alter_ext {A} (f g : option A → option A) (m : M A) i :
  (∀ x, m !! i = x → f x = g x) → partial_alter f i m = partial_alter g i m.
Proof.
  intros. apply map_eq; intros j. rewrite !lookup_partial_alter.
  repeat case_decide; naive_solver.
Qed.
(* stdpp/fin_maps.v *)
Lemma partial_alter_id {A} f (m : M A) i :
  f (m !! i) = m !! i → partial_alter f i m = m.
Proof.
  intros. apply map_eq. intros ii. rewrite !lookup_partial_alter.
  repeat case_decide; naive_solver.
Qed.
(* stdpp/fin_maps.v *)
Lemma partial_alter_self {A} (m : M A) i : partial_alter (λ _, m !! i) i m = m.
Proof. by apply partial_alter_id. Qed.
(* stdpp/fin_maps.v *)
Lemma partial_alter_partial_alter {A} f g (m : M A) i j :
  partial_alter f i (partial_alter g j m) =
    if decide (i = j) then partial_alter (f ∘ g) i m
    else partial_alter g j (partial_alter f i m).
Proof.
  intros. apply map_eq; intros jj.
  case_decide; rewrite !lookup_partial_alter; repeat case_decide; naive_solver.
Qed.
(* stdpp/fin_maps.v *)
Lemma partial_alter_partial_alter_eq {A} f g (m : M A) i :
  partial_alter f i (partial_alter g i m) = partial_alter (f ∘ g) i m.
Proof. intros. by rewrite partial_alter_partial_alter, decide_True. Qed.
(* stdpp/fin_maps.v *)
Lemma partial_alter_partial_alter_ne {A} f g (m : M A) i j :
  i ≠ j →
  partial_alter f i (partial_alter g j m) =
    partial_alter g j (partial_alter f i m).
Proof. intros. by rewrite partial_alter_partial_alter, decide_False. Qed.
(* stdpp/fin_maps.v *)
Lemma partial_alter_alter {A} f g (m : M A) i j :
  partial_alter f i (alter g j m) =
    if decide (i = j) then partial_alter (f ∘ fmap g) i m
    else alter g j (partial_alter f i m).
Proof. apply partial_alter_partial_alter. Qed.
(* stdpp/fin_maps.v *)
Lemma partial_alter_alter_eq {A} f g (m : M A) i :
  partial_alter f i (alter g i m) = partial_alter (f ∘ fmap g) i m.
Proof. intros. by rewrite partial_alter_alter, decide_True. Qed.
(* stdpp/fin_maps.v *)
Lemma partial_alter_alter_ne {A} f g (m : M A) i j :
  i ≠ j → partial_alter f i (alter g j m) = alter g j (partial_alter f i m).
Proof. intros. by rewrite partial_alter_alter, decide_False. Qed.
(* stdpp/fin_maps.v *)
Lemma partial_alter_delete {A} f (m : M A) i j :
  partial_alter f i (delete j m) =
    if decide (i = j) then partial_alter (λ _, f None) i m
    else delete j (partial_alter f i m).
Proof. apply partial_alter_partial_alter. Qed.
(* stdpp/fin_maps.v *)
Lemma partial_alter_delete_eq {A} f (m : M A) i :
  partial_alter f i (delete i m) = partial_alter (λ _, f None) i m.
Proof. intros. by rewrite partial_alter_delete, decide_True. Qed.
(* stdpp/fin_maps.v *)
Lemma partial_alter_delete_ne {A} f (m : M A) i j :
  i ≠ j → partial_alter f i (delete j m) = delete j (partial_alter f i m).
Proof. intros. by rewrite partial_alter_delete, decide_False. Qed.
(* stdpp/fin_maps.v *)
Lemma partial_alter_insert {A} f (m : M A) i j x :
  partial_alter f i (<[j:=x]> m) =
    if decide (i = j) then partial_alter (λ _, f (Some x)) i m
    else <[j:=x]> (partial_alter f i m).
Proof. apply partial_alter_partial_alter. Qed.
(* stdpp/fin_maps.v *)
Lemma partial_alter_insert_eq {A} f (m : M A) i x :
  partial_alter f i (<[i:=x]> m) = partial_alter (λ _, f (Some x)) i m.
Proof. intros. by rewrite partial_alter_insert, decide_True. Qed.
(* stdpp/fin_maps.v *)
Lemma partial_alter_insert_ne {A} f (m : M A) i j x :
  i ≠ j →
  partial_alter f i (<[j:=x]> m) = <[j:=x]> (partial_alter f i m).
Proof. intros. by rewrite partial_alter_insert, decide_False. Qed.
(* stdpp/fin_maps.v *)
Lemma partial_alter_subseteq {A} f (m : M A) i :
  m !! i = None → m ⊆ partial_alter f i m.
Proof.
  rewrite map_subseteq_spec. intros Hi j x Hj. rewrite !lookup_partial_alter.
  repeat case_decide; naive_solver.
Qed.
(* stdpp/fin_maps.v *)
Lemma partial_alter_subset {A} f (m : M A) i :
  m !! i = None → is_Some (f (m !! i)) → m ⊂ partial_alter f i m.
Proof.
  intros Hi Hfi. apply map_subset_alt; split; [by apply partial_alter_subseteq|].
  exists i. by rewrite lookup_partial_alter_eq.
Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_partial_alter_Some {A} (f : option A → option A) (m : M A) i j x :
  partial_alter f i m !! j = Some x ↔
    (i = j ∧ f (m !! i) = Some x) ∨ (i ≠ j ∧ m !! j = Some x).
Proof. rewrite lookup_partial_alter. repeat case_decide; naive_solver. Qed.
(* stdpp/fin_maps.v *)
(* ** Properties of the [alter] operation *)
Lemma lookup_alter {A} (f : A → A) (m : M A) i j :
  alter f i m !! j = if decide (i = j) then f <$> m !! i else m !! j.
Proof. apply lookup_partial_alter. Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_alter_eq {A} (f : A → A) (m : M A) i : alter f i m !! i = f <$> m !! i.
Proof. apply lookup_partial_alter_eq. Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_alter_ne {A} (f : A → A) (m : M A) i j :
  i ≠ j → alter f i m !! j = m !! j.
Proof. apply lookup_partial_alter_ne. Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_total_alter `{!Inhabited A} (f : A → A) (m : M A) i j :
  alter f i m !!! j =
    if decide (i = j) then default inhabitant (f <$> m !! i) else m !!! j.
Proof. apply lookup_total_partial_alter. Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_total_alter_eq `{!Inhabited A} (f : A → A) (m : M A) i :
  alter f i m !!! i = default inhabitant (f <$> m !! i).
Proof. apply lookup_total_partial_alter_eq. Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_total_alter_ne `{!Inhabited A} (f : A → A) (m : M A) i j :
  i ≠ j → alter f i m !!! j = m !!! j.
Proof. apply lookup_total_partial_alter_ne. Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_alter_Some {A} (f : A → A) (m : M A) i j y :
  alter f i m !! j = Some y ↔
    (i = j ∧ ∃ x, m !! j = Some x ∧ y = f x) ∨ (i ≠ j ∧ m !! j = Some y).
Proof.
  rewrite lookup_alter. case_decide; naive_solver (simplify_option_eq; eauto).
Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_alter_is_Some {A} (f : A → A) (m : M A) i j :
  is_Some (alter f i m !! j) ↔ is_Some (m !! j).
Proof.
  unfold is_Some. setoid_rewrite lookup_alter_Some.
  destruct (decide (i = j)); naive_solver.
Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_alter_None {A} (f : A → A) (m : M A) i j :
  alter f i m !! j = None ↔ m !! j = None.
Proof. by rewrite !eq_None_not_Some, lookup_alter_is_Some. Qed.
(* stdpp/fin_maps.v *)
Lemma alter_empty {A} f i : alter f i ∅ =@{M A} ∅.
Proof.
  apply map_eq; intros k. rewrite lookup_alter, !lookup_empty. by case_decide.
Qed.
(* stdpp/fin_maps.v *)
Lemma alter_ext {A} (f g : A → A) (m : M A) i :
  (∀ x, m !! i = Some x → f x = g x) → alter f i m = alter g i m.
Proof. intro. apply partial_alter_ext. intros [x|] ?; f_equal/=; auto. Qed.
(* stdpp/fin_maps.v *)
Lemma alter_id {A} (f : A → A) (m : M A) i :
  (∀ x, m !! i = Some x → f x = x) → alter f i m = m.
Proof. intros. apply partial_alter_id. destruct (m !! i); f_equal/=; auto. Qed.
(* stdpp/fin_maps.v *)
Lemma alter_id' {A} (f : A → A) (m : M A) i :
  m !! i = None → alter f i m = m.
Proof. intros. apply alter_id. naive_solver. Qed.
(* stdpp/fin_maps.v *)
Lemma alter_partial_alter {A} f g (m : M A) i j :
  alter f i (partial_alter g j m) =
    if decide (i = j) then partial_alter (fmap f ∘ g) i m
    else partial_alter g j (alter f i m).
Proof. apply partial_alter_partial_alter. Qed.
(* stdpp/fin_maps.v *)
Lemma alter_partial_alter_eq {A} f g (m : M A) i :
  alter f i (partial_alter g i m) = partial_alter (fmap f ∘ g) i m.
Proof. intros. by rewrite alter_partial_alter, decide_True. Qed.
(* stdpp/fin_maps.v *)
Lemma alter_partial_alter_ne {A} f g (m : M A) i j :
  i ≠ j →
  alter f i (partial_alter g j m) = partial_alter g j (alter f i m).
Proof. intros. by rewrite alter_partial_alter, decide_False. Qed.
(* stdpp/fin_maps.v *)
Lemma alter_alter {A} (f g : A → A) (m : M A) i j :
  alter f i (alter g j m) =
    if decide (i = j) then alter (f ∘ g) i m else alter g j (alter f i m).
Proof.
  unfold alter, map_alter. rewrite partial_alter_partial_alter.
  case_decide; subst; [|done]. apply partial_alter_ext. by intros [?|].
Qed.
(* stdpp/fin_maps.v *)
Lemma alter_alter_eq {A} (f g : A → A) (m : M A) i:
  alter f i (alter g i m) = alter (f ∘ g) i m.
Proof. by rewrite alter_alter, decide_True. Qed.
(* stdpp/fin_maps.v *)
Lemma alter_alter_ne {A} (f g : A → A) (m : M A) i j :
  i ≠ j → alter f i (alter g j m) = alter g j (alter f i m).
Proof. intros. by rewrite alter_alter, decide_False. Qed.
(* stdpp/fin_maps.v *)
Lemma alter_delete {A} (m : M A) i j f :
  alter f i (delete j m) =
    if decide (i = j) then delete i m else delete j (alter f i m).
Proof. apply partial_alter_delete. Qed.
(* stdpp/fin_maps.v *)
Lemma alter_delete_eq {A} (m : M A) i f :
  alter f i (delete i m) = delete i m.
Proof. by rewrite alter_delete, decide_True. Qed.
(* stdpp/fin_maps.v *)
Lemma alter_delete_ne {A} (m : M A) i j f :
  i ≠ j → alter f i (delete j m) = delete j (alter f i m).
Proof. intros. by rewrite alter_delete, decide_False. Qed.
(* stdpp/fin_maps.v *)
Lemma alter_insert {A} (m : M A) i j f x :
  alter f i (<[j:=x]> m) =
    if decide (i = j) then <[i:=f x]> m else <[j:=x]> (alter f i m).
Proof. apply partial_alter_insert. Qed.
(* stdpp/fin_maps.v *)
Lemma alter_insert_eq {A} (m : M A) i f x :
  alter f i (<[i:=x]> m) = <[i:=f x]> m.
Proof. by rewrite alter_insert, decide_True. Qed.
(* stdpp/fin_maps.v *)
Lemma alter_insert_ne {A} (m : M A) i j f x :
  i ≠ j → alter f i (<[j:=x]> m) = <[j:=x]> (alter f i m).
Proof. intros. by rewrite alter_insert, decide_False. Qed.
(* stdpp/fin_maps.v *)
Lemma alter_mono {A} f (m1 m2 : M A) i : m1 ⊆ m2 → alter f i m1 ⊆ alter f i m2.
Proof.
  rewrite !map_subseteq_spec. intros ? j x.
  rewrite !lookup_alter_Some. naive_solver.
Qed.
(* stdpp/fin_maps.v *)
Lemma alter_strict_mono {A} f (m1 m2 : M A) i :
  m1 ⊂ m2 → alter f i m1 ⊂ alter f i m2.
Proof.
  rewrite !map_subset_alt.
  intros [? (j&?&?)]; split; auto using alter_mono.
  exists j. by rewrite lookup_alter_None, lookup_alter_is_Some.
Qed.
(* stdpp/fin_maps.v *)
(* ** Properties of the [delete] operation *)
Lemma lookup_delete {A} (m : M A) i j :
  delete i m !! j = if decide (i = j) then None else m !! j.
Proof. apply lookup_partial_alter. Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_delete_eq {A} (m : M A) i : delete i m !! i = None.
Proof. apply lookup_partial_alter_eq. Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_delete_ne {A} (m : M A) i j : i ≠ j → delete i m !! j = m !! j.
Proof. apply lookup_partial_alter_ne. Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_total_delete `{!Inhabited A} (m : M A) i j :
  delete i m !! j = if decide (i = j) then inhabitant else m !! j.
Proof. apply lookup_partial_alter. Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_total_delete_eq `{!Inhabited A} (m : M A) i :
  delete i m !!! i = inhabitant.
Proof. by rewrite lookup_total_alt, lookup_delete_eq. Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_total_delete_ne `{!Inhabited A} (m : M A) i j :
  i ≠ j → delete i m !!! j = m !!! j.
Proof. intros. by rewrite lookup_total_alt, lookup_delete_ne. Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_delete_Some {A} (m : M A) i j y :
  delete i m !! j = Some y ↔ i ≠ j ∧ m !! j = Some y.
Proof. rewrite lookup_delete. case_decide; naive_solver. Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_delete_is_Some {A} (m : M A) i j :
  is_Some (delete i m !! j) ↔ i ≠ j ∧ is_Some (m !! j).
Proof. unfold is_Some; setoid_rewrite lookup_delete_Some; naive_solver. Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_delete_None {A} (m : M A) i j :
  delete i m !! j = None ↔ i = j ∨ m !! j = None.
Proof. rewrite lookup_delete. case_decide; naive_solver. Qed.
(* stdpp/fin_maps.v *)
Lemma delete_empty {A} i : delete i ∅ =@{M A} ∅.
Proof. rewrite <-(partial_alter_self ∅) at 2. by rewrite lookup_empty. Qed.
(* stdpp/fin_maps.v *)
Lemma delete_id {A} (m : M A) i : m !! i = None → delete i m = m.
Proof. intros. by apply partial_alter_id. Qed.
(* stdpp/fin_maps.v *)
Lemma delete_partial_alter {A} (m : M A) i j f :
  delete i (partial_alter f j m) =
    if decide (i = j) then delete i m else partial_alter f j (delete i m).
Proof. apply partial_alter_partial_alter. Qed.
(* stdpp/fin_maps.v *)
Lemma delete_partial_alter_eq {A} (m : M A) i f :
  delete i (partial_alter f i m) = delete i m.
Proof. by rewrite delete_partial_alter, decide_True. Qed.
(* stdpp/fin_maps.v *)
Lemma delete_partial_alter_ne {A} (m : M A) i j f :
  i ≠ j → delete i (partial_alter f j m) = partial_alter f j (delete i m).
Proof. intros. by rewrite delete_partial_alter, decide_False. Qed.
(* stdpp/fin_maps.v *)
Lemma delete_partial_alter_id {A} (m : M A) i f :
  m !! i = None → delete i (partial_alter f i m) = m.
Proof. intros. by rewrite delete_partial_alter_eq, delete_id. Qed.
(* stdpp/fin_maps.v *)
Lemma delete_alter {A} (m : M A) i j f :
  delete i (alter f j m) =
    if decide (i = j) then delete i m else alter f j (delete i m).
Proof.
  unfold delete, alter, map_delete, map_alter.
  rewrite partial_alter_partial_alter. by case_decide.
Qed.
(* stdpp/fin_maps.v *)
Lemma delete_alter_eq {A} (m : M A) i f :
  delete i (alter f i m) = delete i m.
Proof. by rewrite delete_alter, decide_True. Qed.
(* stdpp/fin_maps.v *)
Lemma delete_alter_ne {A} (m : M A) i j f :
  i ≠ j → delete i (alter f j m) = alter f j (delete i m).
Proof. intros. by rewrite delete_alter, decide_False. Qed.
(* stdpp/fin_maps.v *)
Lemma delete_alter_id {A} f (m : M A) i :
  m !! i = None → delete i (alter f i m) = m.
Proof. intros. by rewrite delete_alter_eq, delete_id. Qed.
(* stdpp/fin_maps.v *)
Lemma delete_delete {A} (m : M A) i j :
  delete i (delete j m) = delete j (delete i m).
Proof.
  apply map_eq; intros k. rewrite !lookup_delete.
  repeat case_decide; naive_solver.
Qed.
(* stdpp/fin_maps.v *)
Lemma delete_delete_eq {A} (m : M A) i :
  delete i (delete i m) = delete i m.
Proof. apply partial_alter_partial_alter_eq. Qed.
(* stdpp/fin_maps.v *)
Lemma delete_insert {A} (m : M A) i j x :
  delete i (<[j:=x]> m) =
    if decide (i = j) then delete i m else <[j:=x]>(delete i m).
Proof. apply delete_partial_alter. Qed.
(* stdpp/fin_maps.v *)
Lemma delete_insert_eq {A} (m : M A) i x :
  delete i (<[i:=x]> m) = delete i m.
Proof. by rewrite delete_insert, decide_True. Qed.
(* stdpp/fin_maps.v *)
Lemma delete_insert_ne {A} (m : M A) i j x :
  i ≠ j → delete i (<[j:=x]> m) = <[j:=x]>(delete i m).
Proof. intros. by rewrite delete_insert, decide_False. Qed.
(* stdpp/fin_maps.v *)
Lemma delete_insert_id {A} (m : M A) i x :
  m !! i = None → delete i (<[i:=x]> m) = m.
Proof. intros. by rewrite delete_insert_eq, delete_id. Qed.
(* stdpp/fin_maps.v *)
Lemma delete_subseteq {A} (m : M A) i : delete i m ⊆ m.
Proof.
  rewrite !map_subseteq_spec. intros j x. rewrite lookup_delete_Some. tauto.
Qed.
(* stdpp/fin_maps.v *)
Lemma delete_subset {A} (m : M A) i : is_Some (m !! i) → delete i m ⊂ m.
Proof.
  intros [x ?]; apply map_subset_alt; split; [apply delete_subseteq|].
  exists i. rewrite lookup_delete_eq; eauto.
Qed.
(* stdpp/fin_maps.v *)
Lemma delete_mono {A} (m1 m2 : M A) i : m1 ⊆ m2 → delete i m1 ⊆ delete i m2.
Proof.
  rewrite !map_subseteq_spec. intros ? j x.
  rewrite !lookup_delete_Some. intuition eauto.
Qed.
(* stdpp/fin_maps.v *)
(* ** Properties of the [insert] operation *)
Lemma lookup_insert {A} (m : M A) i j x :
  <[i:=x]> m !! j = if decide (i = j) then Some x else m !! j.
Proof. apply lookup_partial_alter. Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_insert_eq {A} (m : M A) i x : <[i:=x]> m !! i = Some x.
Proof. apply lookup_partial_alter_eq. Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_insert_ne {A} (m : M A) i j x : i ≠ j → <[i:=x]> m !! j = m !! j.
Proof. apply lookup_partial_alter_ne. Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_total_insert `{!Inhabited A} (m : M A) i j x :
  <[i:=x]> m !!! j = if decide (i = j) then x else m !!! j.
Proof. apply lookup_total_partial_alter. Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_total_insert_eq `{!Inhabited A} (m : M A) i x : <[i:=x]> m !!! i = x.
Proof. apply lookup_total_partial_alter_eq. Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_total_insert_ne `{!Inhabited A} (m : M A) i j x :
  i ≠ j → <[i:=x]> m !!! j = m !!! j.
Proof. apply lookup_total_partial_alter_ne. Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_insert_Some {A} (m : M A) i j x y :
  <[i:=x]> m !! j = Some y ↔ (i = j ∧ x = y) ∨ (i ≠ j ∧ m !! j = Some y).
Proof. rewrite lookup_insert. case_decide; naive_solver. Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_insert_is_Some {A} (m : M A) i j x :
  is_Some (<[i:=x]> m !! j) ↔ i = j ∨ i ≠ j ∧ is_Some (m !! j).
Proof. unfold is_Some; setoid_rewrite lookup_insert_Some; naive_solver. Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_insert_is_Some' {A} (m : M A) i j x :
  is_Some (<[i:=x]> m !! j) ↔ i = j ∨ is_Some (m !! j).
Proof. rewrite lookup_insert_is_Some. destruct (decide (i=j)); naive_solver. Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_insert_None {A} (m : M A) i j x :
  <[i:=x]> m !! j = None ↔ m !! j = None ∧ i ≠ j.
Proof. rewrite lookup_insert. case_decide; naive_solver. Qed.
(* stdpp/fin_maps.v *)
Lemma lookup_insert_rev {A} (m : M A) i x y : <[i:=x]> m !! i = Some y → x = y.
Proof. rewrite lookup_insert_eq. congruence. Qed.
(* stdpp/fin_maps.v *)
Lemma insert_id {A} (m : M A) i x : m !! i = Some x → <[i:=x]> m = m.
Proof.
  intros; apply map_eq; intros j. rewrite lookup_insert.
  case_decide; naive_solver.
Qed.
(* stdpp/fin_maps.v *)
Lemma insert_included {A} R `{!∀ i, Reflexive (R i)} (m : M A) i x :
  (∀ y, m !! i = Some y → R i y x) → map_included R m (<[i:=x]> m).
Proof.
  intros ? j. rewrite lookup_insert.
  destruct (decide (i = j)), (m !! j) eqn:?; naive_solver.
Qed.
(* stdpp/fin_maps.v *)
Lemma insert_empty {A} i (x : A) : <[i:=x]> ∅ =@{M A} {[i:=x]}.
Proof. done. Qed.
(* stdpp/fin_maps.v *)
Lemma insert_non_empty {A} (m : M A) i x : <[i:=x]> m ≠ ∅.
Proof.
  intros Hi%(f_equal (.!! i)). by rewrite lookup_insert_eq, lookup_empty in Hi.
Qed.
(* stdpp/fin_maps.v *)
Lemma insert_partial_alter {A} f (m : M A) i j x :
  <[i:=x]> (partial_alter f j m) =
    if decide (i = j) then <[i:=x]> m else partial_alter f j (<[i:=x]> m).
Proof. apply partial_alter_partial_alter. Qed.
(* stdpp/fin_maps.v *)
Lemma insert_partial_alter_eq {A} f (m : M A) i x :
  <[i:=x]> (partial_alter f i m) = <[i:=x]> m.
Proof. by rewrite insert_partial_alter, decide_True. Qed.
(* stdpp/fin_maps.v *)
Lemma insert_partial_alter_ne {A} f (m : M A) i j x :
  i ≠ j → <[i:=x]> (partial_alter f j m) = partial_alter f j (<[i:=x]> m).
Proof. intros. by rewrite insert_partial_alter, decide_False. Qed.
(* stdpp/fin_maps.v *)
Lemma insert_partial_alter_id {A} f (m : M A) i x :
  m !! i = Some x → <[i:=x]> (partial_alter f i m) = m.
Proof. intros. by rewrite insert_partial_alter_eq, insert_id. Qed.
(* stdpp/fin_maps.v *)
Lemma insert_alter {A} f (m : M A) i j x :
  <[i:=x]> (alter f j m) =
    if decide (i = j) then <[i:=x]> m else alter f j (<[i:=x]> m).
Proof. apply partial_alter_alter. Qed.
(* stdpp/fin_maps.v *)
Lemma insert_alter_eq {A} f (m : M A) i x : <[i:=x]> (alter f i m) = <[i:=x]> m.
Proof. by rewrite insert_alter, decide_True. Qed.
(* stdpp/fin_maps.v *)
Lemma insert_alter_ne {A} f (m : M A) i j x :
  i ≠ j → <[i:=x]> (alter f j m) = alter f j (<[i:=x]> m).
Proof. intros. by rewrite insert_alter, decide_False. Qed.
(* stdpp/fin_maps.v *)
Lemma insert_alter_id {A} f (m : M A) i x :
  m !! i = Some x → <[i:=x]> (alter f i m) = m.
Proof. intros. by rewrite insert_alter_eq, insert_id. Qed.
(* stdpp/fin_maps.v *)
Lemma insert_delete {A} (m : M A) i j x :
  <[i:=x]> (delete j m) =
    if decide (i = j) then <[i:=x]> m else delete j (<[i:=x]> m).
Proof. apply partial_alter_delete. Qed.
(* stdpp/fin_maps.v *)
Lemma insert_delete_eq {A} (m : M A) i x : <[i:=x]> (delete i m) = <[i:=x]> m.
Proof. by rewrite insert_delete, decide_True. Qed.
(* stdpp/fin_maps.v *)
Lemma insert_delete_ne {A} (m : M A) i j x :
  i ≠ j → <[i:=x]> (delete j m) = delete j (<[i:=x]> m).
Proof. intros. by rewrite insert_delete, decide_False. Qed.
(* stdpp/fin_maps.v *)
Lemma insert_delete_id {A} (m : M A) i x :
  m !! i = Some x → <[i:=x]> (delete i m) = m.
Proof. intros. by rewrite insert_delete_eq, insert_id. Qed.
(* stdpp/fin_maps.v *)
Lemma insert_insert {A} (m : M A) i j x y :
  <[i:=x]> (<[j:=y]> m) =
    if decide (i = j) then <[i:=x]> m else <[j:=y]> (<[i:=x]> m).
Proof. apply partial_alter_insert. Qed.
(* stdpp/fin_maps.v *)
Lemma insert_insert_eq {A} (m : M A) i x y : <[i:=x]> (<[i:=y]> m) = <[i:=x]> m.
Proof. by rewrite insert_insert, decide_True. Qed.
(* stdpp/fin_maps.v *)
Lemma insert_insert_ne {A} (m : M A) i j x y :
  i ≠ j → <[i:=x]> (<[j:=y]> m) = <[j:=y]> (<[i:=x]> m).
Proof. intros. by rewrite insert_insert, decide_False. Qed.
(* stdpp/fin_maps.v *)
Lemma alter_alt {A} (f : A → A) (m : M A) i :
  alter f i m = match m !! i with Some x => <[i:=f x]> m | None => m end.
Proof.
  apply map_eq; intros j. rewrite lookup_alter. destruct (m !! i) eqn:?; simpl.
  - by rewrite lookup_insert.
  - destruct (decide _); naive_solver.
Qed.
(* stdpp/fin_maps.v *)
Lemma alter_alt_Some {A} (f : A → A) (m : M A) i x :
  m !! i = Some x → alter f i m = <[i:=f x]> m.
Proof. intros Hi. by rewrite alter_alt, Hi. Qed.
(* stdpp/fin_maps.v *)
Lemma insert_subseteq {A} (m : M A) i x : m !! i = None → m ⊆ <[i:=x]> m.
Proof. apply partial_alter_subseteq. Qed.
(* stdpp/fin_maps.v *)
Lemma insert_subset {A} (m : M A) i x : m !! i = None → m ⊂ <[i:=x]> m.
Proof. intro. apply partial_alter_subset; eauto. Qed.
(* stdpp/fin_maps.v *)
Lemma insert_mono {A} (m1 m2 : M A) i x : m1 ⊆ m2 → <[i:=x]> m1 ⊆ <[i:=x]> m2.
Proof.
  rewrite !map_subseteq_spec.
  intros Hm j y. rewrite !lookup_insert_Some. naive_solver.
Qed.
(* stdpp/fin_maps.v *)
Lemma insert_subseteq_r {A} (m1 m2 : M A) i x :
  m1 !! i = None → m1 ⊆ m2 → m1 ⊆ <[i:=x]> m2.
Proof.
  intros. trans (<[i:=x]> m1); eauto using insert_subseteq, insert_mono.
Qed.
(* stdpp/fin_maps.v *)
Lemma insert_subseteq_l {A} (m1 m2 : M A) i x :
  m2 !! i = Some x → m1 ⊆ m2 → <[i:=x]> m1 ⊆ m2.
Proof.
  intros Hi Hincl. etrans; [apply insert_mono, Hincl|]. by rewrite insert_id.
Qed.
(* stdpp/fin_maps.v *)
Lemma insert_delete_subseteq {A} (m1 m2 : M A) i x :
  m1 !! i = None → <[i:=x]> m1 ⊆ m2 → m1 ⊆ delete i m2.
Proof.
  rewrite !map_subseteq_spec. intros Hi Hix j y Hj.
  destruct (decide (i = j)) as [->|]; [congruence|].
  rewrite lookup_delete_ne by done.
  apply Hix; by rewrite lookup_insert_ne by done.
Qed.
(* stdpp/fin_maps.v *)
Lemma delete_insert_subseteq {A} (m1 m2 : M A) i x :
  m1 !! i = Some x → delete i m1 ⊆ m2 → m1 ⊆ <[i:=x]> m2.
Proof.
  rewrite !map_subseteq_spec.
  intros Hix Hi j y Hj. destruct (decide (i = j)) as [->|?].
  - rewrite lookup_insert_eq. congruence.
  - rewrite lookup_insert_ne by done. apply Hi. by rewrite lookup_delete_ne.
Qed.