(* iris/bi/derived_laws.v *)
From iris.algebra Require Import monoid
From iris.bi Require Export extensions
From iris.prelude Require Import options

Local HintExtern 100 (NonExpansive _) => solve_proper : core.

Global Instanceentails_anti_sym : AntiSymm (⊣⊢) (@bi_entails PROP).
Proof. intros P Q ??. by apply equiv_entails. Qed.

Lemma equiv_entails_1_1P Q : (P ⊣⊢ Q) → (P ⊢ Q).
Proof. apply equiv_entails. Qed.

Lemma equiv_entails_1_2P Q : (P ⊣⊢ Q) → (Q ⊢ P).
Proof. apply equiv_entails. Qed.

Lemma equiv_entails_2P Q : (P ⊢ Q) → (Q ⊢ P) → (P ⊣⊢ Q).
Proof. intros. by apply equiv_entails. Qed.

Global Instanceentails_proper :
  Proper ((⊣⊢) ==> (⊣⊢) ==> iff) ((⊢) : relation PROP).
Proof.
  move => P1 P2 /equiv_entails [HP1 HP2] Q1 Q2 /equiv_entails [HQ1 HQ2]; split=>?.
  - by trans P1; [|trans Q1].
  - by trans P2; [|trans Q2].
Qed.

Lemma entails_equiv_lP Q R : (P ⊣⊢ Q) → (Q ⊢ R) → (P ⊢ R).
Proof. by intros ->. Qed.

Lemma entails_equiv_rP Q R : (P ⊢ Q) → (Q ⊣⊢ R) → (P ⊢ R).
Proof. by intros ? <-. Qed.

Global Instancebi_emp_valid_proper : Proper ((⊣⊢) ==> iff) (@bi_emp_valid PROP).
Proof. solve_proper. Qed.

Global Instancebi_emp_valid_mono : Proper ((⊢) ==> impl) (@bi_emp_valid PROP).
Proof. solve_proper. Qed.

Global Instancebi_emp_valid_flip_mono :
  Proper (flip (⊢) ==> flip impl) (@bi_emp_valid PROP).
Proof. solve_proper. Qed.

Global Instancepure_proper : Proper (iff ==> (⊣⊢)) (@bi_pure PROP) | 0.
Proof. intros φ1 φ2 Hφ. apply equiv_dist=> n. by apply pure_ne. Qed.

Global Instanceand_proper :
  Proper ((⊣⊢) ==> (⊣⊢) ==> (⊣⊢)) (@bi_and PROP) := ne_proper_2 _.

Global Instanceor_proper :
  Proper ((⊣⊢) ==> (⊣⊢) ==> (⊣⊢)) (@bi_or PROP) := ne_proper_2 _.

Global Instanceimpl_proper :
  Proper ((⊣⊢) ==> (⊣⊢) ==> (⊣⊢)) (@bi_impl PROP) := ne_proper_2 _.

Global Instancesep_proper :
  Proper ((⊣⊢) ==> (⊣⊢) ==> (⊣⊢)) (@bi_sep PROP) := ne_proper_2 _.

Global Instancewand_proper :
  Proper ((⊣⊢) ==> (⊣⊢) ==> (⊣⊢)) (@bi_wand PROP) := ne_proper_2 _.

Global Instanceforall_proper A :
  Proper (pointwise_relation _ (⊣⊢) ==> (⊣⊢)) (@bi_forall PROP A).
Proof.
  intros Φ1 Φ2 HΦ. apply equiv_dist=> n.
  apply forall_ne=> x. apply equiv_dist, HΦ.
Qed.

Global Instanceexist_proper A :
  Proper (pointwise_relation _ (⊣⊢) ==> (⊣⊢)) (@bi_exist PROP A).
Proof.
  intros Φ1 Φ2 HΦ. apply equiv_dist=> n.
  apply exist_ne=> x. apply equiv_dist, HΦ.
Qed.

Global Instancepersistently_proper :
  Proper ((⊣⊢) ==> (⊣⊢)) (@bi_persistently PROP) := ne_proper _.

Lemma and_elim_l'P Q R : (P ⊢ R) → P ∧ Q ⊢ R.
Proof. by rewrite and_elim_l. Qed.

Lemma and_elim_r'P Q R : (Q ⊢ R) → P ∧ Q ⊢ R.
Proof. by rewrite and_elim_r. Qed.

Lemma or_intro_l'P Q R : (P ⊢ Q) → P ⊢ Q ∨ R.
Proof. intros ->; apply or_intro_l. Qed.

Lemma or_intro_r'P Q R : (P ⊢ R) → P ⊢ Q ∨ R.
Proof. intros ->; apply or_intro_r. Qed.

Lemma exist_intro'{A} P (Ψ : A → PROP) a : (P ⊢ Ψ a) → P ⊢ ∃ a, Ψ a.
Proof. intros ->; apply exist_intro. Qed.

Lemma forall_elim'{A} P (Ψ : A → PROP) : (P ⊢ ∀ a, Ψ a) → ∀ a, P ⊢ Ψ a.
Proof. move=> HP a. by rewrite HP forall_elim. Qed.

Local HintResolve pure_intro forall_intro : core.

Local HintResolve or_elim or_intro_l' or_intro_r' : core.

Local HintResolve and_intro and_elim_l' and_elim_r' : core.

Lemma impl_intro_lP Q R : (Q ∧ P ⊢ R) → P ⊢ Q → R.
Proof. intros HR; apply impl_intro_r; rewrite -HR; auto. Qed.

Lemma impl_elimP Q R : (P ⊢ Q → R) → (P ⊢ Q) → P ⊢ R.
Proof. intros. rewrite -(impl_elim_l' P Q R); auto. Qed.

Lemma impl_elim_r'P Q R : (Q ⊢ P → R) → P ∧ Q ⊢ R.
Proof. intros; apply impl_elim with P; auto. Qed.

Lemma impl_elim_lP Q : (P → Q) ∧ P ⊢ Q.
Proof. by apply impl_elim_l'. Qed.

Lemma impl_elim_rP Q : P ∧ (P → Q) ⊢ Q.
Proof. by apply impl_elim_r'. Qed.

Lemma False_elimP : False ⊢ P.
Proof. by apply (pure_elim' False). Qed.

Lemma True_introP : P ⊢ True.
Proof. by apply pure_intro. Qed.

Local HintImmediate False_elim : core.

Lemma entails_eq_TrueP Q : (P ⊢ Q) ↔ ((P → Q)%I ≡ True%I).
Proof.
  split=>EQ.
  - apply bi.equiv_entails; split; [by apply True_intro|].
    apply impl_intro_r. rewrite and_elim_r //.
  - trans (P ∧ True)%I.
    + apply and_intro; first done. by apply pure_intro.
    + rewrite -EQ impl_elim_r. done.
Qed.

Lemma entails_impl_TrueP Q : (P ⊢ Q) ↔ (True ⊢ (P → Q)).
Proof. rewrite entails_eq_True equiv_entails; naive_solver. Qed.

Lemma and_monoP P' Q Q' : (P ⊢ Q) → (P' ⊢ Q') → P ∧ P' ⊢ Q ∧ Q'.
Proof. auto. Qed.

Lemma and_mono_lP P' Q : (P ⊢ Q) → P ∧ P' ⊢ Q ∧ P'.
Proof. by intros; apply and_mono. Qed.

Lemma and_mono_rP P' Q' : (P' ⊢ Q') → P ∧ P' ⊢ P ∧ Q'.
Proof. by apply and_mono. Qed.

Lemma or_monoP P' Q Q' : (P ⊢ Q) → (P' ⊢ Q') → P ∨ P' ⊢ Q ∨ Q'.
Proof. auto. Qed.

Lemma or_mono_lP P' Q : (P ⊢ Q) → P ∨ P' ⊢ Q ∨ P'.
Proof. by intros; apply or_mono. Qed.

Lemma or_mono_rP P' Q' : (P' ⊢ Q') → P ∨ P' ⊢ P ∨ Q'.
Proof. by apply or_mono. Qed.

Lemma impl_monoP P' Q Q' : (Q ⊢ P) → (P' ⊢ Q') → (P → P') ⊢ Q → Q'.
Proof.
  intros HP HQ'; apply impl_intro_l; rewrite -HQ'.
  apply impl_elim with P; eauto.
Qed.

Lemma forall_mono{A} (Φ Ψ : A → PROP) :
  (∀ a, Φ a ⊢ Ψ a) → (∀ a, Φ a) ⊢ ∀ a, Ψ a.
Proof.
  intros HP. apply forall_intro=> a; rewrite -(HP a); apply forall_elim.
Qed.

Lemma exist_mono{A} (Φ Ψ : A → PROP) :
  (∀ a, Φ a ⊢ Ψ a) → (∃ a, Φ a) ⊢ ∃ a, Ψ a.
Proof. intros HΦ. apply exist_elim=> a; rewrite (HΦ a); apply exist_intro. Qed.

Global Instanceand_mono' : Proper ((⊢) ==> (⊢) ==> (⊢)) (@bi_and PROP).
Proof. by intros P P' HP Q Q' HQ; apply and_mono. Qed.

Global Instanceand_flip_mono' :
  Proper (flip (⊢) ==> flip (⊢) ==> flip (⊢)) (@bi_and PROP).
Proof. by intros P P' HP Q Q' HQ; apply and_mono. Qed.

Global Instanceor_mono' : Proper ((⊢) ==> (⊢) ==> (⊢)) (@bi_or PROP).
Proof. by intros P P' HP Q Q' HQ; apply or_mono. Qed.

Global Instanceor_flip_mono' :
  Proper (flip (⊢) ==> flip (⊢) ==> flip (⊢)) (@bi_or PROP).
Proof. by intros P P' HP Q Q' HQ; apply or_mono. Qed.

Global Instanceimpl_mono' :
  Proper (flip (⊢) ==> (⊢) ==> (⊢)) (@bi_impl PROP).
Proof. by intros P P' HP Q Q' HQ; apply impl_mono. Qed.

Global Instanceimpl_flip_mono' :
  Proper ((⊢) ==> flip (⊢) ==> flip (⊢)) (@bi_impl PROP).
Proof. by intros P P' HP Q Q' HQ; apply impl_mono. Qed.

Global Instanceforall_mono' A :
  Proper (pointwise_relation _ (⊢) ==> (⊢)) (@bi_forall PROP A).
Proof. intros P1 P2; apply forall_mono. Qed.

Global Instanceforall_flip_mono' A :
  Proper (pointwise_relation _ (flip (⊢)) ==> flip (⊢)) (@bi_forall PROP A).
Proof. intros P1 P2; apply forall_mono. Qed.

Global Instanceexist_mono' A :
  Proper (pointwise_relation _ ((⊢)) ==> (⊢)) (@bi_exist PROP A).
Proof. intros P1 P2; apply exist_mono. Qed.

Global Instanceexist_flip_mono' A :
  Proper (pointwise_relation _ (flip (⊢)) ==> flip (⊢)) (@bi_exist PROP A).
Proof. intros P1 P2; apply exist_mono. Qed.

Global Instanceand_idem : IdemP (⊣⊢) (@bi_and PROP).
Proof. intros P; apply (anti_symm (⊢)); auto. Qed.

Global Instanceor_idem : IdemP (⊣⊢) (@bi_or PROP).
Proof. intros P; apply (anti_symm (⊢)); auto. Qed.

Global Instanceand_comm : Comm (⊣⊢) (@bi_and PROP).
Proof. intros P Q; apply (anti_symm (⊢)); auto. Qed.

Global InstanceTrue_and : LeftId (⊣⊢) True%I (@bi_and PROP).
Proof. intros P; apply (anti_symm (⊢)); auto. Qed.

Global Instanceand_True : RightId (⊣⊢) True%I (@bi_and PROP).
Proof. intros P; apply (anti_symm (⊢)); auto. Qed.

Global InstanceFalse_and : LeftAbsorb (⊣⊢) False%I (@bi_and PROP).
Proof. intros P; apply (anti_symm (⊢)); auto. Qed.

Global Instanceand_False : RightAbsorb (⊣⊢) False%I (@bi_and PROP).
Proof. intros P; apply (anti_symm (⊢)); auto. Qed.

Global InstanceTrue_or : LeftAbsorb (⊣⊢) True%I (@bi_or PROP).
Proof. intros P; apply (anti_symm (⊢)); auto. Qed.

Global Instanceor_True : RightAbsorb (⊣⊢) True%I (@bi_or PROP).
Proof. intros P; apply (anti_symm (⊢)); auto. Qed.

Global InstanceFalse_or : LeftId (⊣⊢) False%I (@bi_or PROP).
Proof. intros P; apply (anti_symm (⊢)); auto. Qed.

Global Instanceor_False : RightId (⊣⊢) False%I (@bi_or PROP).
Proof. intros P; apply (anti_symm (⊢)); auto. Qed.

Global Instanceand_assoc : Assoc (⊣⊢) (@bi_and PROP).
Proof. intros P Q R; apply (anti_symm (⊢)); auto. Qed.

Global Instanceor_comm : Comm (⊣⊢) (@bi_or PROP).
Proof. intros P Q; apply (anti_symm (⊢)); auto. Qed.

Global Instanceor_assoc : Assoc (⊣⊢) (@bi_or PROP).
Proof. intros P Q R; apply (anti_symm (⊢)); auto. Qed.

Global InstanceTrue_impl : LeftId (⊣⊢) True%I (@bi_impl PROP).
Proof.
  intros P; apply (anti_symm (⊢)).
  - by rewrite -(left_id True%I (∧)%I (_ → _)%I) impl_elim_r.
  - by apply impl_intro_l; rewrite left_id.
Qed.

Lemma impl_reflP Q : Q ⊢ P → P.
Proof. apply impl_intro_l, and_elim_l. Qed.

Lemma impl_transP Q R : (P → Q) ∧ (Q → R) ⊢ (P → R).
Proof. apply impl_intro_l. by rewrite assoc !impl_elim_r. Qed.

Lemma False_implP : (False → P) ⊣⊢ True.
Proof.
  apply (anti_symm (⊢)); [by auto|].
  apply impl_intro_l. rewrite left_absorb. auto.
Qed.

Lemma exist_impl_forall{A} P (Ψ : A → PROP) :
  ((∃ x : A, Ψ x) → P) ⊣⊢ ∀ x : A, Ψ x → P.
Proof.
  apply equiv_entails; split.
  - apply forall_intro=>x. by rewrite -exist_intro.
  - apply impl_intro_r, impl_elim_r', exist_elim=>x.
    apply impl_intro_r. by rewrite (forall_elim x) impl_elim_r.
Qed.

Lemma forall_unit(Ψ : unit → PROP) :
  (∀ x, Ψ x) ⊣⊢ Ψ ().
Proof.
  apply (anti_symm (⊢)).
  - rewrite (forall_elim ()) //.
  - apply forall_intro=>[[]]. done.
Qed.

Lemma exist_unit(Ψ : unit → PROP) :
  (∃ x, Ψ x) ⊣⊢ Ψ ().
Proof.
  apply (anti_symm (⊢)).
  - apply exist_elim=>[[]]. done.
  - rewrite -(exist_intro ()). done.
Qed.

Lemma exist_exist{A B} (Ψ : A → B → PROP) :
  (∃ x y, Ψ x y) ⊣⊢ (∃ y x, Ψ x y).
Proof.
  apply (anti_symm (⊢));
    do 2 (apply exist_elim=>?); rewrite -2!exist_intro; eauto.
Qed.

Lemma forall_forall{A B} (Ψ : A → B → PROP) :
  (∀ x y, Ψ x y) ⊣⊢ (∀ y x, Ψ x y).
Proof.
  apply (anti_symm (⊢));
    do 2 (apply forall_intro=>?); rewrite 2!forall_elim; eauto.
Qed.

Lemma exist_forall{A B} (Ψ : A → B → PROP) :
  (∃ x, ∀ y, Ψ x y) ⊢ (∀ y, ∃ x, Ψ x y).
Proof.
  apply forall_intro=>?. apply exist_elim=>?.
  rewrite -exist_intro forall_elim ; eauto.
Qed.

Lemma impl_curryP Q R : (P → Q → R) ⊣⊢ (P ∧ Q → R).
Proof.
  apply (anti_symm _).
  - apply impl_intro_l. by rewrite (comm _ P) -and_assoc !impl_elim_r.
  - do 2 apply impl_intro_l. by rewrite assoc (comm _ Q) impl_elim_r.
Qed.

Lemma or_and_lP Q R : P ∨ Q ∧ R ⊣⊢ (P ∨ Q) ∧ (P ∨ R).
Proof.
  apply (anti_symm (⊢)); first auto.
  do 2 (apply impl_elim_l', or_elim; apply impl_intro_l); auto.
Qed.

Lemma or_and_rP Q R : P ∧ Q ∨ R ⊣⊢ (P ∨ R) ∧ (Q ∨ R).
Proof. by rewrite -!(comm _ R) or_and_l. Qed.

Lemma and_or_lP Q R : P ∧ (Q ∨ R) ⊣⊢ P ∧ Q ∨ P ∧ R.
Proof.
  apply (anti_symm (⊢)); last auto.
  apply impl_elim_r', or_elim; apply impl_intro_l; auto.
Qed.

Lemma and_or_rP Q R : (P ∨ Q) ∧ R ⊣⊢ P ∧ R ∨ Q ∧ R.
Proof. by rewrite -!(comm _ R) and_or_l. Qed.

Lemma and_exist_l{A} P (Ψ : A → PROP) : P ∧ (∃ a, Ψ a) ⊣⊢ ∃ a, P ∧ Ψ a.
Proof.
  apply (anti_symm (⊢)).
  - apply impl_elim_r'. apply exist_elim=>a. apply impl_intro_l.
    by rewrite -(exist_intro a).
  - apply exist_elim=>a. apply and_intro; first by rewrite and_elim_l.
    by rewrite -(exist_intro a) and_elim_r.
Qed.

Lemma and_exist_r{A} P (Φ: A → PROP) : (∃ a, Φ a) ∧ P ⊣⊢ ∃ a, Φ a ∧ P.
Proof.
  rewrite -(comm _ P) and_exist_l. apply exist_proper=>a. by rewrite comm.
Qed.

Lemma or_exist{A} (Φ Ψ : A → PROP) :
  (∃ a, Φ a ∨ Ψ a) ⊣⊢ (∃ a, Φ a) ∨ (∃ a, Ψ a).
Proof.
  apply (anti_symm (⊢)).
  - apply exist_elim=> a. by rewrite -!(exist_intro a).
  - apply or_elim; apply exist_elim=> a; rewrite -(exist_intro a); auto.
Qed.

Lemma and_altP Q : P ∧ Q ⊣⊢ ∀ b : bool, if b then P else Q.
Proof.
   apply (anti_symm _); first apply forall_intro=> -[]; auto.
   by apply and_intro; [rewrite (forall_elim true)|rewrite (forall_elim false)].
Qed.

Lemma or_altP Q : P ∨ Q ⊣⊢ ∃ b : bool, if b then P else Q.
Proof.
  apply (anti_symm _); last apply exist_elim=> -[]; auto.
  by apply or_elim; [rewrite -(exist_intro true)|rewrite -(exist_intro false)].
Qed.

Lemma entails_equiv_andP Q : (P ⊣⊢ Q ∧ P) ↔ (P ⊢ Q).
Proof.
  split.
  - intros ->; auto.
  - intros; apply (anti_symm _); auto.
Qed.

Global Instanceiff_ne : NonExpansive2 (@bi_iff PROP).
Proof. unfold bi_iff; solve_proper. Qed.

Global Instanceiff_proper :
  Proper ((⊣⊢) ==> (⊣⊢) ==> (⊣⊢)) (@bi_iff PROP) := ne_proper_2 _.

Lemma iff_reflQ P : Q ⊢ P ↔ P.
Proof. rewrite /bi_iff. apply and_intro; apply impl_refl. Qed.

Lemma iff_symP Q : (P ↔ Q) ⊣⊢ (Q ↔ P).
Proof.
  apply equiv_entails. split; apply and_intro;
    try apply and_elim_r; apply and_elim_l.
Qed.

Lemma iff_transP Q R : (P ↔ Q) ∧ (Q ↔ R) ⊢ (P ↔ R).
Proof.
  apply and_intro.
  - rewrite /bi_iff (and_elim_l _ (_ → _)) (and_elim_l _ (_ → _)).
    apply impl_trans.
  - rewrite /bi_iff (and_elim_r _ (_ → _)) (and_elim_r _ (_ → _)) comm.
    apply impl_trans.
Qed.

Local HintResolve sep_mono : core.

Lemma sep_mono_lP P' Q : (P ⊢ Q) → P ∗ P' ⊢ Q ∗ P'.
Proof. by intros; apply sep_mono. Qed.

Lemma sep_mono_rP P' Q' : (P' ⊢ Q') → P ∗ P' ⊢ P ∗ Q'.
Proof. by apply sep_mono. Qed.

Global Instancesep_mono' : Proper ((⊢) ==> (⊢) ==> (⊢)) (@bi_sep PROP).
Proof. by intros P P' HP Q Q' HQ; apply sep_mono. Qed.

Global Instancesep_flip_mono' :
  Proper (flip (⊢) ==> flip (⊢) ==> flip (⊢)) (@bi_sep PROP).
Proof. by intros P P' HP Q Q' HQ; apply sep_mono. Qed.

Lemma wand_monoP P' Q Q' : (Q ⊢ P) → (P' ⊢ Q') → (P -∗ P') ⊢ Q -∗ Q'.
Proof.
  intros HP HQ; apply wand_intro_r. rewrite HP -HQ. by apply wand_elim_l'.
Qed.

Global Instancewand_mono' : Proper (flip (⊢) ==> (⊢) ==> (⊢)) (@bi_wand PROP).
Proof. by intros P P' HP Q Q' HQ; apply wand_mono. Qed.

Global Instancewand_flip_mono' :
  Proper ((⊢) ==> flip (⊢) ==> flip (⊢)) (@bi_wand PROP).
Proof. by intros P P' HP Q Q' HQ; apply wand_mono. Qed.

Global Instancesep_comm : Comm (⊣⊢) (@bi_sep PROP).
Proof. intros P Q; apply (anti_symm _); auto using sep_comm'. Qed.

Global Instancesep_assoc : Assoc (⊣⊢) (@bi_sep PROP).
Proof.
  intros P Q R; apply (anti_symm _); auto using sep_assoc'.
  by rewrite !(comm _ P) !(comm _ _ R) sep_assoc'.
Qed.

Global Instanceemp_sep : LeftId (⊣⊢) emp%I (@bi_sep PROP).
Proof. intros P; apply (anti_symm _); auto using emp_sep_1, emp_sep_2. Qed.

Global Instancesep_emp : RightId (⊣⊢) emp%I (@bi_sep PROP).
Proof. by intros P; rewrite comm left_id. Qed.

Global Instancesep_False : LeftAbsorb (⊣⊢) False%I (@bi_sep PROP).
Proof. intros P; apply (anti_symm _); auto using wand_elim_l'. Qed.

Global InstanceFalse_sep : RightAbsorb (⊣⊢) False%I (@bi_sep PROP).
Proof. intros P. by rewrite comm left_absorb. Qed.

Lemma True_sep_2P : P ⊢ True ∗ P.
Proof. rewrite -{1}[P](left_id emp%I bi_sep). auto using sep_mono. Qed.

Lemma sep_True_2P : P ⊢ P ∗ True.
Proof. by rewrite comm -True_sep_2. Qed.

Lemma sep_intro_emp_valid_lP Q R : (⊢ P) → (R ⊢ Q) → R ⊢ P ∗ Q.
Proof. intros ? ->. rewrite -{1}(left_id emp%I _ Q). by apply sep_mono. Qed.

Lemma sep_intro_emp_valid_rP Q R : (R ⊢ P) → (⊢ Q) → R ⊢ P ∗ Q.
Proof. intros -> ?. rewrite comm. by apply sep_intro_emp_valid_l. Qed.

Lemma sep_elim_emp_valid_lP Q R : (⊢ P) → (P ∗ R ⊢ Q) → R ⊢ Q.
Proof. intros <- <-. by rewrite left_id. Qed.

Lemma sep_elim_emp_valid_rP Q R : (⊢P) → (R ∗ P ⊢ Q) → R ⊢ Q.
Proof. intros <- <-. by rewrite right_id. Qed.

Lemma wand_intro_lP Q R : (Q ∗ P ⊢ R) → P ⊢ Q -∗ R.
Proof. rewrite comm; apply wand_intro_r. Qed.

Lemma wand_elim_lP Q : (P -∗ Q) ∗ P ⊢ Q.
Proof. by apply wand_elim_l'. Qed.

Lemma wand_elim_rP Q : P ∗ (P -∗ Q) ⊢ Q.
Proof. rewrite (comm _ P); apply wand_elim_l. Qed.

Lemma wand_elim_r'P Q R : (Q ⊢ P -∗ R) → P ∗ Q ⊢ R.
Proof. intros ->; apply wand_elim_r. Qed.

Lemma wand_applyP Q R S : (P ⊢ Q -∗ R) → (S ⊢ P ∗ Q) → S ⊢ R.
Proof. intros HR%wand_elim_l' HQ. by rewrite HQ. Qed.

Lemma wand_frame_lP Q R : (Q -∗ R) ⊢ P ∗ Q -∗ P ∗ R.
Proof. apply wand_intro_l. rewrite -assoc. apply sep_mono_r, wand_elim_r. Qed.

Lemma wand_frame_rP Q R : (Q -∗ R) ⊢ Q ∗ P -∗ R ∗ P.
Proof.
  apply wand_intro_l. rewrite ![(_ ∗ P)%I]comm -assoc.
  apply sep_mono_r, wand_elim_r.
Qed.

Global Instanceemp_wand : LeftId (⊣⊢) emp%I (@bi_wand PROP).
Proof.
  intros P. apply (anti_symm _).
  - by rewrite -[(emp -∗ P)%I]left_id wand_elim_r.
  - apply wand_intro_l. by rewrite left_id.
Qed.

Lemma False_wandP : (False -∗ P) ⊣⊢ True.
Proof.
  apply (anti_symm (⊢)); [by auto|].
  apply wand_intro_l. rewrite left_absorb. auto.
Qed.

Lemma wand_reflP : ⊢ P -∗ P.
Proof. apply wand_intro_l. by rewrite right_id. Qed.

Lemma wand_transP Q R : (P -∗ Q) ∗ (Q -∗ R) ⊢ (P -∗ R).
Proof. apply wand_intro_l. by rewrite assoc !wand_elim_r. Qed.

Lemma wand_curryP Q R : (P -∗ Q -∗ R) ⊣⊢ (P ∗ Q -∗ R).
Proof.
  apply (anti_symm _).
  - apply wand_intro_l. by rewrite (comm _ P) -assoc !wand_elim_r.
  - do 2 apply wand_intro_l. by rewrite assoc (comm _ Q) wand_elim_r.
Qed.

Lemma sep_and_lP Q R : P ∗ (Q ∧ R) ⊢ (P ∗ Q) ∧ (P ∗ R).
Proof. auto. Qed.

Lemma sep_and_rP Q R : (P ∧ Q) ∗ R ⊢ (P ∗ R) ∧ (Q ∗ R).
Proof. auto. Qed.

Lemma sep_or_lP Q R : P ∗ (Q ∨ R) ⊣⊢ (P ∗ Q) ∨ (P ∗ R).
Proof.
  apply (anti_symm (⊢)); last by eauto 8.
  apply wand_elim_r', or_elim; apply wand_intro_l; auto.
Qed.

Lemma sep_or_rP Q R : (P ∨ Q) ∗ R ⊣⊢ (P ∗ R) ∨ (Q ∗ R).
Proof. by rewrite -!(comm _ R) sep_or_l. Qed.

Lemma sep_exist_l{A} P (Ψ : A → PROP) : P ∗ (∃ a, Ψ a) ⊣⊢ ∃ a, P ∗ Ψ a.
Proof.
  intros; apply (anti_symm (⊢)).
  - apply wand_elim_r', exist_elim=>a. apply wand_intro_l.
    by rewrite -(exist_intro a).
  - apply exist_elim=> a; apply sep_mono; auto using exist_intro.
Qed.

Lemma sep_exist_r{A} (Φ: A → PROP) Q: (∃ a, Φ a) ∗ Q ⊣⊢ ∃ a, Φ a ∗ Q.
Proof. setoid_rewrite (comm _ _ Q); apply sep_exist_l. Qed.

Lemma sep_forall_l{A} P (Ψ : A → PROP) : P ∗ (∀ a, Ψ a) ⊢ ∀ a, P ∗ Ψ a.
Proof. by apply forall_intro=> a; rewrite forall_elim. Qed.

Lemma sep_forall_r{A} (Φ : A → PROP) Q : (∀ a, Φ a) ∗ Q ⊢ ∀ a, Φ a ∗ Q.
Proof. by apply forall_intro=> a; rewrite forall_elim. Qed.

Lemma exist_wand_forall{A} P (Ψ : A → PROP) :
  ((∃ x : A, Ψ x) -∗ P) ⊣⊢ ∀ x : A, Ψ x -∗ P.
Proof.
  apply equiv_entails; split.
  - apply forall_intro=>x. by rewrite -exist_intro.
  - apply wand_intro_r, wand_elim_r', exist_elim=>x.
    apply wand_intro_r. by rewrite (forall_elim x) wand_elim_r.
Qed.

Global Instancewand_iff_ne : NonExpansive2 (@bi_wand_iff PROP).
Proof. solve_proper. Qed.

Global Instancewand_iff_proper :
  Proper ((⊣⊢) ==> (⊣⊢) ==> (⊣⊢)) (@bi_wand_iff PROP) := ne_proper_2 _.

Lemma wand_iff_reflP : ⊢ P ∗-∗ P.
Proof. apply and_intro; apply wand_intro_l; by rewrite right_id. Qed.

Lemma wand_iff_symP Q : (P ∗-∗ Q) ⊣⊢ (Q ∗-∗ P).
Proof. apply equiv_entails; split; rewrite /bi_wand_iff; eauto. Qed.

Lemma wand_iff_transP Q R : (P ∗-∗ Q) ∗ (Q ∗-∗ R) ⊢ (P ∗-∗ R).
Proof.
  apply and_intro.
  - rewrite /bi_wand_iff !and_elim_l. apply wand_trans.
  - rewrite /bi_wand_iff !and_elim_r comm. apply wand_trans.
Qed.

Lemma wand_entailsP Q : (⊢ P -∗ Q) → P ⊢ Q.
Proof. intros. rewrite -[P]emp_sep. by apply wand_elim_l'. Qed.

Lemma entails_wandP Q : (P ⊢ Q) → ⊢ P -∗ Q.
Proof. intros ->. apply wand_intro_r. by rewrite left_id. Qed.

Lemma entails_wand'P Q : (P ⊢ Q) → emp ⊢ (P -∗ Q).
Proof. apply entails_wand. Qed.

Lemma wand_entails'P Q : (emp ⊢ (P -∗ Q)) → P ⊢ Q.
Proof. apply wand_entails. Qed.

Lemma equiv_wand_iffP Q : (P ⊣⊢ Q) → ⊢ P ∗-∗ Q.
Proof. intros ->; apply wand_iff_refl. Qed.

Lemma wand_iff_equivP Q : (⊢ P ∗-∗ Q) → (P ⊣⊢ Q).
Proof.
  intros HPQ; apply (anti_symm (⊢));
    apply wand_entails; rewrite /bi_emp_valid HPQ /bi_wand_iff; auto.
Qed.

Lemma entails_implP Q : (P ⊢ Q) → (⊢ P → Q).
Proof. intros ->. apply impl_intro_l. auto. Qed.

Lemma impl_entailsP Q `{!Affine P} : (⊢ P → Q) → P ⊢ Q.
Proof. intros HPQ. apply impl_elim with P=>//. by rewrite {1}(affine P). Qed.

Lemma equiv_iffP Q : (P ⊣⊢ Q) → (⊢ P ↔ Q).
Proof. intros ->; apply iff_refl. Qed.

Lemma iff_equivP Q `{!Affine P, !Affine Q} : (⊢ P ↔ Q)%I → (P ⊣⊢ Q).
Proof.
  intros HPQ; apply (anti_symm (⊢));
    apply: impl_entails; rewrite /bi_emp_valid HPQ /bi_iff; auto.
Qed.

Lemma and_parallelP1 P2 Q1 Q2 :
  (P1 ∧ P2) -∗ ((P1 -∗ Q1) ∧ (P2 -∗ Q2)) -∗ Q1 ∧ Q2.
Proof.
  apply entails_wand, wand_intro_r, and_intro.
  - rewrite !and_elim_l wand_elim_r. done.
  - rewrite !and_elim_r wand_elim_r. done.
Qed.

Lemma wandM_sound(mP : option PROP) Q :
  (mP -∗? Q) ⊣⊢ (default emp mP -∗ Q).
Proof. destruct mP; simpl; first done. rewrite emp_wand //. Qed.

Global Instanceaffinely_ne : NonExpansive (@bi_affinely PROP).
Proof. solve_proper. Qed.

Global Instanceaffinely_proper : Proper ((⊣⊢) ==> (⊣⊢)) (@bi_affinely PROP).
Proof. solve_proper. Qed.

Global Instanceaffinely_mono' : Proper ((⊢) ==> (⊢)) (@bi_affinely PROP).
Proof. solve_proper. Qed.

Global Instanceaffinely_flip_mono' :
  Proper (flip (⊢) ==> flip (⊢)) (@bi_affinely PROP).
Proof. solve_proper. Qed.

Lemma affinely_elim_empP : <affine> P ⊢ emp.
Proof. rewrite /bi_affinely; auto. Qed.

Global Instanceaffinely_affine P : Affine (<affine> P).
Proof. by rewrite /Affine affinely_elim_emp. Qed.

Lemma affinely_elimP : <affine> P ⊢ P.
Proof. rewrite /bi_affinely; auto. Qed.

Lemma affinely_monoP Q : (P ⊢ Q) → <affine> P ⊢ <affine> Q.
Proof. by intros ->. Qed.

Lemma affinely_idempP : <affine> <affine> P ⊣⊢ <affine> P.
Proof. by rewrite /bi_affinely assoc idemp. Qed.

Lemma affinely_intro'P Q : (<affine> P ⊢ Q) → <affine> P ⊢ <affine> Q.
Proof. intros <-. by rewrite affinely_idemp. Qed.

Lemma affinely_False: <affine> False ⊣⊢ False.
Proof. by rewrite /bi_affinely right_absorb. Qed.

Lemma affinely_emp: <affine> emp ⊣⊢ emp.
Proof. by rewrite /bi_affinely (idemp bi_and). Qed.

Lemma affinely_orP Q : <affine> (P ∨ Q) ⊣⊢ <affine> P ∨ <affine> Q.
Proof. by rewrite /bi_affinely and_or_l. Qed.

Lemma affinely_andP Q : <affine> (P ∧ Q) ⊣⊢ <affine> P ∧ <affine> Q.
Proof.
  rewrite /bi_affinely -(comm _ P) (assoc _ (_ ∧ _)%I) -!(assoc _ P).
  by rewrite idemp !assoc (comm _ P).
Qed.

Lemma affinely_sep_2P Q : <affine> P ∗ <affine> Q ⊢ <affine> (P ∗ Q).
Proof.
  rewrite /bi_affinely. apply and_intro.
  - by rewrite !and_elim_l right_id.
  - by rewrite !and_elim_r.
Qed.

Lemma affinely_sep`{!BiPositive PROP} P Q :
  <affine> (P ∗ Q) ⊣⊢ <affine> P ∗ <affine> Q.
Proof.
  apply (anti_symm _), affinely_sep_2.
  by rewrite -{1}affinely_idemp bi_positive !(comm _ (<affine> P)%I) bi_positive.
Qed.

Lemma affinely_forall{A} (Φ : A → PROP) :
  <affine> (∀ a, Φ a) ⊢ ∀ a, <affine> (Φ a).
Proof. apply forall_intro=> a. by rewrite (forall_elim a). Qed.

Lemma affinely_exist{A} (Φ : A → PROP) :
  <affine> (∃ a, Φ a) ⊣⊢ ∃ a, <affine> (Φ a).
Proof. by rewrite /bi_affinely and_exist_l. Qed.

Lemma affinely_True_emp: <affine> True ⊣⊢ emp.
Proof. apply (anti_symm _); rewrite /bi_affinely; auto. Qed.

Lemma affinely_and_lP Q : <affine> P ∧ Q ⊣⊢ <affine> (P ∧ Q).
Proof. by rewrite /bi_affinely assoc. Qed.

Lemma affinely_and_rP Q : P ∧ <affine> Q ⊣⊢ <affine> (P ∧ Q).
Proof. by rewrite /bi_affinely !assoc (comm _ P). Qed.

Lemma affinely_and_lrP Q : <affine> P ∧ Q ⊣⊢ P ∧ <affine> Q.
Proof. by rewrite affinely_and_l affinely_and_r. Qed.

Global Instanceemp_affine : Affine (PROP:=PROP) emp.
Proof. by rewrite /Affine. Qed.

Global InstanceFalse_affine : Affine (PROP:=PROP) False.
Proof. by rewrite /Affine False_elim. Qed.

Global Instanceand_affine_l P Q : Affine P → Affine (P ∧ Q).
Proof. rewrite /Affine=> ->; auto. Qed.

Global Instanceand_affine_r P Q : Affine Q → Affine (P ∧ Q).
Proof. rewrite /Affine=> ->; auto. Qed.

Global Instanceor_affine P Q : Affine P → Affine Q → Affine (P ∨ Q).
Proof.  rewrite /Affine=> -> ->; auto. Qed.

Global Instanceforall_affine `{Inhabited A} (Φ : A → PROP) :
  (∀ x, Affine (Φ x)) → Affine (∀ x, Φ x).
Proof. intros. rewrite /Affine (forall_elim inhabitant). apply: affine. Qed.

Global Instanceexist_affine {A} (Φ : A → PROP) :
  (∀ x, Affine (Φ x)) → Affine (∃ x, Φ x).
Proof. rewrite /Affine=> H. apply exist_elim=> a. by rewrite H. Qed.

Global Instancesep_affine P Q : Affine P → Affine Q → Affine (P ∗ Q).
Proof. rewrite /Affine=>-> ->. by rewrite left_id. Qed.

Global Instanceabsorbingly_ne : NonExpansive (@bi_absorbingly PROP).
Proof. solve_proper. Qed.

Global Instanceabsorbingly_proper : Proper ((⊣⊢) ==> (⊣⊢)) (@bi_absorbingly PROP).
Proof. solve_proper. Qed.

Global Instanceabsorbingly_mono' : Proper ((⊢) ==> (⊢)) (@bi_absorbingly PROP).
Proof. solve_proper. Qed.

Global Instanceabsorbingly_flip_mono' :
  Proper (flip (⊢) ==> flip (⊢)) (@bi_absorbingly PROP).
Proof. solve_proper. Qed.

Lemma absorbingly_introP : P ⊢ <absorb> P.
Proof. by rewrite /bi_absorbingly -True_sep_2. Qed.

Lemma absorbingly_monoP Q : (P ⊢ Q) → <absorb> P ⊢ <absorb> Q.
Proof. by intros ->. Qed.

Lemma absorbingly_idempP : <absorb> <absorb> P ⊣⊢ <absorb> P.
Proof.
  apply (anti_symm _), absorbingly_intro.
  rewrite /bi_absorbingly assoc. apply sep_mono; auto.
Qed.

Global Instanceabsorbingly_absorbing P : Absorbing (<absorb> P).
Proof. by rewrite /Absorbing absorbingly_idemp. Qed.

Lemma absorbingly_pureφ : <absorb> ⌜ φ ⌝ ⊣⊢ ⌜ φ ⌝.
Proof.
  apply (anti_symm _), absorbingly_intro.
  apply wand_elim_r', pure_elim'=> ?. apply wand_intro_l; auto.
Qed.

Lemma absorbingly_True: <absorb> True ⊣⊢ True.
Proof. apply absorbingly_pure. Qed.

Lemma absorbingly_orP Q : <absorb> (P ∨ Q) ⊣⊢ <absorb> P ∨ <absorb> Q.
Proof. by rewrite /bi_absorbingly sep_or_l. Qed.

Lemma absorbingly_and_1P Q : <absorb> (P ∧ Q) ⊢ <absorb> P ∧ <absorb> Q.
Proof. apply and_intro; apply absorbingly_mono; auto. Qed.

Lemma absorbingly_forall{A} (Φ : A → PROP) :
  <absorb> (∀ a, Φ a) ⊢ ∀ a, <absorb> (Φ a).
Proof. apply forall_intro=> a. by rewrite (forall_elim a). Qed.

Lemma absorbingly_exist{A} (Φ : A → PROP) :
  <absorb> (∃ a, Φ a) ⊣⊢ ∃ a, <absorb> (Φ a).
Proof. by rewrite /bi_absorbingly sep_exist_l. Qed.

Lemma absorbingly_sepP Q : <absorb> (P ∗ Q) ⊣⊢ <absorb> P ∗ <absorb> Q.
Proof.
  by rewrite -{1}absorbingly_idemp /bi_absorbingly !assoc -!(comm _ P) !assoc.
Qed.

Lemma absorbingly_emp_True: <absorb> emp ⊣⊢ True.
Proof. rewrite /bi_absorbingly right_id //. Qed.

Lemma absorbingly_wandP Q : <absorb> (P -∗ Q) ⊢ <absorb> P -∗ <absorb> Q.
Proof. apply wand_intro_l. by rewrite -absorbingly_sep wand_elim_r. Qed.

Lemma absorbingly_sep_lP Q : <absorb> P ∗ Q ⊣⊢ <absorb> (P ∗ Q).
Proof. by rewrite /bi_absorbingly assoc. Qed.

Lemma absorbingly_sep_rP Q : P ∗ <absorb> Q ⊣⊢ <absorb> (P ∗ Q).
Proof. by rewrite /bi_absorbingly !assoc (comm _ P). Qed.

Lemma absorbingly_sep_lrP Q : <absorb> P ∗ Q ⊣⊢ P ∗ <absorb> Q.
Proof. by rewrite absorbingly_sep_l absorbingly_sep_r. Qed.

Lemma affinely_absorbingly_elim`{!BiPositive PROP} P :
  <affine> <absorb> P ⊣⊢ <affine> P.
Proof.
  apply (anti_symm _), affinely_mono, absorbingly_intro.
  by rewrite /bi_absorbingly affinely_sep affinely_True_emp left_id.
Qed.

Global Instancepure_absorbing φ : Absorbing (PROP:=PROP) ⌜φ⌝.
Proof. by rewrite /Absorbing absorbingly_pure. Qed.

Global Instanceand_absorbing P Q : Absorbing P → Absorbing Q → Absorbing (P ∧ Q).
Proof. intros. by rewrite /Absorbing absorbingly_and_1 !absorbing. Qed.

Global Instanceor_absorbing P Q : Absorbing P → Absorbing Q → Absorbing (P ∨ Q).
Proof. intros. by rewrite /Absorbing absorbingly_or !absorbing. Qed.

Global Instanceforall_absorbing {A} (Φ : A → PROP) :
  (∀ x, Absorbing (Φ x)) → Absorbing (∀ x, Φ x).
Proof.
  rewrite /Absorbing=> ?. rewrite absorbingly_forall. auto using forall_mono.
Qed.

Global Instanceexist_absorbing {A} (Φ : A → PROP) :
  (∀ x, Absorbing (Φ x)) → Absorbing (∃ x, Φ x).
Proof.
  rewrite /Absorbing=> ?. rewrite absorbingly_exist. auto using exist_mono.
Qed.

Global Instancesep_absorbing_l P Q : Absorbing P → Absorbing (P ∗ Q).
Proof. intros. by rewrite /Absorbing -absorbingly_sep_l absorbing. Qed.

Global Instancesep_absorbing_r P Q : Absorbing Q → Absorbing (P ∗ Q).
Proof. intros. by rewrite /Absorbing -absorbingly_sep_r absorbing. Qed.

Global Instancewand_absorbing_l P Q : Absorbing P → Absorbing (P -∗ Q).
Proof.
  intros. rewrite /Absorbing. apply wand_intro_l.
  by rewrite absorbingly_sep_r -absorbingly_sep_l absorbing wand_elim_r.
Qed.

Global Instancewand_absorbing_r P Q : Absorbing Q → Absorbing (P -∗ Q).
Proof.
  intros. by rewrite /Absorbing absorbingly_wand !absorbing -absorbingly_intro.
Qed.

Global InstanceAffine_proper : Proper ((⊣⊢) ==> iff) (@Affine PROP).
Proof. solve_proper. Qed.

Global InstanceAbsorbing_proper : Proper ((⊣⊢) ==> iff) (@Absorbing PROP).
Proof. solve_proper. Qed.

Lemma affine_affinelyP `{!Affine P} : <affine> P ⊣⊢ P.
Proof. rewrite /bi_affinely. apply (anti_symm _); auto. Qed.

Lemma absorbing_absorbinglyP `{!Absorbing P} : <absorb> P ⊣⊢ P.
Proof. by apply (anti_symm _), absorbingly_intro. Qed.

Lemma True_affine_all_affineP : Affine (PROP:=PROP) True → Affine P.
Proof. rewrite /Affine=> <-; auto. Qed.

Lemma emp_absorbing_all_absorbingP : Absorbing (PROP:=PROP) emp → Absorbing P.
Proof.
  intros. rewrite /Absorbing -{2}(emp_sep P).
  rewrite -(absorbing emp) absorbingly_sep_l left_id //.
Qed.

Lemma sep_elim_lP Q `{HQP : TCOr (Affine Q) (Absorbing P)} : P ∗ Q ⊢ P.
Proof.
  destruct HQP.
  - by rewrite (affine Q) right_id.
  - by rewrite (True_intro Q) comm.
Qed.

Lemma sep_elim_rP Q `{TCOr (Affine P) (Absorbing Q)} : P ∗ Q ⊢ Q.
Proof. by rewrite comm sep_elim_l. Qed.

Lemma sep_andP Q :
  TCOr (Affine P) (Absorbing Q) → TCOr (Affine Q) (Absorbing P) →
  P ∗ Q ⊢ P ∧ Q.
Proof.
  intros [?|?] [?|?];
    apply and_intro; apply: sep_elim_l || apply: sep_elim_r.
Qed.

Lemma affinely_introP Q `{!Affine P} : (P ⊢ Q) → P ⊢ <affine> Q.
Proof. intros <-. by rewrite affine_affinely. Qed.

Lemma emp_andP `{!Affine P} : emp ∧ P ⊣⊢ P.
Proof. apply (anti_symm _); auto. Qed.

Lemma and_empP `{!Affine P} : P ∧ emp ⊣⊢ P.
Proof. apply (anti_symm _); auto. Qed.

Lemma emp_orP `{!Affine P} : emp ∨ P ⊣⊢ emp.
Proof. apply (anti_symm _); auto. Qed.

Lemma or_empP `{!Affine P} : P ∨ emp ⊣⊢ emp.
Proof. apply (anti_symm _); auto. Qed.

Lemma True_sepP `{!Absorbing P} : True ∗ P ⊣⊢ P.
Proof. apply (anti_symm _); auto using True_sep_2. Qed.

Lemma sep_TrueP `{!Absorbing P} : P ∗ True ⊣⊢ P.
Proof. by rewrite comm True_sep. Qed.

Lemma True_emp_iff_BiAffine:
  BiAffine PROP ↔ (True ⊢ emp).
Proof.
  split.
  - intros ?. exact: affine.
  - rewrite /BiAffine /Affine=>Hemp ?. rewrite -Hemp.
    exact: True_intro.
Qed.

Global Instancebi_affine_absorbing P : Absorbing P | 0.
  Proof. by rewrite /Absorbing /bi_absorbingly (affine True) left_id. Qed.

Global Instancebi_affine_positive : BiPositive PROP.
  Proof. intros P Q. by rewrite !affine_affinely. Qed.

Lemma True_emp: True ⊣⊢ emp.
  Proof. apply (anti_symm _); auto using affine. Qed.

Global Instanceemp_and' : LeftId (⊣⊢) emp%I (@bi_and PROP).
  Proof. intros P. by rewrite -True_emp left_id. Qed.

Global Instanceand_emp' : RightId (⊣⊢) emp%I (@bi_and PROP).
  Proof. intros P. by rewrite -True_emp right_id. Qed.

Global InstanceTrue_sep' : LeftId (⊣⊢) True%I (@bi_sep PROP).
  Proof. intros P. by rewrite True_emp left_id. Qed.

Global Instancesep_True' : RightId (⊣⊢) True%I (@bi_sep PROP).
  Proof. intros P. by rewrite True_emp right_id. Qed.

Lemma impl_wand_1P Q : (P → Q) ⊢ P -∗ Q.
  Proof. apply wand_intro_l. by rewrite sep_and impl_elim_r. Qed.

Lemma pure_elimφ Q R : (Q ⊢ ⌜φ⌝) → (φ → Q ⊢ R) → Q ⊢ R.
Proof.
  intros HQ HQR. rewrite -(idemp (∧)%I Q) {1}HQ.
  apply impl_elim_l', pure_elim'=> ?. apply impl_intro_l.
  rewrite and_elim_l; auto.
Qed.

Lemma pure_monoφ1 φ2 : (φ1 → φ2) → ⌜φ1⌝ ⊢ ⌜φ2⌝.
Proof. auto using pure_elim', pure_intro. Qed.

Global Instancepure_mono' : Proper (impl ==> (⊢)) (@bi_pure PROP).
Proof. intros φ1 φ2; apply pure_mono. Qed.

Global Instancepure_flip_mono : Proper (flip impl ==> flip (⊢)) (@bi_pure PROP).
Proof. intros φ1 φ2; apply pure_mono. Qed.

Lemma pure_iffφ1 φ2 : (φ1 ↔ φ2) → ⌜φ1⌝ ⊣⊢ ⌜φ2⌝.
Proof. intros [??]; apply (anti_symm _); auto using pure_mono. Qed.

Lemma pure_elim_lφ Q R : (φ → Q ⊢ R) → ⌜φ⌝ ∧ Q ⊢ R.
Proof. intros; apply pure_elim with φ; eauto. Qed.

Lemma pure_elim_rφ Q R : (φ → Q ⊢ R) → Q ∧ ⌜φ⌝ ⊢ R.
Proof. intros; apply pure_elim with φ; eauto. Qed.

Lemma pure_True(φ : Prop) : φ → ⌜φ⌝ ⊣⊢ True.
Proof. intros; apply (anti_symm _); auto. Qed.

Lemma pure_False(φ : Prop) : ¬φ → ⌜φ⌝ ⊣⊢ False.
Proof. intros; apply (anti_symm _); eauto using pure_mono. Qed.

Lemma pure_andφ1 φ2 : ⌜φ1 ∧ φ2⌝ ⊣⊢ ⌜φ1⌝ ∧ ⌜φ2⌝.
Proof.
  apply (anti_symm _).
  - apply and_intro; apply pure_mono; tauto.
  - eapply (pure_elim φ1); [auto|]=> ?. rewrite and_elim_r. auto using pure_mono.
Qed.

Lemma pure_orφ1 φ2 : ⌜φ1 ∨ φ2⌝ ⊣⊢ ⌜φ1⌝ ∨ ⌜φ2⌝.
Proof.
  apply (anti_symm _).
  - eapply pure_elim=> // -[?|?]; auto using pure_mono.
  - apply or_elim; eauto using pure_mono.
Qed.

Lemma pure_impl_1φ1 φ2 : ⌜φ1 → φ2⌝ ⊢ (⌜φ1⌝ → ⌜φ2⌝).
Proof. apply impl_intro_l. rewrite -pure_and. apply pure_mono. naive_solver. Qed.

Lemma pure_impl_2`{!BiPureForall PROP} φ1 φ2 : (⌜φ1⌝ → ⌜φ2⌝) ⊢ ⌜φ1 → φ2⌝.
Proof.
  rewrite -pure_forall_2. apply forall_intro=> ?.
  by rewrite -(left_id True bi_and (_→_))%I (pure_True φ1) // impl_elim_r.
Qed.

Lemma pure_impl`{!BiPureForall PROP} φ1 φ2 : ⌜φ1 → φ2⌝ ⊣⊢ (⌜φ1⌝ → ⌜φ2⌝).
Proof. apply (anti_symm _); auto using pure_impl_1, pure_impl_2. Qed.

Lemma pure_forall_1{A} (φ : A → Prop) : ⌜∀ x, φ x⌝ ⊢ ∀ x, ⌜φ x⌝.
Proof. apply forall_intro=> x. eauto using pure_mono. Qed.

Lemma pure_forall`{!BiPureForall PROP} {A} (φ : A → Prop) :
  ⌜∀ x, φ x⌝ ⊣⊢ ∀ x, ⌜φ x⌝.
Proof. apply (anti_symm _); auto using pure_forall_1, pure_forall_2. Qed.

Lemma pure_exist{A} (φ : A → Prop) : ⌜∃ x, φ x⌝ ⊣⊢ ∃ x, ⌜φ x⌝.
Proof.
  apply (anti_symm _).
  - eapply pure_elim=> // -[x ?]. rewrite -(exist_intro x); auto using pure_mono.
  - apply exist_elim=> x. eauto using pure_mono.
Qed.

Lemma bi_pure_forall_em: (∀ φ : Prop, φ ∨ ¬φ) → BiPureForall PROP.
Proof.
  intros Hem A φ. destruct (Hem (∃ a, ¬φ a)) as [[a Hφ]|Hφ].
  { rewrite (forall_elim a). by apply pure_elim'. }
  apply pure_intro=> a. destruct (Hem (φ a)); naive_solver.
Qed.

Lemma pure_impl_forallφ P : (⌜φ⌝ → P) ⊣⊢ (∀ _ : φ, P).
Proof.
  apply (anti_symm _).
  - apply forall_intro=> ?. by rewrite pure_True // left_id.
  - apply impl_intro_l, pure_elim_l=> Hφ. by rewrite (forall_elim Hφ).
Qed.

Lemma pure_altφ : ⌜φ⌝ ⊣⊢ ∃ _ : φ, True.
Proof.
  apply (anti_symm _).
  - eapply pure_elim; eauto=> H. rewrite -(exist_intro H); auto.
  - by apply exist_elim, pure_intro.
Qed.

Lemma pure_wand_forallφ P `{!Absorbing P} : (⌜φ⌝ -∗ P) ⊣⊢ (∀ _ : φ, P).
Proof.
  apply (anti_symm _).
  - apply forall_intro=> Hφ.
    rewrite -(pure_intro φ emp) // emp_wand //.
  - apply wand_intro_l, wand_elim_l', pure_elim'=> Hφ.
    apply wand_intro_l. rewrite (forall_elim Hφ) comm. by apply absorbing.
Qed.

Lemma decide_bi_Trueφ `{!Decision φ} (P : PROP) :
  (if decide φ then P else True) ⊣⊢ (⌜φ⌝ → P).
Proof.
  destruct (decide _).
  - by rewrite pure_True // True_impl.
  - by rewrite (pure_False φ) // False_impl.
Qed.

Lemma decide_emp`{!BiAffine PROP} φ `{!Decision φ} (P : PROP) :
  (if decide φ then P else emp) ⊣⊢ (⌜φ⌝ → P).
Proof.
  rewrite -decide_bi_True. destruct (decide _); [done|]. by rewrite True_emp.
Qed.

Local HintResolve persistently_mono : core.

Global Instancepersistently_mono' : Proper ((⊢) ==> (⊢)) (@bi_persistently PROP).
Proof. intros P Q; apply persistently_mono. Qed.

Global Instancepersistently_flip_mono' :
  Proper (flip (⊢) ==> flip (⊢)) (@bi_persistently PROP).
Proof. intros P Q; apply persistently_mono. Qed.

Global Instancepersistently_persistent P : Persistent (<pers> P).
Proof. by rewrite /Persistent -persistently_idemp_2. Qed.

Lemma absorbingly_elim_persistentlyP : <absorb> <pers> P ⊣⊢ <pers> P.
Proof.
  apply (anti_symm _), absorbingly_intro.
  by rewrite /bi_absorbingly comm persistently_absorbing.
Qed.

Global Instancepersistently_absorbing P : Absorbing (<pers> P).
Proof. by rewrite /Absorbing absorbingly_elim_persistently. Qed.

Lemma persistently_forall_1{A} (Ψ : A → PROP) :
  <pers> (∀ a, Ψ a) ⊢ ∀ a, <pers> (Ψ a).
Proof. apply forall_intro=> x. by rewrite (forall_elim x). Qed.

Lemma persistently_forall`{!BiPersistentlyForall PROP} {A} (Ψ : A → PROP) :
  <pers> (∀ a, Ψ a) ⊣⊢ ∀ a, <pers> (Ψ a).
Proof.
  apply (anti_symm _); auto using persistently_forall_1, persistently_forall_2.
Qed.

Lemma persistently_exist{A} (Ψ : A → PROP) :
  <pers> (∃ a, Ψ a) ⊣⊢ ∃ a, <pers> (Ψ a).
Proof.
  apply (anti_symm _); first by auto using persistently_exist_1.
  apply exist_elim=> x. by rewrite (exist_intro x).
Qed.

Lemma persistently_andP Q : <pers> (P ∧ Q) ⊣⊢ <pers> P ∧ <pers> Q.
Proof. apply (anti_symm _); by auto using persistently_and_2. Qed.

Lemma persistently_orP Q : <pers> (P ∨ Q) ⊣⊢ <pers> P ∨ <pers> Q.
Proof. rewrite !or_alt persistently_exist. by apply exist_proper=> -[]. Qed.

Lemma persistently_implP Q : <pers> (P → Q) ⊢ <pers> P → <pers> Q.
Proof.
  apply impl_intro_l; rewrite -persistently_and.
  apply persistently_mono, impl_elim with P; auto.
Qed.

Lemma persistently_emp_introP : P ⊢ <pers> emp.
Proof.
  rewrite -(left_id emp%I bi_sep P).
  by rewrite {1}persistently_emp_2 sep_elim_l.
Qed.

Lemma persistently_True_emp: <pers> True ⊣⊢ <pers> emp.
Proof. apply (anti_symm _); auto using persistently_emp_intro. Qed.

Lemma persistently_True: <pers> True ⊣⊢ True.
Proof.
  apply (anti_symm _); auto.
  rewrite persistently_True_emp. apply persistently_emp_intro.
Qed.

Lemma persistently_and_empP : <pers> P ⊣⊢ <pers> (emp ∧ P).
Proof.
  apply (anti_symm (⊢)); last by rewrite and_elim_r.
  rewrite persistently_and. apply and_intro; last done.
  apply persistently_emp_intro.
Qed.

Lemma persistently_and_sep_elim_empP Q : <pers> P ∧ Q ⊢ (emp ∧ P) ∗ Q.
Proof.
  rewrite persistently_and_emp.
  apply persistently_and_sep_elim.
Qed.

Lemma persistently_and_sep_assocP Q R : <pers> P ∧ (Q ∗ R) ⊣⊢ (<pers> P ∧ Q) ∗ R.
Proof.
  apply (anti_symm (⊢)).
  - rewrite {1}persistently_idemp_2 persistently_and_sep_elim_emp assoc.
    apply sep_mono_l, and_intro.
    + by rewrite and_elim_r sep_elim_l.
    + by rewrite and_elim_l left_id.
  - apply and_intro.
    + by rewrite and_elim_l sep_elim_l.
    + by rewrite and_elim_r.
Qed.

Lemma persistently_and_emp_elimP : emp ∧ <pers> P ⊢ P.
Proof. by rewrite comm persistently_and_sep_elim_emp right_id and_elim_r. Qed.

Lemma persistently_into_absorbinglyP : <pers> P ⊢ <absorb> P.
Proof.
  rewrite -(right_id True%I _ (<pers> _)%I) -{1}(emp_sep True%I).
  rewrite persistently_and_sep_assoc.
  rewrite (comm bi_and) persistently_and_emp_elim comm //.
Qed.

Lemma persistently_elimP `{!Absorbing P} : <pers> P ⊢ P.
Proof. by rewrite persistently_into_absorbingly absorbing_absorbingly. Qed.

Lemma persistently_idemp_1P : <pers> <pers> P ⊢ <pers> P.
Proof.
  by rewrite persistently_into_absorbingly absorbingly_elim_persistently.
Qed.

Lemma persistently_idempP : <pers> <pers> P ⊣⊢ <pers> P.
Proof.
  apply (anti_symm _); auto using persistently_idemp_1, persistently_idemp_2.
Qed.

Lemma persistently_intro'P Q : (<pers> P ⊢ Q) → <pers> P ⊢ <pers> Q.
Proof. intros <-. apply persistently_idemp_2. Qed.

Lemma persistently_pureφ : <pers> ⌜φ⌝ ⊣⊢ ⌜φ⌝.
Proof.
  apply (anti_symm _).
  { by rewrite persistently_into_absorbingly absorbingly_pure. }
  apply pure_elim'=> Hφ. rewrite -persistently_True.
  auto using persistently_mono, pure_intro.
Qed.

Lemma persistently_sep_dupP : <pers> P ⊣⊢ <pers> P ∗ <pers> P.
Proof.
  apply (anti_symm _).
  - rewrite -{1}(idemp bi_and (<pers> _)%I).
    by rewrite -{2}(emp_sep (<pers> _)%I)
      persistently_and_sep_assoc and_elim_l.
  - by rewrite sep_elim_l.
Qed.

Lemma persistently_and_sep_l_1P Q : <pers> P ∧ Q ⊢ <pers> P ∗ Q.
Proof.
  by rewrite -{1}(emp_sep Q) persistently_and_sep_assoc and_elim_l.
Qed.

Lemma persistently_and_sep_r_1P Q : P ∧ <pers> Q ⊢ P ∗ <pers> Q.
Proof. by rewrite !(comm _ P) persistently_and_sep_l_1. Qed.

Lemma persistently_and_sepP Q : <pers> (P ∧ Q) ⊢ <pers> (P ∗ Q).
Proof.
  rewrite persistently_and.
  rewrite -{1}persistently_idemp -persistently_and -{1}(emp_sep Q).
  by rewrite persistently_and_sep_assoc (comm bi_and) persistently_and_emp_elim.
Qed.

Lemma persistently_affinely_elimP : <pers> <affine> P ⊣⊢ <pers> P.
Proof.
  by rewrite /bi_affinely persistently_and -persistently_True_emp
             persistently_pure left_id.
Qed.

Lemma and_sep_persistentlyP Q : <pers> P ∧ <pers> Q ⊣⊢ <pers> P ∗ <pers> Q.
Proof.
  apply (anti_symm _); auto using persistently_and_sep_l_1.
  apply and_intro.
  - by rewrite sep_elim_l.
  - by rewrite sep_elim_r.
Qed.

Lemma persistently_sep_2P Q : <pers> P ∗ <pers> Q ⊢ <pers> (P ∗ Q).
Proof.
  by rewrite -persistently_and_sep persistently_and -and_sep_persistently.
Qed.

Lemma persistently_sep`{!BiPositive PROP} P Q :
  <pers> (P ∗ Q) ⊣⊢ <pers> P ∗ <pers> Q.
Proof.
  apply (anti_symm _); auto using persistently_sep_2.
  rewrite -persistently_affinely_elim affinely_sep -and_sep_persistently.
  apply and_intro.
  - by rewrite (affinely_elim_emp Q) right_id affinely_elim.
  - by rewrite (affinely_elim_emp P) left_id affinely_elim.
Qed.

Lemma persistently_alt_fixpointP :
  <pers> P ⊣⊢ P ∗ <pers> P.
Proof.
  apply (anti_symm _).
  - rewrite -persistently_and_sep_elim. apply and_intro; done.
  - by rewrite sep_elim_r.
Qed.

Lemma persistently_alt_fixpoint'P :
  <pers> P ⊣⊢ <affine> P ∗ <pers> P.
Proof.
  rewrite -{1}persistently_affinely_elim {1}persistently_alt_fixpoint
          persistently_affinely_elim //.
Qed.

Lemma persistently_wandP Q : <pers> (P -∗ Q) ⊢ <pers> P -∗ <pers> Q.
Proof. apply wand_intro_r. by rewrite persistently_sep_2 wand_elim_l. Qed.

Lemma persistently_entails_lP Q : (P ⊢ <pers> Q) → P ⊢ <pers> Q ∗ P.
Proof. intros; rewrite -persistently_and_sep_l_1; auto. Qed.

Lemma persistently_entails_rP Q : (P ⊢ <pers> Q) → P ⊢ P ∗ <pers> Q.
Proof. intros; rewrite -persistently_and_sep_r_1; auto. Qed.

Lemma persistently_impl_wand_2P Q : <pers> (P -∗ Q) ⊢ <pers> (P → Q).
Proof.
  apply persistently_intro', impl_intro_r.
  rewrite -{2}(emp_sep P) persistently_and_sep_assoc.
  by rewrite (comm bi_and) persistently_and_emp_elim wand_elim_l.
Qed.

Lemma impl_wand_persistently_2P Q : (<pers> P -∗ Q) ⊢ (<pers> P → Q).
Proof. apply impl_intro_l. by rewrite persistently_and_sep_l_1 wand_elim_r. Qed.

Lemma persistently_emp: <pers> emp ⊣⊢ emp.
  Proof. by rewrite -!True_emp persistently_pure. Qed.

Lemma persistently_and_sep_lP Q : <pers> P ∧ Q ⊣⊢ <pers> P ∗ Q.
  Proof.
    apply (anti_symm (⊢));
      eauto using persistently_and_sep_l_1, sep_and with typeclass_instances.
  Qed.

Lemma persistently_and_sep_rP Q : P ∧ <pers> Q ⊣⊢ P ∗ <pers> Q.
  Proof. by rewrite !(comm _ P) persistently_and_sep_l. Qed.

Lemma persistently_impl_wandP Q : <pers> (P → Q) ⊣⊢ <pers> (P -∗ Q).
  Proof.
    apply (anti_symm (⊢)); auto using persistently_impl_wand_2.
    apply persistently_intro', wand_intro_l.
    by rewrite -persistently_and_sep_r persistently_elim impl_elim_r.
  Qed.

Lemma impl_wand_persistentlyP Q : (<pers> P → Q) ⊣⊢ (<pers> P -∗ Q).
  Proof.
    apply (anti_symm (⊢)).
    - by rewrite -impl_wand_1.
    - apply impl_wand_persistently_2.
  Qed.

Lemma wand_altP Q : (P -∗ Q) ⊣⊢ ∃ R, R ∗ <pers> (P ∗ R → Q).
  Proof.
    apply (anti_symm (⊢)).
    - rewrite -(right_id True%I bi_sep (P -∗ Q)%I) -(exist_intro (P -∗ Q)%I).
      apply sep_mono_r. rewrite -persistently_pure.
      apply persistently_intro', impl_intro_l.
      by rewrite wand_elim_r persistently_pure right_id.
    - apply exist_elim=> R. apply wand_intro_l.
      rewrite assoc -persistently_and_sep_r.
      by rewrite persistently_elim impl_elim_r.
  Qed.

Global Instancepure_persistent φ : Persistent (PROP:=PROP) ⌜φ⌝.
Proof. by rewrite /Persistent persistently_pure. Qed.

Global Instanceemp_persistent : Persistent (PROP:=PROP) emp.
Proof. rewrite /Persistent. apply persistently_emp_intro. Qed.

Global Instanceand_persistent P Q :
  Persistent P → Persistent Q → Persistent (P ∧ Q).
Proof. intros. by rewrite /Persistent persistently_and -!persistent. Qed.

Global Instanceor_persistent P Q :
  Persistent P → Persistent Q → Persistent (P ∨ Q).
Proof. intros. by rewrite /Persistent persistently_or -!persistent. Qed.

Global Instanceforall_persistent `{!BiPersistentlyForall PROP} {A} (Ψ : A → PROP) :
  (∀ x, Persistent (Ψ x)) → Persistent (∀ x, Ψ x).
Proof.
  intros. rewrite /Persistent persistently_forall.
  apply forall_mono=> x. by rewrite -!persistent.
Qed.

Global Instanceexist_persistent {A} (Ψ : A → PROP) :
  (∀ x, Persistent (Ψ x)) → Persistent (∃ x, Ψ x).
Proof.
  intros. rewrite /Persistent persistently_exist.
  apply exist_mono=> x. by rewrite -!persistent.
Qed.

Global Instancesep_persistent P Q :
  Persistent P → Persistent Q → Persistent (P ∗ Q).
Proof. intros. by rewrite /Persistent -persistently_sep_2 -!persistent. Qed.

Global Instanceaffinely_persistent P : Persistent P → Persistent (<affine> P).
Proof. rewrite /bi_affinely. apply _. Qed.

Global Instanceabsorbingly_persistent P : Persistent P → Persistent (<absorb> P).
Proof. rewrite /bi_absorbingly. apply _. Qed.

Global Instancefrom_option_persistent {A} P (Ψ : A → PROP) (mx : option A) :
  (∀ x, Persistent (Ψ x)) → Persistent P → Persistent (from_option Ψ P mx).
Proof. destruct mx; apply _. Qed.

Global Instanceintuitionistically_ne : NonExpansive (@bi_intuitionistically PROP).
Proof. solve_proper. Qed.

Global Instanceintuitionistically_proper :
  Proper ((⊣⊢) ==> (⊣⊢)) (@bi_intuitionistically PROP).
Proof. solve_proper. Qed.

Global Instanceintuitionistically_mono' :
  Proper ((⊢) ==> (⊢)) (@bi_intuitionistically PROP).
Proof. solve_proper. Qed.

Global Instanceintuitionistically_flip_mono' :
  Proper (flip (⊢) ==> flip (⊢)) (@bi_intuitionistically PROP).
Proof. solve_proper. Qed.

Global Instanceintuitionistically_affine P : Affine (□ P).
Proof. rewrite /bi_intuitionistically. apply _. Qed.

Global Instanceintuitionistically_persistent P : Persistent (□ P).
Proof. rewrite /bi_intuitionistically. apply _. Qed.

Lemma intuitionistically_defP : (□ P)%I = (<affine> <pers> P)%I.
Proof. done. Qed.

Lemma intuitionistically_elimP : □ P ⊢ P.
Proof. apply persistently_and_emp_elim. Qed.

Lemma intuitionistically_elim_empP : □ P ⊢ emp.
Proof. rewrite /bi_intuitionistically affinely_elim_emp //. Qed.

Lemma intuitionistically_intro'P Q : (□ P ⊢ Q) → □ P ⊢ □ Q.
Proof.
  intros <-. rewrite /bi_intuitionistically.
  by rewrite persistently_affinely_elim persistently_idemp.
Qed.

Lemma intuitionistically_emp: □ emp ⊣⊢ emp.
Proof.
  by rewrite /bi_intuitionistically -persistently_True_emp persistently_pure
             affinely_True_emp.
Qed.

Lemma intuitionistically_False: □ False ⊣⊢ False.
Proof. by rewrite /bi_intuitionistically persistently_pure affinely_False. Qed.

Lemma intuitionistically_True_emp: □ True ⊣⊢ emp.
Proof.
  rewrite -intuitionistically_emp /bi_intuitionistically
    persistently_True_emp //.
Qed.

Lemma intuitionistically_andP Q : □ (P ∧ Q) ⊣⊢ □ P ∧ □ Q.
Proof. by rewrite /bi_intuitionistically persistently_and affinely_and. Qed.

Lemma intuitionistically_forall{A} (Φ : A → PROP) : □ (∀ x, Φ x) ⊢ ∀ x, □ Φ x.
Proof.
  by rewrite /bi_intuitionistically persistently_forall_1 affinely_forall.
Qed.

Lemma intuitionistically_orP Q : □ (P ∨ Q) ⊣⊢ □ P ∨ □ Q.
Proof. by rewrite /bi_intuitionistically persistently_or affinely_or. Qed.

Lemma intuitionistically_exist{A} (Φ : A → PROP) : □ (∃ x, Φ x) ⊣⊢ ∃ x, □ Φ x.
Proof. by rewrite /bi_intuitionistically persistently_exist affinely_exist. Qed.

Lemma intuitionistically_sep_2P Q : □ P ∗ □ Q ⊢ □ (P ∗ Q).
Proof. by rewrite /bi_intuitionistically affinely_sep_2 persistently_sep_2. Qed.

Lemma intuitionistically_sep`{!BiPositive PROP} P Q : □ (P ∗ Q) ⊣⊢ □ P ∗ □ Q.
Proof. by rewrite /bi_intuitionistically -affinely_sep -persistently_sep. Qed.

Lemma intuitionistically_idempP : □ □ P ⊣⊢ □ P.
Proof.
  rewrite /bi_intuitionistically.
  by rewrite persistently_affinely_elim persistently_idemp.
Qed.

Lemma intuitionistically_into_persistently_1P : □ P ⊢ <pers> P.
Proof. rewrite /bi_intuitionistically affinely_elim //. Qed.

Lemma intuitionistically_persistently_elimP : □ <pers> P ⊣⊢ □ P.
Proof. rewrite /bi_intuitionistically persistently_idemp //. Qed.

Lemma intuitionistic_intuitionisticallyP :
  Affine P → Persistent P → □ P ⊣⊢ P.
Proof.
  intros. apply (anti_symm _); first exact: intuitionistically_elim.
  rewrite -{1}(affine_affinely P) {1}(persistent P) //.
Qed.

Lemma intuitionistically_affinelyP : □ P ⊢ <affine> P.
Proof.
  rewrite /bi_intuitionistically /bi_affinely. apply and_intro.
  - rewrite and_elim_l //.
  - apply persistently_and_emp_elim.
Qed.

Lemma intuitionistically_affinely_elimP : □ <affine> P ⊣⊢ □ P.
Proof. rewrite /bi_intuitionistically persistently_affinely_elim //. Qed.

Lemma persistently_and_intuitionistically_sep_lP Q : <pers> P ∧ Q ⊣⊢ □ P ∗ Q.
Proof.
  rewrite /bi_intuitionistically. apply (anti_symm _).
  - by rewrite /bi_affinely -(comm bi_and (<pers> P)%I)
      -persistently_and_sep_assoc left_id.
  - apply and_intro.
    + by rewrite affinely_elim sep_elim_l.
    + by rewrite affinely_elim_emp left_id.
Qed.

Lemma persistently_and_intuitionistically_sep_rP Q : P ∧ <pers> Q ⊣⊢ P ∗ □ Q.
Proof. by rewrite !(comm _ P) persistently_and_intuitionistically_sep_l. Qed.

Lemma and_sep_intuitionisticallyP Q : □ P ∧ □ Q ⊣⊢ □ P ∗ □ Q.
Proof.
  rewrite -persistently_and_intuitionistically_sep_l.
  by rewrite -affinely_and affinely_and_r.
Qed.

Lemma intuitionistically_sep_dupP : □ P ⊣⊢ □ P ∗ □ P.
Proof.
  by rewrite -persistently_and_intuitionistically_sep_l affinely_and_r idemp.
Qed.

Lemma impl_wand_intuitionisticallyP Q : (<pers> P → Q) ⊣⊢ (□ P -∗ Q).
Proof.
  apply (anti_symm (⊢)).
  - apply wand_intro_l.
    by rewrite -persistently_and_intuitionistically_sep_l impl_elim_r.
  - apply impl_intro_l.
    by rewrite persistently_and_intuitionistically_sep_l wand_elim_r.
Qed.

Lemma intuitionistically_alt_fixpointP :
  □ P ⊣⊢ emp ∧ (P ∗ □ P).
Proof.
  apply (anti_symm (⊢)).
  - apply and_intro; first exact: affinely_elim_emp.
    rewrite {1}intuitionistically_sep_dup. apply sep_mono; last done.
    apply intuitionistically_elim.
  - apply and_mono; first done.
    rewrite /bi_intuitionistically {2}persistently_alt_fixpoint.
    apply sep_mono; first done. apply and_elim_r.
Qed.

Lemma intuitionistically_impl_wand_2P Q : □ (P -∗ Q) ⊢ □ (P → Q).
Proof. by rewrite /bi_intuitionistically persistently_impl_wand_2. Qed.

Lemma impl_altP Q : (P → Q) ⊣⊢ ∃ R, R ∧ <pers> (P ∧ R -∗ Q).
Proof.
  apply (anti_symm (⊢)).
  - rewrite -(right_id True%I bi_and (P → Q)%I) -(exist_intro (P → Q)%I).
    apply and_mono_r. rewrite impl_elim_r -entails_wand //.
    apply persistently_emp_intro.
  - apply exist_elim=> R. apply impl_intro_l.
    rewrite assoc persistently_and_intuitionistically_sep_r.
    by rewrite intuitionistically_elim wand_elim_r.
Qed.

Lemma intuitionistically_into_persistentlyP : □ P ⊣⊢ <pers> P.
  Proof. rewrite /bi_intuitionistically affine_affinely //. Qed.

Global Instanceaffinely_if_ne p : NonExpansive (@bi_affinely_if PROP p).
Proof. solve_proper. Qed.

Global Instanceaffinely_if_proper p :
  Proper ((⊣⊢) ==> (⊣⊢)) (@bi_affinely_if PROP p).
Proof. solve_proper. Qed.

Global Instanceaffinely_if_mono' p :
  Proper ((⊢) ==> (⊢)) (@bi_affinely_if PROP p).
Proof. solve_proper. Qed.

Global Instanceaffinely_if_flip_mono' p :
  Proper (flip (⊢) ==> flip (⊢)) (@bi_affinely_if PROP p).
Proof. solve_proper. Qed.

Global Instanceaffinely_if_affine p P : Affine P → Affine (<affine>?p P).
Proof. destruct p; simpl; apply _. Qed.

Global Instanceaffinely_if_persistent p P :
  Persistent P → Persistent (<affine>?p P).
Proof. destruct p; simpl; apply _. Qed.

Lemma affinely_if_monop P Q : (P ⊢ Q) → <affine>?p P ⊢ <affine>?p Q.
Proof. by intros ->. Qed.

Lemma affinely_if_flag_mono(p q : bool) P :
  (q → p) → <affine>?p P ⊢ <affine>?q P.
Proof. destruct p, q; naive_solver auto using affinely_elim. Qed.

Lemma affinely_if_elimp P : <affine>?p P ⊢ P.
Proof. destruct p; simpl; auto using affinely_elim. Qed.

Lemma affinely_affinely_ifp P : <affine> P ⊢ <affine>?p P.
Proof. destruct p; simpl; auto using affinely_elim. Qed.

Lemma affinely_if_intro'p P Q :
  (<affine>?p P ⊢ Q) → <affine>?p P ⊢ <affine>?p Q.
Proof. destruct p; simpl; auto using affinely_intro'. Qed.

Lemma affinely_if_empp : <affine>?p emp ⊣⊢ emp.
Proof. destruct p; simpl; auto using affinely_emp. Qed.

Lemma affinely_if_andp P Q : <affine>?p (P ∧ Q) ⊣⊢ <affine>?p P ∧ <affine>?p Q.
Proof. destruct p; simpl; auto using affinely_and. Qed.

Lemma affinely_if_orp P Q : <affine>?p (P ∨ Q) ⊣⊢ <affine>?p P ∨ <affine>?p Q.
Proof. destruct p; simpl; auto using affinely_or. Qed.

Lemma affinely_if_exist{A} p (Ψ : A → PROP) :
  <affine>?p (∃ a, Ψ a) ⊣⊢ ∃ a, <affine>?p (Ψ a).
Proof. destruct p; simpl; auto using affinely_exist. Qed.

Lemma affinely_if_sep_2p P Q : <affine>?p P ∗ <affine>?p Q ⊢ <affine>?p (P ∗ Q).
Proof. destruct p; simpl; auto using affinely_sep_2. Qed.

Lemma affinely_if_sep`{!BiPositive PROP} p P Q :
  <affine>?p (P ∗ Q) ⊣⊢ <affine>?p P ∗ <affine>?p Q.
Proof. destruct p; simpl; auto using affinely_sep. Qed.

Lemma affinely_if_idempp P : <affine>?p <affine>?p P ⊣⊢ <affine>?p P.
Proof. destruct p; simpl; auto using affinely_idemp. Qed.

Lemma affinely_if_and_lp P Q : <affine>?p P ∧ Q ⊣⊢ <affine>?p (P ∧ Q).
Proof. destruct p; simpl; auto using affinely_and_l. Qed.

Lemma affinely_if_and_rp P Q : P ∧ <affine>?p Q ⊣⊢ <affine>?p (P ∧ Q).
Proof. destruct p; simpl; auto using affinely_and_r. Qed.

Lemma affinely_if_and_lrp P Q : <affine>?p P ∧ Q ⊣⊢ P ∧ <affine>?p Q.
Proof. destruct p; simpl; auto using affinely_and_lr. Qed.

Global Instanceabsorbingly_if_ne p : NonExpansive (@bi_absorbingly_if PROP p).
Proof. solve_proper. Qed.

Global Instanceabsorbingly_if_proper p :
  Proper ((⊣⊢) ==> (⊣⊢)) (@bi_absorbingly_if PROP p).
Proof. solve_proper. Qed.

Global Instanceabsorbingly_if_mono' p :
  Proper ((⊢) ==> (⊢)) (@bi_absorbingly_if PROP p).
Proof. solve_proper. Qed.

Global Instanceabsorbingly_if_flip_mono' p :
  Proper (flip (⊢) ==> flip (⊢)) (@bi_absorbingly_if PROP p).
Proof. solve_proper. Qed.

Global Instanceabsorbingly_if_persistent p P :
  Persistent P → Persistent (<absorb>?p P).
Proof. destruct p; simpl; apply _. Qed.

Lemma absorbingly_if_absorbinglyp P : <absorb>?p P ⊢ <absorb> P.
Proof. destruct p; simpl; auto using absorbingly_intro. Qed.

Lemma absorbingly_if_introp P : P ⊢ <absorb>?p P.
Proof. destruct p; simpl; auto using absorbingly_intro. Qed.

Lemma absorbingly_if_monop P Q : (P ⊢ Q) → <absorb>?p P ⊢ <absorb>?p Q.
Proof. by intros ->. Qed.

Lemma absorbingly_if_flag_mono(p q : bool) P :
  (p → q) → <absorb>?p P ⊢ <absorb>?q P.
Proof. destruct p, q; try naive_solver auto using absorbingly_intro. Qed.

Lemma absorbingly_if_idempp P : <absorb>?p <absorb>?p P ⊣⊢ <absorb>?p P.
Proof. destruct p; simpl; auto using absorbingly_idemp. Qed.

Lemma absorbingly_if_purep φ : <absorb>?p ⌜ φ ⌝ ⊣⊢ ⌜ φ ⌝.
Proof. destruct p; simpl; auto using absorbingly_pure. Qed.

Lemma absorbingly_if_orp P Q :
  <absorb>?p (P ∨ Q) ⊣⊢ <absorb>?p P ∨ <absorb>?p Q.
Proof. destruct p; simpl; auto using absorbingly_or. Qed.

Lemma absorbingly_if_and_1p P Q :
  <absorb>?p (P ∧ Q) ⊢ <absorb>?p P ∧ <absorb>?p Q.
Proof. destruct p; simpl; auto using absorbingly_and_1. Qed.

Lemma absorbingly_if_forall{A} p (Φ : A → PROP) :
  <absorb>?p (∀ a, Φ a) ⊢ ∀ a, <absorb>?p (Φ a).
Proof. destruct p; simpl; auto using absorbingly_forall. Qed.

Lemma absorbingly_if_exist{A} p (Φ : A → PROP) :
  <absorb>?p (∃ a, Φ a) ⊣⊢ ∃ a, <absorb>?p (Φ a).
Proof. destruct p; simpl; auto using absorbingly_exist. Qed.

Lemma absorbingly_if_sepp P Q :
  <absorb>?p (P ∗ Q) ⊣⊢ <absorb>?p P ∗ <absorb>?p Q.
Proof. destruct p; simpl; auto using absorbingly_sep. Qed.

Lemma absorbingly_if_wandp P Q :
  <absorb>?p (P -∗ Q) ⊢ <absorb>?p P -∗ <absorb>?p Q.
Proof. destruct p; simpl; auto using absorbingly_wand. Qed.

Lemma absorbingly_if_sep_lp P Q : <absorb>?p P ∗ Q ⊣⊢ <absorb>?p (P ∗ Q).
Proof. destruct p; simpl; auto using absorbingly_sep_l. Qed.

Lemma absorbingly_if_sep_rp P Q : P ∗ <absorb>?p Q ⊣⊢ <absorb>?p (P ∗ Q).
Proof. destruct p; simpl; auto using absorbingly_sep_r. Qed.

Lemma absorbingly_if_sep_lrp P Q : <absorb>?p P ∗ Q ⊣⊢ P ∗ <absorb>?p Q.
Proof. destruct p; simpl; auto using absorbingly_sep_lr. Qed.

Lemma affinely_if_absorbingly_if_elim`{!BiPositive PROP} p P :
  <affine>?p <absorb>?p P ⊣⊢ <affine>?p P.
Proof. destruct p; simpl; auto using affinely_absorbingly_elim. Qed.

Global Instancepersistently_if_ne p : NonExpansive (@bi_persistently_if PROP p).
Proof. solve_proper. Qed.

Global Instancepersistently_if_proper p :
  Proper ((⊣⊢) ==> (⊣⊢)) (@bi_persistently_if PROP p).
Proof. solve_proper. Qed.

Global Instancepersistently_if_mono' p :
  Proper ((⊢) ==> (⊢)) (@bi_persistently_if PROP p).
Proof. solve_proper. Qed.

Global Instancepersistently_if_flip_mono' p :
  Proper (flip (⊢) ==> flip (⊢)) (@bi_persistently_if PROP p).
Proof. solve_proper. Qed.

Global Instancepersistently_if_absorbing P p :
  Absorbing P → Absorbing (<pers>?p P).
Proof. intros; destruct p; simpl; apply _. Qed.

Lemma persistently_if_monop P Q : (P ⊢ Q) → <pers>?p P ⊢ <pers>?p Q.
Proof. by intros ->. Qed.

Lemma persistently_if_purep φ : <pers>?p ⌜φ⌝ ⊣⊢ ⌜φ⌝.
Proof. destruct p; simpl; auto using persistently_pure. Qed.

Lemma persistently_if_andp P Q : <pers>?p (P ∧ Q) ⊣⊢ <pers>?p P ∧ <pers>?p Q.
Proof. destruct p; simpl; auto using persistently_and. Qed.

Lemma persistently_if_orp P Q : <pers>?p (P ∨ Q) ⊣⊢ <pers>?p P ∨ <pers>?p Q.
Proof. destruct p; simpl; auto using persistently_or. Qed.

Lemma persistently_if_exist{A} p (Ψ : A → PROP) :
  (<pers>?p (∃ a, Ψ a)) ⊣⊢ ∃ a, <pers>?p (Ψ a).
Proof. destruct p; simpl; auto using persistently_exist. Qed.

Lemma persistently_if_sep_2p P Q : <pers>?p P ∗ <pers>?p Q ⊢ <pers>?p (P ∗ Q).
Proof. destruct p; simpl; auto using persistently_sep_2. Qed.

Lemma persistently_if_sep`{!BiPositive PROP} p P Q :
  <pers>?p (P ∗ Q) ⊣⊢ <pers>?p P ∗ <pers>?p Q.
Proof. destruct p; simpl; auto using persistently_sep. Qed.

Lemma persistently_if_idempp P : <pers>?p <pers>?p P ⊣⊢ <pers>?p P.
Proof. destruct p; simpl; auto using persistently_idemp. Qed.

Global Instanceintuitionistically_if_ne p :
  NonExpansive (@bi_intuitionistically_if PROP p).
Proof. solve_proper. Qed.

Global Instanceintuitionistically_if_proper p :
  Proper ((⊣⊢) ==> (⊣⊢)) (@bi_intuitionistically_if PROP p).
Proof. solve_proper. Qed.

Global Instanceintuitionistically_if_mono' p :
  Proper ((⊢) ==> (⊢)) (@bi_intuitionistically_if PROP p).
Proof. solve_proper. Qed.

Global Instanceintuitionistically_if_flip_mono' p :
  Proper (flip (⊢) ==> flip (⊢)) (@bi_intuitionistically_if PROP p).
Proof. solve_proper. Qed.

Global Instanceintuitionistically_if_affine p P : Affine P → Affine (□?p P).
Proof. destruct p; simpl; apply _. Qed.

Lemma intuitionistically_if_monop P Q : (P ⊢ Q) → □?p P ⊢ □?p Q.
Proof. by intros ->. Qed.

Lemma intuitionistically_if_flag_mono(p q : bool) P :
  (q → p) → □?p P ⊢ □?q P.
Proof. destruct p, q; naive_solver auto using intuitionistically_elim. Qed.

Lemma intuitionistically_if_elimp P : □?p P ⊢ P.
Proof. destruct p; simpl; auto using intuitionistically_elim. Qed.

Lemma intuitionistically_intuitionistically_ifp P : □ P ⊢ □?p P.
Proof. destruct p; simpl; auto using intuitionistically_elim. Qed.

Lemma intuitionistically_if_intro'p P Q : (□?p P ⊢ Q) → □?p P ⊢ □?p Q.
Proof. destruct p; simpl; auto using intuitionistically_intro'. Qed.

Lemma intuitionistically_if_empp : □?p emp ⊣⊢ emp.
Proof. destruct p; simpl; auto using intuitionistically_emp. Qed.

Lemma intuitionistically_if_Falsep : □?p False ⊣⊢ False.
Proof. destruct p; simpl; auto using intuitionistically_False. Qed.

Lemma intuitionistically_if_andp P Q : □?p (P ∧ Q) ⊣⊢ □?p P ∧ □?p Q.
Proof. destruct p; simpl; auto using intuitionistically_and. Qed.

Lemma intuitionistically_if_orp P Q : □?p (P ∨ Q) ⊣⊢ □?p P ∨ □?p Q.
Proof. destruct p; simpl; auto using intuitionistically_or. Qed.

Lemma intuitionistically_if_exist{A} p (Ψ : A → PROP) :
  (□?p ∃ a, Ψ a) ⊣⊢ ∃ a, □?p Ψ a.
Proof. destruct p; simpl; auto using intuitionistically_exist. Qed.

Lemma intuitionistically_if_sep_2p P Q : □?p P ∗ □?p Q ⊢ □?p (P ∗ Q).
Proof. destruct p; simpl; auto using intuitionistically_sep_2. Qed.

Lemma intuitionistically_if_sep`{!BiPositive PROP} p P Q :
  □?p (P ∗ Q) ⊣⊢ □?p P ∗ □?p Q.
Proof. destruct p; simpl; auto using intuitionistically_sep. Qed.

Lemma intuitionistically_if_idempp P : □?p □?p P ⊣⊢ □?p P.
Proof. destruct p; simpl; auto using intuitionistically_idemp. Qed.

Lemma intuitionistically_if_unfoldp P : □?p P ⊣⊢ <affine>?p <pers>?p P.
Proof. by destruct p. Qed.

Global InstancePersistent_proper : Proper ((≡) ==> iff) (@Persistent PROP).
Proof. solve_proper. Qed.

Lemma persistent_persistently_2P `{!Persistent P} : P ⊢ <pers> P.
Proof. done. Qed.

Lemma persistent_persistentlyP `{!Persistent P, !Absorbing P} : <pers> P ⊣⊢ P.
Proof.
  apply (anti_symm _); auto using persistent_persistently_2, persistently_elim.
Qed.

Lemma persistently_introP Q `{!Persistent P} : (P ⊢ Q) → P ⊢ <pers> Q.
Proof. intros HP. by rewrite (persistent P) HP. Qed.

Lemma persistent_and_affinely_sep_l_1P Q `{!Persistent P} :
  P ∧ Q ⊢ <affine> P ∗ Q.
Proof.
  rewrite {1}(persistent_persistently_2 P).
  rewrite persistently_and_intuitionistically_sep_l.
  rewrite intuitionistically_affinely //.
Qed.

Lemma persistent_and_affinely_sep_r_1P Q `{!Persistent Q} :
  P ∧ Q ⊢ P ∗ <affine> Q.
Proof. by rewrite !(comm _ P) persistent_and_affinely_sep_l_1. Qed.

Lemma persistent_and_affinely_sep_lP Q `{!Persistent P, !Absorbing P} :
  P ∧ Q ⊣⊢ <affine> P ∗ Q.
Proof.
  rewrite -(persistent_persistently P).
  by rewrite persistently_and_intuitionistically_sep_l.
Qed.

Lemma persistent_and_affinely_sep_rP Q `{!Persistent Q, !Absorbing Q} :
  P ∧ Q ⊣⊢ P ∗ <affine> Q.
Proof.
  rewrite -(persistent_persistently Q).
  by rewrite persistently_and_intuitionistically_sep_r.
Qed.

Lemma persistent_and_sep_1P Q `{HPQ : !TCOr (Persistent P) (Persistent Q)} :
  P ∧ Q ⊢ P ∗ Q.
Proof.
  destruct HPQ.
  - by rewrite persistent_and_affinely_sep_l_1 affinely_elim.
  - by rewrite persistent_and_affinely_sep_r_1 affinely_elim.
Qed.

Lemma persistent_sep_dup_1P `{!Persistent P} :
  P ⊢ P ∗ P.
Proof. by rewrite -persistent_and_sep_1 idemp. Qed.

Lemma persistent_sep_dupP
    `{HP : !TCOr (Affine P) (Absorbing P), !Persistent P} :
  P ⊣⊢ P ∗ P.
Proof. apply (anti_symm _); auto using persistent_sep_dup_1, sep_elim_l. Qed.

Lemma persistent_entails_lP Q `{!Persistent Q} : (P ⊢ Q) → P ⊢ Q ∗ P.
Proof. intros. rewrite -persistent_and_sep_1; auto. Qed.

Lemma persistent_entails_rP Q `{!Persistent Q} : (P ⊢ Q) → P ⊢ P ∗ Q.
Proof. intros. rewrite -persistent_and_sep_1; auto. Qed.

Lemma absorbingly_intuitionistically_into_persistentlyP :
  <absorb> □ P ⊣⊢ <pers> P.
Proof.
  apply (anti_symm _).
  - rewrite intuitionistically_into_persistently_1.
    by rewrite absorbingly_elim_persistently.
  - rewrite -{1}(idemp bi_and (<pers> _)%I).
    rewrite persistently_and_intuitionistically_sep_r.
    by rewrite {1} (True_intro (<pers> _)%I).
Qed.

Lemma persistent_absorbingly_affinely_2P `{!Persistent P} :
  P ⊢ <absorb> <affine> P.
Proof.
  rewrite {1}(persistent P) -absorbingly_intuitionistically_into_persistently.
  by rewrite intuitionistically_affinely.
Qed.

Lemma persistent_absorbingly_affinelyP `{!Persistent P, !Absorbing P} :
  <absorb> <affine> P ⊣⊢ P.
Proof.
  rewrite -(persistent_persistently P).
  by rewrite absorbingly_intuitionistically_into_persistently.
Qed.

Lemma persistent_and_sep_assocP `{!Persistent P, !Absorbing P} Q R :
  P ∧ (Q ∗ R) ⊣⊢ (P ∧ Q) ∗ R.
Proof. by rewrite -(persistent_persistently P) persistently_and_sep_assoc. Qed.

Lemma persistent_impl_wand_affinelyP `{!Persistent P, !Absorbing P} Q :
  (P → Q) ⊣⊢ (<affine> P -∗ Q).
Proof.
  apply (anti_symm _).
  - apply wand_intro_l. rewrite -persistent_and_affinely_sep_l impl_elim_r //.
  - apply impl_intro_l. rewrite persistent_and_affinely_sep_l wand_elim_r //.
Qed.

Lemma impl_wand_2P `{!Persistent P} Q : (P -∗ Q) ⊢ P → Q.
Proof. apply impl_intro_l. by rewrite persistent_and_sep_1 wand_elim_r. Qed.

Lemma intuitionisticP `{!Persistent P, !Affine P} : P ⊢ □ P.
Proof. rewrite intuitionistic_intuitionistically. done. Qed.

Lemma intuitionistically_introP Q `{!Affine P, !Persistent P} : (P ⊢ Q) → P ⊢ □ Q.
Proof. intros. apply: affinely_intro. by apply: persistently_intro. Qed.

Lemma persistent_and_sepP Q `{HPQ : !TCOr (Persistent P) (Persistent Q)} :
    P ∧ Q ⊣⊢ P ∗ Q.
  Proof.
    destruct HPQ.
    - by rewrite -(persistent_persistently P) persistently_and_sep_l.
    - by rewrite -(persistent_persistently Q) persistently_and_sep_r.
  Qed.

Lemma impl_wandP `{!Persistent P} Q : (P → Q) ⊣⊢ (P -∗ Q).
  Proof. apply (anti_symm _); auto using impl_wand_1, impl_wand_2. Qed.

Global Instanceimpl_absorbing P Q :
  Persistent P → Absorbing P → Absorbing Q → Absorbing (P → Q).
Proof.
  intros. rewrite /Absorbing. apply impl_intro_l.
  rewrite persistent_and_affinely_sep_l_1 absorbingly_sep_r.
  by rewrite -persistent_and_affinely_sep_l impl_elim_r.
Qed.

Global Instancebi_and_monoid : Monoid (@bi_and PROP) True%I.
Proof. split; apply _. Qed.

Global Instancebi_or_monoid : Monoid (@bi_or PROP) False%I.
Proof. split; apply _. Qed.

Global Instancebi_sep_monoid : Monoid (@bi_sep PROP) emp%I.
Proof. split; apply _. Qed.

Global Instancebi_persistently_and_homomorphism :
  MonoidHomomorphism bi_and bi_and (≡) (@bi_persistently PROP).
Proof.
  split; [split|]; try apply _.
  - apply persistently_and.
  - apply persistently_pure.
Qed.

Global Instancebi_persistently_or_homomorphism :
  MonoidHomomorphism bi_or bi_or (≡) (@bi_persistently PROP).
Proof.
  split; [split|]; try apply _.
  - apply persistently_or.
  - apply persistently_pure.
Qed.

Global Instancebi_persistently_sep_weak_homomorphism `{!BiPositive PROP} :
  WeakMonoidHomomorphism bi_sep bi_sep (≡) (@bi_persistently PROP).
Proof. split; [by apply _ ..|]. apply persistently_sep. Qed.

Global Instancebi_persistently_sep_homomorphism `{!BiAffine PROP} :
  MonoidHomomorphism bi_sep bi_sep (≡) (@bi_persistently PROP).
Proof. split; [by apply _ ..|]. apply persistently_emp. Qed.

Global Instancebi_persistently_sep_entails_weak_homomorphism :
  WeakMonoidHomomorphism bi_sep bi_sep (flip (⊢)) (@bi_persistently PROP).
Proof. split; [by apply _ ..|]. intros P Q; by rewrite persistently_sep_2. Qed.

Global Instancebi_persistently_sep_entails_homomorphism :
  MonoidHomomorphism bi_sep bi_sep (flip (⊢)) (@bi_persistently PROP).
Proof. split; [by apply _ ..|]. simpl. apply persistently_emp_intro. Qed.

Lemma limit_preserving_entails{A : ofe} `{!Cofe A} (Φ Ψ : A → PROP) :
  NonExpansive Φ → NonExpansive Ψ → LimitPreserving (λ x, Φ x ⊢ Ψ x).
Proof.
  intros. apply limit_preserving_ext with (λ x, True ⊣⊢ (Φ x → Ψ x)).
  - intros x. rewrite entails_eq_True. naive_solver.
  - apply limit_preserving_equiv; solve_proper.
Qed.

Lemma limit_preserving_emp_valid{A : ofe} `{!Cofe A} (Φ : A → PROP) :
  NonExpansive Φ → LimitPreserving (λ x, ⊢ Φ x).
Proof. intros. apply limit_preserving_entails; solve_proper. Qed.

Global Instancelimit_preserving_Persistent {A : ofe} `{!Cofe A} (Φ : A → PROP) :
  NonExpansive Φ → LimitPreserving (λ x, Persistent (Φ x)).
Proof. intros. apply limit_preserving_entails; solve_proper. Qed.

Lemma iter_modal_intro(M : PROP → PROP) P (n : nat) :
  (∀ Q, Q ⊢ M Q) →
  P ⊢ Nat.iter n M P.
Proof.
  intros Hintro; induction n as [|n IHn]; simpl; first done.
  etransitivity; first apply IHn. apply Hintro.
Qed.

Lemma iter_modal_mono(M : PROP → PROP) P Q (n : nat) :
  (∀ P Q, (P -∗ Q) ⊢ M P -∗ M Q) →
  (P -∗ Q) ⊢
  Nat.iter n M P -∗ Nat.iter n M Q.
Proof.
  intros Hmono; induction n as [|n IHn]; simpl; first done.
  rewrite -Hmono //.
Qed.