Fix issue #56.

ProofMode.md

@@ -38,12 +38,17 @@ Context management
   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
-  put `P` in the context of the original goal. The specialization pattern
-  `spat` specifies which hypotheses will be consumed by proving `P`. The
-  introduction pattern `ipat` specifies how to eliminate `P`.
-- `iAssert P with "spat" as %cpat` : assert `P` and eliminate it using the Coq
-  introduction pattern `cpat`.
+- `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`.
+  In case all branches of `ipat` start with a `#` (which causes `P` to be moved
+  to the persistent context) or with an `%` (which causes `P` to be moved to the
+  pure Coq context), then one can use all hypotheses for proving `P` as well as
+  for proving the current goal.
+- `iAssert P as %cpat` : assert `P` and eliminate it using the Coq introduction
+  pattern `cpat`. All hypotheses can be used for proving `P` as well as for
+  proving the current goal.
 
 Introduction of logical connectives
 -----------------------------------
@@ -67,13 +72,16 @@ Elimination of logical connectives
 ----------------------------------
 
 - `iExFalso` : Ex falso sequitur quod libet.
-- `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 (x1 ... xn) "ipat"` : elimination of a series of
+  existential quantifiers using Coq introduction patterns `x1 ... xn`, and
+  elimination of an object level connective using the proof mode introduction
+  pattern `ipat`.
+  In case all branches of `ipat` start with a `#` (which causes the hypothesis
+  to be moved to the persistent context) or with an `%` (which causes the
+  hypothesis to be moved to the pure Coq context), then one can use all
+  hypotheses for proving the premises of `pm_trm`, as well as for proving the
+  resulting goal. Note that in this case the hypotheses still need to be
+  subdivided among the spatial premises.
 - `iDestruct pm_trm as %cpat` : elimination of a pure hypothesis using the Coq
   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

theories/proofmode/coq_tactics.v

@@ -608,13 +608,15 @@ Proof.
   by rewrite right_id HP HQ.
 Qed.
 
-Lemma tac_assert_persistent Δ Δ' j P Q :
-  envs_app true (Esnoc Enil j P) Δ = Some Δ' →
-  (Δ ⊢ P) → PersistentP P → (Δ' ⊢ Q) → Δ ⊢ Q.
+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.
 Proof.
-  intros ? HP ??.
-  rewrite -(idemp uPred_and Δ) {1}HP envs_app_sound //; simpl.
-  by rewrite right_id {1}(persistentP P) always_and_sep_l wand_elim_r.
+  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_pose_proof Δ Δ' j P Q :

theories/proofmode/intro_patterns.v

@@ -17,14 +17,6 @@ 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
-  | IList pps => forallb (forallb intro_pat_persistent) pps
-  | _ => false
-  end.
-
 Module intro_pat.
 Inductive token :=
   | TName : string → token
@@ -186,3 +178,20 @@ Ltac parse_one s :=
      end
   end.
 End intro_pat.
+
+Fixpoint intro_pat_persistent (p : intro_pat) :=
+  match p with
+  | IPureElim => true
+  | IAlwaysElim _ => true
+  | IList pps => forallb (forallb intro_pat_persistent) pps
+  | _ => false
+  end.
+
+Ltac intro_pat_persistent p :=
+  lazymatch type of p with
+  | intro_pat => eval cbv in (intro_pat_persistent p)
+  | string =>
+     let pat := intro_pat.parse_one p in
+     eval cbv in (intro_pat_persistent pat)
+  | _ => p
+  end.

theories/proofmode/tactics.v

@@ -325,18 +325,11 @@ Local Tactic Notation "iSpecializePat" constr(H) constr(pat) :=
          |go H1 pats]
     end in let pats := spec_pat.parse pat in go H pats.
 
-(* p = whether the conclusion of the specialized term is persistent. It can
-either be a Boolean or an introduction pattern, which will be coerced in true
-when it only contains `#` or `%` patterns at the top-level. *)
+(* The argument [p] denotes whether the conclusion of the specialized term is
+persistent. It can either be a Boolean or an introduction pattern, which will be
+coerced into [true] when it only contains `#` or `%` patterns at the top-level. *)
 Tactic Notation "iSpecializeCore" open_constr(t) "as" constr(p) tactic(tac) :=
-  let p :=
-    lazymatch type of p with
-    | intro_pat => eval cbv in (intro_pat_persistent p)
-    | string =>
-       let pat := intro_pat.parse_one p in
-       eval cbv in (intro_pat_persistent pat)
-    | _ => p
-    end in
+  let p := intro_pat_persistent p in
   lazymatch t with
   | ITrm ?H ?xs ?pat =>
     lazymatch type of H with
@@ -1122,41 +1115,61 @@ Tactic Notation "iLöb" "as" constr (IH) "forall" "(" ident(x1) ident(x2)
   iRevertIntros(x1 x2 x3 x4 x5 x6 x7 x8) Hs with (iLöbCore as IH).
 
 (** * Assert *)
-Tactic Notation "iAssertCore" open_constr(Q) "with" constr(Hs) "as" tactic(tac) :=
+(* The argument [p] denotes whether [Q] is persistent. It can either be a
+Boolean or an introduction pattern, which will be coerced into [true] when it
+only contains `#` or `%` patterns at the top-level. *)
+Tactic Notation "iAssertCore" open_constr(Q)
+    "with" constr(Hs) "as" constr(p) tactic(tac) :=
   iStartProof;
+  let p := intro_pat_persistent p in
   let H := iFresh in
   let Hs := spec_pat.parse Hs in
   lazymatch Hs with
   | [SGoalPersistent] =>
-     eapply tac_assert_persistent with _ H Q;
+     eapply tac_assert_persistent with _ _ _ true [] H Q;
        [env_cbv; reflexivity
+       |env_cbv; reflexivity
        |(*goal*)
        |apply _ || fail "iAssert:" Q "not persistent"
        |tac H]
   | [SGoal (SpecGoal ?m ?lr ?Hs_frame ?Hs)] =>
      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"
-        end
-       |env_cbv; reflexivity || fail "iAssert:" Hs "not found"
-       |env_cbv; reflexivity
-       |iFrame Hs_frame (*goal*)
-       |tac H]
+     match p with
+     | false =>
+       eapply tac_assert with _ _ _ lr Hs' H Q _;
+         [match m with
+          | false => apply elim_modal_dummy
+          | true => apply _ || fail "iAssert: goal not a modality"
+          end
+         |env_cbv; reflexivity || fail "iAssert:" Hs "not found"
+         |env_cbv; reflexivity
+         |iFrame Hs_frame (*goal*)
+         |tac H]
+     | true =>
+       eapply tac_assert_persistent with _ _ _ lr Hs' H Q;
+         [env_cbv; reflexivity
+         |env_cbv; reflexivity
+         |(*goal*)
+         |apply _ || fail "iAssert:" Q "not persistent"
+         |tac H]
+     end
   | ?pat => fail "iAssert: invalid pattern" pat
   end.
 
 Tactic Notation "iAssert" open_constr(Q) "with" constr(Hs) "as" constr(pat) :=
-  iAssertCore Q with Hs as (fun H => iDestructHyp H as pat).
+  iAssertCore Q with Hs as pat (fun H => iDestructHyp H as pat).
 Tactic Notation "iAssert" open_constr(Q) "as" constr(pat) :=
-  iAssert Q with "[]" as pat.
+  let p := intro_pat_persistent pat in
+  match p with
+  | true => iAssert Q with "[-]" as pat
+  | false => iAssert Q with "[]" as pat
+  end.
 
 Tactic Notation "iAssert" open_constr(Q) "with" constr(Hs)
     "as" "%" simple_intropattern(pat) :=
-  iAssertCore Q with Hs as (fun H => iPure H as 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.
+  iAssert Q with "[-]" as %pat.
 
 (** * Rewrite *)
 Local Ltac iRewriteFindPred :=

theories/tests/proofmode.v

@@ -105,3 +105,13 @@ End iris.
 Lemma demo_9 (M : ucmraT) (x y z : M) :
   ✓ x → ⌜y ≡ z⌝ -∗ (✓ x ∧ ✓ x ∧ y ≡ z : uPred M).
 Proof. iIntros (Hv) "Hxy". by iFrame (Hv Hv) "Hxy". Qed.
+
+Lemma demo_10 (M : ucmraT) (P Q : uPred M) : 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 as %_. { by iClear "HP HQ". }
+  iAssert True%I with "[HP]" as %_. { Fail iClear "HQ". by iClear "HP". }
+  done.
+Qed.