phanerozoic/Coq-Iris huggingface dataset:
(* iris/bi/derived_laws.v *)
Lemma intuitionistically_if_idemp p P : □?p □?p P ⊣⊢ □?p P.
Proof. destruct p; simpl; auto using intuitionistically_idemp. Qed.
(* iris/bi/derived_laws.v *)
Lemma intuitionistically_if_unfold p P : □?p P ⊣⊢ <affine>?p <pers>?p P.
Proof. by destruct p. Qed.
(* iris/bi/derived_laws.v *)
(* Properties of persistent propositions *)
Instance Persistent_proper : Proper ((≡) ==> iff) (@Persistent PROP).
Proof. solve_proper. Qed.
(* iris/bi/derived_laws.v *)
Lemma persistent_persistently_2 P `{!Persistent P} : P ⊢ <pers> P.
Proof. done. Qed.
(* iris/bi/derived_laws.v *)
Lemma persistent_persistently P `{!Persistent P, !Absorbing P} : <pers> P ⊣⊢ P.
Proof.
  apply (anti_symm _); auto using persistent_persistently_2, persistently_elim.
Qed.
(* iris/bi/derived_laws.v *)
Lemma persistently_intro P Q `{!Persistent P} : (P ⊢ Q) → P ⊢ <pers> Q.
Proof. intros HP. by rewrite (persistent P) HP. Qed.
(* iris/bi/derived_laws.v *)
Lemma persistent_and_affinely_sep_l_1 P 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.
(* iris/bi/derived_laws.v *)
Lemma persistent_and_affinely_sep_r_1 P Q `{!Persistent Q} :
  P ∧ Q ⊢ P ∗ <affine> Q.
Proof. by rewrite !(comm _ P) persistent_and_affinely_sep_l_1. Qed.
(* iris/bi/derived_laws.v *)
Lemma persistent_and_affinely_sep_l P Q `{!Persistent P, !Absorbing P} :
  P ∧ Q ⊣⊢ <affine> P ∗ Q.
Proof.
  rewrite -(persistent_persistently P).
  by rewrite persistently_and_intuitionistically_sep_l.
Qed.
(* iris/bi/derived_laws.v *)
Lemma persistent_and_affinely_sep_r P Q `{!Persistent Q, !Absorbing Q} :
  P ∧ Q ⊣⊢ P ∗ <affine> Q.
Proof.
  rewrite -(persistent_persistently Q).
  by rewrite persistently_and_intuitionistically_sep_r.
Qed.
(* iris/bi/derived_laws.v *)
Lemma persistent_and_sep_1 P 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.
(* iris/bi/derived_laws.v *)
Lemma persistent_sep_dup_1 P `{!Persistent P} :
  P ⊢ P ∗ P.
Proof. by rewrite -persistent_and_sep_1 idemp. Qed.
(* iris/bi/derived_laws.v *)
Lemma persistent_sep_dup P
    `{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.
(* iris/bi/derived_laws.v *)
Lemma persistent_entails_l P Q `{!Persistent Q} : (P ⊢ Q) → P ⊢ Q ∗ P.
Proof. intros. rewrite -persistent_and_sep_1; auto. Qed.
(* iris/bi/derived_laws.v *)
Lemma persistent_entails_r P Q `{!Persistent Q} : (P ⊢ Q) → P ⊢ P ∗ Q.
Proof. intros. rewrite -persistent_and_sep_1; auto. Qed.
(* iris/bi/derived_laws.v *)
Lemma absorbingly_intuitionistically_into_persistently P :
  <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.
(* iris/bi/derived_laws.v *)
Lemma persistent_absorbingly_affinely_2 P `{!Persistent P} :
  P ⊢ <absorb> <affine> P.
Proof.
  rewrite {1}(persistent P) -absorbingly_intuitionistically_into_persistently.
  by rewrite intuitionistically_affinely.
Qed.
(* iris/bi/derived_laws.v *)
Lemma persistent_absorbingly_affinely P `{!Persistent P, !Absorbing P} :
  <absorb> <affine> P ⊣⊢ P.
Proof.
  rewrite -(persistent_persistently P).
  by rewrite absorbingly_intuitionistically_into_persistently.
Qed.
(* iris/bi/derived_laws.v *)
Lemma persistent_and_sep_assoc P `{!Persistent P, !Absorbing P} Q R :
  P ∧ (Q ∗ R) ⊣⊢ (P ∧ Q) ∗ R.
Proof. by rewrite -(persistent_persistently P) persistently_and_sep_assoc. Qed.
(* iris/bi/derived_laws.v *)
Lemma persistent_impl_wand_affinely P `{!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.
(* iris/bi/derived_laws.v *)
Lemma impl_wand_2 P `{!Persistent P} Q : (P -∗ Q) ⊢ P → Q.
Proof. apply impl_intro_l. by rewrite persistent_and_sep_1 wand_elim_r. Qed.
(* iris/bi/derived_laws.v *)
(* We don't have a [Intuitionistic] typeclass, but if we did, this
would be its only field. *)
Lemma intuitionistic P `{!Persistent P, !Affine P} : P ⊢ □ P.
Proof. rewrite intuitionistic_intuitionistically. done. Qed.
(* iris/bi/derived_laws.v *)
Lemma intuitionistically_intro P Q `{!Affine P, !Persistent P} : (P ⊢ Q) → P ⊢ □ Q.
Proof. intros. apply: affinely_intro. by apply: persistently_intro. Qed.
(* iris/bi/derived_laws.v *)
Lemma persistent_and_sep P 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.
(* iris/bi/derived_laws.v *)
Lemma impl_wand P `{!Persistent P} Q : (P → Q) ⊣⊢ (P -∗ Q).
Proof. apply (anti_symm _); auto using impl_wand_1, impl_wand_2. Qed.
(* iris/bi/derived_laws.v *)
Instance impl_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.
(* iris/bi/derived_laws.v *)
(* For big ops *)
Instance bi_and_monoid : Monoid (@bi_and PROP) True%I.
Proof. split; apply _. Qed.
(* iris/bi/derived_laws.v *)
Instance bi_or_monoid : Monoid (@bi_or PROP) False%I.
Proof. split; apply _. Qed.
(* iris/bi/derived_laws.v *)
Instance bi_sep_monoid : Monoid (@bi_sep PROP) emp%I.
Proof. split; apply _. Qed.
(* iris/bi/derived_laws.v *)
Instance bi_persistently_and_homomorphism :
  MonoidHomomorphism bi_and bi_and (≡) (@bi_persistently PROP).
Proof.
  split; [split|]; try apply _.
  - apply persistently_and.
  - apply persistently_pure.
Qed.
(* iris/bi/derived_laws.v *)
Instance bi_persistently_or_homomorphism :
  MonoidHomomorphism bi_or bi_or (≡) (@bi_persistently PROP).
Proof.
  split; [split|]; try apply _.
  - apply persistently_or.
  - apply persistently_pure.
Qed.
(* iris/bi/derived_laws.v *)
Instance bi_persistently_sep_weak_homomorphism `{!BiPositive PROP} :
  WeakMonoidHomomorphism bi_sep bi_sep (≡) (@bi_persistently PROP).
Proof. split; [by apply _ ..|]. apply persistently_sep. Qed.
(* iris/bi/derived_laws.v *)
Instance bi_persistently_sep_homomorphism `{!BiAffine PROP} :
  MonoidHomomorphism bi_sep bi_sep (≡) (@bi_persistently PROP).
Proof. split; [by apply _ ..|]. apply persistently_emp. Qed.
(* iris/bi/derived_laws.v *)
Instance bi_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.
(* iris/bi/derived_laws.v *)
Instance bi_persistently_sep_entails_homomorphism :
  MonoidHomomorphism bi_sep bi_sep (flip (⊢)) (@bi_persistently PROP).
Proof. split; [by apply _ ..|]. simpl. apply persistently_emp_intro. Qed.
(* iris/bi/derived_laws.v *)
(* Limits *)
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.
(* iris/bi/derived_laws.v *)
Lemma limit_preserving_emp_valid {A : ofe} `{!Cofe A} (Φ : A → PROP) :
  NonExpansive Φ → LimitPreserving (λ x, ⊢ Φ x).
Proof. intros. apply limit_preserving_entails; solve_proper. Qed.
(* iris/bi/derived_laws.v *)
Instance limit_preserving_Persistent {A : ofe} `{!Cofe A} (Φ : A → PROP) :
  NonExpansive Φ → LimitPreserving (λ x, Persistent (Φ x)).
Proof. intros. apply limit_preserving_entails; solve_proper. Qed.
(* iris/bi/derived_laws.v *)
(* iterated modalities *)
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.
(* iris/bi/derived_laws.v *)
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.
(* iris/bi/derived_laws_later.v *)
Instance later_proper :
  Proper ((⊣⊢) ==> (⊣⊢)) (@bi_later PROP)
:= ne_proper _.
(* iris/bi/derived_laws_later.v *)
Instance later_mono' : Proper ((⊢) ==> (⊢)) (@bi_later PROP).
Proof. intros P Q; apply later_mono. Qed.
(* iris/bi/derived_laws_later.v *)
Instance later_flip_mono' :
  Proper (flip (⊢) ==> flip (⊢)) (@bi_later PROP).
Proof. intros P Q; apply later_mono. Qed.
(* iris/bi/derived_laws_later.v *)
Lemma later_True : ▷ True ⊣⊢ True.
Proof. apply (anti_symm (⊢)); auto using later_intro. Qed.
(* iris/bi/derived_laws_later.v *)
Lemma later_emp `{!BiAffine PROP} : ▷ emp ⊣⊢ emp.
Proof. by rewrite -True_emp later_True. Qed.
(* iris/bi/derived_laws_later.v *)
Lemma later_forall {A} (Φ : A → PROP) : (▷ ∀ a, Φ a) ⊣⊢ (∀ a, ▷ Φ a).
Proof.
  apply (anti_symm _); auto using later_forall_2.
  apply forall_intro=> x. by rewrite (forall_elim x).
Qed.
(* iris/bi/derived_laws_later.v *)
Lemma later_exist_2 {A} (Φ : A → PROP) : (∃ a, ▷ Φ a) ⊢ ▷ (∃ a, Φ a).
Proof. apply exist_elim; eauto using exist_intro. Qed.
(* iris/bi/derived_laws_later.v *)
Lemma later_exist_except_0 {A} (Φ : A → PROP) : ▷ (∃ a, Φ a) ⊢ ◇ (∃ a, ▷ Φ a).
Proof. apply later_exist_false. Qed.
(* iris/bi/derived_laws_later.v *)
Lemma later_exist `{Inhabited A} (Φ : A → PROP) : ▷ (∃ a, Φ a) ⊣⊢ (∃ a, ▷ Φ a).
Proof.
  apply: anti_symm; [|apply later_exist_2].
  rewrite later_exist_false. apply or_elim; last done.
  rewrite -(exist_intro inhabitant); auto.
Qed.
(* iris/bi/derived_laws_later.v *)
Lemma later_and P Q : ▷ (P ∧ Q) ⊣⊢ ▷ P ∧ ▷ Q.
Proof. rewrite !and_alt later_forall. by apply forall_proper=> -[]. Qed.
(* iris/bi/derived_laws_later.v *)
Lemma later_or P Q : ▷ (P ∨ Q) ⊣⊢ ▷ P ∨ ▷ Q.
Proof. rewrite !or_alt later_exist. by apply exist_proper=> -[]. Qed.
(* iris/bi/derived_laws_later.v *)
Lemma later_impl P Q : ▷ (P → Q) ⊢ ▷ P → ▷ Q.
Proof. apply impl_intro_l. by rewrite -later_and impl_elim_r. Qed.
(* iris/bi/derived_laws_later.v *)
Lemma later_sep P Q : ▷ (P ∗ Q) ⊣⊢ ▷ P ∗ ▷ Q.
Proof. apply (anti_symm _); auto using later_sep_1, later_sep_2. Qed.
(* iris/bi/derived_laws_later.v *)
Lemma later_wand P Q : ▷ (P -∗ Q) ⊢ ▷ P -∗ ▷ Q.
Proof. apply wand_intro_l. by rewrite -later_sep wand_elim_r. Qed.
(* iris/bi/derived_laws_later.v *)
Lemma later_iff P Q : ▷ (P ↔ Q) ⊢ ▷ P ↔ ▷ Q.
Proof. by rewrite /bi_iff later_and !later_impl. Qed.
(* iris/bi/derived_laws_later.v *)
Lemma later_wand_iff P Q : ▷ (P ∗-∗ Q) ⊢ ▷ P ∗-∗ ▷ Q.
Proof. by rewrite /bi_wand_iff later_and !later_wand. Qed.
(* iris/bi/derived_laws_later.v *)
Lemma later_persistently P : ▷ <pers> P ⊣⊢ <pers> ▷ P.
Proof. apply (anti_symm _); auto using later_persistently_1, later_persistently_2. Qed.
(* iris/bi/derived_laws_later.v *)
Lemma later_affinely_2 P : <affine> ▷ P ⊢ ▷ <affine> P.
Proof. rewrite /bi_affinely later_and. auto using later_intro. Qed.
(* iris/bi/derived_laws_later.v *)
Lemma later_intuitionistically_2 P : □ ▷ P ⊢ ▷ □ P.
Proof. by rewrite /bi_intuitionistically -later_persistently later_affinely_2. Qed.
(* iris/bi/derived_laws_later.v *)
Lemma later_intuitionistically_if_2 p P : □?p ▷ P ⊢ ▷ □?p P.
Proof. destruct p; simpl; auto using later_intuitionistically_2. Qed.
(* iris/bi/derived_laws_later.v *)
Lemma later_absorbingly P : ▷ <absorb> P ⊣⊢ <absorb> ▷ P.
Proof. by rewrite /bi_absorbingly later_sep later_True. Qed.
(* iris/bi/derived_laws_later.v *)
Lemma later_affinely `{!BiAffine PROP} P : ▷ <affine> P ⊣⊢ <affine> ▷ P.
Proof. by rewrite !affine_affinely. Qed.
(* iris/bi/derived_laws_later.v *)
Lemma later_intuitionistically `{!BiAffine PROP} P : ▷ □ P ⊣⊢ □ ▷ P.
Proof. by rewrite !intuitionistically_into_persistently later_persistently. Qed.
(* iris/bi/derived_laws_later.v *)
Lemma later_intuitionistically_if `{!BiAffine PROP} p P : ▷ □?p P ⊣⊢ □?p ▷ P.
Proof. destruct p; simpl; auto using later_intuitionistically. Qed.
(* iris/bi/derived_laws_later.v *)
Instance later_persistent P : Persistent P → Persistent (▷ P).
Proof. intros. by rewrite /Persistent -later_persistently {1}(persistent P). Qed.
(* iris/bi/derived_laws_later.v *)
Instance later_absorbing P : Absorbing P → Absorbing (▷ P).
Proof. intros ?. by rewrite /Absorbing -later_absorbingly absorbing. Qed.
(* iris/bi/derived_laws_later.v *)
(* We prove relations between the following statements:

1. [Contractive (▷)], later is contractive as expressed by [BiLaterContractive].
2. [(▷ P ⊢ P) → (True ⊢ P)], the external/"weak" of Löb as expressed by [BiLöb].
3. [(▷ P → P) ⊢ P], the internal version/"strong" of Löb.
4. [□ (□ ▷ P -∗ P) ⊢ P], an internal version of Löb with magic wand instead of
   implication.
5. [□ (▷ P -∗ P) ⊢ P], a weaker version of the former statement, which does not
   make the induction hypothesis intuitionistic.

We prove that:

- (1) implies (2) in all BI logics (lemma [later_contractive_bi_löb]).
- (2) and (3) are logically equivalent in all BI logics (lemma [löb_alt_strong]).
- (2) implies (4) and (5) in all BI logics (lemmas [löb_wand_intuitionistically]
  and [löb_wand]).
- (5) and (2) are logically equivalent in affine BI logics (lemma [löb_alt_wand]).

In particular, this gives that (2), (3), (4) and (5) are logically equivalent in
affine BI logics such as Iris. *)
Lemma löb `{!BiLöb PROP} P : (▷ P → P) ⊢ P.
Proof.
  apply entails_impl_True, löb_weak. apply impl_intro_r.
  rewrite -{2}(idemp (∧) (▷ P → P))%I.
  rewrite {2}(later_intro (▷ P → P)).
  rewrite later_impl.
  rewrite assoc impl_elim_l.
  rewrite impl_elim_r. done.
Qed.
(* iris/bi/derived_laws_later.v *)
Lemma löb_alt_strong : BiLöb PROP ↔ ∀ P, (▷ P → P) ⊢ P.
Proof. split; intros HLöb P; [by apply löb|]. by intros ->%entails_impl_True. Qed.
(* iris/bi/derived_laws_later.v *)
(* Proof following https://en.wikipedia.org/wiki/L%C3%B6b's_theorem#Proof_of_L%C3%B6b's_theorem.
Their [Ψ] is called [Q] in our proof. *)
Instance later_contractive_bi_löb : BiLaterContractive PROP → BiLöb PROP.
Proof.
  intros=> P.
  pose (flöb_pre (P Q : PROP) := (▷ Q → P)%I).
  assert (∀ P, Contractive (flöb_pre P)) by solve_contractive.
  set (Q := fixpoint (flöb_pre P)).
  assert (Q ⊣⊢ (▷ Q → P)) as HQ by (exact: fixpoint_unfold).
  intros HP. rewrite -HP.
  assert (▷ Q ⊢ P) as HQP.
  { rewrite -HP. rewrite -(idemp (∧) (▷ Q))%I {2}(later_intro (▷ Q)).
    by rewrite {1}HQ {1}later_impl impl_elim_l. }
  rewrite -HQP HQ -2!later_intro.
  apply (entails_impl_True _ P). done.
Qed.
(* iris/bi/derived_laws_later.v *)
Lemma löb_wand_intuitionistically `{!BiLöb PROP} P : □ (□ ▷ P -∗ P) ⊢ P.
Proof.
  rewrite -{3}(intuitionistically_elim P) -(löb (□ P)). apply impl_intro_l.
  rewrite {1}intuitionistically_into_persistently_1 later_persistently.
  rewrite persistently_and_intuitionistically_sep_l.
  rewrite -{1}(intuitionistically_idemp (▷ P)) intuitionistically_sep_2.
  by rewrite wand_elim_r.
Qed.
(* iris/bi/derived_laws_later.v *)
Lemma löb_wand `{!BiLöb PROP} P : □ (▷ P -∗ P) ⊢ P.
Proof.
  by rewrite -(intuitionistically_elim (▷ P)) löb_wand_intuitionistically.
Qed.
(* iris/bi/derived_laws_later.v *)
(* The proof of the right-to-left direction relies on the BI being affine. It
is unclear how to generalize the lemma or proof to support non-affine BIs. *)
Lemma löb_alt_wand `{!BiAffine PROP} : BiLöb PROP ↔ ∀ P, □ (▷ P -∗ P) ⊢ P.
Proof.
  split; intros Hlöb; [by apply löb_wand|].
  apply löb_alt_strong=> P.
  rewrite bi.impl_alt. apply bi.exist_elim=> R. apply impl_elim_r'.
  rewrite -(Hlöb (R → P)%I) -intuitionistically_into_persistently.
  apply intuitionistically_intro', wand_intro_l, impl_intro_l.
  rewrite -persistently_and_intuitionistically_sep_r assoc
    persistently_and_intuitionistically_sep_r intuitionistically_elim.
  rewrite -{1}(idemp bi_and R) -(assoc _ R) {2}(later_intro R).
  by rewrite -later_and impl_elim_r (comm _ R) wand_elim_r.
Qed.
(* iris/bi/derived_laws_later.v *)
(* A funny consequence of Löb induction.
This shows that Löb induction is incompatible with classical logic.
See [lib/counterexamples.v] for a fully worked-out proof of that fact. *)
Lemma not_not_later_False `{!BiLöb PROP} : ⊢@{PROP} ¬ ¬ ▷ False.
Proof. apply entails_impl, löb. Qed.
(* iris/bi/derived_laws_later.v *)
(* Iterated later modality *)
Instance laterN_ne m : NonExpansive (@bi_laterN PROP m).
Proof. induction m; simpl; [by intros ???|]. solve_proper. Qed.
(* iris/bi/derived_laws_later.v *)
Instance laterN_proper m :
  Proper ((⊣⊢) ==> (⊣⊢)) (@bi_laterN PROP m)
:= ne_proper _.
(* iris/bi/derived_laws_later.v *)
Lemma laterN_0 P : ▷^0 P ⊣⊢ P.
Proof. done. Qed.
(* iris/bi/derived_laws_later.v *)
Lemma later_laterN n P : ▷^(S n) P ⊣⊢ ▷ ▷^n P.
Proof. done. Qed.
(* iris/bi/derived_laws_later.v *)
Lemma laterN_later n P : ▷^(S n) P ⊣⊢ ▷^n ▷ P.
Proof. induction n; f_equiv/=; auto. Qed.
(* iris/bi/derived_laws_later.v *)
Lemma laterN_add n1 n2 P : ▷^(n1 + n2) P ⊣⊢ ▷^n1 ▷^n2 P.
Proof. induction n1; f_equiv/=; auto. Qed.
(* iris/bi/derived_laws_later.v *)
Lemma laterN_le n1 n2 P : n1 ≤ n2 → ▷^n1 P ⊢ ▷^n2 P.
Proof. induction 1; simpl; by rewrite -?later_intro. Qed.
(* iris/bi/derived_laws_later.v *)
Lemma laterN_iter n P : (▷^n P)%I = Nat.iter n bi_later P.
Proof. induction n; f_equal/=; auto. Qed.
(* iris/bi/derived_laws_later.v *)
Lemma laterN_mono n P Q : (P ⊢ Q) → ▷^n P ⊢ ▷^n Q.
Proof. induction n; simpl; auto. Qed.
(* iris/bi/derived_laws_later.v *)
Instance laterN_mono' n : Proper ((⊢) ==> (⊢)) (@bi_laterN PROP n).
Proof. intros P Q; apply laterN_mono. Qed.
(* iris/bi/derived_laws_later.v *)
Instance laterN_flip_mono' n :
  Proper (flip (⊢) ==> flip (⊢)) (@bi_laterN PROP n).
Proof. intros P Q; apply laterN_mono. Qed.
(* iris/bi/derived_laws_later.v *)
Lemma laterN_intro n P : P ⊢ ▷^n P.
Proof. induction n as [|n IH]; simpl; by rewrite -?later_intro. Qed.
(* iris/bi/derived_laws_later.v *)
Lemma laterN_True n : ▷^n True ⊣⊢ True.
Proof. apply (anti_symm (⊢)); auto using laterN_intro, True_intro. Qed.
(* iris/bi/derived_laws_later.v *)
Lemma laterN_emp `{!BiAffine PROP} n : ▷^n emp ⊣⊢ emp.
Proof. by rewrite -True_emp laterN_True. Qed.
(* iris/bi/derived_laws_later.v *)
Lemma laterN_forall {A} n (Φ : A → PROP) : (▷^n ∀ a, Φ a) ⊣⊢ (∀ a, ▷^n Φ a).
Proof. induction n as [|n IH]; simpl; rewrite -?later_forall ?IH; auto. Qed.
(* iris/bi/derived_laws_later.v *)
Lemma laterN_exist_2 {A} n (Φ : A → PROP) : (∃ a, ▷^n Φ a) ⊢ ▷^n (∃ a, Φ a).
Proof. apply exist_elim; eauto using exist_intro, laterN_mono. Qed.
(* iris/bi/derived_laws_later.v *)
Lemma laterN_exist {A} `{!Inhabited A} n (Φ : A → PROP) :
  (▷^n ∃ a, Φ a) ⊣⊢ ∃ a, ▷^n Φ a.
Proof. induction n as [|n IH]; simpl; rewrite -?later_exist ?IH; auto. Qed.
(* iris/bi/derived_laws_later.v *)
Lemma laterN_and n P Q : ▷^n (P ∧ Q) ⊣⊢ ▷^n P ∧ ▷^n Q.
Proof. induction n as [|n IH]; simpl; rewrite -?later_and ?IH; auto. Qed.
(* iris/bi/derived_laws_later.v *)
Lemma laterN_or n P Q : ▷^n (P ∨ Q) ⊣⊢ ▷^n P ∨ ▷^n Q.
Proof. induction n as [|n IH]; simpl; rewrite -?later_or ?IH; auto. Qed.
(* iris/bi/derived_laws_later.v *)
Lemma laterN_impl n P Q : ▷^n (P → Q) ⊢ ▷^n P → ▷^n Q.
Proof. apply impl_intro_l. by rewrite -laterN_and impl_elim_r. Qed.
(* iris/bi/derived_laws_later.v *)
Lemma laterN_sep n P Q : ▷^n (P ∗ Q) ⊣⊢ ▷^n P ∗ ▷^n Q.
Proof. induction n as [|n IH]; simpl; rewrite -?later_sep ?IH; auto. Qed.
(* iris/bi/derived_laws_later.v *)
Lemma laterN_wand n P Q : ▷^n (P -∗ Q) ⊢ ▷^n P -∗ ▷^n Q.
Proof. apply wand_intro_l. by rewrite -laterN_sep wand_elim_r. Qed.
(* iris/bi/derived_laws_later.v *)
Lemma laterN_iff n P Q : ▷^n (P ↔ Q) ⊢ ▷^n P ↔ ▷^n Q.
Proof. by rewrite /bi_iff laterN_and !laterN_impl. Qed.
(* iris/bi/derived_laws_later.v *)
Lemma laterN_persistently n P : ▷^n <pers> P ⊣⊢ <pers> ▷^n P.
Proof. induction n as [|n IH]; simpl; auto. by rewrite IH later_persistently. Qed.
(* iris/bi/derived_laws_later.v *)
Lemma laterN_affinely_2 n P : <affine> ▷^n P ⊢ ▷^n <affine> P.
Proof. rewrite /bi_affinely laterN_and. auto using laterN_intro. Qed.
(* iris/bi/derived_laws_later.v *)
Lemma laterN_intuitionistically_2 n P : □ ▷^n P ⊢ ▷^n □ P.
Proof. by rewrite /bi_intuitionistically -laterN_persistently laterN_affinely_2. Qed.
(* iris/bi/derived_laws_later.v *)
Lemma laterN_intuitionistically_if_2 n p P : □?p ▷^n P ⊢ ▷^n □?p P.
Proof. destruct p; simpl; auto using laterN_intuitionistically_2. Qed.
(* iris/bi/derived_laws_later.v *)
Lemma laterN_absorbingly n P : ▷^n <absorb> P ⊣⊢ <absorb> ▷^n P.
Proof. by rewrite /bi_absorbingly laterN_sep laterN_True. Qed.
(* iris/bi/derived_laws_later.v *)
Instance laterN_persistent n P : Persistent P → Persistent (▷^n P).
Proof. induction n; apply _. Qed.
(* iris/bi/derived_laws_later.v *)
Instance laterN_absorbing n P : Absorbing P → Absorbing (▷^n P).
Proof. induction n; apply _. Qed.
(* iris/bi/derived_laws_later.v *)
(* Except-0 *)
Instance except_0_ne : NonExpansive (@bi_except_0 PROP).
Proof. solve_proper. Qed.
(* iris/bi/derived_laws_later.v *)
Instance except_0_proper : Proper ((⊣⊢) ==> (⊣⊢)) (@bi_except_0 PROP).
Proof. solve_proper. Qed.
(* iris/bi/derived_laws_later.v *)
Instance except_0_mono' : Proper ((⊢) ==> (⊢)) (@bi_except_0 PROP).
Proof. solve_proper. Qed.
(* iris/bi/derived_laws_later.v *)
Instance except_0_flip_mono' :
  Proper (flip (⊢) ==> flip (⊢)) (@bi_except_0 PROP).
Proof. solve_proper. Qed.
(* iris/bi/derived_laws_later.v *)
Lemma except_0_intro P : P ⊢ ◇ P.
Proof. rewrite /bi_except_0; auto. Qed.
(* iris/bi/derived_laws_later.v *)
Lemma except_0_mono P Q : (P ⊢ Q) → ◇ P ⊢ ◇ Q.
Proof. by intros ->. Qed.
(* iris/bi/derived_laws_later.v *)
Lemma except_0_idemp P : ◇ ◇ P ⊣⊢ ◇ P.
Proof. apply (anti_symm _); rewrite /bi_except_0; auto. Qed.
(* iris/bi/derived_laws_later.v *)
Lemma except_0_True : ◇ True ⊣⊢ True.
Proof. rewrite /bi_except_0. apply (anti_symm _); auto. Qed.
(* iris/bi/derived_laws_later.v *)
Lemma except_0_emp `{!BiAffine PROP} : ◇ emp ⊣⊢ emp.
Proof. by rewrite -True_emp except_0_True. Qed.
(* iris/bi/derived_laws_later.v *)
Lemma except_0_or P Q : ◇ (P ∨ Q) ⊣⊢ ◇ P ∨ ◇ Q.
Proof. rewrite /bi_except_0. apply (anti_symm _); auto. Qed.
(* iris/bi/derived_laws_later.v *)
Lemma except_0_and P Q : ◇ (P ∧ Q) ⊣⊢ ◇ P ∧ ◇ Q.
Proof. by rewrite /bi_except_0 or_and_l. Qed.
(* iris/bi/derived_laws_later.v *)
Lemma except_0_sep P Q : ◇ (P ∗ Q) ⊣⊢ ◇ P ∗ ◇ Q.
Proof.
  rewrite /bi_except_0. apply (anti_symm _).
  - apply or_elim; last by auto using sep_mono.
    by rewrite -!or_intro_l -persistently_pure -later_sep -persistently_sep_dup.
  - rewrite sep_or_r !sep_or_l {1}(later_intro P) {1}(later_intro Q).
    rewrite -!later_sep !left_absorb right_absorb. auto.
Qed.
(* iris/bi/derived_laws_later.v *)
Lemma except_0_forall {A} (Φ : A → PROP) : ◇ (∀ a, Φ a) ⊣⊢ ∀ a, ◇ Φ a.
Proof.
  apply (anti_symm _).
  { apply forall_intro=> a. by rewrite (forall_elim a). }
  trans (▷ (∀ a : A, Φ a) ∧ (∀ a : A, ◇ Φ a))%I.
  { apply and_intro, reflexivity. rewrite later_forall. apply forall_mono=> a.
    apply or_elim; auto using later_intro. }
  rewrite later_false_em and_or_r. apply or_elim.
  { rewrite and_elim_l. apply or_intro_l. }
  apply or_intro_r', forall_intro=> a. rewrite !(forall_elim a).
  by rewrite and_or_l impl_elim_l and_elim_r idemp.
Qed.
(* iris/bi/derived_laws_later.v *)
Lemma except_0_exist_2 {A} (Φ : A → PROP) : (∃ a, ◇ Φ a) ⊢ ◇ ∃ a, Φ a.
Proof. apply exist_elim=> a. by rewrite (exist_intro a). Qed.
(* iris/bi/derived_laws_later.v *)
Lemma except_0_exist `{Inhabited A} (Φ : A → PROP) :
  ◇ (∃ a, Φ a) ⊣⊢ (∃ a, ◇ Φ a).
Proof.
  apply (anti_symm _); [|by apply except_0_exist_2]. apply or_elim.
  - rewrite -(exist_intro inhabitant). by apply or_intro_l.
  - apply exist_mono=> a. apply except_0_intro.
Qed.
(* iris/bi/derived_laws_later.v *)
Lemma except_0_later P : ◇ ▷ P ⊢ ▷ P.
Proof. by rewrite /bi_except_0 -later_or False_or. Qed.
(* iris/bi/derived_laws_later.v *)
Lemma except_0_laterN n P : ◇ ▷^n P ⊢ ▷^n ◇ P.
Proof. by destruct n as [|n]; rewrite //= ?except_0_later -except_0_intro. Qed.