From 8c844e32f0424d1b5080dd6bcafe7b4231d80f6f Mon Sep 17 00:00:00 2001
From: Robbert Krebbers
Date: Wed, 28 Dec 2016 10:10:03 +0100
Subject: [PATCH] Fix issue #56.

ProofMode.md  34 +++++++++
theories/proofmode/coq_tactics.v  14 ++++
theories/proofmode/intro_patterns.v  25 +++++++
theories/proofmode/tactics.v  65 +++++++++++++++++
theories/tests/proofmode.v  10 +++++
5 files changed, 95 insertions(+), 53 deletions()
diff git a/ProofMode.md b/ProofMode.md
index 1ec85aae..a7fa7c43 100644
 a/ProofMode.md
+++ b/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
diff git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index c5170324..63e5989a 100644
 a/theories/proofmode/coq_tactics.v
+++ b/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 :
diff git a/theories/proofmode/intro_patterns.v b/theories/proofmode/intro_patterns.v
index 54a95c72..42760a8f 100644
 a/theories/proofmode/intro_patterns.v
+++ b/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.
diff git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 3d3c2b9b..d9aa76cd 100644
 a/theories/proofmode/tactics.v
+++ b/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 toplevel. *)
+(* 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 toplevel. *)
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 toplevel. *)
+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 :=
diff git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index 833b8fdc..9e8e37be 100644
 a/theories/tests/proofmode.v
+++ b/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.

GitLab