phanerozoic/Coq-Iris huggingface dataset:
(* iris/bi/derived_laws.v *)
Lemma persistently_and_sep P 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.
(* iris/bi/derived_laws.v *)
Lemma persistently_affinely_elim P : <pers> <affine> P ⊣⊢ <pers> P.
Proof.
  by rewrite /bi_affinely persistently_and -persistently_True_emp
             persistently_pure left_id.
Qed.
(* iris/bi/derived_laws.v *)
Lemma and_sep_persistently P 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.
(* iris/bi/derived_laws.v *)
Lemma persistently_sep_2 P Q : <pers> P ∗ <pers> Q ⊢ <pers> (P ∗ Q).
Proof.
  by rewrite -persistently_and_sep persistently_and -and_sep_persistently.
Qed.
(* iris/bi/derived_laws.v *)
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.
(* iris/bi/derived_laws.v *)
Lemma persistently_alt_fixpoint P :
  <pers> P ⊣⊢ P ∗ <pers> P.
Proof.
  apply (anti_symm _).
  - rewrite -persistently_and_sep_elim. apply and_intro; done.
  - by rewrite sep_elim_r.
Qed.
(* iris/bi/derived_laws.v *)
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.
(* iris/bi/derived_laws.v *)
Lemma persistently_wand P Q : <pers> (P -∗ Q) ⊢ <pers> P -∗ <pers> Q.
Proof. apply wand_intro_r. by rewrite persistently_sep_2 wand_elim_l. Qed.
(* iris/bi/derived_laws.v *)
Lemma persistently_entails_l P Q : (P ⊢ <pers> Q) → P ⊢ <pers> Q ∗ P.
Proof. intros; rewrite -persistently_and_sep_l_1; auto. Qed.
(* iris/bi/derived_laws.v *)
Lemma persistently_entails_r P Q : (P ⊢ <pers> Q) → P ⊢ P ∗ <pers> Q.
Proof. intros; rewrite -persistently_and_sep_r_1; auto. Qed.
(* iris/bi/derived_laws.v *)
Lemma persistently_impl_wand_2 P 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.
(* iris/bi/derived_laws.v *)
Lemma impl_wand_persistently_2 P Q : (<pers> P -∗ Q) ⊢ (<pers> P → Q).
Proof. apply impl_intro_l. by rewrite persistently_and_sep_l_1 wand_elim_r. Qed.
(* iris/bi/derived_laws.v *)
Lemma persistently_emp : <pers> emp ⊣⊢ emp.
Proof. by rewrite -!True_emp persistently_pure. Qed.
(* iris/bi/derived_laws.v *)
Lemma persistently_and_sep_l P Q : <pers> P ∧ Q ⊣⊢ <pers> P ∗ Q.
Proof.
    apply (anti_symm (⊢));
      eauto using persistently_and_sep_l_1, sep_and with typeclass_instances.
  Qed.
(* iris/bi/derived_laws.v *)
Lemma persistently_and_sep_r P Q : P ∧ <pers> Q ⊣⊢ P ∗ <pers> Q.
Proof. by rewrite !(comm _ P) persistently_and_sep_l. Qed.
(* iris/bi/derived_laws.v *)
Lemma persistently_impl_wand P 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.
(* iris/bi/derived_laws.v *)
Lemma impl_wand_persistently P Q : (<pers> P → Q) ⊣⊢ (<pers> P -∗ Q).
Proof.
    apply (anti_symm (⊢)).
    - by rewrite -impl_wand_1.
    - apply impl_wand_persistently_2.
  Qed.
(* iris/bi/derived_laws.v *)
Lemma wand_alt P 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.
(* iris/bi/derived_laws.v *)
(* Persistence instances *)
Instance pure_persistent φ : Persistent (PROP:=PROP) ⌜φ⌝.
Proof. by rewrite /Persistent persistently_pure. Qed.
(* iris/bi/derived_laws.v *)
Instance emp_persistent : Persistent (PROP:=PROP) emp.
Proof. rewrite /Persistent. apply persistently_emp_intro. Qed.
(* iris/bi/derived_laws.v *)
Instance and_persistent P Q :
  Persistent P → Persistent Q → Persistent (P ∧ Q).
Proof. intros. by rewrite /Persistent persistently_and -!persistent. Qed.
(* iris/bi/derived_laws.v *)
Instance or_persistent P Q :
  Persistent P → Persistent Q → Persistent (P ∨ Q).
Proof. intros. by rewrite /Persistent persistently_or -!persistent. Qed.
(* iris/bi/derived_laws.v *)
Instance forall_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.
(* iris/bi/derived_laws.v *)
Instance exist_persistent {A} (Ψ : A → PROP) :
  (∀ x, Persistent (Ψ x)) → Persistent (∃ x, Ψ x).
Proof.
  intros. rewrite /Persistent persistently_exist.
  apply exist_mono=> x. by rewrite -!persistent.
Qed.
(* iris/bi/derived_laws.v *)
Instance sep_persistent P Q :
  Persistent P → Persistent Q → Persistent (P ∗ Q).
Proof. intros. by rewrite /Persistent -persistently_sep_2 -!persistent. Qed.
(* iris/bi/derived_laws.v *)
Instance affinely_persistent P : Persistent P → Persistent (<affine> P).
Proof. rewrite /bi_affinely. apply _. Qed.
(* iris/bi/derived_laws.v *)
Instance absorbingly_persistent P : Persistent P → Persistent (<absorb> P).
Proof. rewrite /bi_absorbingly. apply _. Qed.
(* iris/bi/derived_laws.v *)
Instance from_option_persistent {A} P (Ψ : A → PROP) (mx : option A) :
  (∀ x, Persistent (Ψ x)) → Persistent P → Persistent (from_option Ψ P mx).
Proof. destruct mx; apply _. Qed.
(* iris/bi/derived_laws.v *)
(* The intuitionistic modality *)
Instance intuitionistically_ne : NonExpansive (@bi_intuitionistically PROP).
Proof. solve_proper. Qed.
(* iris/bi/derived_laws.v *)
Instance intuitionistically_proper :
  Proper ((⊣⊢) ==> (⊣⊢)) (@bi_intuitionistically PROP).
Proof. solve_proper. Qed.
(* iris/bi/derived_laws.v *)
Instance intuitionistically_mono' :
  Proper ((⊢) ==> (⊢)) (@bi_intuitionistically PROP).
Proof. solve_proper. Qed.
(* iris/bi/derived_laws.v *)
Instance intuitionistically_flip_mono' :
  Proper (flip (⊢) ==> flip (⊢)) (@bi_intuitionistically PROP).
Proof. solve_proper. Qed.
(* iris/bi/derived_laws.v *)
Instance intuitionistically_affine P : Affine (□ P).
Proof. rewrite /bi_intuitionistically. apply _. Qed.
(* iris/bi/derived_laws.v *)
Instance intuitionistically_persistent P : Persistent (□ P).
Proof. rewrite /bi_intuitionistically. apply _. Qed.
(* iris/bi/derived_laws.v *)
Lemma intuitionistically_def P : (□ P)%I = (<affine> <pers> P)%I.
Proof. done. Qed.
(* iris/bi/derived_laws.v *)
Lemma intuitionistically_elim P : □ P ⊢ P.
Proof. apply persistently_and_emp_elim. Qed.
(* iris/bi/derived_laws.v *)
Lemma intuitionistically_elim_emp P : □ P ⊢ emp.
Proof. rewrite /bi_intuitionistically affinely_elim_emp //. Qed.
(* iris/bi/derived_laws.v *)
Lemma intuitionistically_intro' P Q : (□ P ⊢ Q) → □ P ⊢ □ Q.
Proof.
  intros <-. rewrite /bi_intuitionistically.
  by rewrite persistently_affinely_elim persistently_idemp.
Qed.
(* iris/bi/derived_laws.v *)
Lemma intuitionistically_emp : □ emp ⊣⊢ emp.
Proof.
  by rewrite /bi_intuitionistically -persistently_True_emp persistently_pure
             affinely_True_emp.
Qed.
(* iris/bi/derived_laws.v *)
Lemma intuitionistically_False : □ False ⊣⊢ False.
Proof. by rewrite /bi_intuitionistically persistently_pure affinely_False. Qed.
(* iris/bi/derived_laws.v *)
Lemma intuitionistically_True_emp : □ True ⊣⊢ emp.
Proof.
  rewrite -intuitionistically_emp /bi_intuitionistically
    persistently_True_emp //.
Qed.
(* iris/bi/derived_laws.v *)
Lemma intuitionistically_and P Q : □ (P ∧ Q) ⊣⊢ □ P ∧ □ Q.
Proof. by rewrite /bi_intuitionistically persistently_and affinely_and. Qed.
(* iris/bi/derived_laws.v *)
Lemma intuitionistically_forall {A} (Φ : A → PROP) : □ (∀ x, Φ x) ⊢ ∀ x, □ Φ x.
Proof.
  by rewrite /bi_intuitionistically persistently_forall_1 affinely_forall.
Qed.
(* iris/bi/derived_laws.v *)
Lemma intuitionistically_or P Q : □ (P ∨ Q) ⊣⊢ □ P ∨ □ Q.
Proof. by rewrite /bi_intuitionistically persistently_or affinely_or. Qed.
(* iris/bi/derived_laws.v *)
Lemma intuitionistically_exist {A} (Φ : A → PROP) : □ (∃ x, Φ x) ⊣⊢ ∃ x, □ Φ x.
Proof. by rewrite /bi_intuitionistically persistently_exist affinely_exist. Qed.
(* iris/bi/derived_laws.v *)
Lemma intuitionistically_sep_2 P Q : □ P ∗ □ Q ⊢ □ (P ∗ Q).
Proof. by rewrite /bi_intuitionistically affinely_sep_2 persistently_sep_2. Qed.
(* iris/bi/derived_laws.v *)
Lemma intuitionistically_sep `{!BiPositive PROP} P Q : □ (P ∗ Q) ⊣⊢ □ P ∗ □ Q.
Proof. by rewrite /bi_intuitionistically -affinely_sep -persistently_sep. Qed.
(* iris/bi/derived_laws.v *)
Lemma intuitionistically_idemp P : □ □ P ⊣⊢ □ P.
Proof.
  rewrite /bi_intuitionistically.
  by rewrite persistently_affinely_elim persistently_idemp.
Qed.
(* iris/bi/derived_laws.v *)
Lemma intuitionistically_into_persistently_1 P : □ P ⊢ <pers> P.
Proof. rewrite /bi_intuitionistically affinely_elim //. Qed.
(* iris/bi/derived_laws.v *)
Lemma intuitionistically_persistently_elim P : □ <pers> P ⊣⊢ □ P.
Proof. rewrite /bi_intuitionistically persistently_idemp //. Qed.
(* iris/bi/derived_laws.v *)
Lemma intuitionistic_intuitionistically P :
  Affine P → Persistent P → □ P ⊣⊢ P.
Proof.
  intros. apply (anti_symm _); first exact: intuitionistically_elim.
  rewrite -{1}(affine_affinely P) {1}(persistent P) //.
Qed.
(* iris/bi/derived_laws.v *)
Lemma intuitionistically_affinely P : □ P ⊢ <affine> P.
Proof.
  rewrite /bi_intuitionistically /bi_affinely. apply and_intro.
  - rewrite and_elim_l //.
  - apply persistently_and_emp_elim.
Qed.
(* iris/bi/derived_laws.v *)
Lemma intuitionistically_affinely_elim P : □ <affine> P ⊣⊢ □ P.
Proof. rewrite /bi_intuitionistically persistently_affinely_elim //. Qed.
(* iris/bi/derived_laws.v *)
Lemma persistently_and_intuitionistically_sep_l P 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.
(* iris/bi/derived_laws.v *)
Lemma persistently_and_intuitionistically_sep_r P Q : P ∧ <pers> Q ⊣⊢ P ∗ □ Q.
Proof. by rewrite !(comm _ P) persistently_and_intuitionistically_sep_l. Qed.
(* iris/bi/derived_laws.v *)
Lemma and_sep_intuitionistically P Q : □ P ∧ □ Q ⊣⊢ □ P ∗ □ Q.
Proof.
  rewrite -persistently_and_intuitionistically_sep_l.
  by rewrite -affinely_and affinely_and_r.
Qed.
(* iris/bi/derived_laws.v *)
Lemma intuitionistically_sep_dup P : □ P ⊣⊢ □ P ∗ □ P.
Proof.
  by rewrite -persistently_and_intuitionistically_sep_l affinely_and_r idemp.
Qed.
(* iris/bi/derived_laws.v *)
Lemma impl_wand_intuitionistically P 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.
(* iris/bi/derived_laws.v *)
Lemma intuitionistically_alt_fixpoint P :
  □ 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.
(* iris/bi/derived_laws.v *)
Lemma intuitionistically_impl_wand_2 P Q : □ (P -∗ Q) ⊢ □ (P → Q).
Proof. by rewrite /bi_intuitionistically persistently_impl_wand_2. Qed.
(* iris/bi/derived_laws.v *)
Lemma impl_alt P 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.
(* iris/bi/derived_laws.v *)
Lemma intuitionistically_into_persistently P : □ P ⊣⊢ <pers> P.
Proof. rewrite /bi_intuitionistically affine_affinely //. Qed.
(* iris/bi/derived_laws.v *)
(* Conditional affinely modality *)
Instance affinely_if_ne p : NonExpansive (@bi_affinely_if PROP p).
Proof. solve_proper. Qed.
(* iris/bi/derived_laws.v *)
Instance affinely_if_proper p :
  Proper ((⊣⊢) ==> (⊣⊢)) (@bi_affinely_if PROP p).
Proof. solve_proper. Qed.
(* iris/bi/derived_laws.v *)
Instance affinely_if_mono' p :
  Proper ((⊢) ==> (⊢)) (@bi_affinely_if PROP p).
Proof. solve_proper. Qed.
(* iris/bi/derived_laws.v *)
Instance affinely_if_flip_mono' p :
  Proper (flip (⊢) ==> flip (⊢)) (@bi_affinely_if PROP p).
Proof. solve_proper. Qed.
(* iris/bi/derived_laws.v *)
Instance affinely_if_affine p P : Affine P → Affine (<affine>?p P).
Proof. destruct p; simpl; apply _. Qed.
(* iris/bi/derived_laws.v *)
Instance affinely_if_persistent p P :
  Persistent P → Persistent (<affine>?p P).
Proof. destruct p; simpl; apply _. Qed.
(* iris/bi/derived_laws.v *)
Lemma affinely_if_mono p P Q : (P ⊢ Q) → <affine>?p P ⊢ <affine>?p Q.
Proof. by intros ->. Qed.
(* iris/bi/derived_laws.v *)
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.
(* iris/bi/derived_laws.v *)
Lemma affinely_if_elim p P : <affine>?p P ⊢ P.
Proof. destruct p; simpl; auto using affinely_elim. Qed.
(* iris/bi/derived_laws.v *)
Lemma affinely_affinely_if p P : <affine> P ⊢ <affine>?p P.
Proof. destruct p; simpl; auto using affinely_elim. Qed.
(* iris/bi/derived_laws.v *)
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.
(* iris/bi/derived_laws.v *)
Lemma affinely_if_emp p : <affine>?p emp ⊣⊢ emp.
Proof. destruct p; simpl; auto using affinely_emp. Qed.
(* iris/bi/derived_laws.v *)
Lemma affinely_if_and p P Q : <affine>?p (P ∧ Q) ⊣⊢ <affine>?p P ∧ <affine>?p Q.
Proof. destruct p; simpl; auto using affinely_and. Qed.
(* iris/bi/derived_laws.v *)
Lemma affinely_if_or p P Q : <affine>?p (P ∨ Q) ⊣⊢ <affine>?p P ∨ <affine>?p Q.
Proof. destruct p; simpl; auto using affinely_or. Qed.
(* iris/bi/derived_laws.v *)
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.
(* iris/bi/derived_laws.v *)
Lemma affinely_if_sep_2 p P Q : <affine>?p P ∗ <affine>?p Q ⊢ <affine>?p (P ∗ Q).
Proof. destruct p; simpl; auto using affinely_sep_2. Qed.
(* iris/bi/derived_laws.v *)
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.
(* iris/bi/derived_laws.v *)
Lemma affinely_if_idemp p P : <affine>?p <affine>?p P ⊣⊢ <affine>?p P.
Proof. destruct p; simpl; auto using affinely_idemp. Qed.
(* iris/bi/derived_laws.v *)
Lemma affinely_if_and_l p P Q : <affine>?p P ∧ Q ⊣⊢ <affine>?p (P ∧ Q).
Proof. destruct p; simpl; auto using affinely_and_l. Qed.
(* iris/bi/derived_laws.v *)
Lemma affinely_if_and_r p P Q : P ∧ <affine>?p Q ⊣⊢ <affine>?p (P ∧ Q).
Proof. destruct p; simpl; auto using affinely_and_r. Qed.
(* iris/bi/derived_laws.v *)
Lemma affinely_if_and_lr p P Q : <affine>?p P ∧ Q ⊣⊢ P ∧ <affine>?p Q.
Proof. destruct p; simpl; auto using affinely_and_lr. Qed.
(* iris/bi/derived_laws.v *)
(* Conditional absorbingly modality *)
Instance absorbingly_if_ne p : NonExpansive (@bi_absorbingly_if PROP p).
Proof. solve_proper. Qed.
(* iris/bi/derived_laws.v *)
Instance absorbingly_if_proper p :
  Proper ((⊣⊢) ==> (⊣⊢)) (@bi_absorbingly_if PROP p).
Proof. solve_proper. Qed.
(* iris/bi/derived_laws.v *)
Instance absorbingly_if_mono' p :
  Proper ((⊢) ==> (⊢)) (@bi_absorbingly_if PROP p).
Proof. solve_proper. Qed.
(* iris/bi/derived_laws.v *)
Instance absorbingly_if_flip_mono' p :
  Proper (flip (⊢) ==> flip (⊢)) (@bi_absorbingly_if PROP p).
Proof. solve_proper. Qed.
(* iris/bi/derived_laws.v *)
Instance absorbingly_if_persistent p P :
  Persistent P → Persistent (<absorb>?p P).
Proof. destruct p; simpl; apply _. Qed.
(* iris/bi/derived_laws.v *)
Lemma absorbingly_if_absorbingly p P : <absorb>?p P ⊢ <absorb> P.
Proof. destruct p; simpl; auto using absorbingly_intro. Qed.
(* iris/bi/derived_laws.v *)
Lemma absorbingly_if_intro p P : P ⊢ <absorb>?p P.
Proof. destruct p; simpl; auto using absorbingly_intro. Qed.
(* iris/bi/derived_laws.v *)
Lemma absorbingly_if_mono p P Q : (P ⊢ Q) → <absorb>?p P ⊢ <absorb>?p Q.
Proof. by intros ->. Qed.
(* iris/bi/derived_laws.v *)
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.
(* iris/bi/derived_laws.v *)
Lemma absorbingly_if_idemp p P : <absorb>?p <absorb>?p P ⊣⊢ <absorb>?p P.
Proof. destruct p; simpl; auto using absorbingly_idemp. Qed.
(* iris/bi/derived_laws.v *)
Lemma absorbingly_if_pure p φ : <absorb>?p ⌜ φ ⌝ ⊣⊢ ⌜ φ ⌝.
Proof. destruct p; simpl; auto using absorbingly_pure. Qed.
(* iris/bi/derived_laws.v *)
Lemma absorbingly_if_or p P Q :
  <absorb>?p (P ∨ Q) ⊣⊢ <absorb>?p P ∨ <absorb>?p Q.
Proof. destruct p; simpl; auto using absorbingly_or. Qed.
(* iris/bi/derived_laws.v *)
Lemma absorbingly_if_and_1 p P Q :
  <absorb>?p (P ∧ Q) ⊢ <absorb>?p P ∧ <absorb>?p Q.
Proof. destruct p; simpl; auto using absorbingly_and_1. Qed.
(* iris/bi/derived_laws.v *)
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.
(* iris/bi/derived_laws.v *)
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.
(* iris/bi/derived_laws.v *)
Lemma absorbingly_if_sep p P Q :
  <absorb>?p (P ∗ Q) ⊣⊢ <absorb>?p P ∗ <absorb>?p Q.
Proof. destruct p; simpl; auto using absorbingly_sep. Qed.
(* iris/bi/derived_laws.v *)
Lemma absorbingly_if_wand p P Q :
  <absorb>?p (P -∗ Q) ⊢ <absorb>?p P -∗ <absorb>?p Q.
Proof. destruct p; simpl; auto using absorbingly_wand. Qed.
(* iris/bi/derived_laws.v *)
Lemma absorbingly_if_sep_l p P Q : <absorb>?p P ∗ Q ⊣⊢ <absorb>?p (P ∗ Q).
Proof. destruct p; simpl; auto using absorbingly_sep_l. Qed.
(* iris/bi/derived_laws.v *)
Lemma absorbingly_if_sep_r p P Q : P ∗ <absorb>?p Q ⊣⊢ <absorb>?p (P ∗ Q).
Proof. destruct p; simpl; auto using absorbingly_sep_r. Qed.
(* iris/bi/derived_laws.v *)
Lemma absorbingly_if_sep_lr p P Q : <absorb>?p P ∗ Q ⊣⊢ P ∗ <absorb>?p Q.
Proof. destruct p; simpl; auto using absorbingly_sep_lr. Qed.
(* iris/bi/derived_laws.v *)
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.
(* iris/bi/derived_laws.v *)
(* Conditional persistently *)
Instance persistently_if_ne p : NonExpansive (@bi_persistently_if PROP p).
Proof. solve_proper. Qed.
(* iris/bi/derived_laws.v *)
Instance persistently_if_proper p :
  Proper ((⊣⊢) ==> (⊣⊢)) (@bi_persistently_if PROP p).
Proof. solve_proper. Qed.
(* iris/bi/derived_laws.v *)
Instance persistently_if_mono' p :
  Proper ((⊢) ==> (⊢)) (@bi_persistently_if PROP p).
Proof. solve_proper. Qed.
(* iris/bi/derived_laws.v *)
Instance persistently_if_flip_mono' p :
  Proper (flip (⊢) ==> flip (⊢)) (@bi_persistently_if PROP p).
Proof. solve_proper. Qed.
(* iris/bi/derived_laws.v *)
Instance persistently_if_absorbing P p :
  Absorbing P → Absorbing (<pers>?p P).
Proof. intros; destruct p; simpl; apply _. Qed.
(* iris/bi/derived_laws.v *)
Lemma persistently_if_mono p P Q : (P ⊢ Q) → <pers>?p P ⊢ <pers>?p Q.
Proof. by intros ->. Qed.
(* iris/bi/derived_laws.v *)
Lemma persistently_if_pure p φ : <pers>?p ⌜φ⌝ ⊣⊢ ⌜φ⌝.
Proof. destruct p; simpl; auto using persistently_pure. Qed.
(* iris/bi/derived_laws.v *)
Lemma persistently_if_and p P Q : <pers>?p (P ∧ Q) ⊣⊢ <pers>?p P ∧ <pers>?p Q.
Proof. destruct p; simpl; auto using persistently_and. Qed.
(* iris/bi/derived_laws.v *)
Lemma persistently_if_or p P Q : <pers>?p (P ∨ Q) ⊣⊢ <pers>?p P ∨ <pers>?p Q.
Proof. destruct p; simpl; auto using persistently_or. Qed.
(* iris/bi/derived_laws.v *)
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.
(* iris/bi/derived_laws.v *)
Lemma persistently_if_sep_2 p P Q : <pers>?p P ∗ <pers>?p Q ⊢ <pers>?p (P ∗ Q).
Proof. destruct p; simpl; auto using persistently_sep_2. Qed.
(* iris/bi/derived_laws.v *)
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.
(* iris/bi/derived_laws.v *)
Lemma persistently_if_idemp p P : <pers>?p <pers>?p P ⊣⊢ <pers>?p P.
Proof. destruct p; simpl; auto using persistently_idemp. Qed.
(* iris/bi/derived_laws.v *)
(* Conditional intuitionistically *)
Instance intuitionistically_if_ne p :
  NonExpansive (@bi_intuitionistically_if PROP p).
Proof. solve_proper. Qed.
(* iris/bi/derived_laws.v *)
Instance intuitionistically_if_proper p :
  Proper ((⊣⊢) ==> (⊣⊢)) (@bi_intuitionistically_if PROP p).
Proof. solve_proper. Qed.
(* iris/bi/derived_laws.v *)
Instance intuitionistically_if_mono' p :
  Proper ((⊢) ==> (⊢)) (@bi_intuitionistically_if PROP p).
Proof. solve_proper. Qed.
(* iris/bi/derived_laws.v *)
Instance intuitionistically_if_flip_mono' p :
  Proper (flip (⊢) ==> flip (⊢)) (@bi_intuitionistically_if PROP p).
Proof. solve_proper. Qed.
(* iris/bi/derived_laws.v *)
Instance intuitionistically_if_affine p P : Affine P → Affine (□?p P).
Proof. destruct p; simpl; apply _. Qed.
(* iris/bi/derived_laws.v *)
Lemma intuitionistically_if_mono p P Q : (P ⊢ Q) → □?p P ⊢ □?p Q.
Proof. by intros ->. Qed.
(* iris/bi/derived_laws.v *)
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.
(* iris/bi/derived_laws.v *)
Lemma intuitionistically_if_elim p P : □?p P ⊢ P.
Proof. destruct p; simpl; auto using intuitionistically_elim. Qed.
(* iris/bi/derived_laws.v *)
Lemma intuitionistically_intuitionistically_if p P : □ P ⊢ □?p P.
Proof. destruct p; simpl; auto using intuitionistically_elim. Qed.
(* iris/bi/derived_laws.v *)
Lemma intuitionistically_if_intro' p P Q : (□?p P ⊢ Q) → □?p P ⊢ □?p Q.
Proof. destruct p; simpl; auto using intuitionistically_intro'. Qed.
(* iris/bi/derived_laws.v *)
Lemma intuitionistically_if_emp p : □?p emp ⊣⊢ emp.
Proof. destruct p; simpl; auto using intuitionistically_emp. Qed.
(* iris/bi/derived_laws.v *)
Lemma intuitionistically_if_False p : □?p False ⊣⊢ False.
Proof. destruct p; simpl; auto using intuitionistically_False. Qed.
(* iris/bi/derived_laws.v *)
Lemma intuitionistically_if_and p P Q : □?p (P ∧ Q) ⊣⊢ □?p P ∧ □?p Q.
Proof. destruct p; simpl; auto using intuitionistically_and. Qed.
(* iris/bi/derived_laws.v *)
Lemma intuitionistically_if_or p P Q : □?p (P ∨ Q) ⊣⊢ □?p P ∨ □?p Q.
Proof. destruct p; simpl; auto using intuitionistically_or. Qed.
(* iris/bi/derived_laws.v *)
Lemma intuitionistically_if_exist {A} p (Ψ : A → PROP) :
  (□?p ∃ a, Ψ a) ⊣⊢ ∃ a, □?p Ψ a.
Proof. destruct p; simpl; auto using intuitionistically_exist. Qed.
(* iris/bi/derived_laws.v *)
Lemma intuitionistically_if_sep_2 p P Q : □?p P ∗ □?p Q ⊢ □?p (P ∗ Q).
Proof. destruct p; simpl; auto using intuitionistically_sep_2. Qed.
(* iris/bi/derived_laws.v *)
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.