(* tests/proofmode_monpred.v *)
From iris.bi.lib Require Import fractional
From iris.proofmode Require Import proofmode monpred
From iris.base_logic.lib Require Import invariants ghost_var
From iris.prelude Require Import options

Local NotationmonPred := (monPred I PROP).

Local NotationmonPredI := (monPredI I PROP).
  Implicit Types P Q R : monPred.
  Implicit Types 𝓟 𝓠 𝓡 : PROP.
  Implicit Types i j : I.

Lemma test0P : P -∗ P.
  Proof. iIntros "$". Qed.

Lemma test_iStartProof_1P : P -∗ P.
  Proof. iStartProof. iStartProof. iIntros "$". Qed.

Lemma test_iStartProof_2P : P -∗ P.
  Proof. iStartProof monPred. iStartProof monPredI. iIntros "$". Qed.

Lemma test_iStartProof_3P : P -∗ P.
  Proof. iStartProof monPredI. iStartProof monPredI. iIntros "$". Qed.

Lemma test_iStartProof_4P : P -∗ P.
  Proof. iStartProof monPredI. iStartProof monPred. iIntros "$". Qed.

Lemma test_iStartProof_5P : P -∗ P.
  Proof. iStartProof PROP. iIntros (i) "$". Qed.

Lemma test_iStartProof_6P : P ⊣⊢ P.
  Proof. iStartProof PROP. iIntros (i). iSplit; iIntros "$". Qed.

Lemma test_iStartProof_7`{!Sbi PROP} P : ⊢@{monPredI} P ≡ P.
  Proof. iStartProof PROP. done. Qed.

Lemma test_intowand_1P Q : (P -∗ Q) -∗ P -∗ Q.
  Proof.
    iStartProof PROP. iIntros (i) "HW". Show.
    iIntros (j ->) "HP". Show. by iApply "HW".
  Qed.

Lemma test_intowand_2P Q : (P -∗ Q) -∗ P -∗ Q.
  Proof.
    iStartProof PROP. iIntros (i) "HW". iIntros (j ->) "HP".
    iSpecialize ("HW" with "[HP //]"). done.
  Qed.

Lemma test_intowand_3P Q : (P -∗ Q) -∗ P -∗ Q.
  Proof.
    iStartProof PROP. iIntros (i) "HW". iIntros (j ->) "HP".
    iSpecialize ("HW" with "HP"). done.
  Qed.

Lemma test_intowand_4P Q : (P -∗ Q) -∗ ▷ P -∗ ▷ Q.
  Proof.
    iStartProof PROP. iIntros (i) "HW". iIntros (j ->) "HP". by iApply "HW".
  Qed.

Lemma test_intowand_5P Q : (P -∗ Q) -∗ ▷ P -∗ ▷ Q.
  Proof.
    iStartProof PROP. iIntros (i) "HW". iIntros (j ->) "HP".
    iSpecialize ("HW" with "HP"). done.
  Qed.

Lemma test_apply_in_elim(P : monPredI) (i : I) : monPred_in i -∗ ⎡ P i ⎤ → P.
  Proof. iIntros. by iApply monPred_in_elim. Qed.

Lemma test_iStartProof_forall_1(Φ : nat → monPredI) : ∀ n, Φ n -∗ Φ n.
  Proof.
    iStartProof PROP. iIntros (n i) "$".
  Qed.

Lemma test_iStartProof_forall_2(Φ : nat → monPredI) : ∀ n, Φ n -∗ Φ n.
  Proof.
    iStartProof. iIntros (n) "$".
  Qed.

Lemma test_embed_wand(P Q : PROP) : (⎡P⎤ -∗ ⎡Q⎤) ⊢@{monPredI} ⎡P -∗ Q⎤.
  Proof.
    iIntros "H HP". by iApply "H".
  Qed.

Lemma test_objectively`{!BiPersistentlyForall PROP} P Q :
    <obj> emp -∗ <obj> P -∗ <obj> Q -∗ <obj> (P ∗ Q).
  Proof. iIntros "#? HP HQ". iModIntro. by iSplitL "HP". Qed.

Lemma test_objectively_absorbing`{!BiPersistentlyForall PROP} P Q R `{!Absorbing P} :
    <obj> emp -∗ <obj> P -∗ <obj> Q -∗ R -∗ <obj> (P ∗ Q).
  Proof. iIntros "#? HP HQ HR". iModIntro. by iSplitL "HP". Qed.

Lemma test_objectively_affine`{!BiPersistentlyForall PROP} P Q R `{!Affine R} :
    <obj> emp -∗ <obj> P -∗ <obj> Q -∗ R -∗ <obj> (P ∗ Q).
  Proof. iIntros "#? HP HQ HR". iModIntro. by iSplitL "HP". Qed.

Lemma test_iModIntro_embedP `{!Affine Q} 𝓟 𝓠 :
    □ P -∗ Q -∗ ⎡𝓟⎤ -∗ ⎡𝓠⎤ -∗ ⎡ 𝓟 ∗ 𝓠 ⎤.
  Proof. iIntros "#H1 _ H2 H3". iModIntro. iFrame. Qed.

Lemma test_iModIntro_embed_objectiveP `{!Objective Q} 𝓟 𝓠 :
    □ P -∗ Q -∗ ⎡𝓟⎤ -∗ ⎡𝓠⎤ -∗ ⎡ ∀ i, 𝓟 ∗ 𝓠 ∗ Q i ⎤.
  Proof. iIntros "#H1 H2 H3 H4". iModIntro. Show. iFrame. Qed.

Lemma test_iModIntro_embed_nestedP 𝓟 𝓠 :
    □ P -∗ ⎡◇ 𝓟⎤ -∗ ⎡◇ 𝓠⎤ -∗ ⎡ ◇ (𝓟 ∗ 𝓠) ⎤.
  Proof. iIntros "#H1 H2 H3". iModIntro ⎡ _ ⎤%I. by iSplitL "H2". Qed.

Lemma test_into_wand_embed𝓟 𝓠 :
    (𝓟 -∗ ◇ 𝓠) →
    ⎡𝓟⎤ ⊢@{monPredI} ◇ ⎡𝓠⎤.
  Proof.
    iIntros (HPQ) "HP".
    iMod (HPQ with "[-]") as "$"; last by auto.
    iAssumption.
  Qed.

Lemma test_monPred_at_and_pureP i j :
    (monPred_in j ∧ P) i ⊢ ⌜ j ⊑ i ⌝ ∧ P i.
  Proof.
    iDestruct 1 as "[% $]". done.
  Qed.

Lemma test_monPred_at_sep_pureP i j :
    (monPred_in j ∗ <absorb> P) i ⊢ ⌜ j ⊑ i ⌝ ∧ <absorb> P i.
  Proof.
    iDestruct 1 as "[% ?]". auto.
  Qed.
  Context (FU : BiFUpd PROP).

Lemma test_apply_fupd_intro_mask_subseteqE1 E2 P :
    E2 ⊆ E1 → P -∗ |={E1,E2}=> |={E2,E1}=> P.
  Proof. iIntros. by iApply @fupd_mask_intro_subseteq. Qed.

Lemma test_apply_fupd_mask_subseteqE1 E2 P :
    E2 ⊆ E1 → P -∗ |={E1,E2}=> |={E2,E1}=> P.
  Proof. iIntros. iFrame. by iApply @fupd_mask_subseteq. Qed.

Lemma test_iFrame_embed_persistent(P : PROP) (Q: monPred) :
    Q ∗ □ ⎡P⎤ ⊢ Q ∗ ⎡P ∗ P⎤.
  Proof.
    iIntros "[$ #HP]". iFrame "HP".
  Qed.

Lemma test_iNext_BiP :
    ▷ P ⊢@{monPredI} ▷ P.
  Proof. iIntros "H". by iNext. Qed.

Lemma test_iFrame_monPred_at_wand(P Q : monPred) i :
    P i -∗ (Q -∗ P) i.
  Proof. iIntros "$". Show. Abort.

Program DefinitionmonPred_id (R : monPred) : monPred :=
    MonPred (λ V, R V) _.
  Next Obligation. intros ? ???. eauto. Qed.

Lemma test_iFrame_monPred_id(Q R : monPred) i :
    Q i ∗ R i -∗ (Q ∗ monPred_id R) i.
  Proof.
    iIntros "(HQ & HR)". iFrame "HR". iAssumption.
  Qed.

Lemma test_iFrame_relP i j ij :
    IsBiIndexRel i ij → IsBiIndexRel j ij →
    P i -∗ P j -∗ P ij ∗ P ij.
  Proof. iIntros (??) "HPi HPj". iFrame. Qed.

Lemma test_iFrame_later_rel`{!BiAffine PROP} P i j :
    IsBiIndexRel i j →
    ▷ (P i) -∗ (▷ P) j.
  Proof. iIntros (?) "?". iFrame. Qed.

Lemma test_iFrame_laterNn P i :
    ▷^n (P i) -∗ (▷^n P) i.
  Proof. iIntros "?". iFrame. Qed.

Lemma test_iFrame_quantifiersP i :
    P i -∗ (∀ _:(), ∃ _:(), P) i.
  Proof. iIntros "?". iFrame. Show. iIntros ([]). iExists (). iEmpIntro. Qed.

Lemma test_iFrame_embed(P : PROP) i :
    P -∗ (embed (B:=monPredI) P) i.
  Proof. iIntros "$". Qed.

Lemma test_iFrame_monPred_at_evar(P : monPred) i j :
    P i -∗ ∃ Q, (Q j).
  Proof. iIntros "HP". iExists _. Fail iFrame "HP". Abort.

Local NotationmonPred := (monPred I (iPropI Σ)).

Local NotationmonPredI := (monPredI I (iPropI Σ)).
  Implicit Types P Q R : monPred.
  Implicit Types 𝓟 𝓠 𝓡 : iProp Σ.

Lemma test_iInv_0N 𝓟 :
    embed (B:=monPred) (inv N (<pers> 𝓟)) ={⊤}=∗ ⎡▷ 𝓟⎤.
  Proof.
    iIntros "#H".
    iInv N as "#H2". Show.
    iModIntro. iSplit=>//. iModIntro. iModIntro; auto.
  Qed.

Lemma test_iInv_0_with_closeN 𝓟 :
    embed (B:=monPred) (inv N (<pers> 𝓟)) ={⊤}=∗ ⎡▷ 𝓟⎤.
  Proof.
    iIntros "#H".
    iInv N as "#H2" "Hclose". Show.
    iMod ("Hclose" with "H2").
    iModIntro. iModIntro. by iNext.
  Qed.

Lemma test_iPoseProof`{inG Σ A} P γ (x y : A) :
    x ~~> y → P ∗ ⎡own γ x⎤ ==∗ ⎡own γ y⎤.
  Proof.
    iIntros (?) "[_ Hγ]".
    iPoseProof (own_update with "Hγ") as "H"; first done.
    by iMod "H".
  Qed.

Lemma test_embed_fractional`{!ghost_varG Σ A} γ q (a : A) :
    ⎡ghost_var γ q a⎤ ⊢@{monPredI} ⎡ghost_var γ (q/2) a⎤ ∗ ⎡ghost_var γ (q/2) a⎤.
  Proof. iIntros "[$ $]". Qed.

Lemma test_embed_combine`{!ghost_varG Σ A} γ q (a1 a2 : A) :
    ▷ ⎡ghost_var γ (q/2) a1⎤ ∗ ▷ ⎡ghost_var γ (q/2) a2⎤ ⊢@{monPredI}
            ▷⎡ghost_var γ q a1⎤ ∗ ▷ ⌜a1 = a2⌝.
  Proof.
    iIntros "[H1 H2]".
    iCombine "H1 H2" as "$" gives "#H". iNext.
    by iDestruct "H" as %[_ ->].
  Qed.