From 211c2363dec227654c71e72fad02e7a97484afcc Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 11 Feb 2017 21:28:41 +0100
Subject: [PATCH] Improve `iIntros "_"`.
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

In the following ways:
- When having `P → Q` it will now also work when the spatial context
  is non-empty.
- When having `∀ x : A, Q` it will now do an `iIntros (_)`.
---
 theories/proofmode/coq_tactics.v | 4 ++++
 theories/proofmode/tactics.v     | 9 +++++++++
 2 files changed, 13 insertions(+)

diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index 7137e4ec0..20b21e3a5 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -483,6 +483,8 @@ Lemma tac_impl_intro_pure Δ P φ Q : IntoPure P φ → (φ → Δ ⊢ Q) → Δ
 Proof.
   intros. by apply impl_intro_l; rewrite (into_pure P); apply pure_elim_l.
 Qed.
+Lemma tac_impl_intro_drop Δ P Q : (Δ ⊢ Q) → Δ ⊢ P → Q.
+Proof. intros. apply impl_intro_l. by rewrite and_elim_r. Qed.
 
 Lemma tac_wand_intro Δ Δ' i P Q :
   envs_app false (Esnoc Enil i P) Δ = Some Δ' → (Δ' ⊢ Q) → Δ ⊢ P -∗ Q.
@@ -501,6 +503,8 @@ Lemma tac_wand_intro_pure Δ P φ Q : IntoPure P φ → (φ → Δ ⊢ Q) → Δ
 Proof.
   intros. by apply wand_intro_l; rewrite (into_pure P); apply pure_elim_sep_l.
 Qed.
+Lemma tac_wand_intro_drop Δ P Q : (Δ ⊢ Q) → Δ ⊢ P -∗ Q.
+Proof. intros. apply wand_intro_l. by rewrite sep_elim_r. Qed.
 
 (* This is pretty much [tac_specialize_assert] with [js:=[j]] and [tac_exact],
 but it is doing some work to keep the order of hypotheses preserved. *)
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index e622cb100..cd03600c6 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -773,6 +773,14 @@ Local Tactic Notation "iIntro" "#" constr(H) :=
       |env_cbv; reflexivity || fail 1 "iIntro:" H "not fresh"|]
   | fail 1 "iIntro: nothing to introduce" ].
 
+Local Tactic Notation "iIntro" "_" :=
+  try iStartProof;
+  first
+  [ (* (?Q → _) *) apply tac_impl_intro_drop
+  | (* (_ -∗ _) *) apply tac_wand_intro_drop
+  | (* (∀ _, _) *) iIntro (_)
+  | fail 1 "iIntro: nothing to introduce" ].
+
 Local Tactic Notation "iIntroForall" :=
   try iStartProof;
   lazymatch goal with
@@ -795,6 +803,7 @@ Tactic Notation "iIntros" constr(pat) :=
     (* Optimizations to avoid generating fresh names *)
     | IPureElim :: ?pats => iIntro (?); go pats
     | IAlwaysElim (IName ?H) :: ?pats => iIntro #H; go pats
+    | IDrop :: ?pats => iIntro _; go pats
     | IName ?H :: ?pats => iIntro H; go pats
     (* Introduction patterns that can only occur at the top-level *)
     | IPureIntro :: ?pats => iPureIntro; go pats
-- 
GitLab