phanerozoic/Coq-Iris huggingface dataset:
(* iris/bi/derived_connectives.v *)
(* Timeless propositions are propositions that do not depend on the step-index.
   There are two equivalent ways of expressing that a step-indexed proposition
   [P : nat → Prop] is timeless:
   * Option one, used here, says that [∀ n, P n → P (S n)]. In the logic, this
     is stated as [▷ P ⊢ ◇ P] (which actually reads [∀ n > 0, P (n-1) → P n],
     but this is trivially equivalent).
   * Option two says that [∀ n, P 0 → P n]. In the logic, this is stated as a
     meta-entailment [∀ P, (▷ False ∧ P ⊢ Q) → (P ⊢ Q)]. The assumption
     [▷ False] expresses that the step-index is 0.

   Both formulations are equivalent. In the logic, this can be shown using Löb
   induction and [later_false_em]. In the model, this follows from regular
   natural induction.
   The law [timeless_alt] in [derived_laws_later.v] provides option two, by
   proving that both versions are equivalent in the logic. *)
Class Timeless {PROP : bi} (P : PROP)
:= timeless : ▷ P ⊢ ◇ P.
(* iris/bi/derived_connectives.v *)
Instance : Params (@Timeless) 1
:= {}.
(* iris/bi/derived_connectives.v *)
(* An optional precondition [mP] to [Q].
    TODO: We may actually consider generalizing this to a list of preconditions,
    and e.g. also using it for texan triples. *)
Definition bi_wandM {PROP : bi} (mP : option PROP) (Q : PROP) : PROP
:=
  match mP with
  | None => Q
  | Some P => P -∗ Q
  end.
(* iris/bi/derived_connectives.v *)
Notation "mP -∗? Q"
:= (bi_wandM mP Q)
  (at level 99, Q at level 200, right associativity) : bi_scope.
(* iris/bi/derived_laws.v *)
(* Derived stuff about the entailment *)
Instance entails_anti_sym : AntiSymm (⊣⊢) (@bi_entails PROP).
Proof. intros P Q ??. by apply equiv_entails. Qed.
(* iris/bi/derived_laws.v *)
Lemma equiv_entails_1_1 P Q : (P ⊣⊢ Q) → (P ⊢ Q).
Proof. apply equiv_entails. Qed.
(* iris/bi/derived_laws.v *)
Lemma equiv_entails_1_2 P Q : (P ⊣⊢ Q) → (Q ⊢ P).
Proof. apply equiv_entails. Qed.
(* iris/bi/derived_laws.v *)
Lemma equiv_entails_2 P Q : (P ⊢ Q) → (Q ⊢ P) → (P ⊣⊢ Q).
Proof. intros. by apply equiv_entails. Qed.
(* iris/bi/derived_laws.v *)
Instance entails_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.
(* iris/bi/derived_laws.v *)
Lemma entails_equiv_l P Q R : (P ⊣⊢ Q) → (Q ⊢ R) → (P ⊢ R).
Proof. by intros ->. Qed.
(* iris/bi/derived_laws.v *)
Lemma entails_equiv_r P Q R : (P ⊢ Q) → (Q ⊣⊢ R) → (P ⊢ R).
Proof. by intros ? <-. Qed.
(* iris/bi/derived_laws.v *)
Instance bi_emp_valid_proper : Proper ((⊣⊢) ==> iff) (@bi_emp_valid PROP).
Proof. solve_proper. Qed.
(* iris/bi/derived_laws.v *)
Instance bi_emp_valid_mono : Proper ((⊢) ==> impl) (@bi_emp_valid PROP).
Proof. solve_proper. Qed.
(* iris/bi/derived_laws.v *)
Instance bi_emp_valid_flip_mono :
  Proper (flip (⊢) ==> flip impl) (@bi_emp_valid PROP).
Proof. solve_proper. Qed.
(* iris/bi/derived_laws.v *)
(* Propers *)
Instance pure_proper : Proper (iff ==> (⊣⊢)) (@bi_pure PROP) | 0.
Proof. intros φ1 φ2 Hφ. apply equiv_dist=> n. by apply pure_ne. Qed.
(* iris/bi/derived_laws.v *)
Instance and_proper :
  Proper ((⊣⊢) ==> (⊣⊢) ==> (⊣⊢)) (@bi_and PROP)
:= ne_proper_2 _.
(* iris/bi/derived_laws.v *)
Instance or_proper :
  Proper ((⊣⊢) ==> (⊣⊢) ==> (⊣⊢)) (@bi_or PROP)
:= ne_proper_2 _.
(* iris/bi/derived_laws.v *)
Instance impl_proper :
  Proper ((⊣⊢) ==> (⊣⊢) ==> (⊣⊢)) (@bi_impl PROP)
:= ne_proper_2 _.
(* iris/bi/derived_laws.v *)
Instance sep_proper :
  Proper ((⊣⊢) ==> (⊣⊢) ==> (⊣⊢)) (@bi_sep PROP)
:= ne_proper_2 _.
(* iris/bi/derived_laws.v *)
Instance wand_proper :
  Proper ((⊣⊢) ==> (⊣⊢) ==> (⊣⊢)) (@bi_wand PROP)
:= ne_proper_2 _.
(* iris/bi/derived_laws.v *)
Instance forall_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.
(* iris/bi/derived_laws.v *)
Instance exist_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.
(* iris/bi/derived_laws.v *)
Instance persistently_proper :
  Proper ((⊣⊢) ==> (⊣⊢)) (@bi_persistently PROP)
:= ne_proper _.
(* iris/bi/derived_laws.v *)
(* Derived logical stuff *)
Lemma and_elim_l' P Q R : (P ⊢ R) → P ∧ Q ⊢ R.
Proof. by rewrite and_elim_l. Qed.
(* iris/bi/derived_laws.v *)
Lemma and_elim_r' P Q R : (Q ⊢ R) → P ∧ Q ⊢ R.
Proof. by rewrite and_elim_r. Qed.
(* iris/bi/derived_laws.v *)
Lemma or_intro_l' P Q R : (P ⊢ Q) → P ⊢ Q ∨ R.
Proof. intros ->; apply or_intro_l. Qed.
(* iris/bi/derived_laws.v *)
Lemma or_intro_r' P Q R : (P ⊢ R) → P ⊢ Q ∨ R.
Proof. intros ->; apply or_intro_r. Qed.
(* iris/bi/derived_laws.v *)
Lemma exist_intro' {A} P (Ψ : A → PROP) a : (P ⊢ Ψ a) → P ⊢ ∃ a, Ψ a.
Proof. intros ->; apply exist_intro. Qed.
(* iris/bi/derived_laws.v *)
Lemma forall_elim' {A} P (Ψ : A → PROP) : (P ⊢ ∀ a, Ψ a) → ∀ a, P ⊢ Ψ a.
Proof. move=> HP a. by rewrite HP forall_elim. Qed.
(* iris/bi/derived_laws.v *)
Lemma impl_intro_l P Q R : (Q ∧ P ⊢ R) → P ⊢ Q → R.
Proof. intros HR; apply impl_intro_r; rewrite -HR; auto. Qed.
(* iris/bi/derived_laws.v *)
Lemma impl_elim P Q R : (P ⊢ Q → R) → (P ⊢ Q) → P ⊢ R.
Proof. intros. rewrite -(impl_elim_l' P Q R); auto. Qed.
(* iris/bi/derived_laws.v *)
Lemma impl_elim_r' P Q R : (Q ⊢ P → R) → P ∧ Q ⊢ R.
Proof. intros; apply impl_elim with P; auto. Qed.
(* iris/bi/derived_laws.v *)
Lemma impl_elim_l P Q : (P → Q) ∧ P ⊢ Q.
Proof. by apply impl_elim_l'. Qed.
(* iris/bi/derived_laws.v *)
Lemma impl_elim_r P Q : P ∧ (P → Q) ⊢ Q.
Proof. by apply impl_elim_r'. Qed.
(* iris/bi/derived_laws.v *)
Lemma False_elim P : False ⊢ P.
Proof. by apply (pure_elim' False). Qed.
(* iris/bi/derived_laws.v *)
Lemma True_intro P : P ⊢ True.
Proof. by apply pure_intro. Qed.
(* iris/bi/derived_laws.v *)
Lemma entails_eq_True P 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.
(* iris/bi/derived_laws.v *)
Lemma entails_impl_True P Q : (P ⊢ Q) ↔ (True ⊢ (P → Q)).
Proof. rewrite entails_eq_True equiv_entails; naive_solver. Qed.
(* iris/bi/derived_laws.v *)
Lemma and_mono P P' Q Q' : (P ⊢ Q) → (P' ⊢ Q') → P ∧ P' ⊢ Q ∧ Q'.
Proof. auto. Qed.
(* iris/bi/derived_laws.v *)
Lemma and_mono_l P P' Q : (P ⊢ Q) → P ∧ P' ⊢ Q ∧ P'.
Proof. by intros; apply and_mono. Qed.
(* iris/bi/derived_laws.v *)
Lemma and_mono_r P P' Q' : (P' ⊢ Q') → P ∧ P' ⊢ P ∧ Q'.
Proof. by apply and_mono. Qed.
(* iris/bi/derived_laws.v *)
Lemma or_mono P P' Q Q' : (P ⊢ Q) → (P' ⊢ Q') → P ∨ P' ⊢ Q ∨ Q'.
Proof. auto. Qed.
(* iris/bi/derived_laws.v *)
Lemma or_mono_l P P' Q : (P ⊢ Q) → P ∨ P' ⊢ Q ∨ P'.
Proof. by intros; apply or_mono. Qed.
(* iris/bi/derived_laws.v *)
Lemma or_mono_r P P' Q' : (P' ⊢ Q') → P ∨ P' ⊢ P ∨ Q'.
Proof. by apply or_mono. Qed.
(* iris/bi/derived_laws.v *)
Lemma impl_mono P 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.
(* iris/bi/derived_laws.v *)
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.
(* iris/bi/derived_laws.v *)
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.
(* iris/bi/derived_laws.v *)
Instance and_mono' : Proper ((⊢) ==> (⊢) ==> (⊢)) (@bi_and PROP).
Proof. by intros P P' HP Q Q' HQ; apply and_mono. Qed.
(* iris/bi/derived_laws.v *)
Instance and_flip_mono' :
  Proper (flip (⊢) ==> flip (⊢) ==> flip (⊢)) (@bi_and PROP).
Proof. by intros P P' HP Q Q' HQ; apply and_mono. Qed.
(* iris/bi/derived_laws.v *)
Instance or_mono' : Proper ((⊢) ==> (⊢) ==> (⊢)) (@bi_or PROP).
Proof. by intros P P' HP Q Q' HQ; apply or_mono. Qed.
(* iris/bi/derived_laws.v *)
Instance or_flip_mono' :
  Proper (flip (⊢) ==> flip (⊢) ==> flip (⊢)) (@bi_or PROP).
Proof. by intros P P' HP Q Q' HQ; apply or_mono. Qed.
(* iris/bi/derived_laws.v *)
Instance impl_mono' :
  Proper (flip (⊢) ==> (⊢) ==> (⊢)) (@bi_impl PROP).
Proof. by intros P P' HP Q Q' HQ; apply impl_mono. Qed.
(* iris/bi/derived_laws.v *)
Instance impl_flip_mono' :
  Proper ((⊢) ==> flip (⊢) ==> flip (⊢)) (@bi_impl PROP).
Proof. by intros P P' HP Q Q' HQ; apply impl_mono. Qed.
(* iris/bi/derived_laws.v *)
Instance forall_mono' A :
  Proper (pointwise_relation _ (⊢) ==> (⊢)) (@bi_forall PROP A).
Proof. intros P1 P2; apply forall_mono. Qed.
(* iris/bi/derived_laws.v *)
Instance forall_flip_mono' A :
  Proper (pointwise_relation _ (flip (⊢)) ==> flip (⊢)) (@bi_forall PROP A).
Proof. intros P1 P2; apply forall_mono. Qed.
(* iris/bi/derived_laws.v *)
Instance exist_mono' A :
  Proper (pointwise_relation _ ((⊢)) ==> (⊢)) (@bi_exist PROP A).
Proof. intros P1 P2; apply exist_mono. Qed.
(* iris/bi/derived_laws.v *)
Instance exist_flip_mono' A :
  Proper (pointwise_relation _ (flip (⊢)) ==> flip (⊢)) (@bi_exist PROP A).
Proof. intros P1 P2; apply exist_mono. Qed.
(* iris/bi/derived_laws.v *)
Instance and_idem : IdemP (⊣⊢) (@bi_and PROP).
Proof. intros P; apply (anti_symm (⊢)); auto. Qed.
(* iris/bi/derived_laws.v *)
Instance or_idem : IdemP (⊣⊢) (@bi_or PROP).
Proof. intros P; apply (anti_symm (⊢)); auto. Qed.
(* iris/bi/derived_laws.v *)
Instance and_comm : Comm (⊣⊢) (@bi_and PROP).
Proof. intros P Q; apply (anti_symm (⊢)); auto. Qed.
(* iris/bi/derived_laws.v *)
Instance True_and : LeftId (⊣⊢) True%I (@bi_and PROP).
Proof. intros P; apply (anti_symm (⊢)); auto. Qed.
(* iris/bi/derived_laws.v *)
Instance and_True : RightId (⊣⊢) True%I (@bi_and PROP).
Proof. intros P; apply (anti_symm (⊢)); auto. Qed.
(* iris/bi/derived_laws.v *)
Instance False_and : LeftAbsorb (⊣⊢) False%I (@bi_and PROP).
Proof. intros P; apply (anti_symm (⊢)); auto. Qed.
(* iris/bi/derived_laws.v *)
Instance and_False : RightAbsorb (⊣⊢) False%I (@bi_and PROP).
Proof. intros P; apply (anti_symm (⊢)); auto. Qed.
(* iris/bi/derived_laws.v *)
Instance True_or : LeftAbsorb (⊣⊢) True%I (@bi_or PROP).
Proof. intros P; apply (anti_symm (⊢)); auto. Qed.
(* iris/bi/derived_laws.v *)
Instance or_True : RightAbsorb (⊣⊢) True%I (@bi_or PROP).
Proof. intros P; apply (anti_symm (⊢)); auto. Qed.
(* iris/bi/derived_laws.v *)
Instance False_or : LeftId (⊣⊢) False%I (@bi_or PROP).
Proof. intros P; apply (anti_symm (⊢)); auto. Qed.
(* iris/bi/derived_laws.v *)
Instance or_False : RightId (⊣⊢) False%I (@bi_or PROP).
Proof. intros P; apply (anti_symm (⊢)); auto. Qed.
(* iris/bi/derived_laws.v *)
Instance and_assoc : Assoc (⊣⊢) (@bi_and PROP).
Proof. intros P Q R; apply (anti_symm (⊢)); auto. Qed.
(* iris/bi/derived_laws.v *)
Instance or_comm : Comm (⊣⊢) (@bi_or PROP).
Proof. intros P Q; apply (anti_symm (⊢)); auto. Qed.
(* iris/bi/derived_laws.v *)
Instance or_assoc : Assoc (⊣⊢) (@bi_or PROP).
Proof. intros P Q R; apply (anti_symm (⊢)); auto. Qed.
(* iris/bi/derived_laws.v *)
Instance True_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.
(* iris/bi/derived_laws.v *)
Lemma impl_refl P Q : Q ⊢ P → P.
Proof. apply impl_intro_l, and_elim_l. Qed.
(* iris/bi/derived_laws.v *)
Lemma impl_trans P Q R : (P → Q) ∧ (Q → R) ⊢ (P → R).
Proof. apply impl_intro_l. by rewrite assoc !impl_elim_r. Qed.
(* iris/bi/derived_laws.v *)
Lemma False_impl P : (False → P) ⊣⊢ True.
Proof.
  apply (anti_symm (⊢)); [by auto|].
  apply impl_intro_l. rewrite left_absorb. auto.
Qed.
(* iris/bi/derived_laws.v *)
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.
(* iris/bi/derived_laws.v *)
Lemma forall_unit (Ψ : unit → PROP) :
  (∀ x, Ψ x) ⊣⊢ Ψ ().
Proof.
  apply (anti_symm (⊢)).
  - rewrite (forall_elim ()) //.
  - apply forall_intro=>[[]]. done.
Qed.
(* iris/bi/derived_laws.v *)
Lemma exist_unit (Ψ : unit → PROP) :
  (∃ x, Ψ x) ⊣⊢ Ψ ().
Proof.
  apply (anti_symm (⊢)).
  - apply exist_elim=>[[]]. done.
  - rewrite -(exist_intro ()). done.
Qed.
(* iris/bi/derived_laws.v *)
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.
(* iris/bi/derived_laws.v *)
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.
(* iris/bi/derived_laws.v *)
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.
(* iris/bi/derived_laws.v *)
Lemma impl_curry P 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.
(* iris/bi/derived_laws.v *)
Lemma or_and_l P 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.
(* iris/bi/derived_laws.v *)
Lemma or_and_r P Q R : P ∧ Q ∨ R ⊣⊢ (P ∨ R) ∧ (Q ∨ R).
Proof. by rewrite -!(comm _ R) or_and_l. Qed.
(* iris/bi/derived_laws.v *)
Lemma and_or_l P 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.
(* iris/bi/derived_laws.v *)
Lemma and_or_r P Q R : (P ∨ Q) ∧ R ⊣⊢ P ∧ R ∨ Q ∧ R.
Proof. by rewrite -!(comm _ R) and_or_l. Qed.
(* iris/bi/derived_laws.v *)
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.
(* iris/bi/derived_laws.v *)
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.
(* iris/bi/derived_laws.v *)
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.
(* iris/bi/derived_laws.v *)
Lemma and_alt P 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.
(* iris/bi/derived_laws.v *)
Lemma or_alt P 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.
(* iris/bi/derived_laws.v *)
Lemma entails_equiv_and P Q : (P ⊣⊢ Q ∧ P) ↔ (P ⊢ Q).
Proof.
  split.
  - intros ->; auto.
  - intros; apply (anti_symm _); auto.
Qed.
(* iris/bi/derived_laws.v *)
Instance iff_ne : NonExpansive2 (@bi_iff PROP).
Proof. unfold bi_iff; solve_proper. Qed.
(* iris/bi/derived_laws.v *)
Instance iff_proper :
  Proper ((⊣⊢) ==> (⊣⊢) ==> (⊣⊢)) (@bi_iff PROP)
:= ne_proper_2 _.
(* iris/bi/derived_laws.v *)
Lemma iff_refl Q P : Q ⊢ P ↔ P.
Proof. rewrite /bi_iff. apply and_intro; apply impl_refl. Qed.
(* iris/bi/derived_laws.v *)
Lemma iff_sym P Q : (P ↔ Q) ⊣⊢ (Q ↔ P).
Proof.
  apply equiv_entails. split; apply and_intro;
    try apply and_elim_r; apply and_elim_l.
Qed.
(* iris/bi/derived_laws.v *)
Lemma iff_trans P 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.
(* iris/bi/derived_laws.v *)
Lemma sep_mono_l P P' Q : (P ⊢ Q) → P ∗ P' ⊢ Q ∗ P'.
Proof. by intros; apply sep_mono. Qed.
(* iris/bi/derived_laws.v *)
Lemma sep_mono_r P P' Q' : (P' ⊢ Q') → P ∗ P' ⊢ P ∗ Q'.
Proof. by apply sep_mono. Qed.
(* iris/bi/derived_laws.v *)
Instance sep_mono' : Proper ((⊢) ==> (⊢) ==> (⊢)) (@bi_sep PROP).
Proof. by intros P P' HP Q Q' HQ; apply sep_mono. Qed.
(* iris/bi/derived_laws.v *)
Instance sep_flip_mono' :
  Proper (flip (⊢) ==> flip (⊢) ==> flip (⊢)) (@bi_sep PROP).
Proof. by intros P P' HP Q Q' HQ; apply sep_mono. Qed.
(* iris/bi/derived_laws.v *)
Lemma wand_mono P 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.
(* iris/bi/derived_laws.v *)
Instance wand_mono' : Proper (flip (⊢) ==> (⊢) ==> (⊢)) (@bi_wand PROP).
Proof. by intros P P' HP Q Q' HQ; apply wand_mono. Qed.
(* iris/bi/derived_laws.v *)
Instance wand_flip_mono' :
  Proper ((⊢) ==> flip (⊢) ==> flip (⊢)) (@bi_wand PROP).
Proof. by intros P P' HP Q Q' HQ; apply wand_mono. Qed.
(* iris/bi/derived_laws.v *)
Instance sep_comm : Comm (⊣⊢) (@bi_sep PROP).
Proof. intros P Q; apply (anti_symm _); auto using sep_comm'. Qed.
(* iris/bi/derived_laws.v *)
Instance sep_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.
(* iris/bi/derived_laws.v *)
Instance emp_sep : LeftId (⊣⊢) emp%I (@bi_sep PROP).
Proof. intros P; apply (anti_symm _); auto using emp_sep_1, emp_sep_2. Qed.
(* iris/bi/derived_laws.v *)
Instance sep_emp : RightId (⊣⊢) emp%I (@bi_sep PROP).
Proof. by intros P; rewrite comm left_id. Qed.
(* iris/bi/derived_laws.v *)
Instance sep_False : LeftAbsorb (⊣⊢) False%I (@bi_sep PROP).
Proof. intros P; apply (anti_symm _); auto using wand_elim_l'. Qed.
(* iris/bi/derived_laws.v *)
Instance False_sep : RightAbsorb (⊣⊢) False%I (@bi_sep PROP).
Proof. intros P. by rewrite comm left_absorb. Qed.
(* iris/bi/derived_laws.v *)
Lemma True_sep_2 P : P ⊢ True ∗ P.
Proof. rewrite -{1}[P](left_id emp%I bi_sep). auto using sep_mono. Qed.
(* iris/bi/derived_laws.v *)
Lemma sep_True_2 P : P ⊢ P ∗ True.
Proof. by rewrite comm -True_sep_2. Qed.
(* iris/bi/derived_laws.v *)
Lemma sep_intro_emp_valid_l P Q R : (⊢ P) → (R ⊢ Q) → R ⊢ P ∗ Q.
Proof. intros ? ->. rewrite -{1}(left_id emp%I _ Q). by apply sep_mono. Qed.
(* iris/bi/derived_laws.v *)
Lemma sep_intro_emp_valid_r P Q R : (R ⊢ P) → (⊢ Q) → R ⊢ P ∗ Q.
Proof. intros -> ?. rewrite comm. by apply sep_intro_emp_valid_l. Qed.
(* iris/bi/derived_laws.v *)
Lemma sep_elim_emp_valid_l P Q R : (⊢ P) → (P ∗ R ⊢ Q) → R ⊢ Q.
Proof. intros <- <-. by rewrite left_id. Qed.
(* iris/bi/derived_laws.v *)
Lemma sep_elim_emp_valid_r P Q R : (⊢P) → (R ∗ P ⊢ Q) → R ⊢ Q.
Proof. intros <- <-. by rewrite right_id. Qed.
(* iris/bi/derived_laws.v *)
Lemma wand_intro_l P Q R : (Q ∗ P ⊢ R) → P ⊢ Q -∗ R.
Proof. rewrite comm; apply wand_intro_r. Qed.
(* iris/bi/derived_laws.v *)
Lemma wand_elim_l P Q : (P -∗ Q) ∗ P ⊢ Q.
Proof. by apply wand_elim_l'. Qed.
(* iris/bi/derived_laws.v *)
Lemma wand_elim_r P Q : P ∗ (P -∗ Q) ⊢ Q.
Proof. rewrite (comm _ P); apply wand_elim_l. Qed.
(* iris/bi/derived_laws.v *)
Lemma wand_elim_r' P Q R : (Q ⊢ P -∗ R) → P ∗ Q ⊢ R.
Proof. intros ->; apply wand_elim_r. Qed.
(* iris/bi/derived_laws.v *)
Lemma wand_apply P Q R S : (P ⊢ Q -∗ R) → (S ⊢ P ∗ Q) → S ⊢ R.
Proof. intros HR%wand_elim_l' HQ. by rewrite HQ. Qed.
(* iris/bi/derived_laws.v *)
Lemma wand_frame_l P Q R : (Q -∗ R) ⊢ P ∗ Q -∗ P ∗ R.
Proof. apply wand_intro_l. rewrite -assoc. apply sep_mono_r, wand_elim_r. Qed.
(* iris/bi/derived_laws.v *)
Lemma wand_frame_r P 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.
(* iris/bi/derived_laws.v *)
Instance emp_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.
(* iris/bi/derived_laws.v *)
Lemma False_wand P : (False -∗ P) ⊣⊢ True.
Proof.
  apply (anti_symm (⊢)); [by auto|].
  apply wand_intro_l. rewrite left_absorb. auto.
Qed.
(* iris/bi/derived_laws.v *)
Lemma wand_refl P : ⊢ P -∗ P.
Proof. apply wand_intro_l. by rewrite right_id. Qed.
(* iris/bi/derived_laws.v *)
Lemma wand_trans P Q R : (P -∗ Q) ∗ (Q -∗ R) ⊢ (P -∗ R).
Proof. apply wand_intro_l. by rewrite assoc !wand_elim_r. Qed.
(* iris/bi/derived_laws.v *)
Lemma wand_curry P 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.
(* iris/bi/derived_laws.v *)
Lemma sep_and_l P Q R : P ∗ (Q ∧ R) ⊢ (P ∗ Q) ∧ (P ∗ R).
Proof. auto. Qed.
(* iris/bi/derived_laws.v *)
Lemma sep_and_r P Q R : (P ∧ Q) ∗ R ⊢ (P ∗ R) ∧ (Q ∗ R).
Proof. auto. Qed.
(* iris/bi/derived_laws.v *)
Lemma sep_or_l P 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.
(* iris/bi/derived_laws.v *)
Lemma sep_or_r P Q R : (P ∨ Q) ∗ R ⊣⊢ (P ∗ R) ∨ (Q ∗ R).
Proof. by rewrite -!(comm _ R) sep_or_l. Qed.
(* iris/bi/derived_laws.v *)
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.
(* iris/bi/derived_laws.v *)
Lemma sep_exist_r {A} (Φ: A → PROP) Q: (∃ a, Φ a) ∗ Q ⊣⊢ ∃ a, Φ a ∗ Q.
Proof. setoid_rewrite (comm _ _ Q); apply sep_exist_l. Qed.
(* iris/bi/derived_laws.v *)
Lemma sep_forall_l {A} P (Ψ : A → PROP) : P ∗ (∀ a, Ψ a) ⊢ ∀ a, P ∗ Ψ a.
Proof. by apply forall_intro=> a; rewrite forall_elim. Qed.
(* iris/bi/derived_laws.v *)
Lemma sep_forall_r {A} (Φ : A → PROP) Q : (∀ a, Φ a) ∗ Q ⊢ ∀ a, Φ a ∗ Q.
Proof. by apply forall_intro=> a; rewrite forall_elim. Qed.
(* iris/bi/derived_laws.v *)
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.
(* iris/bi/derived_laws.v *)
Instance wand_iff_ne : NonExpansive2 (@bi_wand_iff PROP).
Proof. solve_proper. Qed.
(* iris/bi/derived_laws.v *)
Instance wand_iff_proper :
  Proper ((⊣⊢) ==> (⊣⊢) ==> (⊣⊢)) (@bi_wand_iff PROP)
:= ne_proper_2 _.
(* iris/bi/derived_laws.v *)
Lemma wand_iff_refl P : ⊢ P ∗-∗ P.
Proof. apply and_intro; apply wand_intro_l; by rewrite right_id. Qed.
(* iris/bi/derived_laws.v *)
Lemma wand_iff_sym P Q : (P ∗-∗ Q) ⊣⊢ (Q ∗-∗ P).
Proof. apply equiv_entails; split; rewrite /bi_wand_iff; eauto. Qed.
(* iris/bi/derived_laws.v *)
Lemma wand_iff_trans P 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.
(* iris/bi/derived_laws.v *)
Lemma wand_entails P Q : (⊢ P -∗ Q) → P ⊢ Q.
Proof. intros. rewrite -[P]emp_sep. by apply wand_elim_l'. Qed.
(* iris/bi/derived_laws.v *)
Lemma entails_wand P Q : (P ⊢ Q) → ⊢ P -∗ Q.
Proof. intros ->. apply wand_intro_r. by rewrite left_id. Qed.
(* iris/bi/derived_laws.v *)
(* A version that works with rewrite, in which bi_emp_valid is unfolded. *)
Lemma entails_wand' P Q : (P ⊢ Q) → emp ⊢ (P -∗ Q).
Proof. apply entails_wand. Qed.
(* iris/bi/derived_laws.v *)
Lemma wand_entails' P Q : (emp ⊢ (P -∗ Q)) → P ⊢ Q.
Proof. apply wand_entails. Qed.
(* iris/bi/derived_laws.v *)
Lemma equiv_wand_iff P Q : (P ⊣⊢ Q) → ⊢ P ∗-∗ Q.
Proof. intros ->; apply wand_iff_refl. Qed.