phanerozoic/Coq-Iris huggingface dataset:
(* tests/one_shot.v *)
Lemma wp_one_shot (Φ : val → iProp Σ) :
  (∀ f1 f2 : val,
    (∀ n : Z, □ WP f1 #n {{ w, ⌜w = #true⌝ ∨ ⌜w = #false⌝ }}) ∗
    □ WP f2 #() {{ (g : val), □ WP g #() {{ _, True }} }} -∗ Φ (f1,f2)%V)
  ⊢ WP one_shot_example #() {{ Φ }}.
Proof.
  iIntros "Hf /=". pose proof (nroot .@ "N") as N.
  wp_lam. wp_alloc l as "Hl".
  iMod (own_alloc Pending) as (γ) "Hγ"; first done.
  iMod (inv_alloc N _ (one_shot_inv γ l) with "[Hl Hγ]") as "#HN".
  { iNext. iLeft. by iSplitL "Hl". }
  wp_pures. iModIntro. iApply "Hf"; iSplit.
  - iIntros (n) "!>". wp_lam. wp_pures. wp_bind (CmpXchg _ _ _).
    iInv N as ">[[Hl Hγ]|H]"; last iDestruct "H" as (m) "[Hl Hγ]".
    + iMod (own_update with "Hγ") as "Hγ".
      { by apply cmra_update_exclusive with (y:=Shot n). }
      wp_cmpxchg_suc. iModIntro. iSplitL; last (wp_pures; by eauto).
      iNext; iRight; iExists n; by iFrame.
    + wp_cmpxchg_fail. iModIntro. iSplitL; last (wp_pures; by eauto).
      rewrite /one_shot_inv; eauto 10.
  - iIntros "!> /=". wp_lam. wp_bind (! _)%E.
    iInv N as ">Hγ".
    iAssert (∃ v, l ↦ v ∗ ((⌜v = NONEV⌝ ∗ own γ Pending) ∨
       ∃ n : Z, ⌜v = SOMEV #n⌝ ∗ own γ (Shot n)))%I with "[Hγ]" as "Hv".
    { iDestruct "Hγ" as "[[Hl Hγ]|Hl]"; last iDestruct "Hl" as (m) "[Hl Hγ]".
      + iExists NONEV. iFrame. eauto.
      + iExists (SOMEV #m). iFrame. eauto. }
    iDestruct "Hv" as (v) "[Hl Hv]". wp_load.
    iAssert (one_shot_inv γ l ∗ (⌜v = NONEV⌝ ∨ ∃ n : Z,
      ⌜v = SOMEV #n⌝ ∗ own γ (Shot n)))%I with "[Hl Hv]" as "[Hinv #Hv]".
    { iDestruct "Hv" as "[[% ?]|Hv]"; last iDestruct "Hv" as (m) "[% ?]"; subst.
      + Show. iSplit.
        * iLeft; by iSplitL "Hl".
        * eauto.
      + iSplit.
        * iRight; iExists m; by iSplitL "Hl".
        * eauto. }
    iSplitL "Hinv"; first by eauto.
    iModIntro. wp_pures. iIntros "!> !>". wp_lam.
    iDestruct "Hv" as "[%|Hv]"; last iDestruct "Hv" as (m) "[% Hγ']";
      subst; wp_match; [done|].
    wp_bind (! _)%E.
    iInv N as "[[Hl >Hγ]|H]"; last iDestruct "H" as (m') "[Hl Hγ]".
    { by iCombine "Hγ Hγ'" gives %?. }
    wp_load. Show.
    iCombine "Hγ Hγ'" gives %?%to_agree_op_inv_L; subst.
    iModIntro. iSplitL "Hl".
    { iNext; iRight; by eauto. }
    wp_smart_apply wp_assert. wp_pures. by case_bool_decide.
Qed.
(* tests/one_shot.v *)
Lemma ht_one_shot (Φ : val → iProp Σ) :
  ⊢ {{ True }} one_shot_example #()
    {{ ff,
      (∀ n : Z, {{ True }} Fst ff #n {{ w, ⌜w = #true⌝ ∨ ⌜w = #false⌝ }}) ∗
      {{ True }} Snd ff #() {{ g, {{ True }} g #() {{ _, True }} }}
    }}.
Proof.
  iIntros "!> _". iApply wp_one_shot. iIntros (f1 f2) "[#Hf1 #Hf2]"; iSplit.
  - iIntros (n) "!> _". wp_smart_apply "Hf1".
  - iIntros "!> _". wp_smart_apply (wp_wand with "Hf2"). by iIntros (v) "#? !> _".
Qed.
(* tests/one_shot.v *)
(* Have a client with a closed proof. *)
Definition client : expr
:=
  let: "ff" := one_shot_example #() in
  (Fst "ff" #5 ||| let: "check" := Snd "ff" #() in "check" #()).
(* tests/one_shot.v *)
Lemma client_safe : ⊢ WP client {{ _, True }}.
Proof using Type*.
    rewrite /client. wp_apply wp_one_shot. iIntros (f1 f2) "[#Hf1 #Hf2]".
    wp_let. wp_smart_apply wp_par.
    - wp_smart_apply "Hf1".
    - wp_proj. wp_bind (f2 _)%E. iApply wp_wand; first by iExact "Hf2".
      iIntros (check) "Hcheck". wp_pures. iApply "Hcheck".
    - auto.
  Qed.
(* tests/one_shot.v *)
(* Put together all library functors. *)
Definition clientΣ : gFunctors
:= #[ heapΣ; one_shotΣ; spawnΣ ].
(* tests/one_shot.v *)
(* This lemma implicitly shows that these functors are enough to meet
all library assumptions. *)
Lemma client_adequate σ : adequate NotStuck client σ (λ _ _, True).
Proof. apply (heap_adequacy clientΣ)=> ?. iIntros "_". iApply client_safe. Qed.
(* tests/one_shot_once.v *)
Definition one_shot_example : val
:= λ: <>,
  let: "x" := ref NONE in (
  (* set *) (λ: "n",
    assert: CAS "x" NONE (SOME "n")),
  (* check  *) (λ: <>,
    let: "y" := !"x" in λ: <>,
      let: "y'" := !"x" in
      match: "y" with
        NONE => #()
      | SOME <> => assert: "y" = "y'"
      end)).
(* tests/one_shot_once.v *)
Definition one_shotR
:= csumR fracR (agreeR ZO).
(* tests/one_shot_once.v *)
Definition Pending (q : Qp) : one_shotR
:= Cinl q.
(* tests/one_shot_once.v *)
Definition one_shot_inv (γ : gname) (l : loc) : iProp Σ
:=
  (l ↦ NONEV ∗ own γ (Pending (1/2)%Qp) ∨
   ∃ n : Z, l ↦ SOMEV #n ∗ own γ (Shot n))%I.
(* tests/one_shot_once.v *)
Lemma pending_split γ q :
  own γ (Pending q) ⊣⊢ own γ (Pending (q/2)) ∗ own γ (Pending (q/2)).
Proof.
  rewrite /Pending. rewrite -own_op -Cinl_op. rewrite frac_op Qp.div_2 //.
Qed.
(* tests/one_shot_once.v *)
Lemma pending_shoot γ n :
  own γ (Pending 1%Qp) ==∗ own γ (Shot n).
Proof.
  iIntros "Hγ". iMod (own_update with "Hγ") as "$"; last done.
  by apply cmra_update_exclusive with (y:=Shot n).
Qed.
(* tests/one_shot_once.v *)
Lemma one_shot :
  {{{ True }}}
    one_shot_example #()
  {{{ (f1 f2 : val) (T : iProp Σ), RET (f1,f2);
    T ∗
    (∀ n : Z, {{{ T }}} f1 #n {{{ RET #(); True }}}) ∗
    {{{ True }}} f2 #() {{{ (g : val), RET g; {{{ True }}} g #() {{{ RET #(); True }}} }}}
  }}}.
Proof.
  iIntros "%Φ _ HΦ /=". pose proof (nroot .@ "N") as N.
  wp_lam. wp_alloc l as "Hl".
  iMod (own_alloc (Pending 1%Qp)) as (γ) "Hγ"; first done.
  iDestruct (pending_split with "Hγ") as "[Hγ1 Hγ2]".
  iMod (inv_alloc N _ (one_shot_inv γ l) with "[Hl Hγ2]") as "#HN".
  { iNext. iLeft. by iFrame. }
  wp_pures. iModIntro. iApply ("HΦ" $! _ _ (own γ (Pending (1/2)%Qp))).
  iSplitL; first done. iSplit.
  - clear Φ. iIntros "%n !> %Φ Hγ1 HΦ". wp_pures.
    iApply wp_assert. wp_pures. wp_bind (CmpXchg _ _ _).
    iInv N as ">[[Hl Hγ2]|H]"; last iDestruct "H" as (m) "[Hl Hγ']".
    + iDestruct (pending_split with "[$Hγ1 $Hγ2]") as "Hγ".
      iMod (pending_shoot _ n with "Hγ") as "Hγ".
      wp_cmpxchg_suc. iModIntro. iSplitR "HΦ".
      * iNext; iRight; iExists n; by iFrame.
      * wp_pures. iSplitR; first done. by iApply "HΦ".
    + by iCombine "Hγ1 Hγ'" gives %?.
  - clear Φ. iIntros "!> %Φ _ HΦ /=". wp_lam. wp_bind (! _)%E.
    iInv N as ">Hγ".
    iAssert (∃ v, l ↦ v ∗ (⌜v = NONEV⌝ ∗ own γ (Pending (1/2)%Qp) ∨
       ∃ n : Z, ⌜v = SOMEV #n⌝ ∗ own γ (Shot n)))%I with "[Hγ]" as "Hv".
    { iDestruct "Hγ" as "[[Hl Hγ]|Hl]"; last iDestruct "Hl" as (m) "[Hl Hγ]".
      + iExists NONEV. iFrame. eauto.
      + iExists (SOMEV #m). iFrame. eauto. }
    iDestruct "Hv" as (v) "[Hl Hv]". wp_load.
    iAssert (one_shot_inv γ l ∗ (⌜v = NONEV⌝ ∨ ∃ n : Z,
      ⌜v = SOMEV #n⌝ ∗ own γ (Shot n)))%I with "[Hl Hv]" as "[Hinv #Hv]".
    { iDestruct "Hv" as "[[% ?]|Hv]"; last iDestruct "Hv" as (m) "[% ?]"; subst.
      + Show. iSplit.
        * iLeft; by iSplitL "Hl".
        * eauto.
      + iSplit.
        * iRight; iExists m; by iSplitL "Hl".
        * eauto. }
    iSplitL "Hinv"; first by eauto.
    iModIntro. wp_pures. iApply "HΦ".
    clear Φ. iIntros "!> %Φ !> _ HΦ". wp_lam. wp_bind (! _)%E.
    iInv N as "Hinv".
    iDestruct "Hv" as "[%|Hv]"; last iDestruct "Hv" as (m) "[% Hγ']"; subst.
    + iDestruct "Hinv" as "[[Hl >Hγ]|H]"; last iDestruct "H" as (m') "[Hl Hγ]";
      wp_load; iModIntro; (iSplitL "Hl Hγ"; first by eauto with iFrame);
      wp_pures; by iApply "HΦ".
    + iDestruct "Hinv" as "[[Hl >Hγ]|H]"; last iDestruct "H" as (m') "[Hl Hγ]".
      { by iCombine "Hγ Hγ'" gives %?. }
      wp_load. Show.
      iCombine "Hγ Hγ'" gives %?%to_agree_op_inv_L; subst.
      iModIntro. iSplitL "Hl Hγ"; first by eauto with iFrame.
      wp_pures. iApply wp_assert. wp_op.
      iSplitR; first by case_bool_decide.
      by iApply "HΦ".
Qed.
(* tests/one_shot_once.v *)
Lemma client_safe : ⊢ WP client {{ _, True }}.
Proof using Type*.
    rewrite /client. wp_apply one_shot; first done.
    iIntros (f1 f2 T) "(HT & #Hf1 & #Hf2)".
    wp_let. wp_smart_apply (wp_par (λ _, True)%I (λ _, True)%I with "[HT]").
    - wp_smart_apply ("Hf1" with "HT"). by eauto.
    - wp_proj. wp_bind (f2 _)%E. wp_apply "Hf2"; first done.
      iIntros (check) "Hcheck". wp_pures. iApply "Hcheck"; by auto.
    - auto.
  Qed.
(* tests/proofmode.v *)
Lemma test_eauto_iSplit_emp_wand_iff P : emp ⊢ P ∗-∗ P.
Proof. eauto 6. Qed.
(* tests/proofmode.v *)
Lemma test_eauto_iSplit_wand_iff P : ⊢ P ∗-∗ P.
Proof. eauto. Qed.
(* tests/proofmode.v *)
(* We get the [⊢] automatically from the notation in [stdpp_scope]. *)
Lemma test_eauto_iSplit_wand_iff_std_scope P : P ∗-∗ P.
Proof. eauto. Qed.
(* tests/proofmode.v *)
Fixpoint test_fixpoint (n : nat) {struct n} : True → emp ⊢@{PROP} ⌜ (n + 0)%nat = n ⌝.
Proof.
  case: n => [|n] /=; first (iIntros (_) "_ !%"; reflexivity).
  iIntros (_) "_".
  by iDestruct (test_fixpoint with "[//]") as %->.
Qed.
(* tests/proofmode.v *)
Lemma demo_0 `{!BiPersistentlyForall PROP} P Q :
  □ (P ∨ Q) -∗ (∀ x, ⌜x = 0⌝ ∨ ⌜x = 1⌝) → (Q ∨ P).
Proof.
  iIntros "H #H2". Show. iDestruct "H" as "###H".
  (* should remove the disjunction "H" *)
  iDestruct "H" as "[#?|#?]"; last by iLeft. Show.
  (* should keep the disjunction "H" because it is instantiated *)
  iDestruct ("H2" $! 10) as "[%|%]"; done.
Qed.
(* tests/proofmode.v *)
Lemma demo_2 P1 P2 P3 P4 Q (P5 : nat → PROP) `{!Affine P4, !Absorbing P2} :
  P2 ∗ (P3 ∗ Q) ∗ True ∗ P1 ∗ P2 ∗ (P4 ∗ (∃ x:nat, P5 x ∨ P3)) ∗ emp -∗
    P1 -∗ (True ∗ True) -∗
  (((P2 ∧ False ∨ P2 ∧ ⌜0 = 0⌝) ∗ P3) ∗ Q ∗ P1 ∗ True) ∧
     (P2 ∨ False) ∧ (False → P5 0).
Proof.
  (* Intro-patterns do something :) *)
  iIntros "[H2 ([H3 HQ]&?&H1&H2'&foo&_)] ? [??]".
  (* To test destruct: can also be part of the intro-pattern *)
  iDestruct "foo" as "[_ meh]".
  repeat iSplit; [|by iLeft|iIntros "#[]"].
  iFrame "H2". (* also simplifies the [∧ False] and [∨ False] *)
  (* split takes a list of hypotheses just for the LHS *)
  iSplitL "H3".
  - by iFrame "H3".
  - iSplitL "HQ"; first iAssumption. by iSplitL "H1".
Qed.
(* tests/proofmode.v *)
Lemma test_pure_space_separated P1 :
  <affine> ⌜True⌝ ∗ P1 -∗ P1.
Proof.
  (* [% H] should be parsed as two separate patterns and not the pure name
  [H] *)
  iIntros "[% H] //".
Qed.
(* tests/proofmode.v *)
Definition foo (P : PROP)
:= (P -∗ P)%I.
(* tests/proofmode.v *)
Definition bar : PROP
:= (∀ P, foo P)%I.
(* tests/proofmode.v *)
Lemma test_unfold_constants : ⊢ bar.
Proof. iIntros (P) "HP //". Qed.
(* tests/proofmode.v *)
Lemma test_iStopProof Q : emp -∗ Q -∗ Q.
Proof. iIntros "#H1 H2". Show. iStopProof. Show. by rewrite bi.sep_elim_r. Qed.
(* tests/proofmode.v *)
Lemma test_iRewrite `{!Sbi PROP} {A : ofe} (x y : A) P :
  □ (∀ z, P -∗ <affine> (z ≡ y)) -∗ (P -∗ P ∧ (x,x) ≡ (y,x)).
Proof.
  iIntros "#H1 H2".
  iRewrite (internal_eq_sym x x with "[# //]").
  iRewrite -("H1" $! _ with "[- //]").
  auto.
Qed.
(* tests/proofmode.v *)
Lemma test_iRewrite_dom `{!Sbi PROP} {A : ofe} (m1 m2 : gmap nat A) :
  m1 ≡ m2 ⊢@{PROP} ⌜ dom m1 = dom m2 ⌝.
Proof. iIntros "H". by iRewrite "H". Qed.
(* tests/proofmode.v *)
Lemma test_iDestruct_and_emp P Q `{!Persistent P, !Persistent Q} :
  P ∧ emp -∗ emp ∧ Q -∗ <affine> (P ∗ Q).
Proof. iIntros "[#? _] [_ #?]". Show. auto. Qed.
(* tests/proofmode.v *)
Lemma test_iIntros_persistent P Q `{!Persistent Q} : ⊢ (P → Q → P ∧ Q).
Proof. iIntros "H1 #H2". by iFrame "∗#". Qed.
(* tests/proofmode.v *)
Lemma test_iDestruct_intuitionistic_1 P Q `{!Persistent P}:
  Q ∗ □ (Q -∗ P) -∗ P ∗ Q.
Proof. iIntros "[HQ #HQP]". iDestruct ("HQP" with "HQ") as "#HP". by iFrame. Qed.
(* tests/proofmode.v *)
Lemma test_iDestruct_intuitionistic_2 P Q `{!Persistent P, !Affine P}:
  Q ∗ (Q -∗ P) -∗ P.
Proof. iIntros "[HQ HQP]". iDestruct ("HQP" with "HQ") as "#HP". done. Qed.
(* tests/proofmode.v *)
Lemma test_iDestruct_specialize_wand P Q :
  Q -∗ Q -∗ □ (Q -∗ P) -∗ P ∗ P.
Proof.
  iIntros "HQ1 HQ2 #HQP".
  (* [iDestruct] does not consume "HQP" because a wand is instantiated *)
  iDestruct ("HQP" with "HQ1") as "HP1".
  iDestruct ("HQP" with "HQ2") as "HP2".
  iFrame.
Qed.
(* tests/proofmode.v *)
Lemma test_iPoseProof_specialize_wand P Q :
  Q -∗ Q -∗ □ (Q -∗ P) -∗ P ∗ P.
Proof.
  iIntros "HQ1 HQ2 #HQP".
  (* [iPoseProof] does not consume "HQP" because a wand is instantiated *)
  iPoseProof ("HQP" with "HQ1") as "HP1".
  iPoseProof ("HQP" with "HQ2") as "HP2".
  iFrame.
Qed.
(* tests/proofmode.v *)
Lemma test_iDestruct_pose_forall (Φ : nat → PROP) :
  □ (∀ x, Φ x) -∗ Φ 0 ∗ Φ 1.
Proof.
  iIntros "#H".
  (* [iDestruct] does not consume "H" because quantifiers are instantiated *)
  iDestruct ("H" $! 0) as "$".
  iDestruct ("H" $! 1) as "$".
Qed.
(* tests/proofmode.v *)
Lemma test_iDestruct_or P Q : □ (P ∨ Q) -∗ Q ∨ P.
Proof.
  iIntros "#H".
  (* [iDestruct] consumes "H" because no quantifiers/wands are instantiated *)
  iDestruct "H" as "[H|H]".
  - by iRight.
  - by iLeft.
Qed.
(* tests/proofmode.v *)
Lemma test_iPoseProof_or P Q : □ (P ∨ Q) -∗ (Q ∨ P) ∗ (P ∨ Q).
Proof.
  iIntros "#H".
  (* [iPoseProof] does not consume "H" despite that no quantifiers/wands are
  instantiated. This makes it different from [iDestruct]. *)
  iPoseProof "H" as "[HP|HQ]".
  - iFrame "H". by iRight.
  - iFrame "H". by iLeft.
Qed.
(* tests/proofmode.v *)
Lemma test_iDestruct_intuitionistic_affine_bi `{!BiAffine PROP} P Q `{!Persistent P}:
  Q ∗ (Q -∗ P) -∗ P ∗ Q.
Proof. iIntros "[HQ HQP]". iDestruct ("HQP" with "HQ") as "#HP". by iFrame. Qed.
(* tests/proofmode.v *)
Lemma test_iDestruct_spatial Q : □ Q -∗ Q.
Proof. iIntros "#HQ". iDestruct "HQ" as "-#HQ". Show. done. Qed.
(* tests/proofmode.v *)
Lemma test_iDestruct_spatial_affine Q `{!Affine Q} : □ Q -∗ Q.
Proof.
  iIntros "#-#HQ".
  (* Since [Q] is affine, it should not add an <affine> modality *)
  Show. done.
Qed.
(* tests/proofmode.v *)
Lemma test_iDestruct_spatial_noop Q : Q -∗ Q.
Proof. iIntros "-#HQ". done. Qed.
(* tests/proofmode.v *)
Lemma test_iDestruct_exists (Φ: nat → PROP) :
  (∃ y, Φ y) -∗ ∃ n, Φ n.
Proof. iIntros "H". iDestruct "H" as (y) "H". by iExists y. Qed.
(* tests/proofmode.v *)
Lemma test_iDestruct_exists_automatic (Φ: nat → PROP) :
  (∃ y, Φ y) -∗ ∃ n, Φ n.
Proof.
  iIntros "H".
  iDestruct "H" as (?) "H".
  (* the automatic name should by [y] *)
  by iExists y.
Qed.
(* tests/proofmode.v *)
Lemma test_iDestruct_exists_automatic_multiple (Φ: nat → PROP) :
  (∃ y n baz, Φ (y+n+baz)) -∗ ∃ n, Φ n.
Proof. iDestruct 1 as (???) "H". by iExists (y+n+baz). Qed.
(* tests/proofmode.v *)
Lemma test_iDestruct_exists_freshen (y:nat) (Φ: nat → PROP) :
  (∃ y, Φ y) -∗ ∃ n, Φ n.
Proof.
  iIntros "H".
  iDestruct "H" as (?) "H".
  (* the automatic name is the freshened form of [y] *)
  by iExists y0.
Qed.
(* tests/proofmode.v *)
Lemma test_iDestruct_exists_not_exists P :
  P -∗ P.
Proof. Fail iDestruct 1 as (?) "H". Abort.
(* tests/proofmode.v *)
Lemma test_iDestruct_exists_explicit_name (Φ: nat → PROP) :
  (∃ y, Φ y) -∗ ∃ n, Φ n.
Proof.
  (* give an explicit name that isn't the binder name *)
  iDestruct 1 as (foo) "?".
  by iExists foo.
Qed.
(* tests/proofmode.v *)
Lemma test_iDestruct_exists_pure (Φ: nat → Prop) :
  ⌜∃ y, Φ y⌝ ⊢@{PROP} ∃ n, ⌜Φ n⌝.
Proof.
  iDestruct 1 as (?) "H".
  by iExists y.
Qed.
(* tests/proofmode.v *)
Lemma test_iDestruct_exists_and_pure (H: True) P :
  ⌜False⌝ ∧ P -∗ False.
Proof.
  (* this automatic name uses [fresh H] as a sensible default (it's a hypothesis
  in [Prop] and the user cannot supply a name in their code) *)
  iDestruct 1 as (?) "H".
  contradict H0.
Qed.
(* tests/proofmode.v *)
Lemma test_iDestruct_exists_intuitionistic P (Φ: nat → PROP) :
  □ (∃ y, Φ y ∧ P) -∗ P.
Proof.
  iDestruct 1 as (?) "#H". Show.
  iDestruct "H" as "[_ $]".
Qed.
(* tests/proofmode.v *)
Lemma test_iDestruct_exists_freshen_local_name (Φ: nat → PROP) :
  let y := 0 in
  □ (∃ y, Φ y) -∗ ∃ n, Φ (y+n).
Proof.
  iIntros (y) "#H".
  iDestruct "H" as (?) "H".
  iExists y0; auto.
Qed.
(* tests/proofmode.v *)
Lemma test_iDestruct_exists_anonymous P Φ :
  (∃ _:nat, P) ∗ (∃ x:nat, Φ x) -∗ P ∗ ∃ x, Φ x.
Proof.
  iIntros "[HP HΦ]".
  (* this should not use [x] as the default name for the unnamed binder *)
  iDestruct "HP" as (?) "$". Show.
  iDestruct "HΦ" as (x) "HΦ".
  by iExists x.
Qed.
(* tests/proofmode.v *)
Definition an_exists P : PROP
:= (∃ (an_exists_name:nat), ▷^an_exists_name P)%I.
(* tests/proofmode.v *)
(* should use the name from within [an_exists] *)
Lemma test_iDestruct_exists_automatic_def P :
  an_exists P -∗ ∃ k, ▷^k P.
Proof. iDestruct 1 as (?) "H". by iExists an_exists_name. Qed.
(* tests/proofmode.v *)
(* use an Iris intro pattern [% H] rather than (?) to indicate iExistDestruct *)
Lemma test_exists_intro_pattern_anonymous P (Φ: nat → PROP) :
  P ∗ (∃ y:nat, Φ y) -∗ ∃ x, P ∗ Φ x.
Proof.
  iIntros "[HP1 [% HP2]]".
  iExists y.
  iFrame "HP1 HP2".
Qed.
(* tests/proofmode.v *)
Lemma test_iIntros_pure (ψ φ : Prop) P : ψ → ⊢ ⌜ φ ⌝ → P → ⌜ φ ∧ ψ ⌝ ∧ P.
Proof. iIntros (??) "H". auto. Qed.
(* tests/proofmode.v *)
Lemma test_iDestruct_nameless_exist (Φ : nat → PROP) :
  bi_exist Φ ⊢@{PROP} ∃ x, Φ x.
Proof. iDestruct 1 as (?) "H". Show. auto. Qed.
(* tests/proofmode.v *)
Lemma test_iIntros_nameless_forall (Φ : nat → PROP) :
  (∀ x, Φ x) ⊢@{PROP} bi_forall Φ.
Proof. iIntros "H" (?). Show. done. Qed.
(* tests/proofmode.v *)
Lemma test_iIntros_nameless_pure_forall `{!BiPureForall PROP} (φ : nat → Prop) :
  (∀ x, ⌜ φ x ⌝) ⊢@{PROP} ⌜ ∀ x, φ x ⌝.
Proof. iIntros "H" (?). Show. done. Qed.
(* tests/proofmode.v *)
Lemma test_iIntros_forall_pure (Ψ: nat → PROP) :
  ⊢ ∀ x : nat, Ψ x → Ψ x.
Proof.
  iIntros "%".
  (* should be a trivial implication now *)
  Show. auto.
Qed.
(* tests/proofmode.v *)
Lemma test_iIntros_pure_not `{!BiPureForall PROP} : ⊢@{PROP} ⌜ ¬False ⌝.
Proof. by iIntros (?). Qed.
(* tests/proofmode.v *)
Lemma test_fast_iIntros `{!Sbi PROP} P Q :
  ⊢ ∀ x y z : nat,
    ⌜x = plus 0 x⌝ → ⌜y = 0⌝ → ⌜z = 0⌝ → P → □ Q → foo (x ≡ x).
Proof.
  iIntros (a) "*".
  iIntros "#Hfoo **".
  iIntros "_ //".
Qed.
(* tests/proofmode.v *)
Lemma test_very_fast_iIntros P :
  ∀ x y : nat, ⊢ ⌜ x = y ⌝ → P -∗ P.
Proof. by iIntros. Qed.
(* tests/proofmode.v *)
Lemma test_iIntros_automatic_name (Φ: nat → PROP) :
  ∀ y, Φ y -∗ ∃ x, Φ x.
Proof. iIntros (?) "H". by iExists y. Qed.
(* tests/proofmode.v *)
Lemma test_iIntros_automatic_name_proofmode_intro (Φ: nat → PROP) :
  ∀ y, Φ y -∗ ∃ x, Φ x.
Proof. iIntros "% H". by iExists y. Qed.
(* tests/proofmode.v *)
(* even an object-level forall should get the right name *)
Lemma test_iIntros_object_forall P :
  P -∗ ∀ (y:unit), P.
Proof. iIntros "H". iIntros (?). destruct y. iAssumption. Qed.
(* tests/proofmode.v *)
Lemma test_iIntros_object_proofmode_intro (Φ: nat → PROP) :
  ⊢ ∀ y, Φ y -∗ ∃ x, Φ x.
Proof. iIntros "% H". by iExists y. Qed.
(* tests/proofmode.v *)
Lemma test_iIntros_pure_names (H:True) P :
  ∀ x y : nat, ⊢ ⌜ x = y ⌝ → P -∗ P.
Proof.
  iIntros (???).
  (* the pure hypothesis should get a sensible [H0] as its name *)
  Show. auto.
Qed.
(* tests/proofmode.v *)
Definition tc_opaque_test : PROP
:= tc_opaque (∀ x : nat, ⌜ x = x ⌝)%I.
(* tests/proofmode.v *)
Lemma test_iIntros_tc_opaque : ⊢ tc_opaque_test.
Proof. by iIntros (x). Qed.
(* tests/proofmode.v *)
Definition tc_opaque_test_sep : PROP
:= tc_opaque (emp ∗ emp)%I.
(* tests/proofmode.v *)
Lemma test_iDestruct_tc_opaque_sep : tc_opaque_test_sep -∗ tc_opaque_test_sep.
Proof. iIntros "[H1 H2]". by iSplitL. Qed.
(* tests/proofmode.v *)
Lemma test_iApply_evar P Q R : (∀ Q, Q -∗ P) -∗ R -∗ P.
Proof. iIntros "H1 H2". iApply "H1". iExact "H2". Qed.
(* tests/proofmode.v *)
Lemma test_iApply_evar_refine {A} P (Q : A → PROP) (f : nat → A) :
  ∃ a, ∀ x : A, ∃ b,
    (P -∗ Q (f b)) -∗ (P -∗ Q a).
Proof.
  (* The evar [?b] has [x] in scope, but [?a] has not. When performing the
  [iApply], the unification [?a = f ?b] needs to be solved. Since [?a] has
  a smaller scope, Rocq cannot resolve [?a] to [f ?b] directly. Instead,
  it introduces a new evar [?b'] without [x] in scope, resolves [?a] to [f ?b'],
  and resolves [?b] to [?b']. That new evar appears as a goal that we explicitly
  have to [shelve] in the [Hint Extern] for the leaf instance [into_wand_wand]. *)
  eexists; intros x; eexists.
  iIntros "H HP". by iApply "H". Unshelve. exact 0.
Qed.
(* tests/proofmode.v *)
Lemma test_iExact_evar_refine {A} (Q : A → PROP) (f : nat → A) :
  ∃ a, ∀ x : A, ∃ b,
    Q (f b) -∗ Q a.
Proof.
  eexists; intros x; eexists.
  iIntros "H". iExact "H". Unshelve. exact 0.
Qed.
(* tests/proofmode.v *)
Lemma test_iAssumption_evar_refine {A} (Q : A → PROP) (f : nat → A) :
  ∃ a, ∀ x : A, ∃ b,
    Q (f b) -∗ Q a.
Proof.
  eexists; intros x; eexists.
  iIntros "H". iAssumption. Unshelve. exact 0.
Qed.
(* tests/proofmode.v *)
Lemma test_iFrame_evar_refine {A} (Q : A → PROP) (f : nat → A) :
  ∃ a, ∀ x : A, ∃ b,
    Q (f b) -∗ Q a.
Proof.
  eexists; intros x; eexists.
  iIntros "H". iFrame "H". Unshelve. exact 0.
Qed.
(* tests/proofmode.v *)
Lemma test_iApply_1 (P Q : PROP) :
  (▷ P -∗ Q) -∗ P -∗ Q.
Proof.
  iIntros "H HP".
  iApply ("H" with "HP").
Qed.
(* tests/proofmode.v *)
Lemma test_iApply_2 `{!BiAffine PROP} (P Q : PROP) :
  (▷ P → Q) -∗ P -∗ Q.
Proof.
  iIntros "H HP".
  iApply ("H" with "HP").
Qed.
(* tests/proofmode.v *)
Lemma test_iApply_3 `{!BiAffine PROP} (P Q : PROP) :
  (P → Q) -∗ <pers> P -∗ Q.
Proof.
  iIntros "H HP".
  iApply ("H" with "HP").
Qed.
(* tests/proofmode.v *)
Lemma test_iAssumption_affine P Q R `{!Affine P, !Affine R} : P -∗ Q -∗ R -∗ Q.
Proof. iIntros "H1 H2 H3". iAssumption. Qed.
(* tests/proofmode.v *)
Lemma test_done_goal_evar Q : ∃ P, Q ⊢ P.
Proof. eexists. iIntros "H". Fail done. iAssumption. Qed.
(* tests/proofmode.v *)
Lemma test_iDestruct_spatial_and P Q1 Q2 : P ∗ (Q1 ∧ Q2) -∗ P ∗ Q1.
Proof. iIntros "[H [? _]]". by iFrame. Qed.
(* tests/proofmode.v *)
Lemma test_iAssert_persistent P Q : P -∗ Q -∗ True.
Proof.
  iIntros "HP HQ".
  iAssert True%I as "#_". { by iClear "HP HQ". }
  iAssert True%I with "[HP]" as "#_". { Fail iClear "HQ". by iClear "HP". }
  iAssert True%I as % _. { by iClear "HP HQ". }
  iAssert True%I with "[HP]" as % _. { Fail iClear "HQ". by iClear "HP". }
  done.
Qed.
(* tests/proofmode.v *)
Lemma test_iAssert_persistently P : □ P -∗ True.
Proof.
  iIntros "HP". iAssert (□ P)%I with "[# //]" as "#H". done.
Qed.
(* tests/proofmode.v *)
Lemma test_iSpecialize_auto_frame P Q R :
  (P -∗ True -∗ True -∗ Q -∗ R) -∗ P -∗ Q -∗ R.
Proof. iIntros "H ? HQ". by iApply ("H" with "[$]"). Qed.
(* tests/proofmode.v *)
Lemma test_iSpecialize_persistent_auto_frame P Q :
  Persistent P → P ∗ (P -∗ Q) ⊢ P ∗ Q.
Proof.
  iIntros "% [? H]".
  iSpecialize ("H" with "[# $]").
  iFrame.
Qed.
(* tests/proofmode.v *)
Lemma test_iSpecialize_pure (φ : Prop) Q R :
  φ → (⌜φ⌝ -∗ Q) → ⊢ Q.
Proof. iIntros (HP HPQ). iDestruct (HPQ $! HP) as "?". done. Qed.
(* tests/proofmode.v *)
Lemma test_iSpecialize_pure_done (φ: Prop) Q :
  φ → (⌜φ⌝ -∗ Q) ⊢ Q.
Proof. iIntros (HP) "HQ". iApply ("HQ" with "[% //]"). Qed.
(* tests/proofmode.v *)
Lemma test_iSpecialize_not_pure_error P Q :
  (P -∗ Q) ⊢ Q.
Proof. iIntros "HQ". Fail iSpecialize ("HQ" with "[%]"). Abort.
(* tests/proofmode.v *)
Lemma test_iSpecialize_pure_done_error (φ: Prop) Q :
  (⌜φ⌝ -∗ Q) ⊢ Q.
Proof. iIntros "HQ". Fail iSpecialize ("HQ" with "[% //]"). Abort.
(* tests/proofmode.v *)
Lemma test_iSpecialize_done_error P Q :
  (P -∗ Q) ⊢ Q.
Proof. iIntros "HQ". Fail iSpecialize ("HQ" with "[//]"). Abort.
(* tests/proofmode.v *)
Lemma test_iSpecialize_Coq_entailment P Q R :
  (⊢ P) → (P -∗ Q) → (⊢ Q).
Proof. iIntros (HP HPQ). iDestruct (HPQ $! HP) as "?". done. Qed.
(* tests/proofmode.v *)
Lemma test_iSpecialize_intuitionistic P Q R :
  □ P -∗ □ (P -∗ P -∗ P -∗ P -∗ □ P -∗ P -∗ Q) -∗ R -∗ R ∗ □ (P ∗ Q).
Proof.
  iIntros "#HP #H HR".
  (* Test that [H] remains in the intuitionistic context *)
  iSpecialize ("H" with "HP").
  iSpecialize ("H" with "[HP]"); first done.
  iSpecialize ("H" with "[]"); first done.
  iSpecialize ("H" with "[-HR]"); first done.
  iSpecialize ("H" with "[#]"); first done.
  iFrame "HR".
  iSpecialize ("H" with "[-]"); first done.
  by iFrame "#".
Qed.
(* tests/proofmode.v *)
Lemma test_iSpecialize_intuitionistic_2 P Q R :
  □ P -∗ □ (P -∗ P -∗ P -∗ P -∗ □ P -∗ P -∗ Q) -∗ R -∗ R ∗ □ (P ∗ Q).
Proof.
  iIntros "#HP #H HR".
  (* Test that [H] remains in the intuitionistic context *)
  iSpecialize ("H" with "HP") as #.
  iSpecialize ("H" with "[HP]") as #; first done.
  iSpecialize ("H" with "[]") as #; first done.
  iSpecialize ("H" with "[-HR]") as #; first done.
  iSpecialize ("H" with "[#]") as #; first done.
  iFrame "HR".
  iSpecialize ("H" with "[-]") as #; first done.
  by iFrame "#".
Qed.