Add a bunch of proofmode instances for monPred_car and morphisms.

_CoqProject

@@ -91,6 +91,7 @@ theories/proofmode/tactics.v
 theories/proofmode/notation.v
 theories/proofmode/classes.v
 theories/proofmode/class_instances.v
+theories/proofmode/monpred.v
 theories/tests/heap_lang.v
 theories/tests/one_shot.v
 theories/tests/proofmode.v

theories/bi/derived_laws.v

@@ -2305,6 +2305,16 @@ Section bi_morphims.
   Proof. apply (ne_proper _). Qed.
   Global Instance bi_mor_mono_flip : Proper (flip (⊢) ==> flip (⊢)) bi_embedding.
   Proof. solve_proper. Qed.
+  Global Instance bi_mor_inj : Inj (≡) (≡) bi_embedding.
+  Proof.
+    intros ?? EQ. apply bi.equiv_spec, conj; apply (inj bi_embedding);
+    rewrite EQ //.
+  Qed.
+
+  Lemma bi_mor_valid (P : PROP1) : @bi_embedding PROP1 PROP2 _ P ↔ P.
+  Proof.
+    by rewrite /bi_valid -bi_mor_emp; split=>?; [apply (inj bi_embedding)|f_equiv].
+  Qed.
 
   Lemma bi_mor_forall A (Φ : A → PROP1) : ⎡∀ x, Φ x⎤ ⊣⊢ ∀ x, ⎡Φ x⎤.
   Proof.

theories/bi/interface.v

@@ -536,6 +536,7 @@ Typeclasses Opaque bi_embedding.
 Class BiMorphism (PROP1 PROP2 : bi) `{BiEmbedding PROP1 PROP2} := {
   bi_mor_ne :> NonExpansive bi_embedding;
   bi_mor_mono :> Proper ((⊢) ==> (⊢)) bi_embedding;
+  bi_mor_entails_inj :> Inj (⊢) (⊢) bi_embedding;
   bi_mor_emp : ⎡emp⎤ ⊣⊢ emp;
   bi_mor_impl_2 P Q : (⎡P⎤ → ⎡Q⎤) ⊢ ⎡P → Q⎤;
   bi_mor_forall_2 A (Φ : A → PROP1) : (∀ x, ⎡Φ x⎤) ⊢ ⎡∀ x, Φ x⎤;

theories/bi/monpred.v

@@ -465,9 +465,10 @@ Proof.
 Qed.
 
 Global Instance monPred_ipure_bi_mor :
-  @BiMorphism PROP (monPredI I PROP) bi_embedding.
+  Inhabited I → @BiMorphism PROP (monPredI I PROP) bi_embedding.
 Proof.
   split; try apply _; unseal; try done.
+  - move =>?? /= [/(_ inhabitant) ?] //.
   - split=>? /=.
     by rewrite bi.forall_elim bi.pure_impl_forall bi.forall_elim.
   - split=>? /=.
@@ -497,6 +498,6 @@ Proof.
 Qed.
 
 Global Instance monPred_ipure_sbi_mor :
-  @SbiMorphism PROP (monPredSI I PROP) bi_embedding.
+  Inhabited I → @SbiMorphism PROP (monPredSI I PROP) bi_embedding.
 Proof. split; try apply _. by unseal. Qed.
 End sbi_facts.

theories/proofmode/class_instances.v

@@ -115,6 +115,9 @@ Proof. rewrite /IntoPure=> ->. apply: plainly_elim. Qed.
 Global Instance into_pure_persistently P φ :
   IntoPure P φ → IntoPure (bi_persistently P) φ.
 Proof. rewrite /IntoPure=> ->. apply: persistently_elim. Qed.
+Global Instance into_pure_morphism `{BiMorphism PROP PROP'} P φ :
+  IntoPure P φ → IntoPure ⎡P⎤ φ.
+Proof. rewrite /IntoPure=> ->. by rewrite bi_mor_pure. Qed.
 
 (* FromPure *)
 Global Instance from_pure_pure φ : @FromPure PROP ⌜φ⌝ φ.
@@ -161,6 +164,9 @@ Global Instance from_pure_affinely P φ `{!Affine P} :
 Proof. by rewrite /FromPure affine_affinely. Qed.
 Global Instance from_pure_absorbingly P φ : FromPure P φ → FromPure (bi_absorbingly P) φ.
 Proof. rewrite /FromPure=> <-. by rewrite absorbingly_pure. Qed.
+Global Instance from_pure_morphism `{BiMorphism PROP PROP'} P φ :
+  FromPure P φ → FromPure ⎡P⎤ φ.
+Proof. rewrite /FromPure=> <-. by rewrite bi_mor_pure. Qed.
 
 (* IntoInternalEq *)
 Global Instance into_internal_eq_internal_eq {A : ofeT} (x y : A) :
@@ -178,6 +184,10 @@ Proof. rewrite /IntoInternalEq=> ->. by rewrite plainly_elim. Qed.
 Global Instance into_internal_eq_persistently {A : ofeT} (x y : A) P :
   IntoInternalEq P x y → IntoInternalEq (bi_persistently P) x y.
 Proof. rewrite /IntoInternalEq=> ->. by rewrite persistently_elim. Qed.
+Global Instance into_internal_eq_morphism
+       `{BiMorphism PROP PROP'} {A : ofeT} (x y : A) P :
+  IntoInternalEq P x y → IntoInternalEq ⎡P⎤ x y.
+Proof. rewrite /IntoInternalEq=> ->. by rewrite bi_mor_internal_eq. Qed.
 
 (* IntoPersistent *)
 Global Instance into_persistent_persistently p P Q :
@@ -189,6 +199,11 @@ Qed.
 Global Instance into_persistent_affinely p P Q :
   IntoPersistent p P Q → IntoPersistent p (bi_affinely P) Q | 0.
 Proof. rewrite /IntoPersistent /= => <-. by rewrite affinely_elim. Qed.
+Global Instance into_persistent_morphism `{BiMorphism PROP PROP'} p P Q :
+  IntoPersistent p P Q → IntoPersistent p ⎡P⎤ ⎡Q⎤ | 0.
+Proof.
+  rewrite /IntoPersistent -bi_mor_persistently -bi_mor_persistently_if=> -> //.
+Qed.
 Global Instance into_persistent_here P : IntoPersistent true P P | 1.
 Proof. by rewrite /IntoPersistent. Qed.
 Global Instance into_persistent_persistent P :
@@ -216,6 +231,12 @@ Global Instance from_always_affinely a pe pl P Q :
 Proof.
   rewrite /FromAlways /= => <-. destruct a; by rewrite /= ?affinely_idemp.
 Qed.
+Global Instance from_always_morphism `{BiMorphism PROP PROP'} a pe pl P Q :
+  FromAlways a pe pl P Q → FromAlways a pe pl ⎡P⎤ ⎡Q⎤ | 0.
+Proof.
+  rewrite /FromAlways=><-.
+  by rewrite bi_mor_affinely_if bi_mor_persistently_if bi_mor_plainly_if.
+Qed.
 
 (* IntoWand *)
 Global Instance into_wand_wand p q P Q P' :
@@ -302,6 +323,12 @@ Proof. by rewrite /IntoWand /= persistently_idemp. Qed.
 Global Instance into_wand_persistently_false `{!BiAffine PROP} q R P Q :
   IntoWand false q R P Q → IntoWand false q (bi_persistently R) P Q.
 Proof. by rewrite /IntoWand persistently_elim. Qed.
+Global Instance into_wand_Morphism `{BiMorphism PROP PROP'} p q R P Q :
+  IntoWand p q R P Q → IntoWand p q ⎡R⎤ ⎡P⎤ ⎡Q⎤.
+Proof.
+  rewrite /IntoWand -!bi_mor_persistently_if -!bi_mor_affinely_if
+          -bi_mor_wand => -> //.
+Qed.
 
 (* FromAnd *)
 Global Instance from_and_and P1 P2 : FromAnd (P1 ∧ P2) P1 P2 | 100.
@@ -343,6 +370,10 @@ Global Instance from_and_persistently_sep P Q1 Q2 :
   FromAnd (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2) | 11.
 Proof. rewrite /FromAnd=> <-. by rewrite -persistently_and persistently_and_sep. Qed.
 
+Global Instance from_and_morphism `{BiMorphism PROP PROP'} P Q1 Q2 :
+  FromAnd P Q1 Q2 → FromAnd ⎡P⎤ ⎡Q1⎤ ⎡Q2⎤.
+Proof. by rewrite /FromAnd -bi_mor_and => <-. Qed.
+
 Global Instance from_and_big_sepL_cons_persistent {A} (Φ : nat → A → PROP) x l :
   Persistent (Φ 0 x) →
   FromAnd ([∗ list] k ↦ y ∈ x :: l, Φ k y) (Φ 0 x) ([∗ list] k ↦ y ∈ l, Φ (S k) y).
@@ -379,6 +410,10 @@ Global Instance from_sep_persistently P Q1 Q2 :
   FromSep (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2).
 Proof. rewrite /FromSep=> <-. by rewrite persistently_sep_2. Qed.
 
+Global Instance from_sep_morphism `{BiMorphism PROP PROP'} P Q1 Q2 :
+  FromSep P Q1 Q2 → FromSep ⎡P⎤ ⎡Q1⎤ ⎡Q2⎤.
+Proof. by rewrite /FromSep -bi_mor_sep => <-. Qed.
+
 Global Instance from_sep_big_sepL_cons {A} (Φ : nat → A → PROP) x l :
   FromSep ([∗ list] k ↦ y ∈ x :: l, Φ k y) (Φ 0 x) ([∗ list] k ↦ y ∈ l, Φ (S k) y).
 Proof. by rewrite /FromSep big_sepL_cons. Qed.
@@ -436,6 +471,12 @@ Proof.
   - by rewrite -persistently_and !persistently_idemp.
   - intros ->. by rewrite persistently_and.
 Qed.
+Global Instance into_and_morphism `{BiMorphism PROP PROP'} p P Q1 Q2 :
+  IntoAnd p P Q1 Q2 → IntoAnd p ⎡P⎤ ⎡Q1⎤ ⎡Q2⎤.
+Proof.
+  rewrite /IntoAnd -bi_mor_and -!bi_mor_persistently_if
+          -!bi_mor_affinely_if=> -> //.
+Qed.
 
 (* IntoSep *)
 Global Instance into_sep_sep P Q : IntoSep (P ∗ Q) P Q.
@@ -469,6 +510,10 @@ Qed.
 Global Instance into_sep_pure φ ψ : @IntoSep PROP ⌜φ ∧ ψ⌝ ⌜φ⌝ ⌜ψ⌝.
 Proof. by rewrite /IntoSep pure_and persistent_and_sep_1. Qed.
 
+Global Instance into_sep_morphism `{BiMorphism PROP PROP'} P Q1 Q2 :
+  IntoSep P Q1 Q2 → IntoSep ⎡P⎤ ⎡Q1⎤ ⎡Q2⎤.
+Proof. rewrite /IntoSep -bi_mor_sep=> -> //. Qed.
+
 (* FIXME: This instance is kind of strange, it just gets rid of the bi_affinely. Also, it
 overlaps with `into_sep_affinely_later`, and hence has lower precedence. *)
 Global Instance into_sep_affinely P Q1 Q2 :
@@ -515,6 +560,9 @@ Global Instance from_or_persistently P Q1 Q2 :
   FromOr P Q1 Q2 →
   FromOr (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2).
 Proof. rewrite /FromOr=> <-. by rewrite persistently_or. Qed.
+Global Instance from_or_morphism `{BiMorphism PROP PROP'} P Q1 Q2 :
+  FromOr P Q1 Q2 → FromOr ⎡P⎤ ⎡Q1⎤ ⎡Q2⎤.
+Proof. by rewrite /FromOr -bi_mor_or => <-. Qed.
 
 (* IntoOr *)
 Global Instance into_or_or P Q : IntoOr (P ∨ Q) P Q.
@@ -534,6 +582,9 @@ Global Instance into_or_persistently P Q1 Q2 :
   IntoOr P Q1 Q2 →
   IntoOr (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2).
 Proof. rewrite /IntoOr=>->. by rewrite persistently_or. Qed.
+Global Instance into_or_morphism `{BiMorphism PROP PROP'} P Q1 Q2 :
+  IntoOr P Q1 Q2 → IntoOr ⎡P⎤ ⎡Q1⎤ ⎡Q2⎤.
+Proof. by rewrite /IntoOr -bi_mor_or => <-. Qed.
 
 (* FromExist *)
 Global Instance from_exist_exist {A} (Φ : A → PROP): FromExist (∃ a, Φ a) Φ.
@@ -553,6 +604,9 @@ Proof. rewrite /FromExist=> <-. by rewrite -plainly_exist_2. Qed.
 Global Instance from_exist_persistently {A} P (Φ : A → PROP) :
   FromExist P Φ → FromExist (bi_persistently P) (λ a, bi_persistently (Φ a))%I.
 Proof. rewrite /FromExist=> <-. by rewrite persistently_exist. Qed.
+Global Instance from_exist_morphism `{BiMorphism PROP PROP'} {A} P (Φ : A → PROP) :
+  FromExist P Φ → FromExist ⎡P⎤ (λ a, ⎡Φ a⎤%I).
+Proof. by rewrite /FromExist -bi_mor_exist => <-. Qed.
 
 (* IntoExist *)
 Global Instance into_exist_exist {A} (Φ : A → PROP) : IntoExist (∃ a, Φ a) Φ.
@@ -585,6 +639,9 @@ Proof. rewrite /IntoExist=> HP. by rewrite HP plainly_exist. Qed.
 Global Instance into_exist_persistently {A} P (Φ : A → PROP) :
   IntoExist P Φ → IntoExist (bi_persistently P) (λ a, bi_persistently (Φ a))%I.
 Proof. rewrite /IntoExist=> HP. by rewrite HP persistently_exist. Qed.
+Global Instance into_exist_morphism `{BiMorphism PROP PROP'} {A} P (Φ : A → PROP) :
+  IntoExist P Φ → IntoExist ⎡P⎤ (λ a, ⎡Φ a⎤%I).
+Proof. by rewrite /IntoExist -bi_mor_exist => <-. Qed.
 
 (* IntoForall *)
 Global Instance into_forall_forall {A} (Φ : A → PROP) : IntoForall (∀ a, Φ a) Φ.
@@ -598,6 +655,9 @@ Proof. rewrite /IntoForall=> HP. by rewrite HP plainly_forall. Qed.
 Global Instance into_forall_persistently {A} P (Φ : A → PROP) :
   IntoForall P Φ → IntoForall (bi_persistently P) (λ a, bi_persistently (Φ a))%I.
 Proof. rewrite /IntoForall=> HP. by rewrite HP persistently_forall. Qed.
+Global Instance into_forall_morphism `{BiMorphism PROP PROP'} {A} P (Φ : A → PROP) :
+  IntoForall P Φ → IntoForall ⎡P⎤ (λ a, ⎡Φ a⎤%I).
+Proof. by rewrite /IntoForall -bi_mor_forall => <-. Qed.
 
 (* FromForall *)
 Global Instance from_forall_forall {A} (Φ : A → PROP) :
@@ -635,6 +695,9 @@ Proof. rewrite /FromForall=> <-. by rewrite plainly_forall. Qed.
 Global Instance from_forall_persistently {A} P (Φ : A → PROP) :
   FromForall P Φ → FromForall (bi_persistently P)%I (λ a, bi_persistently (Φ a))%I.
 Proof. rewrite /FromForall=> <-. by rewrite persistently_forall. Qed.
+Global Instance from_forall_morphism `{BiMorphism PROP PROP'} {A} P (Φ : A → PROP) :
+  FromForall P Φ → FromForall ⎡P⎤%I (λ a, ⎡Φ a⎤%I).
+Proof. by rewrite /FromForall -bi_mor_forall => <-. Qed.
 
 (* ElimModal *)
 Global Instance elim_modal_wand P P' Q Q' R :
@@ -673,6 +736,26 @@ Proof.
   rewrite /FromPure /Frame=> <-. by rewrite affinely_persistently_if_elim sep_elim_l.
 Qed.
 
+Class MakeMorphism `{BiMorphism PROP PROP'} P (Q : PROP') :=
+  make_morphism : ⎡P⎤ ⊣⊢ Q.
+Arguments MakeMorphism {_ _ _} _%I _%I.
+Global Instance make_morphism_true `{BiMorphism PROP PROP'} :
+  MakeMorphism True True.
+Proof. by rewrite /MakeMorphism bi_mor_pure. Qed.
+Global Instance make_morphism_emp `{BiMorphism PROP PROP'} :
+  MakeMorphism emp emp.
+Proof. by rewrite /MakeMorphism bi_mor_emp. Qed.
+Global Instance make_morphism_default `{BiMorphism PROP PROP'} :
+  MakeMorphism P ⎡P⎤ | 100.
+Proof. by rewrite /MakeMorphism. Qed.
+
+Global Instance frame_morphism `{BiMorphism PROP PROP'} p P Q (Q' : PROP') R :
+  Frame p R P Q → MakeMorphism Q Q' → Frame p ⎡R⎤ ⎡P⎤ Q'.
+Proof.
+  rewrite /Frame /MakeMorphism => <- <-.
+  rewrite bi_mor_sep bi_mor_affinely_if bi_mor_persistently_if => //.
+Qed.
+
 Class MakeSep (P Q PQ : PROP) := make_sep : P ∗ Q ⊣⊢ PQ.
 Arguments MakeSep _%I _%I _%I.
 Global Instance make_sep_emp_l P : MakeSep emp P P.
@@ -851,6 +934,9 @@ Proof. rewrite /Frame=> ?. by rewrite sep_forall_l; apply forall_mono. Qed.
 (* FromModal *)
 Global Instance from_modal_absorbingly P : FromModal (bi_absorbingly P) P.
 Proof. apply absorbingly_intro. Qed.
+Global Instance from_modal_morphism `{BiMorphism PROP PROP'} P Q :
+  FromModal P Q → FromModal ⎡P⎤ ⎡Q⎤.
+Proof. by rewrite /FromModal=> ->. Qed.
 End bi_instances.
 
 
@@ -1057,6 +1143,9 @@ Global Instance is_except_0_except_0 P : IsExcept0 (◇ P).
 Proof. by rewrite /IsExcept0 except_0_idemp. Qed.
 Global Instance is_except_0_later P : IsExcept0 (▷ P).
 Proof. by rewrite /IsExcept0 except_0_later. Qed.
+Global Instance is_except_0_morphism `{SbiMorphism PROP PROP'} P :
+  IsExcept0 P → IsExcept0 ⎡P⎤.
+Proof. by rewrite /IsExcept0 -sbi_mor_except_0=>->. Qed.
 
 (* FromModal *)
 Global Instance from_modal_later P : FromModal (▷ P) P.
@@ -1084,6 +1173,9 @@ Proof. rewrite /IntoExcept0=> ->. by rewrite except_0_plainly. Qed.
 Global Instance into_except_0_persistently P Q :
   IntoExcept0 P Q → IntoExcept0 (bi_persistently P) (bi_persistently Q).
 Proof. rewrite /IntoExcept0=> ->. by rewrite except_0_persistently. Qed.
+Global Instance into_except_0_morphism `{SbiMorphism PROP PROP'} P Q :
+  IntoExcept0 P Q → IntoExcept0 ⎡P⎤ ⎡Q⎤.
+Proof. rewrite /IntoExcept0=> ->. by rewrite sbi_mor_except_0. Qed.
 
 (* ElimModal *)
 Global Instance elim_modal_timeless P Q :
@@ -1190,6 +1282,9 @@ Proof. rewrite /IntoLaterN=> ->. by rewrite laterN_plainly. Qed.
 Global Instance into_later_persistently n P Q :
   IntoLaterN n P Q → IntoLaterN n (bi_persistently P) (bi_persistently Q).
 Proof. rewrite /IntoLaterN=> ->. by rewrite laterN_persistently. Qed.
+Global Instance into_later_morphism`{SbiMorphism PROP PROP'} n P Q :
+  IntoLaterN n P Q → IntoLaterN n ⎡P⎤ ⎡Q⎤.
+Proof. rewrite /IntoLaterN=> ->. by rewrite sbi_mor_laterN. Qed.
 
 Global Instance into_laterN_sep_l n P1 P2 Q1 Q2 :
   IntoLaterN' n P1 Q1 → IntoLaterN n P2 Q2 →
@@ -1273,6 +1368,9 @@ Proof. by rewrite /FromLaterN laterN_persistently=> ->. Qed.
 Global Instance from_later_absorbingly n P Q :
   FromLaterN n P Q → FromLaterN n (bi_absorbingly P) (bi_absorbingly Q).
 Proof. by rewrite /FromLaterN laterN_absorbingly=> ->. Qed.
+Global Instance from_later_morphism`{SbiMorphism PROP PROP'} n P Q :
+  FromLaterN n P Q → FromLaterN n ⎡P⎤ ⎡Q⎤.
+Proof. rewrite /FromLaterN=> <-. by rewrite sbi_mor_laterN. Qed.
 
 Global Instance from_later_forall {A} n (Φ Ψ : A → PROP) :
   (∀ x, FromLaterN n (Φ x) (Ψ x)) → FromLaterN n (∀ x, Φ x) (∀ x, Ψ x).

theories/proofmode/monpred.v

+From iris.bi Require Export monpred.
+From iris.proofmode Require Import tactics.
+Import MonPred.
+
+Section bi.
+Context {I : bi_index} {PROP : bi}.
+Local Notation monPred := (monPred I PROP).
+Implicit Types P Q R : monPred.
+Implicit Types φ : Prop.
+Implicit Types i j : I.
+
+Global Instance as_valid_monPred_car φ P :
+  AsValid φ P → AsValid φ (∀ i, P i).
+Proof.
+  rewrite /AsValid /bi_valid=> ->; unseal; split.
+  - move=>[/= /bi.forall_intro //].
+  - move=>H. split=>i. rewrite /= H bi.forall_elim //.
+Qed.
+
+Global Instance into_pure_monPred_car P φ i : IntoPure P φ → IntoPure (P i) φ.
+Proof. rewrite /IntoPure=> ->. by unseal. Qed.
+Global Instance from_pure_monPred_car P φ i : FromPure P φ → FromPure (P i) φ.
+Proof. rewrite /FromPure=> <-. by unseal. Qed.
+Global Instance into_internal_eq_monPred_car {A : ofeT} (x y : A) P i :
+  IntoInternalEq P x y → IntoInternalEq (P i) x y.
+Proof. rewrite /IntoInternalEq=> ->. by unseal. Qed.
+
+Global Instance into_persistent_monPred_car p P Q i:
+  IntoPersistent p P Q → IntoPersistent p (P i) (Q i) | 0.
+Proof.
+  rewrite /IntoPersistent /bi_persistently_if. unseal=>-[/(_ i)].
+  by destruct p.
+Qed.
+Global Instance from_always_monPred_car a pe P Q i :
+  FromAlways a pe false P Q → FromAlways a pe false (P i) (Q i) | 0.
+Proof.
+  rewrite /FromAlways /bi_persistently_if /bi_affinely_if=><-.
+  by destruct a, pe; try unseal.
+Qed.
+
+Global Instance into_wand_monPred_car p q R P Q i :
+  IntoWand p q R P Q → IntoWand p q (R i) (P i) (Q i).
+Proof.
+  rewrite /IntoWand /bi_affinely_if /bi_persistently_if=>/bi.wand_elim_l' <-.
+  apply bi.wand_intro_r. by destruct p, q; unseal.
+Qed.
+Global Instance from_forall_monPred_car_wand P Q i :
+  FromForall ((P -∗ Q) i)%I (λ j, ⌜i ⊑ j⌝ → P j -∗ Q j)%I.
+Proof. rewrite /FromForall. by unseal. Qed.
+Global Instance into_forall_monPred_car_wand P Q i :
+  IntoForall ((P -∗ Q) i) (λ j, ⌜i ⊑ j⌝ → P j -∗ Q j)%I.
+Proof. rewrite /IntoForall. by unseal. Qed.
+Global Instance from_forall_monPred_car_impl P Q i :
+  FromForall ((P → Q) i)%I (λ j, ⌜i ⊑ j⌝ → P j → Q j)%I.
+Proof. rewrite /FromForall. by unseal. Qed.
+Global Instance into_forall_monPred_car_impl P Q i :
+  IntoForall ((P → Q) i) (λ j, ⌜i ⊑ j⌝ → P j → Q j)%I.
+Proof. rewrite /IntoForall. by unseal. Qed.
+
+Global Instance from_and_monPred_car P Q1 Q2 i:
+  FromAnd P Q1 Q2 → FromAnd (P i) (Q1 i) (Q2 i).
+Proof. rewrite /FromAnd=> <-. by unseal. Qed.
+Global Instance into_and_monPred_car p P Q1 Q2 i:
+  IntoAnd p P Q1 Q2 → IntoAnd p (P i) (Q1 i) (Q2 i).
+Proof.
+  rewrite /IntoAnd /bi_affinely_if /bi_persistently_if=>-[/(_ i)].
+  by destruct p; unseal.
+Qed.
+
+Global Instance from_sep_monPred_car P Q1 Q2 i:
+  FromSep P Q1 Q2 → FromSep (P i) (Q1 i) (Q2 i).
+Proof. rewrite /FromSep=> <-. by unseal. Qed.
+Global Instance into_sep_monPred_car P Q1 Q2 i:
+  IntoSep P Q1 Q2 → IntoSep (P i) (Q1 i) (Q2 i).
+Proof. rewrite /IntoSep=> ->. by unseal. Qed.
+
+Global Instance from_or_monPred_car P Q1 Q2 i:
+  FromOr P Q1 Q2 → FromOr (P i) (Q1 i) (Q2 i).
+Proof. rewrite /FromOr=> <-. by unseal. Qed.
+Global Instance into_or_monPred_car P Q1 Q2 i:
+  IntoOr P Q1 Q2 → IntoOr (P i) (Q1 i) (Q2 i).
+Proof. rewrite /IntoOr=> ->. by unseal. Qed.
+
+Global Instance from_exist_monPred_car {A} P (Φ : A → monPred) i :
+  FromExist P Φ → FromExist (P i) (λ a, Φ a i).
+Proof. rewrite /FromExist=><-. by unseal. Qed.
+Global Instance into_exist_monPred_car {A} P (Φ : A → monPred) i :
+  IntoExist P Φ → IntoExist (P i) (λ a, Φ a i).
+Proof. rewrite /IntoExist=>->. by unseal. Qed.
+
+Global Instance from_forall_monPred_car {A} P (Φ : A → monPred) i :
+  FromForall P Φ → FromForall (P i) (λ a, Φ a i).
+Proof. rewrite /FromForall=><-. by unseal. Qed.
+Global Instance into_forall_monPred_car {A} P (Φ : A → monPred) i :
+  IntoForall P Φ → IntoForall (P i) (λ a, Φ a i).
+Proof. rewrite /IntoForall=>->. by unseal. Qed.
+
+Class MakeMonPredCar i P (Q : PROP) :=
+  make_monPred_car : P i ⊣⊢ Q.
+Arguments MakeMonPredCar _ _%I _%I.
+Global Instance make_monPred_car_true i : MakeMonPredCar i True True.
+Proof. rewrite /MakeMonPredCar. by unseal. Qed.
+Global Instance make_monPred_car_emp i : MakeMonPredCar i emp emp.
+Proof. rewrite /MakeMonPredCar. by unseal. Qed.
+Global Instance make_monPred_car_default i P : MakeMonPredCar i P (P i).
+Proof. by rewrite /MakeMonPredCar. Qed.
+
+(* FIXME : there are two good ways to frame under a call to
+   monPred_car. This may cause some backtracking in the typeclass
+   search, and hence performance issues. *)
+Global Instance frame_monPred_car i p P Q (Q' : PROP) R :
+  Frame p R P Q → MakeMonPredCar i Q Q' → Frame p (R i) (P i) Q'.
+Proof.
+  rewrite /Frame /MakeMonPredCar /bi_affinely_if /bi_persistently_if=> <- <-.
+  by destruct p; unseal.
+Qed.
+Global Instance frame_monPred_car_embed i p P Q (Q' R: PROP) :
+  Frame p ⎡R⎤ P Q → MakeMonPredCar i Q Q' → Frame p R (P i) Q'.
+Proof.
+  rewrite /Frame /MakeMonPredCar /bi_affinely_if /bi_persistently_if=> <- <-.
+  by destruct p; unseal.
+Qed.
+
+Global Instance from_modal_monPred_car i P Q :
+  FromModal P Q → FromModal (P i) (Q i).
+Proof. by rewrite /FromModal=>->. Qed.
+End bi.
+
+Section sbi.
+Context {I : bi_index} {PROP : sbi}.
+Local Notation monPred := (monPred I PROP).
+Implicit Types P Q R : monPred.
+Implicit Types φ : Prop.
+Implicit Types i j : I.
+
+Global Instance is_except_0_monPred_car i P :
+  IsExcept0 P → IsExcept0 (P i).
+Proof. rewrite /IsExcept0=>- [/(_ i)]. by unseal. Qed.
+Global Instance into_except_0_monPred_car i P Q :
+  IntoExcept0 P Q → IntoExcept0 (P i) (Q i).
+Proof. rewrite /IntoExcept0=> ->. by unseal. Qed.
+Global Instance into_later_monPred_car i n P Q :
+  IntoLaterN n P Q → IntoLaterN n (P i) (Q i).
+Proof.
+  rewrite /IntoLaterN=> ->. induction n as [|? IH]=>//. rewrite /= -IH. by unseal.
+Qed.
+Global Instance from_later_monPred_car i n P Q :
+  FromLaterN n P Q → FromLaterN n (P i) (Q i).
+Proof.
+  rewrite /FromLaterN=> <-. induction n as [|? IH]=>//. rewrite /= IH. by unseal.
+Qed.
+End sbi.

theories/proofmode/tactics.v

@@ -65,22 +65,29 @@ Proof. by apply as_valid. Qed.
 Instance as_valid_valid {PROP : bi} (P : PROP) : AsValid (bi_valid P) P | 0.
 Proof. by rewrite /AsValid. Qed.
 
-Instance as_valid_entails {PROP : bi} (P Q : PROP) : AsValid (P ⊢ Q) (P -∗ Q) | 1.
+Instance as_valid_entails {PROP : bi} (P Q : PROP) : AsValid (P ⊢ Q) (P -∗ Q) | 0.
 Proof. split. apply bi.entails_wand. apply bi.wand_entails. Qed.
 
-Instance as_valid_equiv {PROP : bi} (P Q : PROP) : AsValid (P ≡ Q) (P ∗-∗ Q).
+Instance as_valid_equiv {PROP : bi} (P Q : PROP) : AsValid (P ≡ Q) (P ∗-∗ Q) | 0.
 Proof. split. apply bi.equiv_wand_iff. apply bi.wand_iff_equiv. Qed.
 
+Instance as_valid_morphism `{BiMorphism PROP PROP'} (φ : Prop) (P : PROP) :
+  AsValid φ P → AsValid φ ⎡P⎤.
+Proof. rewrite /AsValid=> ->. rewrite bi_mor_valid //. Qed.
+
 (** * Start a proof *)
-Ltac iStartProof :=
+Tactic Notation "iStartProof" uconstr(PROP) :=
   lazymatch goal with
-  | |- envs_entails _ _ => idtac
+  | |- @envs_entails ?PROP' _ _ =>
+    let x := type_term (eq_refl : PROP = PROP') in idtac
   | |- let _ := _ in _ => fail
-  | |- ?φ => eapply (as_valid_2 φ);
+  | |- ?φ => eapply (@as_valid_2 φ PROP);
                [apply _ || fail "iStartProof: not a Bi entailment"
                |apply tac_adequate]
   end.
 
+Tactic Notation "iStartProof" := iStartProof _.
+
 (** * Context manipulation *)
 Tactic Notation "iRename" constr(H1) "into" constr(H2) :=
   eapply tac_rename with _ H1 H2 _ _; (* (i:=H1) (j:=H2) *)