phanerozoic/Coq-Iris huggingface dataset:
(* tests/proofmode_ascii.v *)
(* test selection by hypothesis name instead of namespace *)
Lemma test_iInv_10 t N1 N2 N3 E1 E2 P:
    ↑N3 ⊆ E1 ->
    inv N1 P ** na_inv t N3 (<pers> P) ** inv N2 P ** na_own t E1 ** na_own t E2
      ={⊤}=* na_own t E1 ** na_own t E2 ** |> P.
Proof.
    iIntros (?) "(#?&#HInv&#?&Hown1&Hown2)".
    iInv "HInv" as "(#HP&Hown1)".
    iModIntro. iSplitL "Hown1"; auto with iFrame.
  Qed.
(* tests/proofmode_ascii.v *)
(* test selection by ident name *)
Lemma test_iInv_11 N P: inv N (<pers> P) ={⊤}=* |> P.
Proof.
    let H := iFresh in
    (iIntros H; iInv H as "#H2"). auto.
  Qed.
(* tests/proofmode_ascii.v *)
Lemma test_iInv_12 N P: inv N (<pers> P) ={⊤}=* True.
Proof.
    iIntros "H".
    Fail iInv 34 as "#H2".
    Fail iInv nroot as "#H2".
    Fail iInv "H2" as "#H2".
    done.
  Qed.
(* tests/proofmode_ascii.v *)
(* test destruction of existentials when opening an invariant *)
Lemma test_iInv_13 N:
    inv N (∃ (v1 v2 v3 : nat), emp ** emp ** emp) ={⊤}=* |> emp.
Proof.
    iIntros "H"; iInv "H" as (v1 v2 v3) "(?&?&_)".
    eauto.
  Qed.
(* tests/proofmode_ascii.v *)
Theorem test_iApply_inG `{!inG Σ A} γ (x x' : A) :
    x' ≼ x ->
    own γ x -* own γ x'.
Proof. intros. by iApply own_mono. Qed.
(* tests/proofmode_ascii.v *)
Notation monPred
:= (monPred I (iPropI Σ)).
(* tests/proofmode_ascii.v *)
Notation monPredI
:= (monPredI I (iPropI Σ)).
(* tests/proofmode_ascii.v *)
Lemma test_iInv N E 𝓟 :
    ↑N ⊆ E ->
    ⎡inv N 𝓟⎤ |-@{monPredI} |={E}=> emp.
Proof.
    iIntros (?) "Hinv".
    iInv N as "HP". Show.
    iFrame "HP". auto.
  Qed.
(* tests/proofmode_ascii.v *)
Lemma test_iInv_with_close N E 𝓟 :
    ↑N ⊆ E ->
    ⎡inv N 𝓟⎤ |-@{monPredI} |={E}=> emp.
Proof.
    iIntros (?) "Hinv".
    iInv N as "HP" "Hclose". Show.
    iMod ("Hclose" with "HP"). auto.
  Qed.
(* tests/proofmode_ascii.v *)
Lemma test_bi_emp_valid : |-@{PROP} True.
Proof. naive_solver. Qed.
(* tests/proofmode_ascii.v *)
Lemma test_bi_emp_valid_parens : (|-@{PROP} True) /\ ((|-@{PROP} True)).
Proof. naive_solver. Qed.
(* tests/proofmode_ascii.v *)
Lemma test_bi_emp_valid_parens_space_open : ( |-@{PROP} True).
Proof. naive_solver. Qed.
(* tests/proofmode_ascii.v *)
Lemma test_bi_emp_valid_parens_space_close : (|-@{PROP} True ).
Proof. naive_solver. Qed.
(* tests/proofmode_ascii.v *)
Lemma test_entails_annot_sections P :
  (P |-@{PROP} P) /\ (|-@{PROP}) P P /\
  (P -|-@{PROP} P) /\ (-|-@{PROP}) P P.
Proof. naive_solver. Qed.
(* tests/proofmode_ascii.v *)
Lemma test_entails_annot_sections_parens P :
  ((P |-@{PROP} P)) /\ ((|-@{PROP})) P P /\
  ((P -|-@{PROP} P)) /\ ((-|-@{PROP})) P P.
Proof. naive_solver. Qed.
(* tests/proofmode_ascii.v *)
Lemma test_entails_annot_sections_space_open P :
  ( P |-@{PROP} P) /\
  ( P -|-@{PROP} P).
Proof. naive_solver. Qed.
(* tests/proofmode_ascii.v *)
Lemma test_entails_annot_sections_space_close P :
  (P |-@{PROP} P ) /\ (|-@{PROP} ) P P /\
  (P -|-@{PROP} P ) /\ (-|-@{PROP} ) P P.
Proof. naive_solver. Qed.
(* tests/proofmode_ascii.v *)
Lemma p1 : forall P, True -> P |- P.
Proof.
  Unset Printing Notations. Set Printing Raw Literals. Show. Set Printing Notations. Unset Printing Raw Literals.
Abort.
(* tests/proofmode_ascii.v *)
Lemma p2 : forall P, True /\ (P |- P).
Proof.
  Unset Printing Notations. Set Printing Raw Literals. Show. Set Printing Notations. Unset Printing Raw Literals.
Abort.
(* tests/proofmode_ascii.v *)
Lemma p3 : exists P, P |- P.
Proof.
  Unset Printing Notations. Set Printing Raw Literals. Show. Set Printing Notations. Unset Printing Raw Literals.
Abort.
(* tests/proofmode_ascii.v *)
Lemma p4 : |-@{PROP} exists (x : nat), ⌜x = 0⌝.
Proof.
  Unset Printing Notations. Set Printing Raw Literals. Show. Set Printing Notations. Unset Printing Raw Literals.
Abort.
(* tests/proofmode_ascii.v *)
Lemma p5 : |-@{PROP} exists (x : nat), ⌜forall y : nat, y = y⌝.
Proof.
  Unset Printing Notations. Set Printing Raw Literals. Show. Set Printing Notations. Unset Printing Raw Literals.
Abort.
(* tests/proofmode_ascii.v *)
Lemma p6 : exists! (z : nat), |-@{PROP} exists (x : nat), ⌜forall y : nat, y = y⌝ ** ⌜z = 0⌝.
Proof.
  Unset Printing Notations. Set Printing Raw Literals. Show. Set Printing Notations. Unset Printing Raw Literals.
Abort.
(* tests/proofmode_ascii.v *)
Lemma p7 : forall (a : nat), a = 0 -> forall y, True |-@{PROP} ⌜y >= 0⌝.
Proof.
  Unset Printing Notations. Set Printing Raw Literals. Show. Set Printing Notations. Unset Printing Raw Literals.
Abort.
(* tests/proofmode_ascii.v *)
Lemma p8 : forall (a : nat), a = 0 -> forall y, |-@{PROP} ⌜y >= 0⌝.
Proof.
  Unset Printing Notations. Set Printing Raw Literals. Show. Set Printing Notations. Unset Printing Raw Literals.
Abort.
(* tests/proofmode_ascii.v *)
Lemma p9 : forall (a : nat), a = 0 -> forall y : nat, |-@{PROP} forall z : nat, ⌜z >= 0⌝.
Proof.
  Unset Printing Notations. Set Printing Raw Literals. Show. Set Printing Notations. Unset Printing Raw Literals.
Abort.
(* tests/proofmode_iris.v *)
Lemma test_random_stuff (P1 P2 P3 : nat → uPred M) :
    ⊢ ∀ (x y : nat) a b,
      x ≡ y →
      □ (uPred_ownM (a ⋅ b) -∗
      (∃ y1 y2 c, P1 ((x + y1) + y2) ∧ True ∧ □ uPred_ownM c) -∗
      □ ▷ (∀ z, P2 z ∨ True → P2 z) -∗
      ▷ (∀ n m : nat, P1 n → □ ((True ∧ P2 n) → □ (⌜n = n⌝ ↔ P3 n))) -∗
      ▷ ⌜x = 0⌝ ∨ ∃ x z, ▷ P3 (x + z) ∗ uPred_ownM b ∗ uPred_ownM (core b)).
Proof.
    iIntros (i [|j] a b ?) "!> [Ha Hb] H1 #H2 H3"; setoid_subst.
    { iLeft. by iNext. }
    iRight.
    iDestruct "H1" as (z1 z2 c) "(H1&_&#Hc)".
    iPoseProof "Hc" as "foo".
    iRevert (a b) "Ha Hb". iIntros (b a) "Hb {foo} Ha".
    iAssert (uPred_ownM (a ⋅ core a)) with "[Ha]" as "[Ha #Hac]".
    { by rewrite cmra_core_r. }
    iIntros "{$Hac $Ha}".
    iExists (S j + z1), z2.
    iNext.
    iApply ("H3" $! _ 0 with "[$]").
    - iSplit; first done. iApply "H2". iLeft. iApply "H2". by iRight.
    - done.
  Qed.
(* tests/proofmode_iris.v *)
Lemma test_iFrame_pure (x y z : M) :
    ✓ x → ⌜y ≡ z⌝ -∗ (✓ x ∧ ✓ x ∧ y ≡ z : uPred M).
Proof. iIntros (Hv) "Hxy". by iFrame (Hv) "Hxy". Qed.
(* tests/proofmode_iris.v *)
Lemma test_iAssert_modality P : (|==> False) -∗ |==> P.
Proof. iIntros. iAssert False%I with "[> - //]" as %[]. Qed.
(* tests/proofmode_iris.v *)
Lemma test_iStartProof_1 P : P -∗ P.
Proof. iStartProof. iStartProof. iIntros "$". Qed.
(* tests/proofmode_iris.v *)
Lemma test_iStartProof_2 P : P -∗ P.
Proof. iStartProof (uPred _). iStartProof (uPredI _). iIntros "$". Qed.
(* tests/proofmode_iris.v *)
Lemma test_iStartProof_3 P : P -∗ P.
Proof. iStartProof (uPredI _). iStartProof (uPredI _). iIntros "$". Qed.
(* tests/proofmode_iris.v *)
Lemma test_iStartProof_4 P : P -∗ P.
Proof. iStartProof (uPredI _). iStartProof (uPred _). iIntros "$". Qed.
(* tests/proofmode_iris.v *)
Lemma test_except_0_inv N P : ▷ False -∗ inv N P.
Proof.
    iIntros "H". by iMod "H". (* works because invariants are [IsExcept0] *)
  Qed.
(* tests/proofmode_iris.v *)
Lemma test_masks  N E P Q R :
    ↑N ⊆ E →
    (True -∗ P -∗ inv N Q -∗ True -∗ R) -∗ P -∗ ▷ Q ={E}=∗ R.
Proof.
    iIntros (?) "H HP HQ".
    iApply ("H" with "[% //] [$] [> HQ] [> //]").
    by iApply inv_alloc.
  Qed.
(* tests/proofmode_iris.v *)
Lemma test_iInv_0 N P: inv N (<pers> P) ={⊤}=∗ ▷ P.
Proof.
    iIntros "#H".
    iInv N as "#H2". Show.
    iModIntro. iSplit; auto.
  Qed.
(* tests/proofmode_iris.v *)
Lemma test_iInv_0_with_close N P: inv N (<pers> P) ={⊤}=∗ ▷ P.
Proof.
    iIntros "#H".
    iInv N as "#H2" "Hclose". Show.
    iMod ("Hclose" with "H2").
    iModIntro. by iNext.
  Qed.
(* tests/proofmode_iris.v *)
Lemma test_iInv_1 N E P:
    ↑N ⊆ E →
    inv N (<pers> P) ={E}=∗ ▷ P.
Proof.
    iIntros (?) "#H".
    iInv N as "#H2".
    iModIntro. iSplit; auto.
  Qed.
(* tests/proofmode_iris.v *)
Lemma test_iInv_2 γ p N P:
    cinv N γ (<pers> P) ∗ cinv_own γ p ={⊤}=∗ cinv_own γ p ∗ ▷ P.
Proof.
    Show.
    iIntros "(#?&?)".
    iInv N as "(#HP&Hown)". Show.
    iModIntro. iSplit; auto with iFrame.
  Qed.
(* tests/proofmode_iris.v *)
Lemma test_iInv_2_with_close γ p N P:
    cinv N γ (<pers> P) ∗ cinv_own γ p ={⊤}=∗ cinv_own γ p ∗ ▷ P.
Proof.
    iIntros "(#?&?)".
    iInv N as "(#HP&Hown)" "Hclose". Show.
    iMod ("Hclose" with "HP").
    iModIntro. iFrame. by iNext.
  Qed.
(* tests/proofmode_iris.v *)
Lemma test_iInv_3 γ p1 p2 N P:
    cinv N γ (<pers> P) ∗ cinv_own γ p1 ∗ cinv_own γ p2
      ={⊤}=∗ cinv_own γ p1 ∗ cinv_own γ p2  ∗ ▷ P.
Proof.
    iIntros "(#?&Hown1&Hown2)".
    iInv N with "[Hown2 //]" as "(#HP&Hown2)".
    iModIntro. iSplit; auto with iFrame.
  Qed.
(* tests/proofmode_iris.v *)
Lemma test_iInv_4 t N E1 E2 P:
    ↑N ⊆ E2 →
    na_inv t N (<pers> P) ∗ na_own t E1 ∗ na_own t E2
       ={⊤}=∗ na_own t E1 ∗ na_own t E2  ∗ ▷ P.
Proof.
    iIntros (?) "(#?&Hown1&Hown2)".
    iInv N as "(#HP&Hown2)". Show.
    iModIntro. iSplitL "Hown2"; auto with iFrame.
  Qed.
(* tests/proofmode_iris.v *)
Lemma test_iInv_4_with_close t N E1 E2 P:
    ↑N ⊆ E2 →
    na_inv t N (<pers> P) ∗ na_own t E1 ∗ na_own t E2
         ={⊤}=∗ na_own t E1 ∗ na_own t E2  ∗ ▷ P.
Proof.
    iIntros (?) "(#?&Hown1&Hown2)".
    iInv N as "(#HP&Hown2)" "Hclose". Show.
    iMod ("Hclose" with "[HP Hown2]").
    { iFrame. done. }
    iModIntro. iFrame. by iNext.
  Qed.
(* tests/proofmode_iris.v *)
(* test named selection of which na_own to use *)
Lemma test_iInv_5 t N E1 E2 P:
    ↑N ⊆ E2 →
    na_inv t N (<pers> P) ∗ na_own t E1 ∗ na_own t E2
      ={⊤}=∗ na_own t E1 ∗ na_own t E2  ∗ ▷ P.
Proof.
    iIntros (?) "(#?&Hown1&Hown2)".
    iInv N with "Hown2" as "(#HP&Hown2)".
    iModIntro. iSplitL "Hown2"; auto with iFrame.
  Qed.
(* tests/proofmode_iris.v *)
Lemma test_iInv_6 t N E1 E2 P:
    ↑N ⊆ E1 →
    na_inv t N (<pers> P) ∗ na_own t E1 ∗ na_own t E2
      ={⊤}=∗ na_own t E1 ∗ na_own t E2  ∗ ▷ P.
Proof.
    iIntros (?) "(#?&Hown1&Hown2)".
    iInv N with "Hown1" as "(#HP&Hown1)".
    iModIntro. iSplitL "Hown1"; auto with iFrame.
  Qed.
(* tests/proofmode_iris.v *)
(* test robustness in presence of other invariants *)
Lemma test_iInv_7 t N1 N2 N3 E1 E2 P:
    ↑N3 ⊆ E1 →
    inv N1 P ∗ na_inv t N3 (<pers> P) ∗ inv N2 P  ∗ na_own t E1 ∗ na_own t E2
      ={⊤}=∗ na_own t E1 ∗ na_own t E2  ∗ ▷ P.
Proof.
    iIntros (?) "(#?&#?&#?&Hown1&Hown2)".
    iInv N3 with "Hown1" as "(#HP&Hown1)".
    iModIntro. iSplitL "Hown1"; auto with iFrame.
  Qed.
(* tests/proofmode_iris.v *)
(* iInv should work even where we have "inv N P" in which P contains an evar *)
Lemma test_iInv_8 N : ∃ P, inv N P ={⊤}=∗ P ≡ True ∧ inv N P.
Proof.
    eexists. iIntros "#H".
    iInv N as "HP". iFrame "HP". auto.
  Qed.
(* tests/proofmode_iris.v *)
(* test selection by hypothesis name instead of namespace *)
Lemma test_iInv_9 t N1 N2 N3 E1 E2 P:
    ↑N3 ⊆ E1 →
    inv N1 P ∗ na_inv t N3 (<pers> P) ∗ inv N2 P  ∗ na_own t E1 ∗ na_own t E2
      ={⊤}=∗ na_own t E1 ∗ na_own t E2  ∗ ▷ P.
Proof.
    iIntros (?) "(#?&#HInv&#?&Hown1&Hown2)".
    iInv "HInv" with "Hown1" as "(#HP&Hown1)".
    iModIntro. iSplitL "Hown1"; auto with iFrame.
  Qed.
(* tests/proofmode_iris.v *)
(* test selection by hypothesis name instead of namespace *)
Lemma test_iInv_10 t N1 N2 N3 E1 E2 P:
    ↑N3 ⊆ E1 →
    inv N1 P ∗ na_inv t N3 (<pers> P) ∗ inv N2 P  ∗ na_own t E1 ∗ na_own t E2
      ={⊤}=∗ na_own t E1 ∗ na_own t E2  ∗ ▷ P.
Proof.
    iIntros (?) "(#?&#HInv&#?&Hown1&Hown2)".
    iInv "HInv" as "(#HP&Hown1)".
    iModIntro. iSplitL "Hown1"; auto with iFrame.
  Qed.
(* tests/proofmode_iris.v *)
(* test selection by ident name *)
Lemma test_iInv_11 N P: inv N (<pers> P) ={⊤}=∗ ▷ P.
Proof.
    let H := iFresh in
    (iIntros H; iInv H as "#H2"). auto.
  Qed.
(* tests/proofmode_iris.v *)
Lemma test_iInv_12 N P: inv N (<pers> P) ={⊤}=∗ True.
Proof.
    iIntros "H".
    Fail iInv 34 as "#H2".
    Fail iInv nroot as "#H2".
    Fail iInv "H2" as "#H2".
    done.
  Qed.
(* tests/proofmode_iris.v *)
Lemma test_iInv_error_no_update N P : inv N P -∗ True.
Proof.
    iIntros "H".
    Fail iInv N as "H".
  Abort.
(* tests/proofmode_iris.v *)
(* test destruction of existentials when opening an invariant *)
Lemma test_iInv_13 N:
    inv N (∃ (v1 v2 v3 : nat), emp ∗ emp ∗ emp) ={⊤}=∗ ▷ emp.
Proof.
    iIntros "H"; iInv "H" as (v1 v2 v3) "(?&?&_)".
    eauto.
  Qed.
(* tests/proofmode_iris.v *)
Lemma test_iInv_accessor_variable Φ : INV Φ ={⊤}=∗ INV Φ.
Proof.
      iIntros "HINV".
      (* There are 4 variants of [iInv] that we have to test *)
      (* No selection pattern, no closing view shift *)
      Fail iInv "HINV" as "HINVinner".
      iInv "HINV" as (b) "HINVinner"; rename b into b_exists. Undo.
      (* Both sel.pattern and closing view shift *)
      Fail iInv "HINV" with "[//]" as "HINVinner" "Hclose".
      iInv "HINV" with "[//]" as (b) "HINVinner" "Hclose";
        rename b into b_exists. Undo.
      (* Sel.pattern but no closing view shift *)
      Fail iInv "HINV" with "[//]" as "HINVinner".
      iInv "HINV" with "[//]" as (b) "HINVinner"; rename b into b_exists. Undo.
      (* Closing view shift, no selection pattern *)
      Fail iInv "HINV" as "HINVinner" "Hclose".
      iInv "HINV" as (b) "HINVinner" "Hclose"; rename b into b_exists.
      by iApply "Hclose".
    Qed.
(* tests/proofmode_iris.v *)
Theorem test_iApply_inG `{!inG Σ A} γ (x x' : A) :
    x' ≼ x →
    own γ x -∗ own γ x'.
Proof. intros. by iApply own_mono. Qed.
(* tests/proofmode_iris.v *)
Lemma test_frac_split_combine `{!inG Σ fracR} γ :
    own γ 1%Qp -∗ own γ 1%Qp.
Proof.
    iIntros "[H1 H2]". Show.
    iCombine "H1 H2" as "H". Show.
    iExact "H".
  Qed.
(* tests/proofmode_iris.v *)
Lemma test_iDestruct_mod_not_fresh P Q :
    P -∗ (|={⊤}=> Q) -∗ (|={⊤}=> False).
Proof.
    iIntros "H H'". Fail iDestruct "H'" as ">H".
  Abort.
(* tests/proofmode_iris.v *)
Lemma test_iIntros_lc n m : £ (S n + m) -∗ £ (S n).
Proof. iIntros "[Hlc1 Hlc2]". Show. iExact "Hlc1". Qed.
(* tests/proofmode_iris.v *)
Lemma lc_iSplit_lc n m : £ (S n) -∗ £ m -∗ £ (S n + m).
Proof. iIntros "Hlc1 Hlc2". iSplitL "Hlc1". Show. all: done. Qed.
(* tests/proofmode_iris.v *)
Lemma test_iCombine_ghost_var_no_beta `{!ghost_varG Σ nat} l (v : nat) q1 q2 :
    l ↪VAR{#q1} v -∗ l ↪VAR{#q2} v -∗ l ↪VAR{#q1+q2} v.
Proof.
    iIntros "H1 H2". iCombine "H1 H2" as "H". Show. done.
  Qed.
(* tests/proofmode_iris.v *)
Lemma iMod_WP_mask_mismatch E1 E2 P (e : expr Λ) :
    (|={E2}=> P) ⊢ WP e @ E1 {{ _, True }}.
Proof.
    Fail iIntros ">HP".
    iIntros "HP". Fail iMod "HP".
    iApply fupd_wp; iMod (fupd_mask_subseteq E2).
  Abort.
(* tests/proofmode_iris.v *)
Lemma iMod_WP_atomic_mask_mismatch E1 E2 E2' P (e : expr Λ) :
    (|={E2,E2'}=> P) ⊢ WP e @ E1 {{ _, True }}.
Proof.
    Fail iIntros ">HP".
    iIntros "HP". Fail iMod "HP".
    iMod (fupd_mask_subseteq E2).
  Abort.
(* tests/proofmode_iris.v *)
Lemma iFrame_WP_no_instantiate (e : expr Λ) (Φ : nat → iProp Σ) :
    □ Φ 0 ⊢ WP e {{ _, Φ 0 ∗ ∃ n, Φ n }}.
Proof.
    iIntros "#$".
    (* [Φ 0] should get framed, [∃ n, Φ n] should remain untouched *)
    Show.
  Abort.
(* tests/proofmode_iris.v *)
Lemma iInv_WP (e : expr Λ) N E P :
    ↑N ⊆ E → 
    inv N P ⊢ WP e @ E {{ _, True }}.
Proof.
    iIntros (?) "Hinv".
    iInv N as "HP". Show.
  Abort.
(* tests/proofmode_iris.v *)
Lemma iMod_TWP_mask_mismatch E1 E2 P (e : expr Λ) :
    (|={E2}=> P) ⊢ WP e @ E1 [{ _, True }].
Proof.
    Fail iIntros ">HP".
    iIntros "HP". Fail iMod "HP".
    iApply fupd_twp; iMod (fupd_mask_subseteq E2).
  Abort.
(* tests/proofmode_iris.v *)
Lemma iMod_TWP_atomic_mask_mismatch E1 E2 E2' P (e : expr Λ) :
    (|={E2,E2'}=> P) ⊢ WP e @ E1 [{ _, True }].
Proof.
    Fail iIntros ">HP".
    iIntros "HP". Fail iMod "HP".
    iMod (fupd_mask_subseteq E2).
  Abort.
(* tests/proofmode_iris.v *)
Lemma iFrame_TWP_no_instantiate (e : expr Λ) (Φ : nat → iProp Σ) :
    □ Φ 0 ⊢ WP e [{ _, Φ 0 ∗ ∃ n, Φ n }].
Proof.
    iIntros "#$".
    (* [Φ 0] should get framed, [∃ n, Φ n] should remain untouched *)
    Show.
  Abort.
(* tests/proofmode_iris.v *)
Lemma iInv_TWP (e : expr Λ) N E P :
    ↑N ⊆ E → 
    inv N P ⊢ WP e @ E [{ _, True }].
Proof.
    iIntros (?) "Hinv".
    iInv N as "HP". Show.
  Abort.
(* tests/proofmode_iris.v *)
Lemma test_iInv N E 𝓟 :
    ↑N ⊆ E →
    ⎡inv N 𝓟⎤ ⊢@{monPredI} |={E}=> emp.
Proof.
    iIntros (?) "Hinv".
    iInv N as "HP". Show.
    iFrame "HP". auto.
  Qed.
(* tests/proofmode_iris.v *)
Lemma test_iInv_with_close N E 𝓟 :
    ↑N ⊆ E →
    ⎡inv N 𝓟⎤ ⊢@{monPredI} |={E}=> emp.
Proof.
    iIntros (?) "Hinv".
    iInv N as "HP" "Hclose". Show.
    iMod ("Hclose" with "HP"). auto.
  Qed.
(* tests/proofmode_monpred.v *)
Lemma test0 P : P -∗ P.
Proof. iIntros "$". Qed.
(* tests/proofmode_monpred.v *)
Lemma test_iStartProof_2 P : P -∗ P.
Proof. iStartProof monPred. iStartProof monPredI. iIntros "$". Qed.
(* tests/proofmode_monpred.v *)
Lemma test_iStartProof_3 P : P -∗ P.
Proof. iStartProof monPredI. iStartProof monPredI. iIntros "$". Qed.
(* tests/proofmode_monpred.v *)
Lemma test_iStartProof_4 P : P -∗ P.
Proof. iStartProof monPredI. iStartProof monPred. iIntros "$". Qed.
(* tests/proofmode_monpred.v *)
Lemma test_iStartProof_5 P : P -∗ P.
Proof. iStartProof PROP. iIntros (i) "$". Qed.
(* tests/proofmode_monpred.v *)
Lemma test_iStartProof_6 P : P ⊣⊢ P.
Proof. iStartProof PROP. iIntros (i). iSplit; iIntros "$". Qed.
(* tests/proofmode_monpred.v *)
Lemma test_iStartProof_7 `{!Sbi PROP} P : ⊢@{monPredI} P ≡ P.
Proof. iStartProof PROP. done. Qed.
(* tests/proofmode_monpred.v *)
Lemma test_intowand_1 P Q : (P -∗ Q) -∗ P -∗ Q.
Proof.
    iStartProof PROP. iIntros (i) "HW". Show.
    iIntros (j ->) "HP". Show. by iApply "HW".
  Qed.
(* tests/proofmode_monpred.v *)
Lemma test_intowand_2 P Q : (P -∗ Q) -∗ P -∗ Q.
Proof.
    iStartProof PROP. iIntros (i) "HW". iIntros (j ->) "HP".
    iSpecialize ("HW" with "[HP //]"). done.
  Qed.
(* tests/proofmode_monpred.v *)
Lemma test_intowand_3 P Q : (P -∗ Q) -∗ P -∗ Q.
Proof.
    iStartProof PROP. iIntros (i) "HW". iIntros (j ->) "HP".
    iSpecialize ("HW" with "HP"). done.
  Qed.
(* tests/proofmode_monpred.v *)
Lemma test_intowand_4 P Q : (P -∗ Q) -∗ ▷ P -∗ ▷ Q.
Proof.
    iStartProof PROP. iIntros (i) "HW". iIntros (j ->) "HP". by iApply "HW".
  Qed.
(* tests/proofmode_monpred.v *)
Lemma test_intowand_5 P Q : (P -∗ Q) -∗ ▷ P -∗ ▷ Q.
Proof.
    iStartProof PROP. iIntros (i) "HW". iIntros (j ->) "HP".
    iSpecialize ("HW" with "HP"). done.
  Qed.
(* tests/proofmode_monpred.v *)
Lemma test_apply_in_elim (P : monPredI) (i : I) : monPred_in i -∗ ⎡ P i ⎤ → P.
Proof. iIntros. by iApply monPred_in_elim. Qed.
(* tests/proofmode_monpred.v *)
Lemma test_iStartProof_forall_1 (Φ : nat → monPredI) : ∀ n, Φ n -∗ Φ n.
Proof.
    iStartProof PROP. iIntros (n i) "$".
  Qed.
(* tests/proofmode_monpred.v *)
Lemma test_iStartProof_forall_2 (Φ : nat → monPredI) : ∀ n, Φ n -∗ Φ n.
Proof.
    iStartProof. iIntros (n) "$".
  Qed.
(* tests/proofmode_monpred.v *)
Lemma test_embed_wand (P Q : PROP) : (⎡P⎤ -∗ ⎡Q⎤) ⊢@{monPredI} ⎡P -∗ Q⎤.
Proof.
    iIntros "H HP". by iApply "H".
  Qed.
(* tests/proofmode_monpred.v *)
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.
(* tests/proofmode_monpred.v *)
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.
(* tests/proofmode_monpred.v *)
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.
(* tests/proofmode_monpred.v *)
Lemma test_iModIntro_embed P `{!Affine Q} 𝓟 𝓠 :
    □ P -∗ Q -∗ ⎡𝓟⎤ -∗ ⎡𝓠⎤ -∗ ⎡ 𝓟 ∗ 𝓠 ⎤.
Proof. iIntros "#H1 _ H2 H3". iModIntro. iFrame. Qed.
(* tests/proofmode_monpred.v *)
Lemma test_iModIntro_embed_objective P `{!Objective Q} 𝓟 𝓠 :
    □ P -∗ Q -∗ ⎡𝓟⎤ -∗ ⎡𝓠⎤ -∗ ⎡ ∀ i, 𝓟 ∗ 𝓠 ∗ Q i ⎤.
Proof. iIntros "#H1 H2 H3 H4". iModIntro. Show. iFrame. Qed.
(* tests/proofmode_monpred.v *)
Lemma test_iModIntro_embed_nested P 𝓟 𝓠 :
    □ P -∗ ⎡◇ 𝓟⎤ -∗ ⎡◇ 𝓠⎤ -∗ ⎡ ◇ (𝓟 ∗ 𝓠) ⎤.
Proof. iIntros "#H1 H2 H3". iModIntro ⎡ _ ⎤%I. by iSplitL "H2". Qed.
(* tests/proofmode_monpred.v *)
Lemma test_into_wand_embed 𝓟 𝓠 :
    (𝓟 -∗ ◇ 𝓠) →
    ⎡𝓟⎤ ⊢@{monPredI} ◇ ⎡𝓠⎤.
Proof.
    iIntros (HPQ) "HP".
    iMod (HPQ with "[-]") as "$"; last by auto.
    iAssumption.
  Qed.
(* tests/proofmode_monpred.v *)
Lemma test_monPred_at_and_pure P i j :
    (monPred_in j ∧ P) i ⊢ ⌜ j ⊑ i ⌝ ∧ P i.
Proof.
    iDestruct 1 as "[% $]". done.
  Qed.
(* tests/proofmode_monpred.v *)
Lemma test_monPred_at_sep_pure P i j :
    (monPred_in j ∗ <absorb> P) i ⊢ ⌜ j ⊑ i ⌝ ∧ <absorb> P i.
Proof.
    iDestruct 1 as "[% ?]". auto.
  Qed.
(* tests/proofmode_monpred.v *)
Lemma test_apply_fupd_intro_mask_subseteq E1 E2 P :
    E2 ⊆ E1 → P -∗ |={E1,E2}=> |={E2,E1}=> P.
Proof. iIntros. by iApply @fupd_mask_intro_subseteq. Qed.
(* tests/proofmode_monpred.v *)
Lemma test_apply_fupd_mask_subseteq E1 E2 P :
    E2 ⊆ E1 → P -∗ |={E1,E2}=> |={E2,E1}=> P.
Proof. iIntros. iFrame. by iApply @fupd_mask_subseteq. Qed.
(* tests/proofmode_monpred.v *)
Lemma test_iFrame_embed_persistent (P : PROP) (Q: monPred) :
    Q ∗ □ ⎡P⎤ ⊢ Q ∗ ⎡P ∗ P⎤.
Proof.
    iIntros "[$ #HP]". iFrame "HP".
  Qed.
(* tests/proofmode_monpred.v *)
Lemma test_iNext_Bi P :
    ▷ P ⊢@{monPredI} ▷ P.
Proof. iIntros "H". by iNext. Qed.
(* tests/proofmode_monpred.v *)
(* Test monPred_at framing *)
Lemma test_iFrame_monPred_at_wand (P Q : monPred) i :
    P i -∗ (Q -∗ P) i.
Proof. iIntros "$". Show. Abort.
(* tests/proofmode_monpred.v *)
Definition monPred_id (R : monPred) : monPred :=
    MonPred (λ V, R V) _.
Next Obligation. intros ? ???. eauto. Qed.
(* tests/proofmode_monpred.v *)
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.
(* tests/proofmode_monpred.v *)
Lemma test_iFrame_rel P i j ij :
    IsBiIndexRel i ij → IsBiIndexRel j ij →
    P i -∗ P j -∗ P ij ∗ P ij.
Proof. iIntros (??) "HPi HPj". iFrame. Qed.
(* tests/proofmode_monpred.v *)
Lemma test_iFrame_later_rel `{!BiAffine PROP} P i j :
    IsBiIndexRel i j →
    ▷ (P i) -∗ (▷ P) j.
Proof. iIntros (?) "?". iFrame. Qed.
(* tests/proofmode_monpred.v *)
Lemma test_iFrame_laterN n P i :
    ▷^n (P i) -∗ (▷^n P) i.
Proof. iIntros "?". iFrame. Qed.
(* tests/proofmode_monpred.v *)
Lemma test_iFrame_quantifiers P i :
    P i -∗ (∀ _:(), ∃ _:(), P) i.
Proof. iIntros "?". iFrame. Show. iIntros ([]). iExists (). iEmpIntro. Qed.
(* tests/proofmode_monpred.v *)
Lemma test_iFrame_embed (P : PROP) i :
    P -∗ (embed (B:=monPredI) P) i.
Proof. iIntros "$". Qed.
(* tests/proofmode_monpred.v *)
(* Make sure search doesn't diverge on an evar *)
Lemma test_iFrame_monPred_at_evar (P : monPred) i j :
    P i -∗ ∃ Q, (Q j).
Proof. iIntros "HP". iExists _. Fail iFrame "HP". Abort.
(* tests/proofmode_monpred.v *)
Lemma test_iInv_0 N 𝓟 :
    embed (B:=monPred) (inv N (<pers> 𝓟)) ={⊤}=∗ ⎡▷ 𝓟⎤.
Proof.
    iIntros "#H".
    iInv N as "#H2". Show.
    iModIntro. iSplit=>//. iModIntro. iModIntro; auto.
  Qed.
(* tests/proofmode_monpred.v *)
Lemma test_iInv_0_with_close N 𝓟 :
    embed (B:=monPred) (inv N (<pers> 𝓟)) ={⊤}=∗ ⎡▷ 𝓟⎤.
Proof.
    iIntros "#H".
    iInv N as "#H2" "Hclose". Show.
    iMod ("Hclose" with "H2").
    iModIntro. iModIntro. by iNext.
  Qed.
(* tests/proofmode_monpred.v *)
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.
(* tests/proofmode_monpred.v *)
Lemma test_embed_fractional `{!ghost_varG Σ A} γ q (a : A) :
    ⎡γ ↪VAR{#q} a⎤ ⊢@{monPredI} ⎡γ  ↪VAR{#q/2} a⎤ ∗ ⎡γ  ↪VAR{#q/2} a⎤.
Proof. iIntros "[$ $]". Qed.
(* tests/proofmode_monpred.v *)
Lemma test_embed_combine `{!ghost_varG Σ A} γ q (a1 a2 : A) :
    ▷ ⎡γ ↪VAR{#q/2} a1⎤ ∗ ▷ ⎡γ ↪VAR{#q/2} a2⎤ ⊢@{monPredI}
            ▷⎡γ ↪VAR{#q} a1⎤ ∗ ▷ ⌜a1 = a2⌝.
Proof.
    iIntros "[H1 H2]".
    iCombine "H1 H2" as "$" gives "#H". iNext.
    by iDestruct "H" as %[_ ->].
  Qed.
(* tests/proofmode_siprop.v *)
Lemma test_everything_persistent P : P -∗ P.
Proof. by iIntros "#HP". Qed.
(* tests/proofmode_siprop.v *)
Lemma test_everything_affine P : P -∗ True.
Proof. by iIntros "_". Qed.