Merge remote-tracking branch 'origin/master' into gen_proofmode

theories/heap_lang/proofmode.v

@@ -16,9 +16,15 @@ Proof. by intros ->. Qed.
 
 Tactic Notation "wp_expr_eval" tactic(t) :=
   iStartProof;
-  try (first [eapply tac_wp_expr_eval|eapply tac_twp_expr_eval];
-       [let x := fresh in intros x; t; unfold x; reflexivity
-       |]).
+  lazymatch goal with
+  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
+    eapply tac_wp_expr_eval;
+      [let x := fresh in intros x; t; unfold x; reflexivity|]
+  | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
+    eapply tac_twp_expr_eval;
+      [let x := fresh in intros x; t; unfold x; reflexivity|]
+  | _ => fail "wp_expr_eval: not a 'wp'"
+  end.
 
 Ltac wp_expr_simpl := wp_expr_eval simpl.
 Ltac wp_expr_simpl_subst := wp_expr_eval simpl_subst.
@@ -295,13 +301,13 @@ Tactic Notation "wp_apply" open_constr(lem) :=
     lazymatch goal with
     | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
       reshape_expr e ltac:(fun K e' =>
-        wp_bind_core K; iApplyHyp H; try iNext; wp_expr_simpl) ||
+        wp_bind_core K; iApplyHyp H; try iNext; try wp_expr_simpl) ||
       lazymatch iTypeOf H with
       | Some (_,?P) => fail "wp_apply: cannot apply" P
       end
     | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
       reshape_expr e ltac:(fun K e' =>
-        twp_bind_core K; iApplyHyp H; wp_expr_simpl) ||
+        twp_bind_core K; iApplyHyp H; try wp_expr_simpl) ||
       lazymatch iTypeOf H with
       | Some (_,?P) => fail "wp_apply: cannot apply" P
       end

theories/tests/heap_lang.v

@@ -104,6 +104,11 @@ Section LiftingTests.
   Lemma Pred_user E :
     WP let: "x" := Pred #42 in Pred "x" @ E [{ v, ⌜v = #40⌝ }]%I.
   Proof. iIntros "". wp_apply Pred_spec. wp_let. by wp_apply Pred_spec. Qed.
+
+  Lemma wp_apply_evar e P :
+    P -∗ (∀ Q Φ, Q -∗ WP e {{ Φ }}) -∗ WP e {{ _, True }}.
+  Proof. iIntros "HP HW". wp_apply "HW". iExact "HP". Qed.
+
 End LiftingTests.
 
 Lemma heap_e_adequate σ : adequate NotStuck heap_e σ (= #2).

theories/tests/proofmode.v

@@ -386,6 +386,9 @@ Proof.
   done.
 Qed.
 
+Lemma test_iIntros_pure_neg : (⌜ ¬False ⌝ : PROP)%I.
+Proof. by iIntros (?). Qed.
+
 Lemma test_iFrame_later_1 P Q : P ∗ ▷ Q -∗ ▷ (P ∗ ▷ Q).
 Proof. iIntros "H". iFrame "H". auto. Qed.