phanerozoic/Coq-Iris huggingface dataset:
(* iris/algebra/sts.v *)
Lemma sts_car_core_mono (x y : car sts) :
  ∃ z, ✓ x → ✓ y → x ## y → core (x ⋅ y) ≡ core x ⋅ z ∧ ✓ z ∧ core x ## z.
Proof.
  exists (core (x ⋅ y))=> ?? Hxy; split_and?.
  + destruct Hxy; constructor; unfold up_set; set_solver.
  + destruct Hxy; simpl;
      eauto using closed_up_set_empty, closed_up_empty with sts.
  + destruct Hxy; econstructor;
      repeat match goal with
      | |- context [ up_set ?S ?T ] =>
         unless (S ⊆ up_set S T) by done; pose proof (subseteq_up_set S T)
      | |- context [ up ?s ?T ] =>
         unless (s ∈ up s T) by done; pose proof (elem_of_up s T)
      end; auto with sts.
Qed.
(* iris/algebra/sts.v *)
(* The resource type for [sts]. *)
Record sts_res
:= StsRes {
  (** The underlying STS carrier element, storing the actual data. *)
  sts_car : car sts;
  (** Defines whether this element is valid. *)
  sts_valid : Prop;
  (** Valid elements must have a valid carrier element. *)
  sts_valid_prf : sts_valid → ✓ sts_car
}.
(* iris/algebra/sts.v *)
(* Setoid and OFE for [sts_res]. *)
Instance sts_equiv : Equiv sts_res
:= λ x y,
  (sts_valid x ↔ sts_valid y) ∧ (sts_valid x → sts_car x ≡ sts_car y).
(* iris/algebra/sts.v *)
Instance sts_equivalence : Equivalence (@equiv sts_res _).
Proof.
  split; unfold equiv, sts_equiv.
  - by intros [x px ?]; simpl.
  - intros [x px ?] [y py ?]; naive_solver.
  - intros [x px ?] [y py ?] [z pz ?] [? Hxy] [? Hyz]; simpl in *.
    split; [|intros; trans y]; tauto.
Qed.
(* iris/algebra/sts.v *)
Canonical sts_resO {SI : sidx} : ofe
:= discreteO sts_res.
(* iris/algebra/sts.v *)
(* RA for [sts_res]. *)
Instance sts_res_valid_instance : Valid sts_res
:= sts_valid.
(* iris/algebra/sts.v *)
Instance sts_res_pcore_instance : PCore sts_res := λ x,
  Some (StsRes (core (sts_car x)) (✓ x)).
Next Obligation.
  intros []; naive_solver eauto using sts_car_core_valid.
Qed.
(* iris/algebra/sts.v *)
Instance sts_res_op_instance : Op sts_res := λ x y,
  StsRes (sts_car x ⋅ sts_car y)
           (✓ x ∧ ✓ y ∧ sts_car x ## sts_car y).
Next Obligation.
  intros [] []; naive_solver eauto using sts_car_op_valid.
Qed.
(* iris/algebra/sts.v *)
Definition sts_res_ra_mixin : RAMixin sts_res.
Proof.
  apply ra_total_mixin; first eauto.
  - intros ??? [? Heq]; split; simpl; [|intros (?&?&?); by rewrite Heq].
    split; intros (?&?&?); split_and!;
      first [rewrite ?Heq; tauto|rewrite -?Heq; tauto|tauto].
  - by intros ?? [? Heq]; split; [done|]; simpl; intros ?; rewrite Heq.
  - intros ?? [??]; naive_solver.
  - intros [x px ?] [y py ?] [z pz ?]; split; simpl;
      [intuition eauto 2 using sts_car_disjoint_lr, sts_car_disjoint_rl
      |intuition eauto using sts_car_op_assoc, sts_car_disjoint_rl].
  - intros [x px ?] [y py ?]; split; naive_solver eauto using sts_car_op_comm.
  - intros [x px ?]; split;
      naive_solver eauto using sts_car_core_l, sts_car_core_disjoint_l.
  - intros [x px ?]; split; naive_solver eauto using sts_car_core_idemp.
  - intros [x px ?] [y py ?] [[z pz ?] [? Hy]]; simpl in *.
    destruct (sts_car_core_mono x z) as (z'&Hz').
    unshelve eexists (StsRes z' (px ∧ py ∧ pz)).
    { intros (?&?&?); apply Hz'; tauto. }
    split; simpl; first tauto.
    intros. rewrite Hy //. tauto.
  - by intros [x px ?] [y py ?] (?&?&?).
Qed.
(* iris/algebra/sts.v *)
Canonical sts_resR : cmra
:=
  discreteR sts_res sts_res_ra_mixin.
(* iris/algebra/sts.v *)
Instance sts_res_disrete_cmra : CmraDiscrete sts_resR.
Proof. apply discrete_cmra_discrete. Qed.
(* iris/algebra/sts.v *)
Instance sts_res_cmra_total : CmraTotal sts_resR.
Proof. rewrite /CmraTotal; eauto. Qed.
(* iris/algebra/sts.v *)
Definition to_sts_res (x : car sts) : sts_res
:=
  @StsRes x (valid x) id.
(* iris/algebra/sts.v *)
Instance to_sts_res_proper : Proper ((≡) ==> (≡)) to_sts_res.
Proof. by intros x1 x2 Hx; split; rewrite /= Hx. Qed.
(* iris/algebra/sts.v *)
Lemma to_sts_res_op a b :
  (✓ (a ⋅ b) → ✓ a ∧ ✓ b ∧ a ## b) →
  to_sts_res (a ⋅ b) ≡ to_sts_res a ⋅ to_sts_res b.
Proof. split; naive_solver eauto using sts_car_op_valid. Qed.
(* iris/algebra/sts.v *)
Definition sts_auth (s : sts.state sts) (T : sts.tokens sts) : sts_resR sts
:=
    to_sts_res (sts.auth s T).
(* iris/algebra/sts.v *)
Definition sts_frag (S : sts.states sts) (T : sts.tokens sts) : sts_resR sts
:=
    to_sts_res (sts.frag S T).
(* iris/algebra/sts.v *)
Definition sts_frag_up (s : sts.state sts) (T : sts.tokens sts) : sts_resR sts
:=
    sts_frag (sts.up s T) T.
(* iris/algebra/sts.v *)
Instance : Params (@sts_auth) 3
:= {}.
(* iris/algebra/sts.v *)
Instance : Params (@sts_frag) 2
:= {}.
(* iris/algebra/sts.v *)
Instance : Params (@sts_frag_up) 3
:= {}.
(* iris/algebra/sts.v *)
(* Setoids *)
Instance sts_auth_proper s : Proper ((≡) ==> (≡)) (sts_auth s).
Proof. solve_proper. Qed.
(* iris/algebra/sts.v *)
Instance sts_frag_proper : Proper ((≡) ==> (≡) ==> (≡)) (@sts_frag SI sts).
Proof. solve_proper. Qed.
(* iris/algebra/sts.v *)
Instance sts_frag_up_proper s : Proper ((≡) ==> (≡)) (sts_frag_up s).
Proof. solve_proper. Qed.
(* iris/algebra/sts.v *)
(* Validity *)
Lemma sts_auth_valid s T : ✓ sts_auth s T ↔ tok s ## T.
Proof. done. Qed.
(* iris/algebra/sts.v *)
Lemma sts_frag_valid S T : ✓ sts_frag S T ↔ closed S T ∧ ∃ s, s ∈ S.
Proof. done. Qed.
(* iris/algebra/sts.v *)
Lemma sts_frag_up_valid s T : ✓ sts_frag_up s T ↔ tok s ## T.
Proof.
  split.
  - move=>/sts_frag_valid [H _]. apply H, elem_of_up.
  - intros. apply sts_frag_valid; split.
    + by apply closed_up.
    + set_solver+.
Qed.
(* iris/algebra/sts.v *)
Lemma sts_auth_frag_valid_inv s S T1 T2 :
  ✓ (sts_auth s T1 ⋅ sts_frag S T2) → s ∈ S.
Proof. by intros (?&?&Hdisj); inversion Hdisj. Qed.
(* iris/algebra/sts.v *)
(* Op *)
Lemma sts_auth_frag_op s S T :
  s ∈ S → closed S T → sts_auth s ∅ ⋅ sts_frag S T ≡ sts_auth s T.
Proof.
  intros; split; [split|constructor; set_solver]; simpl.
  - intros (?&?&?); by apply closed_disjoint with S.
  - intros; split_and?; last constructor; set_solver.
Qed.
(* iris/algebra/sts.v *)
Lemma sts_auth_frag_up_op s T :
  sts_auth s ∅ ⋅ sts_frag_up s T ≡ sts_auth s T.
Proof.
  intros; split; [split|constructor; set_solver]; simpl.
  - intros (?&[??]&?). by apply closed_disjoint with (up s T), elem_of_up.
  - intros; split_and?.
    + set_solver+.
    + by apply closed_up.
    + exists s. set_solver.
    + constructor; last set_solver. apply elem_of_up.
Qed.
(* iris/algebra/sts.v *)
Lemma sts_frag_op S1 S2 T1 T2 :
  T1 ## T2 → sts.closed S1 T1 → sts.closed S2 T2 →
  sts_frag (S1 ∩ S2) (T1 ∪ T2) ≡ sts_frag S1 T1 ⋅ sts_frag S2 T2.
Proof.
  intros HT HS1 HS2. rewrite /sts_frag -to_sts_res_op //.
  move=>/=[?[? ?]]. split_and!; [set_solver..|constructor; set_solver].
Qed.
(* iris/algebra/sts.v *)
(* Frame preserving updates *)
Lemma sts_update_auth s1 s2 T1 T2 :
  steps (s1,T1) (s2,T2) → sts_auth s1 T1 ~~> sts_auth s2 T2.
Proof.
  intros ?. apply cmra_discrete_total_update.
  intros [x x_val Hx_val]; simpl. intros (Htok & Hval & Hdisj).
  specialize (Hx_val Hval).
  inversion Hdisj as [|? S ? Tf|]; simplify_eq/=; destruct_and?.
  destruct (steps_closed s1 s2 T1 T2 S Tf) as (?&?&?); auto; [].
  repeat (done || constructor).
Qed.
(* iris/algebra/sts.v *)
Lemma sts_update_frag S1 S2 T1 T2 :
  (closed S1 T1 → closed S2 T2 ∧ S1 ⊆ S2 ∧ T2 ⊆ T1) → sts_frag S1 T1 ~~> sts_frag S2 T2.
Proof.
  rewrite /sts_frag=> HC HS HT. apply cmra_discrete_total_update.
  intros [x x_val Hx_val]; simpl. intros (Htok & Hval & Hdisj).
  specialize (Hx_val Hval).
  inversion Hdisj as [|? S ? Tf|]; simplify_eq/=;
    (destruct HC as (? & ? & ?); first by destruct_and?).
  - split_and!; first done.
    + set_solver.
    + done.
    + constructor; set_solver.
  - split_and!; first done.
    + set_solver.
    + done.
    + constructor; set_solver.
Qed.
(* iris/algebra/sts.v *)
Lemma sts_update_frag_up s1 S2 T1 T2 :
  (tok s1 ## T1 → closed S2 T2) → s1 ∈ S2 → T2 ⊆ T1 → sts_frag_up s1 T1 ~~> sts_frag S2 T2.
Proof.
  intros HC ? HT; apply sts_update_frag. intros HC1; split; last split; eauto using closed_steps.
  - eapply HC, HC1, elem_of_up.
  - rewrite <-HT. eapply up_subseteq; last done. apply HC, HC1, elem_of_up.
Qed.
(* iris/algebra/sts.v *)
Lemma sts_up_set_intersection S1 Sf Tf :
  closed Sf Tf → S1 ∩ Sf ≡ S1 ∩ up_set (S1 ∩ Sf) Tf.
Proof.
  intros Hclf. apply (anti_symm (⊆)).
  - move=>s [HS1 HSf]. split.
    + by apply HS1.
    + by apply subseteq_up_set.
  - move=>s [HS1 [s' [/elem_of_PropSet Hsup Hs']]]. split; first done.
    eapply closed_steps, Hsup; first done. set_solver +Hs'.
Qed.
(* iris/algebra/sts.v *)
Instance sts_frag_core_id S : CoreId (sts_frag S ∅).
Proof.
  constructor; split=> //= [[??]].
  (* FIXME: rewriting with [sts.up_closed] for some reason fails here. *)
  f_equiv. by rewrite sts.up_closed.
Qed.
(* iris/algebra/sts.v *)
Structure stsT
:= Sts {
  state : Type;
  prim_step : relation state;
}.
(* iris/algebra/sts.v *)
Definition stsT_token
:= Empty_set.
(* iris/algebra/sts.v *)
Definition stsT_tok {sts : stsT} (_ : state sts) : propset stsT_token
:= ∅.
(* iris/algebra/sts.v *)
Canonical sts_notok (sts : stsT) : sts.stsT
:=
  sts.Sts (@prim_step sts) stsT_tok.
(* iris/algebra/sts.v *)
Coercion sts_notok.sts_notok : sts_notok.stsT >-> sts.stsT.
(* iris/algebra/sts.v *)
Notation prim_steps
:= (rtc prim_step).
(* iris/algebra/sts.v *)
Lemma sts_step s1 s2 : prim_step s1 s2 → sts.step (s1, ∅) (s2, ∅).
Proof. intros. split; set_solver. Qed.
(* iris/algebra/sts.v *)
Lemma sts_steps s1 s2 : prim_steps s1 s2 → sts.steps (s1, ∅) (s2, ∅).
Proof. induction 1; eauto using sts_step, rtc_refl, rtc_l. Qed.
(* iris/algebra/sts.v *)
Lemma frame_prim_step T s1 s2 : sts.frame_step T s1 s2 → prim_step s1 s2.
Proof. inversion 1 as [??? Hstep]. by inversion_clear Hstep. Qed.
(* iris/algebra/sts.v *)
Lemma prim_frame_step T s1 s2 : prim_step s1 s2 → sts.frame_step T s1 s2.
Proof.
    intros Hstep. apply sts.Frame_step with ∅ ∅; first set_solver.
    by apply sts_step.
  Qed.
(* iris/algebra/sts.v *)
Lemma mk_closed S :
    (∀ s1 s2, s1 ∈ S → prim_step s1 s2 → s2 ∈ S) → sts.closed S ∅.
Proof. intros ?. constructor; [by set_solver|eauto using frame_prim_step]. Qed.
(* iris/algebra/sts.v *)
Notation sts_notokT
:= sts_notok.stsT.
(* iris/algebra/sts.v *)
Notation Sts_NoTok
:= sts_notok.Sts.
(* iris/algebra/sts.v *)
Lemma sts_notok_update_auth s1 s2 :
    rtc prim_step s1 s2 → sts_auth s1 ∅ ~~> sts_auth s2 ∅.
Proof. intros. by apply sts_update_auth, sts_steps. Qed.
(* iris/algebra/ufrac.v *)
(* Since the standard (0,1] fractional camera [frac] is used more often, we
define [ufrac] through a [Definition] instead of a [Notation]. That way, Coq
infers the [frac] camera by default when using the [Qp] type. *)
Definition ufrac
:= Qp.
(* iris/algebra/ufrac.v *)
Canonical ufracO
:= leibnizO ufrac.
(* iris/algebra/ufrac.v *)
Instance ufrac_valid_instance : Valid ufrac
:= λ x, True.
(* iris/algebra/ufrac.v *)
Instance ufrac_pcore_instance : PCore ufrac
:= λ _, None.
(* iris/algebra/ufrac.v *)
Instance ufrac_op_instance : Op ufrac
:= λ x y, (x + y)%Qp.
(* iris/algebra/ufrac.v *)
Lemma ufrac_op p q : p ⋅ q = (p + q)%Qp.
Proof. done. Qed.
(* iris/algebra/ufrac.v *)
Lemma ufrac_included p q : p ≼ q ↔ (p < q)%Qp.
Proof. by rewrite Qp.lt_sum. Qed.
(* iris/algebra/ufrac.v *)
Corollary ufrac_included_weak p q : p ≼ q → (p ≤ q)%Qp.
Proof. rewrite ufrac_included. apply Qp.lt_le_incl. Qed.
(* iris/algebra/ufrac.v *)
Definition ufrac_ra_mixin : RAMixin ufrac.
Proof. split; try apply _; try done. Qed.
(* iris/algebra/ufrac.v *)
Canonical ufracR
:= discreteR ufrac ufrac_ra_mixin.
(* iris/algebra/ufrac.v *)
Instance ufrac_cmra_discrete : CmraDiscrete ufracR.
Proof. apply discrete_cmra_discrete. Qed.
(* iris/algebra/ufrac.v *)
Instance ufrac_cancelable q : Cancelable q.
Proof. intros n p1 p2 _. apply (inj (Qp.add q)). Qed.
(* iris/algebra/ufrac.v *)
Instance ufrac_id_free q : IdFree q.
Proof. intros p _. apply Qp.add_id_free. Qed.
(* iris/algebra/ufrac.v *)
Instance is_op_ufrac q : IsOp' q (q/2)%Qp (q/2)%Qp.
Proof. by rewrite /IsOp' /IsOp ufrac_op Qp.div_2. Qed.
(* iris/algebra/updates.v *)
(* This quantifies over [option A] for the frame.  That is necessary to
   make the following hold:
     x ~~> P → Some c ~~> Some P *)
Definition cmra_updateP {SI : sidx} {A : cmra} (x : A) (P : A → Prop)
:= ∀ n mz,
  ✓{n} (x ⋅? mz) → ∃ y, P y ∧ ✓{n} (y ⋅? mz).
(* iris/algebra/updates.v *)
Instance : Params (@cmra_updateP) 1
:= {}.
(* iris/algebra/updates.v *)
Definition cmra_update {SI : sidx} {A : cmra} (x y : A)
:= ∀ n mz,
  ✓{n} (x ⋅? mz) → ✓{n} (y ⋅? mz).
(* iris/algebra/updates.v *)
Instance : Params (@cmra_update) 1
:= {}.
(* iris/algebra/updates.v *)
Instance cmra_updateP_proper :
  Proper ((≡) ==> pointwise_relation _ iff ==> iff) (@cmra_updateP SI A).
Proof.
  rewrite /pointwise_relation /cmra_updateP=> x x' Hx P P' HP;
    split=> ? n mz; setoid_subst; naive_solver.
Qed.
(* iris/algebra/updates.v *)
Instance cmra_update_proper :
  Proper ((≡) ==> (≡) ==> iff) (@cmra_update SI A).
Proof.
  rewrite /cmra_update=> x x' Hx y y' Hy; split=> ? n mz ?; setoid_subst; auto.
Qed.
(* iris/algebra/updates.v *)
Lemma cmra_update_updateP x y : x ~~> y ↔ x ~~>: (y =.).
Proof. split=> Hup n z ?; eauto. destruct (Hup n z) as (?&<-&?); auto. Qed.
(* iris/algebra/updates.v *)
Lemma cmra_updateP_id (P : A → Prop) x : P x → x ~~>: P.
Proof. intros ? n mz ?; eauto. Qed.
(* iris/algebra/updates.v *)
Lemma cmra_updateP_compose (P Q : A → Prop) x :
  x ~~>: P → (∀ y, P y → y ~~>: Q) → x ~~>: Q.
Proof. intros Hx Hy n mz ?. destruct (Hx n mz) as (y&?&?); naive_solver. Qed.
(* iris/algebra/updates.v *)
Lemma cmra_updateP_compose_l (Q : A → Prop) x y : x ~~> y → y ~~>: Q → x ~~>: Q.
Proof.
  rewrite cmra_update_updateP.
  intros; apply cmra_updateP_compose with (y =.); naive_solver.
Qed.
(* iris/algebra/updates.v *)
Lemma cmra_updateP_weaken (P Q : A → Prop) x :
  x ~~>: P → (∀ y, P y → Q y) → x ~~>: Q.
Proof. eauto using cmra_updateP_compose, cmra_updateP_id. Qed.
(* iris/algebra/updates.v *)
Lemma cmra_update_exclusive `{!Exclusive x} y:
  ✓ y → x ~~> y.
Proof. move=>??[z|]=>[/exclusiveN_l[]|_]. by apply cmra_valid_validN. Qed.
(* iris/algebra/updates.v *)
(* We set this rewrite relation's cost above the stdlib's
  ([impl], [iff], [eq], ...) and [≡] but below [⊑].
  [eq] (at 100) < [≡] (at 150) < [cmra_update] (at 170) < [⊑] (at 200) *)
Instance cmra_update_rewrite_relation :
  RewriteRelation (@cmra_update SI A) | 170
:= {}.
(* iris/algebra/updates.v *)
Instance cmra_update_preorder : PreOrder (@cmra_update SI A).
Proof.
  split.
  - intros x. by apply cmra_update_updateP, cmra_updateP_id.
  - intros x y z. rewrite !cmra_update_updateP.
    eauto using cmra_updateP_compose with subst.
Qed.
(* iris/algebra/updates.v *)
Instance cmra_update_proper_update :
  Proper (flip cmra_update ==> cmra_update ==> impl) (@cmra_update SI A).
Proof.
  intros x1 x2 Hx y1 y2 Hy ?. etrans; [apply Hx|]. by etrans; [|apply Hy].
Qed.
(* iris/algebra/updates.v *)
Instance cmra_update_flip_proper_update :
  Proper (cmra_update ==> flip cmra_update ==> flip impl) (@cmra_update SI A).
Proof.
  intros x1 x2 Hx y1 y2 Hy ?. etrans; [apply Hx|]. by etrans; [|apply Hy].
Qed.
(* iris/algebra/updates.v *)
Lemma cmra_updateP_op (P1 P2 Q : A → Prop) x1 x2 :
  x1 ~~>: P1 → x2 ~~>: P2 → (∀ y1 y2, P1 y1 → P2 y2 → Q (y1 ⋅ y2)) →
  x1 ⋅ x2 ~~>: Q.
Proof.
  intros Hx1 Hx2 Hy n mz ?.
  destruct (Hx1 n (Some (x2 ⋅? mz))) as (y1&?&?).
  { by rewrite /= -cmra_op_opM_assoc. }
  destruct (Hx2 n (Some (y1 ⋅? mz))) as (y2&?&?).
  { by rewrite /= -cmra_op_opM_assoc (comm _ x2) cmra_op_opM_assoc. }
  exists (y1 ⋅ y2); split; last rewrite (comm _ y1) cmra_op_opM_assoc; auto.
Qed.
(* iris/algebra/updates.v *)
Lemma cmra_updateP_op' (P1 P2 : A → Prop) x1 x2 :
  x1 ~~>: P1 → x2 ~~>: P2 →
  x1 ⋅ x2 ~~>: λ y, ∃ y1 y2, y = y1 ⋅ y2 ∧ P1 y1 ∧ P2 y2.
Proof. eauto 10 using cmra_updateP_op. Qed.
(* iris/algebra/updates.v *)
Lemma cmra_update_op x1 x2 y1 y2 : x1 ~~> y1 → x2 ~~> y2 → x1 ⋅ x2 ~~> y1 ⋅ y2.
Proof.
  rewrite !cmra_update_updateP; eauto using cmra_updateP_op with congruence.
Qed.
(* iris/algebra/updates.v *)
Instance cmra_update_op_proper :
  Proper (cmra_update ==> cmra_update ==> cmra_update) (op (A:=A)).
Proof. intros x1 x2 Hx y1 y2 Hy. by apply cmra_update_op. Qed.
(* iris/algebra/updates.v *)
Instance cmra_update_op_flip_proper :
  Proper (flip cmra_update ==> flip cmra_update ==> flip cmra_update) (op (A:=A)).
Proof. intros x1 x2 Hx y1 y2 Hy. by apply cmra_update_op. Qed.
(* iris/algebra/updates.v *)
Lemma cmra_update_op_l x y : x ⋅ y ~~> x.
Proof. intros n mz. rewrite comm cmra_op_opM_assoc. apply cmra_validN_op_r. Qed.
(* iris/algebra/updates.v *)
Lemma cmra_update_op_r x y : x ⋅ y ~~> y.
Proof. rewrite comm. apply cmra_update_op_l. Qed.
(* iris/algebra/updates.v *)
Lemma cmra_update_included x y : x ≼ y → y ~~> x.
Proof. intros [z ->]. apply cmra_update_op_l. Qed.
(* iris/algebra/updates.v *)
Lemma cmra_update_valid0 x y : (✓{0ᵢ} x → x ~~> y) → x ~~> y.
Proof.
  intros H n mz Hmz. apply H, Hmz.
  apply (cmra_validN_le n), SIdx.le_0_l.
  destruct mz.
  - eapply cmra_validN_op_l, Hmz.
  - apply Hmz.
Qed.
(* iris/algebra/updates.v *)
(* ** Frame preserving updates for total and discete CMRAs *)
Lemma cmra_total_updateP `{!CmraTotal A} x (P : A → Prop) :
  x ~~>: P ↔ ∀ n z, ✓{n} (x ⋅ z) → ∃ y, P y ∧ ✓{n} (y ⋅ z).
Proof.
  split=> Hup; [intros n z; apply (Hup n (Some z))|].
  intros n [z|] ?; simpl; [by apply Hup|].
  destruct (Hup n (core x)) as (y&?&?); first by rewrite cmra_core_r.
  eauto using cmra_validN_op_l.
Qed.
(* iris/algebra/updates.v *)
Lemma cmra_total_update `{!CmraTotal A} x y :
   x ~~> y ↔ ∀ n z, ✓{n} (x ⋅ z) → ✓{n} (y ⋅ z).
Proof. rewrite cmra_update_updateP cmra_total_updateP. naive_solver. Qed.
(* iris/algebra/updates.v *)
Lemma cmra_discrete_updateP `{!CmraDiscrete A} (x : A) (P : A → Prop) :
  x ~~>: P ↔ ∀ mz, ✓ (x ⋅? mz) → ∃ y, P y ∧ ✓ (y ⋅? mz).
Proof.
  unfold cmra_updateP. setoid_rewrite <-cmra_discrete_valid_iff.
  pose 0ᵢ. naive_solver.
Qed.
(* iris/algebra/updates.v *)
Lemma cmra_discrete_update `{!CmraDiscrete A} (x y : A) :
  x ~~> y ↔ ∀ mz, ✓ (x ⋅? mz) → ✓ (y ⋅? mz).
Proof.
  unfold cmra_update. setoid_rewrite <-cmra_discrete_valid_iff.
  pose 0ᵢ. naive_solver.
Qed.
(* iris/algebra/updates.v *)
Lemma cmra_discrete_total_updateP `{!CmraDiscrete A, !CmraTotal A}
    (x : A) (P : A → Prop) :
  x ~~>: P ↔ ∀ z, ✓ (x ⋅ z) → ∃ y, P y ∧ ✓ (y ⋅ z).
Proof.
  rewrite cmra_total_updateP; setoid_rewrite <-cmra_discrete_valid_iff.
  pose 0ᵢ. naive_solver.
Qed.
(* iris/algebra/updates.v *)
Lemma cmra_discrete_total_update `{!CmraDiscrete A, !CmraTotal A} (x y : A) :
  x ~~> y ↔ ∀ z, ✓ (x ⋅ z) → ✓ (y ⋅ z).
Proof.
  rewrite cmra_total_update; setoid_rewrite <-cmra_discrete_valid_iff.
  pose 0ᵢ. naive_solver.
Qed.
(* iris/algebra/updates.v *)
Lemma cmra_transport_updateP (P : A → Prop) (Q : B → Prop) x :
    x ~~>: P → (∀ y, P y → Q (T y)) → T x ~~>: Q.
Proof. destruct H; eauto using cmra_updateP_weaken. Qed.
(* iris/algebra/updates.v *)
Lemma cmra_transport_updateP' (P : A → Prop) x :
    x ~~>: P → T x ~~>: λ y, ∃ y', y = cmra_transport H y' ∧ P y'.
Proof. eauto using cmra_transport_updateP. Qed.
(* iris/algebra/updates.v *)
Lemma iso_cmra_updateP (P : B → Prop) (Q : A → Prop) y
      (gf : ∀ x, g (f x) ≡ x)
      (g_op : ∀ y1 y2, g (y1 ⋅ y2) ≡ g y1 ⋅ g y2)
      (g_validN : ∀ n y, ✓{n} (g y) ↔ ✓{n} y) :
    y ~~>: P →
    (∀ y', P y' → Q (g y')) →
    g y ~~>: Q.
Proof.
    intros Hup Hx n mz Hmz.
    destruct (Hup n (f <$> mz)) as (y'&HPy'&Hy'%g_validN).
    { apply g_validN. destruct mz as [z|]; simpl in *; [|done].
      by rewrite g_op gf. }
    exists (g y'); split; [by eauto|].
    destruct mz as [z|]; simpl in *; [|done].
    revert Hy'. by rewrite g_op gf.
  Qed.
(* iris/algebra/updates.v *)
Lemma iso_cmra_updateP' (P : B → Prop) y
      (gf : ∀ x, g (f x) ≡ x)
      (g_op : ∀ y1 y2, g (y1 ⋅ y2) ≡ g y1 ⋅ g y2)
      (g_validN : ∀ n y, ✓{n} (g y) ↔ ✓{n} y) :
    y ~~>: P →
    g y ~~>: λ x, ∃ y, x = g y ∧ P y.
Proof. eauto using iso_cmra_updateP. Qed.
(* iris/algebra/updates.v *)
(* This lemma shows that if [f] maps non-deterministic updates from [B] to [A]
  (i.e., [cmra_updateP] / [~~>:]), then [f] also maps deterministic updates from
  [B] to [A] (i.e., [cmra_update] / [~~>]) *)
Lemma cmra_update_lift_updateP (f : B → A) b b' :
    (∀ P, b ~~>: P → f b ~~>: λ a', ∃ b', a' = f b' ∧ P b') →
    b ~~> b' →
    f b ~~> f b'.
Proof.
    intros Hgen Hupd.
    eapply cmra_update_updateP, cmra_updateP_weaken.
    { eapply Hgen, cmra_update_updateP, Hupd. }
    naive_solver.
  Qed.
(* iris/algebra/updates.v *)
Lemma prod_updateP P1 P2 (Q : A * B → Prop) x :
    x.1 ~~>: P1 → x.2 ~~>: P2 → (∀ a b, P1 a → P2 b → Q (a,b)) → x ~~>: Q.
Proof.
    intros Hx1 Hx2 HP n mz [??]; simpl in *.
    destruct (Hx1 n (fst <$> mz)) as (a&?&?); first by destruct mz.
    destruct (Hx2 n (snd <$> mz)) as (b&?&?); first by destruct mz.
    exists (a,b); repeat split; destruct mz; auto.
  Qed.
(* iris/algebra/updates.v *)
Lemma prod_updateP' P1 P2 x :
    x.1 ~~>: P1 → x.2 ~~>: P2 → x ~~>: λ y, P1 (y.1) ∧ P2 (y.2).
Proof. eauto using prod_updateP. Qed.
(* iris/algebra/updates.v *)
Lemma prod_update x y : x.1 ~~> y.1 → x.2 ~~> y.2 → x ~~> y.
Proof.
    rewrite !cmra_update_updateP.
    destruct x, y; eauto using prod_updateP with subst.
  Qed.
(* iris/algebra/updates.v *)
Lemma option_updateP (P : A → Prop) (Q : option A → Prop) x :
    x ~~>: P → (∀ y, P y → Q (Some y)) → Some x ~~>: Q.
Proof.
    intros Hx Hy; apply cmra_total_updateP=> n [y|] ?.
    { destruct (Hx n (Some y)) as (y'&?&?); auto. exists (Some y'); auto. }
    destruct (Hx n None) as (y'&?&?); rewrite ?cmra_core_r; auto.
    by exists (Some y'); auto.
  Qed.
(* iris/algebra/updates.v *)
Lemma option_updateP' (P : A → Prop) x :
    x ~~>: P → Some x ~~>: from_option P False.
Proof. eauto using option_updateP. Qed.
(* iris/algebra/updates.v *)
Lemma option_update x y : x ~~> y → Some x ~~> Some y.
Proof. rewrite !cmra_update_updateP; eauto using option_updateP with subst. Qed.
(* iris/algebra/vector.v *)
Instance vec_equiv m : Equiv (vec A m)
:= equiv (A:=list A).
(* iris/algebra/vector.v *)
Instance vec_dist m : Dist (vec A m)
:= dist (A:=list A).
(* iris/algebra/vector.v *)
Definition vec_ofe_mixin m : OfeMixin (vec A m).
Proof. by apply (iso_ofe_mixin vec_to_list). Qed.
(* iris/algebra/vector.v *)
Canonical vecO m : ofe
:= Ofe (vec A m) (vec_ofe_mixin m).
(* iris/algebra/vector.v *)
Instance list_cofe `{!Cofe A} m : Cofe (vecO m).
Proof.
    apply: (iso_cofe_subtype (λ l : list A, length l = m)
      (λ l, eq_rect _ (vec A) (list_to_vec l) m) vec_to_list)=> //.
    - intros v []. by rewrite /= vec_to_list_to_vec.
    - intros c. by rewrite (conv_compl 0ᵢ (chain_map _ c)) /= length_vec_to_list.
    - intros n Hn c.
      rewrite (conv_lbcompl Hn (bchain_map _ c) (SIdx.limit_lt_0 _ Hn)) /=.
      by rewrite length_vec_to_list.
  Qed.
(* iris/algebra/vector.v *)
Instance vnil_discrete : Discrete (@vnil A).
Proof. intros v _. by inv_vec v. Qed.
(* iris/algebra/vector.v *)
Instance vcons_discrete n x (v : vec A n) :
    Discrete x → Discrete v → Discrete (x ::: v).
Proof.
    intros ?? v' ?. inv_vec v'=>x' v'. inversion_clear 1.
    constructor.
    - by apply: discrete.
    - change (v ≡ v'). by apply: discrete.
  Qed.
(* iris/algebra/vector.v *)
Instance vec_ofe_discrete m : OfeDiscrete A → OfeDiscrete (vecO m).
Proof. intros ? v. induction v; apply _. Qed.
(* iris/algebra/vector.v *)
Instance vcons_ne n :
    Proper (dist n ==> forall_relation (λ x, dist n ==> dist n)) (@vcons A).
Proof. by constructor. Qed.
(* iris/algebra/vector.v *)
Instance vcons_proper :
    Proper (equiv ==> forall_relation (λ x, equiv ==> equiv)) (@vcons A).
Proof. by constructor. Qed.
(* iris/algebra/vector.v *)
Instance vlookup_ne n m :
    Proper (dist n ==> eq ==> dist n) (@Vector.nth A m).
Proof.
    intros v. induction v as [|x m v IH]; intros v'; inv_vec v'.
    - intros _ x. inv_fin x.
    - intros x' v' EQ i ? <-. inversion_clear EQ. inv_fin i=> // i. by apply IH.
  Qed.
(* iris/algebra/vector.v *)
Instance vlookup_proper m :
    Proper (equiv ==> eq ==> equiv) (@Vector.nth A m).
Proof.
    intros v v' ? x x' ->. apply equiv_dist=> n. f_equiv. by apply equiv_dist.
  Qed.
(* iris/algebra/vector.v *)
Instance vec_to_list_ne m : NonExpansive (@vec_to_list A m).
Proof. by intros v v'. Qed.