phanerozoic/Coq-Iris huggingface dataset:
(* tests/proofmode.v *)
Lemma test_iSpecialize_intuitionistic_3 P Q R :
  P -∗ □ (P -∗ Q) -∗ □ (P -∗ <pers> Q) -∗ □ (Q -∗ R) -∗ P ∗ □ (Q ∗ R).
Proof.
  iIntros "HP #H1 #H2 #H3".
  (* Should fail, [Q] is not persistent *)
  Fail iSpecialize ("H1" with "HP") as #.
  (* Should succeed, [<pers> Q] is persistent *)
  iSpecialize ("H2" with "HP") as #.
  (* Should succeed, despite [R] not being persistent, no spatial premises are
  needed to prove [Q] *)
  iSpecialize ("H3" with "H2") as #.
  by iFrame "#".
Qed.
(* tests/proofmode.v *)
Lemma test_iSpecialize_impl_pure (φ : Prop) P Q :
  φ → □ (⌜φ⌝ → P) -∗ (⌜φ⌝ → Q) -∗ P ∗ Q.
Proof.
  iIntros (?) "#H1 H2".
  (* Adds an affine modality *)
  iSpecialize ("H1" with "[]"). { Show. done. }
  iSpecialize ("H2" with "[]"). { Show. done. }
Restart. Proof.
  iIntros (?) "#H1 H2".
  (* Solving it directly as a pure goal also works. *)
  iSpecialize ("H1" with "[% //]").
  iSpecialize ("H2" with "[% //]").
  by iFrame.
Abort.
(* tests/proofmode.v *)
Lemma test_iSpecialize_impl_pure_affine `{!BiAffine PROP} (φ : Prop) P Q :
  φ → □ (⌜φ⌝ → P) -∗ (⌜φ⌝ → Q) -∗ P ∗ Q.
Proof.
  iIntros (?) "#H1 H2".
  (* Does not add an affine modality *)
  iSpecialize ("H1" with "[]"). { Show. done. }
  iSpecialize ("H2" with "[]"). { Show. done. }
Restart. Proof.
  iIntros (?) "#H1 H2".
  (* Solving it directly as a pure goal also works. *)
  iSpecialize ("H1" with "[% //]").
  iSpecialize ("H2" with "[% //]").
  by iFrame.
Abort.
(* tests/proofmode.v *)
Lemma test_iSpecialize_forall_pure (φ : Prop) P Q :
  φ → □ (∀ _ : φ, P) -∗ (∀ _ : φ, Q) -∗ P ∗ Q.
Proof.
  iIntros (?) "#H1 H2".
  (* Adds an affine modality *)
  iSpecialize ("H1" with "[]"). { Show. done. }
  iSpecialize ("H2" with "[]"). { Show. done. }
Restart. Proof.
  iIntros (?) "#H1 H2".
  (* Solving it directly as a pure goal also works. *)
  iSpecialize ("H1" with "[% //]").
  iSpecialize ("H2" with "[% //]").
  by iFrame.
Abort.
(* tests/proofmode.v *)
Lemma test_iSpecialize_forall_pure_affine `{!BiAffine PROP} (φ : Prop) P Q :
  φ → □ (∀ _ : φ, P) -∗ (∀ _ : φ, Q) -∗ P ∗ Q.
Proof.
  iIntros (?) "#H1 H2".
  (* Does not add an affine modality *)
  iSpecialize ("H1" with "[]"). { Show. done. }
  iSpecialize ("H2" with "[]"). { Show. done. }
Restart. Proof.
  iIntros (?) "#H1 H2".
  (* Solving it directly as a pure goal also works. *)
  iSpecialize ("H1" with "[% //]").
  iSpecialize ("H2" with "[% //]").
  by iFrame.
Abort.
(* tests/proofmode.v *)
Lemma test_iAssert_intuitionistic `{!BiBUpd PROP} P :
  □ P -∗ □ |==> P.
Proof.
  iIntros "#HP".
  (* Test that [HPupd1] ends up in the intuitionistic context *)
  iAssert (|==> P)%I with "[]" as "#HPupd1"; first done.
  (* This should not work, [|==> P] is not persistent. *)
  Fail iAssert (|==> P)%I with "[#]" as "#HPupd2"; first done.
  done.
Qed.
(* tests/proofmode.v *)
Lemma test_iSpecialize_evar P : (∀ R, R -∗ R) -∗ P -∗ P.
Proof. iIntros "H HP". iApply ("H" with "[HP]"). done. Qed.
(* tests/proofmode.v *)
Lemma test_iPure_intro_emp R `{!Affine R} :
  R -∗ emp.
Proof. iIntros "HR". by iPureIntro. Qed.
(* tests/proofmode.v *)
Lemma test_iEmp_intro P Q R `{!Affine P, !Persistent Q, !Affine R} :
  P -∗ Q → R -∗ emp.
Proof. iIntros "HP #HQ HR". iEmpIntro. Qed.
(* tests/proofmode.v *)
Lemma test_iPure_intro (φ : nat → Prop) P Q R `{!Affine P, !Persistent Q, !Affine R} :
  φ 0 → P -∗ Q → R -∗ ∃ x : nat, <affine> ⌜ φ x ⌝ ∧ ⌜ φ x ⌝.
Proof. iIntros (?) "HP #HQ HR". iPureIntro; eauto. Qed.
(* tests/proofmode.v *)
Lemma test_iPure_intro_2 (φ : nat → Prop) P Q R `{!Persistent Q} :
  φ 0 → P -∗ Q → R -∗ ∃ x : nat, <affine> ⌜ φ x ⌝ ∗ ⌜ φ x ⌝.
Proof. iIntros (?) "HP #HQ HR". iPureIntro; eauto. Qed.
(* tests/proofmode.v *)
(* Ensure that [% ...] works as a pattern when the left-hand side of and/sep is
pure. *)
Lemma test_pure_and_sep_destruct_affine `{!BiAffine PROP} (φ : Prop) P :
  ⌜φ⌝ ∧ (⌜φ⌝ ∗ P) -∗ P.
Proof.
  iIntros "[% [% $]]".
Qed.
(* tests/proofmode.v *)
Lemma test_pure_and_sep_destruct_1 (φ : Prop) P :
  ⌜φ⌝ ∧ (<affine> ⌜φ⌝ ∗ P) -∗ P.
Proof.
  iIntros "[% [% $]]".
Qed.
(* tests/proofmode.v *)
Lemma test_pure_and_sep_destruct_2 (φ : Prop) P :
  ⌜φ⌝ ∧ (⌜φ⌝ ∗ <absorb> P) -∗ <absorb> P.
Proof.
  iIntros "[% [% $]]".
Qed.
(* tests/proofmode.v *)
(* Ensure that [% %] also works when the conjunction is *inside* ⌜...⌝ *)
Lemma test_pure_inner_and_destruct :
  ⌜False ∧ True⌝ ⊢@{PROP} False.
Proof.
  iIntros "[% %]". done.
Qed.
(* tests/proofmode.v *)
(* Ensure that [% %] works as a pattern for an existential with a pure body. *)
Lemma test_exist_pure_destruct_1 :
  (∃ x, ⌜ x = 0 ⌝) ⊢@{PROP} True.
Proof.
  iIntros "[% %]". done.
Qed.
(* tests/proofmode.v *)
(* Also test nested existentials where the type of the 2nd depends on the first
(which could cause trouble if we do things in the wrong order) *)
Lemma test_exist_pure_destruct_2 :
  (∃ x (_:x=0), True) ⊢@{PROP} True.
Proof.
  iIntros "(% & % & $)".
Qed.
(* tests/proofmode.v *)
Lemma test_fresh P Q:
  (P ∗ Q) -∗ (P ∗ Q).
Proof.
  iIntros "H".
  let H1 := iFresh in
  let H2 := iFresh in
  let pat := constr:(IList [cons (IIdent H1) (cons (IIdent H2) nil)]) in
  iDestruct "H" as pat.
  iFrame.
Qed.
(* tests/proofmode.v *)
(* Test for issue #288 *)
Lemma test_iExists_unused : ⊢ ∃ P : PROP, ∃ x : nat, P.
Proof.
  iExists _.
  iExists 10.
  iAssert emp%I as "H"; first done.
  iExact "H".
Qed.
(* tests/proofmode.v *)
(* Check coercions *)
Lemma test_iExist_coercion (P : Z → PROP) : (∀ x, P x) -∗ ∃ x, P x.
Proof. iIntros "HP". iExists (0:nat). iApply ("HP" $! (0:nat)). Qed.
(* tests/proofmode.v *)
Lemma test_iExist_tc `{Set_ A C} P : ⊢ ∃ x1 x2 : gset positive, P -∗ P.
Proof. iExists {[ 1%positive ]}, ∅. auto. Qed.
(* tests/proofmode.v *)
Lemma test_iSpecialize_tc P : (∀ x y z : gset positive, P) -∗ P.
Proof.
  (** Test that type classes in specialization patterns are resolved. Both when
  using [iSpecialize] and tactics that use [iSpecialize] internally. *)
  iIntros "H".
  (* We use [unshelve] to test that there are no unshelved goals *)
  unshelve iSpecialize ("H" $! ∅ {[ 1%positive ]} ∅). done.
Restart. Proof.
  iIntros "H". solve [unshelve iApply ("H" $! ∅ {[ 1%positive ]} ∅)].
Qed.
(* tests/proofmode.v *)
Lemma test_iSpecialize_tc_args P : (∀ x y z : gset positive, ⊢ P) → ⊢ P.
Proof.
  (** Similarly as above, but the arguments of [H] now live at the Rocq level *)
  intros H. solve [unshelve iApply (H ∅ {[ 1%positive ]} ∅)].
Qed.
(* tests/proofmode.v *)
Lemma test_iSpecialize_tc_done_specpat P :
  (∀ X : gset nat, (if decide (X = ∅) then True else False) -∗ P) -∗ P.
Proof.
  (** Test that the instance for [∅] is resolved before the [//] pattern is
  executed, and not only at the very end. *)
  iIntros "H". iApply ("H" $! ∅ with "[//]").
Qed.
(* tests/proofmode.v *)
Lemma test_iSpecialize_tc_done_args P :
  (∀ X : gset nat, (if decide (X = ∅) then True else False) -∗ P) →
  ⊢ P.
Proof. intros H. iApply (H ∅ with "[//]"). Qed.
(* tests/proofmode.v *)
Lemma test_iSpecialize_tc_exact_specpat P Q :
  Q -∗ (∀ X : gset nat, (if decide (X = ∅) then Q else False) -∗ P) -∗ P.
Proof. iIntros "HQ H". iApply ("H" $! ∅ with "HQ"). Qed.
(* tests/proofmode.v *)
Lemma test_iSpecialize_tc_exact_args P Q :
  (∀ X : gset nat, (if decide (X = ∅) then Q else False) -∗ P) →
  Q -∗ P.
Proof. iIntros (H) "HQ". iApply (H ∅ with "HQ"). Qed.
(* tests/proofmode.v *)
Lemma test_iSpecialize_tc_dependency_specpat P :
  (∀ A (_ : Inhabited A) (_ : EqDecision A),
    (if decide (inhabitant =@{A} inhabitant) then True else False) -∗ P) -∗
  P.
Proof.
  (* A variation of the previous test, where the instances depend on a prior
  argument (here [A]). We test that it also works with and without underscores. *)
  iIntros "H". unshelve iSpecialize ("H" $! nat _ _). iApply "H".
Restart. Proof.
  iIntros "H". iApply ("H" $! nat _ _ with "[//]").
Restart. Proof.
  iIntros "H". iApply ("H" $! nat with "[//]").
Qed.
(* tests/proofmode.v *)
Lemma test_iSpecialize_tc_dependency_args P :
  (∀ `{!Inhabited A, !EqDecision A},
    (if decide (inhabitant =@{A} inhabitant) then True else False) -∗ P) →
  ⊢ P.
Proof.
  intros H. unshelve iPoseProof (H nat _ _) as "H". by iApply "H".
Restart. Proof.
  intros H. iApply (H nat _ _ with "[//]").
Restart. Proof.
  intros H. iApply (H nat with "[//]").
Qed.
(* tests/proofmode.v *)
Lemma test_iSpecialize_tc_dependency_lem P :
  let lem (A : Type) := (∀ (ia : Inhabited A), ∀(eqd : EqDecision A),
    ((if decide (inhabitant =@{A} inhabitant) then True else False) -∗ P) : Prop) in
  (∀ A, lem A) →
  ⊢ P.
Proof.
  (* We hide part of the "lemma" behind a definition. This means that the "fast
  path" in [_iIntoEmpValid_go] is not used. *)
  intros lem H. unshelve iPoseProof (H nat _ _) as "lem". by iApply "lem".
Restart. Proof.
  intros lem H. iApply (H nat _ _ with "[//]").
Restart. Proof.
  intros lem H. iApply (H nat with "[//]").
Qed.
(* tests/proofmode.v *)
Lemma test_iSpecialize_tc_dependency_specpat_2 P :
  (∀ A (_ : Empty A) (_ : ∀ m, Decision (m =@{A} ∅)),
    (if decide (∅ =@{A} ∅) then True else False) -∗ P) -∗
  P.
Proof.
  (* Another variation with dependencies between the arguments. In order to
  solve [Decision], we need to solve [Empty] because [Decision] on [gmap] only
  holds for the empty element. *)
  iIntros "H".
  unshelve iSpecialize ("H" $! (gmap nat (nat → nat)) _ _). iApply "H".
Restart. Proof.
  iIntros "H". iApply ("H" $! (gmap nat (nat → nat)) _ _ with "[//]").
Restart. Proof.
  iIntros "H". iApply ("H" $! (gmap nat (nat → nat)) with "[//]").
Qed.
(* tests/proofmode.v *)
Lemma test_iSpecialize_tc_dependency_args_2 P :
  (∀ A `{!Empty A, !∀ m, Decision (m =@{A} ∅)},
    (if decide (∅ =@{A} ∅) then True else False) -∗ P) →
  ⊢ P.
Proof.
  intros H.
  unshelve iPoseProof (H (gmap nat (nat → nat)) _ _) as "lem". iApply "lem".
Restart. Proof.
  intros H. iApply (H (gmap nat (nat → nat)) _ _ with "[//]").
Restart. Proof.
  intros H. iApply (H (gmap nat (nat → nat)) with "[//]").
Qed.
(* tests/proofmode.v *)
Lemma test_iFrame_pure `{!Sbi PROP} {A : ofe} (φ : Prop) (y z : A) :
  φ → <affine> ⌜y ≡ z⌝ -∗ (⌜ φ ⌝ ∧ ⌜ φ ⌝ ∧ y ≡ z : PROP).
Proof. iIntros (Hv) "#Hxy". iFrame (Hv) "Hxy". Qed.
(* tests/proofmode.v *)
Lemma test_iFrame_disjunction_1 P1 P2 Q1 Q2 :
  BiAffine PROP →
  □ P1 -∗ Q2 -∗ P2 -∗ (P1 ∗ P2 ∗ False ∨ P2) ∗ (Q1 ∨ Q2).
Proof. intros ?. iIntros "#HP1 HQ2 HP2". iFrame "HP1 HQ2 HP2". Qed.
(* tests/proofmode.v *)
Lemma test_iFrame_disjunction_2 P : P -∗ (True ∨ True) ∗ P.
Proof. iIntros "HP". iFrame "HP". auto. Qed.
(* tests/proofmode.v *)
Lemma test_iFrame_disjunction_3_evars (Φ : nat → PROP) P1 P2 P3 P4 :
  BiAffine PROP →
  let n := 5 in
  let R := λ a, Nat.iter n (λ P, (P1 ∗ P2 ∗ P3 ∗ P4 ∗ Φ a) ∨ P)%I (Φ a) in
  P1 ⊢ ∃ a, R a.
Proof.
  intros ?. simpl. iIntros "HP1". iExists _.
  Timeout 2 iFrame. (* The combination of evars and nested disjunctions used to
  cause excessive backtracking during the construction of [Frame] instances,
  which made [iFrame] very slow. Above [Timeout] ensures [iFrame] now performs
  acceptably in this situation *)
Abort.
(* tests/proofmode.v *)
Lemma test_iFrame_disjunction_4_evars (Φ : nat → nat → PROP) P :
  Φ 0 1 ⊢ ∃ n m, (Φ n m ∗ Φ 0 1) ∨ (P ∗ Φ m n).
Proof.
  iIntros "HΦ1". iExists _, _.
  Fail iFrame "HΦ1". (* During the construction of [Frame] instances for
  disjunctions, [Frame] instances for each of the sides should be constructed
  _exactly_ once. This test shows that after finding a way to frame "HΦ1" on
  the left-hand side of the disjunction (and instantiating [n = 0] and [m = 1])
  the second way of framing "HΦ1" in the left-hand side is not considered,
  even though this would cause the framing to be successful on the right-hand
  side. Considering multiple successes can cause exponential blowups, see above *)
Abort.
(* tests/proofmode.v *)
Lemma test_iFrame_conjunction_1 P Q :
  P -∗ Q -∗ (P ∗ Q) ∧ (P ∗ Q).
Proof. iIntros "HP HQ". iFrame "HP HQ". Qed.
(* tests/proofmode.v *)
Lemma test_iFrame_conjunction_2 P Q :
  P -∗ Q -∗ (P ∧ P) ∗ (Q ∧ Q).
Proof. iIntros "HP HQ". iFrame "HP HQ". Qed.
(* tests/proofmode.v *)
Lemma test_iFrame_conjunction_3 P Q `{!Absorbing Q} :
  P -∗ Q -∗ ((P ∗ False) ∧ Q).
Proof.
  iIntros "HP HQ".
  iFrame "HP".
  (* [iFrame] should simplify [False ∧ Q] to just [False]. *)
  Show.
Abort.
(* tests/proofmode.v *)
Lemma test_iFrame_conjunction_4_evars (Φ : nat → PROP) P1 P2 P3 P4 P5 :
  BiAffine PROP →
  let n := 5 in
  let R := λ a, Nat.iter n (λ P, (P1 ∗ P2 ∗ P3 ∗ P4 ∗ Φ a) ∧ P)%I (P1 ∗ P2 ∗ P3 ∗ P4 ∗ Φ a)%I in
  P5 ⊢ ∃ a, R a.
Proof.
  intros ?. simpl. iIntros "HP1". iExists _.
  Timeout 1 iFrame. (* The combination of evars and nested conjunctions used to
  cause excessive backtracking during the construction of [Frame] instances,
  which made [iFrame] very slow. Above [Timeout] ensures [iFrame] now performs
  acceptably in this situation *)
Abort.
(* tests/proofmode.v *)
Lemma test_iFrame_exists_instantiate (Φ Ψ : nat → PROP) P Q :
  P ∗ Φ 0 ∗ Ψ 1 ∗ Q ⊢ ∃ n, Φ n ∗ ∃ m, Ψ m ∗ P ∗ Q.
Proof.
  iIntros "(HP & HΦ & HΨ & HQ)".
  iFrame "HΨ". (* instantiates the inner existential quantifier [m] *) Show.
  iFrame "HP". (* keeps the outer existential quantifier [n] around *) Show.
  iFrame "HΦ". (* instantiates the outer existential quantifier [n] *) Show.
  done.
Qed.
(* tests/proofmode.v *)
Lemma test_wrong_instantiation (Φ : nat → PROP) :
  Φ 0 ∗ Φ 1 ⊢ ∃ n m, Φ n ∗ Φ m ∗ ⌜n = 0⌝ ∗ ⌜m = 1⌝.
Proof. iIntros "[HΦ1 HΦ2]". iFrame. Show. Abort.
(* tests/proofmode.v *)
Lemma test_iFrame_nary_exists (Φ Ψ : nat → PROP) P Q :
  let n := 10 in
  let R := Nat.iter n (λ P, ∃ n : nat, P ∗ ⌜n = 0⌝)%I (∃ m, Φ m ∗ P)%I in
  P ∗ Φ 0 ⊢ R.
Proof.
  simpl.
  (* This test asserts that the [Frame] instance for existential quantifiers
  performs acceptably when the number of quantifiers becomes larger. A naive
  implementation of this functionality would face an exponential slowdown. *)
  iIntros "[HP HΦ]".
  Timeout 1 iFrame "HP".
  Timeout 1 iFrame "HΦ".
  repeat (iExists 0; iSplit); eauto.
Qed.
(* tests/proofmode.v *)
Lemma test_iFrame_exists_under_definition (Φ : nat → PROP) :
  let P := (∃ n m, Φ m ∗ Φ n ∗ ⌜n = 0⌝ ∗ ⌜m = 1⌝)%I in
  Φ 0 ∗ Φ 1 ⊢ P.
Proof. iIntros (P) "[HΦ1 HΦ2]". by iFrame. Qed.
(* tests/proofmode.v *)
Lemma test_iFrame_no_instantiate_under_forall (P : nat → PROP) :
  □ P 0 ⊢ P 0 ∗ (∀ m : nat, ∃ n, P n ∗ ⌜n = m⌝ ∗ P 0).
Proof.
  iIntros "#$". Show.
  (* [P 0] should get framed, [∃ n, P n] should remain untouched *)
Abort.
(* tests/proofmode.v *)
Lemma test_iFrame_no_instantiate_under_wand (P : nat → PROP) :
  □ P 0 ⊢ P 0 ∗ (P 1 -∗ ∃ n, P n ∗ ⌜n = 1⌝ ∗ P 0).
Proof.
  iIntros "#$". Show.
  (* [P 0] should get framed, [∃ n, P n] should remain untouched *)
Abort.
(* tests/proofmode.v *)
Lemma test_iFrame_no_instantiate_under_impl (P : nat → PROP) :
  □ P 0 ⊢ P 0 ∗ (P 1 → ∃ n, P n ∗ ⌜n = 1⌝ ∗ P 0).
Proof.
  iIntros "#$". Show.
  (* [P 0] should get framed, [∃ n, P n] should remain untouched *)
Abort.
(* tests/proofmode.v *)
Lemma test_iFrame_later `{!BiAffine PROP} P Q : P -∗ Q -∗ ▷ P ∗ Q.
Proof. iIntros "H1 H2". by iFrame "H1". Qed.
(* tests/proofmode.v *)
Lemma test_iFrame_affinely_1 P Q `{!Affine P} :
  P -∗ <affine> Q -∗ <affine> (P ∗ Q).
Proof. iIntros "HP HQ". iFrame "HQ". by iModIntro. Qed.
(* tests/proofmode.v *)
Lemma test_iFrame_affinely_2 P Q `{!Affine P, !Affine Q} :
  P -∗ Q -∗ <affine> (P ∗ Q).
Proof. iIntros "HP HQ". iModIntro. iFrame "HQ". done. Qed.
(* tests/proofmode.v *)
Lemma test_iFrame_affinely_emp P :
  □ P -∗ ∃ _ : nat, <affine> P.
(* The ∃ makes sure [iFrame] does not solve the
  goal and we can [Show] the result *)
Proof.
  iIntros "#H". iFrame "H".
  Show. (* This should become [∃ _ : nat, emp]. *)
  by iExists 1.
Qed.
(* tests/proofmode.v *)
Lemma test_iFrame_affinely_True `{!BiAffine PROP} P :
  □ P -∗ ∃ x : nat, <affine> P.
Proof.
  iIntros "#H". iFrame "H".
  Show. (* This should become [∃ _ : nat, True]. Since we are in an affine BI,
  no unnecessary [emp]s should be created. *)
  by iExists 1.
Qed.
(* tests/proofmode.v *)
Lemma test_iFrame_or_1 P1 P2 P3 :
  P1 ∗ P2 ∗ P3 -∗ P1 ∗ ▷ (P2 ∗ ∃ x, (P3 ∗ <affine> ⌜x = 0⌝) ∨ P3).
Proof.
  iIntros "($ & $ & $)".
  Show. (* By framing [P3], the disjunction becomes [<affine> ⌜x = 0⌝ ∨ emp].
  The [iFrame] tactic simplifies disjunctions if one side is trivial. In a
  general BI, it can only turn [Q ∨ emp] into [emp]---without information
  loss---if [Q] is affine. Here, we have [Q := <affine> ⌜x = 0⌝], which is
  trivially affine (i.e., [QuickAffine]), and the disjunction is thus
  simplified to [emp]. *)
  by iExists 0.
Qed.
(* tests/proofmode.v *)
Lemma test_iFrame_or_2 P1 P2 P3 :
  P1 ∗ P2 ∗ P3 -∗ P1 ∗ ▷ (P2 ∗ ∃ x, (P3 ∧ ⌜x = 0⌝) ∨ P3).
Proof.
  iIntros "($ & $ & $)".
  Show. (* By framing [P3], the disjunction becomes [emp ∧ ⌜x = 0⌝ ∨ emp].
  Since [emp ∧ ⌜x = 0⌝] is not trivially affine (i.e., not [QuickAffine]) it
  is not simplified to [emp]. *)
  iExists 0. auto.
Qed.
(* tests/proofmode.v *)
Lemma test_iFrame_or_3 P1 P2 P3 :
  P1 ∗ P2 ∗ P3 -∗ P1 ∗ ▷ (P2 ∗ ∃ x, (P3 ∗ ⌜x = 0⌝) ∨ (False ∗ P3)).
Proof.
  iIntros "($ & $ & $)".
  Show. (* After framing [P3], the disjunction becomes [⌜x = 0⌝ ∨ False].
  The simplification of disjunctions by [iFrame] will now get rid of the
  [∨ False], to just [⌜x = 0⌝] *)
  by iExists 0.
Qed.
(* tests/proofmode.v *)
Lemma test_iFrame_or_affine_1 `{!BiAffine PROP} P1 P2 P3 :
  P1 ∗ P2 ∗ P3 -∗ P1 ∗ ▷ (P2 ∗ ∃ x, (P3 ∗ ⌜x = 0⌝) ∨ P3).
Proof.
  iIntros "($ & $ & $)".
  Show. (* If the BI is affine, the disjunction should be turned into [True]. *)
  by iExists 0.
Qed.
(* tests/proofmode.v *)
Lemma test_iFrame_or_affine_2 `{!BiAffine PROP} P1 P2 P3 :
  P1 ∗ P2 ∗ P3 -∗ P1 ∗ ▷ (P2 ∗ ∃ x, (P3 ∧ ⌜x = 0⌝) ∨ P3).
Proof.
  iIntros "($ & $ & $)".
  Show. (* If the BI is affine, the disjunction should be turned into [True]. *)
  by iExists 0.
Qed.
(* tests/proofmode.v *)
Lemma test_iFrame_useless `{BiAffine PROP} P Q : P -∗ Q -∗ P.
Proof.
  iIntros "HP HQ".
  Fail iFrame "HP HQ".
  Fail iFrame "HQ HP".
Abort.
(* tests/proofmode.v *)
Lemma test_iDestruct_frame_useless `{!BiAffine PROP} P Q :
  (P -∗ True) ∗ P ∗ Q -∗ Q.
Proof.
  iIntros "(Hwand & HP & HQ)".
  Fail iDestruct ("Hwand" with "[$HP $HQ]") as "_".
Abort.
(* tests/proofmode.v *)
Lemma test_iAssert_modality P : ◇ False -∗ ▷ P.
Proof.
  iIntros "HF".
  iAssert (<affine> False)%I with "[> -]" as %[].
  by iMod "HF".
Qed.
(* tests/proofmode.v *)
Lemma test_iMod_affinely_timeless P `{!Timeless P} :
  <affine> ▷ P -∗ ◇ <affine> P.
Proof. iIntros "H". iMod "H". done. Qed.
(* tests/proofmode.v *)
Lemma test_iAssumption_False P : False -∗ P.
Proof. iIntros "H". done. Qed.
(* tests/proofmode.v *)
Lemma test_iAssumption_coq_1 P Q : (⊢ Q) → <affine> P -∗ Q.
Proof. iIntros (HQ) "_". iAssumption. Qed.
(* tests/proofmode.v *)
Lemma test_iAssumption_coq_2 P Q : (⊢ □ Q) → <affine> P -∗ ▷ Q.
Proof. iIntros (HQ) "_". iAssumption. Qed.
(* tests/proofmode.v *)
(* Check instantiation and dependent types *)
Lemma test_iSpecialize_dependent_type (P : ∀ n, vec nat n → PROP) :
  (∀ n v, P n v) -∗ ∃ n v, P n v.
Proof.
  iIntros "H". iExists _, [#10].
  iSpecialize ("H" $! _ [#10]). done.
Qed.
(* tests/proofmode.v *)
(* Check that typeclasses are not resolved too early *)
Lemma test_TC_resolution `{!BiAffine PROP} (Φ : nat → PROP) l x :
  x ∈ l → ([∗ list] y ∈ l, Φ y) -∗ Φ x.
Proof.
  iIntros (Hp) "HT".
  iDestruct (big_sepL_elem_of _ _ _ Hp with "HT") as "Hp".
  done.
Qed.
(* tests/proofmode.v *)
Lemma test_eauto_iFrame P Q R `{!Persistent R} :
  P -∗ Q -∗ R → R ∗ Q ∗ P ∗ R ∨ False.
Proof. eauto 10 with iFrame. Qed.
(* tests/proofmode.v *)
Lemma test_iCombine_persistent P Q R `{!Persistent R} :
  P -∗ Q -∗ R → R ∗ Q ∗ P ∗ R ∨ False.
Proof. iIntros "HP HQ #HR". iCombine "HR HQ HP HR" as "H". auto. Qed.
(* tests/proofmode.v *)
Lemma test_iCombine_frame P Q R `{!Persistent R} :
  P -∗ Q -∗ R → R ∗ Q ∗ P ∗ R.
Proof. iIntros "HP HQ #HR". iCombine "HQ HP HR" as "$". by iFrame. Qed.
(* tests/proofmode.v *)
Lemma test_iCombine_nested_no_gives P Q :
  <absorb><affine> P -∗ <absorb><affine> Q -∗ <absorb><affine> (P ∗ Q).
Proof.
  iIntros "HP HQ".
  Fail iCombine "HP HQ" gives "Htriv".
  Fail iCombine "HP HQ" as "HPQ" gives "Htriv".
  iCombine "HP HQ" as "HPQ".
  iExact "HPQ".
Qed.
(* tests/proofmode.v *)
Lemma test_iCombine_nested_gives1 P Q R :
  CombineSepGives P Q R →
  <absorb><affine> P -∗ <absorb><affine> Q -∗ <pers> R.
Proof.
  move => HPQR. iIntros "HP HQ".
  iCombine "HP HQ" gives "#HR".
  iExact "HR".
Qed.
(* tests/proofmode.v *)
Lemma test_iCombine_nested_gives2 n P Q R :
  CombineSepGives P Q R →
  ▷^n ◇ P -∗ ▷^n ◇ Q -∗ ▷^n ◇ (P ∗ Q) ∗ <pers> ▷^n ◇ R.
Proof.
  move => HPQR. iIntros "HP HQ".
  iCombine "HP HQ" as "HPQ" gives "#HR".
  iSplitL "HPQ"; first iExact "HPQ".
  iExact "HR".
Qed.
(* tests/proofmode.v *)
Lemma test_iNext_evar P : P -∗ True.
Proof.
  iIntros "HP". iAssert (▷ _ -∗ ▷ P)%I as "?"; last done.
  iIntros "?". iNext. iAssumption.
Qed.
(* tests/proofmode.v *)
Lemma test_iNext_sep1 P Q (R1 := (P ∗ Q)%I) :
  (▷ P ∗ ▷ Q) ∗ R1 -∗ ▷ ((P ∗ Q) ∗ R1).
Proof.
  iIntros "H". iNext.
  rewrite {1 2}(lock R1). (* check whether R1 has not been unfolded *) done.
Qed.
(* tests/proofmode.v *)
Lemma test_iNext_sep2 P Q : ▷ P ∗ ▷ Q -∗ ▷ (P ∗ Q).
Proof.
  iIntros "H". iNext. iExact "H". (* Check that the laters are all gone. *)
Qed.
(* tests/proofmode.v *)
Lemma test_iNext_quantifier {A} (Φ : A → A → PROP) :
  (∀ y, ∃ x, ▷ Φ x y) -∗ ▷ (∀ y, ∃ x, Φ x y).
Proof. iIntros "H". iNext. done. Qed.
(* tests/proofmode.v *)
Lemma text_iNext_Next `{!Sbi PROP} {A B : ofe} (f : A -n> A) x y :
  Next x ≡ Next y -∗ (Next (f x) ≡ Next (f y) : PROP).
Proof. iIntros "H". iNext. by iRewrite "H". Qed.
(* tests/proofmode.v *)
Lemma test_iFrame_persistent (P Q : PROP) :
  □ P -∗ Q -∗ <pers> (P ∗ P) ∗ (P ∗ Q ∨ Q).
Proof. iIntros "#HP". iFrame "HP". iIntros "$". Qed.
(* tests/proofmode.v *)
Lemma test_iSplit_persistently P Q : □ P -∗ <pers> (P ∗ P).
Proof. iIntros "#?". by iSplit. Qed.
(* tests/proofmode.v *)
Lemma test_iSpecialize_persistent P Q : □ P -∗ (<pers> P → Q) -∗ Q.
Proof. iIntros "#HP HPQ". by iSpecialize ("HPQ" with "HP"). Qed.
(* tests/proofmode.v *)
Lemma test_iDestruct_persistent P (Φ : nat → PROP) `{!∀ x, Persistent (Φ x)}:
  □ (P -∗ ∃ x, Φ x) -∗
  P -∗ ∃ x, Φ x ∗ P.
Proof.
  iIntros "#H HP". iDestruct ("H" with "HP") as (x) "#H2". eauto with iFrame.
Qed.
(* tests/proofmode.v *)
Lemma test_iLöb `{!BiLöb PROP} P : ⊢ ∃ n, ▷^n P.
Proof.
  iLöb as "IH". iDestruct "IH" as (n) "IH".
  by iExists (S n).
Qed.
(* tests/proofmode.v *)
Lemma test_iLöb_forall `{!BiLöb PROP} P (n : nat) : P ⊢ ⌜ n = n ⌝.
Proof.
  iIntros "HP". iLöb as "IH" forall (n) "HP".
Restart. Proof.
  iIntros "HP". iLöb as "IH" forall "HP".
Restart. Proof.
  iIntros "HP". iLöb as "IH" forall (n).
Restart. Proof.
  iIntros "HP". iLöb as "IH".
Abort.
(* tests/proofmode.v *)
Lemma test_iInduction_wf (x : nat) P Q :
  □ P -∗ Q -∗ ⌜ (x + 0 = x)%nat ⌝.
Proof.
  iIntros "#HP HQ".
  iInduction (lt_wf x) as [[|x] _ IH]; simpl; first done.
  rewrite (inj_iff S). by iApply ("IH" with "[%]"); first lia.
Qed.
(* tests/proofmode.v *)
Lemma test_iInduction_using (m : gmap nat nat) (Φ : nat → nat → PROP) y :
  ([∗ map] x ↦ i ∈ m, Φ y x) -∗ ([∗ map] x ↦ i ∈ m, emp ∗ Φ y x).
Proof.
  iIntros "Hm". iInduction m as [|i x m ? IH] using map_ind forall (y).
  - by rewrite !big_sepM_empty.
  - rewrite !big_sepM_insert //. iDestruct "Hm" as "[$ ?]".
    by iApply "IH".
Qed.
(* tests/proofmode.v *)
(* From https://gitlab.mpi-sws.org/iris/iris/-/issues/534 *)
Lemma test_iInduction_big_sepL_impl' {A} (Φ Ψ : nat → A → PROP) (l1 l2 : list A) :
  length l1 = length l2 →
  ([∗ list] k↦x ∈ l1, Φ k x) -∗
  □ (∀ k x1 x2, ⌜l1 !! k = Some x1⌝ -∗ ⌜l2 !! k = Some x2⌝ -∗ Φ k x1 -∗ Ψ k x2) -∗
  [∗ list] k↦x ∈ l2, Ψ k x.
Proof.
  iIntros (Hlen) "Hl #Himpl".
  iInduction l1 as [|x1 l1 IH] forall (Φ Ψ l2 Hlen).
Abort.
(* tests/proofmode.v *)
Inductive tree
:= leaf | node (l r: tree).
(* tests/proofmode.v *)
Lemma test_iInduction_multiple_IHs (t: tree) (Φ : tree → PROP) :
  □ Φ leaf -∗ □ (∀ l r, Φ l -∗ Φ r -∗ Φ (node l r)) -∗ Φ t.
Proof.
  iIntros "#Hleaf #Hnode". iInduction t as [|l IHl r IHr].
  - iExact "Hleaf".
  - Show. (* should have "IHl" and "IHr", since [node] has two trees *)
    iApply ("Hnode" with "IHl IHr").
Qed.