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

theories/heap_lang/proofmode.v

@@ -77,6 +77,7 @@ Qed.
 End heap.
 
 Tactic Notation "wp_apply" open_constr(lem) :=
+  iStartProof;
   lazymatch goal with
   | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
     wp_bind_core K; iApply lem; try iNext)
@@ -84,6 +85,7 @@ Tactic Notation "wp_apply" open_constr(lem) :=
   end.
 
 Tactic Notation "wp_alloc" ident(l) "as" constr(H) :=
+  iStartProof;
   lazymatch goal with
   | |- _ ⊢ wp ?E ?e ?Q =>
     first
@@ -105,6 +107,7 @@ Tactic Notation "wp_alloc" ident(l) :=
   let H := iFresh in wp_alloc l as H.
 
 Tactic Notation "wp_load" :=
+  iStartProof;
   lazymatch goal with
   | |- _ ⊢ wp ?E ?e ?Q =>
     first
@@ -120,6 +123,7 @@ Tactic Notation "wp_load" :=
   end.
 
 Tactic Notation "wp_store" :=
+  iStartProof;
   lazymatch goal with
   | |- _ ⊢ wp ?E ?e ?Q =>
     first
@@ -138,6 +142,7 @@ Tactic Notation "wp_store" :=
   end.
 
 Tactic Notation "wp_cas_fail" :=
+  iStartProof;
   lazymatch goal with
   | |- _ ⊢ wp ?E ?e ?Q =>
     first
@@ -158,6 +163,7 @@ Tactic Notation "wp_cas_fail" :=
   end.
 
 Tactic Notation "wp_cas_suc" :=
+  iStartProof;
   lazymatch goal with
   | |- _ ⊢ wp ?E ?e ?Q =>
     first

theories/program_logic/gen_heap.v

@@ -68,6 +68,9 @@ Section gen_heap.
   Lemma to_gen_heap_insert l v σ :
     to_gen_heap (<[l:=v]> σ) = <[l:=(1%Qp, to_agree (v:leibnizC V))]> (to_gen_heap σ).
   Proof. by rewrite /to_gen_heap fmap_insert. Qed.
+  Lemma to_gen_heap_delete l σ :
+    to_gen_heap (delete l σ) = delete l (to_gen_heap σ).
+  Proof. by rewrite /to_gen_heap fmap_delete. Qed.
 
   (** General properties of mapsto *)
   Global Instance mapsto_timeless l q v : TimelessP (l ↦{q} v).
@@ -121,6 +124,14 @@ Section gen_heap.
     iModIntro. rewrite to_gen_heap_insert. iFrame.
   Qed.
 
+  Lemma gen_heap_dealloc σ l v :
+    gen_heap_ctx σ -∗ l ↦ v ==∗ gen_heap_ctx (delete l σ).
+  Proof.
+    iIntros "Hσ Hl". rewrite /gen_heap_ctx mapsto_eq /mapsto_def.
+    rewrite to_gen_heap_delete. iApply (own_update_2 with "Hσ Hl").
+    eapply auth_update_dealloc, (delete_singleton_local_update _ _ _).
+  Qed.
+
   Lemma gen_heap_valid σ l q v : gen_heap_ctx σ -∗ l ↦{q} v -∗ ⌜σ !! l = Some v⌝.
   Proof.
     iIntros "Hσ Hl". rewrite /gen_heap_ctx mapsto_eq /mapsto_def.

theories/proofmode/tactics.v

@@ -42,16 +42,17 @@ Tactic Notation "iMatchHyp" tactic1(tac) :=
   end.
 
 (** * Start a proof *)
-Tactic Notation "iProof" :=
+Ltac iStartProof :=
   lazymatch goal with
-  | |- of_envs _ ⊢ _ => fail "iProof: already in Iris proofmode"
+  | |- of_envs _ ⊢ _ => idtac
   | |- ?P =>
-    match eval hnf in P with
+    lazymatch eval hnf in P with
     (* need to use the unfolded version of [uPred_valid] due to the hnf *)
     | True ⊢ _ => apply tac_adequate
     | _ ⊢ _ => apply uPred.wand_entails, tac_adequate
     (* need to use the unfolded version of [⊣⊢] due to the hnf *)
     | uPred_equiv' _ _ => apply uPred.iff_equiv, tac_adequate
+    | _ => fail "iStartProof: not a uPred"
     end
   end.
 
@@ -389,6 +390,7 @@ Tactic Notation "iIntoValid" open_constr(t) :=
 Tactic Notation "iPoseProofCore" open_constr(lem) "as" constr(p) tactic(tac) :=
   let pose_trm t tac :=
     let Htmp := iFresh in
+    iStartProof;
     lazymatch type of t with
     | string =>
        eapply tac_pose_proof_hyp with _ _ t _ Htmp _;
@@ -506,10 +508,12 @@ Tactic Notation "iRevert" "(" ident(x1) ident(x2) ident(x3) ident(x4)
 
 (** * Disjunction *)
 Tactic Notation "iLeft" :=
+  iStartProof;
   eapply tac_or_l;
     [let P := match goal with |- FromOr ?P _ _ => P end in
      apply _ || fail "iLeft:" P "not a disjunction"|].
 Tactic Notation "iRight" :=
+  iStartProof;
   eapply tac_or_r;
     [let P := match goal with |- FromOr ?P _ _ => P end in
      apply _ || fail "iRight:" P "not a disjunction"|].
@@ -524,7 +528,7 @@ Local Tactic Notation "iOrDestruct" constr(H) "as" constr(H1) constr(H2) :=
 
 (** * Conjunction and separating conjunction *)
 Tactic Notation "iSplit" :=
-  try iProof;
+  iStartProof;
   lazymatch goal with
   | |- _ ⊢ _ =>
     eapply tac_and_split;
@@ -533,6 +537,7 @@ Tactic Notation "iSplit" :=
   end.
 
 Tactic Notation "iSplitL" constr(Hs) :=
+  iStartProof;
   let Hs := words Hs in
   eapply tac_sep_split with _ _ false Hs _ _; (* (js:=Hs) *)
     [let P := match goal with |- FromSep ?P _ _ => P end in
@@ -540,6 +545,7 @@ Tactic Notation "iSplitL" constr(Hs) :=
     |env_cbv; reflexivity || fail "iSplitL: hypotheses" Hs
                                   "not found in the context"| |].
 Tactic Notation "iSplitR" constr(Hs) :=
+  iStartProof;
   let Hs := words Hs in
   eapply tac_sep_split with _ _ true Hs _ _; (* (js:=Hs) *)
     [let P := match goal with |- FromSep ?P _ _ => P end in
@@ -575,6 +581,7 @@ Tactic Notation "iCombine" constr(H1) constr(H2) "as" constr(H) :=
 
 (** * Existential *)
 Tactic Notation "iExists" uconstr(x1) :=
+  iStartProof;
   eapply tac_exist;
     [let P := match goal with |- FromExist ?P _ => P end in
      apply _ || fail "iExists:" P "not an existential"
@@ -614,11 +621,13 @@ Local Tactic Notation "iExistDestruct" constr(H)
 
 (** * Always *)
 Tactic Notation "iAlways":=
+  iStartProof;
   apply tac_always_intro;
     [reflexivity || fail "iAlways: spatial context non-empty"|].
 
 (** * Later *)
 Tactic Notation "iNext" open_constr(n) :=
+  iStartProof;
   let P := match goal with |- _ ⊢ ?P => P end in
   try lazymatch n with 0 => fail 1 "iNext: cannot strip 0 laters" end;
   eapply (tac_next _ _ n);
@@ -632,6 +641,7 @@ Tactic Notation "iNext":= iNext _.
 
 (** * Update modality *)
 Tactic Notation "iModIntro" :=
+  iStartProof;
   eapply tac_modal_intro;
     [let P := match goal with |- IntoModal _ ?P => P end in
      apply _ || fail "iModIntro:" P "not a modality"|].
@@ -775,11 +785,11 @@ Tactic Notation "iIntros" constr(pat) :=
     | ?pat :: ?pats =>
        let H := iFresh in iIntro H; iDestructHyp H as pat; go pats
     end
-  in let pats := intro_pat.parse pat in try iProof; go pats.
+  in let pats := intro_pat.parse pat in iStartProof; go pats.
 Tactic Notation "iIntros" := iIntros [IAll].
 
 Tactic Notation "iIntros" "(" simple_intropattern(x1) ")" :=
-  try iProof; iIntro ( x1 ).
+  try iStartProof; iIntro ( x1 ).
 Tactic Notation "iIntros" "(" simple_intropattern(x1)
     simple_intropattern(x2) ")" :=
   iIntros ( x1 ); iIntro ( x2 ).
@@ -908,7 +918,7 @@ Tactic Notation "iDestructCore" open_constr(lem) "as" constr(p) tactic(tac) :=
       | 0 => fail "iDestruct: cannot introduce" n "hypotheses"
       | 1 => repeat iIntroForall; let H := iFresh in iIntro H; tac H
       | S ?n' => repeat iIntroForall; let H := iFresh in iIntro H; go n'
-      end in intros; try iProof; go n in
+      end in intros; iStartProof; go n in
   lazymatch type of lem with
   | nat => intro_destruct lem
   | Z => (* to make it work in Z_scope. We should just be able to bind
@@ -1039,6 +1049,7 @@ Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
 
 (** * Löb Induction *)
 Tactic Notation "iLöbCore" "as" constr (IH) :=
+  iStartProof;
   eapply tac_löb with _ IH;
     [reflexivity || fail "iLöb: persistent context not empty"
     |env_cbv; reflexivity || fail "iLöb:" IH "not fresh"|].
@@ -1105,6 +1116,7 @@ Tactic Notation "iLöb" "as" constr (IH) "forall" "(" ident(x1) ident(x2)
 
 (** * Assert *)
 Tactic Notation "iAssertCore" open_constr(Q) "with" constr(Hs) "as" tactic(tac) :=
+  iStartProof;
   let H := iFresh in
   let Hs := spec_pat.parse Hs in
   lazymatch Hs with