Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coq

ProofMode.md

@@ -225,8 +225,7 @@ _specification patterns_ to express splitting of hypotheses:
   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.
-- `[-H1 ... Hn]`  : negated form of the above pattern. This pattern does not
-  accept hypotheses prefixed with a `$`.
+- `[-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
   for the premise will be wrapped into the modality.

heap_lang/lib/assert.v

@@ -13,6 +13,5 @@ Lemma wp_assert `{heapG Σ} E (Φ : val → iProp Σ) e `{!Closed [] e} :
   WP e @ E {{ v, v = #true ∧ ▷ Φ #() }} ⊢ WP assert: e @ E {{ Φ }}.
 Proof.
   iIntros "HΦ". rewrite /assert. wp_let. wp_seq.
-  iApply wp_wand_r; iFrame "HΦ"; iIntros (v) "[% ?]"; subst.
-  wp_if. done.
+  iApply (wp_wand_r with "[- $HΦ]"). iIntros (v) "[% ?]"; subst. by wp_if.
 Qed.

heap_lang/lib/par.v

@@ -24,10 +24,10 @@ Lemma par_spec (Ψ1 Ψ2 : val → iProp Σ) e (f1 f2 : val) (Φ : val → iProp
 Proof.
   iIntros (?) "(#Hh&Hf1&Hf2&HΦ)".
   rewrite /par. wp_value. iModIntro. wp_let. wp_proj.
-  wp_apply (spawn_spec parN); try wp_done; try solve_ndisj; iFrame "Hf1 Hh".
-  iNext. iIntros (l) "Hl". wp_let. wp_proj. wp_bind (f2 _).
-  iApply wp_wand_l; iFrame "Hf2"; iIntros (v) "H2". wp_let.
-  wp_apply join_spec; iFrame "Hl". iNext. iIntros (w) "H1".
+  wp_apply (spawn_spec parN with "[- $Hh $Hf1]"); try wp_done; try solve_ndisj.
+  iIntros (l) "Hl". wp_let. wp_proj. wp_bind (f2 _).
+  iApply (wp_wand_r with "[- $Hf2]"); iIntros (v) "H2". wp_let.
+  wp_apply (join_spec with "[- $Hl]"). iIntros (w) "H1".
   iSpecialize ("HΦ" with "* [-]"); first by iSplitL "H1". by wp_let.
 Qed.
 
@@ -37,7 +37,7 @@ Lemma wp_par (Ψ1 Ψ2 : val → iProp Σ)
    ∀ v1 v2, Ψ1 v1 ★ Ψ2 v2 -★ ▷ Φ (v1,v2)%V)
   ⊢ WP e1 || e2 {{ Φ }}.
 Proof.
-  iIntros "(#Hh&H1&H2&H)". iApply (par_spec Ψ1 Ψ2); try wp_done.
-  iFrame "Hh H". iSplitL "H1"; by wp_let.
+  iIntros "(#Hh&H1&H2&H)". iApply (par_spec Ψ1 Ψ2 with "[- $Hh $H]"); try wp_done.
+  iSplitL "H1"; by wp_let.
 Qed.
 End proof.

heap_lang/lib/spawn.v

@@ -58,7 +58,7 @@ Proof.
   { iNext. iExists NONEV. iFrame; eauto. }
   wp_apply wp_fork; simpl. iSplitR "Hf".
   - iModIntro. wp_seq. iModIntro. iApply "HΦ". rewrite /join_handle. eauto.
-  - wp_bind (f _). iApply wp_wand_l. iFrame "Hf"; iIntros (v) "Hv".
+  - wp_bind (f _). iApply (wp_wand_r with "[ $Hf]"); iIntros (v) "Hv".
     iInv N as (v') "[Hl _]" "Hclose".
     wp_store. iApply "Hclose". iNext. iExists (SOMEV v). iFrame. eauto.
 Qed.

heap_lang/lib/spin_lock.v

@@ -73,8 +73,8 @@ Section proof.
   Lemma acquire_spec γ lk R :
     {{{ is_lock γ lk R }}} acquire lk {{{; #(), locked γ ★ R }}}.
   Proof.
-    iIntros (Φ) "[#Hl HΦ]". iLöb as "IH". wp_rec. wp_bind (try_acquire _).
-    iApply try_acquire_spec. iFrame "#". iSplit.
+    iIntros (Φ) "[#Hl HΦ]". iLöb as "IH". wp_rec.
+    wp_apply (try_acquire_spec with "[- $Hl]"). iSplit.
     - iIntros "Hlked HR". wp_if. iModIntro. iApply "HΦ"; iFrame.
     - wp_if. iApply ("IH" with "[HΦ]"). auto.
   Qed.
@@ -87,7 +87,6 @@ Section proof.
     rewrite /release /=. wp_let. iInv N as (b) "[Hl _]" "Hclose".
     wp_store. iApply "HΦ". iApply "Hclose". iNext. iExists false. by iFrame.
   Qed.
-
 End proof.
 
 Definition spin_lock `{!heapG Σ, !lockG Σ} : lock Σ :=

proofmode/spec_patterns.v

@@ -71,7 +71,6 @@ with parse_goal (ts : list token) (g : spec_goal)
      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 =>
-    guard (¬spec_goal_negate g);
      parse_goal ts (SpecGoal (spec_goal_modal g) (spec_goal_negate g)
        (s :: spec_goal_frame g) (spec_goal_hyps g)) k
   | TBracketR :: ts =>

proofmode/tactics.v

@@ -308,7 +308,8 @@ Local Tactic Notation "iSpecializePat" constr(H) constr(pat) :=
          |(*goal*)
          |go H1 pats]
     | SGoal (SpecGoal ?m ?lr ?Hs_frame ?Hs) :: ?pats =>
-       eapply tac_specialize_assert with _ _ _ H1 _ lr (Hs_frame ++ Hs) _ _ _ _;
+       let Hs' := eval cbv in (if lr then Hs else Hs_frame ++ Hs) in
+       eapply tac_specialize_assert with _ _ _ H1 _ lr Hs' _ _ _ _;
          [env_cbv; reflexivity || fail "iSpecialize:" H1 "not found"
          |solve_to_wand H1
          |match m with
@@ -1084,7 +1085,8 @@ Tactic Notation "iAssertCore" open_constr(Q) "with" constr(Hs) "as" tactic(tac)
        |apply _ || fail "iAssert:" Q "not persistent"
        |tac H]
   | [SGoal (SpecGoal ?m ?lr ?Hs_frame ?Hs)] =>
-     eapply tac_assert with _ _ _ lr (Hs_frame ++ Hs) H Q _;
+     let Hs' := eval cbv in (if lr then Hs else Hs_frame ++ Hs) in
+     eapply tac_assert with _ _ _ lr Hs' H Q _;
        [match m with
         | false => apply elim_modal_dummy
         | true => apply _ || fail "iAssert: goal not a modality"

tests/barrier_client.v

@@ -29,28 +29,26 @@ Section client.
     heap_ctx ★ recv N b (y_inv q y) ⊢ WP worker n #b #y {{ _, True }}.
   Proof.
     iIntros "[#Hh Hrecv]". wp_lam. wp_let.
-    wp_apply wait_spec; iFrame "Hrecv".
-    iNext. iDestruct 1 as (f) "[Hy #Hf]".
+    wp_apply (wait_spec with "[- $Hrecv]"). iDestruct 1 as (f) "[Hy #Hf]".
     wp_seq. wp_load.
-    iApply wp_wand_r; iSplitR; [iApply "Hf"|by iIntros (v) "_"].
+    iApply wp_wand_r. iSplitR; [iApply "Hf"|by iIntros (v) "_"].
   Qed.
 
   Lemma client_safe : heapN ⊥ N → heap_ctx ⊢ WP client {{ _, True }}.
   Proof.
     iIntros (?) "#Hh"; rewrite /client. wp_alloc y as "Hy". wp_let.
-    wp_apply (newbarrier_spec N (y_inv 1 y)); first done.
-    iFrame "Hh". iNext. iIntros (l) "[Hr Hs]". wp_let.
-    iApply (wp_par (λ _, True%I) (λ _, True%I)). iFrame "Hh".
-    iSplitL "Hy Hs".
+    wp_apply (newbarrier_spec N (y_inv 1 y) with "[- $Hh]"); first done.
+    iIntros (l) "[Hr Hs]". wp_let.
+    iApply (wp_par (λ _, True%I) (λ _, True%I) with "[-$Hh]"). iSplitL "Hy Hs".
     - (* The original thread, the sender. *)
-      wp_store. iApply signal_spec; iFrame "Hs"; iSplitL "Hy"; [|by eauto].
+      wp_store. iApply (signal_spec with "[- $Hs]"). iSplitL "Hy"; [|by eauto].
       iExists _; iSplitL; [done|]. iAlways; iIntros (n). wp_let. by wp_op.
     - (* The two spawned threads, the waiters. *)
       iSplitL; [|by iIntros (_ _) "_ !>"].
       iDestruct (recv_weaken with "[] Hr") as "Hr".
       { iIntros "Hy". by iApply (y_inv_split with "Hy"). }
       iMod (recv_split with "Hr") as "[H1 H2]"; first done.
-      iApply (wp_par (λ _, True%I) (λ _, True%I)). iFrame "Hh".
+      iApply (wp_par (λ _, True%I) (λ _, True%I) with "[- $Hh]").
       iSplitL "H1"; [|iSplitL "H2"; [|by iIntros (_ _) "_ !>"]];
         iApply worker_safe; by iSplit.
 Qed.

tests/joining_existentials.v

@@ -35,8 +35,8 @@ Lemma worker_spec e γ l (Φ Ψ : X → iProp Σ) `{!Closed [] e} :
   recv N l (barrier_res γ Φ) ★ (∀ x, {{ Φ x }} e {{ _, Ψ x }})
   ⊢ WP wait #l ;; e {{ _, barrier_res γ Ψ }}.
 Proof.
-  iIntros "[Hl #He]". wp_apply wait_spec; simpl; iFrame "Hl".
-  iNext. iDestruct 1 as (x) "[#Hγ Hx]".
+  iIntros "[Hl #He]". wp_apply (wait_spec with "[- $Hl]"); simpl.
+  iDestruct 1 as (x) "[#Hγ Hx]".
   wp_seq. iApply wp_wand_l. iSplitR; [|by iApply "He"].
   iIntros (v) "?"; iExists x; by iSplit.
 Qed.
@@ -76,21 +76,21 @@ Lemma client_spec_new eM eW1 eW2 `{!Closed [] eM, !Closed [] eW1, !Closed [] eW2
 Proof.
   iIntros (HN) "/= (#Hh&HP&#He&#He1&#He2)"; rewrite /client.
   iMod (own_alloc (Pending : one_shotR Σ F)) as (γ) "Hγ"; first done.
-  wp_apply (newbarrier_spec N (barrier_res γ Φ)); auto.
-  iFrame "Hh". iNext. iIntros (l) "[Hr Hs]".
+  wp_apply (newbarrier_spec N (barrier_res γ Φ) with "[- $Hh]"); auto.
+  iIntros (l) "[Hr Hs]".
   set (workers_post (v : val) := (barrier_res γ Ψ1 ★ barrier_res γ Ψ2)%I).
-  wp_let. wp_apply (wp_par  (λ _, True)%I workers_post); iFrame "Hh".
+  wp_let. wp_apply (wp_par  (λ _, True)%I workers_post with "[- $Hh]").
   iSplitL "HP Hs Hγ"; [|iSplitL "Hr"].
   - wp_bind eM. iApply wp_wand_l; iSplitR "HP"; [|by iApply "He"].
     iIntros (v) "HP"; iDestruct "HP" as (x) "HP". wp_let.
     iMod (own_update with "Hγ") as "Hx".
     { by apply (cmra_update_exclusive (Shot x)). }
-    iApply signal_spec; iFrame "Hs"; iSplitR ""; last auto.
+    iApply (signal_spec with "[- $Hs]"). iSplitR ""; last auto.
     iExists x; auto.
   - iDestruct (recv_weaken with "[] Hr") as "Hr"; first by iApply P_res_split.
     iMod (recv_split with "Hr") as "[H1 H2]"; first done.
     wp_apply (wp_par (λ _, barrier_res γ Ψ1)%I
-                     (λ _, barrier_res γ Ψ2)%I); iFrame "Hh".
+                     (λ _, barrier_res γ Ψ2)%I with "[-$Hh]").
     iSplitL "H1"; [|iSplitL "H2"].
     + iApply worker_spec; auto.
     + iApply worker_spec; auto.

tests/list_reverse.v

@@ -47,7 +47,7 @@ Lemma rev_wp hd xs (Φ : val → iProp Σ) :
   ⊢ WP rev hd (InjL #()) {{ Φ }}.
 Proof.
   iIntros "(#Hh & Hxs & HΦ)".
-  iApply (rev_acc_wp hd NONEV xs []); iFrame "Hh Hxs".
+  iApply (rev_acc_wp hd NONEV xs [] with "[- $Hh $Hxs]").
   iSplit; first done. iIntros (w). rewrite right_id_L. iApply "HΦ".
 Qed.
 End list_reverse.

tests/one_shot.v

@@ -94,6 +94,6 @@ Proof.
   iIntros (f1 f2) "[#Hf1 #Hf2]"; iSplit.
   - iIntros (n) "!# _". wp_proj. iApply "Hf1".
   - iIntros "!# _". wp_proj.
-    iApply wp_wand_l; iFrame "Hf2". by iIntros (v) "#? !# _".
+    iApply (wp_wand_r with "[- $Hf2]"). by iIntros (v) "#? !# _".
 Qed.
 End proof.

tests/tree_sum.v

@@ -62,7 +62,7 @@ Lemma sum_wp `{!heapG Σ} v t Φ :
 Proof.
   iIntros "(#Hh & Ht & HΦ)". rewrite /sum' /=.
   wp_let. wp_alloc l as "Hl". wp_let.
-  wp_apply sum_loop_wp; iFrame "Hh Ht Hl".
+  wp_apply (sum_loop_wp with "[- $Hh $Ht $Hl]").
   rewrite Z.add_0_r.
   iIntros "Hl Ht". wp_seq. wp_load. by iApply "HΦ".
 Qed.