phanerozoic/Coq-Iris huggingface dataset:
(* iris/algebra/excl.v *)
Lemma excl_map_compose {A B C} (f : A → B) (g : B → C) (x : excl A) :
  excl_map (g ∘ f) x = excl_map g (excl_map f x).
Proof. by destruct x. Qed.
(* iris/algebra/excl.v *)
Lemma excl_map_ext {SI : sidx} {A B : ofe} (f g : A → B) x :
  (∀ x, f x ≡ g x) → excl_map f x ≡ excl_map g x.
Proof. by destruct x; constructor. Qed.
(* iris/algebra/excl.v *)
Instance excl_map_ne {SI : sidx} {A B : ofe} n :
  Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@excl_map A B).
Proof. by intros f f' Hf; destruct 1; constructor; apply Hf. Qed.
(* iris/algebra/excl.v *)
Instance excl_map_cmra_morphism {SI : sidx} {A B : ofe} (f : A → B) :
  NonExpansive f → CmraMorphism (excl_map f).
Proof. split; try done; try apply _. by intros n [a|]. Qed.
(* iris/algebra/excl.v *)
Definition exclO_map {SI : sidx} {A B} (f : A -n> B) : exclO A -n> exclO B
:=
  OfeMor (excl_map f).
(* iris/algebra/excl.v *)
Instance exclO_map_ne {SI : sidx} A B : NonExpansive (@exclO_map SI A B).
Proof. by intros n f f' Hf []; constructor; apply Hf. Qed.
(* iris/algebra/excl.v *)
Definition exclRF {SI : sidx} (F : oFunctor) : rFunctor := {|
  rFunctor_car A _ B _ := (exclR (oFunctor_car F A B));
  rFunctor_map A1 _ A2 _ B1 _ B2 _ fg := exclO_map (oFunctor_map F fg)
|}.
Next Obligation.
  intros ? F A1 ? A2 ? B1 ? B2 ? n x1 x2 ??.
  by apply exclO_map_ne, oFunctor_map_ne.
Qed.
(* iris/algebra/excl.v *)
Instance exclRF_contractive {SI : sidx} F :
  oFunctorContractive F → rFunctorContractive (exclRF F).
Proof.
  intros A1 ? A2 ? B1 ? B2 ? n x1 x2 ??.
  by apply exclO_map_ne, oFunctor_map_contractive.
Qed.
(* iris/algebra/frac.v *)
(* Since the standard (0,1] fractional camera is used more often, we define
[frac] through a [Notation] instead of a [Definition]. That way, Coq infers the
[frac] camera by default when using the [Qp] type. *)
Notation frac
:= Qp (only parsing).
(* iris/algebra/frac.v *)
Canonical fracO
:= leibnizO frac.
(* iris/algebra/frac.v *)
Instance frac_valid_instance : Valid frac
:= λ x, (x ≤ 1)%Qp.
(* iris/algebra/frac.v *)
Instance frac_pcore_instance : PCore frac
:= λ _, None.
(* iris/algebra/frac.v *)
Instance frac_op_instance : Op frac
:= λ x y, (x + y)%Qp.
(* iris/algebra/frac.v *)
Lemma frac_valid p : ✓ p ↔ (p ≤ 1)%Qp.
Proof. done. Qed.
(* iris/algebra/frac.v *)
Lemma frac_valid_1 : ✓ 1%Qp.
Proof. done. Qed.
(* iris/algebra/frac.v *)
Lemma frac_op p q : p ⋅ q = (p + q)%Qp.
Proof. done. Qed.
(* iris/algebra/frac.v *)
Lemma frac_included p q : p ≼ q ↔ (p < q)%Qp.
Proof. by rewrite Qp.lt_sum. Qed.
(* iris/algebra/frac.v *)
Corollary frac_included_weak p q : p ≼ q → (p ≤ q)%Qp.
Proof. rewrite frac_included. apply Qp.lt_le_incl. Qed.
(* iris/algebra/frac.v *)
Definition frac_ra_mixin : RAMixin frac.
Proof.
    split; try apply _; try done.
    intros p q. rewrite !frac_valid frac_op=> ?.
    trans (p + q)%Qp; last done. apply Qp.le_add_l.
  Qed.
(* iris/algebra/frac.v *)
Canonical fracR
:= discreteR frac frac_ra_mixin.
(* iris/algebra/frac.v *)
Instance frac_cmra_discrete : CmraDiscrete fracR.
Proof. apply discrete_cmra_discrete. Qed.
(* iris/algebra/frac.v *)
Instance frac_full_exclusive : Exclusive 1%Qp.
Proof. intros p. apply Qp.not_add_le_l. Qed.
(* iris/algebra/frac.v *)
Instance frac_cancelable (q : frac) : Cancelable q.
Proof. intros n p1 p2 _. apply (inj (Qp.add q)). Qed.
(* iris/algebra/frac.v *)
Instance frac_id_free (q : frac) : IdFree q.
Proof. intros p _. apply Qp.add_id_free. Qed.
(* iris/algebra/frac.v *)
(* This one has a higher precendence than [is_op_op] so we get a [+] instead
     of an [⋅]. *)
Instance frac_is_op q1 q2 : IsOp (q1 + q2)%Qp q1 q2 | 10.
Proof. done. Qed.
(* iris/algebra/frac.v *)
Instance is_op_frac q : IsOp' q (q/2)%Qp (q/2)%Qp.
Proof. by rewrite /IsOp' /IsOp frac_op Qp.div_2. Qed.
(* iris/algebra/functions.v *)
Definition discrete_fun_insert {SI : sidx} `{!EqDecision A} {B : A → ofe}
    (x : A) (y : B x) (f : discrete_fun B) : discrete_fun B
:= λ x',
  match decide (x = x') with left H => eq_rect _ B y _ H | right _ => f x' end.
(* iris/algebra/functions.v *)
Instance : Params (@discrete_fun_insert) 6
:= {}.
(* iris/algebra/functions.v *)
Definition discrete_fun_singleton {SI : sidx} `{!EqDecision A} {B : A → ucmra}
  (x : A) (y : B x) : discrete_fun B
:= discrete_fun_insert x y ε.
(* iris/algebra/functions.v *)
Instance : Params (@discrete_fun_singleton) 6
:= {}.
(* iris/algebra/functions.v *)
Instance discrete_funO_ofe_discrete :
    (∀ i, OfeDiscrete (B i)) → OfeDiscrete (discrete_funO B).
Proof. intros HB f f' Heq i. apply HB, Heq. Qed.
(* iris/algebra/functions.v *)
(* Properties of discrete_fun_insert. *)
Instance discrete_fun_insert_ne x :
    NonExpansive2 (discrete_fun_insert (B:=B) x).
Proof.
    intros n y1 y2 ? f1 f2 ? x'; rewrite /discrete_fun_insert.
    by destruct (decide _) as [[]|].
  Qed.
(* iris/algebra/functions.v *)
Instance discrete_fun_insert_proper x :
    Proper ((≡) ==> (≡) ==> (≡)) (discrete_fun_insert (B:=B) x)
:= ne_proper_2 _.
(* iris/algebra/functions.v *)
Lemma discrete_fun_lookup_insert f x y : (discrete_fun_insert x y f) x = y.
Proof.
    rewrite /discrete_fun_insert; destruct (decide _) as [Hx|]; last done.
    by rewrite (proof_irrel Hx eq_refl).
  Qed.
(* iris/algebra/functions.v *)
Lemma discrete_fun_lookup_insert_ne f x x' y :
    x ≠ x' → (discrete_fun_insert x y f) x' = f x'.
Proof. by rewrite /discrete_fun_insert; destruct (decide _). Qed.
(* iris/algebra/functions.v *)
Instance discrete_fun_insert_discrete f x y :
    Discrete f → Discrete y → Discrete (discrete_fun_insert x y f).
Proof.
    intros ?? g Heq x'; destruct (decide (x = x')) as [->|].
    - rewrite discrete_fun_lookup_insert.
      apply: discrete. by rewrite -(Heq x') discrete_fun_lookup_insert.
    - rewrite discrete_fun_lookup_insert_ne //.
      apply: discrete. by rewrite -(Heq x') discrete_fun_lookup_insert_ne.
  Qed.
(* iris/algebra/functions.v *)
Instance discrete_funR_cmra_discrete:
    (∀ i, CmraDiscrete (B i)) → CmraDiscrete (discrete_funR B).
Proof. intros HB. split; [apply _|]. intros x Hv i. apply HB, Hv. Qed.
(* iris/algebra/functions.v *)
Instance discrete_fun_singleton_ne x :
    NonExpansive (discrete_fun_singleton x : B x → _).
Proof.
    intros n y1 y2 ?; apply discrete_fun_insert_ne; [done|].
    by apply equiv_dist.
  Qed.
(* iris/algebra/functions.v *)
Instance discrete_fun_singleton_proper x :
    Proper ((≡) ==> (≡)) (discrete_fun_singleton x)
:= ne_proper _.
(* iris/algebra/functions.v *)
Lemma discrete_fun_lookup_singleton x (y : B x) : (discrete_fun_singleton x y) x = y.
Proof. by rewrite /discrete_fun_singleton discrete_fun_lookup_insert. Qed.
(* iris/algebra/functions.v *)
Lemma discrete_fun_lookup_singleton_ne x x' (y : B x) :
    x ≠ x' → (discrete_fun_singleton x y) x' = ε.
Proof. intros; by rewrite /discrete_fun_singleton discrete_fun_lookup_insert_ne. Qed.
(* iris/algebra/functions.v *)
Instance discrete_fun_singleton_discrete x (y : B x) :
    (∀ i, Discrete (ε : B i)) →  Discrete y → Discrete (discrete_fun_singleton x y).
Proof. apply _. Qed.
(* iris/algebra/functions.v *)
Lemma discrete_fun_singleton_validN n x (y : B x) : ✓{n} discrete_fun_singleton x y ↔ ✓{n} y.
Proof.
    split; [by move=>/(_ x); rewrite discrete_fun_lookup_singleton|].
    move=>Hx x'; destruct (decide (x = x')) as [->|];
      rewrite ?discrete_fun_lookup_singleton ?discrete_fun_lookup_singleton_ne //.
    by apply ucmra_unit_validN.
  Qed.
(* iris/algebra/functions.v *)
Lemma discrete_fun_singleton_valid x (y : B x) : ✓ discrete_fun_singleton x y ↔ ✓ y.
Proof.
    by rewrite !cmra_valid_validN; setoid_rewrite discrete_fun_singleton_validN.
  Qed.
(* iris/algebra/functions.v *)
Lemma discrete_fun_singleton_unit x : discrete_fun_singleton x (ε : B x) ≡ ε.
Proof.
    move=>x'; destruct (decide (x = x')) as [->|];
      by rewrite ?discrete_fun_lookup_singleton ?discrete_fun_lookup_singleton_ne.
  Qed.
(* iris/algebra/functions.v *)
Lemma discrete_fun_singleton_core x (y : B x) :
    core (discrete_fun_singleton x y) ≡ discrete_fun_singleton x (core y).
Proof.
    move=>x'; destruct (decide (x = x')) as [->|];
      by rewrite discrete_fun_lookup_core ?discrete_fun_lookup_singleton
      ?discrete_fun_lookup_singleton_ne // (core_id_core _).
  Qed.
(* iris/algebra/functions.v *)
Instance discrete_fun_singleton_core_id x (y : B x) :
    CoreId y → CoreId (discrete_fun_singleton x y).
Proof. by rewrite !core_id_total discrete_fun_singleton_core=> ->. Qed.
(* iris/algebra/functions.v *)
Lemma discrete_fun_singleton_op (x : A) (y1 y2 : B x) :
    discrete_fun_singleton x y1 ⋅ discrete_fun_singleton x y2 ≡ discrete_fun_singleton x (y1 ⋅ y2).
Proof.
    intros x'; destruct (decide (x' = x)) as [->|].
    - by rewrite discrete_fun_lookup_op !discrete_fun_lookup_singleton.
    - by rewrite discrete_fun_lookup_op !discrete_fun_lookup_singleton_ne // left_id.
  Qed.
(* iris/algebra/functions.v *)
Lemma discrete_fun_insert_updateP x (P : B x → Prop) (Q : discrete_fun B → Prop) g y1 :
    y1 ~~>: P → (∀ y2, P y2 → Q (discrete_fun_insert x y2 g)) →
    discrete_fun_insert x y1 g ~~>: Q.
Proof.
    intros Hy1 HP; apply cmra_total_updateP.
    intros n gf Hg. destruct (Hy1 n (Some (gf x))) as (y2&?&?).
    { move: (Hg x). by rewrite discrete_fun_lookup_op discrete_fun_lookup_insert. }
    exists (discrete_fun_insert x y2 g); split; [auto|].
    intros x'; destruct (decide (x' = x)) as [->|];
      rewrite discrete_fun_lookup_op ?discrete_fun_lookup_insert //; [].
    move: (Hg x'). by rewrite discrete_fun_lookup_op !discrete_fun_lookup_insert_ne.
  Qed.
(* iris/algebra/functions.v *)
Lemma discrete_fun_insert_updateP' x (P : B x → Prop) g y1 :
    y1 ~~>: P →
    discrete_fun_insert x y1 g ~~>: λ g', ∃ y2, g' = discrete_fun_insert x y2 g ∧ P y2.
Proof. eauto using discrete_fun_insert_updateP. Qed.
(* iris/algebra/functions.v *)
Lemma discrete_fun_insert_update g x y1 y2 :
    y1 ~~> y2 → discrete_fun_insert x y1 g ~~> discrete_fun_insert x y2 g.
Proof.
    rewrite !cmra_update_updateP; eauto using discrete_fun_insert_updateP with subst.
  Qed.
(* iris/algebra/functions.v *)
Lemma discrete_fun_singleton_updateP x (P : B x → Prop) (Q : discrete_fun B → Prop) y1 :
    y1 ~~>: P → (∀ y2, P y2 → Q (discrete_fun_singleton x y2)) →
    discrete_fun_singleton x y1 ~~>: Q.
Proof. rewrite /discrete_fun_singleton; eauto using discrete_fun_insert_updateP. Qed.
(* iris/algebra/functions.v *)
Lemma discrete_fun_singleton_updateP' x (P : B x → Prop) y1 :
    y1 ~~>: P →
    discrete_fun_singleton x y1 ~~>: λ g, ∃ y2, g = discrete_fun_singleton x y2 ∧ P y2.
Proof. eauto using discrete_fun_singleton_updateP. Qed.
(* iris/algebra/functions.v *)
Lemma discrete_fun_singleton_update x (y1 y2 : B x) :
    y1 ~~> y2 → discrete_fun_singleton x y1 ~~> discrete_fun_singleton x y2.
Proof. eauto using discrete_fun_insert_update. Qed.
(* iris/algebra/functions.v *)
Lemma discrete_fun_singleton_updateP_empty x (P : B x → Prop) (Q : discrete_fun B → Prop) :
    ε ~~>: P → (∀ y2, P y2 → Q (discrete_fun_singleton x y2)) → ε ~~>: Q.
Proof.
    intros Hx HQ; apply cmra_total_updateP.
    intros n gf Hg. destruct (Hx n (Some (gf x))) as (y2&?&?); first apply Hg.
    exists (discrete_fun_singleton x y2); split; [by apply HQ|].
    intros x'; destruct (decide (x' = x)) as [->|].
    - by rewrite discrete_fun_lookup_op discrete_fun_lookup_singleton.
    - rewrite discrete_fun_lookup_op discrete_fun_lookup_singleton_ne //; by apply Hg.
  Qed.
(* iris/algebra/functions.v *)
Lemma discrete_fun_singleton_updateP_empty' x (P : B x → Prop) :
    ε ~~>: P → ε ~~>: λ g, ∃ y2, g = discrete_fun_singleton x y2 ∧ P y2.
Proof. eauto using discrete_fun_singleton_updateP_empty. Qed.
(* iris/algebra/functions.v *)
Lemma discrete_fun_singleton_update_empty x (y : B x) :
    ε ~~> y → ε ~~> discrete_fun_singleton x y.
Proof.
    rewrite !cmra_update_updateP;
      eauto using discrete_fun_singleton_updateP_empty with subst.
  Qed.
(* iris/algebra/functions.v *)
Lemma discrete_fun_updateP `{!Finite A} f P Q :
    (∀ a, f a ~~>: P a) → (∀ f', (∀ a, P a (f' a)) → Q f') → f ~~>: Q.
Proof.
    repeat setoid_rewrite cmra_total_updateP. intros Hf HP n h Hh.
    destruct (finite_choice
      (λ a y, P a y ∧ ✓{n} (y ⋅ (h a)))) as [f' Hf']; first naive_solver.
    naive_solver.
  Qed.
(* iris/algebra/functions.v *)
Lemma discrete_fun_updateP' `{!Finite A} f P :
    (∀ a, f a ~~>: P a) → f ~~>: λ f', ∀ a, P a (f' a).
Proof. eauto using discrete_fun_updateP. Qed.
(* iris/algebra/functions.v *)
Lemma discrete_fun_update f g :
    (∀ a, f a ~~> g a) → f ~~> g.
Proof.
    repeat setoid_rewrite cmra_total_update.
    intros Hfg n h Hh a. apply (Hfg a), Hh.
  Qed.
(* iris/algebra/gmap.v *)
Instance gmap_dist : Dist (gmap K A)
:= λ n m1 m2,
  ∀ i, m1 !! i ≡{n}≡ m2 !! i.
(* iris/algebra/gmap.v *)
Definition gmap_ofe_mixin : OfeMixin (gmap K A).
Proof.
  split.
  - intros m1 m2; split.
    + by intros Hm n k; apply equiv_dist.
    + intros Hm k; apply equiv_dist; intros n; apply Hm.
  - intros n; split.
    + by intros m k.
    + by intros m1 m2 ? k.
    + by intros m1 m2 m3 ?? k; trans (m2 !! k).
  - intros n n' m1 m2 ? k ?. by eapply dist_le.
Qed.
(* iris/algebra/gmap.v *)
Canonical gmapO : ofe
:= Ofe (gmap K A) gmap_ofe_mixin.
(* iris/algebra/gmap.v *)
Definition gmap_chain (c : chain gmapO) (k : K) : chain (optionO A) :=
  {| chain_car n :=  c n !! k |}.
Next Obligation. intros c k n p Hp. by apply c. Qed.
(* iris/algebra/gmap.v *)
Definition gmap_bchain {n} (c : bchain gmapO n)
    (k : K) : bchain (optionO A) n :=
  {| bchain_car p Hp := c p Hp !! k |}.
Next Obligation. intros n c k p γ Hpγ Hp Hγ; by apply c. Qed.
(* iris/algebra/gmap.v *)
Definition gmap_compl `{!Cofe A} : Compl gmapO
:= λ c,
  map_imap (λ i _, compl (gmap_chain c i)) (c 0ᵢ).
(* iris/algebra/gmap.v *)
Definition gmap_lbcompl `{!Cofe A} : LBCompl gmapO
:= λ n Hn c,
  map_imap (λ i _, lbcompl Hn (gmap_bchain c i)) (c _ (SIdx.limit_lt_0 _ Hn)).
(* iris/algebra/gmap.v *)
Instance gmap_cofe `{!Cofe A} : Cofe gmapO :=
  {| compl := gmap_compl; lbcompl := gmap_lbcompl |}.
Next Obligation.
  intros ? n c k. rewrite /gmap_compl map_lookup_imap.
  oinversion (λ H, chain_cauchy c 0ᵢ n H k); simplify_option_eq;
    [apply SIdx.le_0_l| |done].
  rewrite conv_compl /=. by apply reflexive_eq.
Qed.
(* iris/algebra/gmap.v *)
Instance gmap_ofe_discrete : OfeDiscrete A → OfeDiscrete gmapO.
Proof. intros ? m m' ? i. by apply (discrete_0 _). Qed.
(* iris/algebra/gmap.v *)
(* why doesn't this go automatic? *)
Instance gmapO_leibniz: LeibnizEquiv A → LeibnizEquiv gmapO.
Proof. intros; change (LeibnizEquiv (gmap K A)); apply _. Qed.
(* iris/algebra/gmap.v *)
Instance lookup_ne k : NonExpansive (lookup k : gmap K A → option A).
Proof. by intros n m1 m2. Qed.
(* iris/algebra/gmap.v *)
Instance lookup_total_ne `{!Inhabited A} k :
  NonExpansive (lookup_total k : gmap K A → A).
Proof. intros n m1 m2. rewrite !lookup_total_alt. by intros ->. Qed.
(* iris/algebra/gmap.v *)
Instance partial_alter_ne n :
  Proper ((dist n ==> dist n) ==> (=) ==> dist n ==> dist n)
         (partial_alter (M:=gmap K A)).
Proof.
  by intros f1 f2 Hf i ? <- m1 m2 Hm j; destruct (decide (i = j)) as [->|];
    rewrite ?lookup_partial_alter_eq ?lookup_partial_alter_ne //;
    try apply Hf; apply lookup_ne.
Qed.
(* iris/algebra/gmap.v *)
Instance insert_ne i : NonExpansive2 (insert (M:=gmap K A) i).
Proof. intros n x y ? m m' ? j; apply partial_alter_ne; by try constructor. Qed.
(* iris/algebra/gmap.v *)
Instance singleton_ne i : NonExpansive (singletonM i : A → gmap K A).
Proof. by intros ????; apply insert_ne. Qed.
(* iris/algebra/gmap.v *)
Instance delete_ne i : NonExpansive (delete (M:=gmap K A) i).
Proof.
  intros n m m' ? j; destruct (decide (i = j)); simplify_map_eq;
    [by constructor|by apply lookup_ne].
Qed.
(* iris/algebra/gmap.v *)
Instance alter_ne (f : A → A) (k : K) n :
  Proper (dist n ==> dist n) f → Proper (dist n ==> dist n) (alter (M := gmap K A) f k).
Proof. intros ? m m' Hm k'. by apply partial_alter_ne; [solve_proper|..]. Qed.
(* iris/algebra/gmap.v *)
Instance gmap_empty_discrete : Discrete (∅ : gmap K A).
Proof.
  intros m Hm i; specialize (Hm i); rewrite lookup_empty in Hm |- *.
  inversion_clear Hm; constructor.
Qed.
(* iris/algebra/gmap.v *)
Instance gmap_lookup_discrete m i : Discrete m → Discrete (m !! i).
Proof.
  intros ? [x|] Hx; [|by symmetry; apply: discrete].
  assert (m ≡{0ᵢ}≡ <[i:=x]> m)
    by (by symmetry in Hx; inversion Hx; ofe_subst; rewrite insert_id).
  by rewrite (discrete_0 m (<[i:=x]>m)) // lookup_insert_eq.
Qed.
(* iris/algebra/gmap.v *)
Instance gmap_insert_discrete m i x :
  Discrete x → Discrete m → Discrete (<[i:=x]>m).
Proof.
  intros ?? m' Hm j; destruct (decide (i = j)); simplify_map_eq.
  { by apply: discrete; rewrite -Hm lookup_insert_eq. }
  by apply: discrete; rewrite -Hm lookup_insert_ne.
Qed.
(* iris/algebra/gmap.v *)
Instance gmap_singleton_discrete i x :
  Discrete x → Discrete ({[ i := x ]} : gmap K A).
Proof. rewrite /singletonM /map_singleton. apply _. Qed.
(* iris/algebra/gmap.v *)
Lemma insert_idN n m i x :
  m !! i ≡{n}≡ Some x → <[i:=x]>m ≡{n}≡ m.
Proof. intros (y'&?&->)%dist_Some_inv_r'. by rewrite insert_id. Qed.
(* iris/algebra/gmap.v *)
Instance gmap_dom_ne n :
  Proper ((≡{n}@{gmap K A}≡) ==> (=)) dom.
Proof. intros m1 m2 Hm. apply set_eq=> k. by rewrite !elem_of_dom Hm. Qed.
(* iris/algebra/gmap.v *)
Instance map_seq_ne {SI : sidx} {A : ofe} start :
  NonExpansive (map_seq (M:=gmap nat A) start).
Proof.
  intros n l1 l2 Hl. revert start.
  induction Hl; intros; simpl; repeat (done || f_equiv).
Qed.
(* iris/algebra/gmap.v *)
Instance merge_ne {SI : sidx} `{Countable K} {A B C : ofe} n :
  Proper ((dist (A:=option A) n ==> dist (A:=option B) n ==> dist (A:=option C) n) ==>
          dist n ==> dist n ==> (≡{n}@{gmap K C}≡)) merge.
Proof.
  intros ?? Hf ?? Hm1 ?? Hm2 i. rewrite !lookup_merge.
  destruct (Hm1 i), (Hm2 i); try apply Hf; by constructor.
Qed.
(* iris/algebra/gmap.v *)
Instance union_with_ne {SI : sidx} `{Countable K} {A : ofe} n :
  Proper ((dist n ==> dist n ==> dist n) ==>
          dist n ==> dist n ==> dist n) (union_with (M:=gmap K A)).
Proof.
  intros ?? Hf ?? Hm1 ?? Hm2 i; apply (merge_ne _ _); auto.
  by do 2 destruct 1; first [apply Hf | constructor].
Qed.
(* iris/algebra/gmap.v *)
Instance map_fmap_ne {SI : sidx} `{Countable K} {A B : ofe} (f : A → B) n :
  Proper (dist n ==> dist n) f →
  Proper (dist n ==> (≡{n}@{gmap K B}≡)) (fmap f).
Proof. intros ? m m' ? k; rewrite !lookup_fmap. by repeat f_equiv. Qed.
(* iris/algebra/gmap.v *)
Instance map_zip_with_ne {SI : sidx}
    `{Countable K} {A B C : ofe} (f : A → B → C) n :
  Proper (dist n ==> dist n ==> dist n) f →
  Proper (dist n ==> dist n ==> dist n) (map_zip_with (M:=gmap K) f).
Proof.
  intros Hf m1 m1' Hm1 m2 m2' Hm2. apply merge_ne; try done.
  destruct 1; destruct 1; repeat f_equiv; constructor || done.
Qed.
(* iris/algebra/gmap.v *)
Instance gmap_union_ne {SI : sidx} `{Countable K} {A : ofe} :
  NonExpansive2 (union (A:=gmap K A)).
Proof. intros n. apply union_with_ne. by constructor. Qed.
(* iris/algebra/gmap.v *)
Instance gmap_disjoint_ne {SI : sidx} `{Countable K} {A : ofe} n :
  Proper (dist n ==> dist n ==> iff) (map_disjoint (M:=gmap K) (A:=A)).
Proof.
  intros m1 m1' Hm1 m2 m2' Hm2; split;
    intros Hm i; specialize (Hm i); by destruct (Hm1 i), (Hm2 i).
Qed.
(* iris/algebra/gmap.v *)
Lemma gmap_union_dist_eq {SI : sidx} `{Countable K} {A : ofe}
    (m m1 m2 : gmap K A) n :
  m ≡{n}≡ m1 ∪ m2 ↔ ∃ m1' m2', m = m1' ∪ m2' ∧ m1' ≡{n}≡ m1 ∧ m2' ≡{n}≡ m2.
Proof.
  split; last first.
  { by intros (m1'&m2'&->&<-&<-). }
  intros Hm.
  exists (filter (λ '(l,_), is_Some (m1 !! l)) m),
    (m2 ∩ m1 ∪ filter (λ '(l,_), is_Some (m2 !! l)) m).
  split_and!; [apply map_eq|..]; intros k; move: (Hm k);
    rewrite ?lookup_union ?lookup_intersection !map_lookup_filter;
    case _ : (m !! k)=> [x|] /=; case _ : (m1 !! k)=> [x1|] /=;
      case _ : (m2 !! k)=> [x2|] /=; by inversion 1.
Qed.
(* iris/algebra/gmap.v *)
Lemma big_opM_ne_2 {SI : sidx} {M : ofe} {o: M → M → M}
    `{!Monoid o u} `{Countable K} {A : ofe} (f g : K → A → M) m1 m2 n :
  m1 ≡{n}≡ m2 →
  (∀ k y1 y2,
    m1 !! k = Some y1 → m2 !! k = Some y2 → y1 ≡{n}≡ y2 → f k y1 ≡{n}≡ g k y2) →
  ([^o map] k ↦ y ∈ m1, f k y) ≡{n}≡ ([^o map] k ↦ y ∈ m2, g k y).
Proof.
  intros Hl Hf. apply big_opM_gen_proper_2; try (apply _ || done).
  { by intros ?? ->. }
  { apply monoid_ne. }
  intros k. assert (m1 !! k ≡{n}≡ m2 !! k) as Hlk by (by f_equiv).
  destruct (m1 !! k) eqn:?, (m2 !! k) eqn:?; inversion Hlk; naive_solver.
Qed.
(* iris/algebra/gmap.v *)
Instance gmap_unit_instance : Unit (gmap K A)
:= (∅ : gmap K A).
(* iris/algebra/gmap.v *)
Instance gmap_op_instance : Op (gmap K A)
:= merge op.
(* iris/algebra/gmap.v *)
Instance gmap_pcore_instance : PCore (gmap K A)
:= λ m, Some (omap pcore m).
(* iris/algebra/gmap.v *)
Instance gmap_valid_instance : Valid (gmap K A)
:= λ m, ∀ i, ✓ (m !! i).
(* iris/algebra/gmap.v *)
Instance gmap_validN_instance : ValidN (gmap K A)
:= λ n m, ∀ i, ✓{n} (m !! i).
(* iris/algebra/gmap.v *)
Lemma gmap_op m1 m2 : m1 ⋅ m2 = merge op m1 m2.
Proof. done. Qed.
(* iris/algebra/gmap.v *)
Lemma lookup_op m1 m2 i : (m1 ⋅ m2) !! i = m1 !! i ⋅ m2 !! i.
Proof. rewrite lookup_merge. by destruct (m1 !! i), (m2 !! i). Qed.
(* iris/algebra/gmap.v *)
Lemma lookup_core m i : core m !! i = core (m !! i).
Proof. by apply lookup_omap. Qed.
(* iris/algebra/gmap.v *)
Lemma lookup_includedN n (m1 m2 : gmap K A) : m1 ≼{n} m2 ↔ ∀ i, m1 !! i ≼{n} m2 !! i.
Proof.
  split; [by intros [m Hm] i; exists (m !! i); rewrite -lookup_op Hm|].
  revert m2. induction m1 as [|i x m Hi IH] using map_ind=> m2 Hm.
  { exists m2. by rewrite left_id. }
  destruct (IH (delete i m2)) as [m2' Hm2'].
  { intros j. move: (Hm j); destruct (decide (i = j)) as [->|].
    - intros _. rewrite Hi. apply: ucmra_unit_leastN.
    - rewrite lookup_insert_ne // lookup_delete_ne //. }
  destruct (Hm i) as [my Hi']; simplify_map_eq.
  exists (partial_alter (λ _, my) i m2')=>j; destruct (decide (i = j)) as [->|].
  - by rewrite Hi' lookup_op lookup_insert_eq lookup_partial_alter_eq.
  - move: (Hm2' j). by rewrite !lookup_op lookup_delete_ne //
      lookup_insert_ne // lookup_partial_alter_ne.
Qed.
(* iris/algebra/gmap.v *)
(* [m1 ≼ m2] is not equivalent to [∀ n, m1 ≼{n} m2],
so there is no good way to reuse the above proof. *)
Lemma lookup_included (m1 m2 : gmap K A) : m1 ≼ m2 ↔ ∀ i, m1 !! i ≼ m2 !! i.
Proof.
  split; [by intros [m Hm] i; exists (m !! i); rewrite -lookup_op Hm|].
  revert m2. induction m1 as [|i x m Hi IH] using map_ind=> m2 Hm.
  { exists m2. by rewrite left_id. }
  destruct (IH (delete i m2)) as [m2' Hm2'].
  { intros j. move: (Hm j); destruct (decide (i = j)) as [->|].
    - intros _. rewrite Hi. apply: ucmra_unit_least.
    - rewrite lookup_insert_ne // lookup_delete_ne //. }
  destruct (Hm i) as [my Hi']; simplify_map_eq.
  exists (partial_alter (λ _, my) i m2')=>j; destruct (decide (i = j)) as [->|].
  - by rewrite Hi' lookup_op lookup_insert_eq lookup_partial_alter_eq.
  - move: (Hm2' j). by rewrite !lookup_op lookup_delete_ne //
      lookup_insert_ne // lookup_partial_alter_ne.
Qed.