phanerozoic/Coq-Iris huggingface dataset:
(* tests/proofmode.v *)
Lemma test_bi_emp_valid_parens_space_close : (⊢@{PROP} True ).
Proof. naive_solver. Qed.
(* tests/proofmode.v *)
Lemma test_entails_annot_sections P :
  (P ⊢@{PROP} P) ∧ (⊢@{PROP}) P P ∧ (P ⊢.) P ∧ (.⊢ P) P ∧
  (P ⊣⊢@{PROP} P) ∧ (⊣⊢@{PROP}) P P ∧ (P ⊣⊢.) P ∧ (.⊣⊢ P) P.
Proof. naive_solver. Qed.
(* tests/proofmode.v *)
Lemma test_entails_annot_sections_parens P :
  ((P ⊢@{PROP} P)) ∧ ((⊢@{PROP})) P P ∧ ((P ⊢.)) P ∧ ((.⊢ P)) P ∧
  ((P ⊣⊢@{PROP} P)) ∧ ((⊣⊢@{PROP})) P P ∧ ((P ⊣⊢.)) P ∧ ((.⊣⊢ P)) P.
Proof. naive_solver. Qed.
(* tests/proofmode.v *)
Lemma test_entails_annot_sections_space_open P :
  ( P ⊢@{PROP} P) ∧ ( P ⊢.) P ∧
  ( P ⊣⊢@{PROP} P) ∧ ( P ⊣⊢.) P.
Proof. naive_solver. Qed.
(* tests/proofmode.v *)
Lemma test_entails_annot_sections_space_close P :
  (P ⊢@{PROP} P ) ∧ (⊢@{PROP} ) P P ∧ (.⊢ P ) P ∧
  (P ⊣⊢@{PROP} P ) ∧ (⊣⊢@{PROP} ) P P ∧ (.⊣⊢ P ) P.
Proof. naive_solver. Qed.
(* tests/proofmode.v *)
Lemma test_bi_internal_eq_annot_sections `{!Sbi PROP} P :
  ⊢@{PROP}
    P ≡@{PROP} P ∧ (≡@{PROP}) P P ∧ (P ≡.) P ∧ (.≡ P) P ∧
    ((P ≡@{PROP} P)) ∧ ((≡@{PROP})) P P ∧ ((P ≡.)) P ∧ ((.≡ P)) P ∧
    ( P ≡@{PROP} P) ∧ ( P ≡.) P ∧
    (P ≡@{PROP} P ) ∧ (≡@{PROP} ) P P ∧ (.≡ P ) P.
Proof. naive_solver. Qed.
(* tests/proofmode.v *)
Lemma elim_mod_accessor {X : Type} E1 E2 α (β : X → PROP) γ :
  accessor (fupd E1 E2) (fupd E2 E1) α β γ -∗ |={E1}=> True.
Proof. iIntros ">Hacc". Show. Abort.
(* tests/proofmode.v *)
Lemma print_long_line_1 (P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P : PROP) :
  P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P ∗
  P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P
  -∗ True.
Proof.
  iIntros "HP". Show. Undo. iIntros "?". Show.
Abort.
(* tests/proofmode.v *)
(* This is specifically crafted such that not having the printing box in
   the proofmode notation breaks the output. *)
Notation "'TESTNOTATION' '{{' P '|' Q '}' '}'"
:= (P ∧ Q)%I
  (format "'TESTNOTATION'  '{{'  P  '|'  '/' Q  '}' '}'") : bi_scope.
(* tests/proofmode.v *)
Lemma print_long_line_2 (P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P : PROP) :
  TESTNOTATION {{ P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P | P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P }}
  -∗ True.
Proof.
  iIntros "HP". Show. Undo. iIntros "?". Show.
Abort.
(* tests/proofmode.v *)
Lemma long_impl (PPPPPPPPPPPPPPPPP QQQQQQQQQQQQQQQQQQ : PROP) :
  ⊢ PPPPPPPPPPPPPPPPP → (QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ).
Proof.
  iStartProof. Show.
Abort.
(* tests/proofmode.v *)
Lemma long_impl_nested (PPPPPPPPPPPPPPPPP QQQQQQQQQQQQQQQQQQ : PROP) :
  ⊢ PPPPPPPPPPPPPPPPP → (QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ) → (QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ).
Proof.
  iStartProof. Show.
Abort.
(* tests/proofmode.v *)
Lemma long_wand (PPPPPPPPPPPPPPPPP QQQQQQQQQQQQQQQQQQ : PROP) :
  ⊢ PPPPPPPPPPPPPPPPP -∗ (QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ).
Proof.
  iStartProof. Show.
Abort.
(* tests/proofmode.v *)
Lemma long_wand_nested (PPPPPPPPPPPPPPPPP QQQQQQQQQQQQQQQQQQ : PROP) :
  ⊢ PPPPPPPPPPPPPPPPP -∗ (QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ) -∗ (QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ).
Proof.
  iStartProof. Show.
Abort.
(* tests/proofmode.v *)
Lemma long_fupd E (PPPPPPPPPPPPPPPPP QQQQQQQQQQQQQQQQQQ : PROP) :
  PPPPPPPPPPPPPPPPP ={E}=∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ.
Proof.
  iStartProof. Show.
Abort.
(* tests/proofmode.v *)
Lemma long_fupd_nested E1 E2 (PPPPPPPPPPPPPPPPP QQQQQQQQQQQQQQQQQQ : PROP) :
  PPPPPPPPPPPPPPPPP ={E1,E2}=∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
  ={E1,E2}=∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ.
Proof.
  iStartProof. Show.
Abort.
(* tests/proofmode.v *)
Lemma iStopProof_not_proofmode : 10 = 10.
Proof. Fail iStopProof. Abort.
(* tests/proofmode.v *)
Lemma iAlways_spatial_non_empty P :
  P -∗ □ emp.
Proof. iIntros "HP". Fail iModIntro. Abort.
(* tests/proofmode.v *)
Lemma iDestruct_bad_name P :
  P -∗ P.
Proof. iIntros "HP". Fail iDestruct "HQ" as "HP". Abort.
(* tests/proofmode.v *)
Lemma iIntros_dup_name P Q :
  P -∗ Q -∗ ∀ x y : (), P.
Proof.
  iIntros "HP". Fail iIntros "HP".
  iIntros "HQ" (x). Fail iIntros (x).
Abort.
(* tests/proofmode.v *)
Lemma iIntros_pure_not_forall P Q :
  P -∗ Q.
Proof.
  Fail iIntros (?).
Abort.
(* tests/proofmode.v *)
Lemma iSplitL_one_of_many P :
  P -∗ P -∗ P ∗ P.
Proof.
  iIntros "HP1 HP2". Fail iSplitL "HP1 HPx". Fail iSplitL "HPx HP1".
Abort.
(* tests/proofmode.v *)
Lemma iSplitR_one_of_many P :
  P -∗ P -∗ P ∗ P.
Proof.
  iIntros "HP1 HP2". Fail iSplitR "HP1 HPx". Fail iSplitR "HPx HP1".
Abort.
(* tests/proofmode.v *)
Lemma iSplitL_non_splittable P :
  ⊢ P.
Proof.
  Fail iSplitL "".
Abort.
(* tests/proofmode.v *)
Lemma iSplitR_non_splittable P :
  ⊢ P.
Proof.
  Fail iSplitR "".
Abort.
(* tests/proofmode.v *)
Lemma iCombine_fail P:
  P -∗ P -∗ P ∗ P.
Proof.
  iIntros "HP1 HP2". Fail iCombine "HP1 HP3" as "HP".
Abort.
(* tests/proofmode.v *)
Lemma iSpecialize_bad_name1_fail P Q:
  (P -∗ Q) -∗ P -∗ Q.
Proof.
  iIntros "HW HP". Fail iSpecialize ("H" with "HP").
Abort.
(* tests/proofmode.v *)
Lemma iSpecialize_bad_name2_fail P Q:
  (P -∗ Q) -∗ P -∗ Q.
Proof.
  iIntros "HW HP". Fail iSpecialize ("HW" with "H").
Abort.
(* tests/proofmode.v *)
Lemma iSpecialize_autoframe_fail P Q : (P -∗ Q) -∗ Q.
Proof.
  iIntros "H".
  Fail iSpecialize ("H" with "[$]").
  Fail iApply ("H" with "[$]").
Abort.
(* tests/proofmode.v *)
Lemma iSpecialize_autoframe_fail2 P Q R : (P -∗ Q -∗ R) -∗ P -∗ R.
Proof.
  iIntros "H HP".
  Fail iSpecialize ("H" with "[$] [$]").
  Fail iApply ("H" with "[$] [$]").
Abort.
(* tests/proofmode.v *)
Lemma iExact_fail P Q :
  <affine> P -∗ Q -∗ <affine> P.
Proof.
  iIntros "HP". Fail iExact "HQ". iIntros "HQ". Fail iExact "HQ". Fail iExact "HP".
Abort.
(* tests/proofmode.v *)
Lemma iClear_fail P : P -∗ P.
Proof. Fail iClear "HP". iIntros "HP". Fail iClear "HP". Abort.
(* tests/proofmode.v *)
Lemma iSpecializeArgs_fail P :
  (∀ x : nat, P) -∗ P.
Proof. iIntros "HP". Fail iSpecialize ("HP" $! true). Abort.
(* tests/proofmode.v *)
Lemma iSpecialize_nested_fail P : P -∗ P.
Proof.
  iIntros "H".
  (* Should report that "HH" is not found *)
  Fail iSpecialize ("HH" with "(H H)").
Abort.
(* tests/proofmode.v *)
Lemma iStartProof_fail : 0 = 0.
Proof. Fail iStartProof. Abort.
(* tests/proofmode.v *)
Lemma iPoseProof_fail P : P -∗ P.
Proof.
  Fail iPoseProof (eq_refl 0) as "H".
  iIntros "H". Fail iPoseProof bi.and_intro as "H".
Abort.
(* tests/proofmode.v *)
Lemma iPoseProof_not_found_fail P : P -∗ P.
Proof.
  iIntros "H". Fail iPoseProof "Hx" as "H1".
Abort.
(* tests/proofmode.v *)
Lemma iPoseProof_not_found_fail2 P Q (H: P -∗ Q) : P -∗ Q.
Proof.
  iIntros "HP". Fail iPoseProof (H with "[HQ]") as "H".
Abort.
(* tests/proofmode.v *)
Lemma iPoseProofCoreHyp_not_found_fail P : P -∗ P -∗ P.
Proof.
  iIntros "H". Fail iPoseProofCoreHyp "Hx" as "H1".
Abort.
(* tests/proofmode.v *)
Lemma iPoseProofCoreHyp_not_fresh_fail P : P -∗ P -∗ P.
Proof.
  iIntros "H0 H1". Fail iPoseProofCoreHyp "H0" as "H1".
Abort.
(* tests/proofmode.v *)
Lemma iRevert_fail P : P -∗ P.
Proof. Fail iRevert "H". Abort.
(* tests/proofmode.v *)
Lemma iDestruct_exist_not_fresh_fail P (Φ : nat → PROP) :
  P ∗ (∃ y, Φ y) -∗ ∃ x, P ∗ Φ x.
Proof.
  iIntros "[H HP2]". Fail iDestruct "HP2" as "[%x H]".
Abort.
(* tests/proofmode.v *)
Lemma iDestruct_fail P : P -∗ <absorb> P.
Proof.
  iIntros "HP".
  Fail iDestruct "HP" as "[{HP}]".
  (* IDone is unsupported (see issue #380) *)
  Fail iDestruct "HP" as "// H".
  (* fails due to not having "one proper intro pattern" (see issue #380) *)
  Fail iDestruct "HP" as "HP //".
  (* both of these work *)
  iDestruct "HP" as "HP /=".
  iDestruct "HP" as "/= HP".
  Fail iDestruct "HP" as "[HP HQ HR]".
  Fail iDestruct "HP" as "[HP|HQ|HR]".
  Fail iDestruct "HP" as "[HP]".
  Fail iDestruct "HP" as "[HP HQ|HR]".
Abort.
(* tests/proofmode.v *)
Lemma iOrDestruct_fail P : (P ∨ P) -∗ P -∗ P.
Proof.
  iIntros "H H'". Fail iOrDestruct "H" as "H'" "H2". Fail iOrDestruct "H" as "H1" "H'".
Abort.
(* tests/proofmode.v *)
Lemma iApply_fail P Q : P -∗ Q.
Proof. iIntros "HP". Fail iApply "HP". Abort.
(* tests/proofmode.v *)
Lemma iApply_fail_not_affine_1 P Q : P -∗ Q -∗ Q.
Proof. iIntros "HP HQ". Fail iApply "HQ". Abort.
(* tests/proofmode.v *)
Lemma iIntro_fail_nonempty_spatial P Q : P -∗ P → Q.
Proof. Fail iIntros "? HP". Abort.
(* tests/proofmode.v *)
Lemma iIntro_fail_not_fresh P Q : P -∗ P -∗ Q.
Proof. Fail iIntros "HP HP". Abort.
(* tests/proofmode.v *)
Lemma iIntro_fail_nothing_to_introduce P Q : P -∗ Q.
Proof. Fail iIntros "HP HQ". Abort.
(* tests/proofmode.v *)
Lemma iApply_fail_not_affine_2 P Q R : P -∗ R -∗ (R -∗ Q) -∗ Q.
Proof. iIntros "HP HR HQ". Fail iApply ("HQ" with "HR"). Abort.
(* tests/proofmode.v *)
Lemma iAssumption_fail_not_affine_1 P Q : P -∗ Q -∗ Q.
Proof. iIntros "HP HQ". Fail iAssumption. Abort.
(* tests/proofmode.v *)
Lemma iAssumption_fail_not_affine_2 P Q : (⊢ Q) → P -∗ Q.
Proof. iIntros (HQ) "HP". Fail iAssumption. Abort.
(* tests/proofmode.v *)
Lemma iRevert_wrong_var (k : nat) (Φ : nat → PROP) : ⊢ Φ (S k).
Proof.
  Fail iRevert (k1).
  Fail iLöb as "IH" forall (k1).
Abort.
(* tests/proofmode.v *)
Lemma iRevert_dup_var (k : nat) (Φ : nat → PROP) : ⊢ Φ (S k).
Proof. Fail iRevert (k k). Abort.
(* tests/proofmode.v *)
Lemma iRevert_dep_var_coq (k : nat) (Φ : nat → PROP) : k = 0 → ⊢ Φ (S k).
Proof. intros Hk. Fail iRevert (k). Abort.
(* tests/proofmode.v *)
Lemma iRevert_dep_var (k : nat) (Φ : nat → PROP) : Φ k -∗ Φ (S k).
Proof. iIntros "Hk". Fail iRevert (k). Abort.
(* tests/proofmode.v *)
Lemma iLöb_no_BiLöb P : ⊢ P.
Proof. Fail iLöb as "IH". Abort.
(* tests/proofmode.v *)
Lemma iMod_mask_mismatch `{!BiFUpd PROP} E1 E2 (P : PROP) :
  (|={E2}=> P) ⊢ |={E1}=> P.
Proof.
  Fail iIntros ">HP".
  iIntros "HP". Fail iMod "HP".
Abort.
(* tests/proofmode.v *)
Lemma iMod_mask_mismatch `{!BiFUpd PROP} E1 E2 (P : PROP) :
  ⊢ |={E1,E2}=> P.
Proof.
  Fail iModIntro.
  Fail iIntros "!>".
Abort.
(* tests/proofmode.v *)
Lemma iRevert_wrong_sel_pat (n m : nat) (P Q : nat → PROP) :
  ⌜ n = m ⌝ -∗ P n -∗ P m.
Proof.
  Fail iRevert n.
Abort.
(* tests/proofmode.v *)
Lemma iInduction_wrong_sel_pat (n m : nat) (P Q : nat → PROP) :
  ⌜ n = m ⌝ -∗ P n -∗ P m.
Proof.
  Fail iInduction n as [|n IH] forall m.
Abort.
(* tests/proofmode.v *)
Lemma iInduction_non_fresh_IH Q (P : nat → PROP) n :
  □ Q -∗ P n.
Proof.
  iIntros "IH".
  Fail iInduction n as [|n IH].
  Fail iInduction n as [|n] "IH".
Abort.
(* tests/proofmode.v *)
Lemma iInduction_non_fresh_Coq_IH φ (P : nat → PROP) n :
  □ ⌜ φ ⌝ -∗ P n.
Proof.
  iIntros (IH).
  (* Names for IHs should also be fresh in Coq context *)
  Fail iInduction n as [|n IH].
  (* But for the legacy syntax this is no problem. *)
  iInduction n as [|n] "IH".
Abort.
(* tests/proofmode.v *)
Lemma test_iIntros_let_entails_fail P :
  let Q := (P ∗ P)%I in
  Q ⊢ Q.
Proof.
  Fail iIntros "Q".
Abort.
(* tests/proofmode.v *)
Lemma test_iIntros_let_wand_fail P :
  let Q := (P ∗ P)%I in
  Q -∗ Q.
Proof.
  Fail iIntros "Q".
Abort.
(* tests/proofmode.v *)
Lemma test_iStartProof_iPoseProof_wrong_BI
    {PROP1 PROP2 : bi} (P1 : PROP1) (P2 : PROP2) :
  (⊢@{PROP1} P1) →
  ⊢@{PROP2} P2.
Proof.
  Fail iStartProof PROP1.
  iStartProof PROP2.
  iIntros (H).
  Fail iDestruct H as "H".
Abort.
(* tests/proofmode.v *)
Lemma test_pure_name P (φ1 φ2 : Prop) (Himpl : φ1 → φ2) :
  P ∗ ⌜φ1⌝ -∗ P ∗ ⌜φ2⌝.
Proof.
  iIntros "[HP %HP2]".
  Show.
  iFrame.
  iPureIntro.
  exact (Himpl HP2).
Qed.
(* tests/proofmode.v *)
Lemma test_iIntros_forall_pure_named (Ψ: nat → PROP) :
  (∀ x : nat, Ψ x) ⊢ ∀ x : nat, Ψ x.
Proof. iIntros "HP". iIntros "%y". iApply ("HP" $! y). Qed.
(* tests/proofmode.v *)
Lemma test_not_fresh P (φ : Prop) (H : φ) :
  P ∗ ⌜ φ ⌝ -∗ P ∗ ⌜ φ ⌝.
Proof.
  Fail iIntros "[H %H]".
Abort.
(* tests/proofmode.v *)
Lemma test_exists_intro_pattern P (Φ: nat → PROP) :
  P ∗ (∃ y:nat, Φ y) -∗ ∃ x, P ∗ Φ x.
Proof.
  iIntros "[HP1 [%yy HP2]]".
  iExists yy.
  iFrame "HP1 HP2".
Qed.
(* tests/proofmode.v *)
Lemma test_iRename_select1 P Q :
  □ (P -∗ Q) -∗ □ P -∗ □ Q.
Proof.
  iIntros "#? #?".
  iRename select P into "H1".
  (* The following fails since there are no matching hypotheses. *)
  Fail iRename select (_ ∗ _)%I into "?".
  iRename select (_ -∗ _)%I into "H2".
  iDestruct ("H2" with "H1") as "$".
Qed.
(* tests/proofmode.v *)
Lemma test_iRename_select2 P Q :
  (P -∗ Q) -∗ P -∗ Q.
Proof.
  iIntros "??".
  iRename select P into "H1".
  iRename select (_ -∗ _)%I into "H2".
  by iApply "H2".
Qed.
(* tests/proofmode.v *)
Lemma test_iDestruct_select1 P Q :
  (P ∗ Q) -∗ Q ∗ P.
Proof.
  iIntros "?".
  iDestruct select (_ ∗ _)%I as "[$ $]".
Qed.
(* tests/proofmode.v *)
Lemma test_iDestruct_select2 φ P :
  (∃ x, P ∗ φ x) -∗ ∃ x, φ x ∗ P.
Proof.
  iIntros "?".
  (* The following fails since [Φ n] is not pure. *)
  Fail iDestruct select (∃ _, _)%I as (n) "[H1 %]".
  iDestruct select (∃ _, _)%I as (n) "[H1 H2]".
  iExists n. iFrame.
Qed.
(* tests/proofmode.v *)
Lemma test_iDestruct_select3 Ψ P :
  (∃ x y, P ∗ Ψ x y) -∗ ∃ x y, Ψ x y ∗ P.
Proof.
  iIntros "?".
  iDestruct select (∃ _, _)%I as (n m) "[H1 H2]".
  iExists n, m. iFrame.
Qed.
(* tests/proofmode.v *)
Lemma test_iDestruct_select4 φ :
  □ (∃ x, φ x) -∗ □ (∃ x, φ x).
Proof.
  iIntros "#?".
  iDestruct select (∃ _, _)%I as (n) "H".
  by iExists n.
Qed.
(* tests/proofmode.v *)
Lemma test_iDestruct_select5 (φ : nat → Prop) P :
  P -∗ ⌜∃ n, φ n⌝ -∗ ∃ n, P ∗ ⌜φ n⌝ ∗ ⌜φ n⌝.
Proof.
  iIntros "??".
  iDestruct select ⌜_⌝%I as %[n H].
  iExists n. iFrame. by iSplit.
Qed.
(* tests/proofmode.v *)
Lemma test_iDestruct_select_no_backtracking P Q :
  □ P -∗ Q -∗ Q.
Proof.
  iIntros "??".
  (* The following must fail since the pattern will match [Q], which cannot be
     introduced in the intuitionistic context. This demonstrates that tactics
     based on [iSelect] only act on the last hypothesis of the intuitionistic
     or spatial context that matches the pattern, and they do not backtrack if
     the requested action fails on the hypothesis. *)
  Fail iDestruct select _ as "#X".
  done.
Qed.
(* tests/proofmode.v *)
Lemma test_iDestruct_select_several_match P Q R :
  □ P -∗ □ Q -∗ □ R -∗ □ R.
Proof.
  iIntros "???".
  (* This demonstrates that the last matching hypothesis is used for all the
     tactics based on [iSelect]. *)
  iDestruct select (□ _)%I as "$".
Qed.
(* tests/proofmode.v *)
Lemma test_iRevert_select_iClear_select P Q R :
  □ P -∗ □ Q -∗ □ R -∗ □ R.
Proof.
  iIntros "???".
  iClear select (□ P)%I.
  iRevert select _.
  iClear select _.
  iIntros "$".
Qed.
(* tests/proofmode.v *)
Lemma test_iFrame_select P Q R :
  P -∗ (Q ∗ R) -∗ P ∗ Q ∗ R.
Proof.
  iIntros "??".
  iFrame select (_ ∗ _)%I.
  iFrame select _.
Qed.
(* tests/proofmode.v *)
Lemma test_iDestruct_split_reuse_name P Q :
  P ∗ Q -∗ P ∗ Q.
Proof.
  iIntros "H".
  iDestruct "H" as "[? H]". Undo.
  iDestruct "H" as "[H ?]". Undo.
  auto.
Qed.
(* tests/proofmode.v *)
Lemma test_iDestruct_split_reuse_name_2 P Q R :
  (P ∗ Q) ∗ R -∗ (P ∗ Q) ∗ R.
Proof.
  iIntros "H".
  iDestruct "H" as "[[H H'] ?]". Undo.
  auto.
Qed.
(* tests/proofmode.v *)
Lemma test_iDestruct_intuitionistic_not_fresh P Q :
  P -∗ □ Q -∗ False.
Proof.
  iIntros "H H'". Fail iDestruct "H'" as "#H".
Abort.
(* tests/proofmode.v *)
Lemma test_iDestruct_spatial_not_fresh P Q :
  P -∗ Q -∗ False.
Proof.
  iIntros "H H'". Fail iDestruct "H'" as "-#H".
Abort.
(* tests/proofmode.v *)
Lemma test_iIntros_subgoals (m : gmap nat nat) i x :
  ⊢@{PROP} ⌜kmap (M2 :=gmap nat) id m !! i = Some x⌝ → True.
Proof. iStartProof. iIntros (?%lookup_kmap_Some). Abort.
(* tests/proofmode.v *)
Inductive ntree
:= Tree : list ntree → ntree.
(* tests/proofmode.v *)
(* The common induction principle for finitely branching trees. By default,
  Coq generates a too weak induction principle, so we have to prove it by hand. *)
Lemma ntree_ind (φ : ntree → Prop) :
    (∀ l, Forall φ l → φ (Tree l)) →
    ∀ t, φ t.
Proof.
    intros Hrec. fix REC 1. intros [l]. apply Hrec. clear Hrec.
    induction l as [|t l IH]; constructor; auto.
  Qed.
(* tests/proofmode.v *)
Lemma test_iInduction_Forall (P : ntree → PROP) :
    □ (∀ l, (∀ x, ⌜ x ∈ l ⌝ → P x) -∗ P (Tree l)) -∗
    ∀ t, P t.
Proof.
    iIntros "#H" (t). iInduction t as [l IH].
    Show. (* make sure that the induction hypothesis is exactly what we want *)
    iApply "H". iIntros (x ?). by iApply (big_sepL_elem_of with "IH").
  Qed.
(* tests/proofmode.v *)
(* Now let us define a custom version of [Forall], called [my_Forall], and
  use that in the variant [ntree_ind_alt] of the induction principle. The proof
  mode does not support [my_Forall], so we test if [iInduction] generates a
  proper error message. *)
Inductive my_Forall {A} (φ : A → Prop) : list A → Prop
:=
    | my_Forall_nil : my_Forall φ []
    | my_Forall_cons x l : φ x → my_Forall φ l → my_Forall φ (x :: l).
(* tests/proofmode.v *)
Lemma ntree_ind_alt (φ : ntree → Prop) :
    (∀ l, my_Forall φ l → φ (Tree l)) →
    ∀ t, φ t.
Proof.
    intros Hrec. fix REC 1. intros [l]. apply Hrec. clear Hrec.
    induction l as [|t l IH]; constructor; auto.
  Qed.
(* tests/proofmode.v *)
Lemma test_iInduction_Forall_fail (P : ntree → PROP) :
    □ (∀ l, ([∗ list] x ∈ l, P x) -∗ P (Tree l)) -∗
    ∀ t, P t.
Proof.
    iIntros "#H" (t).
    Fail iInduction t as [l IH] using ntree_ind_alt.
  Abort.
(* tests/proofmode.v *)
(* Making sure that [iFrame] does not diverge on evars gmultisets by turning
  them into disjoint union of new evars. *)
Lemma test_iFrame_gmultiset_divergence `{Countable A} P Q :
    P ⊢ ∃ X : gmultiset A, [∗ mset] y ∈ X, Q.
Proof.
    iIntros "?".
    iExists _.
    (* Makes no progress since there is nothing to do. *)
    Timeout 1 iFrame.
  Abort.
(* tests/proofmode.v *)
(* Making sure that we can still frame in disjoint unions. *)
Lemma test_iFrame_gmultiset_functionality `{Countable A} (X Y: gmultiset A) Q :
    ([∗ mset] y ∈ X, Q) ∗ ([∗ mset] y ∈ Y, Q) ⊢ [∗ mset] y ∈ X ⊎ Y, Q.
Proof.
    iIntros "?".
    solve [iFrame].
  Restart. Proof.
    iIntros "[??]".
    solve [iFrame].
  Qed.
(* tests/proofmode_ascii.v *)
Lemma test_random_stuff (P1 P2 P3 : nat -> uPred M) :
    |- forall (x y : nat) a b,
      x ≡ y ->
      <#> (uPred_ownM (a ⋅ b) -*
      (exists y1 y2 c, P1 ((x + y1) + y2) /\ True /\ <#> uPred_ownM c) -*
      <#> |> (forall z, P2 z ∨ True -> P2 z) -*
      |> (forall n m : nat, P1 n -> <#> (True /\ P2 n -> <#> (⌜n = n⌝ <-> P3 n))) -*
      |> ⌜x = 0⌝ \/ exists 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_ascii.v *)
Lemma test_iFrame_pure (x y z : M) :
    ✓ x -> ⌜y ≡ z⌝ |-@{uPredI M} ✓ x /\ ✓ x /\ y ≡ z.
Proof. iIntros (Hv) "Hxy". by iFrame (Hv) "Hxy". Qed.
(* tests/proofmode_ascii.v *)
Lemma test_iAssert_modality P : (|==> False) -* |==> P.
Proof. iIntros. iAssert False%I with "[> - //]" as %[]. Qed.
(* tests/proofmode_ascii.v *)
Lemma test_iStartProof_1 P : P -* P.
Proof. iStartProof. iStartProof. iIntros "$". Qed.
(* tests/proofmode_ascii.v *)
Lemma test_iStartProof_2 P : P -* P.
Proof. iStartProof (uPred _). iStartProof (uPredI _). iIntros "$". Qed.
(* tests/proofmode_ascii.v *)
Lemma test_iStartProof_3 P : P -* P.
Proof. iStartProof (uPredI _). iStartProof (uPredI _). iIntros "$". Qed.
(* tests/proofmode_ascii.v *)
Lemma test_iStartProof_4 P : P -* P.
Proof. iStartProof (uPredI _). iStartProof (uPred _). iIntros "$". Qed.
(* tests/proofmode_ascii.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_ascii.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_ascii.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_ascii.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_ascii.v *)
Lemma test_iInv_2 γ p N P:
    cinv N γ (<pers> P) ** cinv_own γ p ={⊤}=* cinv_own γ p ** |> P.
Proof.
    iIntros "(#?&?)".
    iInv N as "(#HP&Hown)". Show.
    iModIntro. iSplit; auto with iFrame.
  Qed.
(* tests/proofmode_ascii.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_ascii.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_ascii.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_ascii.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_ascii.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_ascii.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_ascii.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_ascii.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_ascii.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.