phanerozoic/Coq-Iris huggingface dataset:
(* iris/base_logic/bi.v *)
Canonical uPredI (M : ucmra) : bi
:=
  {| bi_ofe_mixin := ofe_mixin_of (uPred M);
     bi_bi_mixin := uPred_bi_mixin M;
     bi_bi_later_mixin := uPred_bi_later_mixin M;
     bi_bi_persistently_mixin := uPred_bi_persistently_mixin M |}.
(* iris/base_logic/bi.v *)
Lemma uPred_sbi_mixin M : SbiMixin (uPredI M) uPred_si_pure uPred_si_emp_valid.
Proof.
  split.
  - exact: si_pure_ne.
  - exact: si_emp_valid_ne.
  - exact: si_pure_mono.
  - exact: si_emp_valid_mono.
  - exact: si_emp_valid_si_pure.
  - exact: si_pure_si_emp_valid.
  - exact: si_pure_impl_2.
  - exact: @si_pure_forall_2.
  - exact: persistently_impl_si_pure.
  - exact: si_pure_later.
  - (* Absorbing (<si_pure> Pi) (ADMISSIBLE) *)
    intros Pi. apply True_sep_2.
  - exact: @si_emp_valid_later_1.
  - (* <si_emp_valid> P -∗ <si_emp_valid> <affine> P (ADMISSIBLE) *)
    intros P. apply si_emp_valid_mono, and_intro; [|done].
    apply bi.True_intro.
Qed.
(* iris/base_logic/bi.v *)
Lemma uPred_sbi_prop_ext_mixin M : SbiPropExtMixin (uPredI M) uPred_si_emp_valid.
Proof. apply sbi_prop_ext_mixin. apply prop_ext_2. Qed.
(* iris/base_logic/bi.v *)
Instance uPred_sbi M : Sbi (uPredI M)
:=
  {| sbi_sbi_mixin := uPred_sbi_mixin M;
     sbi_sbi_prop_ext_mixin := uPred_sbi_prop_ext_mixin M |}.
(* iris/base_logic/bi.v *)
Lemma uPred_bupd_mixin M : BiBUpdMixin (uPredI M) uPred_bupd.
Proof.
  split.
  - exact: bupd_ne.
  - exact: bupd_intro.
  - exact: bupd_mono.
  - exact: bupd_trans.
  - exact: bupd_frame_r.
Qed.
(* iris/base_logic/bi.v *)
Instance uPred_bi_bupd M : BiBUpd (uPredI M)
:=
  {| bi_bupd_mixin := uPred_bupd_mixin M |}.
(* iris/base_logic/bi.v *)
(* extra BI instances *)
Instance uPred_affine M : BiAffine (uPredI M) | 0.
Proof. intros P. exact: bi.pure_intro. Qed.
(* iris/base_logic/bi.v *)
Instance uPred_persistently_forall M : BiPersistentlyForall (uPredI M).
Proof. exact: @persistently_forall_2. Qed.
(* iris/base_logic/bi.v *)
Instance uPred_pure_forall M : BiPureForall (uPredI M).
Proof.
  intros A φ. etrans; [apply si_pure_forall_2|].
  apply si_pure_mono, pure_forall_2.
Qed.
(* iris/base_logic/bi.v *)
Instance uPred_later_contractive {M} : BiLaterContractive (uPredI M).
Proof. exact: @later_contractive. Qed.
(* iris/base_logic/bi.v *)
Instance uPred_sbi_emp_valid_exist {M} : SbiEmpValidExist (uPredI M).
Proof. exact: @si_emp_valid_exist_1. Qed.
(* iris/base_logic/bi.v *)
Instance uPred_bi_bupd_sbi M : BiBUpdSbi (uPredI M).
Proof. exact: bupd_si_pure. Qed.
(* iris/base_logic/bi.v *)
(* Force implicit argument M *)
Notation "P ⊢ Q"
:= (bi_entails (PROP:=uPredI M) P%I Q%I).
(* iris/base_logic/bi.v *)
Notation "P ⊣⊢ Q"
:= (equiv (A:=uPredI M) P%I Q%I).
(* iris/base_logic/bi.v *)
Instance ownM_ne : NonExpansive (@uPred_ownM M)
:= uPred_primitive.ownM_ne.
(* iris/base_logic/bi.v *)
(* Re-exporting primitive lemmas that are not in any interface *)
Lemma ownM_valid (a : M) : uPred_ownM a ⊢ ✓ a.
Proof. exact: uPred_primitive.ownM_valid. Qed.
(* iris/base_logic/bi.v *)
Lemma ownM_op (a1 a2 : M) :
    uPred_ownM (a1 ⋅ a2) ⊣⊢ uPred_ownM a1 ∗ uPred_ownM a2.
Proof. exact: uPred_primitive.ownM_op. Qed.
(* iris/base_logic/bi.v *)
Lemma persistently_ownM_core (a : M) : uPred_ownM a ⊢ <pers> uPred_ownM (core a).
Proof. exact: uPred_primitive.persistently_ownM_core. Qed.
(* iris/base_logic/bi.v *)
Lemma ownM_unit P : P ⊢ uPred_ownM ε.
Proof. exact: uPred_primitive.ownM_unit. Qed.
(* iris/base_logic/bi.v *)
Lemma later_ownM a : ▷ uPred_ownM a ⊢ ∃ b, uPred_ownM b ∧ ▷ (a ≡ b).
Proof. exact: uPred_primitive.later_ownM. Qed.
(* iris/base_logic/bi.v *)
Lemma bupd_ownM_updateP x (Φ : M → Prop) :
    x ~~>: Φ → uPred_ownM x ⊢ |==> ∃ y, ⌜Φ y⌝ ∧ uPred_ownM y.
Proof. exact: uPred_primitive.bupd_ownM_updateP. Qed.
(* iris/base_logic/bi.v *)
Lemma ownM_forall {A} (f : A → M) :
    (∀ a, uPred_ownM (f a)) ⊢ ∃ z, uPred_ownM z ∧ (∀ a, f a ≼ z).
Proof. exact: uPred_primitive.ownM_forall. Qed.
(* iris/base_logic/bi.v *)
(* We restate the unsealing lemmas for the BI layer. The sealing lemmas
  are partially applied so that they also rewrite under binders. *)
Lemma uPred_emp_unseal :
    bi_emp = @upred.uPred_si_pure_def M (siprop.siProp_pure_def True).
Proof. by rewrite -upred.uPred_si_pure_unseal -siprop.siProp_pure_unseal. Qed.
(* iris/base_logic/bi.v *)
Lemma uPred_pure_unseal :
    bi_pure = λ φ, @upred.uPred_si_pure_def M (siprop.siProp_pure_def φ).
Proof. by rewrite -upred.uPred_si_pure_unseal -siprop.siProp_pure_unseal. Qed.
(* iris/base_logic/bi.v *)
Lemma uPred_si_pure_unseal : si_pure = @upred.uPred_si_pure_def M.
Proof. by rewrite -upred.uPred_si_pure_unseal. Qed.
(* iris/base_logic/bi.v *)
Lemma uPred_si_emp_valid_unseal :
    si_emp_valid = @upred.uPred_si_emp_valid_def M.
Proof. by rewrite -upred.uPred_si_emp_valid_unseal. Qed.
(* iris/base_logic/bi.v *)
Lemma uPred_and_unseal : bi_and = @upred.uPred_and_def M.
Proof. by rewrite -upred.uPred_and_unseal. Qed.
(* iris/base_logic/bi.v *)
Lemma uPred_or_unseal : bi_or = @upred.uPred_or_def M.
Proof. by rewrite -upred.uPred_or_unseal. Qed.
(* iris/base_logic/bi.v *)
Lemma uPred_impl_unseal : bi_impl = @upred.uPred_impl_def M.
Proof. by rewrite -upred.uPred_impl_unseal. Qed.
(* iris/base_logic/bi.v *)
Lemma uPred_forall_unseal : @bi_forall _ = @upred.uPred_forall_def M.
Proof. by rewrite -upred.uPred_forall_unseal. Qed.
(* iris/base_logic/bi.v *)
Lemma uPred_exist_unseal : @bi_exist _ = @upred.uPred_exist_def M.
Proof. by rewrite -upred.uPred_exist_unseal. Qed.
(* iris/base_logic/bi.v *)
Lemma uPred_sep_unseal : bi_sep = @upred.uPred_sep_def M.
Proof. by rewrite -upred.uPred_sep_unseal. Qed.
(* iris/base_logic/bi.v *)
Lemma uPred_wand_unseal : bi_wand = @upred.uPred_wand_def M.
Proof. by rewrite -upred.uPred_wand_unseal. Qed.
(* iris/base_logic/bi.v *)
Lemma uPred_persistently_unseal :
    bi_persistently = @upred.uPred_persistently_def M.
Proof. by rewrite -upred.uPred_persistently_unseal. Qed.
(* iris/base_logic/bi.v *)
Lemma uPred_later_unseal : bi_later = @upred.uPred_later_def M.
Proof. by rewrite -upred.uPred_later_unseal. Qed.
(* iris/base_logic/bi.v *)
Lemma uPred_bupd_unseal : bupd = @upred.uPred_bupd_def M.
Proof. by rewrite -upred.uPred_bupd_unseal. Qed.
(* iris/base_logic/bi.v *)
Definition uPred_unseal
:=
    (uPred_emp_unseal, uPred_pure_unseal,
    uPred_si_pure_unseal, uPred_si_emp_valid_unseal,
    uPred_and_unseal, uPred_or_unseal,
    uPred_impl_unseal, uPred_forall_unseal, uPred_exist_unseal,
    uPred_sep_unseal, uPred_wand_unseal,
    uPred_persistently_unseal, uPred_later_unseal,
    upred.uPred_ownM_unseal, @uPred_bupd_unseal).
(* iris/base_logic/bi.v *)
(* A tactic for rewriting with the above lemmas. Unfolds [uPred] goals that use
the BI layer. This is used by [base_logic.algebra] and [base_logic.bupd_alt]. *)
Ltac unseal
:= rewrite !uPred_unseal /=.
(* iris/base_logic/bupd_alt.v *)
(* This file contains an alternative version of basic updates, that is
expression in terms of just the plain modality [■]. *)
Definition bupd_alt {PROP : bi} `{!Sbi PROP} (P : PROP) : PROP
:=
  ∀ R, (P -∗ ■ R) -∗ ■ R.
(* iris/base_logic/bupd_alt.v *)
(* This definition is stated for any BI with a plain modality. The above
definition is akin to the continuation monad, where one should think of [■ R]
being the final result that one wants to get out of the basic update in the end
of the day (via [bupd_alt (■ P) ⊢ ■ P]).

We show that:

1. [bupd_alt] enjoys the usual rules of the basic update modality.
2. Any other modality that enjoys the laws of a basic update modality
   entails [bupd_alt] (see [bupd_bupd_alt]).
3. [bupd_alt] entails the ordinary basic update modality [|==>] on [uPred] 
   (see [bupd_alt_bupd]). This result is proven in the model of [uPred].

The first two points are shown for any BI with a plain modality. *)
Coercion uPred_holds : uPred >-> Funclass.
(* iris/base_logic/bupd_alt.v *)
Notation bupd_alt
:= (@bupd_alt PROP _).
(* iris/base_logic/bupd_alt.v *)
Instance bupd_alt_ne : NonExpansive bupd_alt.
Proof. solve_proper. Qed.
(* iris/base_logic/bupd_alt.v *)
Instance bupd_alt_proper : Proper ((≡) ==> (≡)) bupd_alt.
Proof. solve_proper. Qed.
(* iris/base_logic/bupd_alt.v *)
Instance bupd_alt_mono' : Proper ((⊢) ==> (⊢)) bupd_alt.
Proof. solve_proper. Qed.
(* iris/base_logic/bupd_alt.v *)
Instance bupd_alt_flip_mono' : Proper (flip (⊢) ==> flip (⊢)) bupd_alt.
Proof. solve_proper. Qed.
(* iris/base_logic/bupd_alt.v *)
(* The laws of the basic update modality hold *)
Lemma bupd_alt_intro P : P ⊢ bupd_alt P.
Proof. iIntros "HP" (R) "H". by iApply "H". Qed.
(* iris/base_logic/bupd_alt.v *)
Lemma bupd_alt_mono P Q : (P ⊢ Q) → bupd_alt P ⊢ bupd_alt Q.
Proof. by intros ->. Qed.
(* iris/base_logic/bupd_alt.v *)
Lemma bupd_alt_trans P : bupd_alt (bupd_alt P) ⊢ bupd_alt P.
Proof. iIntros "HP" (R) "H". iApply "HP". iIntros "HP". by iApply "HP". Qed.
(* iris/base_logic/bupd_alt.v *)
Lemma bupd_alt_frame_r P Q : bupd_alt P ∗ Q ⊢ bupd_alt (P ∗ Q).
Proof.
    iIntros "[HP HQ]" (R) "H". iApply "HP". iIntros "HP". iApply ("H" with "[$]").
  Qed.
(* iris/base_logic/bupd_alt.v *)
Lemma bupd_alt_plainly P : bupd_alt (■ P) ⊢ ■ P.
Proof. iIntros "H". iApply ("H" $! P with "[]"); auto. Qed.
(* iris/base_logic/bupd_alt.v *)
(* Any modality conforming with [BiBUpdPlainly] entails the alternative
  definition *)
Lemma bupd_bupd_alt `{!BiBUpd PROP, !BiBUpdSbi PROP, !BiAffine PROP} P :
    (|==> P) ⊢ bupd_alt P.
Proof. iIntros "HP" (R) "H". by iMod ("H" with "HP") as "?". Qed.
(* iris/base_logic/bupd_alt.v *)
Lemma own_updateP x (Φ : M → Prop) :
    x ~~>: Φ → own x ⊢ bupd_alt (∃ y, ⌜Φ y⌝ ∧ own y).
Proof.
    iIntros (Hup) "Hx"; iIntros (R) "H".
    iApply (own_updateP_plainly with "[$Hx H]"); first done.
    iIntros (y ?) "Hy". iApply "H"; auto.
  Qed.
(* iris/base_logic/bupd_alt.v *)
(* The alternative definition entails the ordinary basic update *)
Lemma bupd_alt_bupd {M} (P : uPred M) : bupd_alt P ⊢ |==> P.
Proof.
  rewrite /bupd_alt /plainly. uPred.unseal; split=> n x Hx H k y ? Hxy.
  unshelve refine (H {| uPred_holds k _ :=
    ∃ x' : M, ✓{k} (x' ⋅ y) ∧ P k x' |} k y _ _ _).
  - intros n1 n2 x1 x2 (z&?&?) _ ?.
    eauto using cmra_validN_le, uPred_mono.
  - done.
  - done.
  - intros k' z ?? HP. exists z. by rewrite (comm op).
Qed.
(* iris/base_logic/bupd_alt.v *)
Lemma bupd_alt_bupd_iff {M} (P : uPred M) : bupd_alt P ⊣⊢ |==> P.
Proof.
  apply (anti_symm _).
  - apply bupd_alt_bupd.
  - apply bupd_bupd_alt.
Qed.
(* iris/base_logic/bupd_alt.v *)
(* The law about the interaction between [uPred_ownM] and plainly holds. *)
Lemma ownM_updateP {M : ucmra} x (Φ : M → Prop) (R : uPred M) :
  x ~~>: Φ →
  uPred_ownM x ∗ (∀ y, ⌜Φ y⌝ -∗ uPred_ownM y -∗ ■ R) ⊢ ■ R.
Proof.
  intros Hup. rewrite /plainly. uPred.unseal.
  split. intros n z Hv (?&z2&?&[z1 ?]&HR); ofe_subst.
  destruct (Hup n (Some (z1 ⋅ z2))) as (y&?&?); simpl in *.
  { by rewrite assoc. }
  refine (HR y n z1 _ _ _ n y _ _ _); auto.
  - rewrite comm. by eapply cmra_validN_op_r.
  - by rewrite (comm _ _ y) (comm _ z2).
  - apply (reflexivity (R:=includedN _)).
Qed.
(* iris/base_logic/derived.v *)
(* Force implicit argument M *)
Notation "P ⊢ Q"
:= (bi_entails (PROP:=uPredI M) P Q).
(* iris/base_logic/derived.v *)
(* Propers *)
Instance ownM_proper: Proper ((≡) ==> (⊣⊢)) (@uPred_ownM M)
:= ne_proper _.
(* iris/base_logic/derived.v *)
(* Own and valid derived *)
Lemma intuitionistically_ownM (a : M) : CoreId a → □ uPred_ownM a ⊣⊢ uPred_ownM a.
Proof.
    rewrite /bi_intuitionistically affine_affinely=>?; apply (anti_symm _);
      [by rewrite persistently_elim|].
    by rewrite {1}persistently_ownM_core core_id_core.
  Qed.
(* iris/base_logic/derived.v *)
Lemma ownM_invalid (a : M) : ¬ ✓{0} a → uPred_ownM a ⊢ False.
Proof.
    intros. rewrite ownM_valid internal_cmra_valid_elim. by apply pure_elim'.
  Qed.
(* iris/base_logic/derived.v *)
Instance ownM_mono : Proper (flip (≼) ==> (⊢)) (@uPred_ownM M).
Proof. intros a b [b' ->]. by rewrite ownM_op sep_elim_l. Qed.
(* iris/base_logic/derived.v *)
Lemma ownM_unit' : uPred_ownM ε ⊣⊢ True.
Proof. apply (anti_symm _); first by apply pure_intro. apply ownM_unit. Qed.
(* iris/base_logic/derived.v *)
Lemma bupd_ownM_update x y : x ~~> y → uPred_ownM x ⊢ |==> uPred_ownM y.
Proof.
    intros; rewrite (bupd_ownM_updateP _ (y =.)); last by apply cmra_update_updateP.
    by apply bupd_mono, exist_elim=> y'; apply pure_elim_l=> ->.
  Qed.
(* iris/base_logic/derived.v *)
(* Timeless instances *)
Instance ownM_timeless (a : M) : Discrete a → Timeless (uPred_ownM a).
Proof.
    intros ?. rewrite /Timeless later_ownM. apply exist_elim=> b.
    rewrite (timeless (a≡b)) (except_0_intro (uPred_ownM b)) -except_0_and.
    apply except_0_mono. rewrite internal_eq_sym.
    apply (internal_eq_rewrite' b a (uPred_ownM) _);
      [solve_proper|auto using and_elim_l, and_elim_r..].
  Qed.
(* iris/base_logic/derived.v *)
(* Persistence *)
Instance ownM_persistent a : CoreId a → Persistent (@uPred_ownM M a).
Proof.
    intros. rewrite /Persistent -{2}(core_id_core a). apply persistently_ownM_core.
  Qed.
(* iris/base_logic/derived.v *)
(* For big ops *)
Instance uPred_ownM_sep_homomorphism :
    MonoidHomomorphism op uPred_sep (≡) (@uPred_ownM M).
Proof. split; [split|]; try apply _; [apply ownM_op | apply ownM_unit']. Qed.
(* iris/base_logic/derived.v *)
(* Soundness statement for our modalities: facts derived under modalities in
  the empty context also without the modalities.
  For basic updates, soundness only holds for plain propositions. *)
Lemma bupd_soundness P `{!Plain P} : (⊢ |==> P) → ⊢ P.
Proof. rewrite bupd_elim. done. Qed.
(* iris/base_logic/derived.v *)
(* As pure demonstration, we also show that this holds for an arbitrary nesting
  of modalities. We have to do a bit of work to be able to state this theorem
  though. *)
Inductive modality
:= MBUpd | MLater | MPersistently | MPlainly.
(* iris/base_logic/derived.v *)
Definition denote_modality (m : modality) : uPred M → uPred M
:=
    match m with
    | MBUpd => bupd
    | MLater => bi_later
    | MPersistently => bi_persistently
    | MPlainly => plainly
    end.
(* iris/base_logic/derived.v *)
Definition denote_modalities (ms : list modality) : uPred M → uPred M
:=
    λ P, foldr denote_modality P ms.
(* iris/base_logic/derived.v *)
(* Now we can state and prove 'soundness under arbitrary modalities' for plain
  propositions. This is probably not a lemma you want to actually use. *)
Corollary modal_soundness P `{!Plain P} (ms : list modality) :
    (⊢ denote_modalities ms P) → ⊢ P.
Proof.
    intros H. apply (laterN_soundness _ (length ms)).
    move: H. apply bi_emp_valid_mono.
    induction ms as [|m ms IH]; first done; simpl.
    destruct m; simpl; rewrite IH.
    - rewrite -later_intro. apply: bupd_elim.
    - done.
    - rewrite -later_intro persistently_elim. done.
    - rewrite -later_intro plainly_elim. done.
  Qed.
(* iris/base_logic/derived.v *)
(* Consistency: one cannot deive [False] in the logic, not even under
  modalities. Again this is just for demonstration and probably not practically
  useful. *)
Corollary consistency : ¬ ⊢@{uPredI M} False.
Proof. apply: pure_soundness. Qed.
(* iris/base_logic/proofmode.v *)
Instance from_sep_ownM (a b1 b2 : M) :
    IsOp a b1 b2 →
    FromSep (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
Proof. intros. by rewrite /FromSep -ownM_op -is_op. Qed.
(* iris/base_logic/proofmode.v *)
(* Cost > 50 to give priority to [combine_sep_as_fractional]. *)
Instance combine_sep_as_ownM (a b1 b2 : M) :
    IsOp a b1 b2 →
    CombineSepAs (uPred_ownM b1) (uPred_ownM b2) (uPred_ownM a) | 60.
Proof. intros. by rewrite /CombineSepAs -ownM_op -is_op. Qed.
(* iris/base_logic/proofmode.v *)
(* TODO: Improve this instance with generic own validity simplification
  machinery once https://gitlab.mpi-sws.org/iris/iris/-/issues/460 is fixed *)
Instance combine_sep_gives_ownM (b1 b2 : M) :
    CombineSepGives (uPred_ownM b1) (uPred_ownM b2) (✓ (b1 ⋅ b2)).
Proof.
    intros. rewrite /CombineSepGives -ownM_op ownM_valid.
    by apply: bi.persistently_intro.
  Qed.
(* iris/base_logic/proofmode.v *)
Instance from_sep_ownM_core_id (a b1 b2 : M) :
    IsOp a b1 b2 → TCOr (CoreId b1) (CoreId b2) →
    FromAnd (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
Proof.
    intros ? H. rewrite /FromAnd (is_op a) ownM_op.
    destruct H; by rewrite bi.persistent_and_sep.
  Qed.
(* iris/base_logic/proofmode.v *)
Instance into_and_ownM p (a b1 b2 : M) :
    IsOp a b1 b2 → IntoAnd p (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
Proof.
    intros. apply bi.intuitionistically_if_mono. by rewrite (is_op a) ownM_op bi.sep_and.
  Qed.
(* iris/base_logic/proofmode.v *)
Instance into_sep_ownM (a b1 b2 : M) :
    IsOp a b1 b2 → IntoSep (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
Proof. intros. by rewrite /IntoSep (is_op a) ownM_op. Qed.
(* iris/base_logic/upred.v *)
(* Note that, somewhat curiously, [uPred M] is *not* in general a Camera,
   at least not if all propositions are considered "valid" Camera elements.
   It fails to satisfy the extension axiom. Here is the counterexample:

We use [M := (option Ex {A,B})^2] -- so we have pairs
whose components are ε, A or B.

Let
[[
  P r n := (ownM (A,A) ∧ ▷ False) ∨ ownM (A,B) ∨ ownM (B,A) ∨ ownM (B,B)
         ↔ r = (A,A) ∧ n = 0 ∨
           r = (A,B) ∨
           r = (B,A) ∨
           r = (B,B)
 Q1 r n := ownM (A, ε) ∨ ownM (B, ε)
         ↔ (A, ε) ≼ r ∨ (B, ε) ≼ r
           ("Left component is not ε")
 Q2 r n := ownM (ε, A) ∨ ownM (ε, B)
         ↔ (ε, A) ≼ r ∨ (ε, B) ≼ r
           ("Right component is not ε")
]]
These are all sufficiently closed and non-expansive and whatnot.
We have [P ≡{0}≡ Q1 * Q2]. So assume extension holds, then we get Q1', Q2'
such that
[[
  P ≡ Q1' ∗ Q2'
 Q1 ≡{0}≡ Q1'
 Q2 ≡{0}≡ Q2'
]]
Now comes the contradiction:
We know that [P (A,A) 1] does *not* hold, but I am going to show that
[(Q1' ∗ Q2') (A,A) 1] holds, which would be a contraction.
To this end, I will show (a) [Q1' (A,ε) 1] and (b) [Q2' (ε,A) 1].
The result [(Q1' ∗ Q2') (A,A)] follows from [(A,ε) ⋅ (ε,A) = (A,A)].

(a) Proof of [Q1' (A,ε) 1].
    We have [P (A,B) 1], and thus [Q1' r1 1] and [Q2' r2 1] for some
    [r1 ⋅ r2 = (A,B)]. There are four possible decompositions [r1 ⋅ r2]:
    - [(ε,ε) ⋅ (A,B)]: This would give us [Q1' (ε,ε) 1], from which we
      obtain (through down-closure and the equality [Q1 ≡{0}≡ Q1'] above) that
      [Q1 (ε,ε) 0]. However, we know that's false.
    - [(A,B) ⋅ (ε,ε)]: Can be excluded for similar reasons
      (the second resource must not be ε in the 2nd component).
    - [(ε,B) ⋅ (A,ε)]: Can be excluded for similar reasons
      (the first resource must not be ε in the 1st component).
    - [(A,ε) ⋅ (ε,B)]: This gives us the desired [Q1' (A,ε) 1].

(b) Proof of [Q2' (ε,A) 1].
    We have [P (B,A) 1], and thus [Q1' r1 1] and [Q2' r2 1] for some
    [r1 ⋅ r2 = (B,A)]. There are again four possible decompositions,
    and like above we can exclude three of them. This leaves us with
    [(B,ε) ⋅ (ε,A)] and thus [Q2' (ε,A) 1].

This completes the proof. *)
Record uPred (M : ucmra) : Type
:= UPred {
  uPred_holds : nat → M → Prop;

  uPred_mono n1 n2 x1 x2 :
    uPred_holds n1 x1 → x1 ≼{n2} x2 → n2 ≤ n1 → uPred_holds n2 x2
}.
(* iris/base_logic/upred.v *)
Instance : Params (@uPred_holds) 3
:= {}.
(* iris/base_logic/upred.v *)
Inductive uPred_equiv' (P Q : uPred M) : Prop
:=
    { uPred_in_equiv : ∀ n x, ✓{n} x → P n x ↔ Q n x }.
(* iris/base_logic/upred.v *)
Instance uPred_equiv : Equiv (uPred M)
:= uPred_equiv'.
(* iris/base_logic/upred.v *)
Inductive uPred_dist' (n : nat) (P Q : uPred M) : Prop
:=
    { uPred_in_dist : ∀ n' x, n' ≤ n → ✓{n'} x → P n' x ↔ Q n' x }.
(* iris/base_logic/upred.v *)
Instance uPred_dist : Dist (uPred M)
:= uPred_dist'.
(* iris/base_logic/upred.v *)
Definition uPred_ofe_mixin : OfeMixin (uPred M).
Proof.
    apply ofe_mixin_finite.
    - intros P Q; split.
      + by intros HPQ n; split=> i x ??; apply HPQ.
      + intros HPQ; split=> n x ?; apply HPQ with n; auto.
    - intros n; split.
      + by intros P; split=> x i.
      + by intros P Q HPQ; split=> x i ??; symmetry; apply HPQ.
      + intros P Q Q' HP HQ; split=> i x ??.
        by trans (Q i x);[apply HP|apply HQ].
    - intros n P Q HPQ. split=> i x ??; apply HPQ; eauto with lia.
  Qed.
(* iris/base_logic/upred.v *)
Canonical uPredO : ofe
:= Ofe (uPred M) uPred_ofe_mixin.
(* iris/base_logic/upred.v *)
Definition uPred_compl : Compl uPredO := λ c,
    {| uPred_holds n x := ∀ n', n' ≤ n → ✓{n'} x → c n' n' x |}.
Next Obligation.
    move=> /= c n1 n2 x1 x2 HP Hx12 Hn12 n3 Hn23 Hv. eapply uPred_mono.
    - eapply HP, cmra_validN_includedN, cmra_includedN_le=>//; lia.
    - eapply cmra_includedN_le=>//; lia.
    - done.
  Qed.
(* iris/base_logic/upred.v *)
Instance uPred_cofe : Cofe uPredO := cofe_finite uPred_compl _.
Next Obligation.
    intros n c; split=>i x Hin Hv.
    etrans; [|by symmetry; apply (chain_cauchy c i n)].
    split=>H; [by apply H|].
    repeat intro. apply (chain_cauchy c _ i)=>//. by eapply uPred_mono.
  Qed.
(* iris/base_logic/upred.v *)
Instance uPred_ne {M} (P : uPred M) n : Proper (dist n ==> iff) (P n).
Proof.
  intros x1 x2 Hx; split=> ?; eapply uPred_mono; eauto; by rewrite Hx.
Qed.
(* iris/base_logic/upred.v *)
Instance uPred_proper {M} (P : uPred M) n : Proper ((≡) ==> iff) (P n).
Proof. by intros x1 x2 Hx; apply uPred_ne, equiv_dist. Qed.
(* iris/base_logic/upred.v *)
Lemma uPred_holds_ne {M} (P Q : uPred M) n1 n2 x :
  P ≡{n2}≡ Q → n2 ≤ n1 → ✓{n2} x → Q n1 x → P n2 x.
Proof.
  intros [Hne] ???. eapply Hne; try done. eauto using uPred_mono, cmra_validN_le.
Qed.
(* iris/base_logic/upred.v *)
(* Equivalence to the definition of uPred in the appendix. *)
Lemma uPred_alt {M : ucmra} (P: nat → M → Prop) :
  (∀ n1 n2 x1 x2, P n1 x1 → x1 ≼{n1} x2 → n2 ≤ n1 → P n2 x2) ↔
  ( (∀ x n1 n2, n2 ≤ n1 → P n1 x → P n2 x) (* Pointwise down-closed *)
  ∧ (∀ n x1 x2, x1 ≡{n}≡ x2 → ∀ m, m ≤ n → P m x1 ↔ P m x2) (* Non-expansive *)
  ∧ (∀ n x1 x2, x1 ≼{n} x2 → ∀ m, m ≤ n → P m x1 → P m x2) (* Monotonicity *)
  ).
Proof.
  (* Provide this lemma to eauto. *)
  assert (∀ n1 n2 (x1 x2 : M), n2 ≤ n1 → x1 ≡{n1}≡ x2 → x1 ≼{n2} x2).
  { intros ????? H. eapply cmra_includedN_le; last done. by rewrite H. }
  (* Now go ahead. *)
  split.
  - intros Hupred. repeat split; eauto using cmra_includedN_le.
  - intros (Hdown & _ & Hmono) **. eapply Hmono; [done..|]. eapply Hdown; done.
Qed.
(* iris/base_logic/upred.v *)
(* functor *)
Definition uPred_map {M1 M2 : ucmra} (f : M2 -n> M1)
  `{!CmraMorphism f} (P : uPred M1) :
  uPred M2 := {| uPred_holds n x := P n (f x) |}.
Next Obligation. naive_solver eauto using uPred_mono, cmra_morphism_monoN. Qed.
(* iris/base_logic/upred.v *)
Instance uPred_map_ne {M1 M2 : ucmra} (f : M2 -n> M1)
  `{!CmraMorphism f} n : Proper (dist n ==> dist n) (uPred_map f).
Proof.
  intros x1 x2 Hx; split=> n' y ??.
  split; apply Hx; auto using cmra_morphism_validN.
Qed.
(* iris/base_logic/upred.v *)
Lemma uPred_map_id {M : ucmra} (P : uPred M): uPred_map cid P ≡ P.
Proof. by split=> n x ?. Qed.
(* iris/base_logic/upred.v *)
Lemma uPred_map_compose {M1 M2 M3 : ucmra} (f : M1 -n> M2) (g : M2 -n> M3)
    `{!CmraMorphism f, !CmraMorphism g} (P : uPred M3):
  uPred_map (g ◎ f) P ≡ uPred_map f (uPred_map g P).
Proof. by split=> n x Hx. Qed.
(* iris/base_logic/upred.v *)
Lemma uPred_map_ext {M1 M2 : ucmra} (f g : M1 -n> M2)
      `{!CmraMorphism f} `{!CmraMorphism g}:
  (∀ x, f x ≡ g x) → ∀ x, uPred_map f x ≡ uPred_map g x.
Proof. intros Hf P; split=> n x Hx /=; by rewrite /uPred_holds /= Hf. Qed.
(* iris/base_logic/upred.v *)
Definition uPredO_map {M1 M2 : ucmra} (f : M2 -n> M1) `{!CmraMorphism f} :
  uPredO M1 -n> uPredO M2
:= OfeMor (uPred_map f : uPredO M1 → uPredO M2).
(* iris/base_logic/upred.v *)
Lemma uPredO_map_ne {M1 M2 : ucmra} (f g : M2 -n> M1)
    `{!CmraMorphism f, !CmraMorphism g} n :
  f ≡{n}≡ g → uPredO_map f ≡{n}≡ uPredO_map g.
Proof.
  by intros Hfg P; split=> n' y ??;
  rewrite /uPred_holds /= (dist_le _ _ _ _(Hfg y)).
Qed.
(* iris/base_logic/upred.v *)
Definition uPredOF (F : urFunctor) : oFunctor := {|
  oFunctor_car A _ B _ := uPredO (urFunctor_car F B A);
  oFunctor_map A1 _ A2 _ B1 _ B2 _ fg := uPredO_map (urFunctor_map F (fg.2, fg.1))
|}.
Next Obligation.
  intros F A1 ? A2 ? B1 ? B2 ? n P Q HPQ.
  apply uPredO_map_ne, urFunctor_map_ne; split; by apply HPQ.
Qed.