(* tests/telescopes.v *)
From stdpp Require Import coPset namespaces
From iris.proofmode Require Import proofmode
From iris.prelude Require Import options

Lemma test_iIntros_tforall{TT : tele} (Φ : TT → PROP) :
    ⊢ ∀.. x, Φ x -∗ Φ x.
  Proof. iIntros (x) "H". done. Qed.

Lemma test_iPoseProof_tforall{TT : tele} P (Φ : TT → PROP) :
    (∀.. x, P ⊢ Φ x) → P -∗ ∀.. x, Φ x.
  Proof.
    iIntros (H1) "H2"; iIntros (x).
    iPoseProof (H1) as "H1". by iApply "H1".
  Qed.

Lemma test_iApply_tforall{TT : tele} P (Φ : TT → PROP) :
    (∀.. x, P -∗ Φ x) -∗ P -∗ ∀.. x, Φ x.
  Proof. iIntros "H1 H2" (x). by iApply "H1". Qed.

Lemma test_iAssumption_tforall{TT : tele} (Φ : TT → PROP) :
    (∀.. x, Φ x) -∗ ∀.. x, Φ x.
  Proof. iIntros "H" (x). iAssumption. Qed.

Lemma test_exist_texist_auto_name{TT : tele} (Φ : TT → PROP) :
    (∃.. y, Φ y) -∗ ∃.. x, Φ x.
  Proof. iDestruct 1 as (?) "H". by iExists y. Qed.

Lemma test_pure_texist{TT : tele} (φ : TT → Prop) :
    (∃.. x, ⌜ φ x ⌝) -∗ ∃.. x, ⌜ φ x ⌝ : PROP.
  Proof. iIntros (H) "!%". done. Qed.

Lemma test_pure_tforall`{!BiPureForall PROP} {TT : tele} (φ : TT → Prop) :
    (∀.. x, ⌜ φ x ⌝) -∗ ∀.. x, ⌜ φ x ⌝ : PROP.
  Proof. iIntros (H) "!%". done. Qed.

Lemma test_pure_tforall_persistent`{!BiPersistentlyForall PROP} {TT : tele} (Φ : TT → PROP) :
    (∀.. x, <pers> (Φ x)) -∗ <pers> ∀.. x, Φ x.
  Proof. iIntros "#H !>" (x). done. Qed.

Lemma test_pure_texists_intuitionistic{TT : tele} (Φ : TT → PROP) :
    (∃.. x, □ (Φ x)) -∗ □ ∃.. x, Φ x.
  Proof. iDestruct 1 as (x) "#H". iExists (x). done. Qed.

Lemma test_iMod_tforall{TT : tele} P (Φ : TT → PROP) :
    ◇ P -∗ (∀.. x, Φ x) -∗ ∀.. x, ◇ (P ∗ Φ x).
  Proof. iIntros ">H1 H2" (x) "!> {$H1}". done. Qed.

Lemma test_timeless_tforall{TT : tele} (φ : TT → Prop) :
    ▷ (∀.. x, ⌜ φ x ⌝) -∗ ◇ ∀.. x, ⌜ φ x ⌝ : PROP.
  Proof. iIntros ">H1 !>". done. Qed.

Lemma test_timeless_texist{TT : tele} (φ : TT → Prop) :
    ▷ (∃.. x, ⌜ φ x ⌝) -∗ ◇ ∃.. x, ⌜ φ x ⌝ : PROP.
  Proof. iIntros ">H1 !>". done. Qed.

Lemma test_add_model_texist`{!BiBUpd PROP} {TT : tele} P Q (Φ : TT → PROP) :
    (|==> P) -∗ (P -∗ Q) -∗ ∀.. x, |==> Q ∗ (Φ x -∗ Φ x).
  Proof. iIntros "H1 H2". iDestruct ("H2" with "[> $H1]") as "$". auto. Qed.

Lemma test_iFrame_tforall{TT : tele} P (Φ : TT → PROP) :
    P -∗ ∀.. x, P ∗ (Φ x -∗ Φ x).
  Proof. iIntros "$". auto. Qed.

Lemma test_iFrame_texist{TT : tele} P (Φ : TT → PROP) :
    P -∗ (∃.. x, Φ x) -∗ ∃.. x, P ∗ Φ x.
  Proof. iIntros "$". auto. Qed.

Definition accessor`{!BiFUpd PROP} {X : tele} (E1 E2 : coPset)
           (α β γ : X → PROP) : PROP :=
  (|={E1,E2}=> ∃.. x, α x ∗ (β x -∗ |={E2,E1}=> (γ x)))%I.

Lemma acc_monoE1 E2 α β γ1 γ2 :
  (∀.. x, γ1 x -∗ γ2 x) -∗
  accessor E1 E2 α β γ1 -∗ accessor E1 E2 α β γ2.
Proof.
  iIntros "Hγ12 >Hacc". iDestruct "Hacc" as (x') "[Hα Hclose]". Show.
  iModIntro. iExists x'. iFrame. iIntros "Hβ".
  iMod ("Hclose" with "Hβ") as "Hγ". iApply "Hγ12". auto.
Qed.

Lemma acc_mono_disjE1 E2 α β γ1 γ2 :
  accessor E1 E2 α β γ1 -∗ accessor E1 E2 α β (λ.. x, γ1 x ∨ γ2 x).
Proof.
  Show.
  iApply acc_mono. iIntros (x) "Hγ1". Show.
  rewrite ->tele_app_bind. Show.
  iLeft. done.
Qed.

Lemma acc_elim_test_1E1 E2 :
  ACC @ E1, E2 {{ ∃ a b : nat, <affine> ⌜a = b⌝ | True | <affine> ⌜a ≠ b⌝ }}
    ⊢@{PROP} |={E1}=> False.
Proof.
  iIntros ">H". Show.
  iDestruct "H" as (a b) "[% Hclose]". iMod ("Hclose" with "[//]") as "%".
  done.
Qed.

Definition test1{PROP : bi} {X : tele} (α : X → PROP) : PROP :=
  (∃.. x, α x)%I.

Definition test2{PROP : bi} {X : tele} (α : X → PROP) : PROP :=
  (▷ ∃.. x, α x)%I.

Definition test3{PROP : bi} {X : tele} (α : X → PROP) : PROP :=
  (◇ ∃.. x, α x)%I.

Lemma test1_test{PROP : bi}  :
  TEST1 {{ ∃ a b : nat, <affine> ⌜a = b⌝ }} ⊢@{PROP} ▷ False.
Proof.
  iIntros "H". iDestruct "H" as (x) "H". Show.
Restart. Proof.
  iIntros "H". unfold test1. iDestruct "H" as (x) "H". Show.
Abort.
Check "test2_test".

Lemma test2_test{PROP : bi}  :
  TEST2 {{ ∃ a b : nat, <affine> ⌜a = b⌝ }} ⊢@{PROP} ▷ False.
Proof.
  iIntros "H". iModIntro. Show.
  iDestruct "H" as (x) "H". Show.
Restart. Proof.
  iIntros "H". iDestruct "H" as (x) "H". Show.
Abort.
Check "test3_test".

Lemma test3_test{PROP : bi}  :
  TEST3 {{ ∃ a b : nat, <affine> ⌜a = b⌝ }} ⊢@{PROP} ▷ False.
Proof.
  iIntros "H". iMod "H".
  iDestruct "H" as (x) "H".
  Show.
Restart. Proof.
  iIntros "H". iDestruct "H" as (x) "H". Show.
Abort.

Lemma tele_universe{PROP : bi} (TT : tele@{bi.Quant}) (P : TT → PROP) :
  bi_texist P ⊣⊢ bi_exist P.
Proof. apply bi_texist_exist. Qed.