Commit 87a8a19c authored by Robbert Krebbers's avatar Robbert Krebbers

Extend specialization patterns.

- Support for a `//` modifier to close the goal using `done`.
- Support for framing in the `[#]` specialization pattern for
  persistent premises, i.e. `[# $H1 $H2]`
- Add new "auto framing patterns" `[$]`, `[# $]` and `>[$]` that
  will try to solve the premise by framing. Hypothesis that are
  not framed are carried over to the next goal.
parent 14fe028c
......@@ -203,6 +203,8 @@ appear at the top level:
- `!#` : introduce an always modality (given that the spatial context is empty).
- `!>` : introduce a modality.
- `/=` : perform `simpl`.
- `//` : perform `try done` on all goals.
- `//=` : syntactic sugar for `/= //`
- `*` : introduce all universal quantifiers.
- `**` : introduce all universal quantifiers, as well as all arrows and wands.
......@@ -238,7 +240,7 @@ _specification patterns_ to express splitting of hypotheses:
- `[H1 ... Hn]` : generate a goal with the (spatial) hypotheses `H1 ... Hn` and
all persistent hypotheses. The spatial hypotheses among `H1 ... Hn` will be
consumed. Hypotheses may be prefixed with a `$`, which results in them being
framed in the generated goal.
framed in the generated goal for the premise.
- `[-H1 ... Hn]` : negated form of the above pattern.
- `>[H1 ... Hn]` : same as the above pattern, but can only be used if the goal
is a modality, in which case the modality will be kept in the generated goal
......@@ -246,19 +248,29 @@ _specification patterns_ to express splitting of hypotheses:
- `>[-H1 ... Hn]` : negated form of the above pattern.
- `>` : shorthand for `>[-]` (typically used for the last premise of an applied
lemma).
- `[#]` : This pattern can be used when eliminating `P -∗ Q` with `P`
- `[#]` : This pattern can be used when eliminating `P -∗ Q` with `P` being
persistent. Using this pattern, all hypotheses are available in the goal for
`P`, as well the remaining goal.
`P`, as well the remaining goal. The pattern can optionally contain
hypotheses prefixed with a `$`, which results in them being framed in the
generated goal for the premise.
- `[%]` : 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.
- `[$]` :
- `[# $]` :
- `>[$]` :
The specialization patterns `[H1 .. H2]`, `[-H1 ... Hn]`, `>[H1 ... Hn]`,
`>[H1 ... Hn]`, `[#]` and `[%]` can optionally be ended with a `//`. This causes
the `done` tactic being called to close the goal (after framing).
For example, given:
H : □ P -∗ P 2 -∗ x = 0 -∗ Q1 ∗ Q2
H : □ P -∗ P 2 -∗ R -∗ x = 0 -∗ Q1 ∗ Q2
One can write:
You can write:
iDestruct ("H" with "[#] [H1 $H2] [$] [% //]") as "[H4 H5]".
iDestruct ("H" with "[#] [H1 H2] [%]") as "[H4 H5]".
Proof mode terms
================
......
......@@ -104,7 +104,7 @@ 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 "[$Hw $Hi]") as (Q) "[% #HPQ]".
iDestruct (invariant_lookup I i P with "[$]") as (Q) "[% #HPQ]".
iDestruct (big_sepM_delete _ _ i with "HI") as "[[[HQ $]|HiE'] HI]"; eauto.
- iSplitR "HQ"; last by iNext; iRewrite -"HPQ".
iExists I. iFrame "Hw". iApply (big_sepM_delete _ _ i); eauto.
......@@ -114,9 +114,9 @@ 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 "[$Hw $Hi]") as (Q) "[% #HPQ]".
iDestruct (invariant_lookup with "[$]") as (Q) "[% #HPQ]".
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 %[].
- iExists I. iFrame "Hw". iApply (big_sepM_delete _ _ i); eauto.
iFrame "HI". iLeft. iFrame "HiD". by iNext; iRewrite "HPQ".
Qed.
......@@ -127,7 +127,7 @@ Lemma ownI_alloc φ P :
Proof.
iIntros (Hfresh) "[Hw HP]". iDestruct "Hw" as (I) "[? HI]".
iMod (own_empty (gset_disjUR positive) disabled_name) as "HE".
iMod (own_updateP with "HE") as "HE".
iMod (own_updateP with "[$]") as "HE".
{ apply (gset_disj_alloc_empty_updateP_strong' (λ i, I !! i = None φ i)).
intros E. destruct (Hfresh (E dom _ I))
as (i & [? HIi%not_elem_of_dom]%not_elem_of_union & ?); eauto. }
......@@ -149,7 +149,7 @@ Lemma ownI_alloc_open φ P :
Proof.
iIntros (Hfresh) "Hw". iDestruct "Hw" as (I) "[? HI]".
iMod (own_empty (gset_disjUR positive) disabled_name) as "HD".
iMod (own_updateP with "HD") as "HD".
iMod (own_updateP with "[$]") as "HD".
{ apply (gset_disj_alloc_empty_updateP_strong' (λ i, I !! i = None φ i)).
intros E. destruct (Hfresh (E dom _ I))
as (i & [? HIi%not_elem_of_dom]%not_elem_of_union & ?); eauto. }
......
......@@ -131,9 +131,9 @@ Proof.
destruct (to_val e) as [v|] eqn:?.
{ iApply ("HΦ" with ">[-]"). by iApply (fupd_mask_mono E1 _). }
iIntros (σ1) "Hσ". iMod (fupd_intro_mask' E2 E1) as "Hclose"; first done.
iMod ("H" $! σ1 with "Hσ") as "[$ H]".
iMod ("H" with "[$]") as "[$ H]".
iModIntro. iNext. iIntros (e2 σ2 efs Hstep).
iMod ("H" $! _ σ2 efs with "[#]") as "($ & H & $)"; auto.
iMod ("H" with "[//]") as "($ & H & $)"; auto.
iMod "Hclose" as "_". by iApply ("IH" with "HΦ").
Qed.
......@@ -155,10 +155,10 @@ Proof.
{ by iDestruct "H" as ">>> $". }
iIntros (σ1) "Hσ". iMod "H". iMod ("H" $! σ1 with "Hσ") as "[$ H]".
iModIntro. iNext. iIntros (e2 σ2 efs Hstep).
iMod ("H" with "[]") as "(Hphy & H & $)"; first done.
iMod ("H" with "[//]") as "(Hphy & H & $)".
rewrite !wp_unfold /wp_pre. destruct (to_val e2) as [v2|] eqn:He2.
- iDestruct "H" as ">> $". iFrame. eauto.
- iMod ("H" with "Hphy") as "[H _]".
- iDestruct "H" as ">> $". eauto with iFrame.
- iMod ("H" with "[$]") as "[H _]".
iDestruct "H" as %(? & ? & ? & ?). by edestruct (Hatomic _ _ _ _ Hstep).
Qed.
......@@ -167,9 +167,9 @@ Lemma wp_step_fupd E1 E2 e P Φ :
(|={E1,E2}=> P) - WP e @ E2 {{ v, P ={E1}= Φ v }} - WP e @ E1 {{ Φ }}.
Proof.
rewrite !wp_unfold /wp_pre. iIntros (-> ?) "HR H".
iIntros (σ1) "Hσ". iMod "HR". iMod ("H" $! _ with "Hσ") as "[$ H]".
iIntros (σ1) "Hσ". iMod "HR". iMod ("H" with "[$]") as "[$ H]".
iModIntro; iNext; iIntros (e2 σ2 efs Hstep).
iMod ("H" $! e2 σ2 efs with "[%]") as "($ & H & $)"; auto.
iMod ("H" $! e2 σ2 efs with "[% //]") as "($ & H & $)".
iMod "HR". iModIntro. iApply (wp_strong_mono E2); first done.
iSplitR "H"; last iExact "H". iIntros (v) "H". by iApply "H".
Qed.
......@@ -181,11 +181,11 @@ Proof.
destruct (to_val e) as [v|] eqn:He.
{ apply of_to_val in He as <-. by iApply fupd_wp. }
rewrite wp_unfold /wp_pre fill_not_val //.
iIntros (σ1) "Hσ". iMod ("H" $! _ with "Hσ") as "[% H]". iModIntro; iSplit.
iIntros (σ1) "Hσ". iMod ("H" with "[$]") as "[% H]". iModIntro; iSplit.
{ iPureIntro. unfold reducible in *. naive_solver eauto using fill_step. }
iNext; iIntros (e2 σ2 efs Hstep).
destruct (fill_step_inv e σ1 e2 σ2 efs) as (e2'&->&?); auto.
iMod ("H" $! e2' σ2 efs with "[%]") as "($ & H & $)"; auto.
iMod ("H" $! e2' σ2 efs with "[//]") as "($ & H & $)".
by iApply "IH".
Qed.
......
......@@ -573,6 +573,24 @@ Proof.
by rewrite always_if_elim assoc !wand_elim_r.
Qed.
Lemma tac_unlock P Q : (P Q) P locked Q.
Proof. by unlock. Qed.
Lemma tac_specialize_frame Δ Δ' j q R P1 P2 P1' Q Q' :
envs_lookup_delete j Δ = Some (q, R, Δ')
IntoWand R P1 P2
ElimModal P1' P1 Q Q
(Δ' P1' locked Q')
Q' = (P2 - Q)%I
Δ Q.
Proof.
intros [? ->]%envs_lookup_delete_Some ?? HPQ ->.
rewrite envs_lookup_sound //. rewrite HPQ -lock.
rewrite (into_wand R) assoc -(comm _ P1') -assoc always_if_elim.
rewrite -{2}(elim_modal P1' P1 Q Q). apply sep_mono_r, wand_intro_l.
by rewrite assoc !wand_elim_r.
Qed.
Lemma tac_specialize_assert_pure Δ Δ' j q R P1 P2 φ Q :
envs_lookup j Δ = Some (q, R)
IntoWand R P1 P2 FromPure P1 φ
......@@ -643,14 +661,23 @@ Qed.
Lemma tac_assert_persistent Δ Δ1 Δ2 Δ' lr js j P Q :
envs_split lr js Δ = Some (Δ1,Δ2)
envs_app false (Esnoc Enil j P) Δ = Some Δ'
(Δ1 P) PersistentP P
(Δ' Q) Δ Q.
PersistentP P
(Δ1 P) (Δ' Q) Δ Q.
Proof.
intros ?? HP ? <-. rewrite -(idemp uPred_and Δ) {1}envs_split_sound //.
intros ??? HP <-. rewrite -(idemp uPred_and Δ) {1}envs_split_sound //.
rewrite HP sep_elim_l (always_and_sep_l P) envs_app_sound //; simpl.
by rewrite right_id wand_elim_r.
Qed.
Lemma tac_assert_pure Δ Δ' j P φ Q :
envs_app false (Esnoc Enil j P) Δ = Some Δ'
FromPure P φ
φ (Δ' Q) Δ Q.
Proof.
intros ??? <-. rewrite envs_app_sound //; simpl.
by rewrite right_id -(from_pure P) pure_True // -always_impl_wand True_impl.
Qed.
Lemma tac_pose_proof Δ Δ' j P Q :
P
envs_app true (Esnoc Enil j P) Δ = Some Δ'
......
......@@ -15,6 +15,7 @@ Inductive intro_pat :=
| IAlwaysIntro : intro_pat
| IModalIntro : intro_pat
| ISimpl : intro_pat
| IDone : intro_pat
| IForall : intro_pat
| IAll : intro_pat
| IClear : string intro_pat
......@@ -87,6 +88,7 @@ Fixpoint parse_go (ts : list token) (k : stack) : option stack :=
| TAlwaysIntro :: ts => parse_go ts (SPat IAlwaysIntro :: k)
| TModalIntro :: ts => parse_go ts (SPat IModalIntro :: k)
| TSimpl :: ts => parse_go ts (SPat ISimpl :: k)
| TDone :: ts => parse_go ts (SPat IDone :: k)
| TAll :: ts => parse_go ts (SPat IAll :: k)
| TForall :: ts => parse_go ts (SPat IForall :: k)
| TBraceL :: ts => parse_clear ts k
......
......@@ -2,22 +2,31 @@ From stdpp Require Export strings.
From iris.proofmode Require Import tokens.
Set Default Proof Using "Type".
Inductive goal_kind := GSpatial | GModal | GPersistent.
Record spec_goal := SpecGoal {
spec_goal_modal : bool;
spec_goal_kind : goal_kind;
spec_goal_negate : bool;
spec_goal_frame : list string;
spec_goal_hyps : list string
spec_goal_hyps : list string;
spec_goal_done : bool
}.
Inductive spec_pat :=
| SGoal : spec_goal spec_pat
| SGoalPersistent : spec_pat
| SGoalPure : spec_pat
| SForall : spec_pat
| SName : string spec_pat
| SForall : spec_pat.
| SPureGoal : bool spec_pat
| SGoal : spec_goal spec_pat
| SAutoFrame : goal_kind spec_pat.
Definition goal_kind_modal (k : goal_kind) : bool :=
match k with GModal => true | _ => false end.
Definition spec_pat_modal (p : spec_pat) : bool :=
match p with SGoal g => spec_goal_modal g | _ => false end.
match p with
| SGoal g => goal_kind_modal (spec_goal_kind g)
| SAutoFrame k => goal_kind_modal k
| _ => false
end.
Module spec_pat.
Inductive state :=
......@@ -28,30 +37,34 @@ Fixpoint parse_go (ts : list token) (k : list spec_pat) : option (list spec_pat)
match ts with
| [] => Some (reverse k)
| TName s :: ts => parse_go ts (SName s :: k)
| TBracketL :: TAlways :: TBracketR :: ts => parse_go ts (SGoalPersistent :: k)
| TBracketL :: TPure :: TBracketR :: ts => parse_go ts (SGoalPure :: k)
| TBracketL :: ts => parse_goal ts (SpecGoal false false [] []) k
| TModal :: TBracketL :: ts => parse_goal ts (SpecGoal true false [] []) k
| TModal :: ts => parse_go ts (SGoal (SpecGoal true true [] []) :: k)
| TBracketL :: TAlways :: TFrame :: TBracketR :: ts =>
parse_go ts (SAutoFrame GPersistent :: k)
| TBracketL :: TFrame :: TBracketR :: ts =>
parse_go ts (SAutoFrame GSpatial :: k)
| TModal :: TBracketL :: TFrame :: TBracketR :: ts =>
parse_go ts (SAutoFrame GModal :: k)
| TBracketL :: TPure :: TBracketR :: ts => parse_go ts (SPureGoal false :: k)
| TBracketL :: TPure :: TDone :: TBracketR :: ts => parse_go ts (SPureGoal true :: k)
| TBracketL :: TAlways :: ts => parse_goal ts GPersistent false [] [] k
| TBracketL :: ts => parse_goal ts GSpatial false [] [] k
| TModal :: TBracketL :: ts => parse_goal ts GModal false [] [] k
| TModal :: ts => parse_go ts (SGoal (SpecGoal GModal true [] [] false) :: k)
| TForall :: ts => parse_go ts (SForall :: k)
| _ => None
end
with parse_goal (ts : list token) (g : spec_goal)
with parse_goal (ts : list token)
(ki : goal_kind) (neg : bool) (frame hyps : list string)
(k : list spec_pat) : option (list spec_pat) :=
match ts with
| TMinus :: ts =>
guard (¬spec_goal_negate g spec_goal_frame g = [] spec_goal_hyps g = []);
parse_goal ts (SpecGoal (spec_goal_modal g) true
(spec_goal_frame g) (spec_goal_hyps g)) k
| TName s :: ts =>
parse_goal ts (SpecGoal (spec_goal_modal g) (spec_goal_negate g)
(spec_goal_frame g) (s :: spec_goal_hyps g)) k
| TFrame :: TName s :: ts =>
parse_goal ts (SpecGoal (spec_goal_modal g) (spec_goal_negate g)
(s :: spec_goal_frame g) (spec_goal_hyps g)) k
guard (¬neg frame = [] hyps = []);
parse_goal ts ki true frame hyps k
| TName s :: ts => parse_goal ts ki neg frame (s :: hyps) k
| TFrame :: TName s :: ts => parse_goal ts ki neg (s :: frame) hyps k
| TDone :: TBracketR :: ts =>
parse_go ts (SGoal (SpecGoal ki neg (reverse frame) (reverse hyps) true) :: k)
| TBracketR :: ts =>
parse_go ts (SGoal (SpecGoal (spec_goal_modal g) (spec_goal_negate g)
(reverse (spec_goal_frame g)) (reverse (spec_goal_hyps g))) :: k)
parse_go ts (SGoal (SpecGoal ki neg (reverse frame) (reverse hyps) false) :: k)
| _ => None
end.
Definition parse (s : string) : option (list spec_pat) :=
......
This diff is collapsed.
......@@ -20,6 +20,7 @@ Inductive token :=
| TAlwaysIntro : token
| TModalIntro : token
| TSimpl : token
| TDone : token
| TForall : token
| TAll : token
| TMinus : token
......@@ -46,6 +47,9 @@ Fixpoint tokenize_go (s : string) (k : list token) (kn : string) : list token :=
| String "!" (String "%" s) => tokenize_go s (TPureIntro :: cons_name kn k) ""
| String "!" (String "#" s) => tokenize_go s (TAlwaysIntro :: cons_name kn k) ""
| String "!" (String ">" s) => tokenize_go s (TModalIntro :: cons_name kn k) ""
| String "/" (String "/" (String "=" s)) =>
tokenize_go s (TSimpl :: TDone :: cons_name kn k) ""
| String "/" (String "/" s) => tokenize_go s (TDone :: cons_name kn k) ""
| String "/" (String "=" s) => tokenize_go s (TSimpl :: cons_name kn k) ""
| String "*" (String "*" s) => tokenize_go s (TAll :: cons_name kn k) ""
| String "*" s => tokenize_go s (TForall :: cons_name kn k) ""
......
......@@ -32,7 +32,7 @@ Proof.
iIntros "{$Hac $Ha}".
iExists (S j + z1), z2.
iNext.
iApply ("H3" $! _ 0 with "H1 []").
iApply ("H3" $! _ 0 with "[$]").
- iSplit. done. iApply "H2". iLeft. iApply "H2". by iRight.
- done.
Qed.
......@@ -63,14 +63,14 @@ Definition foo {M} (P : uPred M) := (P → P)%I.
Definition bar {M} : uPred M := ( P, foo P)%I.
Lemma demo_4 (M : ucmraT) : True - @bar M.
Proof. iIntros. iIntros (P) "HP". done. Qed.
Proof. iIntros. iIntros (P) "HP //". Qed.
Lemma demo_5 (M : ucmraT) (x y : M) (P : uPred M) :
( z, P z y) - (P - (x,x) (y,x)).
Proof.
iIntros "H1 H2".
iRewrite (uPred.internal_eq_sym x x with "[#]"); first done.
iRewrite -("H1" $! _ with "[-]"); first done.
iRewrite (uPred.internal_eq_sym x x with "[# //]").
iRewrite -("H1" $! _ with "[- //]").
done.
Qed.
......@@ -80,7 +80,7 @@ Lemma demo_6 (M : ucmraT) (P Q : uPred M) :
Proof.
iIntros (a) "*".
iIntros "#Hfoo **".
by iIntros "# _".
iIntros "# _ //".
Qed.
Lemma demo_7 (M : ucmraT) (P Q1 Q2 : uPred M) : P (Q1 Q2) - P Q1.
......@@ -96,10 +96,8 @@ Section iris.
(True - P - inv N Q - True - R) - P - Q ={E}= R.
Proof.
iIntros (?) "H HP HQ".
iApply ("H" with "[#] HP >[HQ] >").
- done.
- by iApply inv_alloc.
- done.
iApply ("H" with "[% //] HP >[HQ] >[//]").
by iApply inv_alloc.
Qed.
End iris.
......@@ -119,7 +117,7 @@ Qed.
Lemma demo_11 (M : ucmraT) (P Q R : uPred M) :
(P - True - True - Q - R) - P - Q - R.
Proof. iIntros "H HP HQ". by iApply ("H" with "[HP]"). Qed.
Proof. iIntros "H HP HQ". by iApply ("H" with "[$]"). Qed.
(* Check coercions *)
Lemma demo_12 (M : ucmraT) (P : Z uPred M) : ( x, P x) - x, P x.
......
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