phanerozoic/Coq-Iris huggingface dataset:
(* iris/bi/derived_laws_later.v *)
Lemma except_0_into_later P : ◇ P ⊢ ▷ P.
Proof. by rewrite -except_0_later -later_intro. Qed.
(* iris/bi/derived_laws_later.v *)
Lemma except_0_persistently P : ◇ <pers> P ⊣⊢ <pers> ◇ P.
Proof.
  by rewrite /bi_except_0 persistently_or -later_persistently persistently_pure.
Qed.
(* iris/bi/derived_laws_later.v *)
Lemma except_0_affinely_2 P : <affine> ◇ P ⊢ ◇ <affine> P.
Proof. rewrite /bi_affinely except_0_and. auto using except_0_intro. Qed.
(* iris/bi/derived_laws_later.v *)
Lemma except_0_intuitionistically_2 P : □ ◇ P ⊢ ◇ □ P.
Proof. by rewrite /bi_intuitionistically -except_0_persistently except_0_affinely_2. Qed.
(* iris/bi/derived_laws_later.v *)
Lemma except_0_intuitionistically_if_2 p P : □?p ◇ P ⊢ ◇ □?p P.
Proof. destruct p; simpl; auto using except_0_intuitionistically_2. Qed.
(* iris/bi/derived_laws_later.v *)
Lemma except_0_absorbingly P : ◇ <absorb> P ⊣⊢ <absorb> ◇ P.
Proof. by rewrite /bi_absorbingly except_0_sep except_0_True. Qed.
(* iris/bi/derived_laws_later.v *)
Lemma except_0_frame_l P Q : P ∗ ◇ Q ⊢ ◇ (P ∗ Q).
Proof. by rewrite {1}(except_0_intro P) except_0_sep. Qed.
(* iris/bi/derived_laws_later.v *)
Lemma except_0_frame_r P Q : ◇ P ∗ Q ⊢ ◇ (P ∗ Q).
Proof. by rewrite {1}(except_0_intro Q) except_0_sep. Qed.
(* iris/bi/derived_laws_later.v *)
Lemma later_affinely_1 `{!Timeless (PROP:=PROP) emp} P : ▷ <affine> P ⊢ ◇ <affine> ▷ P.
Proof.
  rewrite /bi_affinely later_and (timeless emp) except_0_and.
  by apply and_mono, except_0_intro.
Qed.
(* iris/bi/derived_laws_later.v *)
Instance except_0_persistent P : Persistent P → Persistent (◇ P).
Proof. rewrite /bi_except_0; apply _. Qed.
(* iris/bi/derived_laws_later.v *)
Instance except_0_absorbing P : Absorbing P → Absorbing (◇ P).
Proof. rewrite /bi_except_0; apply _. Qed.
(* iris/bi/derived_laws_later.v *)
(* Timeless instances *)
Instance Timeless_proper : Proper ((≡) ==> iff) (@Timeless PROP).
Proof. solve_proper. Qed.
(* iris/bi/derived_laws_later.v *)
(* The left-to-right direction of this lemma shows that to prove a timeless
   proposition [Q], we can additionally assume that we are at step-index 0, i.e.
   we can add [▷ False] to our assumptions. The right-to-left direction shows
   that this is in fact an exact characterization of timeless propositions.
   See also the comment above the definition of [Timeless]. *)
Lemma timeless_alt `{!BiLöb PROP} Q :
  Timeless Q ↔ (∀ P, (▷ False ∧ P ⊢ Q) → (P ⊢ Q)).
Proof.
  split; rewrite /Timeless => H.
  * intros P Hpr.
    rewrite -(löb Q). apply impl_intro_l.
    rewrite H /bi_except_0 and_or_r. apply or_elim; auto.
  * rewrite later_false_em.
    apply or_mono; first done.
    apply H, impl_elim_r.
Qed.
(* iris/bi/derived_laws_later.v *)
Instance pure_timeless φ : Timeless (PROP:=PROP) ⌜φ⌝.
Proof.
  rewrite /Timeless /bi_except_0 pure_alt later_exist_false.
  apply or_elim, exist_elim; [auto|]=> Hφ. rewrite -(exist_intro Hφ). auto.
Qed.
(* iris/bi/derived_laws_later.v *)
Instance emp_timeless `{!BiAffine PROP} : Timeless (PROP:=PROP) emp.
Proof. rewrite -True_emp. apply _. Qed.
(* iris/bi/derived_laws_later.v *)
Instance and_timeless P Q : Timeless P → Timeless Q → Timeless (P ∧ Q).
Proof. intros; rewrite /Timeless except_0_and later_and; auto. Qed.
(* iris/bi/derived_laws_later.v *)
Instance or_timeless P Q : Timeless P → Timeless Q → Timeless (P ∨ Q).
Proof. intros; rewrite /Timeless except_0_or later_or; auto. Qed.
(* iris/bi/derived_laws_later.v *)
Instance impl_timeless `{!BiLöb PROP} P Q : Timeless Q → Timeless (P → Q).
Proof.
  rewrite !timeless_alt=> HQ R HR. apply impl_intro_l, HQ.
  rewrite assoc -(comm _ P) -assoc. by apply impl_elim_r'.
Qed.
(* iris/bi/derived_laws_later.v *)
Instance sep_timeless P Q: Timeless P → Timeless Q → Timeless (P ∗ Q).
Proof.
  intros; rewrite /Timeless except_0_sep later_sep; auto using sep_mono.
Qed.
(* iris/bi/derived_laws_later.v *)
Instance wand_timeless `{!BiLöb PROP} P Q : Timeless Q → Timeless (P -∗ Q).
Proof.
  rewrite !timeless_alt=> HQ R HR. apply wand_intro_l, HQ.
  rewrite persistent_and_affinely_sep_l assoc -(comm _ P) -assoc.
  rewrite -persistent_and_affinely_sep_l. by apply wand_elim_r'.
Qed.
(* iris/bi/derived_laws_later.v *)
Instance forall_timeless {A} (Ψ : A → PROP) :
  (∀ x, Timeless (Ψ x)) → Timeless (∀ x, Ψ x).
Proof.
  rewrite /Timeless=> HQ. rewrite except_0_forall later_forall.
  apply forall_mono; auto.
Qed.
(* iris/bi/derived_laws_later.v *)
Instance exist_timeless {A} (Ψ : A → PROP) :
  (∀ x, Timeless (Ψ x)) → Timeless (∃ x, Ψ x).
Proof.
  rewrite /Timeless=> ?. rewrite later_exist_false. apply or_elim.
  - rewrite /bi_except_0; auto.
  - apply exist_elim=> x. rewrite -(exist_intro x); auto.
Qed.
(* iris/bi/derived_laws_later.v *)
Instance persistently_timeless P : Timeless P → Timeless (<pers> P).
Proof.
  intros. rewrite /Timeless /bi_except_0 later_persistently_1.
  by rewrite (timeless P) /bi_except_0 persistently_or {1}persistently_elim.
Qed.
(* iris/bi/derived_laws_later.v *)
Instance affinely_timeless P :
  Timeless (PROP:=PROP) emp → Timeless P → Timeless (<affine> P).
Proof. rewrite /bi_affinely; apply _. Qed.
(* iris/bi/derived_laws_later.v *)
Instance absorbingly_timeless P : Timeless P → Timeless (<absorb> P).
Proof. rewrite /bi_absorbingly; apply _. Qed.
(* iris/bi/derived_laws_later.v *)
Instance intuitionistically_timeless P :
  Timeless (PROP:=PROP) emp → Timeless P → Timeless (□ P).
Proof. rewrite /bi_intuitionistically; apply _. Qed.
(* iris/bi/derived_laws_later.v *)
Instance from_option_timeless {A} P (Ψ : A → PROP) (mx : option A) :
  (∀ x, Timeless (Ψ x)) → Timeless P → Timeless (from_option Ψ P mx).
Proof. destruct mx; apply _. Qed.
(* iris/bi/derived_laws_later.v *)
Lemma timeless_laterN P n : Timeless P → ▷^n P ⊢ ▷^n False ∨ P.
Proof.
  intros. induction n as [|n IH]; simpl; first by auto.
  rewrite IH later_or. apply or_elim; first by auto.
  rewrite timeless. apply or_mono; auto.
Qed.
(* iris/bi/derived_laws_later.v *)
(* Big op stuff *)
Instance bi_later_monoid_and_homomorphism :
  MonoidHomomorphism bi_and bi_and (≡) (@bi_later PROP).
Proof.
  split; [split|]; try apply _.
  - apply later_and.
  - apply later_True.
Qed.
(* iris/bi/derived_laws_later.v *)
Instance bi_laterN_and_homomorphism n :
  MonoidHomomorphism bi_and bi_and (≡) (@bi_laterN PROP n).
Proof.
  split; [split|]; try apply _.
  - apply laterN_and.
  - apply laterN_True.
Qed.
(* iris/bi/derived_laws_later.v *)
Instance bi_except_0_and_homomorphism :
  MonoidHomomorphism bi_and bi_and (≡) (@bi_except_0 PROP).
Proof.
  split; [split|]; try apply _.
  - apply except_0_and.
  - apply except_0_True.
Qed.
(* iris/bi/derived_laws_later.v *)
Instance bi_later_monoid_or_homomorphism :
  WeakMonoidHomomorphism bi_or bi_or (≡) (@bi_later PROP).
Proof. split; try apply _. apply later_or. Qed.
(* iris/bi/derived_laws_later.v *)
Instance bi_laterN_or_homomorphism n :
  WeakMonoidHomomorphism bi_or bi_or (≡) (@bi_laterN PROP n).
Proof. split; try apply _. apply laterN_or. Qed.
(* iris/bi/derived_laws_later.v *)
Instance bi_except_0_or_homomorphism :
  WeakMonoidHomomorphism bi_or bi_or (≡) (@bi_except_0 PROP).
Proof. split; try apply _. apply except_0_or. Qed.
(* iris/bi/derived_laws_later.v *)
Instance bi_later_monoid_sep_weak_homomorphism :
  WeakMonoidHomomorphism bi_sep bi_sep (≡) (@bi_later PROP).
Proof. split; try apply _. apply later_sep. Qed.
(* iris/bi/derived_laws_later.v *)
Instance bi_laterN_sep_weak_homomorphism n :
  WeakMonoidHomomorphism bi_sep bi_sep (≡) (@bi_laterN PROP n).
Proof. split; try apply _. apply laterN_sep. Qed.
(* iris/bi/derived_laws_later.v *)
Instance bi_except_0_sep_weak_homomorphism :
  WeakMonoidHomomorphism bi_sep bi_sep (≡) (@bi_except_0 PROP).
Proof. split; try apply _. apply except_0_sep. Qed.
(* iris/bi/derived_laws_later.v *)
Instance bi_later_monoid_sep_homomorphism `{!BiAffine PROP} :
  MonoidHomomorphism bi_sep bi_sep (≡) (@bi_later PROP).
Proof. split; try apply _. apply later_emp. Qed.
(* iris/bi/derived_laws_later.v *)
Instance bi_laterN_sep_homomorphism `{!BiAffine PROP} n :
  MonoidHomomorphism bi_sep bi_sep (≡) (@bi_laterN PROP n).
Proof. split; try apply _. apply laterN_emp. Qed.
(* iris/bi/derived_laws_later.v *)
Instance bi_except_0_sep_homomorphism `{!BiAffine PROP} :
  MonoidHomomorphism bi_sep bi_sep (≡) (@bi_except_0 PROP).
Proof. split; try apply _. apply except_0_emp. Qed.
(* iris/bi/derived_laws_later.v *)
Instance bi_later_monoid_sep_entails_weak_homomorphism :
  WeakMonoidHomomorphism bi_sep bi_sep (flip (⊢)) (@bi_later PROP).
Proof. split; try apply _. intros P Q. by rewrite later_sep. Qed.
(* iris/bi/derived_laws_later.v *)
Instance bi_laterN_sep_entails_weak_homomorphism n :
  WeakMonoidHomomorphism bi_sep bi_sep (flip (⊢)) (@bi_laterN PROP n).
Proof. split; try apply _. intros P Q. by rewrite laterN_sep. Qed.
(* iris/bi/derived_laws_later.v *)
Instance bi_except_0_sep_entails_weak_homomorphism :
  WeakMonoidHomomorphism bi_sep bi_sep (flip (⊢)) (@bi_except_0 PROP).
Proof. split; try apply _. intros P Q. by rewrite except_0_sep. Qed.
(* iris/bi/derived_laws_later.v *)
Instance bi_later_monoid_sep_entails_homomorphism :
  MonoidHomomorphism bi_sep bi_sep (flip (⊢)) (@bi_later PROP).
Proof. split; try apply _. apply later_intro. Qed.
(* iris/bi/derived_laws_later.v *)
Instance bi_laterN_sep_entails_homomorphism n :
  MonoidHomomorphism bi_sep bi_sep (flip (⊢)) (@bi_laterN PROP n).
Proof. split; try apply _. apply laterN_intro. Qed.
(* iris/bi/derived_laws_later.v *)
Instance bi_except_0_sep_entails_homomorphism :
  MonoidHomomorphism bi_sep bi_sep (flip (⊢)) (@bi_except_0 PROP).
Proof. split; try apply _. apply except_0_intro. Qed.
(* iris/bi/embedding.v *)
Class Embed (A B : Type)
:= embed : A → B.
(* iris/bi/embedding.v *)
Notation "⎡ P ⎤"
:= (embed P) : bi_scope.
(* iris/bi/embedding.v *)
Instance : Params (@embed) 3
:= {}.
(* iris/bi/embedding.v *)
(* Mixins allow us to create instances easily without having to use Program *)
Record BiEmbedMixin (PROP1 PROP2 : bi) `(Embed PROP1 PROP2)
:= {
  bi_embed_mixin_ne : NonExpansive (embed (A:=PROP1) (B:=PROP2));
  bi_embed_mixin_mono : Proper ((⊢) ==> (⊢)) (embed (A:=PROP1) (B:=PROP2));
  bi_embed_mixin_emp_valid_inj (P : PROP1) :
    (⊢@{PROP2} ⎡P⎤) → ⊢ P;
  bi_embed_mixin_emp_2 : emp ⊢@{PROP2} ⎡emp⎤;
  bi_embed_mixin_impl_2 (P Q : PROP1) :
    (⎡P⎤ → ⎡Q⎤) ⊢@{PROP2} ⎡P → Q⎤;
  bi_embed_mixin_forall_2 A (Φ : A → PROP1) :
    (∀ x, ⎡Φ x⎤) ⊢@{PROP2} ⎡∀ x, Φ x⎤;
  bi_embed_mixin_exist_1 A (Φ : A → PROP1) :
    ⎡∃ x, Φ x⎤ ⊢@{PROP2} ∃ x, ⎡Φ x⎤;
  bi_embed_mixin_sep (P Q : PROP1) :
    ⎡P ∗ Q⎤ ⊣⊢@{PROP2} ⎡P⎤ ∗ ⎡Q⎤;
  bi_embed_mixin_wand_2 (P Q : PROP1) :
    (⎡P⎤ -∗ ⎡Q⎤) ⊢@{PROP2} ⎡P -∗ Q⎤;
  bi_embed_mixin_persistently (P : PROP1) :
    ⎡<pers> P⎤ ⊣⊢@{PROP2} <pers> ⎡P⎤
}.
(* iris/bi/embedding.v *)
Class BiEmbed (PROP1 PROP2 : bi)
:= {
  #[global] bi_embed_embed :: Embed PROP1 PROP2;
  bi_embed_mixin : BiEmbedMixin PROP1 PROP2 bi_embed_embed;
}.
(* iris/bi/embedding.v *)
Class BiEmbedEmp (PROP1 PROP2 : bi) `{!BiEmbed PROP1 PROP2}
:=
  embed_emp_1 : ⎡ emp : PROP1 ⎤ ⊢ emp.
(* iris/bi/embedding.v *)
Class BiEmbedLater (PROP1 PROP2 : bi) `{!BiEmbed PROP1 PROP2}
:=
  embed_later P : ⎡▷ P⎤ ⊣⊢@{PROP2} ▷ ⎡P⎤.
(* iris/bi/embedding.v *)
Class BiEmbedBUpd (PROP1 PROP2 : bi)
    `{!BiEmbed PROP1 PROP2, !BiBUpd PROP1, !BiBUpd PROP2}
:=
  embed_bupd P : ⎡|==> P⎤ ⊣⊢@{PROP2} |==> ⎡P⎤.
(* iris/bi/embedding.v *)
Class BiEmbedFUpd (PROP1 PROP2 : bi)
    `{!BiEmbed PROP1 PROP2, !BiFUpd PROP1, !BiFUpd PROP2}
:=
  embed_fupd E1 E2 P : ⎡|={E1,E2}=> P⎤ ⊣⊢@{PROP2} |={E1,E2}=> ⎡P⎤.
(* iris/bi/embedding.v *)
Class BiEmbedSbi (PROP1 PROP2 : bi)
    `{!BiEmbed PROP1 PROP2, !Sbi PROP1, !Sbi PROP2}
:= {
  embed_si_emp_valid (P : PROP1) :
    <si_emp_valid> ⎡ P ⎤ ⊣⊢@{siPropI} <si_emp_valid> P;
  embed_si_pure_1 Pi : ⎡ <si_pure> Pi ⎤ ⊢@{PROP2} <si_pure> Pi;
}.
(* iris/bi/embedding.v *)
Notation embed
:= (embed (A:=bi_car PROP1) (B:=bi_car PROP2)).
(* iris/bi/embedding.v *)
Instance embed_ne : NonExpansive embed.
Proof. eapply bi_embed_mixin_ne, bi_embed_mixin. Qed.
(* iris/bi/embedding.v *)
Instance embed_mono : Proper ((⊢) ==> (⊢)) embed.
Proof. eapply bi_embed_mixin_mono, bi_embed_mixin. Qed.
(* iris/bi/embedding.v *)
Lemma embed_emp_valid_inj P : (⊢@{PROP2} ⎡P⎤) → ⊢ P.
Proof. eapply bi_embed_mixin_emp_valid_inj, bi_embed_mixin. Qed.
(* iris/bi/embedding.v *)
Lemma embed_emp_2 : emp ⊢ ⎡emp⎤.
Proof. eapply bi_embed_mixin_emp_2, bi_embed_mixin. Qed.
(* iris/bi/embedding.v *)
Lemma embed_impl_2 P Q : (⎡P⎤ → ⎡Q⎤) ⊢ ⎡P → Q⎤.
Proof. eapply bi_embed_mixin_impl_2, bi_embed_mixin. Qed.
(* iris/bi/embedding.v *)
Lemma embed_forall_2 A (Φ : A → PROP1) : (∀ x, ⎡Φ x⎤) ⊢ ⎡∀ x, Φ x⎤.
Proof. eapply bi_embed_mixin_forall_2, bi_embed_mixin. Qed.
(* iris/bi/embedding.v *)
Lemma embed_exist_1 A (Φ : A → PROP1) : ⎡∃ x, Φ x⎤ ⊢ ∃ x, ⎡Φ x⎤.
Proof. eapply bi_embed_mixin_exist_1, bi_embed_mixin. Qed.
(* iris/bi/embedding.v *)
Lemma embed_sep P Q : ⎡P ∗ Q⎤ ⊣⊢ ⎡P⎤ ∗ ⎡Q⎤.
Proof. eapply bi_embed_mixin_sep, bi_embed_mixin. Qed.
(* iris/bi/embedding.v *)
Lemma embed_wand_2 P Q : (⎡P⎤ -∗ ⎡Q⎤) ⊢ ⎡P -∗ Q⎤.
Proof. eapply bi_embed_mixin_wand_2, bi_embed_mixin. Qed.
(* iris/bi/embedding.v *)
Lemma embed_persistently P : ⎡<pers> P⎤ ⊣⊢ <pers> ⎡P⎤.
Proof. eapply bi_embed_mixin_persistently, bi_embed_mixin. Qed.
(* iris/bi/embedding.v *)
Instance embed_proper : Proper ((≡) ==> (≡)) embed.
Proof. apply (ne_proper _). Qed.
(* iris/bi/embedding.v *)
Instance embed_flip_mono : Proper (flip (⊢) ==> flip (⊢)) embed.
Proof. solve_proper. Qed.
(* iris/bi/embedding.v *)
Instance embed_entails_inj : Inj (⊢) (⊢) embed.
Proof.
    move=> P Q /bi.entails_wand. rewrite embed_wand_2.
    by move=> /embed_emp_valid_inj /bi.wand_entails.
  Qed.
(* iris/bi/embedding.v *)
Instance embed_inj : Inj (≡) (≡) embed.
Proof.
    intros P Q EQ. apply bi.equiv_entails, conj; apply (inj embed); rewrite EQ //.
  Qed.
(* iris/bi/embedding.v *)
Lemma embed_emp_valid (P : PROP1) : (⊢ ⎡P⎤) ↔ (⊢ P).
Proof.
    rewrite /bi_emp_valid. split=> HP.
    - by apply embed_emp_valid_inj.
    - by rewrite embed_emp_2 HP.
  Qed.
(* iris/bi/embedding.v *)
Lemma embed_emp `{!BiEmbedEmp PROP1 PROP2} : ⎡ emp ⎤ ⊣⊢ emp.
Proof. apply (anti_symm _); eauto using embed_emp_1, embed_emp_2. Qed.
(* iris/bi/embedding.v *)
Lemma embed_forall A (Φ : A → PROP1) : ⎡∀ x, Φ x⎤ ⊣⊢ ∀ x, ⎡Φ x⎤.
Proof.
    apply bi.equiv_entails; split; [|apply embed_forall_2].
    apply bi.forall_intro=>?. by rewrite bi.forall_elim.
  Qed.
(* iris/bi/embedding.v *)
Lemma embed_exist A (Φ : A → PROP1) : ⎡∃ x, Φ x⎤ ⊣⊢ ∃ x, ⎡Φ x⎤.
Proof.
    apply bi.equiv_entails; split; [apply embed_exist_1|].
    apply bi.exist_elim=>?. by rewrite -bi.exist_intro.
  Qed.
(* iris/bi/embedding.v *)
Lemma embed_and P Q : ⎡P ∧ Q⎤ ⊣⊢ ⎡P⎤ ∧ ⎡Q⎤.
Proof. rewrite !bi.and_alt embed_forall. by f_equiv=>-[]. Qed.
(* iris/bi/embedding.v *)
Lemma embed_or P Q : ⎡P ∨ Q⎤ ⊣⊢ ⎡P⎤ ∨ ⎡Q⎤.
Proof. rewrite !bi.or_alt embed_exist. by f_equiv=>-[]. Qed.
(* iris/bi/embedding.v *)
Lemma embed_impl P Q : ⎡P → Q⎤ ⊣⊢ (⎡P⎤ → ⎡Q⎤).
Proof.
    apply bi.equiv_entails; split; [|apply embed_impl_2].
    apply bi.impl_intro_l. by rewrite -embed_and bi.impl_elim_r.
  Qed.
(* iris/bi/embedding.v *)
Lemma embed_wand P Q : ⎡P -∗ Q⎤ ⊣⊢ (⎡P⎤ -∗ ⎡Q⎤).
Proof.
    apply bi.equiv_entails; split; [|apply embed_wand_2].
    apply bi.wand_intro_l. by rewrite -embed_sep bi.wand_elim_r.
  Qed.
(* iris/bi/embedding.v *)
Lemma embed_pure φ : ⎡⌜φ⌝⎤ ⊣⊢ ⌜φ⌝.
Proof.
    rewrite (@bi.pure_alt PROP1) (@bi.pure_alt PROP2) embed_exist.
    do 2 f_equiv. apply bi.equiv_entails. split; [apply bi.True_intro|].
    rewrite -(_ : (emp → emp : PROP1) ⊢ True) ?embed_impl;
      last apply bi.True_intro.
    apply bi.impl_intro_l. by rewrite right_id.
  Qed.
(* iris/bi/embedding.v *)
Lemma embed_iff P Q : ⎡P ↔ Q⎤ ⊣⊢ (⎡P⎤ ↔ ⎡Q⎤).
Proof. by rewrite embed_and !embed_impl. Qed.
(* iris/bi/embedding.v *)
Lemma embed_wand_iff P Q : ⎡P ∗-∗ Q⎤ ⊣⊢ (⎡P⎤ ∗-∗ ⎡Q⎤).
Proof. by rewrite embed_and !embed_wand. Qed.
(* iris/bi/embedding.v *)
Lemma embed_affinely_2 P : <affine> ⎡P⎤ ⊢ ⎡<affine> P⎤.
Proof. by rewrite embed_and -embed_emp_2. Qed.
(* iris/bi/embedding.v *)
Lemma embed_affinely `{!BiEmbedEmp PROP1 PROP2} P : ⎡<affine> P⎤ ⊣⊢ <affine> ⎡P⎤.
Proof. by rewrite /bi_intuitionistically embed_and embed_emp. Qed.
(* iris/bi/embedding.v *)
Lemma embed_absorbingly P : ⎡<absorb> P⎤ ⊣⊢ <absorb> ⎡P⎤.
Proof. by rewrite embed_sep embed_pure. Qed.
(* iris/bi/embedding.v *)
Lemma embed_intuitionistically_2 P : □ ⎡P⎤ ⊢ ⎡□ P⎤.
Proof. by rewrite /bi_intuitionistically -embed_affinely_2 embed_persistently. Qed.
(* iris/bi/embedding.v *)
Lemma embed_intuitionistically `{!BiEmbedEmp PROP1 PROP2} P : ⎡□ P⎤ ⊣⊢ □ ⎡P⎤.
Proof. by rewrite /bi_intuitionistically embed_affinely embed_persistently. Qed.
(* iris/bi/embedding.v *)
Lemma embed_persistently_if P b : ⎡<pers>?b P⎤ ⊣⊢ <pers>?b ⎡P⎤.
Proof. destruct b; simpl; auto using embed_persistently. Qed.
(* iris/bi/embedding.v *)
Lemma embed_affinely_if_2 P b : <affine>?b ⎡P⎤ ⊢ ⎡<affine>?b P⎤.
Proof. destruct b; simpl; auto using embed_affinely_2. Qed.
(* iris/bi/embedding.v *)
Lemma embed_affinely_if `{!BiEmbedEmp PROP1 PROP2} P b :
    ⎡<affine>?b P⎤ ⊣⊢ <affine>?b ⎡P⎤.
Proof. destruct b; simpl; auto using embed_affinely. Qed.
(* iris/bi/embedding.v *)
Lemma embed_absorbingly_if b P : ⎡<absorb>?b P⎤ ⊣⊢ <absorb>?b ⎡P⎤.
Proof. destruct b; simpl; auto using embed_absorbingly. Qed.
(* iris/bi/embedding.v *)
Lemma embed_intuitionistically_if_2 P b : □?b ⎡P⎤ ⊢ ⎡□?b P⎤.
Proof. destruct b; simpl; auto using embed_intuitionistically_2. Qed.
(* iris/bi/embedding.v *)
Lemma embed_intuitionistically_if `{!BiEmbedEmp PROP1 PROP2} P b :
    ⎡□?b P⎤ ⊣⊢ □?b ⎡P⎤.
Proof. destruct b; simpl; auto using embed_intuitionistically. Qed.
(* iris/bi/embedding.v *)
Instance embed_persistent P : Persistent P → Persistent ⎡P⎤.
Proof. intros ?. by rewrite /Persistent -embed_persistently -persistent. Qed.
(* iris/bi/embedding.v *)
Instance embed_affine `{!BiEmbedEmp PROP1 PROP2} P : Affine P → Affine ⎡P⎤.
Proof. intros ?. by rewrite /Affine (affine P) embed_emp. Qed.
(* iris/bi/embedding.v *)
Instance embed_absorbing P : Absorbing P → Absorbing ⎡P⎤.
Proof. intros ?. by rewrite /Absorbing -embed_absorbingly absorbing. Qed.
(* iris/bi/embedding.v *)
Instance embed_and_homomorphism :
    MonoidHomomorphism bi_and bi_and (≡) embed.
Proof.
    by split; [split|]; try apply _;
      [setoid_rewrite embed_and|rewrite embed_pure].
  Qed.
(* iris/bi/embedding.v *)
Instance embed_or_homomorphism :
    MonoidHomomorphism bi_or bi_or (≡) embed.
Proof.
    by split; [split|]; try apply _;
      [setoid_rewrite embed_or|rewrite embed_pure].
  Qed.
(* iris/bi/embedding.v *)
Instance embed_sep_entails_homomorphism :
    MonoidHomomorphism bi_sep bi_sep (flip (⊢)) embed.
Proof.
    split; [split|]; simpl; try apply _;
      [by setoid_rewrite embed_sep|by rewrite embed_emp_2].
  Qed.
(* iris/bi/embedding.v *)
Lemma embed_big_sepL_2 {A} (Φ : nat → A → PROP1) l :
    ([∗ list] k↦x ∈ l, ⎡Φ k x⎤) ⊢ ⎡[∗ list] k↦x ∈ l, Φ k x⎤.
Proof. apply (big_opL_commute (R:=flip (⊢)) _). Qed.
(* iris/bi/embedding.v *)
Lemma embed_big_sepM_2 `{Countable K} {A} (Φ : K → A → PROP1) (m : gmap K A) :
    ([∗ map] k↦x ∈ m, ⎡Φ k x⎤) ⊢ ⎡[∗ map] k↦x ∈ m, Φ k x⎤.
Proof. apply (big_opM_commute (R:=flip (⊢)) _). Qed.
(* iris/bi/embedding.v *)
Lemma embed_big_sepS_2 `{Countable A} (Φ : A → PROP1) (X : gset A) :
    ([∗ set] y ∈ X, ⎡Φ y⎤) ⊢ ⎡[∗ set] y ∈ X, Φ y⎤.
Proof. apply (big_opS_commute (R:=flip (⊢)) _). Qed.
(* iris/bi/embedding.v *)
Lemma embed_big_sepMS_2 `{Countable A} (Φ : A → PROP1) (X : gmultiset A) :
    ([∗ mset] y ∈ X, ⎡Φ y⎤) ⊢ ⎡[∗ mset] y ∈ X, Φ y⎤.
Proof. apply (big_opMS_commute (R:=flip (⊢)) _). Qed.
(* iris/bi/embedding.v *)
Instance embed_sep_homomorphism :
      MonoidHomomorphism bi_sep bi_sep (≡) embed.
Proof.
      by split; [split|]; try apply _;
        [setoid_rewrite embed_sep|rewrite embed_emp].
    Qed.
(* iris/bi/embedding.v *)
Lemma embed_big_sepL {A} (Φ : nat → A → PROP1) l :
      ⎡[∗ list] k↦x ∈ l, Φ k x⎤ ⊣⊢ [∗ list] k↦x ∈ l, ⎡Φ k x⎤.
Proof. apply (big_opL_commute _). Qed.
(* iris/bi/embedding.v *)
Lemma embed_big_sepM `{Countable K} {A} (Φ : K → A → PROP1) (m : gmap K A) :
      ⎡[∗ map] k↦x ∈ m, Φ k x⎤ ⊣⊢ [∗ map] k↦x ∈ m, ⎡Φ k x⎤.
Proof. apply (big_opM_commute _). Qed.
(* iris/bi/embedding.v *)
Lemma embed_big_sepS `{Countable A} (Φ : A → PROP1) (X : gset A) :
      ⎡[∗ set] y ∈ X, Φ y⎤ ⊣⊢ [∗ set] y ∈ X, ⎡Φ y⎤.
Proof. apply (big_opS_commute _). Qed.
(* iris/bi/embedding.v *)
Lemma embed_big_sepMS `{Countable A} (Φ : A → PROP1) (X : gmultiset A) :
      ⎡[∗ mset] y ∈ X, Φ y⎤ ⊣⊢ [∗ mset] y ∈ X, ⎡Φ y⎤.
Proof. apply (big_opMS_commute _). Qed.
(* iris/bi/embedding.v *)
Lemma embed_laterN n P : ⎡▷^n P⎤ ⊣⊢ ▷^n ⎡P⎤.
Proof. induction n=>//=. rewrite embed_later. by f_equiv. Qed.
(* iris/bi/embedding.v *)
Lemma embed_except_0 P : ⎡◇ P⎤ ⊣⊢ ◇ ⎡P⎤.
Proof. by rewrite embed_or embed_later embed_pure. Qed.
(* iris/bi/embedding.v *)
Instance embed_timeless P : Timeless P → Timeless ⎡P⎤.
Proof.
      intros ?. by rewrite /Timeless -embed_except_0 -embed_later timeless.
    Qed.
(* iris/bi/embedding.v *)
Lemma embed_si_pure Pi : ⎡<si_pure> Pi⎤ ⊣⊢ <si_pure> Pi.
Proof.
      apply (anti_symm _); [apply embed_si_pure_1|].
      rewrite -(si_pure_si_emp_valid_elim ⎡ _ ⎤).
      by rewrite embed_si_emp_valid si_emp_valid_si_pure.
    Qed.
(* iris/bi/embedding.v *)
Lemma embed_internal_inj `{!Sbi PROP3} P Q : ⎡P⎤ ≡ ⎡Q⎤ ⊢@{PROP3} P ≡ Q.
Proof.
      intros. rewrite -(si_pure_internal_eq ⎡ _ ⎤%I) -(si_pure_internal_eq P).
      f_equiv. rewrite !prop_ext_si_emp_valid.
      rewrite /bi_wand_iff !si_emp_valid_and.
      by rewrite -!embed_wand !embed_si_emp_valid.
    Qed.
(* iris/bi/embedding.v *)
Lemma embed_internal_eq (A : ofe) (x y : A) : ⎡x ≡ y⎤ ⊣⊢@{PROP2} x ≡ y.
Proof. apply embed_si_pure. Qed.
(* iris/bi/embedding.v *)
Lemma embed_plainly P : ⎡■ P⎤ ⊣⊢ ■ ⎡P⎤.
Proof. by rewrite /plainly embed_si_pure embed_si_emp_valid. Qed.
(* iris/bi/embedding.v *)
Lemma embed_plainly_if p P : ⎡■?p P⎤ ⊣⊢ ■?p ⎡P⎤.
Proof. destruct p; simpl; auto using embed_plainly. Qed.
(* iris/bi/embedding.v *)
Lemma embed_plain (P : PROP1) : Plain P → Plain (PROP:=PROP2) ⎡P⎤.
Proof. intros ?. by rewrite /Plain {1}(plain P) embed_plainly. Qed.
(* iris/bi/embedding.v *)
Instance embed_embed : Embed PROP1 PROP3
:= λ P, ⎡ ⎡ P ⎤ ⎤%I.
(* iris/bi/embedding.v *)
Lemma embed_embedding_mixin : BiEmbedMixin PROP1 PROP3 embed_embed.
Proof.
    split; unfold embed, embed_embed.
    - solve_proper.
    - solve_proper.
    - intros P. by rewrite !embed_emp_valid.
    - by rewrite -!embed_emp_2.
    - intros P Q. by rewrite -!embed_impl.
    - intros A Φ. by rewrite -!embed_forall.
    - intros A Φ. by rewrite -!embed_exist.
    - intros P Q. by rewrite -!embed_sep.
    - intros P Q. by rewrite -!embed_wand.
    - intros P. by rewrite -!embed_persistently.
  Qed.
(* iris/bi/embedding.v *)
Instance embed_bi_embed : BiEmbed PROP1 PROP3
:=
    {| bi_embed_mixin := embed_embedding_mixin |}.
(* iris/bi/embedding.v *)
Lemma embed_embed_alt (P : PROP1) : ⎡ P ⎤ ⊣⊢@{PROP3} ⎡ ⎡ P ⎤ ⎤.
Proof. done. Qed.
(* iris/bi/embedding.v *)
Lemma embed_embed_emp :
    BiEmbedEmp PROP1 PROP2 → BiEmbedEmp PROP2 PROP3 →
    BiEmbedEmp PROP1 PROP3.
Proof. rewrite /BiEmbedEmp !embed_embed_alt. by intros -> ->. Qed.
(* iris/bi/embedding.v *)
Lemma embed_embed_later :
    BiEmbedLater PROP1 PROP2 → BiEmbedLater PROP2 PROP3 →
    BiEmbedLater PROP1 PROP3.
Proof. intros ?? P. by rewrite !embed_embed_alt !embed_later. Qed.
(* iris/bi/embedding.v *)
Lemma embed_embed_sbi `{!Sbi PROP1, !Sbi PROP2, !Sbi PROP3} :
    BiEmbedSbi PROP1 PROP2 → BiEmbedSbi PROP2 PROP3 →
    BiEmbedSbi PROP1 PROP3.
Proof.
    intros ??; split.
    - intros P. by rewrite embed_embed_alt !embed_si_emp_valid.
    - intros Pi. by rewrite embed_embed_alt !embed_si_pure.
  Qed.
(* iris/bi/embedding.v *)
Lemma embed_embed_bupd `{!BiBUpd PROP1, !BiBUpd PROP2, !BiBUpd PROP3} :
    BiEmbedBUpd PROP1 PROP2 → BiEmbedBUpd PROP2 PROP3 →
    BiEmbedBUpd PROP1 PROP3.
Proof. intros ?? P. by rewrite !embed_embed_alt !embed_bupd. Qed.
(* iris/bi/embedding.v *)
Lemma embed_embed_fupd `{!BiFUpd PROP1, !BiFUpd PROP2, !BiFUpd PROP3} :
    BiEmbedFUpd PROP1 PROP2 → BiEmbedFUpd PROP2 PROP3 →
    BiEmbedFUpd PROP1 PROP3.
Proof. intros ?? E1 E2 P. by rewrite !embed_embed_alt !embed_fupd. Qed.
(* iris/bi/extensions.v *)
Class BiAffine (PROP : bi)
:= absorbing_bi (Q : PROP) : Affine Q.