Commit 090aaea3 authored by Robbert Krebbers's avatar Robbert Krebbers

Support for specialization of P₁ -★ .. -★ Pₙ -★ Q where Q is persistent.

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.
parent 7caec2ef
......@@ -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.
......
......@@ -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 *)
......
......@@ -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.
......
......@@ -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φ]".
......
......@@ -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).
......
......@@ -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.
......
......@@ -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.
......
......@@ -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 //.
......
......@@ -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 :
......
......@@ -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
......
......@@ -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
......
This diff is collapsed.
......@@ -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|].
......
......@@ -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.
......@@ -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.
......
......@@ -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.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment