Merge branch 'robbert/issue520' into 'master'

Better handling of `let` bindings in proof mode

Closes #520

See merge request iris/iris!921

CHANGELOG.md

@@ -87,6 +87,13 @@ Coq 8.13 is no longer supported.
   `CombineSepGives` typeclass. The 'gives' clause is still experimental;
   in future versions of Iris it will combine `own` connectives based on the
   validity rules for cameras.
+- Make sure that `iStartProof` fails with a proper error message on goals with
+  `let`. These `let`s should either be `simpl`ed or introduced into the Coq
+  context using `intros x`, `iIntros (x)`, or `iIntros "%x"`.
+  This can break some proofs that did `iIntros "?"` on a goal of the shape
+  `let ... in P ⊢ Q`.
+- Make `iApply`/`iPoseProof`/`iDestruct` more reliable for lemmas whose
+  statement involves `let`.
 
 **Changes in `base_logic`:**
 

iris/proofmode/ltac_tactics.v

@@ -66,6 +66,8 @@ Tactic Notation "iSelect" open_constr(pat) tactic1(tac) :=
 (** * Start a proof *)
 Tactic Notation "iStartProof" :=
   lazymatch goal with
+  | |- (let _ := _ in _) => fail "iStartProof: goal is a `let`, use `simpl`,"
+                                 "`intros x`, `iIntros (x)`, or `iIntros ""%x"""
   | |- envs_entails _ _ => idtac
   | |- ?φ => notypeclasses refine (as_emp_valid_2 φ _ _);
                [tc_solve || fail "iStartProof: not a BI assertion"
@@ -825,6 +827,11 @@ time.
 *)
 Ltac iIntoEmpValid_go :=
   lazymatch goal with
+  | |- IntoEmpValid (let _ := _ in _) _ =>
+    (* Normalize [let] so we don't need to rely on type class search to do so.
+    Letting type class search do so is unreliable, see Iris issue #520, and test
+    [test_apply_wand_below_let]. *)
+    lazy zeta; iIntoEmpValid_go
   | |- IntoEmpValid (?φ → ?ψ) _ =>
     (* Case [φ → ψ] *)
     (* note: the ltac pattern [_ → _] would not work as it would also match

tests/proofmode.ref

@@ -954,6 +954,16 @@ 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"
+     : string
+The command has indeed failed with message:
+Tactic failure: iStartProof: goal is a `let`, use `simpl`,
+`intros x`, `iIntros (x)`, or `iIntros "%x".
+"test_iIntros_let_wand_fail"
+     : string
+The command has indeed failed with message:
+Tactic failure: iStartProof: goal is a `let`, use `simpl`,
+`intros x`, `iIntros (x)`, or `iIntros "%x".
 "test_pure_name"
      : string
 1 goal

tests/proofmode.v

@@ -885,11 +885,46 @@ Proof.
   iIntros (help) "HP".
   iPoseProof (help with "[$HP]") as "?". done.
 Qed.
+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.
+
+Lemma test_iPoseProof_let_in_string 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_iIntros_let 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.
+Proof. iIntros (Q R) "$ _ $". Qed.
+
+Lemma lemma_for_test_apply_below_let (Φ : nat → PROP) :
+  let Q := Φ 5 in
+  Q ⊢ Q.
+Proof. iIntros (?) "?". done. Qed.
+Lemma test_apply_below_let (Φ : nat → PROP) :
+  Φ 5 -∗ Φ 5.
+Proof. iIntros "?". iApply lemma_for_test_apply_below_let. done. Qed.
+
+Lemma lemma_for_test_apply_wand_below_let (Φ : nat → PROP) :
+  let Q := Φ 5 in
+  Q -∗ Q.
+Proof. iIntros (?) "?". done. Qed.
+Lemma test_apply_wand_below_let (Φ : nat → PROP) :
+  Φ 5 -∗ Φ 5.
+Proof. iIntros "?". iApply lemma_for_test_apply_wand_below_let. done. Qed.
+
 Lemma test_iNext_iRewrite `{!BiInternalEq PROP} P Q :
   <affine> ▷ (Q ≡ P) -∗ <affine> ▷ Q -∗ <affine> ▷ P.
 Proof.
@@ -1756,6 +1791,22 @@ Proof.
   Fail iInduction n as [|n] "IH" forall m.
 Abort.
 
+Check "test_iIntros_let_fail".
+Lemma test_iIntros_let_fail P :
+  let Q := (P ∗ P)%I in
+  Q ⊢ Q.
+Proof.
+  Fail iIntros "Q".
+Abort.
+
+Check "test_iIntros_let_wand_fail".
+Lemma test_iIntros_let_wand_fail P :
+  let Q := (P ∗ P)%I in
+  Q ⊢ Q.
+Proof.
+  Fail iIntros "Q".
+Abort.
+
 End error_tests.
 
 Section pure_name_tests.