(* iris/bi/telescopes.v *)
From stdpp Require Export telescopes
From iris.bi Require Export bi
From iris.prelude Require Import options

Definition bi_texist{PROP : bi} {TT : tele@{Quant}} (Ψ : TT → PROP) : PROP :=
  tele_fold (@bi_exist PROP) (λ x, x) (tele_bind Ψ).

Global Argumentsbi_texist {_ !_} _ /.

Definition bi_tforall{PROP : bi} {TT : tele@{Quant}} (Ψ : TT → PROP) : PROP :=
  tele_fold (@bi_forall PROP) (λ x, x) (tele_bind Ψ).

Global Argumentsbi_tforall {_ !_} _ /.

Lemma bi_tforall_forallΨ : bi_tforall Ψ ⊣⊢ bi_forall Ψ.
  Proof.
    symmetry. unfold bi_tforall. induction TT as [|X ft IH].
    - simpl. apply (anti_symm _).
      + by rewrite (forall_elim TargO).
      + rewrite -forall_intro; first done.
        intros p. rewrite (tele_arg_O_inv p) /= //.
    - simpl. apply (anti_symm _); apply forall_intro; intros a.
      + rewrite /= -IH. apply forall_intro; intros p.
        by rewrite (forall_elim (TargS a p)).
      + destruct a=> /=.
        setoid_rewrite <- IH.
        rewrite 2!forall_elim. done.
  Qed.

Lemma bi_texist_existΨ : bi_texist Ψ ⊣⊢ bi_exist Ψ.
  Proof.
    symmetry. unfold bi_texist. induction TT as [|X ft IH].
    - simpl. apply (anti_symm _).
      + apply exist_elim; intros p.
        rewrite (tele_arg_O_inv p) //.
      + by rewrite -(exist_intro TargO).
    - simpl. apply (anti_symm _); apply exist_elim.
      + intros p. destruct p => /=.
        by rewrite -exist_intro -IH -exist_intro.
      + intros x.
        rewrite /= -IH. apply exist_elim; intros p.
        by rewrite -(exist_intro (TargS x p)).
  Qed.

Global Instancebi_tforall_ne n :
    Proper (pointwise_relation _ (dist n) ==> dist n) (@bi_tforall PROP TT).
  Proof. intros ?? EQ. rewrite !bi_tforall_forall. rewrite EQ //. Qed.

Global Instancebi_tforall_proper :
    Proper (pointwise_relation _ (⊣⊢) ==> (⊣⊢)) (@bi_tforall PROP TT).
  Proof. intros ?? EQ. rewrite !bi_tforall_forall. rewrite EQ //. Qed.

Global Instancebi_texist_ne n :
    Proper (pointwise_relation _ (dist n) ==> dist n) (@bi_texist PROP TT).
  Proof. intros ?? EQ. rewrite !bi_texist_exist. rewrite EQ //. Qed.

Global Instancebi_texist_proper :
    Proper (pointwise_relation _ (⊣⊢) ==> (⊣⊢)) (@bi_texist PROP TT).
  Proof. intros ?? EQ. rewrite !bi_texist_exist. rewrite EQ //. Qed.

Global Instancebi_tforall_absorbing Ψ :
    (∀ x, Absorbing (Ψ x)) → Absorbing (∀.. x, Ψ x).
  Proof. rewrite bi_tforall_forall. apply _. Qed.

Global Instancebi_tforall_persistent `{!BiPersistentlyForall PROP} Ψ :
    (∀ x, Persistent (Ψ x)) → Persistent (∀.. x, Ψ x).
  Proof. rewrite bi_tforall_forall. apply _. Qed.

Global Instancebi_texist_affine Ψ :
    (∀ x, Affine (Ψ x)) → Affine (∃.. x, Ψ x).
  Proof. rewrite bi_texist_exist. apply _. Qed.

Global Instancebi_texist_absorbing Ψ :
    (∀ x, Absorbing (Ψ x)) → Absorbing (∃.. x, Ψ x).
  Proof. rewrite bi_texist_exist. apply _. Qed.

Global Instancebi_texist_persistent Ψ :
    (∀ x, Persistent (Ψ x)) → Persistent (∃.. x, Ψ x).
  Proof. rewrite bi_texist_exist. apply _. Qed.

Global Instancebi_tforall_timeless Ψ :
    (∀ x, Timeless (Ψ x)) → Timeless (∀.. x, Ψ x).
  Proof. rewrite bi_tforall_forall. apply _. Qed.

Global Instancebi_texist_timeless Ψ :
    (∀ x, Timeless (Ψ x)) → Timeless (∃.. x, Ψ x).
  Proof. rewrite bi_texist_exist. apply _. Qed.