phanerozoic/Coq-Iris huggingface dataset:
(* iris/bi/derived_laws.v *)
Lemma wand_iff_equiv P Q : (⊢ P ∗-∗ Q) → (P ⊣⊢ Q).
Proof.
  intros HPQ; apply (anti_symm (⊢));
    apply wand_entails; rewrite /bi_emp_valid HPQ /bi_wand_iff; auto.
Qed.
(* iris/bi/derived_laws.v *)
Lemma entails_impl P Q : (P ⊢ Q) → (⊢ P → Q).
Proof. intros ->. apply impl_intro_l. auto. Qed.
(* iris/bi/derived_laws.v *)
Lemma impl_entails P Q `{!Affine P} : (⊢ P → Q) → P ⊢ Q.
Proof. intros HPQ. apply impl_elim with P=>//. by rewrite {1}(affine P). Qed.
(* iris/bi/derived_laws.v *)
Lemma equiv_iff P Q : (P ⊣⊢ Q) → (⊢ P ↔ Q).
Proof. intros ->; apply iff_refl. Qed.
(* iris/bi/derived_laws.v *)
Lemma iff_equiv P 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.
(* iris/bi/derived_laws.v *)
Lemma and_parallel P1 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.
(* iris/bi/derived_laws.v *)
Lemma wandM_sound (mP : option PROP) Q :
  (mP -∗? Q) ⊣⊢ (default emp mP -∗ Q).
Proof. destruct mP; simpl; first done. rewrite emp_wand //. Qed.
(* iris/bi/derived_laws.v *)
(* Properties of the affinely modality *)
Instance affinely_ne : NonExpansive (@bi_affinely PROP).
Proof. solve_proper. Qed.
(* iris/bi/derived_laws.v *)
Instance affinely_proper : Proper ((⊣⊢) ==> (⊣⊢)) (@bi_affinely PROP).
Proof. solve_proper. Qed.
(* iris/bi/derived_laws.v *)
Instance affinely_mono' : Proper ((⊢) ==> (⊢)) (@bi_affinely PROP).
Proof. solve_proper. Qed.
(* iris/bi/derived_laws.v *)
Instance affinely_flip_mono' :
  Proper (flip (⊢) ==> flip (⊢)) (@bi_affinely PROP).
Proof. solve_proper. Qed.
(* iris/bi/derived_laws.v *)
Lemma affinely_elim_emp P : <affine> P ⊢ emp.
Proof. rewrite /bi_affinely; auto. Qed.
(* iris/bi/derived_laws.v *)
Instance affinely_affine P : Affine (<affine> P).
Proof. by rewrite /Affine affinely_elim_emp. Qed.
(* iris/bi/derived_laws.v *)
Lemma affinely_elim P : <affine> P ⊢ P.
Proof. rewrite /bi_affinely; auto. Qed.
(* iris/bi/derived_laws.v *)
Lemma affinely_mono P Q : (P ⊢ Q) → <affine> P ⊢ <affine> Q.
Proof. by intros ->. Qed.
(* iris/bi/derived_laws.v *)
Lemma affinely_idemp P : <affine> <affine> P ⊣⊢ <affine> P.
Proof. by rewrite /bi_affinely assoc idemp. Qed.
(* iris/bi/derived_laws.v *)
Lemma affinely_intro' P Q : (<affine> P ⊢ Q) → <affine> P ⊢ <affine> Q.
Proof. intros <-. by rewrite affinely_idemp. Qed.
(* iris/bi/derived_laws.v *)
Lemma affinely_False : <affine> False ⊣⊢ False.
Proof. by rewrite /bi_affinely right_absorb. Qed.
(* iris/bi/derived_laws.v *)
Lemma affinely_emp : <affine> emp ⊣⊢ emp.
Proof. by rewrite /bi_affinely (idemp bi_and). Qed.
(* iris/bi/derived_laws.v *)
Lemma affinely_or P Q : <affine> (P ∨ Q) ⊣⊢ <affine> P ∨ <affine> Q.
Proof. by rewrite /bi_affinely and_or_l. Qed.
(* iris/bi/derived_laws.v *)
Lemma affinely_and P 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.
(* iris/bi/derived_laws.v *)
Lemma affinely_sep_2 P 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.
(* iris/bi/derived_laws.v *)
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.
(* iris/bi/derived_laws.v *)
Lemma affinely_forall {A} (Φ : A → PROP) :
  <affine> (∀ a, Φ a) ⊢ ∀ a, <affine> (Φ a).
Proof. apply forall_intro=> a. by rewrite (forall_elim a). Qed.
(* iris/bi/derived_laws.v *)
Lemma affinely_exist {A} (Φ : A → PROP) :
  <affine> (∃ a, Φ a) ⊣⊢ ∃ a, <affine> (Φ a).
Proof. by rewrite /bi_affinely and_exist_l. Qed.
(* iris/bi/derived_laws.v *)
Lemma affinely_True_emp : <affine> True ⊣⊢ emp.
Proof. apply (anti_symm _); rewrite /bi_affinely; auto. Qed.
(* iris/bi/derived_laws.v *)
Lemma affinely_and_l P Q : <affine> P ∧ Q ⊣⊢ <affine> (P ∧ Q).
Proof. by rewrite /bi_affinely assoc. Qed.
(* iris/bi/derived_laws.v *)
Lemma affinely_and_r P Q : P ∧ <affine> Q ⊣⊢ <affine> (P ∧ Q).
Proof. by rewrite /bi_affinely !assoc (comm _ P). Qed.
(* iris/bi/derived_laws.v *)
Lemma affinely_and_lr P Q : <affine> P ∧ Q ⊣⊢ P ∧ <affine> Q.
Proof. by rewrite affinely_and_l affinely_and_r. Qed.
(* iris/bi/derived_laws.v *)
(* Affine instances *)
Instance emp_affine : Affine (PROP:=PROP) emp.
Proof. by rewrite /Affine. Qed.
(* iris/bi/derived_laws.v *)
Instance False_affine : Affine (PROP:=PROP) False.
Proof. by rewrite /Affine False_elim. Qed.
(* iris/bi/derived_laws.v *)
Instance and_affine_l P Q : Affine P → Affine (P ∧ Q).
Proof. rewrite /Affine=> ->; auto. Qed.
(* iris/bi/derived_laws.v *)
Instance and_affine_r P Q : Affine Q → Affine (P ∧ Q).
Proof. rewrite /Affine=> ->; auto. Qed.
(* iris/bi/derived_laws.v *)
Instance or_affine P Q : Affine P → Affine Q → Affine (P ∨ Q).
Proof.  rewrite /Affine=> -> ->; auto. Qed.
(* iris/bi/derived_laws.v *)
Instance forall_affine `{Inhabited A} (Φ : A → PROP) :
  (∀ x, Affine (Φ x)) → Affine (∀ x, Φ x).
Proof. intros. rewrite /Affine (forall_elim inhabitant). apply: affine. Qed.
(* iris/bi/derived_laws.v *)
Instance exist_affine {A} (Φ : A → PROP) :
  (∀ x, Affine (Φ x)) → Affine (∃ x, Φ x).
Proof. rewrite /Affine=> H. apply exist_elim=> a. by rewrite H. Qed.
(* iris/bi/derived_laws.v *)
Instance sep_affine P Q : Affine P → Affine Q → Affine (P ∗ Q).
Proof. rewrite /Affine=>-> ->. by rewrite left_id. Qed.
(* iris/bi/derived_laws.v *)
(* Properties of the absorbingly modality *)
Instance absorbingly_ne : NonExpansive (@bi_absorbingly PROP).
Proof. solve_proper. Qed.
(* iris/bi/derived_laws.v *)
Instance absorbingly_proper : Proper ((⊣⊢) ==> (⊣⊢)) (@bi_absorbingly PROP).
Proof. solve_proper. Qed.
(* iris/bi/derived_laws.v *)
Instance absorbingly_mono' : Proper ((⊢) ==> (⊢)) (@bi_absorbingly PROP).
Proof. solve_proper. Qed.
(* iris/bi/derived_laws.v *)
Instance absorbingly_flip_mono' :
  Proper (flip (⊢) ==> flip (⊢)) (@bi_absorbingly PROP).
Proof. solve_proper. Qed.
(* iris/bi/derived_laws.v *)
Lemma absorbingly_intro P : P ⊢ <absorb> P.
Proof. by rewrite /bi_absorbingly -True_sep_2. Qed.
(* iris/bi/derived_laws.v *)
Lemma absorbingly_mono P Q : (P ⊢ Q) → <absorb> P ⊢ <absorb> Q.
Proof. by intros ->. Qed.
(* iris/bi/derived_laws.v *)
Lemma absorbingly_idemp P : <absorb> <absorb> P ⊣⊢ <absorb> P.
Proof.
  apply (anti_symm _), absorbingly_intro.
  rewrite /bi_absorbingly assoc. apply sep_mono; auto.
Qed.
(* iris/bi/derived_laws.v *)
Instance absorbingly_absorbing P : Absorbing (<absorb> P).
Proof. by rewrite /Absorbing absorbingly_idemp. Qed.
(* iris/bi/derived_laws.v *)
Lemma absorbingly_pure φ : <absorb> ⌜ φ ⌝ ⊣⊢ ⌜ φ ⌝.
Proof.
  apply (anti_symm _), absorbingly_intro.
  apply wand_elim_r', pure_elim'=> ?. apply wand_intro_l; auto.
Qed.
(* iris/bi/derived_laws.v *)
Lemma absorbingly_True : <absorb> True ⊣⊢ True.
Proof. apply absorbingly_pure. Qed.
(* iris/bi/derived_laws.v *)
Lemma absorbingly_or P Q : <absorb> (P ∨ Q) ⊣⊢ <absorb> P ∨ <absorb> Q.
Proof. by rewrite /bi_absorbingly sep_or_l. Qed.
(* iris/bi/derived_laws.v *)
Lemma absorbingly_and_1 P Q : <absorb> (P ∧ Q) ⊢ <absorb> P ∧ <absorb> Q.
Proof. apply and_intro; apply absorbingly_mono; auto. Qed.
(* iris/bi/derived_laws.v *)
Lemma absorbingly_forall {A} (Φ : A → PROP) :
  <absorb> (∀ a, Φ a) ⊢ ∀ a, <absorb> (Φ a).
Proof. apply forall_intro=> a. by rewrite (forall_elim a). Qed.
(* iris/bi/derived_laws.v *)
Lemma absorbingly_exist {A} (Φ : A → PROP) :
  <absorb> (∃ a, Φ a) ⊣⊢ ∃ a, <absorb> (Φ a).
Proof. by rewrite /bi_absorbingly sep_exist_l. Qed.
(* iris/bi/derived_laws.v *)
Lemma absorbingly_sep P Q : <absorb> (P ∗ Q) ⊣⊢ <absorb> P ∗ <absorb> Q.
Proof.
  by rewrite -{1}absorbingly_idemp /bi_absorbingly !assoc -!(comm _ P) !assoc.
Qed.
(* iris/bi/derived_laws.v *)
Lemma absorbingly_emp_True : <absorb> emp ⊣⊢ True.
Proof. rewrite /bi_absorbingly right_id //. Qed.
(* iris/bi/derived_laws.v *)
Lemma absorbingly_wand P Q : <absorb> (P -∗ Q) ⊢ <absorb> P -∗ <absorb> Q.
Proof. apply wand_intro_l. by rewrite -absorbingly_sep wand_elim_r. Qed.
(* iris/bi/derived_laws.v *)
Lemma absorbingly_sep_l P Q : <absorb> P ∗ Q ⊣⊢ <absorb> (P ∗ Q).
Proof. by rewrite /bi_absorbingly assoc. Qed.
(* iris/bi/derived_laws.v *)
Lemma absorbingly_sep_r P Q : P ∗ <absorb> Q ⊣⊢ <absorb> (P ∗ Q).
Proof. by rewrite /bi_absorbingly !assoc (comm _ P). Qed.
(* iris/bi/derived_laws.v *)
Lemma absorbingly_sep_lr P Q : <absorb> P ∗ Q ⊣⊢ P ∗ <absorb> Q.
Proof. by rewrite absorbingly_sep_l absorbingly_sep_r. Qed.
(* iris/bi/derived_laws.v *)
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.
(* iris/bi/derived_laws.v *)
(* Absorbing instances *)
Instance pure_absorbing φ : Absorbing (PROP:=PROP) ⌜φ⌝.
Proof. by rewrite /Absorbing absorbingly_pure. Qed.
(* iris/bi/derived_laws.v *)
Instance and_absorbing P Q : Absorbing P → Absorbing Q → Absorbing (P ∧ Q).
Proof. intros. by rewrite /Absorbing absorbingly_and_1 !absorbing. Qed.
(* iris/bi/derived_laws.v *)
Instance or_absorbing P Q : Absorbing P → Absorbing Q → Absorbing (P ∨ Q).
Proof. intros. by rewrite /Absorbing absorbingly_or !absorbing. Qed.
(* iris/bi/derived_laws.v *)
Instance forall_absorbing {A} (Φ : A → PROP) :
  (∀ x, Absorbing (Φ x)) → Absorbing (∀ x, Φ x).
Proof.
  rewrite /Absorbing=> ?. rewrite absorbingly_forall. auto using forall_mono.
Qed.
(* iris/bi/derived_laws.v *)
Instance exist_absorbing {A} (Φ : A → PROP) :
  (∀ x, Absorbing (Φ x)) → Absorbing (∃ x, Φ x).
Proof.
  rewrite /Absorbing=> ?. rewrite absorbingly_exist. auto using exist_mono.
Qed.
(* iris/bi/derived_laws.v *)
(* The instance for [Absorbing (P → Q)] is in the persistence section *)
Instance sep_absorbing_l P Q : Absorbing P → Absorbing (P ∗ Q).
Proof. intros. by rewrite /Absorbing -absorbingly_sep_l absorbing. Qed.
(* iris/bi/derived_laws.v *)
Instance sep_absorbing_r P Q : Absorbing Q → Absorbing (P ∗ Q).
Proof. intros. by rewrite /Absorbing -absorbingly_sep_r absorbing. Qed.
(* iris/bi/derived_laws.v *)
Instance wand_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.
(* iris/bi/derived_laws.v *)
Instance wand_absorbing_r P Q : Absorbing Q → Absorbing (P -∗ Q).
Proof.
  intros. by rewrite /Absorbing absorbingly_wand !absorbing -absorbingly_intro.
Qed.
(* iris/bi/derived_laws.v *)
(* Affine and absorbing propositions *)
Instance Affine_proper : Proper ((⊣⊢) ==> iff) (@Affine PROP).
Proof. solve_proper. Qed.
(* iris/bi/derived_laws.v *)
Instance Absorbing_proper : Proper ((⊣⊢) ==> iff) (@Absorbing PROP).
Proof. solve_proper. Qed.
(* iris/bi/derived_laws.v *)
Lemma affine_affinely P `{!Affine P} : <affine> P ⊣⊢ P.
Proof. rewrite /bi_affinely. apply (anti_symm _); auto. Qed.
(* iris/bi/derived_laws.v *)
Lemma absorbing_absorbingly P `{!Absorbing P} : <absorb> P ⊣⊢ P.
Proof. by apply (anti_symm _), absorbingly_intro. Qed.
(* iris/bi/derived_laws.v *)
Lemma True_affine_all_affine P : Affine (PROP:=PROP) True → Affine P.
Proof. rewrite /Affine=> <-; auto. Qed.
(* iris/bi/derived_laws.v *)
Lemma emp_absorbing_all_absorbing P : Absorbing (PROP:=PROP) emp → Absorbing P.
Proof.
  intros. rewrite /Absorbing -{2}(emp_sep P).
  rewrite -(absorbing emp) absorbingly_sep_l left_id //.
Qed.
(* iris/bi/derived_laws.v *)
Lemma sep_elim_l P 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.
(* iris/bi/derived_laws.v *)
Lemma sep_elim_r P Q `{TCOr (Affine P) (Absorbing Q)} : P ∗ Q ⊢ Q.
Proof. by rewrite comm sep_elim_l. Qed.
(* iris/bi/derived_laws.v *)
Lemma sep_and P 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.
(* iris/bi/derived_laws.v *)
Lemma affinely_intro P Q `{!Affine P} : (P ⊢ Q) → P ⊢ <affine> Q.
Proof. intros <-. by rewrite affine_affinely. Qed.
(* iris/bi/derived_laws.v *)
Lemma emp_and P `{!Affine P} : emp ∧ P ⊣⊢ P.
Proof. apply (anti_symm _); auto. Qed.
(* iris/bi/derived_laws.v *)
Lemma and_emp P `{!Affine P} : P ∧ emp ⊣⊢ P.
Proof. apply (anti_symm _); auto. Qed.
(* iris/bi/derived_laws.v *)
Lemma emp_or P `{!Affine P} : emp ∨ P ⊣⊢ emp.
Proof. apply (anti_symm _); auto. Qed.
(* iris/bi/derived_laws.v *)
Lemma or_emp P `{!Affine P} : P ∨ emp ⊣⊢ emp.
Proof. apply (anti_symm _); auto. Qed.
(* iris/bi/derived_laws.v *)
Lemma True_sep P `{!Absorbing P} : True ∗ P ⊣⊢ P.
Proof. apply (anti_symm _); auto using True_sep_2. Qed.
(* iris/bi/derived_laws.v *)
Lemma sep_True P `{!Absorbing P} : P ∗ True ⊣⊢ P.
Proof. by rewrite comm True_sep. Qed.
(* iris/bi/derived_laws.v *)
Lemma True_emp_iff_BiAffine :
  BiAffine PROP ↔ (True ⊢ emp).
Proof.
  split.
  - intros ?. exact: affine.
  - rewrite /BiAffine /Affine=>Hemp ?. rewrite -Hemp.
    exact: True_intro.
Qed.
(* iris/bi/derived_laws.v *)
Instance bi_affine_absorbing P : Absorbing P | 0.
Proof. by rewrite /Absorbing /bi_absorbingly (affine True) left_id. Qed.
(* iris/bi/derived_laws.v *)
Instance bi_affine_positive : BiPositive PROP.
Proof. intros P Q. by rewrite !affine_affinely. Qed.
(* iris/bi/derived_laws.v *)
Lemma True_emp : True ⊣⊢ emp.
Proof. apply (anti_symm _); auto using affine. Qed.
(* iris/bi/derived_laws.v *)
Instance emp_and' : LeftId (⊣⊢) emp%I (@bi_and PROP).
Proof. intros P. by rewrite -True_emp left_id. Qed.
(* iris/bi/derived_laws.v *)
Instance and_emp' : RightId (⊣⊢) emp%I (@bi_and PROP).
Proof. intros P. by rewrite -True_emp right_id. Qed.
(* iris/bi/derived_laws.v *)
Instance True_sep' : LeftId (⊣⊢) True%I (@bi_sep PROP).
Proof. intros P. by rewrite True_emp left_id. Qed.
(* iris/bi/derived_laws.v *)
Instance sep_True' : RightId (⊣⊢) True%I (@bi_sep PROP).
Proof. intros P. by rewrite True_emp right_id. Qed.
(* iris/bi/derived_laws.v *)
Lemma impl_wand_1 P Q : (P → Q) ⊢ P -∗ Q.
Proof. apply wand_intro_l. by rewrite sep_and impl_elim_r. Qed.
(* iris/bi/derived_laws.v *)
(* Pure stuff *)
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.
(* iris/bi/derived_laws.v *)
Lemma pure_mono φ1 φ2 : (φ1 → φ2) → ⌜φ1⌝ ⊢ ⌜φ2⌝.
Proof. auto using pure_elim', pure_intro. Qed.
(* iris/bi/derived_laws.v *)
Instance pure_mono' : Proper (impl ==> (⊢)) (@bi_pure PROP).
Proof. intros φ1 φ2; apply pure_mono. Qed.
(* iris/bi/derived_laws.v *)
Instance pure_flip_mono : Proper (flip impl ==> flip (⊢)) (@bi_pure PROP).
Proof. intros φ1 φ2; apply pure_mono. Qed.
(* iris/bi/derived_laws.v *)
Lemma pure_iff φ1 φ2 : (φ1 ↔ φ2) → ⌜φ1⌝ ⊣⊢ ⌜φ2⌝.
Proof. intros [??]; apply (anti_symm _); auto using pure_mono. Qed.
(* iris/bi/derived_laws.v *)
Lemma pure_elim_l φ Q R : (φ → Q ⊢ R) → ⌜φ⌝ ∧ Q ⊢ R.
Proof. intros; apply pure_elim with φ; eauto. Qed.
(* iris/bi/derived_laws.v *)
Lemma pure_elim_r φ Q R : (φ → Q ⊢ R) → Q ∧ ⌜φ⌝ ⊢ R.
Proof. intros; apply pure_elim with φ; eauto. Qed.
(* iris/bi/derived_laws.v *)
Lemma pure_True (φ : Prop) : φ → ⌜φ⌝ ⊣⊢ True.
Proof. intros; apply (anti_symm _); auto. Qed.
(* iris/bi/derived_laws.v *)
Lemma pure_False (φ : Prop) : ¬φ → ⌜φ⌝ ⊣⊢ False.
Proof. intros; apply (anti_symm _); eauto using pure_mono. Qed.
(* iris/bi/derived_laws.v *)
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.
(* iris/bi/derived_laws.v *)
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.
(* iris/bi/derived_laws.v *)
Lemma pure_impl_1 φ1 φ2 : ⌜φ1 → φ2⌝ ⊢ (⌜φ1⌝ → ⌜φ2⌝).
Proof. apply impl_intro_l. rewrite -pure_and. apply pure_mono. naive_solver. Qed.
(* iris/bi/derived_laws.v *)
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.
(* iris/bi/derived_laws.v *)
Lemma pure_impl `{!BiPureForall PROP} φ1 φ2 : ⌜φ1 → φ2⌝ ⊣⊢ (⌜φ1⌝ → ⌜φ2⌝).
Proof. apply (anti_symm _); auto using pure_impl_1, pure_impl_2. Qed.
(* iris/bi/derived_laws.v *)
Lemma pure_forall_1 {A} (φ : A → Prop) : ⌜∀ x, φ x⌝ ⊢ ∀ x, ⌜φ x⌝.
Proof. apply forall_intro=> x. eauto using pure_mono. Qed.
(* iris/bi/derived_laws.v *)
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.
(* iris/bi/derived_laws.v *)
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.
(* iris/bi/derived_laws.v *)
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.
(* iris/bi/derived_laws.v *)
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.
(* iris/bi/derived_laws.v *)
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.
(* iris/bi/derived_laws.v *)
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.
(* iris/bi/derived_laws.v *)
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.
(* iris/bi/derived_laws.v *)
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.
(* iris/bi/derived_laws.v *)
Instance persistently_mono' : Proper ((⊢) ==> (⊢)) (@bi_persistently PROP).
Proof. intros P Q; apply persistently_mono. Qed.
(* iris/bi/derived_laws.v *)
Instance persistently_flip_mono' :
  Proper (flip (⊢) ==> flip (⊢)) (@bi_persistently PROP).
Proof. intros P Q; apply persistently_mono. Qed.
(* iris/bi/derived_laws.v *)
Instance persistently_persistent P : Persistent (<pers> P).
Proof. by rewrite /Persistent -persistently_idemp_2. Qed.
(* iris/bi/derived_laws.v *)
Lemma absorbingly_elim_persistently P : <absorb> <pers> P ⊣⊢ <pers> P.
Proof.
  apply (anti_symm _), absorbingly_intro.
  by rewrite /bi_absorbingly comm persistently_absorbing.
Qed.
(* iris/bi/derived_laws.v *)
Instance persistently_absorbing P : Absorbing (<pers> P).
Proof. by rewrite /Absorbing absorbingly_elim_persistently. Qed.
(* iris/bi/derived_laws.v *)
Lemma persistently_forall_1 {A} (Ψ : A → PROP) :
  <pers> (∀ a, Ψ a) ⊢ ∀ a, <pers> (Ψ a).
Proof. apply forall_intro=> x. by rewrite (forall_elim x). Qed.
(* iris/bi/derived_laws.v *)
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.
(* iris/bi/derived_laws.v *)
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.
(* iris/bi/derived_laws.v *)
Lemma persistently_and P Q : <pers> (P ∧ Q) ⊣⊢ <pers> P ∧ <pers> Q.
Proof. apply (anti_symm _); by auto using persistently_and_2. Qed.
(* iris/bi/derived_laws.v *)
Lemma persistently_or P Q : <pers> (P ∨ Q) ⊣⊢ <pers> P ∨ <pers> Q.
Proof. rewrite !or_alt persistently_exist. by apply exist_proper=> -[]. Qed.
(* iris/bi/derived_laws.v *)
Lemma persistently_impl P 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.
(* iris/bi/derived_laws.v *)
Lemma persistently_emp_intro P : P ⊢ <pers> emp.
Proof.
  rewrite -(left_id emp%I bi_sep P).
  by rewrite {1}persistently_emp_2 sep_elim_l.
Qed.
(* iris/bi/derived_laws.v *)
Lemma persistently_True_emp : <pers> True ⊣⊢ <pers> emp.
Proof. apply (anti_symm _); auto using persistently_emp_intro. Qed.
(* iris/bi/derived_laws.v *)
Lemma persistently_True : <pers> True ⊣⊢ True.
Proof.
  apply (anti_symm _); auto.
  rewrite persistently_True_emp. apply persistently_emp_intro.
Qed.
(* iris/bi/derived_laws.v *)
Lemma persistently_and_emp P : <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.
(* iris/bi/derived_laws.v *)
Lemma persistently_and_sep_elim_emp P Q : <pers> P ∧ Q ⊢ (emp ∧ P) ∗ Q.
Proof.
  rewrite persistently_and_emp.
  apply persistently_and_sep_elim.
Qed.
(* iris/bi/derived_laws.v *)
Lemma persistently_and_sep_assoc P 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.
(* iris/bi/derived_laws.v *)
Lemma persistently_and_emp_elim P : emp ∧ <pers> P ⊢ P.
Proof. by rewrite comm persistently_and_sep_elim_emp right_id and_elim_r. Qed.
(* iris/bi/derived_laws.v *)
Lemma persistently_into_absorbingly P : <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.
(* iris/bi/derived_laws.v *)
Lemma persistently_elim P `{!Absorbing P} : <pers> P ⊢ P.
Proof. by rewrite persistently_into_absorbingly absorbing_absorbingly. Qed.
(* iris/bi/derived_laws.v *)
Lemma persistently_idemp_1 P : <pers> <pers> P ⊢ <pers> P.
Proof.
  by rewrite persistently_into_absorbingly absorbingly_elim_persistently.
Qed.
(* iris/bi/derived_laws.v *)
Lemma persistently_idemp P : <pers> <pers> P ⊣⊢ <pers> P.
Proof.
  apply (anti_symm _); auto using persistently_idemp_1, persistently_idemp_2.
Qed.
(* iris/bi/derived_laws.v *)
Lemma persistently_intro' P Q : (<pers> P ⊢ Q) → <pers> P ⊢ <pers> Q.
Proof. intros <-. apply persistently_idemp_2. Qed.
(* iris/bi/derived_laws.v *)
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.
(* iris/bi/derived_laws.v *)
Lemma persistently_sep_dup P : <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.
(* iris/bi/derived_laws.v *)
Lemma persistently_and_sep_l_1 P Q : <pers> P ∧ Q ⊢ <pers> P ∗ Q.
Proof.
  by rewrite -{1}(emp_sep Q) persistently_and_sep_assoc and_elim_l.
Qed.
(* iris/bi/derived_laws.v *)
Lemma persistently_and_sep_r_1 P Q : P ∧ <pers> Q ⊢ P ∗ <pers> Q.
Proof. by rewrite !(comm _ P) persistently_and_sep_l_1. Qed.