phanerozoic/Coq-Iris huggingface dataset:
(* tests/proofmode.v *)
(* Copies of the above tests for the legacy syntax of naming IHs *)
Lemma test_iInduction_wf_legacy (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_legacy (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 *)
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 *)
Lemma test_iInduction_multiple_IHs_legacy (t: tree) (Φ : tree → PROP) :
  □ Φ leaf -∗ □ (∀ l r, Φ l -∗ Φ r -∗ Φ (node l r)) -∗ Φ t.
Proof.
  iIntros "#Hleaf #Hnode". iInduction t as [|l ? r] "IH".
  - iExact "Hleaf".
  - Show. (* should have "IH" and "IH1", since [node] has two trees *)
    iApply ("Hnode" with "IH IH1").
Qed.
(* tests/proofmode.v *)
Lemma test_iIntros_start_proof :
  ⊢@{PROP} True.
Proof.
  (* Make sure iIntros actually makes progress and enters the proofmode. *)
  progress iIntros. done.
Qed.
(* tests/proofmode.v *)
Lemma test_True_intros : (True : PROP) -∗ True.
Proof.
  iIntros "?". done.
Qed.
(* tests/proofmode.v *)
Lemma test_iPoseProof_let_entails P Q :
  (let R := True%I in R ∗ P ⊢ Q) →
  P ⊢ Q.
Proof.
  iIntros (help) "HP".
  iPoseProof (help with "[$HP]") as "?". done.
Qed.
(* tests/proofmode.v *)
Lemma test_iPoseProof_let_wand P Q :
  (let R := True%I in R ∗ P -∗ Q) →
  P -∗ Q.
Proof.
  iIntros (help) "HP".
  iPoseProof (help with "[$HP]") as "?". done.
Qed.
(* tests/proofmode.v *)
Lemma test_iPoseProof_let_entails_pm_intro_pat P Q :
  (let R := True%I in R ∗ P ⊢ Q) →
  P ⊢ Q.
Proof.
  iIntros "%help HP".
  iPoseProof (help with "[$HP]") as "?". done.
Qed.
(* tests/proofmode.v *)
Lemma test_iIntros_let_entails P :
  ∀ Q, let R := emp%I in P ⊢ R -∗ Q -∗ P ∗ Q.
Proof. iIntros (Q R) "$ _ $". Qed.
(* tests/proofmode.v *)
Lemma test_iIntros_let_wand P :
  ∀ Q, let R := emp%I in P -∗ R -∗ Q -∗ P ∗ Q.
Proof. iIntros (Q R) "$ _ $". Qed.
(* tests/proofmode.v *)
Lemma lemma_for_test_apply_entails_below_let (Φ : nat → PROP) :
  let Q := Φ 5 in
  Q ⊢ Q.
Proof. iIntros (?) "?". done. Qed.
(* tests/proofmode.v *)
Lemma test_apply_entails_below_let (Φ : nat → PROP) :
  Φ 5 -∗ Φ 5.
Proof. iIntros "?". iApply lemma_for_test_apply_entails_below_let. done. Qed.
(* tests/proofmode.v *)
Lemma lemma_for_test_apply_wand_below_let (Φ : nat → PROP) :
  let Q := Φ 5 in
  Q -∗ Q.
Proof. iIntros (?) "?". done. Qed.
(* tests/proofmode.v *)
Lemma test_apply_wand_below_let (Φ : nat → PROP) :
  Φ 5 -∗ Φ 5.
Proof. iIntros "?". iApply lemma_for_test_apply_wand_below_let. done. Qed.
(* tests/proofmode.v *)
Lemma test_iNext_iRewrite `{!Sbi PROP} P Q :
  <affine> ▷ (Q ≡ P) -∗ <affine> ▷ Q -∗ <affine> ▷ P.
Proof.
  iIntros "#HPQ HQ !>". iNext. by iRewrite "HPQ" in "HQ".
Qed.
(* tests/proofmode.v *)
Lemma test_iIntros_modalities `{!BiPersistentlyForall PROP} `(!Absorbing P) :
  ⊢ <pers> (▷ ∀  x : nat, ⌜ x = 0 ⌝ → ⌜ x = 0 ⌝ -∗ False -∗ P -∗ P).
Proof.
  iIntros (x ??).
  iIntros "* **". (* Test that fast intros do not work under modalities *)
  iIntros ([]).
Qed.
(* tests/proofmode.v *)
Lemma test_iIntros_rewrite P (x1 x2 x3 x4 : nat) :
  x1 = x2 → (⌜ x2 = x3 ⌝ ∗ ⌜ x3 ≡ x4 ⌝ ∗ P) -∗ ⌜ x1 = x4 ⌝ ∗ P.
Proof. iIntros (?) "(-> & -> & $)"; auto. Qed.
(* tests/proofmode.v *)
Lemma test_iIntros_leibniz_equiv `{!Sbi PROP} {A : ofe} (x y : A) :
  Discrete x → LeibnizEquiv A →
  x ≡ y ⊢@{PROP} ⌜x = y⌝.
Proof.
  intros ??.
  iIntros (->). (* test that the [IntoPure] instance converts [≡] into [=] *)
  done.
Qed.
(* tests/proofmode.v *)
Lemma test_iIntros_leibniz_equiv_prod `{!Sbi PROP}
    {A B : ofe} (a1 a2 : A) (b1 b2 : B) :
  Discrete a1 → Discrete b1 → LeibnizEquiv A → LeibnizEquiv B →
  (a1, b1) ≡ (a2, b2) ⊢@{PROP} ⌜a1 = a2⌝.
Proof.
  intros ????.
  iIntros ([-> _]%pair_eq).
  (* another test that the [IntoPure] instance converts [≡] into [=], also under
  combinators *)
  done.
Qed.
(* tests/proofmode.v *)
Lemma test_iPureIntro_leibniz_equiv `{!Sbi PROP}
    {A : ofe} `{!LeibnizEquiv A} (x y : A) :
  (x ≡ y) → ⊢@{PROP} x ≡ y.
Proof.
  intros Heq. iPureIntro.
  (* test that the [FromPure] instance does _not_ convert [≡] into [=] *)
  exact Heq.
Qed.
(* tests/proofmode.v *)
Lemma test_iDestruct_rewrite_not_consume P (x1 x2 : nat) :
  (P -∗ ⌜ x1 = x2 ⌝) →
  P -∗ ⌜ x1 = x2 ⌝ ∗ P.
Proof.
  iIntros (lemma) "HP". iDestruct (lemma with "HP") as "->".
  auto. (* Make sure that "HP" has not been consumed; [auto] would fail
  otherwise. *)
Qed.
(* tests/proofmode.v *)
Lemma test_iNext_affine `{!Sbi PROP} P Q :
  <affine> ▷ (Q ≡ P) -∗ <affine> ▷ Q -∗ <affine> ▷ P.
Proof. iIntros "#HPQ HQ !>". iNext. by iRewrite "HPQ" in "HQ". Qed.
(* tests/proofmode.v *)
Lemma test_iAlways P Q R :
  □ P -∗ <pers> Q → R -∗ <pers> <affine> <affine> P ∗ □ Q.
Proof.
  iIntros "#HP #HQ HR". iSplitL.
  - iModIntro. done.
  - iModIntro. done.
Qed.
(* tests/proofmode.v *)
(* A bunch of test cases from #127 to establish that tactics behave the same on
`⌜ φ ⌝ → P` and `∀ _ : φ, P` *)
Lemma test_forall_nondep_1 (φ : Prop) :
  φ → (∀ _ : φ, False : PROP) -∗ False.
Proof. iIntros (Hφ) "Hφ". by iApply "Hφ". Qed.
(* tests/proofmode.v *)
Lemma test_forall_nondep_2 (φ : Prop) :
  φ → (∀ _ : φ, False : PROP) -∗ False.
Proof. iIntros (Hφ) "Hφ". iSpecialize ("Hφ" with "[% //]"). done. Qed.
(* tests/proofmode.v *)
Lemma test_forall_nondep_3 (φ : Prop) :
  φ → (∀ _ : φ, False : PROP) -∗ False.
Proof. iIntros (Hφ) "Hφ". unshelve iSpecialize ("Hφ" $! _); done. Qed.
(* tests/proofmode.v *)
Lemma test_forall_nondep_4 (φ : Prop) :
  φ → (∀ _ : φ, False : PROP) -∗ False.
Proof. iIntros (Hφ) "Hφ". iSpecialize ("Hφ" $! Hφ); done. Qed.
(* tests/proofmode.v *)
Lemma test_pure_impl_1 (φ : Prop) :
  φ → (⌜φ⌝ → False : PROP) -∗ False.
Proof. iIntros (Hφ) "Hφ". by iApply "Hφ". Qed.
(* tests/proofmode.v *)
Lemma test_pure_impl_2 (φ : Prop) :
  φ → (⌜φ⌝ → False : PROP) -∗ False.
Proof. iIntros (Hφ) "Hφ". iSpecialize ("Hφ" with "[% //]"). done. Qed.
(* tests/proofmode.v *)
Lemma test_pure_impl_3 (φ : Prop) :
  φ → (⌜φ⌝ → False : PROP) -∗ False.
Proof. iIntros (Hφ) "Hφ". unshelve iSpecialize ("Hφ" $! _); done. Qed.
(* tests/proofmode.v *)
Lemma test_pure_impl_4 (φ : Prop) :
  φ → (⌜φ⌝ → False : PROP) -∗ False.
Proof. iIntros (Hφ) "Hφ". iSpecialize ("Hφ" $! Hφ). done. Qed.
(* tests/proofmode.v *)
Lemma test_forall_nondep_impl2 (φ : Prop) P :
  φ → P -∗ (∀ _ : φ, P -∗ False : PROP) -∗ False.
Proof.
  iIntros (Hφ) "HP Hφ".
  Fail iSpecialize ("Hφ" with "HP").
  iSpecialize ("Hφ" with "[% //] HP"). done.
Qed.
(* tests/proofmode.v *)
Lemma test_pure_impl2 (φ : Prop) P :
  φ → P -∗ (⌜φ⌝ → P -∗ False : PROP) -∗ False.
Proof.
  iIntros (Hφ) "HP Hφ".
  Fail iSpecialize ("Hφ" with "HP").
  iSpecialize ("Hφ" with "[% //] HP"). done.
Qed.
(* tests/proofmode.v *)
Lemma demo_laterN_forall {A} (Φ Ψ: A → PROP) n: (∀ x, ▷^n Φ x) -∗ ▷^n (∀ x, Φ x).
Proof.
  iIntros "H" (w). iApply ("H" $! w).
Qed.
(* tests/proofmode.v *)
Lemma test_iNext_laterN_later P n : ▷ ▷^n P -∗ ▷^n ▷ P.
Proof. iIntros "H". iNext. by iNext. Qed.
(* tests/proofmode.v *)
Lemma test_iNext_laterN_bool_later b P : ▷?b P -∗ ▷ P.
Proof. iIntros "H". by iNext. Qed.
(* tests/proofmode.v *)
Lemma test_iNext_laterN_bool_later_2 b P : ▷?b ▷ P -∗ ▷ ▷?b P.
Proof. iIntros "H". by do 2 iNext. Qed.
(* tests/proofmode.v *)
Lemma test_iNext_later_laterN P n : ▷^n ▷ P -∗ ▷ ▷^n P.
Proof. iIntros "H". iNext. by iNext. Qed.
(* tests/proofmode.v *)
Lemma test_iNext_plus_1 P n1 n2 : ▷ ▷^n1 ▷^n2 P -∗ ▷^n1 ▷^n2 ▷ P.
Proof. iIntros "H". iNext. iNext. by iNext. Qed.
(* tests/proofmode.v *)
Lemma test_iNext_plus_2 P n m : ▷^n ▷^m P -∗ ▷^(n+m) P.
Proof. iIntros "H". iNext. done. Qed.
(* tests/proofmode.v *)
Lemma test_iNext_plus_3 P Q n m k :
  ▷^m ▷^(2 + S n + k) P -∗ ▷^m ▷ ▷^(2 + S n) Q -∗ ▷^k ▷ ▷^(S (S n + S m)) (P ∗ Q).
Proof. iIntros "H1 H2". iNext. iNext. iNext. iFrame. Show. iModIntro. done. Qed.
(* tests/proofmode.v *)
Lemma test_iNext_unfold P Q n m (R := (▷^n P)%I) :
  R ⊢ ▷^m True.
Proof.
  iIntros "HR". iNext.
  match goal with |-  context [ R ] => idtac | |- _ => fail end.
  done.
Qed.
(* tests/proofmode.v *)
Lemma test_iNext_fail P Q a b c d e f g h i j:
  ▷^(a + b) ▷^(c + d + e) P -∗ ▷^(f + g + h + i + j) True.
Proof. iIntros "H". iNext. done. Qed.
(* tests/proofmode.v *)
Lemma test_specialize_affine_pure (φ : Prop) P :
  φ → (<affine> ⌜φ⌝ -∗ P) ⊢ P.
Proof.
  iIntros (Hφ) "H". by iSpecialize ("H" with "[% //]").
Qed.
(* tests/proofmode.v *)
Lemma test_assert_affine_pure (φ : Prop) P :
  φ → P ⊢ P ∗ <affine> ⌜φ⌝.
Proof. iIntros (Hφ). iAssert (<affine> ⌜φ⌝)%I with "[%]" as "$"; auto. Qed.
(* tests/proofmode.v *)
Lemma test_assert_pure (φ : Prop) P :
  φ → P ⊢ P ∗ ⌜φ⌝.
Proof. iIntros (Hφ). iAssert ⌜φ⌝%I with "[%]" as "$"; auto with iFrame. Qed.
(* tests/proofmode.v *)
Lemma test_specialize_very_nested (φ : Prop) P P2 Q R1 R2 :
  φ →
  P -∗ P2 -∗
  (<affine> ⌜ φ ⌝ -∗ P2 -∗ Q) -∗
  (P -∗ Q -∗ R1) -∗
  (R1 -∗ True -∗ R2) -∗
  R2.
Proof.
  iIntros (?) "HP HP2 HQ H1 H2".
  by iApply ("H2" with "(H1 HP (HQ [% //] [-])) [//]").
Qed.
(* tests/proofmode.v *)
Lemma test_specialize_very_very_nested P1 P2 P3 P4 P5 :
  □ P1 -∗
  □ (P1 -∗ P2) -∗
  (P2 -∗ P2 -∗ P3) -∗
  (P3 -∗ P4) -∗
  (P4 -∗ P5) -∗
  P5.
Proof.
  iIntros "#H #H1 H2 H3 H4".
  by iSpecialize ("H4" with "(H3 (H2 (H1 H) (H1 H)))").
Qed.
(* tests/proofmode.v *)
Lemma test_specialize_nested_intuitionistic (φ : Prop) P P2 Q R1 R2 :
  φ →
  □ P -∗ □ (P -∗ Q) -∗ (Q -∗ Q -∗ R2) -∗ R2.
Proof.
  iIntros (?) "#HP #HQ HR".
  iSpecialize ("HR" with "(HQ HP) (HQ HP)").
  Show.
  done.
Qed.
(* tests/proofmode.v *)
Lemma test_specialize_intuitionistic P Q :
  □ P -∗ □ (P -∗ Q) -∗ □ Q.
Proof. iIntros "#HP #HQ". iSpecialize ("HQ" with "HP"). done. Qed.
(* tests/proofmode.v *)
Lemma test_iEval x y : ⌜ (y + x)%nat = 1 ⌝ ⊢@{PROP} ⌜ S (x + y) = 2%nat ⌝.
Proof.
  iIntros (H).
  iEval (rewrite (Nat.add_comm x y) // H).
  done.
Qed.
(* tests/proofmode.v *)
Lemma test_iEval_precedence : True ⊢ True : PROP.
Proof.
  iIntros.
  (* Ensure that in [iEval (a); b], b is not parsed as part of the argument of [iEval]. *)
  iEval (rewrite /=); iPureIntro; exact I.
Qed.
(* tests/proofmode.v *)
Lemma test_iSimpl_in x y : ⌜ (3 + x)%nat = y ⌝ ⊢@{PROP} ⌜ S (S (S x)) = y ⌝.
Proof. iIntros "H". iSimpl in "H". Show. done. Qed.
(* tests/proofmode.v *)
Lemma test_iSimpl_in_2 x y z :
  ⌜ (3 + x)%nat = y ⌝ ⊢@{PROP} ⌜ (1 + y)%nat = z ⌝ -∗
  ⌜ S (S (S x)) = y ⌝.
Proof. iIntros "H1 H2". iSimpl in "H1 H2". Show. done. Qed.
(* tests/proofmode.v *)
Lemma test_iSimpl_in3 x y z :
  ⌜ (3 + x)%nat = y ⌝ ⊢@{PROP} ⌜ (1 + y)%nat = z ⌝ -∗
  ⌜ S (S (S x)) = y ⌝.
Proof. iIntros "#H1 H2". iSimpl in "#". Show. done. Qed.
(* tests/proofmode.v *)
Lemma test_iSimpl_in4 x y : ⌜ (3 + x)%nat = y ⌝ ⊢@{PROP} ⌜ S (S (S x)) = y ⌝.
Proof. iIntros "H". Fail iSimpl in "%". by iSimpl in "H". Qed.
(* tests/proofmode.v *)
Lemma test_iUnfold : def2 = 10 → ⊢@{PROP} ⌜ def2 = 10 ⌝.
Proof. intros Hdef. iUnfold def2, def1. Show. done. Qed.
(* tests/proofmode.v *)
Lemma test_iUnfold_in : def2 = 10 → ⌜ def2 = 10 ⌝ ⊢@{PROP} ⌜ def2 = 10 ⌝.
Proof. iIntros "%Hdef Hdef". iUnfold def2, def1 in "Hdef". Show. done. Qed.
(* tests/proofmode.v *)
Lemma test_iRename P : □P -∗ P.
Proof. iIntros "#H". iRename "H" into "X". Show. iExact "X". Qed.
(* tests/proofmode.v *)
(* [iTypeOf] is an internal tactic for the proofmode *)
Lemma test_iTypeOf Q R φ : □ Q ∗ R ∗ ⌜φ⌝ -∗ True.
Proof.
  iIntros "(#HQ & H)".
  lazymatch iTypeOf "HQ" with
  | Some (true, Q) => idtac
  | ?x => fail "incorrect iTypeOf HQ" x
  end.
  lazymatch iTypeOf "H" with
  | Some (false, (R ∗ ⌜φ⌝)%I) => idtac
  | ?x => fail "incorrect iTypeOf H" x
  end.
  lazymatch iTypeOf "missing" with
  | None => idtac
  | ?x => fail "incorrect iTypeOf missing" x
  end.
Abort.
(* tests/proofmode.v *)
Lemma test_iPureIntro_absorbing (φ : Prop) :
  φ → ⊢@{PROP} <absorb> ⌜φ⌝.
Proof. intros ?. iPureIntro. done. Qed.
(* tests/proofmode.v *)
Lemma test_iFrame_later_1 P Q : P ∗ ▷ Q -∗ ▷ (P ∗ ▷ Q).
Proof. iIntros "H". iFrame "H". Show. auto. Qed.
(* tests/proofmode.v *)
Lemma test_iFrame_later_2 P Q : ▷ P ∗ ▷ Q -∗ ▷ (▷ P ∗ ▷ Q).
Proof. iIntros "H". iFrame "H". Show. auto. Qed.
(* tests/proofmode.v *)
Lemma test_with_ident P Q R : P -∗ Q -∗ (P -∗ Q -∗ R) -∗ R.
Proof.
  iIntros "? HQ H".
  iMatchHyp (fun H _ =>
    iApply ("H" with [spec_patterns.SIdent H []; spec_patterns.SIdent "HQ" []])).
Qed.
(* tests/proofmode.v *)
Lemma iFrame_with_evar_r P Q :
  ∃ R, (P -∗ Q -∗ P ∗ R) ∧ R = Q.
Proof.
  eexists. split.
  - iIntros "HP HQ". iFrame. iApply "HQ".
  - done.
Qed.
(* tests/proofmode.v *)
Lemma iFrame_with_evar_l P Q :
  ∃ R, (P -∗ Q -∗ R ∗ P) ∧ R = Q.
Proof.
  eexists. split.
  - iIntros "HP HQ". Fail iFrame "HQ".
    iSplitR "HP"; iAssumption.
  - done.
Qed.
(* tests/proofmode.v *)
Lemma iFrame_with_evar_persistent P Q :
  ∃ R, (P -∗ □ Q -∗ P ∗ R ∗ Q) ∧ R = emp%I.
Proof.
  eexists. split.
  - iIntros "HP #HQ". iFrame "HQ HP". iEmpIntro.
  - done.
Qed.
(* tests/proofmode.v *)
Lemma test_iAccu P Q R S :
  ∃ PP, (□P -∗ Q -∗ R -∗ S -∗ PP) ∧ PP = (Q ∗ R ∗ S)%I.
Proof.
  eexists. split.
  - iIntros "#? ? ? ?". iAccu.
  - done.
Qed.
(* tests/proofmode.v *)
Lemma test_iAssumption_evar P : ∃ R, (R ⊢ P) ∧ R = P.
Proof.
  eexists. split.
  - iIntros "H". iAssumption.
  - (* Verify that [iAssumption] instantiates the evar for the existential [R]
    to become [P], and in particular, that it does not make it [False]. *)
    reflexivity.
Qed.
(* tests/proofmode.v *)
(* Prior to 0b84351c this used to loop, now [iAssumption] fails. *)
Lemma test_iAssumption_False_no_loop : ∃ R, R ⊢ ∀ P, P.
Proof.
  eexists. iIntros "H" (P).
  (* Make sure that [iAssumption] does not perform False elimination on
  hypotheses that are evars. *)
  Fail iAssumption.
  (* And neither does [done]. *)
  Fail done.
  (* But we can of course achieve that using an explicit proof. *)
  iExFalso. iExact "H".
Qed.
(* tests/proofmode.v *)
Lemma test_apply_affine_impl `{!Sbi PROP} (P : PROP) :
  P -∗ (∀ Q : PROP, ■ (Q -∗ <pers> Q) → ■ (P -∗ Q) → Q).
Proof. iIntros "HP" (Q) "_ #HPQ". by iApply "HPQ". Qed.
(* tests/proofmode.v *)
Lemma test_apply_affine_wand `{!Sbi PROP} (P : PROP) :
  P -∗ (∀ Q : PROP, <affine> ■ (Q -∗ <pers> Q) -∗ <affine> ■ (P -∗ Q) -∗ Q).
Proof. iIntros "HP" (Q) "_ #HPQ". by iApply "HPQ". Qed.
(* tests/proofmode.v *)
Lemma test_and_sep (P Q R : PROP) : P ∧ (Q ∗ □ R) ⊢ (P ∧ Q) ∗ □ R.
Proof.
  iIntros "H". repeat iSplit.
  - iDestruct "H" as "[$ _]".
  - iDestruct "H" as "[_ [$ _]]".
  - iDestruct "H" as "[_ [_ #$]]".
Qed.
(* tests/proofmode.v *)
Lemma test_and_sep_2 (P Q R : PROP) `{!Persistent R, !Affine R} :
  P ∧ (Q ∗ R) ⊢ (P ∧ Q) ∗ R.
Proof.
  iIntros "H". repeat iSplit.
  - iDestruct "H" as "[$ _]".
  - iDestruct "H" as "[_ [$ _]]".
  - iDestruct "H" as "[_ [_ #$]]".
Qed.
(* tests/proofmode.v *)
(* [from_and_pure_iff] and [from_sep_pure_if] instances work correctly. *)
Lemma test_iSplit_pure_iff (φ : Prop) :
  ⊢ ⌜φ ↔ φ⌝ : PROP.
Proof.
  by iSplit.
Restart. Proof.
  by iSplitL.
Restart. Proof.
  by iSplitR.
Qed.
(* tests/proofmode.v *)
Lemma test_iSplit_wand_iff (P : PROP) :
  ⊢ P ∗-∗ P.
Proof.
  iSplit; by auto.
Restart.
  (* fails without [BiAffine] instance *)
  Fail iSplitL. Fail iSplitR.
Abort.
(* tests/proofmode.v *)
Lemma test_iSplit_bi_wand_iff_affine `{!BiAffine PROP} (P : PROP) :
  ⊢ P ∗-∗ P.
Proof.
  iSplit; by auto.
Restart.
  iSplitL; by auto.
Restart. Proof.
  iSplitR; by auto.
Qed.
(* tests/proofmode.v *)
Lemma test_iSplit_iff (P : PROP) :
  ⊢ P ↔ P.
Proof.
  iSplit; by auto.
Restart.
  (* fails without [BiAffine] instance *)
  Fail iSplitL. Fail iSplitR.
Abort.
(* tests/proofmode.v *)
Lemma test_iSplit_bi_iff_affine `{!BiAffine PROP} (P : PROP) :
  ⊢ P ↔ P.
Proof.
  iSplit; by auto.
Restart.
  iSplitL; by auto.
Restart. Proof.
  iSplitR; by auto.
Qed.
(* tests/proofmode.v *)
Lemma test_and_sep_affine_bi `{!BiAffine PROP} P Q : □ P ∧ Q ⊢ □ P ∗ Q.
Proof.
  iIntros "[??]". iSplit; last done. Show. done.
Qed.
(* tests/proofmode.v *)
Lemma test_big_sepL_simpl x (l : list nat) P :
   P -∗
  ([∗ list] k↦y ∈ l, <affine> ⌜ y = y ⌝) -∗
  ([∗ list] y ∈ x :: l, <affine> ⌜ y = y ⌝) -∗
  P.
Proof. iIntros "HP ??". Show. simpl. Show. done. Qed.
(* tests/proofmode.v *)
Lemma test_big_sepL2_simpl x1 x2 (l1 l2 : list nat) P :
  P -∗
  ([∗ list] k↦y1;y2 ∈ []; l2, <affine> ⌜ y1 = y2 ⌝) -∗
  ([∗ list] y1;y2 ∈ x1 :: l1; (x2 :: l2) ++ l2, <affine> ⌜ y1 = y2 ⌝) -∗
  P ∨ ([∗ list] y1;y2 ∈ x1 :: l1; x2 :: l2, True).
Proof. iIntros "HP ??". Show. simpl. Show. by iLeft. Qed.
(* tests/proofmode.v *)
Lemma test_big_sepL2_iDestruct (Φ : nat → nat → PROP) x1 x2 (l1 l2 : list nat) :
  ([∗ list] y1;y2 ∈ x1 :: l1; x2 :: l2, Φ y1 y2) -∗
  <absorb> Φ x1 x2.
Proof. iIntros "[??]". Show. iFrame. Qed.
(* tests/proofmode.v *)
Lemma test_big_sepL2_iFrame (Φ : nat → nat → PROP) (l1 l2 : list nat) P :
  Φ 0 10 -∗ ([∗ list] y1;y2 ∈ l1;l2, Φ y1 y2) -∗
  ([∗ list] y1;y2 ∈ (0 :: l1);(10 :: l2), Φ y1 y2).
Proof. iIntros "$ ?". iFrame. Qed.
(* tests/proofmode.v *)
Lemma test_lemma_1 (b : bool) :
  emp ⊢@{PROP} □?b True.
Proof. destruct b; simpl; eauto. Qed.
(* tests/proofmode.v *)
Lemma test_reducing_after_iDestruct : emp ⊢@{PROP} True.
Proof.
  iIntros "H". iDestruct (test_lemma_1 true with "H") as "H". Show. done.
Qed.
(* tests/proofmode.v *)
Lemma test_lemma_2 (b : bool) :
  □?b emp ⊢@{PROP} emp.
Proof. destruct b; simpl; eauto. Qed.
(* tests/proofmode.v *)
Lemma test_reducing_after_iApply : emp ⊢@{PROP} emp.
Proof.
  iIntros "#H". iApply (test_lemma_2 true). Show. auto.
Qed.
(* tests/proofmode.v *)
Lemma test_lemma_3 (b : bool) :
  □?b emp ⊢@{PROP} ⌜b = b⌝.
Proof. destruct b; simpl; eauto. Qed.
(* tests/proofmode.v *)
Lemma test_reducing_after_iApply_late_evar : emp ⊢@{PROP} ⌜true = true⌝.
Proof.
  iIntros "#H". iApply (test_lemma_3). Show. auto.
Qed.
(* tests/proofmode.v *)
Lemma test_wandM mP Q R :
    (mP -∗? Q) -∗ (Q -∗ R) -∗ (mP -∗? R).
Proof.
    iIntros "HPQ HQR HP". Show.
    iApply "HQR". iApply "HPQ". Show.
    done.
  Qed.
(* tests/proofmode.v *)
Definition modal_if_def b (P : PROP)
:=
  (□?b P)%I.
(* tests/proofmode.v *)
Lemma modal_if_lemma1 b P :
  False -∗ □?b P.
Proof. iIntros "?". by iExFalso. Qed.
(* tests/proofmode.v *)
Lemma test_iApply_prettification1 (P : PROP) :
  False -∗ modal_if_def true P.
Proof.
  (* Make sure the goal is not prettified before [iApply] unifies. *)
  iIntros "?". rewrite /modal_if_def. iApply modal_if_lemma1. iAssumption.
Qed.
(* tests/proofmode.v *)
Lemma modal_if_lemma2 P :
  False -∗ □?false P.
Proof. iIntros "?". by iExFalso. Qed.
(* tests/proofmode.v *)
Lemma test_iApply_prettification2 (P  : PROP) :
  False -∗ ∃ b, □?b P.
Proof.
  (* Make sure the conclusion of the lemma is not prettified too early. *)
  iIntros "?". iExists _. iApply modal_if_lemma2. done.
Qed.
(* tests/proofmode.v *)
Lemma test_iApply_prettification3 (Ψ Φ : nat → PROP) :
  (∀ f y, TCEq f (λ x, x + 10) → Ψ (f 1) -∗ Φ y) →
  Ψ 11 -∗ Φ 10.
Proof.
  iIntros (HP) "H".
  iApply HP. (* should be [Ψ (1 + 10)], without a beta redex *)
  Show.
  iApply "H".
Qed.
(* tests/proofmode.v *)
Lemma test_iDestruct_clear P Q R :
  P -∗ (Q ∗ R) -∗ True.
Proof.
  iIntros "HP HQR". iDestruct "HQR" as "{HP} [HQ HR]". done.
Qed.
(* tests/proofmode.v *)
Lemma test_iSpecialize_bupd `{!BiBUpd PROP} A (a : A) (P : A -> PROP) :
  (|==> ∀ x, P x) ⊢ |==> P a.
Proof.
  iIntros "H". iSpecialize ("H" $! a). done.
Qed.
(* tests/proofmode.v *)
Lemma test_iSpecialize_fupd `{!BiFUpd PROP} A (a : A) (P : A -> PROP) E1 E2 :
  (|={E1, E2}=> ∀ x, P x) ⊢ |={E1, E2}=> P a.
Proof.
  iIntros "H". iSpecialize ("H" $! a). done.
Qed.
(* tests/proofmode.v *)
Lemma test_iDestruct_and_bupd `{!BiBUpd PROP} (P Q : PROP) :
  (|==> P ∧ Q) ⊢ |==> P.
Proof.
  iIntros "[P _]". done.
Qed.
(* tests/proofmode.v *)
Lemma test_iDestruct_and_fupd `{!BiFUpd PROP} (P Q : PROP) E1 E2 :
  (|={E1, E2}=> P ∧ Q) ⊢ |={E1, E2}=> P.
Proof.
  iIntros "[P _]". done.
Qed.
(* tests/proofmode.v *)
Lemma test_iModIntro_make_laterable `{!BiAffine PROP} (P Q : PROP) :
  Laterable Q →
  P -∗ Q -∗ make_laterable (▷ P ∗ Q).
Proof.
  iIntros (?) "HP HQ". iModIntro. Show. by iFrame.
Qed.
(* tests/proofmode.v *)
Lemma test_iExfalso_start_proof P : 0 = 1 → ⊢ P.
Proof.
  intros. iExFalso. done.
Qed.
(* tests/proofmode.v *)
Lemma test_iRevert_pure (φ : Prop) P :
  φ → (<affine> ⌜ φ ⌝ -∗ P) -∗ P.
Proof.
  (* Check that iRevert creates a wand instead of an implication *)
  iIntros (Hφ) "H". iRevert (Hφ). Show. done.
Qed.
(* tests/proofmode.v *)
Lemma test_iRevert_order_and_names P1 P2 : P1 -∗ P2 -∗ P1 ∗ P2.
Proof.
  iIntros "H1 H2". iRevert (P1 P2) "H1 H2".
  (* Check that the reverts are performed in the right order (i.e., reverse),
  and that the names [P1] and [P2] are used in the goal. *)
  Show.
  auto with iFrame.
Qed.
(* tests/proofmode.v *)
Lemma test_iRevert_pure_affine `{!BiAffine PROP} (φ : Prop) P :
  φ → (⌜ φ ⌝ -∗ P) -∗ P.
Proof.
  (* If the BI is affine, no affine modality should be added *)
  iIntros (Hφ) "H". iRevert (Hφ). Show. done.
Qed.
(* tests/proofmode.v *)
Lemma test_iInduction_revert_pure (n : nat) (Hn : 0 < n) (P : nat → PROP) :
  ⊢ P n.
Proof.
  (* Check that we consistently get [<affine> _ -∗], not [→] *)
  iInduction n as [|n IH] forall (Hn); first lia.
  Show.
Restart.
Proof.
  iInduction n as [|n IH]; first lia.
  Show.
Abort.
(* tests/proofmode.v *)
Lemma test_iInduction_revert_pure_affine `{!BiAffine PROP}
  (n : nat) (Hn : 0 < n) (P : nat → PROP) : ⊢ P n.
Proof.
  (* Check that we consistently get [-∗], not [→]; and no [<affine>] *)
  iInduction n as [|n IH] forall (Hn); first lia.
  Show.
Restart.
Proof.
  iInduction n as [|n IH]; first lia.
  Show.
Abort.
(* tests/proofmode.v *)
Lemma test_iFrame_not_add_emp_for_intuitionistically `{!BiAffine PROP} (P : PROP) :
  □ P -∗ ∃ _ : nat, □ P.
Proof. iIntros "#H". iFrame "H". Show. by iExists 0. Qed.
(* tests/proofmode.v *)
Lemma test_auto_iff P : ⊢ P ↔ P.
Proof. auto. Qed.
(* tests/proofmode.v *)
Lemma test_auto_wand_iff P : ⊢ P ∗-∗ P.
Proof. auto. Qed.
(* tests/proofmode.v *)
Lemma test_iIntros_auto_name_used_later (Φ: nat → PROP) :
  ⊢ ∀ x y, Φ (x+y).
Proof.
  (* This test documents a difference between [intros ...] and [iIntros (...)]:
  the latter will pick [x] as the name for the [?] here (matching the name in the goal)
  and then fail later when another [x] is attempted to be introduced. [intros] will
  somehow realize that [x] is coming later, and pick a different name for the [?]. *)
  Fail iIntros (? x).
Abort.
(* tests/proofmode.v *)
Lemma test_iExistDestruct_generic_error_1 P :
  P -∗ False.
Proof. Fail iIntros "[%x ?]". Abort.
(* tests/proofmode.v *)
Lemma test_iExistDestruct_generic_error_2 P :
  (P ∗ ∃ x : nat, True) -∗ False.
Proof. Fail iIntros "[%x ?]". Abort.
(* tests/proofmode.v *)
Lemma test_iExistDestruct_later_error_1 {A} (Φ : A → PROP) :
  (▷ ∃ x, Φ x) -∗ False.
Proof. Fail iIntros "[%x ?]". Abort.
(* tests/proofmode.v *)
Lemma test_iExistDestruct_later_error_2 {A B} (Φ : A → B → PROP) :
  (▷ ∃ (x : A) (y : B), Φ x y) -∗ False.
Proof. Fail iIntros "[%x ?]". (* Should report [A], not [B] *) Abort.
(* tests/proofmode.v *)
Lemma test_iExistDestruct_later_error_3 {A} (Φ : A → PROP) :
  (▷ □ ∃ x, Φ x) -∗ False.
Proof. Fail iIntros "[%x ?]". Abort.
(* tests/proofmode.v *)
Lemma test_iExistDestruct_later_error_4 {A} (Φ : A → PROP) :
  (□ ▷ ∃ x, Φ x) -∗ False.
Proof. Fail iIntros "[%x ?]". Abort.
(* tests/proofmode.v *)
(* Test notations for (bi)entailment and internal equality. These tests are
especially extensive because of past problems such as
https://gitlab.mpi-sws.org/iris/iris/-/issues/302. *)
Lemma test_bi_emp_valid : ⊢@{PROP} True.
Proof. naive_solver. Qed.
(* tests/proofmode.v *)
Lemma test_bi_emp_valid_parens : (⊢@{PROP} True) ∧ ((⊢@{PROP} True)).
Proof. naive_solver. Qed.
(* tests/proofmode.v *)
Lemma test_bi_emp_valid_parens_space_open : ( ⊢@{PROP} True).
Proof. naive_solver. Qed.