From 307d0084e75ae9597c669f5ca61d3cd545cdd51d Mon Sep 17 00:00:00 2001
From: Robbert Krebbers
Date: Tue, 20 Feb 2018 01:26:42 +0100
Subject: [PATCH] Have the `[$]` pattern succeed if the premise is `True` or
`emp`.
In the same way that `iFrame` would succeed on said goals.
---
theories/proofmode/coq_tactics.v | 4 ++++
theories/proofmode/tactics.v | 7 +++++--
2 files changed, 9 insertions(+), 2 deletions(-)
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index 3c56dc01..9f94d98b 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -817,6 +817,10 @@ Proof.
apply wand_intro_l. by rewrite assoc !wand_elim_r.
Qed.
+Lemma tac_unlock_emp Δ Q : envs_entails Δ Q → envs_entails Δ (emp ∗ locked Q).
+Proof. rewrite envs_entails_eq=> ->. by rewrite -lock left_id. Qed.
+Lemma tac_unlock_True Δ Q : envs_entails Δ Q → envs_entails Δ (True ∗ locked Q).
+Proof. rewrite envs_entails_eq=> ->. by rewrite -lock -True_sep_2. Qed.
Lemma tac_unlock Δ Q : envs_entails Δ Q → envs_entails Δ (locked Q).
Proof. by unlock. Qed.
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 4a1a64e0..3755bba6 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -553,8 +553,11 @@ Local Tactic Notation "iSpecializePat" open_constr(H) constr(pat) :=
| GSpatial => apply add_modal_id
| GModal => apply _ || fail "iSpecialize: goal not a modality"
end
- |iFrame "∗ #"; apply tac_unlock ||
- fail "iSpecialize: premise cannot be solved by framing"
+ |first
+ [apply tac_unlock_emp
+ |apply tac_unlock_True
+ |iFrame "∗ #"; apply tac_unlock
+ |fail "iSpecialize: premise cannot be solved by framing"]
|reflexivity]; iIntro H1; go H1 pats
end in let pats := spec_pat.parse pat in go H pats.
--
GitLab