phanerozoic/Coq-Iris huggingface dataset:
(* iris/bi/monpred.v *)
Lemma monPred_objectively_mono P Q : (P ⊢ Q) → (<obj> P ⊢ <obj> Q).
Proof. rewrite monPred_objectively_unfold. solve_proper. Qed.
(* iris/bi/monpred.v *)
Instance monPred_objectively_mono' :
    Proper ((⊢) ==> (⊢)) (@monPred_objectively I PROP).
Proof. intros ???. by apply monPred_objectively_mono. Qed.
(* iris/bi/monpred.v *)
Instance monPred_objectively_flip_mono' :
    Proper (flip (⊢) ==> flip (⊢)) (@monPred_objectively I PROP).
Proof. intros ???. by apply monPred_objectively_mono. Qed.
(* iris/bi/monpred.v *)
Instance monPred_objectively_persistent `{!BiPersistentlyForall PROP} P :
    Persistent P → Persistent (<obj> P).
Proof. rewrite monPred_objectively_unfold. apply _. Qed.
(* iris/bi/monpred.v *)
Instance monPred_objectively_absorbing P : Absorbing P → Absorbing (<obj> P).
Proof. rewrite monPred_objectively_unfold. apply _. Qed.
(* iris/bi/monpred.v *)
Instance monPred_objectively_affine P : Affine P → Affine (<obj> P).
Proof. rewrite monPred_objectively_unfold. apply _. Qed.
(* iris/bi/monpred.v *)
Instance monPred_subjectively_ne : NonExpansive (@monPred_subjectively I PROP).
Proof. rewrite monPred_subjectively_unfold. solve_proper. Qed.
(* iris/bi/monpred.v *)
Instance monPred_subjectively_proper :
    Proper ((≡) ==> (≡)) (@monPred_subjectively I PROP).
Proof. apply (ne_proper _). Qed.
(* iris/bi/monpred.v *)
Lemma monPred_subjectively_mono P Q : (P ⊢ Q) → <subj> P ⊢ <subj> Q.
Proof. rewrite monPred_subjectively_unfold. solve_proper. Qed.
(* iris/bi/monpred.v *)
Instance monPred_subjectively_mono' :
    Proper ((⊢) ==> (⊢)) (@monPred_subjectively I PROP).
Proof. intros ???. by apply monPred_subjectively_mono. Qed.
(* iris/bi/monpred.v *)
Instance monPred_subjectively_flip_mono' :
    Proper (flip (⊢) ==> flip (⊢)) (@monPred_subjectively I PROP).
Proof. intros ???. by apply monPred_subjectively_mono. Qed.
(* iris/bi/monpred.v *)
Instance monPred_subjectively_persistent P :
    Persistent P → Persistent (<subj> P).
Proof. rewrite monPred_subjectively_unfold. apply _. Qed.
(* iris/bi/monpred.v *)
Instance monPred_subjectively_absorbing P :
    Absorbing P → Absorbing (<subj> P).
Proof. rewrite monPred_subjectively_unfold. apply _. Qed.
(* iris/bi/monpred.v *)
Instance monPred_subjectively_affine P : Affine P → Affine (<subj> P).
Proof. rewrite monPred_subjectively_unfold. apply _. Qed.
(* iris/bi/monpred.v *)
(* Laws for monPred_objectively and of Objective. *)
Lemma monPred_objectively_elim P : <obj> P ⊢ P.
Proof. rewrite monPred_objectively_unfold. unseal. split=>?. apply bi.forall_elim. Qed.
(* iris/bi/monpred.v *)
Lemma monPred_objectively_idemp P : <obj> <obj> P ⊣⊢ <obj> P.
Proof.
    apply bi.equiv_entails; split; [by apply monPred_objectively_elim|].
    unseal. split=>i /=. by apply bi.forall_intro=>_.
  Qed.
(* iris/bi/monpred.v *)
Lemma monPred_objectively_forall {A} (Φ : A → monPred) :
    <obj> (∀ x, Φ x) ⊣⊢ ∀ x, <obj> (Φ x).
Proof.
    unseal. split=>i. apply bi.equiv_entails; split=>/=;
      do 2 apply bi.forall_intro=>?; by do 2 rewrite bi.forall_elim.
  Qed.
(* iris/bi/monpred.v *)
Lemma monPred_objectively_and P Q : <obj> (P ∧ Q) ⊣⊢ <obj> P ∧ <obj> Q.
Proof.
    unseal. split=>i. apply bi.equiv_entails; split=>/=.
    - apply bi.and_intro; do 2 f_equiv.
      + apply bi.and_elim_l.
      + apply bi.and_elim_r.
    - apply bi.forall_intro=>?. by rewrite !bi.forall_elim.
  Qed.
(* iris/bi/monpred.v *)
Lemma monPred_objectively_exist {A} (Φ : A → monPred) :
    (∃ x, <obj> (Φ x)) ⊢ <obj> (∃ x, (Φ x)).
Proof. apply bi.exist_elim=>?. f_equiv. apply bi.exist_intro. Qed.
(* iris/bi/monpred.v *)
Lemma monPred_objectively_or P Q : <obj> P ∨ <obj> Q ⊢ <obj> (P ∨ Q).
Proof.
    apply bi.or_elim; f_equiv.
    - apply bi.or_intro_l.
    - apply bi.or_intro_r.
  Qed.
(* iris/bi/monpred.v *)
Lemma monPred_objectively_sep_2 P Q : <obj> P ∗ <obj> Q ⊢ <obj> (P ∗ Q).
Proof.
    unseal. split=>i /=. apply bi.forall_intro=>?. by rewrite !bi.forall_elim.
  Qed.
(* iris/bi/monpred.v *)
Lemma monPred_objectively_sep `{BiIndexBottom bot} P Q :
    <obj> (P ∗ Q) ⊣⊢ <obj> P ∗ <obj> Q.
Proof.
    apply bi.equiv_entails, conj, monPred_objectively_sep_2. unseal. split=>i /=.
    rewrite (bi.forall_elim bot). by f_equiv; apply bi.forall_intro=>j; f_equiv.
  Qed.
(* iris/bi/monpred.v *)
Lemma monPred_objectively_embed (P : PROP) : <obj> ⎡P⎤ ⊣⊢@{monPredI} ⎡P⎤.
Proof.
    apply bi.equiv_entails; split; unseal; split=>i /=.
    - by rewrite (bi.forall_elim inhabitant).
    - by apply bi.forall_intro.
  Qed.
(* iris/bi/monpred.v *)
Lemma monPred_objectively_emp : <obj> (emp : monPred) ⊣⊢ emp.
Proof. rewrite monPred_emp_unfold. apply monPred_objectively_embed. Qed.
(* iris/bi/monpred.v *)
Lemma monPred_objectively_pure φ : <obj> (⌜ φ ⌝ : monPred) ⊣⊢ ⌜ φ ⌝.
Proof. rewrite monPred_pure_unfold. apply monPred_objectively_embed. Qed.
(* iris/bi/monpred.v *)
Lemma monPred_subjectively_intro P : P ⊢ <subj> P.
Proof. unseal. split=>?. apply bi.exist_intro. Qed.
(* iris/bi/monpred.v *)
Lemma monPred_subjectively_forall {A} (Φ : A → monPred) :
    (<subj> (∀ x, Φ x)) ⊢ ∀ x, <subj> (Φ x).
Proof. apply bi.forall_intro=>?. f_equiv. apply bi.forall_elim. Qed.
(* iris/bi/monpred.v *)
Lemma monPred_subjectively_and P Q : <subj> (P ∧ Q) ⊢ <subj> P ∧ <subj> Q.
Proof.
    apply bi.and_intro; f_equiv.
    - apply bi.and_elim_l.
    - apply bi.and_elim_r.
  Qed.
(* iris/bi/monpred.v *)
Lemma monPred_subjectively_exist {A} (Φ : A → monPred) :
    <subj> (∃ x, Φ x) ⊣⊢ ∃ x, <subj> (Φ x).
Proof.
    unseal. split=>i. apply bi.equiv_entails; split=>/=;
      do 2 apply bi.exist_elim=>?; by do 2 rewrite -bi.exist_intro.
  Qed.
(* iris/bi/monpred.v *)
Lemma monPred_subjectively_or P Q : <subj> (P ∨ Q) ⊣⊢ <subj> P ∨ <subj> Q.
Proof. split=>i. unseal. apply bi.or_exist. Qed.
(* iris/bi/monpred.v *)
Lemma monPred_subjectively_sep P Q : <subj> (P ∗ Q) ⊢ <subj> P ∗ <subj> Q.
Proof.
    unseal. split=>i /=. apply bi.exist_elim=>?. by rewrite -!bi.exist_intro.
  Qed.
(* iris/bi/monpred.v *)
Lemma monPred_subjectively_idemp P : <subj> <subj> P ⊣⊢ <subj> P.
Proof.
    apply bi.equiv_entails; split; [|by apply monPred_subjectively_intro].
    unseal. split=>i /=. by apply bi.exist_elim=>_.
  Qed.
(* iris/bi/monpred.v *)
Lemma objective_objectively P `{!Objective P} : P ⊢ <obj> P.
Proof.
    rewrite monPred_objectively_unfold /= embed_forall. apply bi.forall_intro=>?.
    split=>?. unseal. apply objective_at, _.
  Qed.
(* iris/bi/monpred.v *)
Lemma objective_subjectively P `{!Objective P} : <subj> P ⊢ P.
Proof.
    rewrite monPred_subjectively_unfold /= embed_exist. apply bi.exist_elim=>?.
    split=>?. unseal. apply objective_at, _.
  Qed.
(* iris/bi/monpred.v *)
Instance embed_objective (P : PROP) : @Objective I PROP ⎡P⎤.
Proof. intros ??. by unseal. Qed.
(* iris/bi/monpred.v *)
Instance pure_objective φ : @Objective I PROP ⌜φ⌝.
Proof. intros ??. by unseal. Qed.
(* iris/bi/monpred.v *)
Instance emp_objective : @Objective I PROP emp.
Proof. intros ??. by unseal. Qed.
(* iris/bi/monpred.v *)
Instance objectively_objective P : Objective (<obj> P).
Proof. intros ??. by unseal. Qed.
(* iris/bi/monpred.v *)
Instance subjectively_objective P : Objective (<subj> P).
Proof. intros ??. by unseal. Qed.
(* iris/bi/monpred.v *)
Instance and_objective P Q `{!Objective P, !Objective Q} :
    Objective (P ∧ Q).
Proof. intros i j. unseal. by rewrite !(objective_at _ i j). Qed.
(* iris/bi/monpred.v *)
Instance or_objective P Q `{!Objective P, !Objective Q} :
    Objective (P ∨ Q).
Proof. intros i j. by rewrite !monPred_at_or !(objective_at _ i j). Qed.
(* iris/bi/monpred.v *)
Instance impl_objective P Q `{!Objective P, !Objective Q} :
    Objective (P → Q).
Proof.
    intros i j. unseal. rewrite (bi.forall_elim i) bi.pure_impl_forall.
    rewrite bi.forall_elim //. apply bi.forall_intro=> k.
    rewrite bi.pure_impl_forall. apply bi.forall_intro=>_.
    rewrite (objective_at Q i). by rewrite (objective_at P k).
  Qed.
(* iris/bi/monpred.v *)
Instance forall_objective {A} Φ {H : ∀ x : A, Objective (Φ x)} :
    @Objective I PROP (∀ x, Φ x)%I.
Proof. intros i j. unseal. do 2 f_equiv. by apply objective_at. Qed.
(* iris/bi/monpred.v *)
Instance exists_objective {A} Φ {H : ∀ x : A, Objective (Φ x)} :
    @Objective I PROP (∃ x, Φ x)%I.
Proof. intros i j. unseal. do 2 f_equiv. by apply objective_at. Qed.
(* iris/bi/monpred.v *)
Instance sep_objective P Q `{!Objective P, !Objective Q} :
    Objective (P ∗ Q).
Proof. intros i j. unseal. by rewrite !(objective_at _ i j). Qed.
(* iris/bi/monpred.v *)
Instance wand_objective P Q `{!Objective P, !Objective Q} :
    Objective (P -∗ Q).
Proof.
    intros i j. unseal. rewrite (bi.forall_elim i) bi.pure_impl_forall.
    rewrite bi.forall_elim //. apply bi.forall_intro=> k.
    rewrite bi.pure_impl_forall. apply bi.forall_intro=>_.
    rewrite (objective_at Q i). by rewrite (objective_at P k).
  Qed.
(* iris/bi/monpred.v *)
Instance persistently_objective P `{!Objective P} : Objective (<pers> P).
Proof. intros i j. unseal. by rewrite objective_at. Qed.
(* iris/bi/monpred.v *)
Instance affinely_objective P `{!Objective P} : Objective (<affine> P).
Proof. rewrite /bi_affinely. apply _. Qed.
(* iris/bi/monpred.v *)
Instance intuitionistically_objective P `{!Objective P} : Objective (□ P).
Proof. rewrite /bi_intuitionistically. apply _. Qed.
(* iris/bi/monpred.v *)
Instance absorbingly_objective P `{!Objective P} : Objective (<absorb> P).
Proof. rewrite /bi_absorbingly. apply _. Qed.
(* iris/bi/monpred.v *)
Instance persistently_if_objective P p `{!Objective P} :
    Objective (<pers>?p P).
Proof. rewrite /bi_persistently_if. destruct p; apply _. Qed.
(* iris/bi/monpred.v *)
Instance affinely_if_objective P p `{!Objective P} :
    Objective (<affine>?p P).
Proof. rewrite /bi_affinely_if. destruct p; apply _. Qed.
(* iris/bi/monpred.v *)
Instance absorbingly_if_objective P p `{!Objective P} :
    Objective (<absorb>?p P).
Proof. rewrite /bi_absorbingly_if. destruct p; apply _. Qed.
(* iris/bi/monpred.v *)
Instance intuitionistically_if_objective P p `{!Objective P} :
    Objective (□?p P).
Proof. rewrite /bi_intuitionistically_if. destruct p; apply _. Qed.
(* iris/bi/monpred.v *)
(* monPred_in *)
Lemma monPred_in_intro P : P ⊢ ∃ i, monPred_in i ∧ ⎡P i⎤.
Proof.
    unseal. split=>i /=.
    rewrite /= -(bi.exist_intro i). apply bi.and_intro=>//. by apply bi.pure_intro.
  Qed.
(* iris/bi/monpred.v *)
Lemma monPred_in_elim P i : monPred_in i ⊢ ⎡P i⎤ → P .
Proof.
    apply bi.impl_intro_r. unseal. split=>i' /=.
    eapply bi.pure_elim; [apply bi.and_elim_l|]=>?. rewrite bi.and_elim_r. by f_equiv.
  Qed.
(* iris/bi/monpred.v *)
(* Big op *)
Instance monPred_at_monoid_and_homomorphism i :
    MonoidHomomorphism bi_and bi_and (≡) (flip monPred_at i).
Proof.
    split; [split|]; try apply _; [apply monPred_at_and | apply monPred_at_pure].
  Qed.
(* iris/bi/monpred.v *)
Instance monPred_at_monoid_or_homomorphism i :
    MonoidHomomorphism bi_or bi_or (≡) (flip monPred_at i).
Proof.
    split; [split|]; try apply _; [apply monPred_at_or | apply monPred_at_pure].
  Qed.
(* iris/bi/monpred.v *)
Instance monPred_at_monoid_sep_homomorphism i :
    MonoidHomomorphism bi_sep bi_sep (≡) (flip monPred_at i).
Proof.
    split; [split|]; try apply _; [apply monPred_at_sep | apply monPred_at_emp].
  Qed.
(* iris/bi/monpred.v *)
Lemma monPred_at_big_sepL {A} i (Φ : nat → A → monPred) l :
    ([∗ list] k↦x ∈ l, Φ k x) i ⊣⊢ [∗ list] k↦x ∈ l, Φ k x i.
Proof. apply (big_opL_commute (flip monPred_at i)). Qed.
(* iris/bi/monpred.v *)
Lemma monPred_at_big_sepM `{Countable K} {A} i (Φ : K → A → monPred) (m : gmap K A) :
    ([∗ map] k↦x ∈ m, Φ k x) i ⊣⊢ [∗ map] k↦x ∈ m, Φ k x i.
Proof. apply (big_opM_commute (flip monPred_at i)). Qed.
(* iris/bi/monpred.v *)
Lemma monPred_at_big_sepS `{Countable A} i (Φ : A → monPred) (X : gset A) :
    ([∗ set] y ∈ X, Φ y) i ⊣⊢ [∗ set] y ∈ X, Φ y i.
Proof. apply (big_opS_commute (flip monPred_at i)). Qed.
(* iris/bi/monpred.v *)
Lemma monPred_at_big_sepMS `{Countable A} i (Φ : A → monPred) (X : gmultiset A) :
    ([∗ mset] y ∈ X, Φ y) i ⊣⊢ ([∗ mset] y ∈ X, Φ y i).
Proof. apply (big_opMS_commute (flip monPred_at i)). Qed.
(* iris/bi/monpred.v *)
Instance monPred_objectively_monoid_and_homomorphism :
    MonoidHomomorphism bi_and bi_and (≡) (@monPred_objectively I PROP).
Proof.
    split; [split|]; try apply _.
    - apply monPred_objectively_and.
    - apply monPred_objectively_pure.
  Qed.
(* iris/bi/monpred.v *)
Instance monPred_objectively_monoid_sep_entails_homomorphism :
    MonoidHomomorphism bi_sep bi_sep (flip (⊢)) (@monPred_objectively I PROP).
Proof.
    split; [split|]; try apply _.
    - apply monPred_objectively_sep_2.
    - by rewrite monPred_objectively_emp.
  Qed.
(* iris/bi/monpred.v *)
Instance monPred_objectively_monoid_sep_homomorphism `{BiIndexBottom bot} :
    MonoidHomomorphism bi_sep bi_sep (≡) (@monPred_objectively I PROP).
Proof.
    split; [split|]; try apply _.
    - apply monPred_objectively_sep.
    - by rewrite monPred_objectively_emp.
  Qed.
(* iris/bi/monpred.v *)
Lemma monPred_objectively_big_sepL_entails {A} (Φ : nat → A → monPred) l :
    ([∗ list] k↦x ∈ l, <obj> (Φ k x)) ⊢ <obj> ([∗ list] k↦x ∈ l, Φ k x).
Proof. apply (big_opL_commute monPred_objectively (R:=flip (⊢))). Qed.
(* iris/bi/monpred.v *)
Lemma monPred_objectively_big_sepM_entails
        `{Countable K} {A} (Φ : K → A → monPred) (m : gmap K A) :
    ([∗ map] k↦x ∈ m, <obj> (Φ k x)) ⊢ <obj> ([∗ map] k↦x ∈ m, Φ k x).
Proof. apply (big_opM_commute monPred_objectively (R:=flip (⊢))). Qed.
(* iris/bi/monpred.v *)
Lemma monPred_objectively_big_sepS_entails `{Countable A}
      (Φ : A → monPred) (X : gset A) :
    ([∗ set] y ∈ X, <obj> (Φ y)) ⊢ <obj> ([∗ set] y ∈ X, Φ y).
Proof. apply (big_opS_commute monPred_objectively (R:=flip (⊢))). Qed.
(* iris/bi/monpred.v *)
Lemma monPred_objectively_big_sepMS_entails `{Countable A}
      (Φ : A → monPred) (X : gmultiset A) :
    ([∗ mset] y ∈ X, <obj> (Φ y)) ⊢ <obj> ([∗ mset] y ∈ X, Φ y).
Proof. apply (big_opMS_commute monPred_objectively (R:=flip (⊢))). Qed.
(* iris/bi/monpred.v *)
Lemma monPred_objectively_big_sepL `{BiIndexBottom bot} {A}
      (Φ : nat → A → monPred) l :
    <obj> ([∗ list] k↦x ∈ l, Φ k x) ⊣⊢ ([∗ list] k↦x ∈ l, <obj> (Φ k x)).
Proof. apply (big_opL_commute _). Qed.
(* iris/bi/monpred.v *)
Lemma monPred_objectively_big_sepM `{BiIndexBottom bot} `{Countable K} {A}
        (Φ : K → A → monPred) (m : gmap K A) :
    <obj> ([∗ map] k↦x ∈ m, Φ k x) ⊣⊢ ([∗ map] k↦x ∈ m, <obj> (Φ k x)).
Proof. apply (big_opM_commute _). Qed.
(* iris/bi/monpred.v *)
Lemma monPred_objectively_big_sepS `{BiIndexBottom bot} `{Countable A}
        (Φ : A → monPred) (X : gset A) :
    <obj> ([∗ set] y ∈ X, Φ y) ⊣⊢ ([∗ set] y ∈ X, <obj> (Φ y)).
Proof. apply (big_opS_commute _). Qed.
(* iris/bi/monpred.v *)
Lemma monPred_objectively_big_sepMS `{BiIndexBottom bot} `{Countable A}
        (Φ : A → monPred) (X : gmultiset A) :
    <obj> ([∗ mset] y ∈ X, Φ y) ⊣⊢  ([∗ mset] y ∈ X, <obj> (Φ y)).
Proof. apply (big_opMS_commute _). Qed.
(* iris/bi/monpred.v *)
Instance big_sepL_objective {A} (l : list A) Φ `{∀ n x, Objective (Φ n x)} :
    @Objective I PROP ([∗ list] n↦x ∈ l, Φ n x).
Proof. generalize dependent Φ. induction l=>/=; apply _. Qed.
(* iris/bi/monpred.v *)
Instance big_sepM_objective `{Countable K} {A}
         (Φ : K → A → monPred) (m : gmap K A) `{∀ k x, Objective (Φ k x)} :
    Objective ([∗ map] k↦x ∈ m, Φ k x).
Proof.
    intros ??. rewrite !monPred_at_big_sepM. do 3 f_equiv. by apply objective_at.
  Qed.
(* iris/bi/monpred.v *)
Instance big_sepS_objective `{Countable A} (Φ : A → monPred)
         (X : gset A) `{∀ y, Objective (Φ y)} :
    Objective ([∗ set] y ∈ X, Φ y).
Proof.
    intros ??. rewrite !monPred_at_big_sepS. do 2 f_equiv. by apply objective_at.
  Qed.
(* iris/bi/monpred.v *)
Instance big_sepMS_objective `{Countable A} (Φ : A → monPred)
         (X : gmultiset A) `{∀ y, Objective (Φ y)} :
    Objective ([∗ mset] y ∈ X, Φ y).
Proof.
    intros ??. rewrite !monPred_at_big_sepMS. do 2 f_equiv. by apply objective_at.
  Qed.
(* iris/bi/monpred.v *)
(* BUpd *)
Lemma monPred_at_bupd `{!BiBUpd PROP} i P : (|==> P) i ⊣⊢ |==> P i.
Proof. by rewrite monPred_bupd_unseal. Qed.
(* iris/bi/monpred.v *)
Instance bupd_objective `{!BiBUpd PROP} P `{!Objective P} :
    Objective (|==> P).
Proof. intros ??. by rewrite !monPred_at_bupd objective_at. Qed.
(* iris/bi/monpred.v *)
(* Later *)
Instance monPred_at_timeless P i : Timeless P → Timeless (P i).
Proof. move => [] /(_ i). rewrite /Timeless /bi_except_0. by unseal. Qed.
(* iris/bi/monpred.v *)
Instance monPred_in_timeless i0 : Timeless (@monPred_in I PROP i0).
Proof. split => ? /=. rewrite /bi_except_0. unseal. apply timeless, _. Qed.
(* iris/bi/monpred.v *)
Instance monPred_objectively_timeless P : Timeless P → Timeless (<obj> P).
Proof.
    move=>[]. rewrite /Timeless /bi_except_0. unseal=>Hti. split=> ? /=.
    by apply timeless, bi.forall_timeless.
  Qed.
(* iris/bi/monpred.v *)
Instance monPred_subjectively_timeless P : Timeless P → Timeless (<subj> P).
Proof.
    move=>[]. rewrite /Timeless /bi_except_0. unseal=>Hti. split=> ? /=.
    by apply timeless, bi.exist_timeless.
  Qed.
(* iris/bi/monpred.v *)
Lemma monPred_at_later i P : (▷ P) i ⊣⊢ ▷ P i.
Proof. by unseal. Qed.
(* iris/bi/monpred.v *)
Lemma monPred_at_laterN n i P : (▷^n P) i ⊣⊢ ▷^n P i.
Proof. induction n as [|? IHn]; first done. rewrite /= monPred_at_later IHn //. Qed.
(* iris/bi/monpred.v *)
Lemma monPred_at_except_0 i P : (◇ P) i ⊣⊢ ◇ P i.
Proof. rewrite /bi_except_0. by unseal. Qed.
(* iris/bi/monpred.v *)
Instance later_objective P `{!Objective P} : Objective (▷ P).
Proof. intros ??. unseal. by rewrite objective_at. Qed.
(* iris/bi/monpred.v *)
Instance laterN_objective P `{!Objective P} n : Objective (▷^n P).
Proof. induction n; apply _. Qed.
(* iris/bi/monpred.v *)
Instance except0_objective P `{!Objective P} : Objective (◇ P).
Proof. rewrite /bi_except_0. apply _. Qed.
(* iris/bi/monpred.v *)
Lemma monPred_si_pure_unfold :
      @si_pure monPredI _ = λ Pi, ⎡ <si_pure> Pi ⎤%I.
Proof. by unseal. Qed.
(* iris/bi/monpred.v *)
Lemma monPred_si_emp_valid_unfold :
      @si_emp_valid monPredI _ = λ P, (<si_emp_valid> ∀ i, P i)%I.
Proof. by unseal. Qed.
(* iris/bi/monpred.v *)
Instance si_pure_objective Pi :
      Objective (PROP:=PROP) (I:=I) (<si_pure> Pi).
Proof. rewrite monPred_si_pure_unfold. apply _. Qed.
(* iris/bi/monpred.v *)
(* Internal equality *)
Lemma monPred_internal_eq_unfold :
      @internal_eq monPredI _ = λ A x y, ⎡ x ≡ y ⎤%I.
Proof. by rewrite /internal_eq monPred_si_pure_unfold. Qed.
(* iris/bi/monpred.v *)
Lemma monPred_at_internal_eq {A : ofe} i (a b : A) :
      @monPred_at (a ≡ b) i ⊣⊢ a ≡ b.
Proof. rewrite monPred_internal_eq_unfold. by apply monPred_at_embed. Qed.
(* iris/bi/monpred.v *)
Lemma monPred_equivI `{!Sbi PROP'} P Q :
      P ≡ Q ⊣⊢@{PROP'} ∀ i, P i ≡ Q i.
Proof.
      apply bi.equiv_entails. split.
      - apply bi.forall_intro=> ?. apply (f_equivI (flip monPred_at _)).
      - by rewrite -{2}(sig_monPred_sig P) -{2}(sig_monPred_sig Q)
                   -f_equivI -sig_equivI !discrete_fun_equivI.
    Qed.
(* iris/bi/monpred.v *)
Instance internal_eq_objective {A : ofe} (x y : A) :
      @Objective I PROP (x ≡ y).
Proof. intros ??. rewrite monPred_internal_eq_unfold. by unseal. Qed.
(* iris/bi/monpred.v *)
(* FUpd *)
Lemma monPred_at_fupd `{!BiFUpd PROP} i E1 E2 P :
      (|={E1,E2}=> P) i ⊣⊢ |={E1,E2}=> P i.
Proof. by rewrite monPred_fupd_unseal. Qed.
(* iris/bi/monpred.v *)
Instance fupd_objective E1 E2 P `{!Objective P} `{!BiFUpd PROP} :
      Objective (|={E1,E2}=> P).
Proof. intros ??. by rewrite !monPred_at_fupd objective_at. Qed.
(* iris/bi/monpred.v *)
(* Plainly *)
Lemma monPred_at_plainly i P : (■ P) i ⊣⊢ ∀ j, ■ (P j).
Proof.
      rewrite /plainly !monPred_si_pure_unfold monPred_si_emp_valid_unfold.
      by rewrite monPred_at_embed -si_pure_forall -si_emp_valid_forall.
    Qed.
(* iris/bi/monpred.v *)
Instance monPred_at_plain P i : Plain P → Plain (P i).
Proof. move => [] /(_ i). rewrite /Plain monPred_at_plainly bi.forall_elim //. Qed.
(* iris/bi/monpred.v *)
Instance plainly_objective P : Objective (■ P).
Proof. rewrite /plainly. apply _. Qed.
(* iris/bi/monpred.v *)
Instance plainly_if_objective P p `{!Objective P} :
      Objective (■?p P).
Proof. rewrite /plainly_if. destruct p; apply _. Qed.
(* iris/bi/monpred.v *)
Instance monPred_objectively_plain P :
      Plain P → Plain (<obj> P).
Proof. rewrite monPred_objectively_unfold. apply _. Qed.
(* iris/bi/monpred.v *)
Instance monPred_subjectively_plain P :
      Plain P → Plain (<subj> P).
Proof. rewrite monPred_subjectively_unfold. apply _. Qed.
(* iris/bi/plainly.v *)
Definition plainly `{!Sbi PROP} (P : PROP) : PROP
:=
  <si_pure> <si_emp_valid> P.
(* iris/bi/plainly.v *)
Instance : Params (@plainly) 2
:= {}.
(* iris/bi/plainly.v *)
Notation "■ P"
:= (plainly P) : bi_scope.
(* iris/bi/plainly.v *)
Class Plain `{!Sbi PROP} (P : PROP)
:= plain : P ⊢ ■ P.
(* iris/bi/plainly.v *)
Instance : Params (@Plain) 1
:= {}.
(* iris/bi/plainly.v *)
Instance siProp_plain (P : siProp) : Plain P | 0.
Proof. done. Qed.
(* iris/bi/plainly.v *)
Definition plainly_if `{!Sbi PROP} (p : bool) (P : PROP) : PROP
:=
  (if p then ■ P else P)%I.
(* iris/bi/plainly.v *)
Instance : Params (@plainly_if) 2
:= {}.
(* iris/bi/plainly.v *)
Notation "■? p P"
:= (plainly_if p P) : bi_scope.
(* iris/bi/plainly.v *)
Instance plainly_ne : NonExpansive (plainly (PROP:=PROP)).
Proof. solve_proper. Qed.
(* iris/bi/plainly.v *)
Instance plainly_proper : Proper ((⊣⊢) ==> (⊣⊢)) (@plainly PROP _).
Proof. apply ne_proper, _. Qed.
(* iris/bi/plainly.v *)
Lemma plainly_mono P Q : (P ⊢ Q) → ■ P ⊢ ■ Q.
Proof. intros. by apply si_pure_mono, si_emp_valid_mono. Qed.
(* iris/bi/plainly.v *)
Instance plainly_mono' : Proper ((⊢) ==> (⊢)) (@plainly PROP _).
Proof. intros P Q; apply plainly_mono. Qed.
(* iris/bi/plainly.v *)
Instance plainly_flip_mono' :
    Proper (flip (⊢) ==> flip (⊢)) (@plainly PROP _).
Proof. intros P Q; apply plainly_mono. Qed.
(* iris/bi/plainly.v *)
Lemma plainly_elim_persistently P : ■ P ⊢ <pers> P.
Proof. apply si_pure_si_emp_valid. Qed.
(* iris/bi/plainly.v *)
Lemma plainly_idemp_2 P : ■ P ⊢ ■ ■ P.
Proof. by rewrite /plainly si_emp_valid_si_pure. Qed.
(* iris/bi/plainly.v *)
Lemma plainly_forall_2 {A} (Ψ : A → PROP) : (∀ a, ■ (Ψ a)) ⊢ ■ (∀ a, Ψ a).
Proof. by rewrite /plainly si_emp_valid_forall si_pure_forall. Qed.
(* iris/bi/plainly.v *)
Lemma plainly_exist_1 `{!SbiEmpValidExist PROP} {A} (Ψ : A → PROP) :
    ■ (∃ a, Ψ a) ⊢ ∃ a, ■ (Ψ a).
Proof. by rewrite /plainly si_emp_valid_exist si_pure_exist. Qed.
(* iris/bi/plainly.v *)
Lemma plainly_impl_plainly P Q : (■ P → ■ Q) ⊢ ■ (■ P → Q).
Proof. by rewrite /plainly si_pure_impl_2 -si_emp_valid_impl_si_pure. Qed.
(* iris/bi/plainly.v *)
Lemma plainly_emp_intro P : P ⊢ ■ emp.
Proof. rewrite /plainly si_emp_valid_emp si_pure_pure. apply True_intro. Qed.
(* iris/bi/plainly.v *)
Lemma plainly_absorb P Q : ■ P ∗ Q ⊢ ■ P.
Proof. by rewrite /plainly sep_elim_l. Qed.
(* iris/bi/plainly.v *)
Lemma later_plainly P : ▷ ■ P ⊣⊢ ■ ▷ P.
Proof. by rewrite /plainly -si_pure_later -si_emp_valid_later. Qed.
(* iris/bi/plainly.v *)
Lemma later_plainly_1 P : ▷ ■ P ⊢ ■ (▷ P).
Proof. by rewrite later_plainly. Qed.
(* iris/bi/plainly.v *)
Lemma later_plainly_2 P : ■ ▷ P ⊢ ▷ ■ P.
Proof. by rewrite later_plainly. Qed.
(* iris/bi/plainly.v *)
Lemma affinely_plainly_elim P : <affine> ■ P ⊢ P.
Proof.
    by rewrite plainly_elim_persistently /bi_affinely persistently_and_emp_elim.
  Qed.
(* iris/bi/plainly.v *)
Lemma persistently_elim_plainly P : <pers> ■ P ⊣⊢ ■ P.
Proof.
    apply (anti_symm _).
    - by rewrite persistently_into_absorbingly /bi_absorbingly comm plainly_absorb.
    - by rewrite {1}plainly_idemp_2 plainly_elim_persistently.
  Qed.
(* iris/bi/plainly.v *)
Lemma persistently_if_elim_plainly P p : <pers>?p ■ P ⊣⊢ ■ P.
Proof. destruct p; last done. exact: persistently_elim_plainly. Qed.
(* iris/bi/plainly.v *)
Lemma plainly_persistently_elim P : ■ <pers> P ⊣⊢ ■ P.
Proof.
    apply (anti_symm _).
    - rewrite -{1}(left_id True%I bi_and (■ _)%I) (plainly_emp_intro True).
      rewrite -{2}(persistently_and_emp_elim P).
      rewrite !and_alt -plainly_forall_2. by apply forall_mono=> -[].
    - by rewrite {1}plainly_idemp_2 (plainly_elim_persistently P).
  Qed.