Missing proof mode instances for telescopes.

theories/proofmode/class_instances_bi.v

@@ -45,6 +45,12 @@ Proof.
   - apply bi.forall_intro=>?. apply H1, H2.
   - intros x. apply H1. revert H2. by rewrite (bi.forall_elim x).
 Qed.
+Global Instance as_emp_valid_tforall {TT : tele} (φ : TT → Prop) (P : TT → PROP) :
+  (∀ x, AsEmpValid (φ x) (P x)) → AsEmpValid (∀.. x, φ x) (∀.. x, P x).
+Proof.
+  rewrite /AsEmpValid !tforall_forall bi_tforall_forall.
+  apply as_emp_valid_forall.
+Qed.
 
 (* We add a useless hypothesis [BiEmbed PROP PROP'] in order to make
    sure this instance is not used when there is no embedding between
@@ -142,6 +148,12 @@ Proof.
   rewrite /KnownLFromAssumption /FromAssumption=> <-.
   by rewrite forall_elim.
 Qed.
+Global Instance from_assumption_tforall {TT : tele} p (Φ : TT → PROP) Q x :
+  FromAssumption p (Φ x) Q → KnownLFromAssumption p (∀.. x, Φ x) Q.
+Proof.
+  rewrite /KnownLFromAssumption /FromAssumption=> <-.
+  by rewrite bi_tforall_forall forall_elim.
+Qed.
 
 Global Instance from_assumption_bupd `{BiBUpd PROP} p P Q :
   FromAssumption p P Q → KnownRFromAssumption p P (|==> Q).
@@ -164,9 +176,17 @@ Proof. rewrite /FromPure /IntoPure pure_impl=> <- -> //. Qed.
 Global Instance into_pure_exist {A} (Φ : A → PROP) (φ : A → Prop) :
   (∀ x, IntoPure (Φ x) (φ x)) → IntoPure (∃ x, Φ x) (∃ x, φ x).
 Proof. rewrite /IntoPure=>Hx. rewrite pure_exist. by setoid_rewrite Hx. Qed.
+Global Instance into_pure_texist {TT : tele} (Φ : TT → PROP) (φ : TT → Prop) :
+  (∀ x, IntoPure (Φ x) (φ x)) → IntoPure (∃.. x, Φ x) (∃.. x, φ x).
+Proof. rewrite /IntoPure texist_exist bi_texist_exist. apply into_pure_exist. Qed.
 Global Instance into_pure_forall {A} (Φ : A → PROP) (φ : A → Prop) :
   (∀ x, IntoPure (Φ x) (φ x)) → IntoPure (∀ x, Φ x) (∀ x, φ x).
 Proof. rewrite /IntoPure=>Hx. rewrite -pure_forall_2. by setoid_rewrite Hx. Qed.
+Global Instance into_pure_tforall {TT : tele} (Φ : TT → PROP) (φ : TT → Prop) :
+  (∀ x, IntoPure (Φ x) (φ x)) → IntoPure (∀.. x, Φ x) (∀.. x, φ x).
+Proof.
+  rewrite /IntoPure !tforall_forall bi_tforall_forall. apply into_pure_forall.
+Qed.
 
 Global Instance into_pure_pure_sep (φ1 φ2 : Prop) P1 P2 :
   IntoPure P1 φ1 → IntoPure P2 φ2 → IntoPure (P1 ∗ P2) (φ1 ∧ φ2).
@@ -225,12 +245,20 @@ Proof.
   rewrite /FromPure=>Hx. rewrite pure_exist affinely_if_exist.
   by setoid_rewrite Hx.
 Qed.
+Global Instance from_pure_texist {TT : tele} a (Φ : TT → PROP) (φ : TT → Prop) :
+  (∀ x, FromPure a (Φ x) (φ x)) → FromPure a (∃.. x, Φ x) (∃.. x, φ x).
+Proof. rewrite /FromPure texist_exist bi_texist_exist. apply from_pure_exist. Qed.
 Global Instance from_pure_forall {A} a (Φ : A → PROP) (φ : A → Prop) :
   (∀ x, FromPure a (Φ x) (φ x)) → FromPure a (∀ x, Φ x) (∀ x, φ x).
 Proof.
   rewrite /FromPure=>Hx. rewrite pure_forall. setoid_rewrite <-Hx.
   destruct a=>//=. apply affinely_forall.
 Qed.
+Global Instance from_pure_tforall {TT : tele} a (Φ : TT → PROP) (φ : TT → Prop) :
+  (∀ x, FromPure a (Φ x) (φ x)) → FromPure a (∀.. x, Φ x) (∀.. x, φ x).
+Proof.
+  rewrite /FromPure !tforall_forall bi_tforall_forall. apply from_pure_forall.
+Qed.
 
 Global Instance from_pure_pure_sep_true a1 a2 (φ1 φ2 : Prop) P1 P2 :
   FromPure a1 P1 φ1 → FromPure a2 P2 φ2 →
@@ -1004,6 +1032,9 @@ Proof. by rewrite /FromForall bi_tforall_forall. Qed.
 Global Instance from_forall_pure {A} (φ : A → Prop) :
   @FromForall PROP A ⌜∀ a : A, φ a⌝ (λ a, ⌜ φ a ⌝)%I.
 Proof. by rewrite /FromForall pure_forall. Qed.
+Global Instance from_tforall_pure {TT : tele} (φ : TT → Prop) :
+  @FromForall PROP TT ⌜∀.. x : TT, φ x⌝ (λ x, ⌜ φ x ⌝)%I.
+Proof. by rewrite /FromForall tforall_forall pure_forall. Qed.
 Global Instance from_forall_pure_not (φ : Prop) :
   @FromForall PROP φ ⌜¬ φ⌝ (λ a : φ, False)%I.
 Proof. by rewrite /FromForall pure_forall. Qed.
@@ -1051,10 +1082,15 @@ Global Instance elim_modal_wandM φ p p' P P' Q Q' mR :
   ElimModal φ p p' P P' (mR -∗? Q) (mR -∗? Q').
 Proof. rewrite /ElimModal !wandM_sound. exact: elim_modal_wand. Qed.
 Global Instance elim_modal_forall {A} φ p p' P P' (Φ Ψ : A → PROP) :
-  (∀ x, ElimModal φ p p' P P' (Φ x) (Ψ x)) → ElimModal φ p p' P P' (∀ x, Φ x) (∀ x, Ψ x).
+  (∀ x, ElimModal φ p p' P P' (Φ x) (Ψ x)) →
+  ElimModal φ p p' P P' (∀ x, Φ x) (∀ x, Ψ x).
 Proof.
   rewrite /ElimModal=> H ?. apply forall_intro=> a. rewrite (forall_elim a); auto.
 Qed.
+Global Instance elim_modal_tforall {TT : tele} φ p p' P P' (Φ Ψ : TT → PROP) :
+  (∀ x, ElimModal φ p p' P P' (Φ x) (Ψ x)) →
+  ElimModal φ p p' P P' (∀.. x, Φ x) (∀.. x, Ψ x).
+Proof. rewrite /ElimModal !bi_tforall_forall. apply elim_modal_forall. Qed.
 Global Instance elim_modal_absorbingly_here p P Q :
   Absorbing Q → ElimModal True p false (<absorb> P) P Q Q.
 Proof.
@@ -1095,6 +1131,9 @@ Global Instance add_modal_forall {A} P P' (Φ : A → PROP) :
 Proof.
   rewrite /AddModal=> H. apply forall_intro=> a. by rewrite (forall_elim a).
 Qed.
+Global Instance add_modal_tforall {TT : tele} P P' (Φ : TT → PROP) :
+  (∀ x, AddModal P P' (Φ x)) → AddModal P P' (∀.. x, Φ x).
+Proof. rewrite /AddModal bi_tforall_forall. apply add_modal_forall. Qed.
 Global Instance add_modal_embed_bupd_goal `{BiEmbedBUpd PROP PROP'}
        (P P' : PROP') (Q : PROP) :
   AddModal P P' (|==> ⎡Q⎤)%I → AddModal P P' ⎡|==> Q⎤.

theories/proofmode/frame_instances.v

 From stdpp Require Import nat_cancel.
-From iris.bi Require Import bi tactics.
+From iris.bi Require Import bi tactics telescopes.
 From iris.proofmode Require Import classes.
 Set Default Proof Using "Type".
 Import bi.
@@ -265,9 +265,15 @@ Qed.
 Global Instance frame_exist {A} p R (Φ Ψ : A → PROP) :
   (∀ a, Frame p R (Φ a) (Ψ a)) → Frame p R (∃ x, Φ x) (∃ x, Ψ x).
 Proof. rewrite /Frame=> ?. by rewrite sep_exist_l; apply exist_mono. Qed.
+Global Instance frame_texist {TT : tele} p R (Φ Ψ : TT → PROP) :
+  (∀ x, Frame p R (Φ x) (Ψ x)) → Frame p R (∃.. x, Φ x) (∃.. x, Ψ x).
+Proof. rewrite /Frame !bi_texist_exist. apply frame_exist. Qed.
 Global Instance frame_forall {A} p R (Φ Ψ : A → PROP) :
   (∀ a, Frame p R (Φ a) (Ψ a)) → Frame p R (∀ x, Φ x) (∀ x, Ψ x).
 Proof. rewrite /Frame=> ?. by rewrite sep_forall_l; apply forall_mono. Qed.
+Global Instance frame_tforall {TT : tele} p R (Φ Ψ : TT → PROP) :
+  (∀ x, Frame p R (Φ x) (Ψ x)) → Frame p R (∀.. x, Φ x) (∀.. x, Ψ x).
+Proof. rewrite /Frame !bi_tforall_forall. apply frame_forall. Qed.
 
 Global Instance frame_impl_persistent R P1 P2 Q2 :
   Frame true R P2 Q2 → Frame true R (P1 → P2) (P1 → Q2).