Commit 9835899b authored by Robbert Krebbers's avatar Robbert Krebbers

Syntax `iAssert (Q with spat) as ...` which is consistent with `with`s elsewhere.

parent 50d85ae3
......@@ -43,7 +43,7 @@ Context management
eliminates it. This tactic is essentially the same as `iDestruct` with the
difference that when `pm_trm` is a non-universally quantified spatial
hypothesis, it will not throw the hypothesis away.
- `iAssert P with "spat" as "ipat"` : generates a new subgoal `P` and adds the
- `iAssert (P with "spat") as "ipat"` : generates a new subgoal `P` and adds the
hypothesis `P` to the current goal. The specialization pattern `spat`
specifies which hypotheses will be consumed by proving `P`. The introduction
pattern `ipat` specifies how to eliminate `P`.
......
......@@ -225,9 +225,9 @@ Lemma box_empty E f P :
box N f P ={E}= P box N (const false <$> f) P.
Proof.
iDestruct 1 as (Φ) "[#HeqP Hf]".
iAssert (([ map] γ↦b f, Φ γ)
iAssert ((([ map] γ↦b f, Φ γ)
[ map] γ↦b f, box_own_auth γ ( Excl' false) box_own_prop γ (Φ γ)
inv N (slice_inv γ (Φ γ)))%I with "[> Hf]" as "[HΦ ?]".
inv N (slice_inv γ (Φ γ)))%I with "[> Hf]") as "[HΦ ?]".
{ rewrite -big_opM_opM -fupd_big_sepM. iApply (@big_sepM_impl with "[$Hf]").
iIntros "!#" (γ b ?) "(Hγ' & #HγΦ & #Hinv)".
assert (true = b) as <- by eauto.
......
......@@ -39,6 +39,6 @@ Proof.
{ by iMod ("HQP" with "HQ [$]") as "(_ & _ & HP)". }
iMod "HP". iFrame. auto.
- rewrite uPred_fupd_eq /uPred_fupd_def. iIntros (E P ?) "HP [Hw HE]".
iAssert ( P)%I with "[-]" as "#$"; last by iFrame.
iAssert (( P)%I with "[-]") as "#$"; last by iFrame.
iNext. by iMod ("HP" with "[$]") as "(_ & _ & HP)".
Qed.
......@@ -56,8 +56,8 @@ Proof.
rewrite inv_eq /inv_def uPred_fupd_eq. iIntros (Sub) "[Hw HE]".
iMod (ownI_alloc_open ( (N : coPset)) P with "Hw")
as (i ?) "(Hw & #Hi & HD)"; auto using fresh_inv_name.
iAssert (ownE {[i]} ownE ( N {[i]}) ownE (E N))%I
with "[HE]" as "(HEi & HEN\i & HE\N)".
iAssert ((ownE {[i]} ownE ( N {[i]}) ownE (E N))%I
with "[HE]") as "(HEi & HEN\i & HE\N)".
{ rewrite -?ownE_op; [|set_solver..].
rewrite assoc_L -!union_difference_L //. set_solver. }
do 2 iModIntro. iFrame "HE\N". iSplitL "Hw HEi"; first by iApply "Hw".
......
......@@ -159,7 +159,7 @@ Module inv. Section inv.
Proof.
iIntros "(#HsP & #HsQ & #HP)". iDestruct "HsP" as (i) "HiP".
iApply (inv_open' i). iSplit; first done.
iIntros "HaP". iAssert (fupd M0 (finished γ)) with "[HaP]" as "> Hf".
iIntros "HaP". iAssert (fupd M0 (finished γ) with "[HaP]") as "> Hf".
{ iDestruct "HaP" as "[Hs | [Hf _]]".
- by iApply start_finish.
- by iApply fupd_intro. }
......
......@@ -71,7 +71,7 @@ Proof.
iModIntro. rewrite -{2}(left_id_L [] (++) (e2 :: _)). iApply "IH2".
by setoid_rewrite (right_id_L [] (++)).
+ iMod ("IH1" with "[%] Hσ1") as "[$ [IH1 _]]"; first by econstructor.
iAssert (twptp t2) with "[IH2]" as "Ht2".
iAssert (twptp t2 with "[IH2]") as "Ht2".
{ rewrite twptp_unfold. iApply (twptp_pre_mono with "[] IH2").
iIntros "!# * [_ ?] //". }
iModIntro. rewrite -assoc_L (comm _ t2) !cons_middle !assoc_L.
......
......@@ -1681,13 +1681,28 @@ Tactic Notation "iLöb" "as" constr (IH) "forall" "(" ident(x1) ident(x2)
iLöbRevert Hs with (iRevertIntros(x1 x2 x3 x4 x5 x6 x7 x8) "" with (iLöbCore as IH)).
(** * Assert *)
(* The argument [p] denotes whether [Q] is persistent. It can either be a
Boolean or an introduction pattern, which will be coerced into [true] if it
only contains `#` or `%` patterns at the top-level, and [false] otherwise. *)
Tactic Notation "iAssertCore" open_constr(Q)
"with" constr(Hs) "as" constr(p) tactic(tac) :=
(* The argument [p] denotes whether the asserted proposition is persistent. It
can either be a Boolean or an introduction pattern, which will be coerced into
[true] if it only contains `#` or `%` patterns at the top-level, and [false]
otherwise. *)
Tactic Notation "iAssertCore" open_constr(t) "as" constr(p) tactic(tac) :=
iStartProof;
let pats := spec_pat.parse Hs in
lazymatch t with
| ITrm _ (hcons _ _) _ => fail "iAssert: $! not supposed"
| _ => idtac
end;
let Q :=
lazymatch t with ITrm ?Q _ _ => Q | _ => t end in
let pats :=
lazymatch t with
| ITrm _ _ ?pats => spec_pat.parse pats
| _ =>
let p := intro_pat_persistent p in
lazymatch p with
| true => constr:([SGoal (SpecGoal GPersistent false [] [] false)])
| false => constr:([SGoal (SpecGoal GSpatial false [] [] false)])
end
end in
lazymatch pats with
| [_] => idtac
| _ => fail "iAssert: exactly one specialization pattern should be given"
......@@ -1697,30 +1712,6 @@ Tactic Notation "iAssertCore" open_constr(Q)
[env_reflexivity
|iSpecializeCore H with hnil pats as p; [..|tac H]].
Tactic Notation "iAssertCore" open_constr(Q) "as" constr(p) tactic(tac) :=
let p := intro_pat_persistent p in
lazymatch p with
| true => iAssertCore Q with "[#]" as p tac
| false => iAssertCore Q with "[]" as p tac
end.
Tactic Notation "iAssert" open_constr(Q) "with" constr(Hs) "as" constr(pat) :=
iAssertCore Q with Hs as pat (fun H => iDestructHyp H as pat).
Tactic Notation "iAssert" open_constr(Q) "with" constr(Hs) "as"
"(" simple_intropattern(x1) ")" constr(pat) :=
iAssertCore Q with Hs as pat (fun H => iDestructHyp H as (x1) pat).
Tactic Notation "iAssert" open_constr(Q) "with" constr(Hs) "as"
"(" simple_intropattern(x1) simple_intropattern(x2) ")" constr(pat) :=
iAssertCore Q with Hs as pat (fun H => iDestructHyp H as (x1 x2) pat).
Tactic Notation "iAssert" open_constr(Q) "with" constr(Hs) "as"
"(" simple_intropattern(x1) simple_intropattern(x2) simple_intropattern(x3)
")" constr(pat) :=
iAssertCore Q with Hs as pat (fun H => iDestructHyp H as (x1 x2 x3) pat).
Tactic Notation "iAssert" open_constr(Q) "with" constr(Hs) "as"
"(" simple_intropattern(x1) simple_intropattern(x2) simple_intropattern(x3)
simple_intropattern(x4) ")" constr(pat) :=
iAssertCore Q with Hs as pat (fun H => iDestructHyp H as (x1 x2 x3 x4) pat).
Tactic Notation "iAssert" open_constr(Q) "as" constr(pat) :=
iAssertCore Q as pat (fun H => iDestructHyp H as pat).
Tactic Notation "iAssert" open_constr(Q) "as"
......@@ -1738,11 +1729,8 @@ Tactic Notation "iAssert" open_constr(Q) "as"
simple_intropattern(x4) ")" constr(pat) :=
iAssertCore Q as pat (fun H => iDestructHyp H as (x1 x2 x3 x4) pat).
Tactic Notation "iAssert" open_constr(Q) "with" constr(Hs)
"as" "%" simple_intropattern(pat) :=
iAssertCore Q with Hs as true (fun H => iPure H as pat).
Tactic Notation "iAssert" open_constr(Q) "as" "%" simple_intropattern(pat) :=
iAssert Q with "[-]" as %pat.
iAssertCore Q as true (fun H => iPure H as pat).
(** * Rewrite *)
Local Ltac iRewriteFindPred :=
......
......@@ -58,14 +58,14 @@ Proof.
rewrite /one_shot_inv; eauto 10.
- iIntros "!# /=". wp_seq. wp_bind (! _)%E.
iInv N as ">Hγ" "Hclose".
iAssert ( v, l v ((v = NONEV own γ Pending)
n : Z, v = SOMEV #n own γ (Shot n)))%I with "[Hγ]" as "Hv".
iAssert (( v, l v ((v = NONEV own γ Pending)
n : Z, v = SOMEV #n own γ (Shot n)))%I with "[Hγ]") as "Hv".
{ iDestruct "Hγ" as "[[Hl Hγ]|Hl]"; last iDestruct "Hl" as (m) "[Hl Hγ]".
+ iExists NONEV. iFrame. eauto.
+ iExists (SOMEV #m). iFrame. eauto. }
iDestruct "Hv" as (v) "[Hl Hv]". wp_load.
iAssert (one_shot_inv γ l (v = NONEV n : Z,
v = SOMEV #n own γ (Shot n)))%I with "[Hl Hv]" as "[Hinv #Hv]".
iAssert ((one_shot_inv γ l (v = NONEV n : Z,
v = SOMEV #n own γ (Shot n)))%I with "[Hl Hv]") as "[Hinv #Hv]".
{ iDestruct "Hv" as "[[% ?]|Hv]"; last iDestruct "Hv" as (m) "[% ?]"; subst.
+ iSplit. iLeft; by iSplitL "Hl". eauto.
+ iSplit. iRight; iExists m; by iSplitL "Hl". eauto. }
......
......@@ -88,9 +88,9 @@ Lemma test_iAssert_persistent P Q : P -∗ Q -∗ True.
Proof.
iIntros "HP HQ".
iAssert True%I as "#_". { by iClear "HP HQ". }
iAssert True%I with "[HP]" as "#_". { Fail iClear "HQ". by iClear "HP". }
iAssert (True%I with "[HP]") as "#_". { Fail iClear "HQ". by iClear "HP". }
iAssert True%I as %_. { by iClear "HP HQ". }
iAssert True%I with "[HP]" as %_. { Fail iClear "HQ". by iClear "HP". }
iAssert (True%I with "[HP]") as %_. { Fail iClear "HQ". by iClear "HP". }
done.
Qed.
......@@ -119,7 +119,7 @@ Proof. iIntros (Hv) "#Hxy". iFrame (Hv) "Hxy". Qed.
Lemma test_iAssert_modality P : False - P.
Proof.
iIntros "HF".
iAssert (bi_affinely False)%I with "[> -]" as %[].
iAssert (bi_affinely False with "[> -]") as %[].
by iMod "HF".
Qed.
......@@ -309,9 +309,8 @@ Qed.
Lemma test_assert_affine_pure (φ : Prop) P :
φ P P bi_affinely ⌜φ⌝.
Proof. iIntros (Hφ). iAssert (bi_affinely ⌜φ⌝) with "[%]" as "$"; auto. Qed.
Proof. iIntros (Hφ). iAssert (bi_affinely ⌜φ⌝ with "[%]") as "$"; auto. Qed.
Lemma test_assert_pure (φ : Prop) P :
φ P P ⌜φ⌝.
Proof. iIntros (Hφ). iAssert ⌜φ⌝%I with "[%]" as "$"; auto. Qed.
Proof. iIntros (Hφ). iAssert (⌜φ⌝%I with "[%]") as "$"; auto. Qed.
End tests.
......@@ -20,7 +20,7 @@ Section base_logic_tests.
iDestruct "H1" as (z1 z2 c) "(H1&_&#Hc)".
iPoseProof "Hc" as "foo".
iRevert (a b) "Ha Hb". iIntros (b a) "Hb {foo} Ha".
iAssert (uPred_ownM (a core a)) with "[Ha]" as "[Ha #Hac]".
iAssert (uPred_ownM (a core a) with "[Ha]") as "[Ha #Hac]".
{ by rewrite cmra_core_r. }
iIntros "{$Hac $Ha}".
iExists (S j + z1), z2.
......@@ -35,7 +35,7 @@ Section base_logic_tests.
Proof. iIntros (Hv) "Hxy". by iFrame (Hv) "Hxy". Qed.
Lemma test_iAssert_modality P : (|==> False) - |==> P.
Proof. iIntros. iAssert False%I with "[> - //]" as %[]. Qed.
Proof. iIntros. iAssert (False%I with "[> - //]") as %[]. Qed.
Lemma test_iStartProof_1 P : P - P.
Proof. iStartProof. iStartProof. iIntros "$". 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