Library iris.bi.monpred

From stdpp Require Import coPset.
From iris.bi Require Import bi.
From iris.prelude Require Import options.

Definitions.
Structure biIndex :=
  BiIndex
    { bi_index_type :> Type;
      bi_index_inhabited : Inhabited bi_index_type;
      bi_index_rel : SqSubsetEq bi_index_type;
      bi_index_rel_preorder : PreOrder (⊑@{bi_index_type}) }.
Global Existing Instances bi_index_inhabited bi_index_rel bi_index_rel_preorder.

Class BiIndexBottom {I : biIndex} (bot : I) :=
  bi_index_bot i : bot ⊑ i.

Section cofe.
  Context {I : biIndex} {PROP : bi}.
  Implicit Types i : I.

  Record monPred :=
    MonPred { monPred_at :> I → PROP;
              monPred_mono : Proper ((⊑) ==> (⊢)) monPred_at }.
  Local Existing Instance monPred_mono.

  Bind Scope bi_scope with monPred.

  Implicit Types P Q : monPred.

Ofe + Cofe instances

  Section cofe_def.
    Inductive monPred_equiv' P Q : Prop :=
      { monPred_in_equiv i : P i ≡ Q i } .
    Local Instance monPred_equiv : Equiv monPred := monPred_equiv'.
    Inductive monPred_dist' (n : nat) (P Q : monPred) : Prop :=
      { monPred_in_dist i : P i ≡{n}≡ Q i }.
    Local Instance monPred_dist : Dist monPred := monPred_dist'.

    Definition monPred_sig P : { f : I -d> PROP | Proper ((⊑) ==> (⊢)) f } :=
      exist _ (monPred_at P) (monPred_mono P).

    Definition sig_monPred (P' : { f : I -d> PROP | Proper ((⊑) ==> (⊢)) f })
      : monPred :=
      MonPred (proj1_sig P') (proj2_sig P').

    Let monPred_sig_equiv:
      ∀ P Q, P ≡ Q ↔ monPred_sig P ≡ monPred_sig Q.
    Proof. by split; [intros []|]. Defined.
    Let monPred_sig_dist:
      ∀ n, ∀ P Q : monPred, P ≡{n}≡ Q ↔ monPred_sig P ≡{n}≡ monPred_sig Q.
    Proof. by split; [intros []|]. Defined.

    Definition monPred_ofe_mixin : OfeMixin monPred.
    Proof.
      by apply (iso_ofe_mixin monPred_sig monPred_sig_equiv monPred_sig_dist).
    Qed.

    Canonical Structure monPredO := Ofe monPred monPred_ofe_mixin.

    Global Instance monPred_cofe `{!Cofe PROP} : Cofe monPredO.
    Proof.
      refine ((iso_cofe_subtype' (A:=I-d>PROP) _ MonPred monPred_at _ _ _) _);
        [done..|].
      apply limit_preserving_forall⇒ y. apply limit_preserving_forall⇒ x.
      apply limit_preserving_impl; [solve_proper|].
      apply bi.limit_preserving_entails; solve_proper.
    Qed.
  End cofe_def.

  Lemma monPred_sig_monPred (P' : { f : I -d> PROP | Proper ((⊑) ==> (⊢)) f }) :
    monPred_sig (sig_monPred P') ≡ P'.
  Proof. by change (P' ≡ P'). Qed.
  Lemma sig_monPred_sig P : sig_monPred (monPred_sig P) ≡ P.
  Proof. done. Qed.

  Global Instance monPred_sig_ne : NonExpansive monPred_sig.
  Proof. move⇒ ??? [?] ? //=. Qed.
  Global Instance monPred_sig_proper : Proper ((≡) ==> (≡)) monPred_sig.
  Proof. eapply (ne_proper _). Qed.
  Global Instance sig_monPred_ne : NonExpansive (@sig_monPred).
  Proof. split=>? //=. Qed.
  Global Instance sig_monPred_proper : Proper ((≡) ==> (≡)) sig_monPred.
  Proof. eapply (ne_proper _). Qed.

  Global Instance monPred_at_ne (R : relation I) :
    Proper (R ==> R ==> iff) (⊑) → Reflexive R →
    ∀ n, Proper (dist n ==> R ==> dist n) monPred_at.
  Proof.
    intros ????? [Hd] ?? HR. rewrite Hd.
    apply equiv_dist, bi.equiv_entails; split; f_equiv; rewrite →HR; done.
  Qed.
  Global Instance monPred_at_proper (R : relation I) :
    Proper (R ==> R ==> iff) (⊑) → Reflexive R →
    Proper ((≡) ==> R ==> (≡)) monPred_at.
  Proof. repeat intro. apply equiv_dist=>?. f_equiv=>//. by apply equiv_dist. Qed.
End cofe.

Global Arguments monPred _ _ : clear implicits.
Global Arguments monPred_at {_ _} _%_I _.
Local Existing Instance monPred_mono.
Global Arguments monPredO _ _ : clear implicits.

BI canonical structure and type class instances
Module Export monPred_defs.
Section monPred_defs.
  Context {I : biIndex} {PROP : bi}.
  Implicit Types i : I.
  Notation monPred := (monPred I PROP).
  Implicit Types P Q : monPred.

  Inductive monPred_entails (P1 P2 : monPred) : Prop :=
    { monPred_in_entails i : P1 i ⊢ P2 i }.
  Local Hint Immediate monPred_in_entails : core.

  Program Definition monPred_upclosed (Φ : I → PROP) : monPred :=
    MonPred (λ i, (∀ j, ⌜i ⊑ j⌝ → Φ j)%I) _.
  Next Obligation. solve_proper. Qed.

  Local Definition monPred_embed_def : Embed PROP monPred := λ (P : PROP),
    MonPred (λ _, P) _.
  Local Definition monPred_embed_aux : seal (@monPred_embed_def).
  Proof. by eexists. Qed.
  Definition monPred_embed := monPred_embed_aux.(unseal).
  Local Definition monPred_embed_unseal :
    @embed _ _ monPred_embed = _ := monPred_embed_aux.(seal_eq).

  Local Definition monPred_emp_def : monPred := MonPred (λ _, emp)%I _.
  Local Definition monPred_emp_aux : seal (@monPred_emp_def). Proof. by eexists. Qed.
  Definition monPred_emp := monPred_emp_aux.(unseal).
  Local Definition monPred_emp_unseal :
    @monPred_emp = _ := monPred_emp_aux.(seal_eq).

  Local Definition monPred_pure_def (φ : Prop) : monPred := MonPred (λ _, ⌜φ⌝)%I _.
  Local Definition monPred_pure_aux : seal (@monPred_pure_def).
  Proof. by eexists. Qed.
  Definition monPred_pure := monPred_pure_aux.(unseal).
  Local Definition monPred_pure_unseal :
    @monPred_pure = _ := monPred_pure_aux.(seal_eq).

  Local Definition monPred_objectively_def P : monPred :=
    MonPred (λ _, ∀ i, P i)%I _.
  Local Definition monPred_objectively_aux : seal (@monPred_objectively_def).
  Proof. by eexists. Qed.
  Definition monPred_objectively := monPred_objectively_aux.(unseal).
  Local Definition monPred_objectively_unseal :
    @monPred_objectively = _ := monPred_objectively_aux.(seal_eq).

  Local Definition monPred_subjectively_def P : monPred := MonPred (λ _, ∃ i, P i)%I _.
  Local Definition monPred_subjectively_aux : seal (@monPred_subjectively_def).
  Proof. by eexists. Qed.
  Definition monPred_subjectively := monPred_subjectively_aux.(unseal).
  Local Definition monPred_subjectively_unseal :
    @monPred_subjectively = _ := monPred_subjectively_aux.(seal_eq).

  Local Program Definition monPred_and_def P Q : monPred :=
    MonPred (λ i, P i ∧ Q i)%I _.
  Next Obligation. solve_proper. Qed.
  Local Definition monPred_and_aux : seal (@monPred_and_def).
  Proof. by eexists. Qed.
  Definition monPred_and := monPred_and_aux.(unseal).
  Local Definition monPred_and_unseal :
    @monPred_and = _ := monPred_and_aux.(seal_eq).

  Local Program Definition monPred_or_def P Q : monPred :=
    MonPred (λ i, P i ∨ Q i)%I _.
  Next Obligation. solve_proper. Qed.
  Local Definition monPred_or_aux : seal (@monPred_or_def).
  Proof. by eexists. Qed.
  Definition monPred_or := monPred_or_aux.(unseal).
  Local Definition monPred_or_unseal :
    @monPred_or = _ := monPred_or_aux.(seal_eq).

  Local Definition monPred_impl_def P Q : monPred :=
    monPred_upclosed (λ i, P i → Q i)%I.
  Local Definition monPred_impl_aux : seal (@monPred_impl_def).
  Proof. by eexists. Qed.
  Definition monPred_impl := monPred_impl_aux.(unseal).
  Local Definition monPred_impl_unseal :
    @monPred_impl = _ := monPred_impl_aux.(seal_eq).

  Local Program Definition monPred_forall_def A (Φ : A → monPred) : monPred :=
    MonPred (λ i, ∀ x : A, Φ x i)%I _.
  Next Obligation. solve_proper. Qed.
  Local Definition monPred_forall_aux : seal (@monPred_forall_def).
  Proof. by eexists. Qed.
  Definition monPred_forall := monPred_forall_aux.(unseal).
  Local Definition monPred_forall_unseal :
    @monPred_forall = _ := monPred_forall_aux.(seal_eq).

  Local Program Definition monPred_exist_def A (Φ : A → monPred) : monPred :=
    MonPred (λ i, ∃ x : A, Φ x i)%I _.
  Next Obligation. solve_proper. Qed.
  Local Definition monPred_exist_aux : seal (@monPred_exist_def).
  Proof. by eexists. Qed.
  Definition monPred_exist := monPred_exist_aux.(unseal).
  Local Definition monPred_exist_unseal :
    @monPred_exist = _ := monPred_exist_aux.(seal_eq).

  Local Program Definition monPred_sep_def P Q : monPred :=
    MonPred (λ i, P i ∗ Q i)%I _.
  Next Obligation. solve_proper. Qed.
  Local Definition monPred_sep_aux : seal (@monPred_sep_def).
  Proof. by eexists. Qed.
  Definition monPred_sep := monPred_sep_aux.(unseal).
  Local Definition monPred_sep_unseal :
    @monPred_sep = _ := monPred_sep_aux.(seal_eq).

  Local Definition monPred_wand_def P Q : monPred :=
    monPred_upclosed (λ i, P i -∗ Q i)%I.
  Local Definition monPred_wand_aux : seal (@monPred_wand_def).
  Proof. by eexists. Qed.
  Definition monPred_wand := monPred_wand_aux.(unseal).
  Local Definition monPred_wand_unseal :
    @monPred_wand = _ := monPred_wand_aux.(seal_eq).

  Local Program Definition monPred_persistently_def P : monPred :=
    MonPred (λ i, <pers> (P i))%I _.
  Next Obligation. solve_proper. Qed.
  Local Definition monPred_persistently_aux : seal (@monPred_persistently_def).
  Proof. by eexists. Qed.
  Definition monPred_persistently := monPred_persistently_aux.(unseal).
  Local Definition monPred_persistently_unseal :
    @monPred_persistently = _ := monPred_persistently_aux.(seal_eq).

  Local Program Definition monPred_in_def (i0 : I) : monPred :=
    MonPred (λ i : I, ⌜i0 ⊑ i⌝%I) _.
  Next Obligation. solve_proper. Qed.
  Local Definition monPred_in_aux : seal (@monPred_in_def). Proof. by eexists. Qed.
  Definition monPred_in := monPred_in_aux.(unseal).
  Local Definition monPred_in_unseal :
    @monPred_in = _ := monPred_in_aux.(seal_eq).

  Local Program Definition monPred_later_def P : monPred := MonPred (λ i, ▷ (P i))%I _.
  Next Obligation. solve_proper. Qed.
  Local Definition monPred_later_aux : seal monPred_later_def.
  Proof. by eexists. Qed.
  Definition monPred_later := monPred_later_aux.(unseal).
  Local Definition monPred_later_unseal :
    monPred_later = _ := monPred_later_aux.(seal_eq).

  Local Program Definition monPred_bupd_def `{BiBUpd PROP}
    (P : monPred) : monPred := MonPred (λ i, |==> P i)%I _.
  Next Obligation. solve_proper. Qed.
  Local Definition monPred_bupd_aux : seal (@monPred_bupd_def).
  Proof. by eexists. Qed.
  Definition monPred_bupd := monPred_bupd_aux.(unseal).
  Global Arguments monPred_bupd {_}.
  Local Definition monPred_bupd_unseal `{BiBUpd PROP} :
    @bupd _ monPred_bupd = monPred_bupd_def.
  Proof. by rewrite -monPred_bupd_aux.(seal_eq). Qed.

  Local Program Definition monPred_fupd_def `{BiFUpd PROP} (E1 E2 : coPset)
    (P : monPred) : monPred := MonPred (λ i, |={E1,E2}=> P i)%I _.
  Next Obligation. solve_proper. Qed.
  Local Definition monPred_fupd_aux : seal (@monPred_fupd_def).
  Proof. by eexists. Qed.
  Definition monPred_fupd := monPred_fupd_aux.(unseal).
  Global Arguments monPred_fupd {_}.
  Local Definition monPred_fupd_unseal `{BiFUpd PROP} :
    @fupd _ monPred_fupd = monPred_fupd_def.
  Proof. by rewrite -monPred_fupd_aux.(seal_eq). Qed.

  Local Definition monPred_si_pure_def `{Sbi PROP} (Pi : siProp) : monPred :=
    MonPred (λ _, <si_pure> Pi)%I _.
  Local Definition monPred_si_pure_aux : seal (@monPred_si_pure_def).
  Proof. by eexists. Qed.
  Definition monPred_si_pure := monPred_si_pure_aux.(unseal).
  Global Arguments monPred_si_pure {_}.
  Local Definition monPred_si_pure_unseal `{Sbi PROP} :
    @si_pure _ monPred_si_pure = monPred_si_pure_def.
  Proof. by rewrite -monPred_si_pure_aux.(seal_eq). Qed.

  Local Definition monPred_si_emp_valid_def `{!Sbi PROP} P : siProp :=
    <si_emp_valid> ∀ i, P i.
  Local Definition monPred_si_emp_valid_aux : seal (@monPred_si_emp_valid_def).
  Proof. by eexists. Qed.
  Definition monPred_si_emp_valid := monPred_si_emp_valid_aux.(unseal).
  Global Arguments monPred_si_emp_valid {_}.
  Local Definition monPred_si_emp_valid_unseal `{!Sbi PROP} :
    @si_emp_valid _ monPred_si_emp_valid = monPred_si_emp_valid_def.
  Proof. by rewrite -monPred_si_emp_valid_aux.(seal_eq). Qed.
End monPred_defs.

This is not the final collection of unsealing lemmas, below we redefine monPred_unseal to also unfold the BI layer (i.e., the projections of the BI structures/classes).
Local Definition monPred_unseal :=
  (@monPred_embed_unseal, @monPred_emp_unseal, @monPred_pure_unseal,
   @monPred_objectively_unseal, @monPred_subjectively_unseal,
   @monPred_and_unseal, @monPred_or_unseal, @monPred_impl_unseal,
   @monPred_forall_unseal, @monPred_exist_unseal, @monPred_sep_unseal,
   @monPred_wand_unseal, @monPred_persistently_unseal,
   @monPred_in_unseal, @monPred_later_unseal).
End monPred_defs.

Global Arguments monPred_objectively {_ _} _%_I.
Global Arguments monPred_subjectively {_ _} _%_I.
Notation "'<obj>' P" := (monPred_objectively P) : bi_scope.
Notation "'<subj>' P" := (monPred_subjectively P) : bi_scope.

Section instances.
  Context (I : biIndex) (PROP : bi).

  Lemma monPred_bi_mixin : BiMixin (PROP:=monPred I PROP)
    monPred_entails monPred_emp monPred_pure monPred_and monPred_or
    monPred_impl monPred_forall monPred_exist monPred_sep monPred_wand.
  Proof.
    split; rewrite ?monPred_defs.monPred_unseal;
      try by (split⇒ ? /=; repeat f_equiv).
    - split.
      + intros P. by split.
      + intros P Q R [H1] [H2]. split ⇒ ?. by rewrite H1 H2.
    - split.
      + intros [HPQ]. split; split ⇒ i; move: (HPQ i); by apply bi.equiv_entails.
      + intros [[] []]. split⇒i. by apply bi.equiv_entails.
    - intros P φ ?. split⇒ i. by apply bi.pure_intro.
    - intros φ P HP. split⇒ i. apply bi.pure_elim'⇒ ?. by apply HP.
    - intros P Q. split⇒ i. by apply bi.and_elim_l.
    - intros P Q. split⇒ i. by apply bi.and_elim_r.
    - intros P Q R [?] [?]. split⇒ i. by apply bi.and_intro.
    - intros P Q. split⇒ i. by apply bi.or_intro_l.
    - intros P Q. split⇒ i. by apply bi.or_intro_r.
    - intros P Q R [?] [?]. split⇒ i. by apply bi.or_elim.
    - intros P Q R [HR]. split⇒ i /=. setoid_rewrite bi.pure_impl_forall.
      apply bi.forall_intro⇒ j. apply bi.forall_intro⇒ Hij.
      apply bi.impl_intro_r. by rewrite -HR /= !Hij.
    - intros P Q R [HR]. split⇒ i /=.
      rewrite HR /= bi.forall_elim bi.pure_impl_forall bi.forall_elim //.
      apply bi.impl_elim_l.
    - intros A P Ψ HΨ. split⇒ i. apply bi.forall_intro ⇒ ?. by apply HΨ.
    - intros A Ψ. split⇒ i. by apply: bi.forall_elim.
    - intros A Ψ a. split⇒ i. by rewrite /= -bi.exist_intro.
    - intros A Ψ Q HΨ. split⇒ i. apply bi.exist_elim ⇒ a. by apply HΨ.
    - intros P P' Q Q' [?] [?]. split⇒ i. by apply bi.sep_mono.
    - intros P. split⇒ i. by apply bi.emp_sep_1.
    - intros P. split⇒ i. by apply bi.emp_sep_2.
    - intros P Q. split⇒ i. by apply bi.sep_comm'.
    - intros P Q R. split⇒ i. by apply bi.sep_assoc'.
    - intros P Q R [HR]. split⇒ i /=. setoid_rewrite bi.pure_impl_forall.
      apply bi.forall_intro⇒ j. apply bi.forall_intro⇒ Hij.
      apply bi.wand_intro_r. by rewrite -HR /= !Hij.
    - intros P Q R [HP]. split⇒ i. apply bi.wand_elim_l'.
      rewrite HP /= bi.forall_elim bi.pure_impl_forall bi.forall_elim //.
  Qed.

  Lemma monPred_bi_persistently_mixin :
    BiPersistentlyMixin (PROP:=monPred I PROP)
      monPred_entails monPred_emp monPred_and
      monPred_exist monPred_sep monPred_persistently.
  Proof.
    split; rewrite ?monPred_defs.monPred_unseal;
      try by (split⇒ ? /=; repeat f_equiv).
    - intros P Q [?]. split⇒ i /=. by f_equiv.
    - intros P. split⇒ i. by apply bi.persistently_idemp_2.
    - split⇒ i. by apply bi.persistently_emp_intro.
    - intros A Ψ. split⇒ i. by apply bi.persistently_and_2.
    - intros A Ψ. split⇒ i. by apply bi.persistently_exist_1.
    - intros P Q. split⇒ i. apply bi.sep_elim_l, _.
    - intros P Q. split⇒ i. by apply bi.persistently_and_sep_elim.
  Qed.

  Lemma monPred_bi_later_mixin :
    BiLaterMixin (PROP:=monPred I PROP)
      monPred_entails monPred_pure
      monPred_or monPred_impl monPred_forall monPred_exist
      monPred_sep monPred_persistently monPred_later.
  Proof.
    split; rewrite ?monPred_defs.monPred_unseal.
    - by split⇒ ? /=; repeat f_equiv.
    - intros P Q [?]. split⇒ i. by apply bi.later_mono.
    - intros P. split⇒ i /=. by apply bi.later_intro.
    - intros A Ψ. split⇒ i. by apply bi.later_forall_2.
    - intros A Ψ. split⇒ i. by apply bi.later_exist_false.
    - intros P Q. split⇒ i. by apply bi.later_sep_1.
    - intros P Q. split⇒ i. by apply bi.later_sep_2.
    - intros P. split⇒ i. by apply bi.later_persistently_1.
    - intros P. split⇒ i. by apply bi.later_persistently_2.
    - intros P. split⇒ i /=. rewrite -bi.forall_intro.
      + apply bi.later_false_em.
      + intros j. rewrite bi.pure_impl_forall. apply bi.forall_intro⇒ Hij.
        by rewrite Hij.
  Qed.

  Canonical Structure monPredI : bi :=
    {| bi_ofe_mixin := monPred_ofe_mixin;
       bi_bi_mixin := monPred_bi_mixin;
       bi_bi_persistently_mixin := monPred_bi_persistently_mixin;
       bi_bi_later_mixin := monPred_bi_later_mixin |}.

We restate the unsealing lemmas so that they also unfold the BI layer. The sealing lemmas are partially applied so that they also work under binders.
  Local Lemma monPred_emp_unseal :
    bi_emp = @monPred_defs.monPred_emp_def I PROP.
  Proof. by rewrite -monPred_defs.monPred_emp_unseal. Qed.
  Local Lemma monPred_pure_unseal :
    bi_pure = @monPred_defs.monPred_pure_def I PROP.
  Proof. by rewrite -monPred_defs.monPred_pure_unseal. Qed.
  Local Lemma monPred_and_unseal :
    bi_and = @monPred_defs.monPred_and_def I PROP.
  Proof. by rewrite -monPred_defs.monPred_and_unseal. Qed.
  Local Lemma monPred_or_unseal :
    bi_or = @monPred_defs.monPred_or_def I PROP.
  Proof. by rewrite -monPred_defs.monPred_or_unseal. Qed.
  Local Lemma monPred_impl_unseal :
    bi_impl = @monPred_defs.monPred_impl_def I PROP.
  Proof. by rewrite -monPred_defs.monPred_impl_unseal. Qed.
  Local Lemma monPred_forall_unseal :
    @bi_forall _ = @monPred_defs.monPred_forall_def I PROP.
  Proof. by rewrite -monPred_defs.monPred_forall_unseal. Qed.
  Local Lemma monPred_exist_unseal :
    @bi_exist _ = @monPred_defs.monPred_exist_def I PROP.
  Proof. by rewrite -monPred_defs.monPred_exist_unseal. Qed.
  Local Lemma monPred_sep_unseal :
    bi_sep = @monPred_defs.monPred_sep_def I PROP.
  Proof. by rewrite -monPred_defs.monPred_sep_unseal. Qed.
  Local Lemma monPred_wand_unseal :
    bi_wand = @monPred_defs.monPred_wand_def I PROP.
  Proof. by rewrite -monPred_defs.monPred_wand_unseal. Qed.
  Local Lemma monPred_persistently_unseal :
    bi_persistently = @monPred_defs.monPred_persistently_def I PROP.
  Proof. by rewrite -monPred_defs.monPred_persistently_unseal. Qed.
  Local Lemma monPred_later_unseal :
    bi_later = @monPred_defs.monPred_later_def I PROP.
  Proof. by rewrite -monPred_defs.monPred_later_unseal. Qed.

This definition only includes the unseal lemmas for the bi connectives. After we have defined the right class instances, we define monPred_unseal, which also includes embed, internal_eq, bupd, fupd, plainly, monPred_objectively, monPred_subjectively and monPred_in.
  Local Definition monPred_unseal_bi :=
    (monPred_emp_unseal, monPred_pure_unseal, monPred_and_unseal,
    monPred_or_unseal, monPred_impl_unseal, monPred_forall_unseal,
    monPred_exist_unseal, monPred_sep_unseal, monPred_wand_unseal,
    monPred_persistently_unseal, monPred_later_unseal).

  Definition monPred_embedding_mixin : BiEmbedMixin PROP monPredI monPred_embed.
  Proof.
    split; try apply _; rewrite /bi_emp_valid
      !(monPred_defs.monPred_embed_unseal, monPred_unseal_bi); try done.
    - move⇒ P /= [/(_ inhabitant) ?] //.
    - intros P Q. split⇒ i /=.
      by rewrite bi.forall_elim bi.pure_impl_forall bi.forall_elim.
    - intros P Q. split⇒ i /=.
      by rewrite bi.forall_elim bi.pure_impl_forall bi.forall_elim.
  Qed.
  Global Instance monPred_bi_embed : BiEmbed PROP monPredI :=
    {| bi_embed_mixin := monPred_embedding_mixin |}.

  Lemma monPred_sbi_mixin `{!Sbi PROP} :
    SbiMixin monPredI monPred_si_pure monPred_si_emp_valid.
  Proof.
    split; rewrite /Absorbing /bi_affinely /bi_absorbingly
      !(monPred_defs.monPred_si_pure_unseal,
        monPred_defs.monPred_si_emp_valid_unseal, monPred_unseal_bi)
      /monPred_defs.monPred_si_emp_valid_def /=.
    - split⇒ i /=. solve_proper.
    - solve_proper.
    - intros Pi Qi HPQ. split⇒ i /=. by rewrite HPQ.
    - intros P Q [HPQ]. by setoid_rewrite HPQ.
    - intros Pi. apply (anti_symm _).
      + by rewrite (bi.forall_elim inhabitant) si_emp_valid_si_pure.
      + rewrite si_emp_valid_forall. apply bi.forall_intro⇒ _.
        by rewrite si_emp_valid_si_pure.
    - intros P. split⇒ i /=. by rewrite si_pure_si_emp_valid (bi.forall_elim i).
    - intros Pi Qi. split⇒ i /=. rewrite si_pure_impl.
      by rewrite (bi.forall_elim i) bi.pure_True // left_id.
    - intros A Φi. split⇒ i /=. apply si_pure_forall_2.
    - intros Pi. split⇒ i /=. apply si_pure_later.
    - intros Pi. split⇒ i /=. by rewrite bi.sep_elim_r.
    - intros P. by rewrite -si_emp_valid_later_1 bi.later_forall.
    - intros P. rewrite !si_emp_valid_forall. f_equiv⇒ i.
      apply si_emp_valid_affinely_2.
  Qed.
  Lemma monPred_sbi_prop_ext_mixin `{!Sbi PROP} :
    SbiPropExtMixin monPredI monPred_si_emp_valid.
  Proof.
    apply sbi_prop_ext_mixin⇒ P Q.
    rewrite /bi_wand_iff
      !(monPred_defs.monPred_si_emp_valid_unseal, monPred_unseal_bi)
      /monPred_defs.monPred_si_emp_valid_def /=.
    rewrite -{3}(sig_monPred_sig P) -{3}(sig_monPred_sig Q)
      -f_equivI -sig_equivI !discrete_fun_equivI /=.
    apply bi.forall_intro⇒ j. rewrite prop_ext_si_emp_valid.
    by rewrite !(bi.forall_elim j) !bi.pure_True // !bi.True_impl.
  Qed.
  Global Instance monPred_sbi `{!Sbi PROP} : Sbi monPredI :=
    {| sbi_sbi_mixin := monPred_sbi_mixin;
       sbi_sbi_prop_ext_mixin := monPred_sbi_prop_ext_mixin |}.

  Lemma monPred_bupd_mixin `{BiBUpd PROP} : BiBUpdMixin monPredI monPred_bupd.
  Proof.
    split; rewrite !(monPred_defs.monPred_bupd_unseal, monPred_unseal_bi).
    - split=>/= i. solve_proper.
    - intros P. split=>/= i. apply bupd_intro.
    - intros P Q [HPQ]. split=>/= i. by rewrite HPQ.
    - intros P. split=>/= i. apply bupd_trans.
    - intros P Q. split=>/= i. apply bupd_frame_r.
  Qed.
  Global Instance monPred_bi_bupd `{BiBUpd PROP} : BiBUpd monPredI :=
    {| bi_bupd_mixin := monPred_bupd_mixin |}.

  Lemma monPred_fupd_mixin `{BiFUpd PROP} : BiFUpdMixin monPredI monPred_fupd.
  Proof.
    split; rewrite /bi_emp_valid /bi_except_0
      !(monPred_defs.monPred_fupd_unseal, monPred_unseal_bi).
    - split=>/= i. solve_proper.
    - intros E1 E2 HE12. split=>/= i. by apply fupd_mask_intro_subseteq.
    - intros E1 E2 P. split=>/= i. apply except_0_fupd.
    - intros E1 E2 P Q [HPQ]. split=>/= i. by rewrite HPQ.
    - intros E1 E2 E3 P. split=>/= i. apply fupd_trans.
    - intros E1 E2 Ef P HE1f. split=>/= i.
      by rewrite (bi.forall_elim i) bi.pure_True // left_id fupd_mask_frame_r'.
    - intros E1 E2 P Q. split=>/= i. apply fupd_frame_r.
  Qed.
  Global Instance monPred_bi_fupd `{BiFUpd PROP} : BiFUpd monPredI :=
    {| bi_fupd_mixin := monPred_fupd_mixin |}.

  Local Lemma monPred_embed_unseal :
    embed = @monPred_defs.monPred_embed_def I PROP.
  Proof. by rewrite -monPred_defs.monPred_embed_unseal. Qed.
  Local Lemma monPred_bupd_unseal `{!BiBUpd PROP} :
    bupd = @monPred_defs.monPred_bupd_def I PROP _.
  Proof. by rewrite -monPred_defs.monPred_bupd_unseal. Qed.
  Local Lemma monPred_fupd_unseal `{!BiFUpd PROP} :
    fupd = @monPred_defs.monPred_fupd_def I PROP _.
  Proof. by rewrite -monPred_defs.monPred_fupd_unseal. Qed.
  Local Lemma monPred_si_pure_unseal `{!Sbi PROP} :
    si_pure = @monPred_defs.monPred_si_pure_def I PROP _.
  Proof. by rewrite -monPred_defs.monPred_si_pure_unseal. Qed.
  Local Lemma monPred_si_emp_valid_unseal `{!Sbi PROP} :
    si_emp_valid = @monPred_defs.monPred_si_emp_valid_def I PROP _.
  Proof. by rewrite -monPred_defs.monPred_si_emp_valid_unseal. Qed.

And finally the proper unseal tactic (which we also redefine outside of the section since Ltac definitions do not outlive a section).
  Local Definition monPred_unseal :=
    (monPred_unseal_bi,
    @monPred_defs.monPred_objectively_unseal,
    @monPred_defs.monPred_subjectively_unseal,
    @monPred_embed_unseal, @monPred_bupd_unseal, @monPred_fupd_unseal,
    @monPred_si_pure_unseal, @monPred_si_emp_valid_unseal,
    @monPred_defs.monPred_in_unseal).
  Ltac unseal := rewrite !monPred_unseal /=.

  Global Instance monPred_bi_löb : BiLöb PROP → BiLöb monPredI.
  Proof. rewrite {2}/BiLöb; unseal⇒ ? P HP; split⇒ i /=. apply löb_weak, HP. Qed.
  Global Instance monPred_bi_positive : BiPositive PROP → BiPositive monPredI.
  Proof. split ⇒ ?. rewrite /bi_affinely. unseal. apply bi_positive. Qed.
  Global Instance monPred_bi_affine : BiAffine PROP → BiAffine monPredI.
  Proof. split ⇒ ?. unseal. by apply affine. Qed.

  Global Instance monPred_bi_persistently_forall :
    BiPersistentlyForall PROP → BiPersistentlyForall monPredI.
  Proof. intros ? A φ. split⇒ /= i. unseal. by apply persistently_forall_2. Qed.

  Global Instance monPred_bi_pure_forall :
    BiPureForall PROP → BiPureForall monPredI.
  Proof. intros ? A φ. split⇒ /= i. unseal. by apply pure_forall_2. Qed.

  Global Instance monPred_bi_later_contractive :
    BiLaterContractive PROP → BiLaterContractive monPredI.
  Proof. intros ? n. unseal⇒ P Q HPQ. split⇒ i /=. f_contractive. apply HPQ. Qed.

  Global Instance monPred_bi_embed_emp : BiEmbedEmp PROP monPredI.
  Proof. split. by unseal. Qed.

  Global Instance monPred_bi_embed_later : BiEmbedLater PROP monPredI.
  Proof. split; by unseal. Qed.

  Global Instance monPred_bi_bupd_fupd `{BiBUpdFUpd PROP} : BiBUpdFUpd monPredI.
  Proof. intros E P. split⇒ i. unseal. apply bupd_fupd. Qed.

  Global Instance monPred_bi_embed_bupd `{!BiBUpd PROP} :
    BiEmbedBUpd PROP monPredI.
  Proof. split. by unseal. Qed.

  Global Instance monPred_bi_embed_fupd `{BiFUpd PROP} : BiEmbedFUpd PROP monPredI.
  Proof. split. by unseal. Qed.

  Global Instance monPred_bi_persistently_impl_si_pure `{!Sbi PROP,
      !@BiIndexBottom I bot, !BiPersistentlyForall PROP,
      !BiPersistentlyImplSiPure PROP} :
    BiPersistentlyImplSiPure monPredI.
  Proof.
    intros P Q. split⇒ i. unseal. setoid_rewrite bi.pure_impl_forall.
    do 2 setoid_rewrite bi.persistently_forall.
    by setoid_rewrite persistently_impl_si_pure.
  Qed.

  Global Instance monPred_sbi_emp_valid_exist `{!Sbi PROP, @BiIndexBottom I bot} :
    SbiEmpValidExist PROP → SbiEmpValidExist monPredI.
  Proof.
    intros ? A Φ. unseal. rewrite /monPred_defs.monPred_si_emp_valid_def
      /monPred_defs.monPred_exist_def /=.
    rewrite (bi.forall_elim bot) si_emp_valid_exist_1.
    do 3 f_equiv. apply bi.forall_intro⇒ ?. by f_equiv.
  Qed.

  Global Instance monPred_bi_embed_sbi `{!Sbi PROP} : BiEmbedSbi PROP monPredI.
  Proof.
    split; unseal; rewrite /monPred_defs.monPred_si_emp_valid_def /=; [|done].
    intros P. apply (anti_symm _).
    + by rewrite (bi.forall_elim inhabitant).
    + rewrite si_emp_valid_forall. by apply bi.forall_intro.
  Qed.

  Global Instance monPred_bi_bupd_sbi `{BiBUpdSbi PROP, !@BiIndexBottom I bot} :
    BiBUpdSbi monPredI.
  Proof. intros P. split⇒ /= i. unseal. apply bupd_si_pure. Qed.

  Global Instance monPred_bi_fupd_sbi `{BiFUpdSbi PROP, !@BiIndexBottom I bot} :
    BiFUpdSbi monPredI.
  Proof.
    split; rewrite /bi_except_0; unseal.
    - intros E E' P R. split=>/= i.
      rewrite (bi.forall_elim i) bi.pure_True // bi.True_impl.
      apply fupd_si_pure_keep_l.
    - intros E P. split=>/= i. apply fupd_si_pure_later.
    - intros E A Φ. split=>/= i. apply fupd_si_pure_forall_2.
  Qed.
End instances.

The final unseal tactic that also unfolds the BI layer.
Module Import monPred.
  Ltac unseal := rewrite !monPred_unseal /=.
End monPred.

Class Objective {I : biIndex} {PROP : bi} (P : monPred I PROP) :=
  objective_at i j : P i ⊢ P j.
Global Arguments Objective {_ _} _%_I.
Global Arguments objective_at {_ _} _%_I {_}.
Global Hint Mode Objective + + ! : typeclass_instances.
Global Instance: Params (@Objective) 2 := {}.

Primitive facts that cannot be deduced from the BI structure.
Section bi_facts.
  Context {I : biIndex} {PROP : bi}.
  Local Notation monPred := (monPred I PROP).
  Local Notation monPredI := (monPredI I PROP).
  Local Notation monPred_at := (@monPred_at I PROP).
  Local Notation BiIndexBottom := (@BiIndexBottom I).
  Implicit Types i : I.
  Implicit Types P Q : monPred.

monPred_at unfolding laws
  Lemma monPred_at_pure i (φ : Prop) : monPred_at ⌜φ⌝ i ⊣⊢ ⌜φ⌝.
  Proof. by unseal. Qed.
  Lemma monPred_at_emp i : monPred_at emp i ⊣⊢ emp.
  Proof. by unseal. Qed.
  Lemma monPred_at_and i P Q : (P ∧ Q) i ⊣⊢ P i ∧ Q i.
  Proof. by unseal. Qed.
  Lemma monPred_at_or i P Q : (P ∨ Q) i ⊣⊢ P i ∨ Q i.
  Proof. by unseal. Qed.
  Lemma monPred_at_impl i P Q : (P → Q) i ⊣⊢ ∀ j, ⌜i ⊑ j⌝ → P j → Q j.
  Proof. by unseal. Qed.
  Lemma monPred_at_forall {A} i (Φ : A → monPred) : (∀ x, Φ x) i ⊣⊢ ∀ x, Φ x i.
  Proof. by unseal. Qed.
  Lemma monPred_at_exist {A} i (Φ : A → monPred) : (∃ x, Φ x) i ⊣⊢ ∃ x, Φ x i.
  Proof. by unseal. Qed.
  Lemma monPred_at_sep i P Q : (P ∗ Q) i ⊣⊢ P i ∗ Q i.
  Proof. by unseal. Qed.
  Lemma monPred_at_wand i P Q : (P -∗ Q) i ⊣⊢ ∀ j, ⌜i ⊑ j⌝ → P j -∗ Q j.
  Proof. by unseal. Qed.
  Lemma monPred_at_persistently i P : (<pers> P) i ⊣⊢ <pers> (P i).
  Proof. by unseal. Qed.
  Lemma monPred_at_in i j : monPred_at (monPred_in j) i ⊣⊢ ⌜j ⊑ i⌝.
  Proof. by unseal. Qed.
  Lemma monPred_at_objectively i P : (<obj> P) i ⊣⊢ ∀ j, P j.
  Proof. by unseal. Qed.
  Lemma monPred_at_subjectively i P : (<subj> P) i ⊣⊢ ∃ j, P j.
  Proof. by unseal. Qed.
  Lemma monPred_at_persistently_if i p P : (<pers>?p P) i ⊣⊢ <pers>?p (P i).
  Proof. destruct p=>//=. apply monPred_at_persistently. Qed.
  Lemma monPred_at_affinely i P : (<affine> P) i ⊣⊢ <affine> (P i).
  Proof. by rewrite /bi_affinely monPred_at_and monPred_at_emp. Qed.
  Lemma monPred_at_affinely_if i p P : (<affine>?p P) i ⊣⊢ <affine>?p (P i).
  Proof. destruct p=>//=. apply monPred_at_affinely. Qed.
  Lemma monPred_at_intuitionistically i P : (□ P) i ⊣⊢ □ (P i).
  Proof.
    by rewrite /bi_intuitionistically monPred_at_affinely monPred_at_persistently.
  Qed.
  Lemma monPred_at_intuitionistically_if i p P : (□?p P) i ⊣⊢ □?p (P i).
  Proof. destruct p=>//=. apply monPred_at_intuitionistically. Qed.
  Lemma monPred_at_absorbingly i P : (<absorb> P) i ⊣⊢ <absorb> (P i).
  Proof. by rewrite /bi_absorbingly monPred_at_sep monPred_at_pure. Qed.
  Lemma monPred_at_absorbingly_if i p P : (<absorb>?p P) i ⊣⊢ <absorb>?p (P i).
  Proof. destruct p=>//=. apply monPred_at_absorbingly. Qed.

  Lemma monPred_wand_force i P Q : (P -∗ Q) i ⊢ (P i -∗ Q i).
  Proof. unseal. rewrite bi.forall_elim bi.pure_impl_forall bi.forall_elim //. Qed.
  Lemma monPred_impl_force i P Q : (P → Q) i ⊢ (P i → Q i).
  Proof. unseal. rewrite bi.forall_elim bi.pure_impl_forall bi.forall_elim //. Qed.

Instances
  Global Instance monPred_at_mono :
    Proper ((⊢) ==> (⊑) ==> (⊢)) monPred_at.
  Proof. by move⇒ ?? [?] ?? →. Qed.
  Global Instance monPred_at_flip_mono :
    Proper (flip (⊢) ==> flip (⊑) ==> flip (⊢)) monPred_at.
  Proof. solve_proper. Qed.

  Global Instance monPred_in_proper (R : relation I) :
    Proper (R ==> R ==> iff) (⊑) → Reflexive R →
    Proper (R ==> (≡)) (@monPred_in I PROP).
  Proof. unseal. split. solve_proper. Qed.
  Global Instance monPred_in_mono : Proper (flip (⊑) ==> (⊢)) (@monPred_in I PROP).
  Proof. unseal. split. solve_proper. Qed.
  Global Instance monPred_in_flip_mono : Proper ((⊑) ==> flip (⊢)) (@monPred_in I PROP).
  Proof. solve_proper. Qed.

  Lemma monPred_persistent P : (∀ i, Persistent (P i)) → Persistent P.
  Proof. intros HP. constructor⇒ i. unseal. apply HP. Qed.
  Lemma monPred_absorbing P : (∀ i, Absorbing (P i)) → Absorbing P.
  Proof. intros HP. constructor⇒ i. rewrite /bi_absorbingly. unseal. apply HP. Qed.
  Lemma monPred_affine P : (∀ i, Affine (P i)) → Affine P.
  Proof. intros HP. constructor⇒ i. unseal. apply HP. Qed.

  Global Instance monPred_at_persistent P i : Persistent P → Persistent (P i).
  Proof. move ⇒ [] /(_ i). by unseal. Qed.
  Global Instance monPred_at_absorbing P i : Absorbing P → Absorbing (P i).
  Proof. move ⇒ [] /(_ i). rewrite /Absorbing /bi_absorbingly. by unseal. Qed.
  Global Instance monPred_at_affine P i : Affine P → Affine (P i).
  Proof. move ⇒ [] /(_ i). unfold Affine. by unseal. Qed.

Note that monPred_in is *not* Plain, because it depends on the index.
  Global Instance monPred_in_persistent i : Persistent (@monPred_in I PROP i).
  Proof. apply monPred_persistent⇒ j. rewrite monPred_at_in. apply _. Qed.
  Global Instance monPred_in_absorbing i : Absorbing (@monPred_in I PROP i).
  Proof. apply monPred_absorbing⇒ j. rewrite monPred_at_in. apply _. Qed.

  Lemma monPred_at_embed i (P : PROP) : monPred_at ⎡P⎤ i ⊣⊢ P.
  Proof. by unseal. Qed.

  Lemma monPred_emp_unfold : emp%I =@{monPred} ⎡emp : PROP⎤%I.
  Proof. by unseal. Qed.
  Lemma monPred_pure_unfold : bi_pure =@{_ → monPred} λ φ, ⎡ ⌜ φ ⌝ : PROP⎤%I.
  Proof. by unseal. Qed.
  Lemma monPred_objectively_unfold : monPred_objectively = λ P, ⎡∀ i, P i⎤%I.
  Proof. by unseal. Qed.
  Lemma monPred_subjectively_unfold : monPred_subjectively = λ P, ⎡∃ i, P i⎤%I.
  Proof. by unseal. Qed.

  Global Instance monPred_objectively_ne : NonExpansive (@monPred_objectively I PROP).
  Proof. rewrite monPred_objectively_unfold. solve_proper. Qed.
  Global Instance monPred_objectively_proper :
    Proper ((≡) ==> (≡)) (@monPred_objectively I PROP).
  Proof. apply (ne_proper _). Qed.
  Lemma monPred_objectively_mono P Q : (P ⊢ Q) → (<obj> P ⊢ <obj> Q).
  Proof. rewrite monPred_objectively_unfold. solve_proper. Qed.
  Global Instance monPred_objectively_mono' :
    Proper ((⊢) ==> (⊢)) (@monPred_objectively I PROP).
  Proof. intros ???. by apply monPred_objectively_mono. Qed.
  Global Instance monPred_objectively_flip_mono' :
    Proper (flip (⊢) ==> flip (⊢)) (@monPred_objectively I PROP).
  Proof. intros ???. by apply monPred_objectively_mono. Qed.

  Global Instance monPred_objectively_persistent `{!BiPersistentlyForall PROP} P :
    Persistent P → Persistent (<obj> P).
  Proof. rewrite monPred_objectively_unfold. apply _. Qed.
  Global Instance monPred_objectively_absorbing P : Absorbing P → Absorbing (<obj> P).
  Proof. rewrite monPred_objectively_unfold. apply _. Qed.
  Global Instance monPred_objectively_affine P : Affine P → Affine (<obj> P).
  Proof. rewrite monPred_objectively_unfold. apply _. Qed.

  Global Instance monPred_subjectively_ne : NonExpansive (@monPred_subjectively I PROP).
  Proof. rewrite monPred_subjectively_unfold. solve_proper. Qed.
  Global Instance monPred_subjectively_proper :
    Proper ((≡) ==> (≡)) (@monPred_subjectively I PROP).
  Proof. apply (ne_proper _). Qed.
  Lemma monPred_subjectively_mono P Q : (P ⊢ Q) → <subj> P ⊢ <subj> Q.
  Proof. rewrite monPred_subjectively_unfold. solve_proper. Qed.
  Global Instance monPred_subjectively_mono' :
    Proper ((⊢) ==> (⊢)) (@monPred_subjectively I PROP).
  Proof. intros ???. by apply monPred_subjectively_mono. Qed.
  Global Instance monPred_subjectively_flip_mono' :
    Proper (flip (⊢) ==> flip (⊢)) (@monPred_subjectively I PROP).
  Proof. intros ???. by apply monPred_subjectively_mono. Qed.

  Global Instance monPred_subjectively_persistent P :
    Persistent P → Persistent (<subj> P).
  Proof. rewrite monPred_subjectively_unfold. apply _. Qed.
  Global Instance monPred_subjectively_absorbing P :
    Absorbing P → Absorbing (<subj> P).
  Proof. rewrite monPred_subjectively_unfold. apply _. Qed.
  Global Instance monPred_subjectively_affine P : Affine P → Affine (<subj> P).
  Proof. rewrite monPred_subjectively_unfold. apply _. Qed.

  Lemma monPred_objectively_elim P : <obj> P ⊢ P.
  Proof. rewrite monPred_objectively_unfold. unseal. split=>?. apply bi.forall_elim. Qed.
  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.

  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.
  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.
  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.
  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.

  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.
  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.
  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.
  Lemma monPred_objectively_emp : <obj> (emp : monPred) ⊣⊢ emp.
  Proof. rewrite monPred_emp_unfold. apply monPred_objectively_embed. Qed.
  Lemma monPred_objectively_pure φ : <obj> (⌜ φ ⌝ : monPred) ⊣⊢ ⌜ φ ⌝.
  Proof. rewrite monPred_pure_unfold. apply monPred_objectively_embed. Qed.

  Lemma monPred_subjectively_intro P : P ⊢ <subj> P.
  Proof. unseal. split=>?. apply bi.exist_intro. Qed.

  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.
  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.
  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.
  Lemma monPred_subjectively_or P Q : <subj> (P ∨ Q) ⊣⊢ <subj> P ∨ <subj> Q.
  Proof. split⇒i. unseal. apply bi.or_exist. Qed.

  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.

  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.

  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.
  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.

  Global Instance embed_objective (P : PROP) : @Objective I PROP ⎡P⎤.
  Proof. intros ??. by unseal. Qed.
  Global Instance pure_objective φ : @Objective I PROP ⌜φ⌝.
  Proof. intros ??. by unseal. Qed.
  Global Instance emp_objective : @Objective I PROP emp.
  Proof. intros ??. by unseal. Qed.
  Global Instance objectively_objective P : Objective (<obj> P).
  Proof. intros ??. by unseal. Qed.
  Global Instance subjectively_objective P : Objective (<subj> P).
  Proof. intros ??. by unseal. Qed.

  Global Instance and_objective P Q `{!Objective P, !Objective Q} :
    Objective (P ∧ Q).
  Proof. intros i j. unseal. by rewrite !(objective_at _ i j). Qed.
  Global 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.
  Global 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.
  Global 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.
  Global 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.

  Global Instance sep_objective P Q `{!Objective P, !Objective Q} :
    Objective (P ∗ Q).
  Proof. intros i j. unseal. by rewrite !(objective_at _ i j). Qed.
  Global 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.
  Global Instance persistently_objective P `{!Objective P} : Objective (<pers> P).
  Proof. intros i j. unseal. by rewrite objective_at. Qed.

  Global Instance affinely_objective P `{!Objective P} : Objective (<affine> P).
  Proof. rewrite /bi_affinely. apply _. Qed.
  Global Instance intuitionistically_objective P `{!Objective P} : Objective (□ P).
  Proof. rewrite /bi_intuitionistically. apply _. Qed.
  Global Instance absorbingly_objective P `{!Objective P} : Objective (<absorb> P).
  Proof. rewrite /bi_absorbingly. apply _. Qed.
  Global Instance persistently_if_objective P p `{!Objective P} :
    Objective (<pers>?p P).
  Proof. rewrite /bi_persistently_if. destruct p; apply _. Qed.
  Global Instance affinely_if_objective P p `{!Objective P} :
    Objective (<affine>?p P).
  Proof. rewrite /bi_affinely_if. destruct p; apply _. Qed.
  Global Instance absorbingly_if_objective P p `{!Objective P} :
    Objective (<absorb>?p P).
  Proof. rewrite /bi_absorbingly_if. destruct p; apply _. Qed.
  Global Instance intuitionistically_if_objective P p `{!Objective P} :
    Objective (□?p P).
  Proof. rewrite /bi_intuitionistically_if. destruct p; apply _. Qed.

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.
  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.

Big op
  Global 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.
  Global 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.
  Global 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.

  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.
  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.
  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.
  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.

  Global 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.
  Global 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.
  Global 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.

  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.
  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.
  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.
  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.

  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.
  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.
  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.
  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.

  Global 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.
  Global 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.
  Global 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.
  Global 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.

BUpd
  Lemma monPred_at_bupd `{!BiBUpd PROP} i P : (|==> P) i ⊣⊢ |==> P i.
  Proof. by rewrite monPred_bupd_unseal. Qed.

  Global Instance bupd_objective `{!BiBUpd PROP} P `{!Objective P} :
    Objective (|==> P).
  Proof. intros ??. by rewrite !monPred_at_bupd objective_at. Qed.

Later
  Global Instance monPred_at_timeless P i : Timeless P → Timeless (P i).
  Proof. move ⇒ [] /(_ i). rewrite /Timeless /bi_except_0. by unseal. Qed.
  Global Instance monPred_in_timeless i0 : Timeless (@monPred_in I PROP i0).
  Proof. split ⇒ ? /=. rewrite /bi_except_0. unseal. apply timeless, _. Qed.
  Global 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.
  Global 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.

  Lemma monPred_at_later i P : (▷ P) i ⊣⊢ ▷ P i.
  Proof. by unseal. Qed.
  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.
  Lemma monPred_at_except_0 i P : (◇ P) i ⊣⊢ ◇ P i.
  Proof. rewrite /bi_except_0. by unseal. Qed.

  Global Instance later_objective P `{!Objective P} : Objective (▷ P).
  Proof. intros ??. unseal. by rewrite objective_at. Qed.
  Global Instance laterN_objective P `{!Objective P} n : Objective (▷^n P).
  Proof. induction n; apply _. Qed.
  Global Instance except0_objective P `{!Objective P} : Objective (◇ P).
  Proof. rewrite /bi_except_0. apply _. Qed.

Sbi
  Section sbi.
    Context `{!Sbi PROP}.

    Lemma monPred_si_pure_unfold :
      @si_pure monPredI _ = λ Pi, ⎡ <si_pure> Pi ⎤%I.
    Proof. by unseal. Qed.
    Lemma monPred_si_emp_valid_unfold :
      @si_emp_valid monPredI _ = λ P, (<si_emp_valid> ∀ i, P i)%I.
    Proof. by unseal. Qed.

    Global Instance si_pure_objective Pi :
      Objective (PROP:=PROP) (I:=I) (<si_pure> Pi).
    Proof. rewrite monPred_si_pure_unfold. apply _. Qed.

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.

    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.

    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.

    Global Instance internal_eq_objective {A : ofe} (x y : A) :
      @Objective I PROP (x ≡ y).
    Proof. intros ??. rewrite monPred_internal_eq_unfold. by unseal. Qed.

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.

    Global Instance fupd_objective E1 E2 P `{!Objective P} `{!BiFUpd PROP} :
      Objective (|={E1,E2}=> P).
    Proof. intros ??. by rewrite !monPred_at_fupd objective_at. Qed.

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.

    Global Instance monPred_at_plain P i : Plain P → Plain (P i).
    Proof. move ⇒ [] /(_ i). rewrite /Plain monPred_at_plainly bi.forall_elim //. Qed.

    Global Instance plainly_objective P : Objective (■ P).
    Proof. rewrite /plainly. apply _. Qed.
    Global Instance plainly_if_objective P p `{!Objective P} :
      Objective (■?p P).
    Proof. rewrite /plainly_if. destruct p; apply _. Qed.

    Global Instance monPred_objectively_plain P :
      Plain P → Plain (<obj> P).
    Proof. rewrite monPred_objectively_unfold. apply _. Qed.
    Global Instance monPred_subjectively_plain P :
      Plain P → Plain (<subj> P).
    Proof. rewrite monPred_subjectively_unfold. apply _. Qed.
  End sbi.
End bi_facts.