From 090aaea3a4162d6ce5608b4040a097f321928bc9 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 9 Sep 2016 00:43:28 +0200
Subject: [PATCH] =?UTF-8?q?Support=20for=20specialization=20of=20P?=
=?UTF-8?q?=E2=82=81=20-=E2=98=85=20..=20-=E2=98=85=20P=E2=82=99=20-?=
=?UTF-8?q?=E2=98=85=20Q=20where=20Q=20is=20persistent.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
Before this commit, given "HP" : P and "H" : P -★ Q with Q persistent, one
could write:
iSpecialize ("H" with "#HP")
to eliminate the wand in "H" while keeping the resource "HP". The lemma:
own_valid : own γ x ⊢ ✓ x
was the prototypical example where this pattern (using the #) was used.
However, the pattern was too limited. For example, given "H" : P₠-★ P₂ -★ Q",
one could not write iSpecialize ("H" with "#HPâ‚") because Pâ‚‚ -★ Q is not
persistent, even when Q is.
So, instead, this commit introduces the following tactic:
iSpecialize pm_trm as #
which allows one to eliminate implications and wands while being able to use
all hypotheses to prove the premises, as well as being able to use all
hypotheses to prove the resulting goal.
In the case of iDestruct, we now check whether all branches of the introduction
pattern start with an `#` (moving the hypothesis to the persistent context) or
`%` (moving the hypothesis to the pure Coq context). If this is the case, we
allow one to use all hypotheses for proving the premises, as well as for proving
the resulting goal.
---
ProofMode.md | 25 ++++---
heap_lang/lib/ticket_lock.v | 2 +-
program_logic/adequacy.v | 2 +-
program_logic/auth.v | 2 +-
program_logic/boxes.v | 9 +--
program_logic/lifting.v | 2 +-
program_logic/ownership.v | 12 ++--
program_logic/sts.v | 2 +-
proofmode/coq_tactics.v | 39 ++++++-----
proofmode/intro_patterns.v | 9 +++
proofmode/spec_patterns.v | 5 +-
proofmode/tactics.v | 132 +++++++++++++++++++----------------
tests/counter.v | 4 +-
tests/joining_existentials.v | 2 +-
tests/one_shot.v | 2 +-
tests/proofmode.v | 2 +-
16 files changed, 141 insertions(+), 110 deletions(-)
diff --git a/ProofMode.md b/ProofMode.md
index 59846cef5..ae2233edf 100644
--- a/ProofMode.md
+++ b/ProofMode.md
@@ -32,6 +32,10 @@ Context management
- `iRename "H1" into "H2"` : rename the hypothesis `H1` into `H2`.
- `iSpecialize pm_trm` : instantiate universal quantifiers and eliminate
implications/wands of a hypothesis `pm_trm`. See proof mode terms below.
+- `iSpecialize pm_trm as #` : instantiate universal quantifiers and eliminate
+ implications/wands of a hypothesis whose conclusion is persistent. In this
+ case, all hypotheses can be used for proving the premises, as well as for
+ the resulting goal.
- `iPoseProof pm_trm as "H"` : put `pm_trm` into the context as a new hypothesis
`H`.
- `iAssert P with "spat" as "ipat"` : create a new goal with conclusion `P` and
@@ -60,12 +64,17 @@ Elimination of logical connectives
----------------------------------
- `iExFalso` : Ex falso sequitur quod libet.
-- `iDestruct pm_trm as (x1 ... xn) "spat1 ... spatn"` : elimination of
- existential quantifiers using Coq introduction patterns `x1 ... xn` and
- elimination of object level connectives using the proof mode introduction
- patterns `ipat1 ... ipatn`.
+- `iDestruct pm_trm as (x1 ... xn) "ipat"` : elimination of existential
+ quantifiers using Coq introduction patterns `x1 ... xn` and elimination of
+ object level connectives using the proof mode introduction pattern `ipat`.
+ In case all branches of `ipat` start with an `#` (moving the hypothesis to the
+ persistent context) or `%` (moving the hypothesis to the pure Coq context),
+ one can use all hypotheses for proving the premises of `pm_trm`, as well as
+ for proving the resulting goal.
- `iDestruct pm_trm as %cpat` : elimination of a pure hypothesis using the Coq
- introduction pattern `cpat`.
+ introduction pattern `cpat`. When using this tactic, all hypotheses can be
+ used for proving the premises of `pm_trm`, as well as for proving the
+ resulting goal.
Separating logic specific tactics
---------------------------------
@@ -180,9 +189,9 @@ so called specification patterns to express this splitting:
- `==>[H1 ... Hn]` : same as the above pattern, but can only be used if the goal
is a primitive view shift, in which case the view shift will be kept in the
goal of the premise too.
-- `[#]` : This pattern can be used when eliminating `P -★ Q` when either `P` or
- `Q` is persistent. In this case, all hypotheses are available in the goal for
- the premise as none will be consumed.
+- `[#]` : This pattern can be used when eliminating `P -★ Q` with `P`
+ persistent. Using this pattern, all hypotheses are available in the goal for
+ `P`, as well the remaining goal.
- `[%]` : This pattern can be used when eliminating `P -★ Q` when `P` is pure.
It will generate a Coq goal for `P` and does not consume any hypotheses.
- `*` : instantiate all top-level universal quantifiers with meta variables.
diff --git a/heap_lang/lib/ticket_lock.v b/heap_lang/lib/ticket_lock.v
index 219a66abe..d4994cd76 100644
--- a/heap_lang/lib/ticket_lock.v
+++ b/heap_lang/lib/ticket_lock.v
@@ -166,7 +166,7 @@ Section proof.
as %[[[[?|] ?] [=]%leibniz_equiv_iff] ?]%auth_valid_discrete. }
iDestruct "Haown" as "[[Hγo' _]|?]".
{ iCombine "Hγo" "Hγo'" as "Hγo".
- iDestruct (own_valid with "#Hγo") as %[[] ?]. }
+ iDestruct (own_valid with "Hγo") as %[[] ?]. }
iCombine "Hauth" "Hγo" as "Hauth".
iVs (own_update with "Hauth") as "Hauth".
{ rewrite pair_split_L. apply: (auth_update _ _ (Excl' (S o), _)). (* FIXME: apply is slow *)
diff --git a/program_logic/adequacy.v b/program_logic/adequacy.v
index b2480ac7e..5569939f7 100644
--- a/program_logic/adequacy.v
+++ b/program_logic/adequacy.v
@@ -134,7 +134,7 @@ Proof.
rewrite pvs_eq in HI;
iVs (HI with "HI [Hw HE]") as "> (_ & _ & H)"; first by iFrame.
iDestruct "H" as (σ2') "[Hσf %]".
- iDestruct (ownP_agree σ2 σ2' with "[#]") as %<-. by iFrame. eauto.
+ iDestruct (ownP_agree σ2 σ2' with "[-]") as %<-. by iFrame. eauto.
Qed.
End adequacy.
diff --git a/program_logic/auth.v b/program_logic/auth.v
index a56f54d5b..99231ad4b 100644
--- a/program_logic/auth.v
+++ b/program_logic/auth.v
@@ -98,7 +98,7 @@ Section auth.
Proof.
iIntros (?) "(#? & >Hγf)". rewrite /auth_ctx /auth_own.
iInv N as (a') "[>Hγ Hφ]" "Hclose". iCombine "Hγ" "Hγf" as "Hγ".
- iDestruct (own_valid with "#Hγ") as % [[af Ha'] ?]%auth_valid_discrete.
+ iDestruct (own_valid with "Hγ") as % [[af Ha'] ?]%auth_valid_discrete.
simpl in Ha'; rewrite ->(left_id _ _) in Ha'; setoid_subst.
iVsIntro. iExists af; iFrame "Hφ"; iSplit; first done.
iIntros (b) "[% Hφ]".
diff --git a/program_logic/boxes.v b/program_logic/boxes.v
index 97a46c231..29c34b6b8 100644
--- a/program_logic/boxes.v
+++ b/program_logic/boxes.v
@@ -118,8 +118,7 @@ Proof.
iDestruct (big_sepM_delete _ f _ false with "Hf")
as "[[Hγ' #[HγΦ ?]] ?]"; first done.
iDestruct (box_own_agree γ Q (Φ γ) with "[#]") as "HeqQ"; first by eauto.
- iDestruct (box_own_auth_agree γ b false with "[#]")
- as "%"; subst; first by iFrame.
+ iDestruct (box_own_auth_agree γ b false with "[-]") as %->; first by iFrame.
iSplitL "Hγ"; last iSplit.
- iExists false; eauto.
- iNext. iRewrite "HeqP". iRewrite "HeqQ". by rewrite -big_sepM_delete.
@@ -153,8 +152,7 @@ Proof.
iDestruct (big_sepM_later _ f with "Hf") as "Hf".
iDestruct (big_sepM_delete _ f with "Hf")
as "[[>Hγ' #[HγΦ Hinv']] ?]"; first done.
- iDestruct (box_own_auth_agree γ b true with "[#]")
- as %?; subst; first by iFrame.
+ iDestruct (box_own_auth_agree γ b true with "[-]") as %->; first by iFrame.
iFrame "HQ".
iVs (box_own_auth_update γ with "[Hγ Hγ']") as "[Hγ Hγ']"; first by iFrame.
iVs ("Hclose" with "[Hγ]"); first (iNext; iExists false; by repeat iSplit).
@@ -189,8 +187,7 @@ Proof.
iAlways; iIntros (γ b ?) "(Hγ' & #$ & #$)".
assert (true = b) as <- by eauto.
iInv N as (b) "(>Hγ & _ & HΦ)" "Hclose".
- iDestruct (box_own_auth_agree γ b true with "[#]")
- as "%"; subst; first by iFrame.
+ iDestruct (box_own_auth_agree γ b true with "[-]") as %->; first by iFrame.
iVs (box_own_auth_update γ true true false with "[Hγ Hγ']")
as "[Hγ $]"; first by iFrame.
iVs ("Hclose" with "[Hγ]"); first (iNext; iExists false; iFrame; eauto).
diff --git a/program_logic/lifting.v b/program_logic/lifting.v
index 1dcd9a8b0..16ef16d2a 100644
--- a/program_logic/lifting.v
+++ b/program_logic/lifting.v
@@ -20,7 +20,7 @@ Lemma wp_lift_step E Φ e1 :
Proof.
iIntros (?) "H". rewrite wp_unfold /wp_pre; iRight; iSplit; auto.
iIntros (σ1) "Hσ". iVs "H" as (σ1') "(% & >Hσf & H)".
- iDestruct (ownP_agree σ1 σ1' with "[#]") as %<-; first by iFrame.
+ iDestruct (ownP_agree σ1 σ1' with "[-]") as %<-; first by iFrame.
iVsIntro; iSplit; [done|]; iNext; iIntros (e2 σ2 efs Hstep).
iVs (ownP_update σ1 σ2 with "[-H]") as "[$ ?]"; first by iFrame.
iApply "H"; eauto.
diff --git a/program_logic/ownership.v b/program_logic/ownership.v
index aa42399a2..b6f3ad902 100644
--- a/program_logic/ownership.v
+++ b/program_logic/ownership.v
@@ -89,7 +89,7 @@ Proof. rewrite /ownE -own_op own_valid. by iIntros (?%coPset_disj_valid_op). Qed
Lemma ownE_op' E1 E2 : E1 ⊥ E2 ∧ ownE (E1 ∪ E2) ⊣⊢ ownE E1 ★ ownE E2.
Proof.
iSplit; [iIntros "[% ?]"; by iApply ownE_op|].
- iIntros "HE". iDestruct (ownE_disjoint with "#HE") as %?.
+ iIntros "HE". iDestruct (ownE_disjoint with "HE") as %?.
iSplit; first done. iApply ownE_op; by try iFrame.
Qed.
Lemma ownE_singleton_twice i : ownE {[i]} ★ ownE {[i]} ⊢ False.
@@ -104,7 +104,7 @@ Proof. rewrite /ownD -own_op own_valid. by iIntros (?%gset_disj_valid_op). Qed.
Lemma ownD_op' E1 E2 : E1 ⊥ E2 ∧ ownD (E1 ∪ E2) ⊣⊢ ownD E1 ★ ownD E2.
Proof.
iSplit; [iIntros "[% ?]"; by iApply ownD_op|].
- iIntros "HE". iDestruct (ownD_disjoint with "#HE") as %?.
+ iIntros "HE". iDestruct (ownD_disjoint with "HE") as %?.
iSplit; first done. iApply ownD_op; by try iFrame.
Qed.
Lemma ownD_singleton_twice i : ownD {[i]} ★ ownD {[i]} ⊢ False.
@@ -132,19 +132,19 @@ Qed.
Lemma ownI_open i P : wsat ★ ownI i P ★ ownE {[i]} ⊢ wsat ★ ▷ P ★ ownD {[i]}.
Proof.
rewrite /ownI. iIntros "(Hw & Hi & HiE)". iDestruct "Hw" as (I) "[? HI]".
- iDestruct (invariant_lookup I i P with "[#]") as (Q) "[% #HPQ]"; [by iFrame|].
+ iDestruct (invariant_lookup I i P with "[-]") as (Q) "[% #HPQ]"; [by iFrame|].
iDestruct (big_sepM_delete _ _ i with "HI") as "[[[HQ $]|?] HI]"; eauto.
- iSplitR "HQ"; last by iNext; iRewrite -"HPQ".
iExists I. iFrame "Hw". iApply (big_sepM_delete _ _ i); eauto.
iFrame "HI"; eauto.
- - iDestruct (ownE_singleton_twice with "[#]") as %[]. by iFrame.
+ - iDestruct (ownE_singleton_twice with "[-]") as %[]. by iFrame.
Qed.
Lemma ownI_close i P : wsat ★ ownI i P ★ ▷ P ★ ownD {[i]} ⊢ wsat ★ ownE {[i]}.
Proof.
rewrite /ownI. iIntros "(Hw & Hi & HP & HiD)". iDestruct "Hw" as (I) "[? HI]".
- iDestruct (invariant_lookup with "[#]") as (Q) "[% #HPQ]"; first by iFrame.
+ iDestruct (invariant_lookup with "[-]") as (Q) "[% #HPQ]"; first by iFrame.
iDestruct (big_sepM_delete _ _ i with "HI") as "[[[HQ ?]|$] HI]"; eauto.
- - iDestruct (ownD_singleton_twice with "[#]") as %[]. by iFrame.
+ - iDestruct (ownD_singleton_twice with "[-]") as %[]. by iFrame.
- iExists I. iFrame "Hw". iApply (big_sepM_delete _ _ i); eauto.
iFrame "HI". iLeft. iFrame "HiD". by iNext; iRewrite "HPQ".
Qed.
diff --git a/program_logic/sts.v b/program_logic/sts.v
index 4693dc29d..a27c28ce6 100644
--- a/program_logic/sts.v
+++ b/program_logic/sts.v
@@ -95,7 +95,7 @@ Section sts.
Proof.
iIntros "[Hinv Hγf]". rewrite /sts_ownS /sts_inv /sts_own.
iDestruct "Hinv" as (s) "[>Hγ Hφ]".
- iCombine "Hγ" "Hγf" as "Hγ"; iDestruct (own_valid with "#Hγ") as %Hvalid.
+ iCombine "Hγ" "Hγf" as "Hγ"; iDestruct (own_valid with "Hγ") as %Hvalid.
assert (s ∈ S) by eauto using sts_auth_frag_valid_inv.
assert (✓ sts_frag S T) as [??] by eauto using cmra_valid_op_r.
rewrite sts_op_auth_frag //.
diff --git a/proofmode/coq_tactics.v b/proofmode/coq_tactics.v
index 0d116ac97..0917c2769 100644
--- a/proofmode/coq_tactics.v
+++ b/proofmode/coq_tactics.v
@@ -488,7 +488,7 @@ Proof.
by rewrite always_if_elim assoc !wand_elim_r.
Qed.
-Lemma tac_specialize_pure Δ Δ' j q R P1 P2 φ Q :
+Lemma tac_specialize_assert_pure Δ Δ' j q R P1 P2 φ Q :
envs_lookup j Δ = Some (q, R) →
IntoWand R P1 P2 → FromPure P1 φ →
envs_simple_replace j q (Esnoc Enil j P2) Δ = Some Δ' →
@@ -498,24 +498,31 @@ Proof.
by rewrite right_id (into_wand R) -(from_pure P1) // wand_True wand_elim_r.
Qed.
-Lemma tac_specialize_persistent Δ Δ' Δ'' j q P1 P2 R Q :
+Lemma tac_specialize_assert_persistent Δ Δ' Δ'' j q P1 P2 R Q :
envs_lookup_delete j Δ = Some (q, R, Δ') →
- IntoWand R P1 P2 →
+ IntoWand R P1 P2 → PersistentP P1 →
envs_simple_replace j q (Esnoc Enil j P2) Δ = Some Δ'' →
- (Δ' ⊢ P1) → (PersistentP P1 ∨ PersistentP P2) →
- (Δ'' ⊢ Q) → Δ ⊢ Q.
+ (Δ' ⊢ P1) → (Δ'' ⊢ Q) → Δ ⊢ Q.
+Proof.
+ intros [? ->]%envs_lookup_delete_Some ??? HP1 <-.
+ rewrite envs_lookup_sound //.
+ rewrite -(idemp uPred_and (envs_delete _ _ _)).
+ rewrite {1}HP1 (persistentP P1) always_and_sep_l assoc.
+ rewrite envs_simple_replace_sound' //; simpl.
+ rewrite right_id (into_wand R) (always_elim_if q) -always_if_sep wand_elim_l.
+ by rewrite wand_elim_r.
+Qed.
+
+Lemma tac_specialize_persistent_helper Δ Δ' j q P R Q :
+ envs_lookup j Δ = Some (q,P) →
+ (Δ ⊢ R) → PersistentP R →
+ envs_replace j q true (Esnoc Enil j R) Δ = Some Δ' →
+ (Δ' ⊢ Q) → Δ ⊢ Q.
Proof.
- intros [? ->]%envs_lookup_delete_Some ?? HP1 [?|?] <-.
- - rewrite envs_lookup_sound //.
- rewrite -(idemp uPred_and (envs_delete _ _ _)).
- rewrite {1}HP1 (persistentP P1) always_and_sep_l assoc.
- rewrite envs_simple_replace_sound' //; simpl.
- rewrite right_id (into_wand R) (always_elim_if q) -always_if_sep wand_elim_l.
- by rewrite wand_elim_r.
- - rewrite -(idemp uPred_and Δ) {1}envs_lookup_sound //; simpl; rewrite HP1.
- rewrite envs_simple_replace_sound //; simpl.
- rewrite (sep_elim_r _ (_ -★ _)) right_id (into_wand R) always_if_elim.
- by rewrite wand_elim_l always_and_sep_l -{1}(always_if_always q P2) wand_elim_r.
+ intros ? HR ?? <-.
+ rewrite -(idemp uPred_and Δ) {1}HR always_and_sep_l.
+ rewrite envs_replace_sound //; simpl.
+ by rewrite right_id assoc (sep_elim_l R) always_always wand_elim_r.
Qed.
Lemma tac_revert Δ Δ' i p P Q :
diff --git a/proofmode/intro_patterns.v b/proofmode/intro_patterns.v
index ac49db839..f2feecb44 100644
--- a/proofmode/intro_patterns.v
+++ b/proofmode/intro_patterns.v
@@ -19,6 +19,15 @@ Inductive intro_pat :=
| IAll : intro_pat
| IClear : list (bool * string) → intro_pat. (* true = frame, false = clear *)
+Fixpoint intro_pat_persistent (p : intro_pat) :=
+ match p with
+ | IPureElim => true
+ | IAlwaysElim _ => true
+ | ILaterElim p => intro_pat_persistent p
+ | IList pps => forallb (forallb intro_pat_persistent) pps
+ | _ => false
+ end.
+
Module intro_pat.
Inductive token :=
| TName : string → token
diff --git a/proofmode/spec_patterns.v b/proofmode/spec_patterns.v
index 03f6d40f9..d72706b2f 100644
--- a/proofmode/spec_patterns.v
+++ b/proofmode/spec_patterns.v
@@ -6,7 +6,7 @@ Inductive spec_pat :=
| SGoal : spec_goal_kind → bool → list string → spec_pat
| SGoalPersistent : spec_pat
| SGoalPure : spec_pat
- | SName : bool → string → spec_pat (* first arg = persistent *)
+ | SName : string → spec_pat
| SForall : spec_pat.
Module spec_pat.
@@ -44,13 +44,12 @@ Inductive state :=
Fixpoint parse_go (ts : list token) (k : list spec_pat) : option (list spec_pat) :=
match ts with
| [] => Some (rev k)
- | TName s :: ts => parse_go ts (SName false s :: k)
+ | TName s :: ts => parse_go ts (SName s :: k)
| TBracketL :: TPersistent :: TBracketR :: ts => parse_go ts (SGoalPersistent :: k)
| TBracketL :: TPure :: TBracketR :: ts => parse_go ts (SGoalPure :: k)
| TBracketL :: ts => parse_goal ts GoalStd false [] k
| TVs :: TBracketL :: ts => parse_goal ts GoalVs false [] k
| TVs :: ts => parse_go ts (SGoal GoalVs true [] :: k)
- | TPersistent :: TName s :: ts => parse_go ts (SName true s :: k)
| TForall :: ts => parse_go ts (SForall :: k)
| _ => None
end
diff --git a/proofmode/tactics.v b/proofmode/tactics.v
index 3db566b13..382e488ae 100644
--- a/proofmode/tactics.v
+++ b/proofmode/tactics.v
@@ -152,7 +152,7 @@ Local Tactic Notation "iSpecializePat" constr(H) constr(pat) :=
lazymatch pats with
| [] => idtac
| SForall :: ?pats => try (iSpecializeArgs H1 (hcons _ _)); go H1 pats
- | SName false ?H2 :: ?pats =>
+ | SName ?H2 :: ?pats =>
eapply tac_specialize with _ _ H2 _ H1 _ _ _ _; (* (j:=H1) (i:=H2) *)
[env_cbv; reflexivity || fail "iSpecialize:" H2 "not found"
|env_cbv; reflexivity || fail "iSpecialize:" H1 "not found"
@@ -160,30 +160,17 @@ Local Tactic Notation "iSpecializePat" constr(H) constr(pat) :=
let Q := match goal with |- IntoWand ?P ?Q _ => Q end in
apply _ || fail "iSpecialize: cannot instantiate" P "with" Q
|env_cbv; reflexivity|go H1 pats]
- | SName true ?H2 :: ?pats =>
- eapply tac_specialize_persistent with _ _ H1 _ _ _ _;
- [env_cbv; reflexivity || fail "iSpecialize:" H1 "not found"
- |solve_to_wand H1
- |env_cbv; reflexivity
- |iExact H2 || fail "iSpecialize:" H2 "not found or wrong type"
- |let Q1 := match goal with |- PersistentP ?Q1 ∨ _ => Q1 end in
- let Q2 := match goal with |- _ ∨ PersistentP ?Q2 => Q2 end in
- first [left; apply _ | right; apply _]
- || fail "iSpecialize:" Q1 "nor" Q2 "persistent"
- |go H1 pats]
| SGoalPersistent :: ?pats =>
- eapply tac_specialize_persistent with _ _ H1 _ _ _ _;
+ eapply tac_specialize_assert_persistent with _ _ H1 _ _ _ _;
[env_cbv; reflexivity || fail "iSpecialize:" H1 "not found"
|solve_to_wand H1
+ |let Q := match goal with |- PersistentP ?Q => Q end in
+ apply _ || fail "iSpecialize:" Q "not persistent"
|env_cbv; reflexivity
|(*goal*)
- |let Q1 := match goal with |- PersistentP ?Q1 ∨ _ => Q1 end in
- let Q2 := match goal with |- _ ∨ PersistentP ?Q2 => Q2 end in
- first [left; apply _ | right; apply _]
- || fail "iSpecialize:" Q1 "nor" Q2 "persistent"
|go H1 pats]
| SGoalPure :: ?pats =>
- eapply tac_specialize_pure with _ H1 _ _ _ _ _;
+ eapply tac_specialize_assert_pure with _ H1 _ _ _ _ _;
[env_cbv; reflexivity || fail "iSpecialize:" H1 "not found"
|solve_to_wand H1
|let Q := match goal with |- FromPure ?Q _ => Q end in
@@ -204,11 +191,37 @@ Local Tactic Notation "iSpecializePat" constr(H) constr(pat) :=
|go H1 pats]
end in let pats := spec_pat.parse pat in go H pats.
-Tactic Notation "iSpecialize" open_constr(t) :=
- match t with
- | ITrm ?H ?xs ?pat => iSpecializeArgs H xs; iSpecializePat H pat
+(* p = whether the conclusion of the specialized term is persistent. It can
+either be a Boolean or an introduction pattern, which will be coerced in true
+when it only contains `#` or `%` patterns at the top-level. *)
+Tactic Notation "iSpecializeCore" open_constr(t) "as" constr(p) tactic(tac) :=
+ let p :=
+ lazymatch type of p with
+ | intro_pat => eval cbv in (intro_pat_persistent p)
+ | string =>
+ let pat := intro_pat.parse_one p in
+ eval cbv in (intro_pat_persistent pat)
+ | _ => p
+ end in
+ lazymatch t with
+ | ITrm ?H ?xs ?pat =>
+ lazymatch p with
+ | true =>
+ eapply tac_specialize_persistent_helper with _ H _ _ _;
+ [env_cbv; reflexivity || fail "iSpecialize:" H "not found"
+ |iSpecializeArgs H xs; iSpecializePat H pat; last (iExact H)
+ |let Q := match goal with |- PersistentP ?Q => Q end in
+ apply _ || fail "iSpecialize:" Q "not persistent"
+ |env_cbv; reflexivity|tac H]
+ | false => iSpecializeArgs H xs; iSpecializePat H pat; last (tac H)
+ end
end.
+Tactic Notation "iSpecialize" open_constr(t) :=
+ iSpecializeCore t as false (fun _ => idtac).
+Tactic Notation "iSpecialize" open_constr(t) "#" :=
+ iSpecializeCore t as true (fun _ => idtac).
+
(** * Pose proof *)
(* The tactic [iIntoEntails] tactic solves a goal [True ⊢ Q]. The arguments [t]
is a Coq term whose type is of the following shape:
@@ -236,7 +249,7 @@ Tactic Notation "iIntoEntails" open_constr(t) :=
end
in go t.
-Tactic Notation "iPoseProofCore" open_constr(lem) "as" tactic(tac) :=
+Tactic Notation "iPoseProofCore" open_constr(lem) "as" constr(p) tactic(tac) :=
let pose_trm t tac :=
let Htmp := iFresh in
lazymatch type of t with
@@ -255,16 +268,12 @@ Tactic Notation "iPoseProofCore" open_constr(lem) "as" tactic(tac) :=
after the continuation [tac] has been called. *)
in lazymatch lem with
| ITrm ?t ?xs ?pat =>
- pose_trm t ltac:(fun Htmp =>
- iSpecializeArgs Htmp xs; iSpecializePat Htmp pat; last (tac Htmp))
+ pose_trm t ltac:(fun Htmp => iSpecializeCore (ITrm Htmp xs pat) as p tac)
| _ => pose_trm lem tac
end.
Tactic Notation "iPoseProof" open_constr(lem) "as" constr(H) :=
- iPoseProofCore lem as (fun Htmp => iRename Htmp into H).
-
-Tactic Notation "iPoseProof" open_constr(lem) :=
- iPoseProofCore lem as (fun _ => idtac).
+ iPoseProofCore lem as false (fun Htmp => iRename Htmp into H).
(** * Apply *)
Tactic Notation "iApply" open_constr(lem) :=
@@ -277,12 +286,12 @@ Tactic Notation "iApply" open_constr(lem) :=
|lazy beta (* reduce betas created by instantiation *)]] in
lazymatch lem with
| ITrm ?t ?xs ?pat =>
- iPoseProofCore t as (fun Htmp =>
+ iPoseProofCore t as false (fun Htmp =>
iSpecializeArgs Htmp xs;
try (iSpecializeArgs Htmp (hcons _ _));
iSpecializePat Htmp pat; last finish Htmp)
| _ =>
- iPoseProofCore lem as (fun Htmp =>
+ iPoseProofCore lem as false (fun Htmp =>
try (iSpecializeArgs Htmp (hcons _ _));
finish Htmp)
end.
@@ -723,7 +732,7 @@ Tactic Notation "iIntros" "(" simple_intropattern(x1) simple_intropattern(x2)
iIntros ( x1 x2 x3 x4 x5 x6 x7 x8 ); iIntros p.
(** * Destruct tactic *)
-Tactic Notation "iDestructCore" open_constr(lem) "as" tactic(tac) :=
+Tactic Notation "iDestructCore" open_constr(lem) "as" constr(p) tactic(tac) :=
let intro_destruct n :=
let rec go n' :=
lazymatch n' with
@@ -738,49 +747,50 @@ Tactic Notation "iDestructCore" open_constr(lem) "as" tactic(tac) :=
let n := eval compute in (Z.to_nat lem) in intro_destruct n
| string => tac lem
| iTrm =>
+ (* only copy the hypothesis when universal quantifiers are instantiated *)
lazymatch lem with
- | @iTrm string ?H _ hnil ?pat => iSpecializePat H pat; last (tac H)
- | _ => iPoseProofCore lem as tac
+ | @iTrm string ?H _ hnil ?pat => iSpecializeCore lem as p tac
+ | _ => iPoseProofCore lem as p tac
end
- | _ => iPoseProofCore lem as tac
+ | _ => iPoseProofCore lem as p tac
end.
Tactic Notation "iDestruct" open_constr(lem) "as" constr(pat) :=
- iDestructCore lem as (fun H => iDestructHyp H as pat).
+ iDestructCore lem as pat (fun H => iDestructHyp H as pat).
Tactic Notation "iDestruct" open_constr(lem) "as" "(" simple_intropattern(x1) ")"
constr(pat) :=
- iDestructCore lem as (fun H => iDestructHyp H as ( x1 ) pat).
+ iDestructCore lem as pat (fun H => iDestructHyp H as ( x1 ) pat).
Tactic Notation "iDestruct" open_constr(lem) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) ")" constr(pat) :=
- iDestructCore lem as (fun H => iDestructHyp H as ( x1 x2 ) pat).
+ iDestructCore lem as pat (fun H => iDestructHyp H as ( x1 x2 ) pat).
Tactic Notation "iDestruct" open_constr(lem) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) ")" constr(pat) :=
- iDestructCore lem as (fun H => iDestructHyp H as ( x1 x2 x3 ) pat).
+ iDestructCore lem as pat (fun H => iDestructHyp H as ( x1 x2 x3 ) pat).
Tactic Notation "iDestruct" open_constr(lem) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) ")"
constr(pat) :=
- iDestructCore lem as (fun H => iDestructHyp H as ( x1 x2 x3 x4 ) pat).
+ iDestructCore lem as pat (fun H => iDestructHyp H as ( x1 x2 x3 x4 ) pat).
Tactic Notation "iDestruct" open_constr(lem) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) ")" constr(pat) :=
- iDestructCore lem as (fun H => iDestructHyp H as ( x1 x2 x3 x4 x5 ) pat).
+ iDestructCore lem as pat (fun H => iDestructHyp H as ( x1 x2 x3 x4 x5 ) pat).
Tactic Notation "iDestruct" open_constr(lem) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) simple_intropattern(x6) ")" constr(pat) :=
- iDestructCore lem as (fun H => iDestructHyp H as ( x1 x2 x3 x4 x5 x6 ) pat).
+ iDestructCore lem as pat (fun H => iDestructHyp H as ( x1 x2 x3 x4 x5 x6 ) pat).
Tactic Notation "iDestruct" open_constr(lem) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7) ")"
constr(pat) :=
- iDestructCore lem as (fun H => iDestructHyp H as ( x1 x2 x3 x4 x5 x6 x7 ) pat).
+ iDestructCore lem as pat (fun H => iDestructHyp H as ( x1 x2 x3 x4 x5 x6 x7 ) pat).
Tactic Notation "iDestruct" open_constr(lem) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7)
simple_intropattern(x8) ")" constr(pat) :=
- iDestructCore lem as (fun H => iDestructHyp H as ( x1 x2 x3 x4 x5 x6 x7 x8 ) pat).
+ iDestructCore lem as pat (fun H => iDestructHyp H as ( x1 x2 x3 x4 x5 x6 x7 x8 ) pat).
Tactic Notation "iDestruct" open_constr(lem) "as" "%" simple_intropattern(pat) :=
- iDestructCore lem as (fun H => iPure H as pat).
+ iDestructCore lem as true (fun H => iPure H as pat).
(* This is pretty ugly, but without Ltac support for manipulating lists of
idents I do not know how to do this better. *)
@@ -857,7 +867,7 @@ Local Ltac iRewriteFindPred :=
end.
Local Tactic Notation "iRewriteCore" constr(lr) open_constr(lem) :=
- iPoseProofCore lem as (fun Heq =>
+ iPoseProofCore lem as true (fun Heq =>
eapply (tac_rewrite _ Heq _ _ lr);
[env_cbv; reflexivity || fail "iRewrite:" Heq "not found"
|let P := match goal with |- ?P ⊢ _ => P end in
@@ -869,7 +879,7 @@ Tactic Notation "iRewrite" open_constr(lem) := iRewriteCore false lem.
Tactic Notation "iRewrite" "-" open_constr(lem) := iRewriteCore true lem.
Local Tactic Notation "iRewriteCore" constr(lr) open_constr(lem) "in" constr(H) :=
- iPoseProofCore lem as (fun Heq =>
+ iPoseProofCore lem as true (fun Heq =>
eapply (tac_rewrite_in _ Heq _ _ H _ _ lr);
[env_cbv; reflexivity || fail "iRewrite:" Heq "not found"
|env_cbv; reflexivity || fail "iRewrite:" H "not found"
@@ -890,45 +900,45 @@ Ltac iSimplifyEq := repeat (
(** * View shifts *)
Tactic Notation "iVs" open_constr(lem) :=
- iDestructCore lem as (fun H => iVsCore H; last iDestruct H as "?").
+ iDestructCore lem as false (fun H => iVsCore H).
Tactic Notation "iVs" open_constr(lem) "as" constr(pat) :=
- iDestructCore lem as (fun H => iVsCore H; last iDestruct H as pat).
+ iDestructCore lem as false (fun H => iVsCore H; last iDestructHyp H as pat).
Tactic Notation "iVs" open_constr(lem) "as" "(" simple_intropattern(x1) ")"
constr(pat) :=
- iDestructCore lem as (fun H => iVsCore H; last iDestruct H as ( x1 ) pat).
+ iDestructCore lem as false (fun H => iVsCore H; last iDestructHyp H as ( x1 ) pat).
Tactic Notation "iVs" open_constr(lem) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) ")" constr(pat) :=
- iDestructCore lem as (fun H => iVsCore H; last iDestruct H as ( x1 x2 ) pat).
+ iDestructCore lem as false (fun H => iVsCore H; last iDestructHyp H as ( x1 x2 ) pat).
Tactic Notation "iVs" open_constr(lem) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) ")" constr(pat) :=
- iDestructCore lem as (fun H => iVsCore H; last iDestruct H as ( x1 x2 x3 ) pat).
+ iDestructCore lem as false (fun H => iVsCore H; last iDestructHyp H as ( x1 x2 x3 ) pat).
Tactic Notation "iVs" open_constr(lem) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) ")"
constr(pat) :=
- iDestructCore lem as (fun H =>
- iVsCore H; last iDestruct H as ( x1 x2 x3 x4 ) pat).
+ iDestructCore lem as false (fun H =>
+ iVsCore H; last iDestructHyp H as ( x1 x2 x3 x4 ) pat).
Tactic Notation "iVs" open_constr(lem) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) ")" constr(pat) :=
- iDestructCore lem as (fun H =>
- iVsCore H; last iDestruct H as ( x1 x2 x3 x4 x5 ) pat).
+ iDestructCore lem as false (fun H =>
+ iVsCore H; last iDestructHyp H as ( x1 x2 x3 x4 x5 ) pat).
Tactic Notation "iVs" open_constr(lem) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) simple_intropattern(x6) ")" constr(pat) :=
- iDestructCore lem as (fun H =>
- iVsCore H; last iDestruct H as ( x1 x2 x3 x4 x5 x6 ) pat).
+ iDestructCore lem as false (fun H =>
+ iVsCore H; last iDestructHyp H as ( x1 x2 x3 x4 x5 x6 ) pat).
Tactic Notation "iVs" open_constr(lem) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7) ")"
constr(pat) :=
- iDestructCore lem as (fun H =>
- iVsCore H; last iDestruct H as ( x1 x2 x3 x4 x5 x6 x7 ) pat).
+ iDestructCore lem as false (fun H =>
+ iVsCore H; last iDestructHyp H as ( x1 x2 x3 x4 x5 x6 x7 ) pat).
Tactic Notation "iVs" open_constr(lem) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7)
simple_intropattern(x8) ")" constr(pat) :=
- iDestructCore lem as (fun H =>
- iVsCore H; last iDestruct H as ( x1 x2 x3 x4 x5 x6 x7 x8 ) pat).
+ iDestructCore lem as false (fun H =>
+ iVsCore H; last iDestructHyp H as ( x1 x2 x3 x4 x5 x6 x7 x8 ) pat).
(* Make sure that by and done solve trivial things in proof mode *)
Hint Extern 0 (of_envs _ ⊢ _) => by iPureIntro.
diff --git a/tests/counter.v b/tests/counter.v
index c5e84d11d..8d5bb62c1 100644
--- a/tests/counter.v
+++ b/tests/counter.v
@@ -113,7 +113,7 @@ Proof.
wp_bind (CAS _ _ _). iInv N as (c') ">[Hl Hγ]" "Hclose".
destruct (decide (c' = c)) as [->|].
- iCombine "Hγ" "Hγf" as "Hγ".
- iDestruct (own_valid with "#Hγ") as %?%auth_frag_valid; rewrite -auth_frag_op //.
+ iDestruct (own_valid with "Hγ") as %?%auth_frag_valid; rewrite -auth_frag_op //.
iVs (own_update with "Hγ") as "Hγ"; first apply M_update.
rewrite (auth_frag_op (S n) (S c)); last lia; iDestruct "Hγ" as "[Hγ Hγf]".
wp_cas_suc. iVs ("Hclose" with "[Hl Hγ]").
@@ -129,7 +129,7 @@ Lemma read_spec l n :
Proof.
iIntros "!# Hl /=". iDestruct "Hl" as (N γ) "(% & #Hh & #Hinv & Hγf)".
rewrite /read /=. wp_let. iInv N as (c) "[Hl Hγ]" "Hclose". wp_load.
- iDestruct (own_valid γ (Frag n ⋅ Auth c) with "[#]") as % ?%auth_frag_valid.
+ iDestruct (own_valid γ (Frag n ⋅ Auth c) with "[-]") as % ?%auth_frag_valid.
{ iApply own_op. by iFrame. }
rewrite (auth_frag_op c c); last lia; iDestruct "Hγ" as "[Hγ Hγf']".
iVs ("Hclose" with "[Hl Hγ]"); [iNext; iExists c; by iFrame|].
diff --git a/tests/joining_existentials.v b/tests/joining_existentials.v
index e06e47214..78adb9719 100644
--- a/tests/joining_existentials.v
+++ b/tests/joining_existentials.v
@@ -95,6 +95,6 @@ Proof.
+ iApply worker_spec; auto.
+ iApply worker_spec; auto.
+ auto.
- - iIntros (_ v) "[_ H]"; iPoseProof (Q_res_join with "H"). auto.
+ - iIntros (_ v) "[_ H]". iDestruct (Q_res_join with "H") as "?". auto.
Qed.
End proof.
diff --git a/tests/one_shot.v b/tests/one_shot.v
index 3e610b65d..92598f562 100644
--- a/tests/one_shot.v
+++ b/tests/one_shot.v
@@ -77,7 +77,7 @@ Proof.
{ iCombine "Hγ" "Hγ'" as "Hγ". by iDestruct (own_valid with "Hγ") as %?. }
wp_load.
iCombine "Hγ" "Hγ'" as "Hγ".
- iDestruct (own_valid with "#Hγ") as %[=->]%dec_agree_op_inv.
+ iDestruct (own_valid with "Hγ") as %[=->]%dec_agree_op_inv.
iVs ("Hclose" with "[Hl]") as "_".
{ iNext; iRight; by eauto. }
iVsIntro. wp_match. iApply wp_assert. wp_op=>?; simplify_eq/=; eauto.
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 49e2160cc..c6d23574c 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -68,7 +68,7 @@ Lemma demo_5 (M : ucmraT) (x y : M) (P : uPred M) :
Proof.
iIntros "H1 H2".
iRewrite (uPred.eq_sym x x with "[#]"); first done.
- iRewrite -("H1" $! _ with "[#]"); first done.
+ iRewrite -("H1" $! _ with "[-]"); first done.
done.
Qed.
--
GitLab