Library iris.proofmode.monpred

From iris.bi Require Export monpred.
From iris.bi Require Import plainly.
From iris.proofmode Require Import tactics modality_instances.

Class MakeMonPredAt {I : biIndex} {PROP : bi} (i : I)
      (P : monPred I PROP) (š“Ÿ : PROP) :=
  make_monPred_at : P i āŠ£āŠ¢ š“Ÿ.
Arguments MakeMonPredAt {_ _} _ _%I _%I.
Since MakeMonPredAt is used by AsEmpValid to import lemmas into the proof mode, the index I and BI PROP often contain evars. Hence, it is important to use the mode ! also for the first two arguments.
Hint Mode MakeMonPredAt ! ! - ! - : typeclass_instances.

Class IsBiIndexRel {I : biIndex} (i j : I) := is_bi_index_rel : i āŠ‘ j.
Hint Mode IsBiIndexRel + - - : typeclass_instances.
Instance is_bi_index_rel_refl {I : biIndex} (i : I) : IsBiIndexRel i i | 0.
Proof. by rewrite /IsBiIndexRel. Qed.
Hint Extern 1 (IsBiIndexRel _ _) ā‡’ unfold IsBiIndexRel; assumption
            : typeclass_instances.

Frame š“” into the goal monPred_at P i and determine the remainder š“ . Used when framing encounters a monPred_at in the goal.
Class FrameMonPredAt {I : biIndex} {PROP : bi} (p : bool) (i : I)
      (š“” : PROP) (P : monPred I PROP) (š“  : PROP) :=
  frame_monPred_at : ā–”?p š“” āˆ— š“  -āˆ— P i.
Arguments FrameMonPredAt {_ _} _ _ _%I _%I _%I.
Hint Mode FrameMonPredAt + + + - ! ! - : typeclass_instances.

Section modalities.
  Context {I : biIndex} {PROP : bi}.

  Lemma modality_objectively_mixin :
    modality_mixin (@monPred_objectively I PROP)
      (MIEnvFilter Objective) (MIEnvFilter Objective).
  Proof.
    split; simpl; split_and?; intros;
      try match goal with H : TCDiag _ _ _ |- _ ā‡’ destruct H end;
      eauto using bi.equiv_entails_sym, objective_objectively,
        monPred_objectively_mono, monPred_objectively_and,
        monPred_objectively_sep_2 with typeclass_instances.
  Qed.
  Definition modality_objectively :=
    Modality _ modality_objectively_mixin.
End modalities.

Section bi.
Context {I : biIndex} {PROP : bi}.
Local Notation monPredI := (monPredI I PROP).
Local Notation monPred := (monPred I PROP).
Local Notation MakeMonPredAt := (@MakeMonPredAt I PROP).
Implicit Types P Q R : monPred.
Implicit Types š“Ÿ š“  š“” : PROP.
Implicit Types Ļ† : Prop.
Implicit Types i j : I.

Global Instance from_modal_objectively P :
  FromModal modality_objectively (<obj> P) (<obj> P) P | 1.
Proof. by rewrite /FromModal. Qed.
Global Instance from_modal_subjectively P :
  FromModal modality_id (<subj> P) (<subj> P) P | 1.
Proof. by rewrite /FromModal /= -monPred_subjectively_intro. Qed.

Global Instance from_modal_affinely_monPred_at `(sel : A) P Q š“  i :
  FromModal modality_affinely sel P Q ā†’ MakeMonPredAt i Q š“  ā†’
  FromModal modality_affinely sel (P i) š“  | 0.
Proof.
  rewrite /FromModal /MakeMonPredAt /==> <- <-. by rewrite monPred_at_affinely.
Qed.
Global Instance from_modal_persistently_monPred_at `(sel : A) P Q š“  i :
  FromModal modality_persistently sel P Q ā†’ MakeMonPredAt i Q š“  ā†’
  FromModal modality_persistently sel (P i) š“  | 0.
Proof.
  rewrite /FromModal /MakeMonPredAt /==> <- <-. by rewrite monPred_at_persistently.
Qed.
Global Instance from_modal_intuitionistically_monPred_at `(sel : A) P Q š“  i :
  FromModal modality_intuitionistically sel P Q ā†’ MakeMonPredAt i Q š“  ā†’
  FromModal modality_intuitionistically sel (P i) š“  | 0.
Proof.
  rewrite /FromModal /MakeMonPredAt /==> <- <-.
  by rewrite monPred_at_affinely monPred_at_persistently.
Qed.
Global Instance from_modal_id_monPred_at `(sel : A) P Q š“  i :
  FromModal modality_id sel P Q ā†’ MakeMonPredAt i Q š“  ā†’
  FromModal modality_id sel (P i) š“ .
Proof. by rewrite /FromModal /MakeMonPredAtā‡’ <- <-. Qed.

Global Instance make_monPred_at_pure Ļ† i : MakeMonPredAt i āŒœĻ†āŒ āŒœĻ†āŒ.
Proof. by rewrite /MakeMonPredAt monPred_at_pure. Qed.
Global Instance make_monPred_at_emp i : MakeMonPredAt i emp emp.
Proof. by rewrite /MakeMonPredAt monPred_at_emp. Qed.
Global Instance make_monPred_at_sep i P š“Ÿ Q š“  :
  MakeMonPredAt i P š“Ÿ ā†’ MakeMonPredAt i Q š“  ā†’
  MakeMonPredAt i (P āˆ— Q) (š“Ÿ āˆ— š“ ).
Proof. by rewrite /MakeMonPredAt monPred_at_sep=><-<-. Qed.
Global Instance make_monPred_at_and i P š“Ÿ Q š“  :
  MakeMonPredAt i P š“Ÿ ā†’ MakeMonPredAt i Q š“  ā†’
  MakeMonPredAt i (P āˆ§ Q) (š“Ÿ āˆ§ š“ ).
Proof. by rewrite /MakeMonPredAt monPred_at_and=><-<-. Qed.
Global Instance make_monPred_at_or i P š“Ÿ Q š“  :
  MakeMonPredAt i P š“Ÿ ā†’ MakeMonPredAt i Q š“  ā†’
  MakeMonPredAt i (P āˆØ Q) (š“Ÿ āˆØ š“ ).
Proof. by rewrite /MakeMonPredAt monPred_at_or=><-<-. Qed.
Global Instance make_monPred_at_forall {A} i (Ī¦ : A ā†’ monPred) (ĪØ : A ā†’ PROP) :
  (āˆ€ a, MakeMonPredAt i (Ī¦ a) (ĪØ a)) ā†’ MakeMonPredAt i (āˆ€ a, Ī¦ a) (āˆ€ a, ĪØ a).
Proof. rewrite /MakeMonPredAt monPred_at_forallā‡’H. by setoid_rewrite <- H. Qed.
Global Instance make_monPred_at_exists {A} i (Ī¦ : A ā†’ monPred) (ĪØ : A ā†’ PROP) :
  (āˆ€ a, MakeMonPredAt i (Ī¦ a) (ĪØ a)) ā†’ MakeMonPredAt i (āˆƒ a, Ī¦ a) (āˆƒ a, ĪØ a).
Proof. rewrite /MakeMonPredAt monPred_at_existā‡’H. by setoid_rewrite <- H. Qed.
Global Instance make_monPred_at_persistently i P š“Ÿ :
  MakeMonPredAt i P š“Ÿ ā†’ MakeMonPredAt i (<pers> P) (<pers> š“Ÿ).
Proof. by rewrite /MakeMonPredAt monPred_at_persistently=><-. Qed.
Global Instance make_monPred_at_affinely i P š“Ÿ :
  MakeMonPredAt i P š“Ÿ ā†’ MakeMonPredAt i (<affine> P) (<affine> š“Ÿ).
Proof. by rewrite /MakeMonPredAt monPred_at_affinely=><-. Qed.
Global Instance make_monPred_at_intuitionistically i P š“Ÿ :
  MakeMonPredAt i P š“Ÿ ā†’ MakeMonPredAt i (ā–” P) (ā–” š“Ÿ).
Proof. by rewrite /MakeMonPredAt monPred_at_intuitionistically=><-. Qed.
Global Instance make_monPred_at_absorbingly i P š“Ÿ :
  MakeMonPredAt i P š“Ÿ ā†’ MakeMonPredAt i (<absorb> P) (<absorb> š“Ÿ).
Proof. by rewrite /MakeMonPredAt monPred_at_absorbingly=><-. Qed.
Global Instance make_monPred_at_persistently_if i P š“Ÿ p :
  MakeMonPredAt i P š“Ÿ ā†’
  MakeMonPredAt i (<pers>?p P) (<pers>?p š“Ÿ).
Proof. destruct p; simpl; apply _. Qed.
Global Instance make_monPred_at_affinely_if i P š“Ÿ p :
  MakeMonPredAt i P š“Ÿ ā†’
  MakeMonPredAt i (<affine>?p P) (<affine>?p š“Ÿ).
Proof. destruct p; simpl; apply _. Qed.
Global Instance make_monPred_at_absorbingly_if i P š“Ÿ p :
  MakeMonPredAt i P š“Ÿ ā†’
  MakeMonPredAt i (<absorb>?p P) (<absorb>?p š“Ÿ).
Proof. destruct p; simpl; apply _. Qed.
Global Instance make_monPred_at_intuitionistically_if i P š“Ÿ p :
  MakeMonPredAt i P š“Ÿ ā†’
  MakeMonPredAt i (ā–”?p P) (ā–”?p š“Ÿ).
Proof. destruct p; simpl; apply _. Qed.
Global Instance make_monPred_at_embed i š“Ÿ : MakeMonPredAt i āŽ”š“ŸāŽ¤ š“Ÿ.
Proof. by rewrite /MakeMonPredAt monPred_at_embed. Qed.
Global Instance make_monPred_at_in i j : MakeMonPredAt j (monPred_in i) āŒœi āŠ‘ jāŒ.
Proof. by rewrite /MakeMonPredAt monPred_at_in. Qed.
Global Instance make_monPred_at_default i P : MakeMonPredAt i P (P i) | 100.
Proof. by rewrite /MakeMonPredAt. Qed.
Global Instance make_monPred_at_bupd `{BiBUpd PROP} i P š“Ÿ :
  MakeMonPredAt i P š“Ÿ ā†’ MakeMonPredAt i (|==> P)%I (|==> š“Ÿ)%I.
Proof. by rewrite /MakeMonPredAt monPred_at_bupdā‡’ <-. Qed.

Global Instance from_assumption_make_monPred_at_l p i j P š“Ÿ :
  MakeMonPredAt i P š“Ÿ ā†’ IsBiIndexRel j i ā†’ KnownLFromAssumption p (P j) š“Ÿ.
Proof.
  rewrite /MakeMonPredAt /KnownLFromAssumption /FromAssumption /IsBiIndexRel=><- ā†’.
  apply bi.intuitionistically_if_elim.
Qed.
Global Instance from_assumption_make_monPred_at_r p i j P š“Ÿ :
  MakeMonPredAt i P š“Ÿ ā†’ IsBiIndexRel i j ā†’ KnownRFromAssumption p š“Ÿ (P j).
Proof.
  rewrite /MakeMonPredAt /KnownRFromAssumption /FromAssumption /IsBiIndexRel=><- ā†’.
  apply bi.intuitionistically_if_elim.
Qed.

Global Instance from_assumption_make_monPred_objectively P Q :
  FromAssumption p P Q ā†’ KnownLFromAssumption p (<obj> P) Q.
Proof.
  intros ?.
  by rewrite /KnownLFromAssumption /FromAssumption monPred_objectively_elim.
Qed.
Global Instance from_assumption_make_monPred_subjectively P Q :
  FromAssumption p P Q ā†’ KnownRFromAssumption p P (<subj> Q).
Proof.
  intros ?.
  by rewrite /KnownRFromAssumption /FromAssumption -monPred_subjectively_intro.
Qed.

Global Instance as_emp_valid_monPred_at Ļ† P (Ī¦ : I ā†’ PROP) :
  AsEmpValid0 Ļ† P ā†’ (āˆ€ i, MakeMonPredAt i P (Ī¦ i)) ā†’ AsEmpValid Ļ† (āˆ€ i, Ī¦ i) | 100.
Proof.
  rewrite /MakeMonPredAt /AsEmpValid0 /AsEmpValid /bi_emp_validā‡’ ā†’ EQ.
  setoid_rewrite <-EQ. split.
  - move=>[H]. apply bi.forall_introā‡’i. rewrite -H. by rewrite monPred_at_emp.
  - moveā‡’HP. splitā‡’i. rewrite monPred_at_emp HP bi.forall_elim //.
Qed.
Global Instance as_emp_valid_monPred_at_wand Ļ† P Q (Ī¦ ĪØ : I ā†’ PROP) :
  AsEmpValid0 Ļ† (P -āˆ— Q) ā†’
  (āˆ€ i, MakeMonPredAt i P (Ī¦ i)) ā†’ (āˆ€ i, MakeMonPredAt i Q (ĪØ i)) ā†’
  AsEmpValid Ļ† (āˆ€ i, Ī¦ i -āˆ— ĪØ i).
Proof.
  rewrite /AsEmpValid0 /AsEmpValid /MakeMonPredAt. intros ā†’ EQ1 EQ2.
  setoid_rewrite <-EQ1. setoid_rewrite <-EQ2. split.
  - move=>/bi.wand_entails HP. setoid_rewrite HP. by iIntros (i) "$".
  - moveā‡’HP. apply bi.entails_wand. splitā‡’i. iIntros "H". by iApply HP.
Qed.
Global Instance as_emp_valid_monPred_at_equiv Ļ† P Q (Ī¦ ĪØ : I ā†’ PROP) :
  AsEmpValid0 Ļ† (P āˆ—-āˆ— Q) ā†’
  (āˆ€ i, MakeMonPredAt i P (Ī¦ i)) ā†’ (āˆ€ i, MakeMonPredAt i Q (ĪØ i)) ā†’
  AsEmpValid Ļ† (āˆ€ i, Ī¦ i āˆ—-āˆ— ĪØ i).
Proof.
  rewrite /AsEmpValid0 /AsEmpValid /MakeMonPredAt. intros ā†’ EQ1 EQ2.
  setoid_rewrite <-EQ1. setoid_rewrite <-EQ2. split.
  - move=>/bi.wand_iff_equiv HP. setoid_rewrite HP. iIntros. iSplit; iIntros "$".
  - moveā‡’HP. apply bi.equiv_wand_iff. splitā‡’i. by iSplit; iIntros; iApply HP.
Qed.

Global Instance into_pure_monPred_at P Ļ† i : IntoPure P Ļ† ā†’ IntoPure (P i) Ļ†.
Proof. rewrite /IntoPure=>->. by rewrite monPred_at_pure. Qed.
Global Instance from_pure_monPred_at a P Ļ† i : FromPure a P Ļ† ā†’ FromPure a (P i) Ļ†.
Proof. rewrite /FromPure=><-. by rewrite monPred_at_affinely_if monPred_at_pure. Qed.
Global Instance into_pure_monPred_in i j : @IntoPure PROP (monPred_in i j) (i āŠ‘ j).
Proof. by rewrite /IntoPure monPred_at_in. Qed.
Global Instance from_pure_monPred_in i j : @FromPure PROP false (monPred_in i j) (i āŠ‘ j).
Proof. by rewrite /FromPure monPred_at_in. Qed.

Global Instance into_persistent_monPred_at p P Q š“  i :
  IntoPersistent p P Q ā†’ MakeMonPredAt i Q š“  ā†’ IntoPersistent p (P i) š“  | 0.
Proof.
  rewrite /IntoPersistent /MakeMonPredAt =>-[/(_ i) ?] <-.
  by rewrite -monPred_at_persistently -monPred_at_persistently_if.
Qed.

Lemma into_wand_monPred_at_unknown_unknown p q R P š“Ÿ Q š“  i :
  IntoWand p q R P Q ā†’ MakeMonPredAt i P š“Ÿ ā†’ MakeMonPredAt i Q š“  ā†’
  IntoWand p q (R i) š“Ÿ š“ .
Proof.
  rewrite /IntoWand /MakeMonPredAt /bi_affinely_if /bi_persistently_if.
  destruct p, qā‡’ /bi.wand_elim_l' [/(_ i) H] <- <-; apply bi.wand_intro_r;
  revert H; by rewrite monPred_at_sep ?monPred_at_affinely ?monPred_at_persistently.
Qed.
Lemma into_wand_monPred_at_unknown_known p q R P š“Ÿ Q i j :
  IsBiIndexRel i j ā†’ IntoWand p q R P Q ā†’
  MakeMonPredAt j P š“Ÿ ā†’ IntoWand p q (R i) š“Ÿ (Q j).
Proof.
  rewrite /IntoWand /IsBiIndexRel /MakeMonPredAt=>-> ? ?.
  eapply into_wand_monPred_at_unknown_unknown=>//. apply _.
Qed.
Lemma into_wand_monPred_at_known_unknown_le p q R P Q š“  i j :
  IsBiIndexRel i j ā†’ IntoWand p q R P Q ā†’
  MakeMonPredAt j Q š“  ā†’ IntoWand p q (R i) (P j) š“ .
Proof.
  rewrite /IntoWand /IsBiIndexRel /MakeMonPredAt=>-> ? ?.
  eapply into_wand_monPred_at_unknown_unknown=>//. apply _.
Qed.
Lemma into_wand_monPred_at_known_unknown_ge p q R P Q š“  i j :
  IsBiIndexRel i j ā†’ IntoWand p q R P Q ā†’
  MakeMonPredAt j Q š“  ā†’ IntoWand p q (R j) (P i) š“ .
Proof.
  rewrite /IntoWand /IsBiIndexRel /MakeMonPredAt=>-> ? ?.
  eapply into_wand_monPred_at_unknown_unknown=>//. apply _.
Qed.

Global Instance into_wand_wand'_monPred p q P Q š“Ÿ š“  i :
  IntoWand' p q ((P -āˆ— Q) i) š“Ÿ š“  ā†’ IntoWand p q ((P -āˆ— Q) i) š“Ÿ š“  | 100.
Proof. done. Qed.
Global Instance into_wand_impl'_monPred p q P Q š“Ÿ š“  i :
  IntoWand' p q ((P ā†’ Q) i) š“Ÿ š“  ā†’ IntoWand p q ((P ā†’ Q) i) š“Ÿ š“  | 100.
Proof. done. Qed.

Global Instance from_forall_monPred_at_wand P Q (Ī¦ ĪØ : I ā†’ PROP) i :
  (āˆ€ j, MakeMonPredAt j P (Ī¦ j)) ā†’ (āˆ€ j, MakeMonPredAt j Q (ĪØ j)) ā†’
  FromForall ((P -āˆ— Q) i)%I (Ī» j, āŒœi āŠ‘ jāŒ ā†’ Ī¦ j -āˆ— ĪØ j)%I.
Proof.
  rewrite /FromForall /MakeMonPredAt monPred_at_wandā‡’ H1 H2. do 2 f_equiv.
  by rewrite H1 H2.
Qed.
Global Instance from_forall_monPred_at_impl P Q (Ī¦ ĪØ : I ā†’ PROP) i :
  (āˆ€ j, MakeMonPredAt j P (Ī¦ j)) ā†’ (āˆ€ j, MakeMonPredAt j Q (ĪØ j)) ā†’
  FromForall ((P ā†’ Q) i)%I (Ī» j, āŒœi āŠ‘ jāŒ ā†’ Ī¦ j ā†’ ĪØ j)%I.
Proof.
  rewrite /FromForall /MakeMonPredAt monPred_at_implā‡’ H1 H2. do 2 f_equiv.
  by rewrite H1 H2 bi.pure_impl_forall.
Qed.

Global Instance into_forall_monPred_at_index P i :
  IntoForall (P i) (Ī» j, āŒœi āŠ‘ jāŒ ā†’ P j)%I | 100.
Proof.
  rewrite /IntoForall. setoid_rewrite bi.pure_impl_forall.
  do 2 apply bi.forall_intro=>?. by f_equiv.
Qed.

Global Instance from_and_monPred_at P Q1 š“ 1 Q2 š“ 2 i :
  FromAnd P Q1 Q2 ā†’ MakeMonPredAt i Q1 š“ 1 ā†’ MakeMonPredAt i Q2 š“ 2 ā†’
  FromAnd (P i) š“ 1 š“ 2.
Proof.
  rewrite /FromAnd /MakeMonPredAt /MakeMonPredAtā‡’ <- <- <-.
  by rewrite monPred_at_and.
Qed.
Global Instance into_and_monPred_at p P Q1 š“ 1 Q2 š“ 2 i :
  IntoAnd p P Q1 Q2 ā†’ MakeMonPredAt i Q1 š“ 1 ā†’ MakeMonPredAt i Q2 š“ 2 ā†’
  IntoAnd p (P i) š“ 1 š“ 2.
Proof.
  rewrite /IntoAnd /MakeMonPredAt /bi_affinely_if /bi_persistently_if.
  destruct p=>-[/(_ i) H] <- <-; revert H;
  by rewrite ?monPred_at_affinely ?monPred_at_persistently monPred_at_and.
Qed.

Global Instance from_sep_monPred_at P Q1 š“ 1 Q2 š“ 2 i :
  FromSep P Q1 Q2 ā†’ MakeMonPredAt i Q1 š“ 1 ā†’ MakeMonPredAt i Q2 š“ 2 ā†’
  FromSep (P i) š“ 1 š“ 2.
Proof. rewrite /FromSep /MakeMonPredAtā‡’ <- <- <-. by rewrite monPred_at_sep. Qed.
Global Instance into_sep_monPred_at P Q1 š“ 1 Q2 š“ 2 i :
  IntoSep P Q1 Q2 ā†’ MakeMonPredAt i Q1 š“ 1 ā†’ MakeMonPredAt i Q2 š“ 2 ā†’
  IntoSep (P i) š“ 1 š“ 2.
Proof. rewrite /IntoSep /MakeMonPredAtā‡’ ā†’ <- <-. by rewrite monPred_at_sep. Qed.
Global Instance from_or_monPred_at P Q1 š“ 1 Q2 š“ 2 i :
  FromOr P Q1 Q2 ā†’ MakeMonPredAt i Q1 š“ 1 ā†’ MakeMonPredAt i Q2 š“ 2 ā†’
  FromOr (P i) š“ 1 š“ 2.
Proof. rewrite /FromOr /MakeMonPredAtā‡’ <- <- <-. by rewrite monPred_at_or. Qed.
Global Instance into_or_monPred_at P Q1 š“ 1 Q2 š“ 2 i :
  IntoOr P Q1 Q2 ā†’ MakeMonPredAt i Q1 š“ 1 ā†’ MakeMonPredAt i Q2 š“ 2 ā†’
  IntoOr (P i) š“ 1 š“ 2.
Proof. rewrite /IntoOr /MakeMonPredAtā‡’ ā†’ <- <-. by rewrite monPred_at_or. Qed.

Global Instance from_exist_monPred_at {A} P (Ī¦ : A ā†’ monPred) (ĪØ : A ā†’ PROP) i :
  FromExist P Ī¦ ā†’ (āˆ€ a, MakeMonPredAt i (Ī¦ a) (ĪØ a)) ā†’ FromExist (P i) ĪØ.
Proof.
  rewrite /FromExist /MakeMonPredAt=><- H. setoid_rewrite <- H.
  by rewrite monPred_at_exist.
Qed.
Global Instance into_exist_monPred_at {A} P (Ī¦ : A ā†’ monPred) (ĪØ : A ā†’ PROP) i :
  IntoExist P Ī¦ ā†’ (āˆ€ a, MakeMonPredAt i (Ī¦ a) (ĪØ a)) ā†’ IntoExist (P i) ĪØ.
Proof.
  rewrite /IntoExist /MakeMonPredAt=>-> H. setoid_rewrite <- H.
  by rewrite monPred_at_exist.
Qed.

Global Instance from_forall_monPred_at_objectively P (Ī¦ : I ā†’ PROP) i :
  (āˆ€ i, MakeMonPredAt i P (Ī¦ i)) ā†’ FromForall ((<obj> P) i)%I Ī¦.
Proof.
  rewrite /FromForall /MakeMonPredAt monPred_at_objectivelyā‡’H. by setoid_rewrite <- H.
Qed.
Global Instance into_forall_monPred_at_objectively P (Ī¦ : I ā†’ PROP) i :
  (āˆ€ i, MakeMonPredAt i P (Ī¦ i)) ā†’ IntoForall ((<obj> P) i) Ī¦.
Proof.
  rewrite /IntoForall /MakeMonPredAt monPred_at_objectivelyā‡’H. by setoid_rewrite <- H.
Qed.

Global Instance from_exist_monPred_at_ex P (Ī¦ : I ā†’ PROP) i :
  (āˆ€ i, MakeMonPredAt i P (Ī¦ i)) ā†’ FromExist ((<subj> P) i) Ī¦.
Proof.
  rewrite /FromExist /MakeMonPredAt monPred_at_subjectivelyā‡’H. by setoid_rewrite <- H.
Qed.
Global Instance into_exist_monPred_at_ex P (Ī¦ : I ā†’ PROP) i :
  (āˆ€ i, MakeMonPredAt i P (Ī¦ i)) ā†’ IntoExist ((<subj> P) i) Ī¦.
Proof.
  rewrite /IntoExist /MakeMonPredAt monPred_at_subjectivelyā‡’H. by setoid_rewrite <- H.
Qed.

Global Instance from_forall_monPred_at {A} P (Ī¦ : A ā†’ monPred) (ĪØ : A ā†’ PROP) i :
  FromForall P Ī¦ ā†’ (āˆ€ a, MakeMonPredAt i (Ī¦ a) (ĪØ a)) ā†’ FromForall (P i) ĪØ.
Proof.
  rewrite /FromForall /MakeMonPredAt=><- H. setoid_rewrite <- H.
  by rewrite monPred_at_forall.
Qed.
Global Instance into_forall_monPred_at {A} P (Ī¦ : A ā†’ monPred) (ĪØ : A ā†’ PROP) i :
  IntoForall P Ī¦ ā†’ (āˆ€ a, MakeMonPredAt i (Ī¦ a) (ĪØ a)) ā†’ IntoForall (P i) ĪØ.
Proof.
  rewrite /IntoForall /MakeMonPredAt=>-> H. setoid_rewrite <- H.
  by rewrite monPred_at_forall.
Qed.

Global Instance frame_monPred_at_enter p i š“” P š“  :
  FrameMonPredAt p i š“” P š“  ā†’ Frame p š“” (P i) š“ .
Proof. intros. done. Qed.
Global Instance frame_monPred_at_here p P i j :
  IsBiIndexRel i j ā†’ FrameMonPredAt p j (P i) P emp | 0.
Proof.
  rewrite /FrameMonPredAt /IsBiIndexRel right_id bi.intuitionistically_if_elimā‡’ ā†’ //.
Qed.

Global Instance frame_monPred_at_embed p š“” š“  š“Ÿ i :
  Frame p š“” š“Ÿ š“  ā†’ FrameMonPredAt p i š“” (embed (B:=monPredI) š“Ÿ) š“ .
Proof. rewrite /Frame /FrameMonPredAtā‡’ ā†’. by rewrite monPred_at_embed. Qed.
Global Instance frame_monPred_at_sep p P Q š“” š“  i :
  Frame p š“” (P i āˆ— Q i) š“  ā†’ FrameMonPredAt p i š“” (P āˆ— Q) š“ .
Proof. rewrite /Frame /FrameMonPredAtā‡’ ā†’. by rewrite monPred_at_sep. Qed.
Global Instance frame_monPred_at_and p P Q š“” š“  i :
  Frame p š“” (P i āˆ§ Q i) š“  ā†’ FrameMonPredAt p i š“” (P āˆ§ Q) š“ .
Proof. rewrite /Frame /FrameMonPredAtā‡’ ā†’. by rewrite monPred_at_and. Qed.
Global Instance frame_monPred_at_or p P Q š“” š“  i :
  Frame p š“” (P i āˆØ Q i) š“  ā†’ FrameMonPredAt p i š“” (P āˆØ Q) š“ .
Proof. rewrite /Frame /FrameMonPredAtā‡’ ā†’. by rewrite monPred_at_or. Qed.
Global Instance frame_monPred_at_wand p P R Q1 Q2 i j :
  IsBiIndexRel i j ā†’
  Frame p R Q1 Q2 ā†’
  FrameMonPredAt p j (R i) (P -āˆ— Q1) ((P -āˆ— Q2) i).
Proof.
  rewrite /Frame /FrameMonPredAt=>-> Hframe.
  rewrite -monPred_at_intuitionistically_if -monPred_at_sep. apply monPred_in_entails.
  change ((ā–”?p R āˆ— (P -āˆ— Q2)) -āˆ— P -āˆ— Q1). apply bi.wand_intro_r.
  rewrite -assoc bi.wand_elim_l. done.
Qed.
Global Instance frame_monPred_at_impl P R Q1 Q2 i j :
  IsBiIndexRel i j ā†’
  Frame true R Q1 Q2 ā†’
  FrameMonPredAt true j (R i) (P ā†’ Q1) ((P ā†’ Q2) i).
Proof.
  rewrite /Frame /FrameMonPredAt=>-> Hframe.
  rewrite -monPred_at_intuitionistically_if -monPred_at_sep. apply monPred_in_entails.
  change ((ā–” R āˆ— (P ā†’ Q2)) -āˆ— P ā†’ Q1).
  rewrite -bi.persistently_and_intuitionistically_sep_l. apply bi.impl_intro_r.
  rewrite -assoc bi.impl_elim_l bi.persistently_and_intuitionistically_sep_l. done.
Qed.
Global Instance frame_monPred_at_forall {X : Type} p (ĪØ : X ā†’ monPred) š“” š“  i :
  Frame p š“” (āˆ€ x, ĪØ x i) š“  ā†’ FrameMonPredAt p i š“” (āˆ€ x, ĪØ x) š“ .
Proof. rewrite /Frame /FrameMonPredAtā‡’ ā†’. by rewrite monPred_at_forall. Qed.
Global Instance frame_monPred_at_exist {X : Type} p (ĪØ : X ā†’ monPred) š“” š“  i :
  Frame p š“” (āˆƒ x, ĪØ x i) š“  ā†’ FrameMonPredAt p i š“” (āˆƒ x, ĪØ x) š“ .
Proof. rewrite /Frame /FrameMonPredAtā‡’ ā†’. by rewrite monPred_at_exist. Qed.

Global Instance frame_monPred_at_absorbingly p P š“” š“  i :
  Frame p š“” (<absorb> P i) š“  ā†’ FrameMonPredAt p i š“” (<absorb> P) š“ .
Proof. rewrite /Frame /FrameMonPredAtā‡’ ā†’. by rewrite monPred_at_absorbingly. Qed.
Global Instance frame_monPred_at_affinely p P š“” š“  i :
  Frame p š“” (<affine> P i) š“  ā†’ FrameMonPredAt p i š“” (<affine> P) š“ .
Proof. rewrite /Frame /FrameMonPredAtā‡’ ā†’. by rewrite monPred_at_affinely. Qed.
Global Instance frame_monPred_at_persistently p P š“” š“  i :
  Frame p š“” (<pers> P i) š“  ā†’ FrameMonPredAt p i š“” (<pers> P) š“ .
Proof. rewrite /Frame /FrameMonPredAtā‡’ ā†’. by rewrite monPred_at_persistently. Qed.
Global Instance frame_monPred_at_intuitionistically p P š“” š“  i :
  Frame p š“” (ā–” P i) š“  ā†’ FrameMonPredAt p i š“” (ā–” P) š“ .
Proof. rewrite /Frame /FrameMonPredAtā‡’ ā†’. by rewrite monPred_at_intuitionistically. Qed.
Global Instance frame_monPred_at_objectively p P š“” š“  i :
  Frame p š“” (āˆ€ i, P i) š“  ā†’ FrameMonPredAt p i š“” (<obj> P) š“ .
Proof. rewrite /Frame /FrameMonPredAtā‡’ ā†’. by rewrite monPred_at_objectively. Qed.
Global Instance frame_monPred_at_subjectively p P š“” š“  i :
  Frame p š“” (āˆƒ i, P i) š“  ā†’ FrameMonPredAt p i š“” (<subj> P) š“ .
Proof. rewrite /Frame /FrameMonPredAtā‡’ ā†’. by rewrite monPred_at_subjectively. Qed.
Global Instance frame_monPred_at_bupd `{BiBUpd PROP} p P š“” š“  i :
  Frame p š“” (|==> P i) š“  ā†’ FrameMonPredAt p i š“” (|==> P) š“ .
Proof. rewrite /Frame /FrameMonPredAtā‡’ ā†’. by rewrite monPred_at_bupd. Qed.

Global Instance into_embed_objective P :
  Objective P ā†’ IntoEmbed P (āˆ€ i, P i).
Proof.
  rewrite /IntoEmbedā‡’ ?.
  by rewrite {1}(objective_objectively P) monPred_objectively_unfold.
Qed.

Global Instance elim_modal_at_bupd_goal `{BiBUpd PROP} Ļ† p p' š“Ÿ š“Ÿ' Q Q' i :
  ElimModal Ļ† p p' š“Ÿ š“Ÿ' (|==> Q i) (|==> Q' i) ā†’
  ElimModal Ļ† p p' š“Ÿ š“Ÿ' ((|==> Q) i) ((|==> Q') i).
Proof. by rewrite /ElimModal !monPred_at_bupd. Qed.
Global Instance elim_modal_at_bupd_hyp `{BiBUpd PROP} Ļ† p p' P š“Ÿ š“Ÿ' š“  š“ ' i:
  MakeMonPredAt i P š“Ÿ ā†’
  ElimModal Ļ† p p' (|==> š“Ÿ) š“Ÿ' š“  š“ ' ā†’
  ElimModal Ļ† p p' ((|==> P) i) š“Ÿ' š“  š“ '.
Proof. by rewrite /MakeMonPredAt /ElimModal monPred_at_bupd=><-. Qed.
Global Instance elim_modal_at Ļ† p p' š“Ÿ š“Ÿ' P P' V:
  ElimModal Ļ† p p' āŽ”š“ŸāŽ¤ āŽ”š“Ÿ'āŽ¤ P P' ā†’ ElimModal Ļ† p p' š“Ÿ š“Ÿ' (P V) (P' V).
Proof.
  rewrite /ElimModal -!embed_intuitionistically_if.
  iIntros (HH HĻ†) "[? HP]". iApply HH; [done|]. iFrame. iIntros (? <-) "?".
  by iApply "HP".
Qed.

Global Instance add_modal_at_bupd_goal `{BiBUpd PROP} Ļ† š“Ÿ š“Ÿ' Q i :
  AddModal š“Ÿ š“Ÿ' (|==> Q i)%I ā†’ AddModal š“Ÿ š“Ÿ' ((|==> Q) i).
Proof. by rewrite /AddModal !monPred_at_bupd. Qed.
End bi.

Hint Extern 3 (IntoWand _ _ (monPred_at _ _) ?P ?Q) ā‡’
     is_evar P; is_evar Q;
     eapply @into_wand_monPred_at_unknown_unknown
     : typeclass_instances.
Hint Extern 2 (IntoWand _ _ (monPred_at _ _) ?P (monPred_at ?Q _)) ā‡’
     eapply @into_wand_monPred_at_unknown_known
     : typeclass_instances.
Hint Extern 2 (IntoWand _ _ (monPred_at _ _) (monPred_at ?P _) ?Q) ā‡’
     eapply @into_wand_monPred_at_known_unknown_le
     : typeclass_instances.
Hint Extern 2 (IntoWand _ _ (monPred_at _ _) (monPred_at ?P _) ?Q) ā‡’
     eapply @into_wand_monPred_at_known_unknown_ge
     : typeclass_instances.

Section sbi.
Context {I : biIndex} {PROP : sbi}.
Local Notation monPred := (monPred I PROP).
Implicit Types P Q R : monPred.
Implicit Types š“Ÿ š“  š“” : PROP.
Implicit Types Ļ† : Prop.
Implicit Types i j : I.

Global Instance from_forall_monPred_at_plainly `{BiPlainly PROP} i P Ī¦ :
  (āˆ€ i, MakeMonPredAt i P (Ī¦ i)) ā†’
  FromForall ((ā–  P) i) (Ī» j, ā–  (Ī¦ j))%I.
Proof.
  rewrite /FromForall /MakeMonPredAtā‡’HPĪ¦. rewrite monPred_at_plainly.
  by setoid_rewrite HPĪ¦.
Qed.
Global Instance into_forall_monPred_at_plainly `{BiPlainly PROP} i P Ī¦ :
  (āˆ€ i, MakeMonPredAt i P (Ī¦ i)) ā†’
  IntoForall ((ā–  P) i) (Ī» j, ā–  (Ī¦ j))%I.
Proof.
  rewrite /IntoForall /MakeMonPredAtā‡’HPĪ¦. rewrite monPred_at_plainly.
  by setoid_rewrite HPĪ¦.
Qed.

Global Instance is_except_0_monPred_at i P :
  IsExcept0 P ā†’ IsExcept0 (P i).
Proof. rewrite /IsExcept0=>- [/(_ i)]. by rewrite monPred_at_except_0. Qed.

Global Instance make_monPred_at_internal_eq {A : ofeT} (x y : A) i :
  @MakeMonPredAt I PROP i (x ā‰” y) (x ā‰” y).
Proof. by rewrite /MakeMonPredAt monPred_at_internal_eq. Qed.
Global Instance make_monPred_at_except_0 i P š“  :
  MakeMonPredAt i P š“  ā†’ MakeMonPredAt i (ā—‡ P)%I (ā—‡ š“ )%I.
Proof. by rewrite /MakeMonPredAt monPred_at_except_0=><-. Qed.
Global Instance make_monPred_at_later i P š“  :
  MakeMonPredAt i P š“  ā†’ MakeMonPredAt i (ā–· P)%I (ā–· š“ )%I.
Proof. by rewrite /MakeMonPredAt monPred_at_later=><-. Qed.
Global Instance make_monPred_at_laterN i n P š“  :
  MakeMonPredAt i P š“  ā†’ MakeMonPredAt i (ā–·^n P)%I (ā–·^n š“ )%I.
Proof. rewrite /MakeMonPredAtā‡’ <-. elim n=>//= ? <-. by rewrite monPred_at_later. Qed.
Global Instance make_monPred_at_fupd `{BiFUpd PROP} i E1 E2 P š“Ÿ :
  MakeMonPredAt i P š“Ÿ ā†’ MakeMonPredAt i (|={E1,E2}=> P)%I (|={E1,E2}=> š“Ÿ)%I.
Proof. by rewrite /MakeMonPredAt monPred_at_fupdā‡’ <-. Qed.

Global Instance into_internal_eq_monPred_at {A : ofeT} (x y : A) P i :
  IntoInternalEq P x y ā†’ IntoInternalEq (P i) x y.
Proof. rewrite /IntoInternalEqā‡’ ā†’. by rewrite monPred_at_internal_eq. Qed.

Global Instance into_except_0_monPred_at_fwd i P Q š“  :
  IntoExcept0 P Q ā†’ MakeMonPredAt i Q š“  ā†’ IntoExcept0 (P i) š“ .
Proof. rewrite /IntoExcept0 /MakeMonPredAtā‡’ ā†’ <-. by rewrite monPred_at_except_0. Qed.
Global Instance into_except_0_monPred_at_bwd i P š“Ÿ Q :
  IntoExcept0 P Q ā†’ MakeMonPredAt i P š“Ÿ ā†’ IntoExcept0 š“Ÿ (Q i).
Proof. rewrite /IntoExcept0 /MakeMonPredAtā‡’ H <-. by rewrite H monPred_at_except_0. Qed.

Global Instance maybe_into_later_monPred_at i n P Q š“  :
  IntoLaterN false n P Q ā†’ MakeMonPredAt i Q š“  ā†’
  IntoLaterN false n (P i) š“ .
Proof.
  rewrite /IntoLaterN /MaybeIntoLaterN /MakeMonPredAtā‡’ ā†’ <-. elim n=>//= ? <-.
  by rewrite monPred_at_later.
Qed.
Global Instance from_later_monPred_at i `(sel : A) n P Q š“  :
  FromModal (modality_laterN n) sel P Q ā†’ MakeMonPredAt i Q š“  ā†’
  FromModal (modality_laterN n) sel (P i) š“ .
Proof.
  rewrite /FromModal /MakeMonPredAtā‡’ <- <-. elim n=>//= ? ā†’.
  by rewrite monPred_at_later.
Qed.

Global Instance frame_monPred_at_later p P š“” š“  i :
  Frame p š“” (ā–· P i) š“  ā†’ FrameMonPredAt p i š“” (ā–· P) š“ .
Proof. rewrite /Frame /FrameMonPredAtā‡’ ā†’. by rewrite monPred_at_later. Qed.
Global Instance frame_monPred_at_laterN p n P š“” š“  i :
  Frame p š“” (ā–·^n P i) š“  ā†’ FrameMonPredAt p i š“” (ā–·^n P) š“ .
Proof. rewrite /Frame /FrameMonPredAtā‡’ ā†’. by rewrite monPred_at_laterN. Qed.
Global Instance frame_monPred_at_fupd `{BiFUpd PROP} E1 E2 p P š“” š“  i :
  Frame p š“” (|={E1,E2}=> P i) š“  ā†’ FrameMonPredAt p i š“” (|={E1,E2}=> P) š“ .
Proof. rewrite /Frame /FrameMonPredAtā‡’ ā†’. by rewrite monPred_at_fupd. Qed.

Global Instance elim_modal_at_fupd_goal `{BiFUpd PROP} Ļ† p p' E1 E2 E3 š“Ÿ š“Ÿ' Q Q' i :
  ElimModal Ļ† p p' š“Ÿ š“Ÿ' (|={E1,E3}=> Q i) (|={E2,E3}=> Q' i) ā†’
  ElimModal Ļ† p p' š“Ÿ š“Ÿ' ((|={E1,E3}=> Q) i) ((|={E2,E3}=> Q') i).
Proof. by rewrite /ElimModal !monPred_at_fupd. Qed.
Global Instance elim_modal_at_fupd_hyp `{BiFUpd PROP} Ļ† p p' E1 E2 P š“Ÿ š“Ÿ' š“  š“ ' i :
  MakeMonPredAt i P š“Ÿ ā†’
  ElimModal Ļ† p p' (|={E1,E2}=> š“Ÿ) š“Ÿ' š“  š“ ' ā†’
  ElimModal Ļ† p p' ((|={E1,E2}=> P) i) š“Ÿ' š“  š“ '.
Proof. by rewrite /MakeMonPredAt /ElimModal monPred_at_fupd=><-. Qed.

Global Instance elim_acc_at_None `{BiFUpd PROP} {X} E1 E2 E3 E4 Ī± Ī±' Ī² Ī²' P P'x V:
  (āˆ€ x, MakeEmbed (Ī± x) (Ī±' x)) ā†’ (āˆ€ x, MakeEmbed (Ī² x) (Ī²' x)) ā†’
  ElimAcc (X:=X) (fupd E1 E2) (fupd E3 E4) Ī±' Ī²' (Ī» _, None) P P'x ā†’
  ElimAcc (X:=X) (fupd E1 E2) (fupd E3 E4) Ī± Ī² (Ī» _, None) (P V) (Ī» x, P'x x V).
Proof.
  rewrite /ElimAcc /MakeEmbed. iIntros (HĪ± HĪ² HEA) "Hinner Hacc".
  iApply (HEA with "[Hinner]").
  - iIntros (x). iSpecialize ("Hinner" $! x). rewrite -HĪ±. by iIntros (? <-).
  - iMod "Hacc". iDestruct "Hacc" as (x) "[HĪ± Hclose]". iModIntro. iExists x.
    rewrite -HĪ± -HĪ². iFrame. iIntros (? _) "HĪ²". by iApply "Hclose".
Qed.
Global Instance elim_acc_at_Some `{BiFUpd PROP} {X} E1 E2 E3 E4 Ī± Ī±' Ī² Ī²' Ī³ Ī³' P P'x V:
  (āˆ€ x, MakeEmbed (Ī± x) (Ī±' x)) ā†’
  (āˆ€ x, MakeEmbed (Ī² x) (Ī²' x)) ā†’
  (āˆ€ x, MakeEmbed (Ī³ x) (Ī³' x)) ā†’
  ElimAcc (X:=X) (fupd E1 E2) (fupd E3 E4) Ī±' Ī²' (Ī» x, Some (Ī³' x)) P P'x ā†’
  ElimAcc (X:=X) (fupd E1 E2) (fupd E3 E4) Ī± Ī² (Ī» x, Some (Ī³ x)) (P V) (Ī» x, P'x x V).
Proof.
  rewrite /ElimAcc /MakeEmbed. iIntros (HĪ± HĪ² HĪ³ HEA) "Hinner Hacc".
  iApply (HEA with "[Hinner]").
  - iIntros (x). iSpecialize ("Hinner" $! x). rewrite -HĪ±. by iIntros (? <-).
  - iMod "Hacc". iDestruct "Hacc" as (x) "[HĪ± Hclose]". iModIntro. iExists x.
    rewrite -HĪ± -HĪ² -HĪ³. iFrame. iIntros (? _) "HĪ² /=". by iApply "Hclose".
Qed.

Global Instance add_modal_at_fupd_goal `{BiFUpd PROP} E1 E2 š“Ÿ š“Ÿ' Q i :
  AddModal š“Ÿ š“Ÿ' (|={E1,E2}=> Q i) ā†’ AddModal š“Ÿ š“Ÿ' ((|={E1,E2}=> Q) i).
Proof. by rewrite /AddModal !monPred_at_fupd. Qed.

Global Instance elim_inv_embed_with_close {X : Type} Ļ†
       š“Ÿinv š“Ÿin (š“Ÿout š“Ÿclose : X ā†’ PROP)
       Pin (Pout Pclose : X ā†’ monPred)
       Q Q' :
  (āˆ€ i, ElimInv Ļ† š“Ÿinv š“Ÿin š“Ÿout (Some š“Ÿclose) (Q i) (Ī» _, Q' i)) ā†’
  MakeEmbed š“Ÿin Pin ā†’ (āˆ€ x, MakeEmbed (š“Ÿout x) (Pout x)) ā†’
  (āˆ€ x, MakeEmbed (š“Ÿclose x) (Pclose x)) ā†’
  ElimInv (X:=X) Ļ† āŽ”š“ŸinvāŽ¤ Pin Pout (Some Pclose) Q (Ī» _, Q').
Proof.
  rewrite /MakeEmbed /ElimInvā‡’H <- Hout Hclose ?. iStartProof PROP.
  setoid_rewrite <-Hout. setoid_rewrite <-Hclose.
  iIntros (?) "(?&?&HQ')". iApply H; [done|]. iFrame. iIntros (x) "?". by iApply "HQ'".
Qed.
Global Instance elim_inv_embed_without_close {X : Type}
       Ļ† š“Ÿinv š“Ÿin (š“Ÿout : X ā†’ PROP) Pin (Pout : X ā†’ monPred) Q (Q' : X ā†’ monPred) :
  (āˆ€ i, ElimInv Ļ† š“Ÿinv š“Ÿin š“Ÿout None (Q i) (Ī» x, Q' x i)) ā†’
  MakeEmbed š“Ÿin Pin ā†’ (āˆ€ x, MakeEmbed (š“Ÿout x) (Pout x)) ā†’
  ElimInv (X:=X) Ļ† āŽ”š“ŸinvāŽ¤ Pin Pout None Q Q'.
Proof.
  rewrite /MakeEmbed /ElimInvā‡’H <-Hout ?. iStartProof PROP.
  setoid_rewrite <-Hout.
  iIntros (?) "(?&?&HQ')". iApply H; [done|]. iFrame. iIntros (x) "?". by iApply "HQ'".
Qed.
End sbi.