phanerozoic/Coq-Iris huggingface dataset:
(* iris/bi/sbi_unfold.v *)
Instance sbi_unfold_and clo P Q Pi Qi :
    SbiUnfold clo P Pi →
    SbiUnfold clo Q Qi →
    SbiUnfold clo (P ∧ Q) (λ n, Pi n ∧ Qi n).
Proof.
    intros [? HP] [? HQ]. split; [naive_solver|].
    rewrite HP HQ -si_pure_and. f_equiv.
    siProp.unseal. split=> n /=. destruct clo; naive_solver.
  Qed.
(* iris/bi/sbi_unfold.v *)
Instance sbi_unfold_sep clo P Q Pi Qi :
    SbiUnfold clo P Pi →
    SbiUnfold clo Q Qi →
    SbiUnfold clo (P ∗ Q) (λ n, Pi n ∧ Qi n).
Proof.
    intros [? HP] [? HQ]. split; [naive_solver|].
    rewrite HP HQ -si_pure_and_sep. f_equiv.
    siProp.unseal. split=> n /=. destruct clo; naive_solver.
  Qed.
(* iris/bi/sbi_unfold.v *)
(* The instance for disjunction needs the sub-expressions to be already down
  closed because [∨] and [∀] do not commute. *)
Instance sbi_unfold_or clo P Q Pi Qi :
    SbiUnfold DownClosed P Pi →
    SbiUnfold DownClosed Q Qi →
    SbiUnfold clo (P ∨ Q) (λ n, Pi n ∨ Qi n).
Proof.
    intros [? HP] [? HQ]. apply: SbiUnfold_closed; [naive_solver|].
    intros ?. rewrite HP HQ -si_pure_or. f_equiv.
    split=> n /=; siProp.unseal; naive_solver.
  Qed.
(* iris/bi/sbi_unfold.v *)
Instance sbi_unfold_impl clo P Q Pi Qi :
    SbiUnfold DownClosed P Pi →
    SbiUnfold NotClosed Q Qi →
    SbiUnfold clo (P → Q) (sbi_unfold_maybe_downclose clo (λ n, Pi n → Qi n)).
Proof.
    intros [? HP] [? HQ]. apply SbiUnfold_downclose.
    rewrite HP HQ -si_pure_impl. f_equiv.
    split=> n /=; siProp.unseal; naive_solver eauto with lia.
  Qed.
(* iris/bi/sbi_unfold.v *)
Instance sbi_unfold_wand clo P Q Pi Qi :
    SbiUnfold DownClosed P Pi →
    SbiUnfold NotClosed Q Qi →
    SbiUnfold clo (P -∗ Q) (sbi_unfold_maybe_downclose clo (λ n, Pi n → Qi n)).
Proof.
    intros [? HP] [? HQ]. apply SbiUnfold_downclose.
    rewrite HP HQ -si_pure_impl_wand. f_equiv. 
    split=> n /=; siProp.unseal; naive_solver eauto with lia.
  Qed.
(* iris/bi/sbi_unfold.v *)
Instance sbi_unfold_iff clo P Q Pi Qi :
    SbiUnfold DownClosed P Pi →
    SbiUnfold DownClosed Q Qi →
    SbiUnfold clo (P ↔ Q) (sbi_unfold_maybe_downclose clo (λ n, Pi n ↔ Qi n)).
Proof.
    intros [? HP] [? HQ]. apply SbiUnfold_downclose.
    rewrite HP HQ -si_pure_iff. f_equiv.
    split=> n /=; rewrite /bi_iff; siProp.unseal; naive_solver eauto with lia.
  Qed.
(* iris/bi/sbi_unfold.v *)
Instance sbi_unfold_iff_wand clo P Q Pi Qi :
    SbiUnfold DownClosed P Pi →
    SbiUnfold DownClosed Q Qi →
    SbiUnfold clo (P ∗-∗ Q) (sbi_unfold_maybe_downclose clo (λ n, Pi n ↔ Qi n)).
Proof.
    intros [? HP] [? HQ]. apply SbiUnfold_downclose.
    rewrite HP HQ -si_pure_impl_iff_wand. f_equiv.
    split=> n /=; rewrite /bi_iff; siProp.unseal; naive_solver eauto with lia.
  Qed.
(* iris/bi/sbi_unfold.v *)
Instance sbi_unfold_forall {A} clo (Φ : A → PROP) Φi :
    (∀ x, SbiUnfold clo (Φ x) (Φi x)) →
    SbiUnfold clo (∀ x, Φ x) (λ n, ∀ x, Φi x n).
Proof.
    intros HΦ. split; [naive_solver|]. etrans; [f_equiv=> x; apply HΦ|].
    rewrite -si_pure_forall. f_equiv.
    split=> n /=; siProp.unseal; destruct clo; naive_solver eauto with lia.
  Qed.
(* iris/bi/sbi_unfold.v *)
(* The instance for existential needs the sub-expression to be already down
  closed because [∃] and [∀] do not commute. *)
Instance sbi_unfold_exist {A} clo (Φ : A → PROP) Φi :
    (∀ x, SbiUnfold DownClosed (Φ x) (Φi x)) →
    SbiUnfold clo (∃ x, Φ x) (λ n, ∃ x, Φi x n).
Proof.
    intros HΦ. apply: SbiUnfold_closed; [naive_solver|].
    intros ?. etrans; [f_equiv=> x; apply HΦ|].
    rewrite -si_pure_exist. f_equiv.
    split=> n /=; siProp.unseal; destruct clo; naive_solver eauto with lia.
  Qed.
(* iris/bi/sbi_unfold.v *)
Instance sbi_unfold_later clo P Pi :
    SbiUnfold clo P Pi →
    SbiUnfold clo (▷ P) (λ n, match n with 0 => True | S n' => Pi n' end).
Proof.
    intros [? HP]. split.
    { intros [] []; naive_solver eauto with lia. }
    rewrite HP -si_pure_later. f_equiv.
    split=> n /=; siProp.unseal; simpl. split.
    - destruct n; intros ? []; naive_solver eauto with lia.
    - destruct n; [done|]. intros HPi n' ?. apply (HPi (S n')); lia.
  Qed.
(* iris/bi/sbi_unfold.v *)
(* A helper to help with HO-unification in the [Hint Extern] below. *)
Lemma sbi_unfold_tceq `{Sbi PROP} clo (P : PROP) Pi Pi' :
  SbiUnfold clo P Pi' → TCEq Pi Pi' → SbiUnfold clo P Pi.
Proof. by intros ? ->. Qed.
(* iris/bi/sbi_unfold.v *)
Ltac sbi_unfold
:=
  match goal with
  | |- ⊢ _ => apply sbi_unfold_emp_valid
  | |- _ ⊣⊢ _ => apply sbi_unfold_equiv
  | |- _ ⊢ _ => apply sbi_unfold_entails
  | |- _ => fail "sbi_unfold: not a BI entailment"
  end;
  (* Some instances leave a down closure, which we simplify *)
  lazy [sbi_unfold_maybe_downclose].
(* iris/bi/telescopes.v *)
(* Telescopic quantifiers *)
Definition bi_texist {PROP : bi} {TT : tele@{Quant}} (Ψ : TT → PROP) : PROP
:=
  tele_fold (@bi_exist PROP) (λ x, x) (tele_bind Ψ).
(* iris/bi/telescopes.v *)
Definition bi_tforall {PROP : bi} {TT : tele@{Quant}} (Ψ : TT → PROP) : PROP
:=
  tele_fold (@bi_forall PROP) (λ x, x) (tele_bind Ψ).
(* iris/bi/telescopes.v *)
Notation "'∃..' x .. y , P"
:= (bi_texist (λ x, .. (bi_texist (λ y, P)) .. )%I)
  (at level 200, x binder, y binder, right associativity,
  format "∃..  x  ..  y ,  P") : bi_scope.
(* iris/bi/telescopes.v *)
Notation "'∀..' x .. y , P"
:= (bi_tforall (λ x, .. (bi_tforall (λ y, P)) .. )%I)
  (at level 200, x binder, y binder, right associativity,
  format "∀..  x  ..  y ,  P") : bi_scope.
(* iris/bi/telescopes.v *)
Lemma bi_tforall_forall Ψ : bi_tforall Ψ ⊣⊢ bi_forall Ψ.
Proof.
    unfold bi_tforall. apply (anti_symm _).
    - apply forall_intro. induction TT as [|X ft IH].
      { by intros []. }
      intros [x xs]; simpl. by rewrite (forall_elim x) IH.
    - induction TT as [|X ft IH]; simpl.
      { by rewrite (forall_elim TargO). }
      apply forall_intro=> x. rewrite -IH. apply forall_intro=> xs.
      by rewrite (forall_elim (TargS x xs)).
  Qed.
(* iris/bi/telescopes.v *)
Lemma bi_texist_exist Ψ : bi_texist Ψ ⊣⊢ bi_exist Ψ.
Proof.
    unfold bi_texist. apply (anti_symm _).
    - induction TT as [|X ft IH]; simpl.
      { by rewrite -(exist_intro TargO). }
      apply exist_elim=> x. rewrite IH. apply exist_elim=> xs.
      by rewrite (exist_intro (TargS x xs)).
    - apply exist_elim. induction TT as [|X ft IH].
      { by intros []. }
      intros [x xs]; simpl. by rewrite -(exist_intro x) -IH.
  Qed.
(* iris/bi/telescopes.v *)
Instance bi_tforall_ne n :
    Proper (pointwise_relation _ (dist n) ==> dist n) (@bi_tforall PROP TT).
Proof. intros ?? EQ. rewrite !bi_tforall_forall. rewrite EQ //. Qed.
(* iris/bi/telescopes.v *)
Instance bi_tforall_proper :
    Proper (pointwise_relation _ (⊣⊢) ==> (⊣⊢)) (@bi_tforall PROP TT).
Proof. intros ?? EQ. rewrite !bi_tforall_forall. rewrite EQ //. Qed.
(* iris/bi/telescopes.v *)
Instance bi_texist_ne n :
    Proper (pointwise_relation _ (dist n) ==> dist n) (@bi_texist PROP TT).
Proof. intros ?? EQ. rewrite !bi_texist_exist. rewrite EQ //. Qed.
(* iris/bi/telescopes.v *)
Instance bi_texist_proper :
    Proper (pointwise_relation _ (⊣⊢) ==> (⊣⊢)) (@bi_texist PROP TT).
Proof. intros ?? EQ. rewrite !bi_texist_exist. rewrite EQ //. Qed.
(* iris/bi/telescopes.v *)
Instance bi_tforall_absorbing Ψ :
    (∀ x, Absorbing (Ψ x)) → Absorbing (∀.. x, Ψ x).
Proof. rewrite bi_tforall_forall. apply _. Qed.
(* iris/bi/telescopes.v *)
Instance bi_tforall_persistent `{!BiPersistentlyForall PROP} Ψ :
    (∀ x, Persistent (Ψ x)) → Persistent (∀.. x, Ψ x).
Proof. rewrite bi_tforall_forall. apply _. Qed.
(* iris/bi/telescopes.v *)
Instance bi_texist_affine Ψ :
    (∀ x, Affine (Ψ x)) → Affine (∃.. x, Ψ x).
Proof. rewrite bi_texist_exist. apply _. Qed.
(* iris/bi/telescopes.v *)
Instance bi_texist_absorbing Ψ :
    (∀ x, Absorbing (Ψ x)) → Absorbing (∃.. x, Ψ x).
Proof. rewrite bi_texist_exist. apply _. Qed.
(* iris/bi/telescopes.v *)
Instance bi_texist_persistent Ψ :
    (∀ x, Persistent (Ψ x)) → Persistent (∃.. x, Ψ x).
Proof. rewrite bi_texist_exist. apply _. Qed.
(* iris/bi/telescopes.v *)
Instance bi_tforall_timeless Ψ :
    (∀ x, Timeless (Ψ x)) → Timeless (∀.. x, Ψ x).
Proof. rewrite bi_tforall_forall. apply _. Qed.
(* iris/bi/telescopes.v *)
Instance bi_texist_timeless Ψ :
    (∀ x, Timeless (Ψ x)) → Timeless (∃.. x, Ψ x).
Proof. rewrite bi_texist_exist. apply _. Qed.
(* iris/bi/updates.v *)
(* We first define operational type classes for the notations, and then later
bundle these operational type classes with the laws. *)
Class BUpd (PROP : Type) : Type
:= bupd : PROP → PROP.
(* iris/bi/updates.v *)
Instance : Params (@bupd) 2
:= {}.
(* iris/bi/updates.v *)
Notation "|==> Q"
:= (bupd Q) : bi_scope.
(* iris/bi/updates.v *)
Notation "P ==∗ Q"
:= (P -∗ |==> Q)%I : bi_scope.
(* iris/bi/updates.v *)
Notation "P ==∗ Q"
:= (P -∗ |==> Q) : stdpp_scope.
(* iris/bi/updates.v *)
Class FUpd (PROP : Type) : Type
:= fupd : coPset → coPset → PROP → PROP.
(* iris/bi/updates.v *)
Instance : Params (@fupd) 4
:= {}.
(* iris/bi/updates.v *)
Notation "P ={ E1 , E2 }=∗ Q"
:= (P -∗ |={E1,E2}=> Q)%I : bi_scope.
(* iris/bi/updates.v *)
Notation "P ={ E1 , E2 }=∗ Q"
:= (P -∗ |={E1,E2}=> Q) : stdpp_scope.
(* iris/bi/updates.v *)
Notation "|={ E }=> Q"
:= (fupd E E Q) : bi_scope.
(* iris/bi/updates.v *)
Notation "P ={ E }=∗ Q"
:= (P -∗ |={E}=> Q)%I : bi_scope.
(* iris/bi/updates.v *)
Notation "P ={ E }=∗ Q"
:= (P -∗ |={E}=> Q) : stdpp_scope.
(* iris/bi/updates.v *)
(* These have two masks, but they are different than the two masks of a
    mask-changing update: in [|={Eo}[Ei]▷=> Q], the first mask [Eo] ("outer
    mask") holds at the beginning and the end; the second mask [Ei] ("inner
    mask") holds around each ▷. This is also why we use a different notation
    than for the two masks of a mask-changing updates. *)
Notation "|={ Eo } [ Ei ]▷=> Q"
:= (|={Eo,Ei}=> ▷ |={Ei,Eo}=> Q)%I : bi_scope.
(* iris/bi/updates.v *)
Notation "P ={ Eo } [ Ei ]▷=∗ Q"
:= (P -∗ |={Eo}[Ei]▷=> Q)%I : bi_scope.
(* iris/bi/updates.v *)
Notation "P ={ Eo } [ Ei ]▷=∗ Q"
:= (P -∗ |={Eo}[Ei]▷=> Q) : stdpp_scope.
(* iris/bi/updates.v *)
Notation "|={ E }▷=> Q"
:= (|={E}[E]▷=> Q)%I : bi_scope.
(* iris/bi/updates.v *)
Notation "P ={ E }▷=∗ Q"
:= (P ={E}[E]▷=∗ Q)%I : bi_scope.
(* iris/bi/updates.v *)
Notation "P ={ E }▷=∗ Q"
:= (P ={E}[E]▷=∗ Q) : stdpp_scope.
(* iris/bi/updates.v *)
(* For the iterated version, in principle there are 4 masks: "outer" and
    "inner" of [|={Eo}[Ei]▷=>], as well as "begin" and "end" masks [E1] and [E2]
    that could potentially differ from [Eo]. The latter can be obtained from
    this notation by adding normal mask-changing update modalities: [
    |={E1,Eo}=> |={Eo}[Ei]▷=>^n |={Eo,E2}=> Q] *)
Notation "|={ Eo } [ Ei ]▷=>^ n Q"
:= (Nat.iter n (λ P, |={Eo}[Ei]▷=> P) Q)%I : bi_scope.
(* iris/bi/updates.v *)
Notation "P ={ Eo } [ Ei ]▷=∗^ n Q"
:= (P -∗ |={Eo}[Ei]▷=>^n Q)%I : bi_scope.
(* iris/bi/updates.v *)
Notation "P ={ Eo } [ Ei ]▷=∗^ n Q"
:= (P -∗ |={Eo}[Ei]▷=>^n Q) : stdpp_scope.
(* iris/bi/updates.v *)
Notation "|={ E }▷=>^ n Q"
:= (|={E}[E]▷=>^n Q)%I : bi_scope.
(* iris/bi/updates.v *)
Notation "P ={ E }▷=∗^ n Q"
:= (P ={E}[E]▷=∗^n Q)%I : bi_scope.
(* iris/bi/updates.v *)
Notation "P ={ E }▷=∗^ n Q"
:= (P ={E}[E]▷=∗^n Q) : stdpp_scope.
(* iris/bi/updates.v *)
(* Mixins allow us to create instances easily without having to use Program *)
Record BiBUpdMixin (PROP : bi) `(BUpd PROP)
:= {
  bi_bupd_mixin_bupd_ne : NonExpansive (bupd (PROP:=PROP));
  bi_bupd_mixin_bupd_intro (P : PROP) : P ⊢ |==> P;
  bi_bupd_mixin_bupd_mono (P Q : PROP) : (P ⊢ Q) → (|==> P) ⊢ |==> Q;
  bi_bupd_mixin_bupd_trans (P : PROP) : (|==> |==> P) ⊢ |==> P;
  bi_bupd_mixin_bupd_frame_r (P R : PROP) : (|==> P) ∗ R ⊢ |==> P ∗ R;
}.
(* iris/bi/updates.v *)
Record BiFUpdMixin (PROP : bi) `(FUpd PROP)
:= {
  bi_fupd_mixin_fupd_ne E1 E2 :
    NonExpansive (fupd (PROP:=PROP) E1 E2);
  bi_fupd_mixin_fupd_mask_subseteq E1 E2 :
    E2 ⊆ E1 → ⊢@{PROP} |={E1,E2}=> |={E2,E1}=> emp;
  bi_fupd_mixin_except_0_fupd E1 E2 (P : PROP) :
    ◇ (|={E1,E2}=> P) ⊢ |={E1,E2}=> P;
  bi_fupd_mixin_fupd_mono E1 E2 (P Q : PROP) :
    (P ⊢ Q) → (|={E1,E2}=> P) ⊢ |={E1,E2}=> Q;
  bi_fupd_mixin_fupd_trans E1 E2 E3 (P : PROP) :
    (|={E1,E2}=> |={E2,E3}=> P) ⊢ |={E1,E3}=> P;
  bi_fupd_mixin_fupd_mask_frame_r' E1 E2 Ef (P : PROP) :
    E1 ## Ef → (|={E1,E2}=> ⌜E2 ## Ef⌝ → P) ⊢ |={E1 ∪ Ef,E2 ∪ Ef}=> P;
  bi_fupd_mixin_fupd_frame_r E1 E2 (P R : PROP) :
    (|={E1,E2}=> P) ∗ R ⊢ |={E1,E2}=> P ∗ R;
}.
(* iris/bi/updates.v *)
Class BiBUpd (PROP : bi)
:= {
  #[global] bi_bupd_bupd :: BUpd PROP;
  bi_bupd_mixin : BiBUpdMixin PROP bi_bupd_bupd;
}.
(* iris/bi/updates.v *)
Class BiFUpd (PROP : bi)
:= {
  #[global] bi_fupd_fupd :: FUpd PROP;
  bi_fupd_mixin : BiFUpdMixin PROP bi_fupd_fupd;
}.
(* iris/bi/updates.v *)
Class BiBUpdFUpd (PROP : bi) `{BiBUpd PROP, BiFUpd PROP}
:=
  bupd_fupd E (P : PROP) : (|==> P) ⊢ |={E}=> P.
(* iris/bi/updates.v *)
Class BiBUpdSbi (PROP : bi) `{!BiBUpd PROP, !Sbi PROP}
:=
  bupd_si_pure Pi : (|==> <si_pure> Pi) ⊢@{PROP} <si_pure> Pi.
(* iris/bi/updates.v *)
(* These rules for the interaction between [<si_pure>] and the [|={E1,E2=>]
modality only make sense for affine logics. For general BIs we do not know the
canonical set of rules and linear models in which they might hold. *)
Class BiFUpdSbi (PROP : bi) `{!BiFUpd PROP, !Sbi PROP}
:= {
  (** This rule allows you to use the current context for proving a purely
  step-indexed proposition [Pi] *without* actually using up the context. You can
  then continue the proof in the second conjunct. The mask-changing version
  [fupd_si_pure_keep] can be derived. *)
  fupd_keep_si_pure' {E} E' Pi (R : PROP) :
    (|={E,E'}=> <si_pure> Pi) ∧ (<si_pure> Pi ={E}=∗ R) ⊢ |={E}=> R;
  (** Later "almost" commutes with fancy updates over plain propositions. It
  commutes "almost" because of the ◇ modality, which is needed in the definition
  of fancy updates so one can remove laters of timeless propositions. *)
  fupd_si_pure_later E Pi :
    (▷ |={E}=> <si_pure> Pi) ⊢@{PROP} |={E}=> ▷ ◇ <si_pure> Pi;
  (** Forall quantifiers commute with fancy updates over plain propositions. *)
  fupd_si_pure_forall_2 E {A} (Φi : A → siProp) :
    (∀ x, |={E}=> <si_pure> Φi x) ⊢@{PROP} |={E}=> ∀ x, <si_pure> Φi x
}.
(* iris/bi/updates.v *)
Instance bupd_ne : NonExpansive (@bupd PROP _).
Proof. eapply bi_bupd_mixin_bupd_ne, bi_bupd_mixin. Qed.
(* iris/bi/updates.v *)
Lemma bupd_intro P : P ⊢ |==> P.
Proof. eapply bi_bupd_mixin_bupd_intro, bi_bupd_mixin. Qed.
(* iris/bi/updates.v *)
Lemma bupd_mono (P Q : PROP) : (P ⊢ Q) → (|==> P) ⊢ |==> Q.
Proof. eapply bi_bupd_mixin_bupd_mono, bi_bupd_mixin. Qed.
(* iris/bi/updates.v *)
Lemma bupd_trans (P : PROP) : (|==> |==> P) ⊢ |==> P.
Proof. eapply bi_bupd_mixin_bupd_trans, bi_bupd_mixin. Qed.
(* iris/bi/updates.v *)
Lemma bupd_frame_r (P R : PROP) : (|==> P) ∗ R ⊢ |==> P ∗ R.
Proof. eapply bi_bupd_mixin_bupd_frame_r, bi_bupd_mixin. Qed.
(* iris/bi/updates.v *)
Instance fupd_ne E1 E2 : NonExpansive (@fupd PROP _ E1 E2).
Proof. eapply bi_fupd_mixin_fupd_ne, bi_fupd_mixin. Qed.
(* iris/bi/updates.v *)
(* [iMod] with this lemma is useful to change the current mask to a subset,
  and obtain a fupd for changing it back. For the case where you want to get rid
  of a mask-changing fupd in the goal, [iApply fupd_mask_intro] avoids having to
  specify the mask. *)
Lemma fupd_mask_subseteq {E1} E2 : E2 ⊆ E1 → ⊢@{PROP} |={E1,E2}=> |={E2,E1}=> emp.
Proof. eapply bi_fupd_mixin_fupd_mask_subseteq, bi_fupd_mixin. Qed.
(* iris/bi/updates.v *)
Lemma except_0_fupd E1 E2 (P : PROP) : ◇ (|={E1,E2}=> P) ⊢ |={E1,E2}=> P.
Proof. eapply bi_fupd_mixin_except_0_fupd, bi_fupd_mixin. Qed.
(* iris/bi/updates.v *)
Lemma fupd_mono E1 E2 (P Q : PROP) : (P ⊢ Q) → (|={E1,E2}=> P) ⊢ |={E1,E2}=> Q.
Proof. eapply bi_fupd_mixin_fupd_mono, bi_fupd_mixin. Qed.
(* iris/bi/updates.v *)
Lemma fupd_trans E1 E2 E3 (P : PROP) : (|={E1,E2}=> |={E2,E3}=> P) ⊢ |={E1,E3}=> P.
Proof. eapply bi_fupd_mixin_fupd_trans, bi_fupd_mixin. Qed.
(* iris/bi/updates.v *)
Lemma fupd_mask_frame_r' E1 E2 Ef (P : PROP) :
    E1 ## Ef → (|={E1,E2}=> ⌜E2 ## Ef⌝ → P) ⊢ |={E1 ∪ Ef,E2 ∪ Ef}=> P.
Proof. eapply bi_fupd_mixin_fupd_mask_frame_r', bi_fupd_mixin. Qed.
(* iris/bi/updates.v *)
Lemma fupd_frame_r E1 E2 (P R : PROP) : (|={E1,E2}=> P) ∗ R ⊢ |={E1,E2}=> P ∗ R.
Proof. eapply bi_fupd_mixin_fupd_frame_r, bi_fupd_mixin. Qed.
(* iris/bi/updates.v *)
Instance bupd_proper :
    Proper ((≡) ==> (≡)) (bupd (PROP:=PROP))
:= ne_proper _.
(* iris/bi/updates.v *)
(* BUpd derived rules *)
Instance bupd_mono' : Proper ((⊢) ==> (⊢)) (bupd (PROP:=PROP)).
Proof. intros P Q; apply bupd_mono. Qed.
(* iris/bi/updates.v *)
Instance bupd_flip_mono' : Proper (flip (⊢) ==> flip (⊢)) (bupd (PROP:=PROP)).
Proof. intros P Q; apply bupd_mono. Qed.
(* iris/bi/updates.v *)
Lemma bupd_frame_l R Q : (R ∗ |==> Q) ⊢ |==> R ∗ Q.
Proof. rewrite !(comm _ R); apply bupd_frame_r. Qed.
(* iris/bi/updates.v *)
Lemma bupd_wand_l P Q : (P -∗ Q) ∗ (|==> P) ⊢ |==> Q.
Proof. by rewrite bupd_frame_l wand_elim_l. Qed.
(* iris/bi/updates.v *)
Lemma bupd_wand_r P Q : (|==> P) ∗ (P -∗ Q) ⊢ |==> Q.
Proof. by rewrite bupd_frame_r wand_elim_r. Qed.
(* iris/bi/updates.v *)
Lemma bupd_sep P Q : (|==> P) ∗ (|==> Q) ⊢ |==> P ∗ Q.
Proof. by rewrite bupd_frame_r bupd_frame_l bupd_trans. Qed.
(* iris/bi/updates.v *)
Lemma bupd_idemp P : (|==> |==> P) ⊣⊢ |==> P.
Proof.
    apply: anti_symm.
    - apply bupd_trans.
    - apply bupd_intro.
  Qed.
(* iris/bi/updates.v *)
Instance bupd_sep_homomorphism :
    MonoidHomomorphism bi_sep bi_sep (flip (⊢)) (bupd (PROP:=PROP)).
Proof. split; [split|]; try apply _; [apply bupd_sep | apply bupd_intro]. Qed.
(* iris/bi/updates.v *)
Lemma bupd_or P Q : (|==> P) ∨ (|==> Q) ⊢ |==> (P ∨ Q).
Proof. apply or_elim; apply bupd_mono; [ apply or_intro_l | apply or_intro_r ]. Qed.
(* iris/bi/updates.v *)
Instance bupd_or_homomorphism :
    MonoidHomomorphism bi_or bi_or (flip (⊢)) (bupd (PROP:=PROP)).
Proof. split; [split|]; try apply _; [apply bupd_or | apply bupd_intro]. Qed.
(* iris/bi/updates.v *)
Lemma bupd_and P Q : (|==> (P ∧ Q)) ⊢ (|==> P) ∧ (|==> Q).
Proof. apply and_intro; apply bupd_mono; [apply and_elim_l | apply and_elim_r]. Qed.
(* iris/bi/updates.v *)
Lemma bupd_exist A (Φ : A → PROP) : (∃ x : A, |==> Φ x) ⊢ |==> ∃ x : A, Φ x.
Proof. apply exist_elim=> a. by rewrite -(exist_intro a). Qed.
(* iris/bi/updates.v *)
Lemma bupd_forall A (Φ : A → PROP) : (|==> ∀ x : A, Φ x) ⊢ ∀ x : A, |==> Φ x.
Proof. apply forall_intro=> a. by rewrite -(forall_elim a). Qed.
(* iris/bi/updates.v *)
Lemma big_sepL_bupd {A} (Φ : nat → A → PROP) l :
    ([∗ list] k↦x ∈ l, |==> Φ k x) ⊢ |==> [∗ list] k↦x ∈ l, Φ k x.
Proof. by rewrite (big_opL_commute _). Qed.
(* iris/bi/updates.v *)
Lemma big_sepM_bupd {A} `{Countable K} (Φ : K → A → PROP) l :
    ([∗ map] k↦x ∈ l, |==> Φ k x) ⊢ |==> [∗ map] k↦x ∈ l, Φ k x.
Proof. by rewrite (big_opM_commute _). Qed.
(* iris/bi/updates.v *)
Lemma big_sepM2_bupd {A B} `{Countable K} (Φ : K → A → B → PROP) l1 l2 :
    ([∗ map] k↦a;b ∈ l1;l2, |==> Φ k a b) ⊢ |==> [∗ map] k↦a;b ∈ l1;l2, Φ k a b.
Proof.
    rewrite !big_sepM2_alt big_sepM_bupd.
    rewrite !persistent_and_affinely_sep_l bupd_frame_l //.
  Qed.
(* iris/bi/updates.v *)
Lemma big_sepS_bupd `{Countable A} (Φ : A → PROP) l :
    ([∗ set]  x ∈ l, |==> Φ x) ⊢ |==> [∗ set] x ∈ l, Φ x.
Proof. by rewrite (big_opS_commute _). Qed.
(* iris/bi/updates.v *)
Lemma big_sepMS_bupd `{Countable A} (Φ : A → PROP) l :
    ([∗ mset] x ∈ l, |==> Φ x) ⊢ |==> [∗ mset] x ∈ l, Φ x.
Proof. by rewrite (big_opMS_commute _). Qed.
(* iris/bi/updates.v *)
Lemma except_0_bupd P : ◇ (|==> P) ⊢ (|==> ◇ P).
Proof.
    rewrite /bi_except_0. apply or_elim; eauto using bupd_mono, or_intro_r.
    by rewrite -bupd_intro -or_intro_l.
  Qed.
(* iris/bi/updates.v *)
Instance bupd_absorbing P :
    Absorbing P → Absorbing (|==> P).
Proof. rewrite /Absorbing /bi_absorbingly bupd_frame_l =>-> //. Qed.
(* iris/bi/updates.v *)
Lemma bupd_plainly P : (|==> ■ P) ⊢ ■ P.
Proof. apply bupd_si_pure. Qed.
(* iris/bi/updates.v *)
Lemma bupd_plainly_elim P `{!Absorbing P} : (|==> ■ P) ⊢ P.
Proof. by rewrite bupd_plainly plainly_elim. Qed.
(* iris/bi/updates.v *)
Lemma bupd_elim P `{!Plain P, !Absorbing P} : (|==> P) ⊢ P.
Proof.
      by rewrite {1}(plain P) /plainly bupd_si_pure si_pure_si_emp_valid_elim.
    Qed.
(* iris/bi/updates.v *)
Lemma bupd_plain_forall {A} (Φ : A → PROP)
        `{!∀ x, Plain (Φ x), !∀ x, Absorbing (Φ x)} :
      (|==> ∀ x, Φ x) ⊣⊢ (∀ x, |==> Φ x).
Proof.
      apply (anti_symm _).
      - apply bupd_forall.
      - rewrite -bupd_intro. apply forall_intro=> x.
        by rewrite (forall_elim x) bupd_elim.
    Qed.
(* iris/bi/updates.v *)
Instance bupd_plain P : Plain P → Plain (|==> P).
Proof.
      intros. rewrite /Plain. rewrite {1}(plain P) {1}bupd_elim.
      by rewrite -bupd_intro.
    Qed.
(* iris/bi/updates.v *)
Instance fupd_proper E1 E2 :
    Proper ((≡) ==> (≡)) (fupd (PROP:=PROP) E1 E2)
:= ne_proper _.
(* iris/bi/updates.v *)
(* FUpd derived rules *)
Instance fupd_mono' E1 E2 : Proper ((⊢) ==> (⊢)) (fupd (PROP:=PROP) E1 E2).
Proof. intros P Q; apply fupd_mono. Qed.
(* iris/bi/updates.v *)
Instance fupd_flip_mono' E1 E2 :
    Proper (flip (⊢) ==> flip (⊢)) (fupd (PROP:=PROP) E1 E2).
Proof. intros P Q; apply fupd_mono. Qed.
(* iris/bi/updates.v *)
Lemma fupd_mask_intro_subseteq E1 E2 P :
    E2 ⊆ E1 → P ⊢ |={E1,E2}=> |={E2,E1}=> P.
Proof.
    intros HE.
    apply wand_entails', wand_intro_r.
    rewrite fupd_mask_subseteq; last exact: HE.
    rewrite !fupd_frame_r. rewrite left_id. done.
  Qed.
(* iris/bi/updates.v *)
Lemma fupd_intro E P : P ⊢ |={E}=> P.
Proof. by rewrite {1}(fupd_mask_intro_subseteq E E P) // fupd_trans. Qed.
(* iris/bi/updates.v *)
Lemma fupd_except_0 E1 E2 P : (|={E1,E2}=> ◇ P) ⊢ |={E1,E2}=> P.
Proof. by rewrite {1}(fupd_intro E2 P) except_0_fupd fupd_trans. Qed.
(* iris/bi/updates.v *)
Lemma fupd_idemp E P : (|={E}=> |={E}=> P) ⊣⊢ |={E}=> P.
Proof.
    apply: anti_symm.
    - apply fupd_trans.
    - apply fupd_intro.
  Qed.
(* iris/bi/updates.v *)
(* Weaken the first mask of the goal from [E1] to [E2].
      This lemma is intended to be [iApply]ed.
      However, usually you can [iMod (fupd_mask_subseteq E2)] instead and that
      will be slightly more convenient. *)
Lemma fupd_mask_weaken {E1} E2 {E3 P} :
    E2 ⊆ E1 →
    ((|={E2,E1}=> emp) ={E2,E3}=∗ P) ⊢ |={E1,E3}=> P.
Proof.
    intros HE.
    apply wand_entails', wand_intro_r.
    rewrite {1}(fupd_mask_subseteq E2) //.
    rewrite fupd_frame_r. by rewrite wand_elim_r fupd_trans.
  Qed.
(* iris/bi/updates.v *)
(* Introduction lemma for a mask-changing fupd.
      This lemma is intended to be [iApply]ed. *)
Lemma fupd_mask_intro E1 E2 P :
    E2 ⊆ E1 →
    ((|={E2,E1}=> emp) -∗ P) ⊢ |={E1,E2}=> P.
Proof.
    intros. etrans; [|by apply fupd_mask_weaken]. by rewrite -fupd_intro.
  Qed.
(* iris/bi/updates.v *)
Lemma fupd_mask_intro_discard E1 E2 P `{!Absorbing P} :
    E2 ⊆ E1 → P ⊢ |={E1,E2}=> P.
Proof.
    intros. etrans; [|by apply fupd_mask_intro].
    apply wand_intro_r. rewrite sep_elim_l. done.
  Qed.
(* iris/bi/updates.v *)
Lemma fupd_frame_l E1 E2 R Q : (R ∗ |={E1,E2}=> Q) ⊢ |={E1,E2}=> R ∗ Q.
Proof. rewrite !(comm _ R); apply fupd_frame_r. Qed.
(* iris/bi/updates.v *)
Lemma fupd_wand_l E1 E2 P Q : (P -∗ Q) ∗ (|={E1,E2}=> P) ⊢ |={E1,E2}=> Q.
Proof. by rewrite fupd_frame_l wand_elim_l. Qed.
(* iris/bi/updates.v *)
Lemma fupd_wand_r E1 E2 P Q : (|={E1,E2}=> P) ∗ (P -∗ Q) ⊢ |={E1,E2}=> Q.
Proof. by rewrite fupd_frame_r wand_elim_r. Qed.
(* iris/bi/updates.v *)
Instance fupd_absorbing E1 E2 P :
    Absorbing P → Absorbing (|={E1,E2}=> P).
Proof. rewrite /Absorbing /bi_absorbingly fupd_frame_l =>-> //. Qed.
(* iris/bi/updates.v *)
Lemma fupd_trans_frame E1 E2 E3 P Q :
    ((Q ={E2,E3}=∗ emp) ∗ |={E1,E2}=> (Q ∗ P)) ⊢ |={E1,E3}=> P.
Proof.
    rewrite fupd_frame_l assoc -(comm _ Q) wand_elim_r.
    by rewrite fupd_frame_r left_id fupd_trans.
  Qed.
(* iris/bi/updates.v *)
Lemma fupd_elim E1 E2 E3 P Q :
    (Q ⊢ (|={E2,E3}=> P)) → (|={E1,E2}=> Q) ⊢ (|={E1,E3}=> P).
Proof. intros ->. rewrite fupd_trans //. Qed.
(* iris/bi/updates.v *)
Lemma fupd_mask_frame_r E1 E2 Ef P :
    E1 ## Ef → (|={E1,E2}=> P) ⊢ |={E1 ∪ Ef,E2 ∪ Ef}=> P.
Proof.
    intros ?. rewrite -fupd_mask_frame_r' //. f_equiv.
    apply impl_intro_l, and_elim_r.
  Qed.