From 670f23300361b7067b5f30fdfdaed3fad199d429 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 5 May 2023 08:54:04 +0200
Subject: [PATCH] Improve tests from !921, based on suggestions by Paolo.

---
 tests/proofmode.ref |  2 +-
 tests/proofmode.v   | 24 ++++++++++++------------
 2 files changed, 13 insertions(+), 13 deletions(-)

diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index 7646632b3..cee756d7f 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -954,7 +954,7 @@ The command has indeed failed with message:
 Tactic failure: sel_pat.parse: the term m
 is expected to be a selection pattern (usually a string),
 but has unexpected type nat.
-"test_iIntros_let_fail"
+"test_iIntros_let_entails_fail"
      : string
 The command has indeed failed with message:
 Tactic failure: iStartProof: goal is a `let`, use `simpl`,
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 91f4fa3fc..b235b26eb 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -878,7 +878,7 @@ Proof.
   iIntros "?". done.
 Qed.
 
-Lemma test_iPoseProof_let P Q :
+Lemma test_iPoseProof_let_entails P Q :
   (let R := True%I in R ∗ P ⊢ Q) →
   P ⊢ Q.
 Proof.
@@ -886,14 +886,14 @@ Proof.
   iPoseProof (help with "[$HP]") as "?". done.
 Qed.
 Lemma test_iPoseProof_let_wand P Q :
-  (let R := True%I in R ∗ P ⊢ Q) →
+  (let R := True%I in R ∗ P -∗ Q) →
   P -∗ Q.
 Proof.
   iIntros (help) "HP".
   iPoseProof (help with "[$HP]") as "?". done.
 Qed.
 
-Lemma test_iPoseProof_let_in_string P Q :
+Lemma test_iPoseProof_let_entails_pm_intro_pat P Q :
   (let R := True%I in R ∗ P ⊢ Q) →
   P ⊢ Q.
 Proof.
@@ -901,21 +901,21 @@ Proof.
   iPoseProof (help with "[$HP]") as "?". done.
 Qed.
 
-Lemma test_iIntros_let P :
-  ∀ Q, let R := emp%I in P -∗ R -∗ Q -∗ P ∗ Q.
+Lemma test_iIntros_let_entails P :
+  ∀ Q, let R := emp%I in P ⊢ R -∗ Q -∗ P ∗ Q.
 Proof. iIntros (Q R) "$ _ $". Qed.
 
 Lemma test_iIntros_let_wand P :
-  ∀ Q, let R := emp%I in P ⊢ R -∗ Q -∗ P ∗ Q.
+  ∀ Q, let R := emp%I in P -∗ R -∗ Q -∗ P ∗ Q.
 Proof. iIntros (Q R) "$ _ $". Qed.
 
-Lemma lemma_for_test_apply_below_let (Φ : nat → PROP) :
+Lemma lemma_for_test_apply_entails_below_let (Φ : nat → PROP) :
   let Q := Φ 5 in
   Q ⊢ Q.
 Proof. iIntros (?) "?". done. Qed.
-Lemma test_apply_below_let (Φ : nat → PROP) :
+Lemma test_apply_entails_below_let (Φ : nat → PROP) :
   Φ 5 -∗ Φ 5.
-Proof. iIntros "?". iApply lemma_for_test_apply_below_let. done. Qed.
+Proof. iIntros "?". iApply lemma_for_test_apply_entails_below_let. done. Qed.
 
 Lemma lemma_for_test_apply_wand_below_let (Φ : nat → PROP) :
   let Q := Φ 5 in
@@ -1791,8 +1791,8 @@ Proof.
   Fail iInduction n as [|n] "IH" forall m.
 Abort.
 
-Check "test_iIntros_let_fail".
-Lemma test_iIntros_let_fail P :
+Check "test_iIntros_let_entails_fail".
+Lemma test_iIntros_let_entails_fail P :
   let Q := (P ∗ P)%I in
   Q ⊢ Q.
 Proof.
@@ -1802,7 +1802,7 @@ Abort.
 Check "test_iIntros_let_wand_fail".
 Lemma test_iIntros_let_wand_fail P :
   let Q := (P ∗ P)%I in
-  Q ⊢ Q.
+  Q -∗ Q.
 Proof.
   Fail iIntros "Q".
 Abort.
-- 
GitLab